Propagate an undefined value for possibly-zero ///% divisors

compiler/back_end/cpp/header_generator.py

@@ -836,16 +836,27 @@ def _render_expression(expression, ir, field_reader=None, subexpressions=None):
     # will fit into C++ types, or that operator arguments and return types can fit
     # in the same type: expressions like `-0x8000_0000_0000_0000` and
     # `0x1_0000_0000_0000_0000 - 1` can appear.
+    # A value that can be undefined must not be folded to a compile-time literal,
+    # even when its *defined* range collapses to a single value (modulus ==
+    # "infinity" / a fixed boolean): at runtime it may be Unknown (e.g. a
+    # division by zero), which only the real Maybe<>-returning computation can
+    # represent.
     if expression.type.which_type == "integer":
-        if expression.type.integer.modulus == "infinity":
+        if (
+            expression.type.integer.modulus == "infinity"
+            and not expression.type.integer.can_be_undefined
+        ):
             return _ExpressionResult(
                 _render_integer_for_expression(
                     int(expression.type.integer.modular_value)
                 ),
                 True,
             )
     elif expression.type.which_type == "boolean":
-        if expression.type.boolean.has_field("value"):
+        if (
+            expression.type.boolean.has_field("value")
+            and not expression.type.boolean.can_be_undefined
+        ):
             if expression.type.boolean.value:
                 return _ExpressionResult(_maybe_type("bool") + "(true)", True)
             else:
@@ -1415,9 +1426,15 @@ def _is_discriminant_provably_known(discrim_expr, fields):
         if ir_util.field_is_virtual(f):
             return False
         cond = f.existence_condition
+        # An existence condition that can be undefined is not provably known at
+        # runtime, so the Known() guard on the discriminant read must be kept.
+        # (In practice the boolean folder never sets `value` on a
+        # can-be-undefined condition, so this is belt-and-suspenders; it keeps
+        # the elision sound regardless of how folding evolves.)
         return (
             cond.type.which_type == "boolean"
             and cond.type.boolean.has_field("value")
+            and not cond.type.boolean.can_be_undefined
             and bool(cond.type.boolean.value)
         )
     return False

compiler/back_end/cpp/testcode/division_modulus_test.cc

@@ -89,6 +89,77 @@ TEST(ChunkedPayload, RoundsUpToMultipleOfFour) {
   EXPECT_EQ(8U, view.padded().ElementCount());
 }
 
