xref: /aosp_15_r20/external/emboss/compiler/front_end/expression_bounds.py (revision 99e0aae7469b87d12f0ad23e61142c2d74c1ef70)
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