Cleanup asserts & throws - replace with invariants - dir util/s* (part1) #2898

sonodtt · 2018-09-05T08:22:05Z

Cleanup of asserts - replaced with invariants.

Removed all unstructured throw(...) statements, replacing with INVARIANT, PRECONDITION, etc. where appropriate.

tautschnig

Let's try to do a bit more than the very mechanical cleanup.

tautschnig · 2018-09-05T08:30:14Z

src/util/simplify_expr.cpp

          return false;
        }
        else if(operand.is_false())
        {
-          expr=from_integer(0, expr_type);
-          assert(expr.is_not_nil());
+          expr = from_integer(0, expr_type);


Unrelated change

tautschnig · 2018-09-05T08:31:12Z

src/util/simplify_expr.cpp

@@ -1373,7 +1373,7 @@ bool simplify_exprt::simplify_update(exprt &expr)
      std::size_t number=to_struct_type(value_ptr_type).
        component_number(component_name);

-      assert(number<value_ptr->operands().size());
+      CHECK_RETURN(number < value_ptr->operands().size());


This code should be rewritten to use get_component.

Refactored.

tautschnig · 2018-09-05T08:33:05Z

src/util/simplify_expr.cpp

-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      "typecasts must have exactly one argument");


Introduce const typecast_exprt &tc = to_typecast_expr(expr); above and change the code to use tc with its proper API. Let's not duplicate consistency checks on expressions.

tautschnig · 2018-09-05T08:34:44Z

src/util/simplify_expr_boolean.cpp

-    assert(op.operands().size()==2);
+    DATA_INVARIANT(
+      op.operands().size() == 2,
+      "exists expression has two parameters");


Please introduce to_exists_expr which should do this sort of check and use it here.

tautschnig · 2018-09-05T08:35:59Z

src/util/simplify_expr_floatbv.cpp

-  assert(expr.operands().size()==2);
+  PRECONDITION(expr.id() == ID_floatbv_typecast);
+  DATA_INVARIANT(
+    expr.operands().size() == 2, "float typecast has two operands");


This function should take a floatbv_typecast_exprt as a parameter and should not be doing those checks in here.

I agree that'd be much cleaner, but note that currently all of the simplify_XXX work like this (this is also because many of the simplify functions can take many different types of expressions). We could change that but if we were to do that I'd change all of them at once and that's out of scope for this PR IMHO (if we just changed the one the code would be quite inconsistent)

[...] currently all of the [...]

Not quite true - there is sort of a gradual migration happening. Take a look at the declarations in simplify_expr_class.h.

Hm... I don't really like that. It ends up violating structural invariants to still use the input expression as an out parameter, because most simplifications will "return" a different type than they were given... I find the idea of returning something that's not a plus_exprt through a plus_exprt reference a bit disturbing.

See #2910 (comment).

@tautschnig Can you take a look at #2939 and tell me if that's roughly in line with what you were thinking? Would you be OK with going ahead with this PR and doing further refactorings in one or more separate PRs?

@tautschnig I'm going to split this part out - and make a note for it to be considered in the context of #2939 and your remarks on #2910 (comment)

see
#2939 (comment) that documents this

Sounds good!

allredj

This PR failed Diffblue compatibility checks (cbmc commit: a2c876d).
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).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: a2c876d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/83831905
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).

allredj

Passed Diffblue compatibility checks (cbmc commit: 9c79c23).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84019963

allredj

This PR failed Diffblue compatibility checks (cbmc commit: b0b44fa).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85534606
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).

allredj

Passed Diffblue compatibility checks (cbmc commit: 42f660e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85532856

tautschnig · 2018-09-26T07:31:24Z

src/util/simplify_expr.cpp

-      value_ptr=&value_ptr->operands()[number];
+      auto &designator_as_struct_expr = to_struct_expr(*value_ptr);
+      value_ptr = &designator_as_struct_expr.component(component_name, ns);
+      CHECK_RETURN(value_ptr->id() != ID_nil);


Use value_ptr->is_not_nil()

tautschnig · 2018-09-26T07:31:41Z

src/util/simplify_expr.cpp

-
-      if(!to_struct_type(value_ptr_type).
-         has_component(component_name))
+      const struct_typet &value_ptr_struct_type=to_struct_type(value_ptr_type);


Nit pick: whitespace around =

tautschnig · 2018-09-26T07:31:52Z

src/util/simplify_expr.cpp

-      expr.operands().size() == 1,
-      "typecasts must have exactly one argument");
+    auto const& typecast_expr = to_typecast_expr(expr);
+    const typet &op_type=ns.follow(typecast_expr.op().type());


Space around =

tautschnig · 2018-09-26T07:33:18Z

src/util/simplify_expr.cpp

@@ -1429,10 +1419,10 @@ bool simplify_exprt::simplify_object(exprt &expr)
      // We do a bit of special treatment for (TYPE *)(a+(int)&o) and
      // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'.

-      exprt tmp=expr.op0();
-      if(tmp.id()==ID_plus && tmp.operands().size()==2)
+      exprt casted_expr=typecast_expr.op();


const exprt &casted_expr = typecast_expr.op();

tautschnig · 2018-09-26T07:33:31Z

src/util/simplify_expr.cpp