+// A field whose size uses a `//` with a possibly-zero divisor works normally
+// when the divisor is nonzero.
+TEST(PayloadSizedByDivision, NonzeroDivisor) {
+  static constexpr ::std::array</**/ ::std::uint8_t, 5> kBuf = {{
+      0x04,                          // divisor = 4 -> 16 // 4 = 4 payload bytes
+      0xaa, 0xbb, 0xcc, 0xdd,        // payload
+  }};
+  auto view = MakePayloadSizedByDivisionView(&kBuf);
+  ASSERT_TRUE(view.Ok());
+  EXPECT_EQ(5U, view.SizeInBytes());
+  EXPECT_EQ(4U, view.payload().ElementCount());
+}
+
+// When the divisor is zero the payload size is undefined, so the structure's
+// size is unknown and Ok() is false -- with no division-by-zero UB.
+TEST(PayloadSizedByDivision, ZeroDivisorIsNotOk) {
+  static constexpr ::std::array</**/ ::std::uint8_t, 5> kBuf = {{
+      0x00,                          // divisor = 0 -> 16 // 0 undefined
+      0xaa, 0xbb, 0xcc, 0xdd,
+  }};
+  auto view = MakePayloadSizedByDivisionView(&kBuf);
+  EXPECT_FALSE(view.Ok());
+  EXPECT_FALSE(view.SizeIsKnown());
+  EXPECT_FALSE(view.IntrinsicSizeInBytes().Ok());
+}
+
+// A field guarded by an existence condition that divides by a field: the
+// condition (and therefore Ok()) is well-defined for nonzero divisors...
+TEST(FieldGatedByDivision, ConditionTrueAndFalse) {
+  // divisor = 4 -> 12 // 4 == 3 -> gated present.
+  static constexpr ::std::array</**/ ::std::uint8_t, 2> kPresent = {{0x04, 0x77}};
+  auto present = MakeFieldGatedByDivisionView(&kPresent);
+  ASSERT_TRUE(present.Ok());
+  EXPECT_TRUE(present.has_gated().ValueOr(false));
+  EXPECT_EQ(0x77U, present.gated().Read());
+
+  // divisor = 5 -> 12 // 5 == 2 != 3 -> gated absent (only 1 byte needed).
+  static constexpr ::std::array</**/ ::std::uint8_t, 1> kAbsent = {{0x05}};
+  auto absent = MakeFieldGatedByDivisionView(&kAbsent);
+  ASSERT_TRUE(absent.Ok());
+  EXPECT_FALSE(absent.has_gated().ValueOr(true));
+}
+
+// ...and is *undefined* for a zero divisor.  The existence condition is Unknown,
+// so the field's presence is unknown and Ok() must return false.  This is the
+// soundness guard for the Ok()/switch discriminant optimization: an undefined
+// existence condition must never be folded to a provably-known value.
+TEST(FieldGatedByDivision, ZeroDivisorIsNotOk) {
+  static constexpr ::std::array</**/ ::std::uint8_t, 2> kBuf = {{0x00, 0x77}};
+  auto view = MakeFieldGatedByDivisionView(&kBuf);
+  EXPECT_FALSE(view.Ok());
+  EXPECT_FALSE(view.has_gated().Known());
+}
+
+// `0 // divisor` collapses to the single value {0}, but must not be folded to a
+// literal: it is undefined when the divisor is zero.
+TEST(CollapsingQuotient, DefinedForNonzeroDivisor) {
+  static constexpr ::std::array</**/ ::std::uint8_t, 1> kBuf = {{0x07}};
+  auto view = MakeCollapsingQuotientView(&kBuf);
+  ASSERT_TRUE(view.Ok());
+  EXPECT_TRUE(view.zero_or_undefined().Ok());
+  EXPECT_EQ(0, view.zero_or_undefined().Read());
+}
+
+TEST(CollapsingQuotient, UndefinedForZeroDivisor) {
+  static constexpr ::std::array</**/ ::std::uint8_t, 1> kBuf = {{0x00}};
+  auto view = MakeCollapsingQuotientView(&kBuf);
+  // The accessor is Unknown -- not a bogus literal 0.
+  EXPECT_FALSE(view.zero_or_undefined().Ok());
+}
+
 }  // namespace
 }  // namespace test
 }  // namespace emboss

compiler/front_end/constraints.py

