1*99e0aae7SDavid Rees# Copyright 2019 Google LLC 2*99e0aae7SDavid Rees# 3*99e0aae7SDavid Rees# Licensed under the Apache License, Version 2.0 (the "License"); 4*99e0aae7SDavid Rees# you may not use this file except in compliance with the License. 5*99e0aae7SDavid Rees# You may obtain a copy of the License at 6*99e0aae7SDavid Rees# 7*99e0aae7SDavid Rees# https://www.apache.org/licenses/LICENSE-2.0 8*99e0aae7SDavid Rees# 9*99e0aae7SDavid Rees# Unless required by applicable law or agreed to in writing, software 10*99e0aae7SDavid Rees# distributed under the License is distributed on an "AS IS" BASIS, 11*99e0aae7SDavid Rees# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12*99e0aae7SDavid Rees# See the License for the specific language governing permissions and 13*99e0aae7SDavid Rees# limitations under the License. 14*99e0aae7SDavid Rees 15*99e0aae7SDavid Rees"""Functions for proving mathematical properties of expressions.""" 16*99e0aae7SDavid Rees 17*99e0aae7SDavid Reesimport math 18*99e0aae7SDavid Reesimport fractions 19*99e0aae7SDavid Reesimport operator 20*99e0aae7SDavid Rees 21*99e0aae7SDavid Reesfrom compiler.util import ir_data 22*99e0aae7SDavid Reesfrom compiler.util import ir_data_utils 23*99e0aae7SDavid Reesfrom compiler.util import ir_util 24*99e0aae7SDavid Reesfrom compiler.util import traverse_ir 25*99e0aae7SDavid Rees 26*99e0aae7SDavid Rees 27*99e0aae7SDavid Rees# Create a local alias for math.gcd with a fallback to fractions.gcd if it is 28*99e0aae7SDavid Rees# not available. This can be dropped if pre-3.5 Python support is dropped. 29*99e0aae7SDavid Reesif hasattr(math, 'gcd'): 30*99e0aae7SDavid Rees _math_gcd = math.gcd 31*99e0aae7SDavid Reeselse: 32*99e0aae7SDavid Rees _math_gcd = fractions.gcd 33*99e0aae7SDavid Rees 34*99e0aae7SDavid Rees 35*99e0aae7SDavid Reesdef compute_constraints_of_expression(expression, ir): 36*99e0aae7SDavid Rees """Adds appropriate bounding constraints to the given expression.""" 37*99e0aae7SDavid Rees if ir_util.is_constant_type(expression.type): 38*99e0aae7SDavid Rees return 39*99e0aae7SDavid Rees expression_variety = expression.WhichOneof("expression") 40*99e0aae7SDavid Rees if expression_variety == "constant": 41*99e0aae7SDavid Rees _compute_constant_value_of_constant(expression) 42*99e0aae7SDavid Rees elif expression_variety == "constant_reference": 43*99e0aae7SDavid Rees _compute_constant_value_of_constant_reference(expression, ir) 44*99e0aae7SDavid Rees elif expression_variety == "function": 45*99e0aae7SDavid Rees _compute_constraints_of_function(expression, ir) 46*99e0aae7SDavid Rees elif expression_variety == "field_reference": 47*99e0aae7SDavid Rees _compute_constraints_of_field_reference(expression, ir) 48*99e0aae7SDavid Rees elif expression_variety == "builtin_reference": 49*99e0aae7SDavid Rees _compute_constraints_of_builtin_value(expression) 50*99e0aae7SDavid Rees elif expression_variety == "boolean_constant": 51*99e0aae7SDavid Rees _compute_constant_value_of_boolean_constant(expression) 52*99e0aae7SDavid Rees else: 53*99e0aae7SDavid Rees assert False, "Unknown expression variety {!r}".format(expression_variety) 54*99e0aae7SDavid Rees if expression.type.WhichOneof("type") == "integer": 55*99e0aae7SDavid Rees _assert_integer_constraints(expression) 56*99e0aae7SDavid Rees 57*99e0aae7SDavid Rees 58*99e0aae7SDavid Reesdef _compute_constant_value_of_constant(expression): 59*99e0aae7SDavid Rees value = expression.constant.value 60*99e0aae7SDavid Rees expression.type.integer.modular_value = value 61*99e0aae7SDavid Rees expression.type.integer.minimum_value = value 62*99e0aae7SDavid Rees expression.type.integer.maximum_value = value 63*99e0aae7SDavid Rees expression.type.integer.modulus = "infinity" 64*99e0aae7SDavid Rees 65*99e0aae7SDavid Rees 66*99e0aae7SDavid Reesdef _compute_constant_value_of_constant_reference(expression, ir): 67*99e0aae7SDavid Rees referred_object = ir_util.find_object( 68*99e0aae7SDavid Rees expression.constant_reference.canonical_name, ir) 69*99e0aae7SDavid Rees expression = ir_data_utils.builder(expression) 70*99e0aae7SDavid Rees if isinstance(referred_object, ir_data.EnumValue): 71*99e0aae7SDavid Rees compute_constraints_of_expression(referred_object.value, ir) 72*99e0aae7SDavid Rees assert ir_util.is_constant(referred_object.value) 73*99e0aae7SDavid Rees new_value = str(ir_util.constant_value(referred_object.value)) 74*99e0aae7SDavid Rees expression.type.enumeration.value = new_value 75*99e0aae7SDavid Rees elif isinstance(referred_object, ir_data.Field): 76*99e0aae7SDavid Rees assert ir_util.field_is_virtual(referred_object), ( 77*99e0aae7SDavid Rees "Non-virtual non-enum-value constant reference should have been caught " 78*99e0aae7SDavid Rees "in type_check.py") 79*99e0aae7SDavid Rees compute_constraints_of_expression(referred_object.read_transform, ir) 80*99e0aae7SDavid Rees expression.type.CopyFrom(referred_object.read_transform.type) 81*99e0aae7SDavid Rees else: 82*99e0aae7SDavid Rees assert False, "Unexpected constant reference type." 83*99e0aae7SDavid Rees 84*99e0aae7SDavid Rees 85*99e0aae7SDavid Reesdef _compute_constraints_of_function(expression, ir): 86*99e0aae7SDavid Rees """Computes the known constraints of the result of a function.""" 87*99e0aae7SDavid Rees for arg in expression.function.args: 88*99e0aae7SDavid Rees compute_constraints_of_expression(arg, ir) 89*99e0aae7SDavid Rees op = expression.function.function 90*99e0aae7SDavid Rees if op in (ir_data.FunctionMapping.ADDITION, ir_data.FunctionMapping.SUBTRACTION): 91*99e0aae7SDavid Rees _compute_constraints_of_additive_operator(expression) 92*99e0aae7SDavid Rees elif op == ir_data.FunctionMapping.MULTIPLICATION: 93*99e0aae7SDavid Rees _compute_constraints_of_multiplicative_operator(expression) 94*99e0aae7SDavid Rees elif op in (ir_data.FunctionMapping.EQUALITY, ir_data.FunctionMapping.INEQUALITY, 95*99e0aae7SDavid Rees ir_data.FunctionMapping.LESS, ir_data.FunctionMapping.LESS_OR_EQUAL, 96*99e0aae7SDavid Rees ir_data.FunctionMapping.GREATER, ir_data.FunctionMapping.GREATER_OR_EQUAL, 97*99e0aae7SDavid Rees ir_data.FunctionMapping.AND, ir_data.FunctionMapping.OR): 98*99e0aae7SDavid Rees _compute_constant_value_of_comparison_operator(expression) 99*99e0aae7SDavid Rees elif op == ir_data.FunctionMapping.CHOICE: 100*99e0aae7SDavid Rees _compute_constraints_of_choice_operator(expression) 101*99e0aae7SDavid Rees elif op == ir_data.FunctionMapping.MAXIMUM: 102*99e0aae7SDavid Rees _compute_constraints_of_maximum_function(expression) 103*99e0aae7SDavid Rees elif op == ir_data.FunctionMapping.PRESENCE: 104*99e0aae7SDavid Rees _compute_constraints_of_existence_function(expression, ir) 105*99e0aae7SDavid Rees elif op in (ir_data.FunctionMapping.UPPER_BOUND, ir_data.FunctionMapping.LOWER_BOUND): 106*99e0aae7SDavid Rees _compute_constraints_of_bound_function(expression) 107*99e0aae7SDavid Rees else: 108*99e0aae7SDavid Rees assert False, "Unknown operator {!r}".format(op) 109*99e0aae7SDavid Rees 110*99e0aae7SDavid Rees 111*99e0aae7SDavid Reesdef _compute_constraints_of_existence_function(expression, ir): 112*99e0aae7SDavid Rees """Computes the constraints of a $has(field) expression.""" 113*99e0aae7SDavid Rees field_path = expression.function.args[0].field_reference.path[-1] 114*99e0aae7SDavid Rees field = ir_util.find_object(field_path, ir) 115*99e0aae7SDavid Rees compute_constraints_of_expression(field.existence_condition, ir) 116*99e0aae7SDavid Rees ir_data_utils.builder(expression).type.CopyFrom(field.existence_condition.type) 117*99e0aae7SDavid Rees 118*99e0aae7SDavid Rees 119*99e0aae7SDavid Reesdef _compute_constraints_of_field_reference(expression, ir): 120*99e0aae7SDavid Rees """Computes the constraints of a reference to a structure's field.""" 121*99e0aae7SDavid Rees field_path = expression.field_reference.path[-1] 122*99e0aae7SDavid Rees field = ir_util.find_object(field_path, ir) 123*99e0aae7SDavid Rees if isinstance(field, ir_data.Field) and ir_util.field_is_virtual(field): 124*99e0aae7SDavid Rees # References to virtual fields should have the virtual field's constraints 125*99e0aae7SDavid Rees # copied over. 126*99e0aae7SDavid Rees compute_constraints_of_expression(field.read_transform, ir) 127*99e0aae7SDavid Rees ir_data_utils.builder(expression).type.CopyFrom(field.read_transform.type) 128*99e0aae7SDavid Rees return 129*99e0aae7SDavid Rees # Non-virtual non-integer fields do not (yet) have constraints. 130*99e0aae7SDavid Rees if expression.type.WhichOneof("type") == "integer": 131*99e0aae7SDavid Rees # TODO(bolms): These lines will need to change when support is added for 132*99e0aae7SDavid Rees # fixed-point types. 133*99e0aae7SDavid Rees expression.type.integer.modulus = "1" 134*99e0aae7SDavid Rees expression.type.integer.modular_value = "0" 135*99e0aae7SDavid Rees type_definition = ir_util.find_parent_object(field_path, ir) 136*99e0aae7SDavid Rees if isinstance(field, ir_data.Field): 137*99e0aae7SDavid Rees referrent_type = field.type 138*99e0aae7SDavid Rees else: 139*99e0aae7SDavid Rees referrent_type = field.physical_type_alias 140*99e0aae7SDavid Rees if referrent_type.HasField("size_in_bits"): 141*99e0aae7SDavid Rees type_size = ir_util.constant_value(referrent_type.size_in_bits) 142*99e0aae7SDavid Rees else: 143*99e0aae7SDavid Rees field_size = ir_util.constant_value(field.location.size) 144*99e0aae7SDavid Rees if field_size is None: 145*99e0aae7SDavid Rees type_size = None 146*99e0aae7SDavid Rees else: 147*99e0aae7SDavid Rees type_size = field_size * type_definition.addressable_unit 148*99e0aae7SDavid Rees assert referrent_type.HasField("atomic_type"), field 149*99e0aae7SDavid Rees assert not referrent_type.atomic_type.reference.canonical_name.module_file 150*99e0aae7SDavid Rees _set_integer_constraints_from_physical_type( 151*99e0aae7SDavid Rees expression, referrent_type, type_size) 152*99e0aae7SDavid Rees 153*99e0aae7SDavid Rees 154*99e0aae7SDavid Reesdef _set_integer_constraints_from_physical_type( 155*99e0aae7SDavid Rees expression, physical_type, type_size): 156*99e0aae7SDavid Rees """Copies the integer constraints of an expression from a physical type.""" 157*99e0aae7SDavid Rees # SCAFFOLDING HACK: In order to keep changelists manageable, this hardcodes 158*99e0aae7SDavid Rees # the ranges for all of the Emboss Prelude integer types. This would break 159*99e0aae7SDavid Rees # any user-defined `external` integer types, but that feature isn't fully 160*99e0aae7SDavid Rees # implemented in the C++ backend, so it doesn't matter for now. 161*99e0aae7SDavid Rees # 162*99e0aae7SDavid Rees # Adding the attribute(s) for integer bounds will require new operators: 163*99e0aae7SDavid Rees # integer/flooring division, remainder, and exponentiation (2**N, 10**N). 164*99e0aae7SDavid Rees # 165*99e0aae7SDavid Rees # (Technically, there are a few sets of operators that would work: for 166*99e0aae7SDavid Rees # example, just the choice operator `?:` is sufficient, but very ugly. 167*99e0aae7SDavid Rees # Bitwise AND, bitshift, and exponentiation would also work, but `10**($bits 168*99e0aae7SDavid Rees # >> 2) * 2**($bits & 0b11) - 1` isn't quite as clear as `10**($bits // 4) * 169*99e0aae7SDavid Rees # 2**($bits % 4) - 1`, in my (bolms@) opinion.) 170*99e0aae7SDavid Rees # 171*99e0aae7SDavid Rees # TODO(bolms): Add a scheme for defining integer bounds on user-defined 172*99e0aae7SDavid Rees # external types. 173*99e0aae7SDavid Rees if type_size is None: 174*99e0aae7SDavid Rees # If the type_size is unknown, then we can't actually say anything about the 175*99e0aae7SDavid Rees # minimum and maximum values of the type. For UInt, Int, and Bcd, an error 176*99e0aae7SDavid Rees # will be thrown during the constraints check stage. 177*99e0aae7SDavid Rees expression.type.integer.minimum_value = "-infinity" 178*99e0aae7SDavid Rees expression.type.integer.maximum_value = "infinity" 179*99e0aae7SDavid Rees return 180*99e0aae7SDavid Rees name = tuple(physical_type.atomic_type.reference.canonical_name.object_path) 181*99e0aae7SDavid Rees if name == ("UInt",): 182*99e0aae7SDavid Rees expression.type.integer.minimum_value = "0" 183*99e0aae7SDavid Rees expression.type.integer.maximum_value = str(2**type_size - 1) 184*99e0aae7SDavid Rees elif name == ("Int",): 185*99e0aae7SDavid Rees expression.type.integer.minimum_value = str(-(2**(type_size - 1))) 186*99e0aae7SDavid Rees expression.type.integer.maximum_value = str(2**(type_size - 1) - 1) 187*99e0aae7SDavid Rees elif name == ("Bcd",): 188*99e0aae7SDavid Rees expression.type.integer.minimum_value = "0" 189*99e0aae7SDavid Rees expression.type.integer.maximum_value = str( 190*99e0aae7SDavid Rees 10**(type_size // 4) * 2**(type_size % 4) - 1) 191*99e0aae7SDavid Rees else: 192*99e0aae7SDavid Rees assert False, "Unknown integral type " + ".".join(name) 193*99e0aae7SDavid Rees 194*99e0aae7SDavid Rees 195*99e0aae7SDavid Reesdef _compute_constraints_of_parameter(parameter): 196*99e0aae7SDavid Rees if parameter.type.WhichOneof("type") == "integer": 197*99e0aae7SDavid Rees type_size = ir_util.constant_value( 198*99e0aae7SDavid Rees parameter.physical_type_alias.size_in_bits) 199*99e0aae7SDavid Rees _set_integer_constraints_from_physical_type( 200*99e0aae7SDavid Rees parameter, parameter.physical_type_alias, type_size) 201*99e0aae7SDavid Rees 202*99e0aae7SDavid Rees 203*99e0aae7SDavid Reesdef _compute_constraints_of_builtin_value(expression): 204*99e0aae7SDavid Rees """Computes the constraints of a builtin (like $static_size_in_bits).""" 205*99e0aae7SDavid Rees name = expression.builtin_reference.canonical_name.object_path[0] 206*99e0aae7SDavid Rees if name == "$static_size_in_bits": 207*99e0aae7SDavid Rees expression.type.integer.modulus = "1" 208*99e0aae7SDavid Rees expression.type.integer.modular_value = "0" 209*99e0aae7SDavid Rees expression.type.integer.minimum_value = "0" 210*99e0aae7SDavid Rees # The maximum theoretically-supported size of something is 2**64 bytes, 211*99e0aae7SDavid Rees # which is 2**64 * 8 bits. 212*99e0aae7SDavid Rees # 213*99e0aae7SDavid Rees # Really, $static_size_in_bits is only valid in expressions that have to be 214*99e0aae7SDavid Rees # evaluated at compile time anyway, so it doesn't really matter if the 215*99e0aae7SDavid Rees # bounds are excessive. 216*99e0aae7SDavid Rees expression.type.integer.maximum_value = "infinity" 217*99e0aae7SDavid Rees elif name == "$is_statically_sized": 218*99e0aae7SDavid Rees # No bounds on a boolean variable. 219*99e0aae7SDavid Rees pass 220*99e0aae7SDavid Rees elif name == "$logical_value": 221*99e0aae7SDavid Rees # $logical_value is the placeholder used in inferred write-through 222*99e0aae7SDavid Rees # transformations. 223*99e0aae7SDavid Rees # 224*99e0aae7SDavid Rees # Only integers (currently) have "real" write-through transformations, but 225*99e0aae7SDavid Rees # fields that would otherwise be straight aliases, but which have a 226*99e0aae7SDavid Rees # [requires] attribute, are elevated to write-through fields, so that the 227*99e0aae7SDavid Rees # [requires] clause can be checked in Write, CouldWriteValue, TryToWrite, 228*99e0aae7SDavid Rees # Read, and Ok. 229*99e0aae7SDavid Rees if expression.type.WhichOneof("type") == "integer": 230*99e0aae7SDavid Rees assert expression.type.integer.modulus 231*99e0aae7SDavid Rees assert expression.type.integer.modular_value 232*99e0aae7SDavid Rees assert expression.type.integer.minimum_value 233*99e0aae7SDavid Rees assert expression.type.integer.maximum_value 234*99e0aae7SDavid Rees elif expression.type.WhichOneof("type") == "enumeration": 235*99e0aae7SDavid Rees assert expression.type.enumeration.name 236*99e0aae7SDavid Rees elif expression.type.WhichOneof("type") == "boolean": 237*99e0aae7SDavid Rees pass 238*99e0aae7SDavid Rees else: 239*99e0aae7SDavid Rees assert False, "Unexpected type for $logical_value" 240*99e0aae7SDavid Rees else: 241*99e0aae7SDavid Rees assert False, "Unknown builtin " + name 242*99e0aae7SDavid Rees 243*99e0aae7SDavid Rees 244*99e0aae7SDavid Reesdef _compute_constant_value_of_boolean_constant(expression): 245*99e0aae7SDavid Rees expression.type.boolean.value = expression.boolean_constant.value 246*99e0aae7SDavid Rees 247*99e0aae7SDavid Rees 248*99e0aae7SDavid Reesdef _add(a, b): 249*99e0aae7SDavid Rees """Adds a and b, where a and b are ints, "infinity", or "-infinity".""" 250*99e0aae7SDavid Rees if a in ("infinity", "-infinity"): 251*99e0aae7SDavid Rees a, b = b, a 252*99e0aae7SDavid Rees if b == "infinity": 253*99e0aae7SDavid Rees assert a != "-infinity" 254*99e0aae7SDavid Rees return "infinity" 255*99e0aae7SDavid Rees if b == "-infinity": 256*99e0aae7SDavid Rees assert a != "infinity" 257*99e0aae7SDavid Rees return "-infinity" 258*99e0aae7SDavid Rees return int(a) + int(b) 259*99e0aae7SDavid Rees 260*99e0aae7SDavid Rees 261*99e0aae7SDavid Reesdef _sub(a, b): 262*99e0aae7SDavid Rees """Subtracts b from a, where a and b are ints, "infinity", or "-infinity".""" 263*99e0aae7SDavid Rees if b == "infinity": 264*99e0aae7SDavid Rees return _add(a, "-infinity") 265*99e0aae7SDavid Rees if b == "-infinity": 266*99e0aae7SDavid Rees return _add(a, "infinity") 267*99e0aae7SDavid Rees return _add(a, -int(b)) 268*99e0aae7SDavid Rees 269*99e0aae7SDavid Rees 270*99e0aae7SDavid Reesdef _sign(a): 271*99e0aae7SDavid Rees """Returns 1 if a > 0, 0 if a == 0, and -1 if a < 0.""" 272*99e0aae7SDavid Rees if a == "infinity": 273*99e0aae7SDavid Rees return 1 274*99e0aae7SDavid Rees if a == "-infinity": 275*99e0aae7SDavid Rees return -1 276*99e0aae7SDavid Rees if int(a) > 0: 277*99e0aae7SDavid Rees return 1 278*99e0aae7SDavid Rees if int(a) < 0: 279*99e0aae7SDavid Rees return -1 280*99e0aae7SDavid Rees return 0 281*99e0aae7SDavid Rees 282*99e0aae7SDavid Rees 283*99e0aae7SDavid Reesdef _mul(a, b): 284*99e0aae7SDavid Rees """Multiplies a and b, where a and b are ints, "infinity", or "-infinity".""" 285*99e0aae7SDavid Rees if _is_infinite(a): 286*99e0aae7SDavid Rees a, b = b, a 287*99e0aae7SDavid Rees if _is_infinite(b): 288*99e0aae7SDavid Rees sign = _sign(a) * _sign(b) 289*99e0aae7SDavid Rees if sign > 0: 290*99e0aae7SDavid Rees return "infinity" 291*99e0aae7SDavid Rees if sign < 0: 292*99e0aae7SDavid Rees return "-infinity" 293*99e0aae7SDavid Rees return 0 294*99e0aae7SDavid Rees return int(a) * int(b) 295*99e0aae7SDavid Rees 296*99e0aae7SDavid Rees 297*99e0aae7SDavid Reesdef _is_infinite(a): 298*99e0aae7SDavid Rees return a in ("infinity", "-infinity") 299*99e0aae7SDavid Rees 300*99e0aae7SDavid Rees 301*99e0aae7SDavid Reesdef _max(a): 302*99e0aae7SDavid Rees """Returns max of a, where elements are ints, "infinity", or "-infinity".""" 303*99e0aae7SDavid Rees if any(n == "infinity" for n in a): 304*99e0aae7SDavid Rees return "infinity" 305*99e0aae7SDavid Rees if all(n == "-infinity" for n in a): 306*99e0aae7SDavid Rees return "-infinity" 307*99e0aae7SDavid Rees return max(int(n) for n in a if not _is_infinite(n)) 308*99e0aae7SDavid Rees 309*99e0aae7SDavid Rees 310*99e0aae7SDavid Reesdef _min(a): 311*99e0aae7SDavid Rees """Returns min of a, where elements are ints, "infinity", or "-infinity".""" 312*99e0aae7SDavid Rees if any(n == "-infinity" for n in a): 313*99e0aae7SDavid Rees return "-infinity" 314*99e0aae7SDavid Rees if all(n == "infinity" for n in a): 315*99e0aae7SDavid Rees return "infinity" 316*99e0aae7SDavid Rees return min(int(n) for n in a if not _is_infinite(n)) 317*99e0aae7SDavid Rees 318*99e0aae7SDavid Rees 319*99e0aae7SDavid Reesdef _compute_constraints_of_additive_operator(expression): 320*99e0aae7SDavid Rees """Computes the modular value of an additive expression.""" 321*99e0aae7SDavid Rees funcs = { 322*99e0aae7SDavid Rees ir_data.FunctionMapping.ADDITION: _add, 323*99e0aae7SDavid Rees ir_data.FunctionMapping.SUBTRACTION: _sub, 324*99e0aae7SDavid Rees } 325*99e0aae7SDavid Rees func = funcs[expression.function.function] 326*99e0aae7SDavid Rees args = expression.function.args 327*99e0aae7SDavid Rees for arg in args: 328*99e0aae7SDavid Rees assert arg.type.integer.modular_value, str(expression) 329*99e0aae7SDavid Rees left, right = args 330*99e0aae7SDavid Rees unadjusted_modular_value = func(left.type.integer.modular_value, 331*99e0aae7SDavid Rees right.type.integer.modular_value) 332*99e0aae7SDavid Rees new_modulus = _greatest_common_divisor(left.type.integer.modulus, 333*99e0aae7SDavid Rees right.type.integer.modulus) 334*99e0aae7SDavid Rees expression.type.integer.modulus = str(new_modulus) 335*99e0aae7SDavid Rees if new_modulus == "infinity": 336*99e0aae7SDavid Rees expression.type.integer.modular_value = str(unadjusted_modular_value) 337*99e0aae7SDavid Rees else: 338*99e0aae7SDavid Rees expression.type.integer.modular_value = str(unadjusted_modular_value % 339*99e0aae7SDavid Rees new_modulus) 340*99e0aae7SDavid Rees lmax = left.type.integer.maximum_value 341*99e0aae7SDavid Rees lmin = left.type.integer.minimum_value 342*99e0aae7SDavid Rees if expression.function.function == ir_data.FunctionMapping.SUBTRACTION: 343*99e0aae7SDavid Rees rmax = right.type.integer.minimum_value 344*99e0aae7SDavid Rees rmin = right.type.integer.maximum_value 345*99e0aae7SDavid Rees else: 346*99e0aae7SDavid Rees rmax = right.type.integer.maximum_value 347*99e0aae7SDavid Rees rmin = right.type.integer.minimum_value 348*99e0aae7SDavid Rees expression.type.integer.minimum_value = str(func(lmin, rmin)) 349*99e0aae7SDavid Rees expression.type.integer.maximum_value = str(func(lmax, rmax)) 350*99e0aae7SDavid Rees 351*99e0aae7SDavid Rees 352*99e0aae7SDavid Reesdef _compute_constraints_of_multiplicative_operator(expression): 353*99e0aae7SDavid Rees """Computes the modular value of a multiplicative expression.""" 354*99e0aae7SDavid Rees bounds = [arg.type.integer for arg in expression.function.args] 355*99e0aae7SDavid Rees 356*99e0aae7SDavid Rees # The minimum and maximum values can come from any of the four pairings of 357*99e0aae7SDavid Rees # (left min, left max) with (right min, right max), depending on the signs and 358*99e0aae7SDavid Rees # magnitudes of the minima and maxima. E.g.: 359*99e0aae7SDavid Rees # 360*99e0aae7SDavid Rees # max = left max * right max: [ 2, 3] * [ 2, 3] 361*99e0aae7SDavid Rees # max = left min * right min: [-3, -2] * [-3, -2] 362*99e0aae7SDavid Rees # max = left max * right min: [-3, -2] * [ 2, 3] 363*99e0aae7SDavid Rees # max = left min * right max: [ 2, 3] * [-3, -2] 364*99e0aae7SDavid Rees # max = left max * right max: [-2, 3] * [-2, 3] 365*99e0aae7SDavid Rees # max = left min * right min: [-3, 2] * [-3, 2] 366*99e0aae7SDavid Rees # 367*99e0aae7SDavid Rees # For uncorrelated multiplication, the minimum and maximum will always come 368*99e0aae7SDavid Rees # from multiplying one extreme by another: if x is nonzero, then 369*99e0aae7SDavid Rees # 370*99e0aae7SDavid Rees # (y + e) * x > y * x || (y - e) * x > y * x 371*99e0aae7SDavid Rees # 372*99e0aae7SDavid Rees # for arbitrary nonzero e, so the extrema can only occur when we either cannot 373*99e0aae7SDavid Rees # add or cannot subtract e. 374*99e0aae7SDavid Rees # 375*99e0aae7SDavid Rees # Correlated multiplication (e.g., `x * x`) can have tighter bounds, but 376*99e0aae7SDavid Rees # Emboss is not currently trying to be that smart. 377*99e0aae7SDavid Rees lmin, lmax = bounds[0].minimum_value, bounds[0].maximum_value 378*99e0aae7SDavid Rees rmin, rmax = bounds[1].minimum_value, bounds[1].maximum_value 379*99e0aae7SDavid Rees extrema = [_mul(lmax, rmax), _mul(lmin, rmax), # 380*99e0aae7SDavid Rees _mul(lmax, rmin), _mul(lmin, rmin)] 381*99e0aae7SDavid Rees expression.type.integer.minimum_value = str(_min(extrema)) 382*99e0aae7SDavid Rees expression.type.integer.maximum_value = str(_max(extrema)) 383*99e0aae7SDavid Rees 384*99e0aae7SDavid Rees if all(bound.modulus == "infinity" for bound in bounds): 385*99e0aae7SDavid Rees # If both sides are constant, the result is constant. 386*99e0aae7SDavid Rees expression.type.integer.modulus = "infinity" 387*99e0aae7SDavid Rees expression.type.integer.modular_value = str(int(bounds[0].modular_value) * 388*99e0aae7SDavid Rees int(bounds[1].modular_value)) 389*99e0aae7SDavid Rees return 390*99e0aae7SDavid Rees 391*99e0aae7SDavid Rees if any(bound.modulus == "infinity" for bound in bounds): 392*99e0aae7SDavid Rees # If one side is constant and the other is not, then the non-constant 393*99e0aae7SDavid Rees # modulus and modular_value can both be multiplied by the constant. E.g., 394*99e0aae7SDavid Rees # if `a` is congruent to 3 mod 5, then `4 * a` will be congruent to 12 mod 395*99e0aae7SDavid Rees # 20: 396*99e0aae7SDavid Rees # 397*99e0aae7SDavid Rees # a = ... | 4 * a = ... | 4 * a mod 20 = ... 398*99e0aae7SDavid Rees # 3 | 12 | 12 399*99e0aae7SDavid Rees # 8 | 32 | 12 400*99e0aae7SDavid Rees # 13 | 52 | 12 401*99e0aae7SDavid Rees # 18 | 72 | 12 402*99e0aae7SDavid Rees # 23 | 92 | 12 403*99e0aae7SDavid Rees # 28 | 112 | 12 404*99e0aae7SDavid Rees # 33 | 132 | 12 405*99e0aae7SDavid Rees # 406*99e0aae7SDavid Rees # This is trivially shown by noting that the difference between consecutive 407*99e0aae7SDavid Rees # possible values for `4 * a` always differ by 20. 408*99e0aae7SDavid Rees if bounds[0].modulus == "infinity": 409*99e0aae7SDavid Rees constant, variable = bounds 410*99e0aae7SDavid Rees else: 411*99e0aae7SDavid Rees variable, constant = bounds 412*99e0aae7SDavid Rees if int(constant.modular_value) == 0: 413*99e0aae7SDavid Rees # If the constant is 0, the result is 0, no matter what the variable side 414*99e0aae7SDavid Rees # is. 415*99e0aae7SDavid Rees expression.type.integer.modulus = "infinity" 416*99e0aae7SDavid Rees expression.type.integer.modular_value = "0" 417*99e0aae7SDavid Rees return 418*99e0aae7SDavid Rees new_modulus = int(variable.modulus) * abs(int(constant.modular_value)) 419*99e0aae7SDavid Rees expression.type.integer.modulus = str(new_modulus) 420*99e0aae7SDavid Rees # The `% new_modulus` will force the `modular_value` to be positive, even 421*99e0aae7SDavid Rees # when `constant.modular_value` is negative. 422*99e0aae7SDavid Rees expression.type.integer.modular_value = str( 423*99e0aae7SDavid Rees int(variable.modular_value) * int(constant.modular_value) % new_modulus) 424*99e0aae7SDavid Rees return 425*99e0aae7SDavid Rees 426*99e0aae7SDavid Rees # If neither side is constant, then the result is more complex. Full proof is 427*99e0aae7SDavid Rees # available in g3doc/modular_congruence_multiplication_proof.md 428*99e0aae7SDavid Rees # 429*99e0aae7SDavid Rees # Essentially, if: 430*99e0aae7SDavid Rees # 431*99e0aae7SDavid Rees # l == _ * l_mod + l_mv 432*99e0aae7SDavid Rees # r == _ * r_mod + r_mv 433*99e0aae7SDavid Rees # 434*99e0aae7SDavid Rees # Then we find l_mod0 and r_mod0 in: 435*99e0aae7SDavid Rees # 436*99e0aae7SDavid Rees # l == (_ * l_mod_nz + l_mv_nz) * l_mod0 437*99e0aae7SDavid Rees # r == (_ * r_mod_nz + r_mv_nz) * r_mod0 438*99e0aae7SDavid Rees # 439*99e0aae7SDavid Rees # And finally conclude: 440*99e0aae7SDavid Rees # 441*99e0aae7SDavid Rees # l * r == _ * GCD(l_mod_nz, r_mod_nz) * l_mod0 * r_mod0 + l_mv * r_mv 442*99e0aae7SDavid Rees product_of_zero_congruence_moduli = 1 443*99e0aae7SDavid Rees product_of_modular_values = 1 444*99e0aae7SDavid Rees nonzero_congruence_moduli = [] 445*99e0aae7SDavid Rees for bound in bounds: 446*99e0aae7SDavid Rees zero_congruence_modulus = _greatest_common_divisor(bound.modulus, 447*99e0aae7SDavid Rees bound.modular_value) 448*99e0aae7SDavid Rees assert int(bound.modulus) % zero_congruence_modulus == 0 449*99e0aae7SDavid Rees product_of_zero_congruence_moduli *= zero_congruence_modulus 450*99e0aae7SDavid Rees product_of_modular_values *= int(bound.modular_value) 451*99e0aae7SDavid Rees nonzero_congruence_moduli.append(int(bound.modulus) // 452*99e0aae7SDavid Rees zero_congruence_modulus) 453*99e0aae7SDavid Rees shared_nonzero_congruence_modulus = _greatest_common_divisor( 454*99e0aae7SDavid Rees nonzero_congruence_moduli[0], nonzero_congruence_moduli[1]) 455*99e0aae7SDavid Rees final_modulus = (shared_nonzero_congruence_modulus * 456*99e0aae7SDavid Rees product_of_zero_congruence_moduli) 457*99e0aae7SDavid Rees expression.type.integer.modulus = str(final_modulus) 458*99e0aae7SDavid Rees expression.type.integer.modular_value = str(product_of_modular_values % 459*99e0aae7SDavid Rees final_modulus) 460*99e0aae7SDavid Rees 461*99e0aae7SDavid Rees 462*99e0aae7SDavid Reesdef _assert_integer_constraints(expression): 463*99e0aae7SDavid Rees """Asserts that the integer bounds of expression are self-consistent. 464*99e0aae7SDavid Rees 465*99e0aae7SDavid Rees Asserts that `minimum_value` and `maximum_value` are congruent to 466*99e0aae7SDavid Rees `modular_value` modulo `modulus`. 467*99e0aae7SDavid Rees 468*99e0aae7SDavid Rees If `modulus` is "infinity", asserts that `minimum_value`, `maximum_value`, and 469*99e0aae7SDavid Rees `modular_value` are all equal. 470*99e0aae7SDavid Rees 471*99e0aae7SDavid Rees If `minimum_value` is equal to `maximum_value`, asserts that `modular_value` 472*99e0aae7SDavid Rees is equal to both, and that `modulus` is "infinity". 473*99e0aae7SDavid Rees 474*99e0aae7SDavid Rees Arguments: 475*99e0aae7SDavid Rees expression: an expression with type.integer 476*99e0aae7SDavid Rees 477*99e0aae7SDavid Rees Returns: 478*99e0aae7SDavid Rees None 479*99e0aae7SDavid Rees """ 480*99e0aae7SDavid Rees bounds = expression.type.integer 481*99e0aae7SDavid Rees if bounds.modulus == "infinity": 482*99e0aae7SDavid Rees assert bounds.minimum_value == bounds.modular_value 483*99e0aae7SDavid Rees assert bounds.maximum_value == bounds.modular_value 484*99e0aae7SDavid Rees return 485*99e0aae7SDavid Rees modulus = int(bounds.modulus) 486*99e0aae7SDavid Rees assert modulus > 0 487*99e0aae7SDavid Rees if bounds.minimum_value != "-infinity": 488*99e0aae7SDavid Rees assert int(bounds.minimum_value) % modulus == int(bounds.modular_value) 489*99e0aae7SDavid Rees if bounds.maximum_value != "infinity": 490*99e0aae7SDavid Rees assert int(bounds.maximum_value) % modulus == int(bounds.modular_value) 491*99e0aae7SDavid Rees if bounds.minimum_value == bounds.maximum_value: 492*99e0aae7SDavid Rees # TODO(bolms): I believe there are situations using the not-yet-implemented 493*99e0aae7SDavid Rees # integer division operator that would trigger these asserts, so they should 494*99e0aae7SDavid Rees # be turned into assignments (with corresponding tests) when implementing 495*99e0aae7SDavid Rees # division. 496*99e0aae7SDavid Rees assert bounds.modular_value == bounds.minimum_value 497*99e0aae7SDavid Rees assert bounds.modulus == "infinity" 498*99e0aae7SDavid Rees if bounds.minimum_value != "-infinity" and bounds.maximum_value != "infinity": 499*99e0aae7SDavid Rees assert int(bounds.minimum_value) <= int(bounds.maximum_value) 500*99e0aae7SDavid Rees 501*99e0aae7SDavid Rees 502*99e0aae7SDavid Reesdef _compute_constant_value_of_comparison_operator(expression): 503*99e0aae7SDavid Rees """Computes the constant value, if any, of a comparison operator.""" 504*99e0aae7SDavid Rees args = expression.function.args 505*99e0aae7SDavid Rees if all(ir_util.is_constant(arg) for arg in args): 506*99e0aae7SDavid Rees functions = { 507*99e0aae7SDavid Rees ir_data.FunctionMapping.EQUALITY: operator.eq, 508*99e0aae7SDavid Rees ir_data.FunctionMapping.INEQUALITY: operator.ne, 509*99e0aae7SDavid Rees ir_data.FunctionMapping.LESS: operator.lt, 510*99e0aae7SDavid Rees ir_data.FunctionMapping.LESS_OR_EQUAL: operator.le, 511*99e0aae7SDavid Rees ir_data.FunctionMapping.GREATER: operator.gt, 512*99e0aae7SDavid Rees ir_data.FunctionMapping.GREATER_OR_EQUAL: operator.ge, 513*99e0aae7SDavid Rees ir_data.FunctionMapping.AND: operator.and_, 514*99e0aae7SDavid Rees ir_data.FunctionMapping.OR: operator.or_, 515*99e0aae7SDavid Rees } 516*99e0aae7SDavid Rees func = functions[expression.function.function] 517*99e0aae7SDavid Rees expression.type.boolean.value = func( 518*99e0aae7SDavid Rees *[ir_util.constant_value(arg) for arg in args]) 519*99e0aae7SDavid Rees 520*99e0aae7SDavid Rees 521*99e0aae7SDavid Reesdef _compute_constraints_of_bound_function(expression): 522*99e0aae7SDavid Rees """Computes the constraints of $upper_bound or $lower_bound.""" 523*99e0aae7SDavid Rees if expression.function.function == ir_data.FunctionMapping.UPPER_BOUND: 524*99e0aae7SDavid Rees value = expression.function.args[0].type.integer.maximum_value 525*99e0aae7SDavid Rees elif expression.function.function == ir_data.FunctionMapping.LOWER_BOUND: 526*99e0aae7SDavid Rees value = expression.function.args[0].type.integer.minimum_value 527*99e0aae7SDavid Rees else: 528*99e0aae7SDavid Rees assert False, "Non-bound function" 529*99e0aae7SDavid Rees expression.type.integer.minimum_value = value 530*99e0aae7SDavid Rees expression.type.integer.maximum_value = value 531*99e0aae7SDavid Rees expression.type.integer.modular_value = value 532*99e0aae7SDavid Rees expression.type.integer.modulus = "infinity" 533*99e0aae7SDavid Rees 534*99e0aae7SDavid Rees 535*99e0aae7SDavid Reesdef _compute_constraints_of_maximum_function(expression): 536*99e0aae7SDavid Rees """Computes the constraints of the $max function.""" 537*99e0aae7SDavid Rees assert expression.type.WhichOneof("type") == "integer" 538*99e0aae7SDavid Rees args = expression.function.args 539*99e0aae7SDavid Rees assert args[0].type.WhichOneof("type") == "integer" 540*99e0aae7SDavid Rees # The minimum value of the result occurs when every argument takes its minimum 541*99e0aae7SDavid Rees # value, which means that the minimum result is the maximum-of-minimums. 542*99e0aae7SDavid Rees expression.type.integer.minimum_value = str(_max( 543*99e0aae7SDavid Rees [arg.type.integer.minimum_value for arg in args])) 544*99e0aae7SDavid Rees # The maximum result is the maximum-of-maximums. 545*99e0aae7SDavid Rees expression.type.integer.maximum_value = str(_max( 546*99e0aae7SDavid Rees [arg.type.integer.maximum_value for arg in args])) 547*99e0aae7SDavid Rees # If the expression is dominated by a constant factor, then the result is 548*99e0aae7SDavid Rees # constant. I (bolms@) believe this is the only case where 549*99e0aae7SDavid Rees # _compute_constraints_of_maximum_function might violate the assertions in 550*99e0aae7SDavid Rees # _assert_integer_constraints. 551*99e0aae7SDavid Rees if (expression.type.integer.minimum_value == 552*99e0aae7SDavid Rees expression.type.integer.maximum_value): 553*99e0aae7SDavid Rees expression.type.integer.modular_value = ( 554*99e0aae7SDavid Rees expression.type.integer.minimum_value) 555*99e0aae7SDavid Rees expression.type.integer.modulus = "infinity" 556*99e0aae7SDavid Rees return 557*99e0aae7SDavid Rees result_modulus = args[0].type.integer.modulus 558*99e0aae7SDavid Rees result_modular_value = args[0].type.integer.modular_value 559*99e0aae7SDavid Rees # The result of $max(a, b) could be either a or b, which means that the result 560*99e0aae7SDavid Rees # of $max(a, b) uses the _shared_modular_value() of a and b, just like the 561*99e0aae7SDavid Rees # choice operator '?:'. 562*99e0aae7SDavid Rees # 563*99e0aae7SDavid Rees # This also takes advantage of the fact that $max(a, b, c, d, ...) is 564*99e0aae7SDavid Rees # equivalent to $max(a, $max(b, $max(c, $max(d, ...)))), so it is valid to 565*99e0aae7SDavid Rees # call _shared_modular_value() in a loop. 566*99e0aae7SDavid Rees for arg in args[1:]: 567*99e0aae7SDavid Rees # TODO(bolms): I think the bounds could be tigher in some cases where 568*99e0aae7SDavid Rees # arg.maximum_value is less than the new expression.minimum_value, and 569*99e0aae7SDavid Rees # in some very specific cases where arg.maximum_value is greater than the 570*99e0aae7SDavid Rees # new expression.minimum_value, but arg.maximum_value - arg.modulus is less 571*99e0aae7SDavid Rees # than expression.minimum_value. 572*99e0aae7SDavid Rees result_modulus, result_modular_value = _shared_modular_value( 573*99e0aae7SDavid Rees (result_modulus, result_modular_value), 574*99e0aae7SDavid Rees (arg.type.integer.modulus, arg.type.integer.modular_value)) 575*99e0aae7SDavid Rees expression.type.integer.modulus = str(result_modulus) 576*99e0aae7SDavid Rees expression.type.integer.modular_value = str(result_modular_value) 577*99e0aae7SDavid Rees 578*99e0aae7SDavid Rees 579*99e0aae7SDavid Reesdef _shared_modular_value(left, right): 580*99e0aae7SDavid Rees """Returns the shared modulus and modular value of left and right. 581*99e0aae7SDavid Rees 582*99e0aae7SDavid Rees Arguments: 583*99e0aae7SDavid Rees left: A tuple of (modulus, modular value) 584*99e0aae7SDavid Rees right: A tuple of (modulus, modular value) 585*99e0aae7SDavid Rees 586*99e0aae7SDavid Rees Returns: 587*99e0aae7SDavid Rees A tuple of (modulus, modular_value) such that: 588*99e0aae7SDavid Rees 589*99e0aae7SDavid Rees left.modulus % result.modulus == 0 590*99e0aae7SDavid Rees right.modulus % result.modulus == 0 591*99e0aae7SDavid Rees left.modular_value % result.modulus = result.modular_value 592*99e0aae7SDavid Rees right.modular_value % result.modulus = result.modular_value 593*99e0aae7SDavid Rees 594*99e0aae7SDavid Rees That is, the result.modulus and result.modular_value will be compatible 595*99e0aae7SDavid Rees with, but (possibly) less restrictive than both left.(modulus, 596*99e0aae7SDavid Rees modular_value) and right.(modulus, modular_value). 597*99e0aae7SDavid Rees """ 598*99e0aae7SDavid Rees left_modulus, left_modular_value = left 599*99e0aae7SDavid Rees right_modulus, right_modular_value = right 600*99e0aae7SDavid Rees # The combined modulus is gcd(gcd(left_modulus, right_modulus), 601*99e0aae7SDavid Rees # left_modular_value - right_modular_value). 602*99e0aae7SDavid Rees # 603*99e0aae7SDavid Rees # The inner gcd normalizes the left_modulus and right_modulus, but can leave 604*99e0aae7SDavid Rees # incompatible modular_values. The outer gcd finds a modulus to which both 605*99e0aae7SDavid Rees # modular_values are congruent. Some examples: 606*99e0aae7SDavid Rees # 607*99e0aae7SDavid Rees # left | right | res 608*99e0aae7SDavid Rees # --------------+----------------+-------------------- 609*99e0aae7SDavid Rees # l % 12 == 7 | r % 20 == 15 | res % 4 == 3 610*99e0aae7SDavid Rees # l == 35 | r % 20 == 15 | res % 20 == 15 611*99e0aae7SDavid Rees # l % 24 == 15 | r % 12 == 7 | res % 4 == 3 612*99e0aae7SDavid Rees # l % 20 == 15 | r % 20 == 10 | res % 5 == 0 613*99e0aae7SDavid Rees # l % 20 == 16 | r % 20 == 11 | res % 5 == 1 614*99e0aae7SDavid Rees # l == 10 | r == 7 | res % 3 == 1 615*99e0aae7SDavid Rees # l == 4 | r == 4 | res == 4 616*99e0aae7SDavid Rees # 617*99e0aae7SDavid Rees # The cases where one side or the other are constant are handled 618*99e0aae7SDavid Rees # automatically by the fact that _greatest_common_divisor("infinity", x) 619*99e0aae7SDavid Rees # is x. 620*99e0aae7SDavid Rees common_modulus = _greatest_common_divisor(left_modulus, right_modulus) 621*99e0aae7SDavid Rees new_modulus = _greatest_common_divisor( 622*99e0aae7SDavid Rees common_modulus, abs(int(left_modular_value) - int(right_modular_value))) 623*99e0aae7SDavid Rees if new_modulus == "infinity": 624*99e0aae7SDavid Rees # The only way for the new_modulus to come out as "infinity" *should* be 625*99e0aae7SDavid Rees # if both if_true and if_false have the same constant value. 626*99e0aae7SDavid Rees assert left_modular_value == right_modular_value 627*99e0aae7SDavid Rees assert left_modulus == right_modulus == "infinity" 628*99e0aae7SDavid Rees return new_modulus, left_modular_value 629*99e0aae7SDavid Rees else: 630*99e0aae7SDavid Rees assert (int(left_modular_value) % new_modulus == 631*99e0aae7SDavid Rees int(right_modular_value) % new_modulus) 632*99e0aae7SDavid Rees return new_modulus, int(left_modular_value) % new_modulus 633*99e0aae7SDavid Rees 634*99e0aae7SDavid Rees 635*99e0aae7SDavid Reesdef _compute_constraints_of_choice_operator(expression): 636*99e0aae7SDavid Rees """Computes the constraints of a choice operation '?:'.""" 637*99e0aae7SDavid Rees condition, if_true, if_false = ir_data_utils.reader(expression).function.args 638*99e0aae7SDavid Rees expression = ir_data_utils.builder(expression) 639*99e0aae7SDavid Rees if condition.type.boolean.HasField("value"): 640*99e0aae7SDavid Rees # The generated expressions for $size_in_bits and $size_in_bytes look like 641*99e0aae7SDavid Rees # 642*99e0aae7SDavid Rees # $max((field1_existence_condition ? field1_start + field1_size : 0), 643*99e0aae7SDavid Rees # (field2_existence_condition ? field2_start + field2_size : 0), 644*99e0aae7SDavid Rees # (field3_existence_condition ? field3_start + field3_size : 0), 645*99e0aae7SDavid Rees # ...) 646*99e0aae7SDavid Rees # 647*99e0aae7SDavid Rees # Since most existence_conditions are just "true", it is important to select 648*99e0aae7SDavid Rees # the tighter bounds in those cases -- otherwise, only zero-length 649*99e0aae7SDavid Rees # structures could have a constant $size_in_bits or $size_in_bytes. 650*99e0aae7SDavid Rees side = if_true if condition.type.boolean.value else if_false 651*99e0aae7SDavid Rees expression.type.CopyFrom(side.type) 652*99e0aae7SDavid Rees return 653*99e0aae7SDavid Rees # The type.integer minimum_value/maximum_value bounding code is needed since 654*99e0aae7SDavid Rees # constraints.check_constraints() will complain if minimum and maximum are not 655*99e0aae7SDavid Rees # set correctly. I'm (bolms@) not sure if the modulus/modular_value pulls its 656*99e0aae7SDavid Rees # weight, but for completeness I've left it in. 657*99e0aae7SDavid Rees if if_true.type.WhichOneof("type") == "integer": 658*99e0aae7SDavid Rees # The minimum value of the choice is the minimum value of either side, and 659*99e0aae7SDavid Rees # the maximum is the maximum value of either side. 660*99e0aae7SDavid Rees expression.type.integer.minimum_value = str(_min([ 661*99e0aae7SDavid Rees if_true.type.integer.minimum_value, 662*99e0aae7SDavid Rees if_false.type.integer.minimum_value])) 663*99e0aae7SDavid Rees expression.type.integer.maximum_value = str(_max([ 664*99e0aae7SDavid Rees if_true.type.integer.maximum_value, 665*99e0aae7SDavid Rees if_false.type.integer.maximum_value])) 666*99e0aae7SDavid Rees new_modulus, new_modular_value = _shared_modular_value( 667*99e0aae7SDavid Rees (if_true.type.integer.modulus, if_true.type.integer.modular_value), 668*99e0aae7SDavid Rees (if_false.type.integer.modulus, if_false.type.integer.modular_value)) 669*99e0aae7SDavid Rees expression.type.integer.modulus = str(new_modulus) 670*99e0aae7SDavid Rees expression.type.integer.modular_value = str(new_modular_value) 671*99e0aae7SDavid Rees else: 672*99e0aae7SDavid Rees assert if_true.type.WhichOneof("type") in ("boolean", "enumeration"), ( 673*99e0aae7SDavid Rees "Unknown type {} for expression".format( 674*99e0aae7SDavid Rees if_true.type.WhichOneof("type"))) 675*99e0aae7SDavid Rees 676*99e0aae7SDavid Rees 677*99e0aae7SDavid Reesdef _greatest_common_divisor(a, b): 678*99e0aae7SDavid Rees """Returns the greatest common divisor of a and b. 679*99e0aae7SDavid Rees 680*99e0aae7SDavid Rees Arguments: 681*99e0aae7SDavid Rees a: an integer, a stringified integer, or the string "infinity" 682*99e0aae7SDavid Rees b: an integer, a stringified integer, or the string "infinity" 683*99e0aae7SDavid Rees 684*99e0aae7SDavid Rees Returns: 685*99e0aae7SDavid Rees Conceptually, "infinity" is treated as the product of all integers. 686*99e0aae7SDavid Rees 687*99e0aae7SDavid Rees If both a and b are 0, returns "infinity". 688*99e0aae7SDavid Rees 689*99e0aae7SDavid Rees Otherwise, if either a or b are "infinity", and the other is 0, returns 690*99e0aae7SDavid Rees "infinity". 691*99e0aae7SDavid Rees 692*99e0aae7SDavid Rees Otherwise, if either a or b are "infinity", returns the other. 693*99e0aae7SDavid Rees 694*99e0aae7SDavid Rees Otherwise, returns the greatest common divisor of a and b. 695*99e0aae7SDavid Rees """ 696*99e0aae7SDavid Rees if a != "infinity": a = int(a) 697*99e0aae7SDavid Rees if b != "infinity": b = int(b) 698*99e0aae7SDavid Rees assert a == "infinity" or a >= 0 699*99e0aae7SDavid Rees assert b == "infinity" or b >= 0 700*99e0aae7SDavid Rees if a == b == 0: return "infinity" 701*99e0aae7SDavid Rees # GCD(0, x) is always x, so it's safe to shortcut when a == 0 or b == 0. 702*99e0aae7SDavid Rees if a == 0: return b 703*99e0aae7SDavid Rees if b == 0: return a 704*99e0aae7SDavid Rees if a == "infinity": return b 705*99e0aae7SDavid Rees if b == "infinity": return a 706*99e0aae7SDavid Rees return _math_gcd(a, b) 707*99e0aae7SDavid Rees 708*99e0aae7SDavid Rees 709*99e0aae7SDavid Reesdef compute_constants(ir): 710*99e0aae7SDavid Rees """Computes constant values for all expressions in ir. 711*99e0aae7SDavid Rees 712*99e0aae7SDavid Rees compute_constants calculates all constant values and adds them to the type 713*99e0aae7SDavid Rees information for each expression and subexpression. 714*99e0aae7SDavid Rees 715*99e0aae7SDavid Rees Arguments: 716*99e0aae7SDavid Rees ir: an IR on which to compute constants 717*99e0aae7SDavid Rees 718*99e0aae7SDavid Rees Returns: 719*99e0aae7SDavid Rees A (possibly empty) list of errors. 720*99e0aae7SDavid Rees """ 721*99e0aae7SDavid Rees traverse_ir.fast_traverse_ir_top_down( 722*99e0aae7SDavid Rees ir, [ir_data.Expression], compute_constraints_of_expression, 723*99e0aae7SDavid Rees skip_descendants_of={ir_data.Expression}) 724*99e0aae7SDavid Rees traverse_ir.fast_traverse_ir_top_down( 725*99e0aae7SDavid Rees ir, [ir_data.RuntimeParameter], _compute_constraints_of_parameter, 726*99e0aae7SDavid Rees skip_descendants_of={ir_data.Expression}) 727*99e0aae7SDavid Rees return [] 728