-      exprt tmp=expr.op0();
-      if(tmp.id()==ID_plus && tmp.operands().size()==2)
+      exprt casted_expr=typecast_expr.op();
+      if(casted_expr.id()==ID_plus && casted_expr.operands().size()==2)


Add spacing around ==

tautschnig · 2018-09-26T07:33:38Z

src/util/simplify_expr.cpp

      {
-        exprt cand=tmp.op0().id()==ID_typecast?tmp.op0():tmp.op1();
+        exprt cand=casted_expr.op0().id()==ID_typecast?casted_expr.op0():casted_expr.op1();


tautschnig · 2018-09-26T07:34:52Z

src/util/simplify_expr_boolean.cpp

-    simplify_node(expr.op1());
+    auto const& op_as_exists = to_exists_expr(op);
+    forall_exprt rewritten_op(op_as_exists.symbol()
+      , op_as_exists.where());


forall_exprt rewritten_op( op_as_exists.symbol(), not_exprt(op_as_exists.where()));

and remove the line below

tautschnig · 2018-09-26T07:36:58Z

src/util/simplify_expr.cpp

@@ -1365,7 +1365,8 @@ bool simplify_exprt::simplify_update(exprt &expr)
    {
      const irep_idt &component_name=
        e.get(ID_component_name);
-      const struct_typet &value_ptr_struct_type=to_struct_type(value_ptr_type);
+      const struct_typet &value_ptr_struct_type =
+        to_struct_type(value_ptr_type);


Please squash with the previous commit, the clang-format changes are restricted to code that you have introduced in the preceding commit.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 8734b32).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86134560
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).

allredj

Passed Diffblue compatibility checks (cbmc commit: cba81d9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86174685

allredj

Passed Diffblue compatibility checks (cbmc commit: 6c0ab09).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86178555

Deprecated c-style asserts in favour of cbmc invariants. Some minor refactoring that was relevant to the cleanup.

* Use to_XXX_expr functions instead of asserts to make sure invariants are not violated * Use named accessors instead of op0, op1 etc * Rename variables (e.g. "casted_expr" instead of "op0") for readability

hannes-steffenhagen-diffblue · 2018-09-28T16:20:59Z

@tautschnig I believe all of your comments (aside from changing the function signatures to be more strongly typed which will happen in another PR as previously discussed) have been addressed now.

allredj

Passed Diffblue compatibility checks (cbmc commit: a168b24).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86316058

sonodtt requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 5, 2018 08:22

tautschnig requested changes Sep 5, 2018

View reviewed changes

allredj reviewed Sep 5, 2018

View reviewed changes

sonodtt changed the title ~~Cleanup asserts & throws - replace with invariants~~ Cleanup asserts & throws - replace with invariants - dir util/s* (part1) Sep 6, 2018

sonodtt force-pushed the invariant-cleanup-util_dir-s_files-part1 branch from a2c876d to 9c79c23 Compare September 6, 2018 14:30

allredj reviewed Sep 6, 2018

View reviewed changes

hannes-steffenhagen-diffblue mentioned this pull request Sep 12, 2018

Refactor simplify floatbv typecast #2939

Closed

sonodtt force-pushed the invariant-cleanup-util_dir-s_files-part1 branch 2 times, most recently from b0b44fa to 42f660e Compare September 21, 2018 07:59

allredj reviewed Sep 21, 2018

View reviewed changes

tautschnig assigned sonodtt Sep 24, 2018

tautschnig reviewed Sep 26, 2018

View reviewed changes

sonodtt force-pushed the invariant-cleanup-util_dir-s_files-part1 branch 2 times, most recently from 8734b32 to cba81d9 Compare September 27, 2018 10:19

allredj reviewed Sep 27, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-s_files-part1 branch from cba81d9 to 6c0ab09 Compare September 27, 2018 16:07

hannes-steffenhagen-diffblue self-assigned this Sep 27, 2018

allredj reviewed Sep 27, 2018

View reviewed changes

Sonny Martin and others added 2 commits September 28, 2018 17:06

Cleanup asserts & throws - replace with invariants

bf19b39

Deprecated c-style asserts in favour of cbmc invariants. Some minor refactoring that was relevant to the cleanup.

Refactor simplify_floatbv_typecast

a168b24

* Use to_XXX_expr functions instead of asserts to make sure invariants are not violated * Use named accessors instead of op0, op1 etc * Rename variables (e.g. "casted_expr" instead of "op0") for readability

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-s_files-part1 branch from 6c0ab09 to a168b24 Compare September 28, 2018 16:18

tautschnig approved these changes Sep 28, 2018

View reviewed changes

tautschnig merged commit 9e07c3f into diffblue:develop Sep 28, 2018

allredj reviewed Sep 28, 2018

View reviewed changes

Cleanup asserts & throws - replace with invariants - dir util/s* (part1) #2898

Cleanup asserts & throws - replace with invariants - dir util/s* (part1) #2898

Uh oh!

Conversation

sonodtt commented Sep 5, 2018

Uh oh!

tautschnig 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!

hannes-steffenhagen-diffblue Sep 5, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

sonodtt Sep 26, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

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!

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!

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!

hannes-steffenhagen-diffblue Sep 5, 2018 •

edited

Loading

sonodtt Sep 26, 2018 •

edited

Loading