numeric_cast_v(expr) now requires constant_expr #4004

kroening · 2019-01-31T10:16:10Z

This is follow-up from a discussion on PR #3998, and a comment by
@tautschnig.

This function always fails, with an exception, when given anything but a
constant_exprt.

This change means that the caller must do the type conversion. The benefit
is to make the caller more aware of the requirement that this must be a
constant, and to make the caller handle the error appropriately (with an
user-friendly error message) in case this is not possible.

The disadvantage is additional code at the call site.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
n/a Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

smowton

A few redundant invariants, and two apparent changes in behaviour that should be tested or reverted

smowton · 2019-01-31T10:36:04Z

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -155,7 +155,9 @@ void symbol_factoryt::gen_nondet_array_init(
  const recursion_sett &recursion_set)
 {
  auto const &array_type = to_array_type(expr.type());
-  auto const array_size = numeric_cast_v<size_t>(array_type.size());
+  const auto &size = array_type.size();
+  PRECONDITION(size.id() == ID_constant);


Redundant with to_constant_expr?

⛏️ Just noting this never got addressed.

smowton · 2019-01-31T10:40:29Z

src/solvers/flattening/boolbv.cpp

@@ -72,9 +72,13 @@ bool boolbvt::literal(
      std::size_t element_width=boolbv_width(index_expr.type());
      CHECK_RETURN(element_width != 0);

-      mp_integer index = numeric_cast_v<mp_integer>(index_expr.index());
+      const auto &index = index_expr.index();
+      PRECONDITION(index.id() == ID_constant);


⛏️ Or this

smowton · 2019-01-31T10:42:32Z

src/solvers/flattening/boolbv_update.cpp


    std::size_t element_size=boolbv_width(subtype);

+    DATA_INVARIANT(
+      size.id() == ID_constant, "update expects constant-sized array");


@smowton 👎 - this provides more information that just relying on the cast. But according to guidelines, should be framed in the should form, for clarity:

Array should be constant size for boolbv_update

smowton · 2019-01-31T10:47:50Z

src/util/pointer_offset_size.cpp

-    const mp_integer size =
-      numeric_cast_v<mp_integer>(to_vector_type(type).size());
+    const mp_integer size_int =
+      numeric_cast_v<mp_integer>(to_constant_expr(size));


Change in behaviour: returning 0 vs. {}?

smowton · 2019-01-31T10:49:12Z

src/util/simplify_expr.cpp


-    const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
+    if(!size.is_constant())


Change in behaviour: returning empty array vs. nil?

That one seems like a bugfix!

This is a change in behaviour - could you add a unit test checking this and ideally put it into a separate commit in case it breaks anything (this would be a big commit to comb through!)

Presumably this change came about, because in a regression test the size here is non-const, perhaps the test could be tightened so it would have failed before too?

src/ansi-c/expr2c.cpp

tautschnig · 2019-01-31T11:34:07Z

src/goto-programs/xml_expr.cpp

@@ -127,6 +127,8 @@ xmlt xml(const exprt &expr, const namespacet &ns)

  if(expr.id() == ID_constant)
  {
+    const auto &constant_expr = to_constant_expr(expr);


Isn't this also in another PR? Maybe get that other one merged first?

src/solvers/flattening/boolbv_quantifier.cpp

src/solvers/flattening/boolbv_width.cpp

tautschnig · 2019-01-31T11:37:19Z

src/solvers/smt2/smt2_conv.cpp

@@ -2636,8 +2644,10 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
 void smt2_convt::flatten_array(const exprt &expr)
 {
  const array_typet &array_type = to_array_type(expr.type());
+  const exprt &size_expr = array_type.size();
+  PRECONDITION(size_expr.id() == ID_constant);


src/util/endianness_map.cpp

src/util/expr_initializer.cpp

tautschnig · 2019-01-31T11:38:46Z

src/util/pointer_offset_size.cpp

+    const auto &size = vector_type.size();
+
+    auto sub = pointer_offset_bits(vector_type.subtype(), ns);
+    if(!sub.has_value() || size.id() != ID_constant)


Should be an invariant

tautschnig · 2019-01-31T11:39:44Z

src/util/simplify_expr.cpp


-    const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
+    if(!size.is_constant())


That one seems like a bugfix!

kroening · 2019-01-31T11:51:09Z

On the preconditions: I do feel these are important as a way of documenting the contract of the function they are in.
vector size: I'll do a PR that makes that invariant part of the signature.
Yes, there are two changes of behaviour here, where the case of "size is not constant" was overlooked. I'll make these more explicit.

kroening · 2019-01-31T12:00:36Z

This PR will shrink a lot with #4007.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: ebfb529).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99263775
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 94ec292).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99494027
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 00df0f4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99498173
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

tautschnig

Some small bits left, but also will need a TG bump.

src/solvers/flattening/boolbv_replication.cpp

antlechner · 2019-02-05T11:59:29Z

Some tests are still failing on the TG bump for this, I'm investigating and I'll post updates here.

antlechner · 2019-02-06T10:44:25Z

The TG bump is now passing. 👍

thk123

Please fix the variable name and the test for the bug fix

thk123 · 2019-02-07T11:08:34Z

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -155,7 +155,9 @@ void symbol_factoryt::gen_nondet_array_init(
  const recursion_sett &recursion_set)
 {
  auto const &array_type = to_array_type(expr.type());
-  auto const array_size = numeric_cast_v<size_t>(array_type.size());
+  const auto &size = array_type.size();
+  PRECONDITION(size.id() == ID_constant);


⛏️ Just noting this never got addressed.

thk123 · 2019-02-07T11:08:49Z

src/solvers/flattening/boolbv.cpp

@@ -72,9 +72,13 @@ bool boolbvt::literal(
      std::size_t element_width=boolbv_width(index_expr.type());
      CHECK_RETURN(element_width != 0);

-      mp_integer index = numeric_cast_v<mp_integer>(index_expr.index());
+      const auto &index = index_expr.index();
+      PRECONDITION(index.id() == ID_constant);


⛏️ Or this

thk123 · 2019-02-07T11:10:04Z

src/solvers/flattening/boolbv_extractbit.cpp


  // constant?
-  if(expr.index().is_constant())
+  if(index.is_constant())


I think more idiomatic in this code base to:

if(const auto &constant_index = try_expr_dynamic_cast<constant_exprt>(index)) { ... numeric_cast_v<mp_integer>(constant_index);

Since seems plausible the is_constant method will go away at some point

or shorter using an optional:

if(const auto index_as_integer = numeric_cast<mp_integer>(index))

thk123 · 2019-02-07T11:11:54Z

src/solvers/flattening/boolbv_quantifier.cpp

@@ -87,8 +87,10 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
        continue;
      if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
      {
-        exprt over_expr=x.op1();
+        const constant_exprt &over_expr = to_constant_expr(x.op1());


⛏️ While in the area, you might like to tidy the if to not duplicate the checking the id by using try_dynamic_cast

or the version of numeric_cast which returns an optional

thk123 · 2019-02-07T11:13:41Z

src/solvers/flattening/boolbv_update.cpp


    std::size_t element_size=boolbv_width(subtype);

+    DATA_INVARIANT(
+      size.id() == ID_constant, "update expects constant-sized array");


@smowton 👎 - this provides more information that just relying on the cast. But according to guidelines, should be framed in the should form, for clarity:

Array should be constant size for boolbv_update

src/solvers/flattening/boolbv_update.cpp

src/solvers/smt2/smt2_conv.cpp

src/util/simplify_expr.cpp

thk123 · 2019-02-07T11:22:14Z

src/util/simplify_expr.cpp


-    const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
+    if(!size.is_constant())


This is a change in behaviour - could you add a unit test checking this and ideally put it into a separate commit in case it breaks anything (this would be a big commit to comb through!)

Presumably this change came about, because in a regression test the size here is non-const, perhaps the test could be tightened so it would have failed before too?

src/goto-programs/interpreter.cpp

romainbrenguier · 2019-02-07T14:47:56Z

src/solvers/flattening/boolbv_extractbit.cpp


  // constant?
-  if(expr.index().is_constant())
+  if(index.is_constant())


or shorter using an optional:

if(const auto index_as_integer = numeric_cast<mp_integer>(index))

romainbrenguier · 2019-02-07T14:50:10Z

src/solvers/flattening/boolbv_quantifier.cpp

@@ -87,8 +87,10 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
        continue;
      if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
      {
-        exprt over_expr=x.op1();
+        const constant_exprt &over_expr = to_constant_expr(x.op1());


or the version of numeric_cast which returns an optional

tautschnig · 2019-02-16T18:01:39Z

src/util/simplify_expr.cpp


-    for(std::size_t i=0; i<n_el; ++i)
+    for(std::size_t i=0; i<number_of_elements; ++i)


This isn't clang-format correctly spaced out.

@tautschnig

This is follow-up from a discussion on PR #3998, and a comment by @tautschnig. This function always fails, with an exception, when given anything but a constant_exprt. This change means that the caller must do the type conversion. The benefit is to make the caller more aware of the requirement that this must be a constant, and to make the caller handle the error appropriately (with an user-friendly error message) in case this is not possible. The disadvantage is additional code at the call site.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 4a133b3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101202288

kroening assigned tautschnig Jan 31, 2019

kroening requested review from allredj, cesaro, chrisr-diffblue, cristina-david, martin-cs, NathanJPhillips, peterschrammel, pkesseli, romainbrenguier, smowton, tautschnig and thk123 as code owners January 31, 2019 10:16

smowton reviewed Jan 31, 2019

View reviewed changes

tautschnig reviewed Jan 31, 2019

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Jan 31, 2019

allredj reviewed Jan 31, 2019

View reviewed changes

kroening force-pushed the numeric_cast_v_constant_expr branch 3 times, most recently from 5b1192e to 00df0f4 Compare February 1, 2019 22:07

allredj reviewed Feb 1, 2019

View reviewed changes

allredj reviewed Feb 2, 2019

View reviewed changes

kroening assigned thk123 and tautschnig and unassigned kroening Feb 2, 2019

tautschnig approved these changes Feb 2, 2019

View reviewed changes

src/solvers/flattening/boolbv_replication.cpp Outdated Show resolved Hide resolved

tautschnig removed their assignment Feb 2, 2019

majakusber assigned antlechner and unassigned thk123 and majakusber Feb 4, 2019

tautschnig unassigned antlechner Feb 6, 2019

kroening assigned thk123 and romainbrenguier and unassigned kroening Feb 6, 2019

thk123 reviewed Feb 7, 2019

View reviewed changes

tautschnig assigned kroening Feb 7, 2019

romainbrenguier approved these changes Feb 7, 2019

View reviewed changes

kroening force-pushed the numeric_cast_v_constant_expr branch from a4dded0 to 3a6425c Compare February 16, 2019 16:36

kroening requested review from danpoe and hannes-steffenhagen-diffblue as code owners February 16, 2019 16:36

kroening force-pushed the numeric_cast_v_constant_expr branch 3 times, most recently from 89345ef to bd13a73 Compare February 16, 2019 17:01

kroening unassigned thk123 and kroening Feb 16, 2019

tautschnig reviewed Feb 16, 2019

View reviewed changes

kroening force-pushed the numeric_cast_v_constant_expr branch from bd13a73 to 4a133b3 Compare February 16, 2019 21:21

allredj reviewed Feb 16, 2019

View reviewed changes

peterschrammel approved these changes Feb 17, 2019

View reviewed changes

peterschrammel assigned kroening and unassigned peterschrammel and romainbrenguier Feb 17, 2019

kroening merged commit a5944a7 into develop Feb 17, 2019

kroening deleted the numeric_cast_v_constant_expr branch February 17, 2019 16:27


		const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
		if(!size.is_constant())


		for(std::size_t i=0; i<n_el; ++i)
		for(std::size_t i=0; i<number_of_elements; ++i)

numeric_cast_v(expr) now requires constant_expr #4004

numeric_cast_v(expr) now requires constant_expr #4004

Uh oh!

Conversation

kroening commented Jan 31, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Jan 31, 2019

Uh oh!

kroening commented Jan 31, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

antlechner commented Feb 5, 2019

Uh oh!

antlechner commented Feb 6, 2019

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment