Cleanup of asserts and throws under the goto-symex directory #2902

NlightNFotis · 2018-09-05T14:16:41Z

This PR is similar in spirit to #2703 but it targets the goto-symex/ directory.

tautschnig

Essentially the same comments as I've put on other PRs related to the assert cleanup: let's please use APIs and thereby lift invariants as much as possible.

tautschnig · 2018-09-05T14:22:40Z

src/goto-symex/build_goto_trace.cpp

-    assert(tmp.operands().size()==2);
+    DATA_INVARIANT(
+      tmp.operands().size() == 2,
+      "byte_extract_exprt should have two operands.");


Let's please use to_byte_extract_expr, and use byte_extract_exprt's API. Otherwise we duplicate consistency checks across the code base and risk getting out-of-sync.

tautschnig · 2018-09-05T14:23:02Z

src/goto-symex/goto_symex_state.cpp

-    if(expr.operands().size()!=1)
-      throw "member expects one operand";
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "member_exprt takes one operand.");


Let's use to_member_expr: return constant_propagation_reference(to_member_expr(expr).compound();

tautschnig · 2018-09-05T14:24:20Z

src/goto-symex/postcondition.cpp

@@ -76,20 +76,23 @@ bool postconditiont::is_used_address_of(
  }
  else if(expr.id()==ID_index)
  {
-    assert(expr.operands().size()==2);
+    DATA_INVARIANT(
+      expr.operands().size() == 2, "index_exprt takes two operands.");


Please use to_index_expr and use its API below.

tautschnig · 2018-09-05T14:24:58Z

src/goto-symex/postcondition.cpp


    return
      is_used_address_of(expr.op0(), identifier) ||
      is_used(expr.op1(), identifier);
  }
  else if(expr.id()==ID_member)
  {
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "member_exprt takes one operand.");


Please use return is_used_address_of(to_member_expr(expr).compound(), identifier);

tautschnig · 2018-09-05T14:25:33Z

src/goto-symex/postcondition.cpp

    return is_used_address_of(expr.op0(), identifier);
  }
  else if(expr.id()==ID_dereference)
  {
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "dereference_exprt takes one operand.");


Please use return is_used(to_dereference_expr(expr).pointer(), identifier);

tautschnig · 2018-09-05T14:26:24Z

src/goto-symex/postcondition.cpp