@@ -713,13 +713,15 @@ def _check_bounds_on_runtime_integer_expressions(
 def _check_division_and_modulus_have_nonzero_divisors(
     expression, source_file_name, errors
 ):
-    """Rejects `l // r` and `l % r` whose divisor range could contain zero.
-
-    This is the initial, strict rollout of `//` and `%`: because the expression
-    type system does not yet track an `undefined` value, the only sound option
-    for a divisor whose range includes zero is to reject it at compile time.  A
-    later change will loosen this to allow a *possibly*-zero divisor to propagate
-    an `undefined` value, keeping the error only for a *provably*-zero divisor.
+    """Rejects `l // r` and `l % r` whose divisor is *provably always* zero.
+
+    A divisor that is provably zero (its range is exactly {0}, e.g. `x // 0`)
+    has no defined result and is rejected at compile time.  A divisor that is
+    merely *possibly* zero (a non-constant range that includes zero, e.g.
+    `x // d` for a byte `d`) is allowed: the expression type system propagates an
+    `undefined` value (tracked by IntegerType.can_be_undefined) and the runtime
+    yields an Unknown result for a `// 0`, so the field's `Ok()` becomes false
+    rather than the whole schema failing to compile.
     """
     if expression.which_expression != "function":
         return
@@ -734,9 +736,10 @@ def _check_division_and_modulus_have_nonzero_divisors(
         return
     rmin = divisor.type.integer.minimum_value
     rmax = divisor.type.integer.maximum_value
-    rmin_le_zero = rmin == "-infinity" or int(rmin) <= 0
-    rmax_ge_zero = rmax == "infinity" or int(rmax) >= 0
-    if rmin_le_zero and rmax_ge_zero:
+    # Provably always zero iff the divisor's range is exactly {0}.  (The bounds
+    # invariant guarantees minimum_value == maximum_value implies the value is a
+    # constant.)
+    if rmin == "0" and rmax == "0":
         op_text = expression.function.function_name.text
         errors.append(
             [
@@ -748,9 +751,7 @@ def _check_division_and_modulus_have_nonzero_divisors(
                 error.note(
                     source_file_name,
                     divisor.source_location,
-                    "Divisor range is {} to {}, which includes zero.".format(
-                        rmin, rmax
-                    ),
+                    "Divisor is always zero.",
                 ),
             ]
         )

compiler/front_end/constraints_test.py

@@ -80,31 +80,50 @@ def test_no_error_on_modulus_by_positive_constant(self):
         )
         self.assertEqual([], constraints.check_constraints(ir))
 
-    def test_error_on_division_with_divisor_range_including_zero(self):
+    def test_no_error_on_division_with_divisor_range_including_zero(self):
+        # A *possibly*-zero divisor is now allowed: it propagates an `undefined`
+        # value (IntegerType.can_be_undefined) and yields an Unknown result at
+        # runtime rather than failing to compile.
         ir = _make_ir_from_emb(
             "struct Foo:\n"
             "  0 [+1]  UInt  divisor\n"
             "  1 [+1]  UInt  dividend\n"
             "  let q = dividend // divisor\n"
         )
-        errors = error.filter_errors(constraints.check_constraints(ir))
-        self.assertEqual(1, len(errors))
-        self.assertIn("Right argument of '//' cannot be zero.", errors[0][0].message)
+        self.assertEqual([], constraints.check_constraints(ir))
 
-    def test_error_on_modulus_with_divisor_range_including_zero(self):
+    def test_no_error_on_modulus_with_divisor_range_including_zero(self):
         ir = _make_ir_from_emb(
             "struct Foo:\n"
             "  0 [+1]  UInt  divisor\n"
             "  1 [+1]  UInt  dividend\n"
             "  let r = dividend % divisor\n"
         )
+        self.assertEqual([], constraints.check_constraints(ir))
+
+    def test_error_on_division_by_zero_literal(self):
+        # A *provably*-always-zero divisor is still a hard compile error.
+        ir = _make_ir_from_emb(
+            "struct Foo:\n" "  0 [+1]  UInt  x\n" "  let q = x // 0\n"
+        )
+        errors = error.filter_errors(constraints.check_constraints(ir))
+        self.assertEqual(1, len(errors))
+        self.assertIn("Right argument of '//' cannot be zero.", errors[0][0].message)
+
+    def test_error_on_modulus_by_zero_literal(self):
+        ir = _make_ir_from_emb(
+            "struct Foo:\n" "  0 [+1]  UInt  x\n" "  let r = x % 0\n"
+        )
         errors = error.filter_errors(constraints.check_constraints(ir))
         self.assertEqual(1, len(errors))
         self.assertIn("Right argument of '%' cannot be zero.", errors[0][0].message)
 
-    def test_error_on_division_by_zero_literal(self):
+    def test_error_on_division_by_provably_zero_expression(self):
+        # A divisor that folds to a constant zero (range exactly {0}) is
+        # provably always zero, so it is rejected even though it is not a bare
+        # `0` literal.
         ir = _make_ir_from_emb(
-            "struct Foo:\n" "  0 [+1]  UInt  x\n" "  let q = x // 0\n"
+            "struct Foo:\n" "  0 [+1]  UInt  x\n" "  let q = x // (3 - 3)\n"
         )
         errors = error.filter_errors(constraints.check_constraints(ir))
         self.assertEqual(1, len(errors))

compiler/front_end/expression_bounds.py

@@ -368,6 +368,34 @@ def _min(a):
     return min(int(n) for n in a if not _is_infinite(n))
 
 
+def _range_includes_zero(minimum_value, maximum_value):
+    """Returns True if the closed range [minimum_value, maximum_value] holds 0.
+
+    minimum_value and maximum_value are ints, stringified ints, "-infinity", or
+    "infinity".
+    """
+    min_le_zero = minimum_value == "-infinity" or int(minimum_value) <= 0
+    max_ge_zero = maximum_value == "infinity" or int(maximum_value) >= 0
+    return min_le_zero and max_ge_zero
+
+
+def _any_can_be_undefined(operands):
+    """Returns True if any of the given operand expressions can be undefined."""
+    for operand in operands:
+        operand_type = operand.type
+        if (
+            operand_type.which_type == "integer"
+            and operand_type.integer.can_be_undefined
+        ):
+            return True
+        if (
+            operand_type.which_type == "boolean"
+            and operand_type.boolean.can_be_undefined
+        ):
+            return True
+    return False
+
+
 def _compute_constraints_of_additive_operator(expression):
     """Computes the modular value of an additive expression."""
     funcs = {
@@ -402,6 +430,8 @@ def _compute_constraints_of_additive_operator(expression):
         rmin = right.type.integer.minimum_value
     expression.type.integer.minimum_value = str(func(lmin, rmin))
     expression.type.integer.maximum_value = str(func(lmax, rmax))
+    if _any_can_be_undefined(args):
+        expression.type.integer.can_be_undefined = True
 
 
 def _compute_constraints_of_multiplicative_operator(expression):
@@ -439,6 +469,8 @@ def _compute_constraints_of_multiplicative_operator(expression):
     ]
     expression.type.integer.minimum_value = str(_min(extrema))
     expression.type.integer.maximum_value = str(_max(extrema))
+    if _any_can_be_undefined(expression.function.args):
+        expression.type.integer.can_be_undefined = True
 
     if all(bound.modulus == "infinity" for bound in bounds):
         # If both sides are constant, the result is constant.
@@ -557,6 +589,15 @@ def _compute_constraints_of_division_operator(expression):
     """Computes the bounds of a `//` (flooring integer division) expression."""
     left, right = (arg.type.integer for arg in expression.function.args)
 
+    # `//` introduces undefined-ness: the result can be undefined if either
+    # operand can be undefined, or if the divisor's range includes zero (a
+    # runtime `// 0`).  The constraints pass rejects a *provably*-zero divisor;
+    # a merely *possibly*-zero divisor is allowed and carries this flag.
+    if _any_can_be_undefined(expression.function.args) or _range_includes_zero(
+        right.minimum_value, right.maximum_value
+    ):
+        expression.type.integer.can_be_undefined = True
+
     # Both sides constant: compute the exact result.
     if left.modulus == "infinity" and right.modulus == "infinity":
         r_val = int(right.modular_value)
@@ -610,6 +651,13 @@ def _compute_constraints_of_modulus_operator(expression):
     """Computes the bounds of a `%` (flooring modulus) expression."""
     left, right = (arg.type.integer for arg in expression.function.args)
 
+    # As with `//`, `%` introduces undefined-ness when the divisor's range
+    # includes zero (or an operand is already undefined).
+    if _any_can_be_undefined(expression.function.args) or _range_includes_zero(
+        right.minimum_value, right.maximum_value
+    ):
+        expression.type.integer.can_be_undefined = True
+
     if left.modulus == "infinity" and right.modulus == "infinity":
         r_val = int(right.modular_value)
         if r_val == 0:
@@ -693,6 +741,12 @@ def _compute_constant_value_of_comparison_operator(expression):
         expression.type.boolean.value = func(
             *[ir_util.constant_value(arg) for arg in args]
         )
+    # An operand that can be undefined poisons the result.  Note that an operand
+    # that can be undefined is never a compile-time constant (see
+    # ir_util.constant_value), so the branch above never sets a boolean `value`
+    # in that case -- the two are mutually exclusive.
+    if _any_can_be_undefined(args):
+        expression.type.boolean.can_be_undefined = True
 
 
 def _compute_constraints_of_bound_function(expression):
@@ -723,6 +777,8 @@ def _compute_constraints_of_maximum_function(expression):
     expression.type.integer.maximum_value = str(
         _max([arg.type.integer.maximum_value for arg in args])
     )
+    if _any_can_be_undefined(args):
+        expression.type.integer.can_be_undefined = True
     # If the expression is dominated by a constant factor, then the result is
     # constant.  I (bolms@) believe this is the only case where
     # _compute_constraints_of_maximum_function might violate the assertions in
@@ -865,6 +921,17 @@ def _compute_constraints_of_choice_operator(expression):
             "boolean",
             "enumeration",
         ), "Unknown type {} for expression".format(if_true.type.which_type)
+    # The result can be undefined if the condition or the selected branch can be
+    # undefined.  Conservatively, if any of the three operands can be undefined,
+    # the result can be too.  (An `enumeration` result cannot carry the flag, but
+    # a non-constant choice is never treated as a constant enum, so it stays
+    # correctly un-foldable regardless.)
+    if _any_can_be_undefined((condition, if_true, if_false)):
+        # The choice's result type matches if_true's (and if_false's) type.
+        if if_true.type.which_type == "integer":
+            expression.type.integer.can_be_undefined = True
+        elif if_true.type.which_type == "boolean":
+            expression.type.boolean.can_be_undefined = True
 
 
 def _greatest_common_divisor(a, b):