@@ -155,7 +158,8 @@ bool postconditiont::is_used(
  if(expr.id()==ID_address_of)
  {
    // only do index!
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size() == 1, "address_of_exprt takes one operand.");


See above: use to_address_of_expr etc - I'll stop putting the same comments, it applies several times below.

tautschnig · 2018-09-05T14:27:26Z

src/goto-symex/slice.cpp

@@ -112,7 +112,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
 void symex_slicet::slice_assignment(
  symex_target_equationt::SSA_stept &SSA_step)
 {
-  assert(SSA_step.ssa_lhs.id()==ID_symbol);
+  PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);


I believe this should be true by design.

Still, isn't it a good idea to leave it there, even if only for documentation purposes?

Not a big deal, but I think if we were to go down that route we'd have, e.g., any use of an index_exprt prefixed by expr.id() == ID_index.

tautschnig · 2018-09-05T14:28:57Z

src/goto-symex/symex_assign.cpp

@@ -283,7 +285,7 @@ void goto_symext::symex_assign_typecast(
 {
  // these may come from dereferencing on the lhs

-  assert(lhs.operands().size()==1);
+  PRECONDITION(lhs.operands().size() == 1);


True by virtue of it being a typecast_exprt

tautschnig · 2018-09-05T14:29:17Z

src/goto-symex/symex_assign.cpp

-
-  if(lhs.operands().size()!=2)
-    throw "index must have two operands";
+  DATA_INVARIANT(lhs.operands().size() == 2, "index_exprt takes two operands");


True for all index_exprt

tautschnig · 2018-09-05T14:29:32Z

src/goto-symex/symex_assign.cpp

@@ -368,7 +368,8 @@ void goto_symext::symex_assign_struct_member(
  // typecasts involved? C++ does that for inheritance.
  if(lhs_struct.id()==ID_typecast)
  {
-    assert(lhs_struct.operands().size()==1);
+    DATA_INVARIANT(
+      lhs_struct.operands().size() == 1, "typecast_exprt takes one operand.");


Use to_typecast_expr

NlightNFotis · 2018-09-07T21:25:05Z

@tautschnig I have implemented most of the changes you suggested. I found them to be very good suggestions. Just two observations: Don't review it yet, I need to go through the whole PR and see where else I could apply the casts with the integrated checks, and also, for some of the superfluous PRECONDITIONs, aren't they okay, even if only for documentation purposes (iirc they are not built into the release builds, so no performance overhead for a user)

NlightNFotis · 2018-09-19T16:22:40Z

As a general update on this, I'm happy with the changes thus far. It's failing CI on some JBMC regression tests, which are expecting some particular output string to be present, alone, in one line. The exception added here makes the particular errors to be multiline, so the tests are failing. I'm going to fix the tests, but first I'm waiting for #2996 to go in, as it contains some exception classes that I think are more appropriate in a couple of cases. Once that goes in, I'm going to rebase, see the behaviour of the tests, and then I'm going to fix the tests that need fixing based on the error messages coming out of the improved exception classes.

tautschnig · 2018-09-19T16:35:55Z

src/goto-symex/goto_symex_state.cpp

@@ -495,12 +493,12 @@ void goto_symex_statet::rename(
  }
  else if(expr.id()==ID_address_of)
  {
+    DATA_INVARIANT(
+      expr.type().id() == ID_pointer,
+      "type of expression required to be pointer");


I think this should just be removed, as should the DATA_INVARIANT below. We don't even care whether the type of the expression is a pointer, and the subsequent invariant should be replaced by a use of to_address_of_expr

tautschnig · 2018-09-19T16:36:39Z

src/goto-symex/precondition.cpp

-    assert(dest.operands().size()==2);
+    DATA_INVARIANT(
+      dest.operands().size() == 2,
+      "index expression expected to have two operands");


Should be to_index_expr

tautschnig · 2018-09-19T16:36:49Z

src/goto-symex/precondition.cpp

-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+      dest.operands().size() == 1,
+      "member expression expected to have one operand");


to_member_expr

tautschnig · 2018-09-19T16:37:01Z

src/goto-symex/precondition.cpp

-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+      dest.operands().size() == 1,
+      "dereference expression expected to have 1 operand");


to_dereference_expr

tautschnig · 2018-09-19T16:37:11Z

src/goto-symex/precondition.cpp

-    assert(dest.operands().size()==1);
+    DATA_INVARIANT(
+      dest.operands().size() == 1,
+      "address_of expression expected to have one operand at this point");


to_address_of_expr

tautschnig · 2018-09-19T16:46:41Z

src/goto-symex/symex_dereference.cpp

@@ -155,6 +156,9 @@ exprt goto_symext::address_arithmetic(
  }
  else if(expr.id()==ID_dereference)
  {
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      "dereference expression expected to have one operand");


to_dereference_expr

tautschnig · 2018-09-19T16:46:55Z

src/goto-symex/symex_dereference.cpp

-      throw "dereference takes one operand";
+    DATA_INVARIANT(
+      expr.operands().size() == 1,
+      "dereference expression expected to have one operand");


to_dereference_expr

tautschnig · 2018-09-19T16:47:38Z

src/goto-symex/symex_goto.cpp

-    throw "atomic sections differ across branches";
+  INVARIANT(
+    state.atomic_section_id == goto_state.atomic_section_id,
+    "atomic sections differ across branches");


Should be an exception as one can craft programs exhibiting this.

tautschnig · 2018-09-19T16:48:23Z

src/goto-symex/symex_main.cpp

-    PRECONDITION(expr.op0().id()==ID_symbol);
+    DATA_INVARIANT(
+      expr.operands().size() == 2,
+      "for_all expression expected to have two operands");


to_quantifier_expr

tautschnig · 2018-09-19T16:48:59Z

src/goto-symex/symex_start_thread.cpp

+  INVARIANT(
+    state.atomic_section_id == 0,
+    "spawning threads out of atomic sections is not allowed; "
+    "this would require amendments to ordering constraints");


Should be an exception as you can write input programs doing so.

NlightNFotis · 2018-09-24T14:25:09Z

@tautschnig Hi Michael, I have addressed all the comments in your review, aside from one.

You have suggested to remove some code, after advising with either Matthias or Daniel. It's not easy for me to get hold of either of them now, so I suggest we leave this for a later cleanup (I have already marked it on my todo, so it's not lost, however if you believe that it should be done now, I will see what I can do, I just thought it could be a good idea to not get hung up on this now since this work is relatively high priority).

I want a little bit of advising on a different part of the PR however. In goto_symex_state.cpp:514 there's a DATA_INVARIANT that seems suspiciously general. I thought it a good idea to move it to the transfer functions (to_if_expr), but in doing so some of the tests get broken. This happens because all the tests that use our internal malloc get to code that looks like this:

__CPROVER_deallocated =
    (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;

where __CPROVER_deallocated is declared as a pointer in a different file. (For a live example of this take a look here. In this case __CPROVER_deallocated's type is a symbol whereas the 0 is a constant, hence the DATA_INVARIANT failing in multiple of the tests. This seems to me that the promotion is not being handled correctly (I have also checked with the C standard n1124 and that should be typechecking, but on the condition that both the consequent and the alternative expressions are of the same type (in this case 6.5.15-3 indicates that it should typecheck on the condition that one operand is a pointer and the other is a null pointer constant).

This made me instinctively want to go and modify the parser, to do automatic implicit typecasts when it parses a conditional expression, however most of what I have tried seems to be convoluted, and most likely wrong (couldn't get them to work). Do you have any particular input on that, or maybe some pointers on what should change? If it's elaborate work, I'm happy to do it as part of a different PR and get this in as it is now if you think it's good as a cleanup PR, I just thought that moving the invariant to the transfer functions is a good piece of work in line with us not duplicating checks.

tautschnig · 2018-09-24T15:36:49Z

[...] In goto_symex_state.cpp:514 there's a DATA_INVARIANT that seems suspiciously general. I thought it a good idea to move it to the transfer functions (to_if_expr), but in doing so some of the tests get broken. [...]

This sound like a very good idea, and we should dig deeper. Would you mind creating an fresh PR doing just this (CI will fail, of course). Let's then you and I debug this - it seems that symbol types aren't uniformly expanded.

allredj

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

NlightNFotis self-assigned this Sep 5, 2018

NlightNFotis requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 5, 2018 14:16

NlightNFotis force-pushed the custom_exception branch from 44c4789 to 63543a5 Compare September 5, 2018 14:31

tautschnig requested changes Sep 5, 2018

View reviewed changes

NlightNFotis force-pushed the custom_exception branch from 63543a5 to 37d6b83 Compare September 7, 2018 21:22

NlightNFotis mentioned this pull request Sep 8, 2018

Cleanup of error handling of some of the files under goto-programs #2904

Merged

NlightNFotis force-pushed the custom_exception branch from 37d6b83 to d5cd7bd Compare September 14, 2018 15:26

tautschnig reviewed Sep 19, 2018

View reviewed changes

John Nonweiler and others added 2 commits September 20, 2018 12:27

Replace asserts and throws with INVARIANT etc.

d263ce7

Translate asserts and throws to PRECONDITIONS and INVARIANTS

8558c57

NlightNFotis force-pushed the custom_exception branch from d5cd7bd to 8558c57 Compare September 24, 2018 14:13

tautschnig approved these changes Sep 24, 2018

View reviewed changes

tautschnig merged commit 2e9e73d into diffblue:develop Sep 24, 2018

allredj reviewed Sep 24, 2018

View reviewed changes

NlightNFotis deleted the custom_exception branch February 19, 2021 11:19

Cleanup of asserts and throws under the goto-symex directory #2902

Cleanup of asserts and throws under the goto-symex directory #2902

Uh oh!

Conversation

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

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!

NlightNFotis commented Sep 7, 2018

Uh oh!

NlightNFotis commented Sep 19, 2018

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!

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

Uh oh!

Uh oh!

tautschnig commented Sep 24, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

NlightNFotis commented Sep 24, 2018 •

edited

Loading