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

NlightNFotis · 2018-09-05T15:24:56Z

This is nothing new as a PR, it's just me taking over #2836. I have now rebased and I am now responsible for further development on it.

Addressing some of the comments by @kroening on the previous PR: There should be a new PR in the next few days, where we will have structured goto_locationt inside the invariants, to my understanding at least. This PR will be extended to handle the appropriate cases once that goes in.

allredj

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

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

src/goto-programs/goto_convert_side_effect.cpp

-         statement==ID_predecrement);
+  DATA_INVARIANT(
+    statement == ID_preincrement || statement == ID_predecrement,
+    " expected preincrement or predecrement");


Spurious space at beginning of error message?

tautschnig · 2018-09-05T19:31:47Z

src/goto-programs/goto_convert_side_effect.cpp

+  DATA_INVARIANT(
+    !expr.operands().empty(),
+    expr.find_source_location().as_string() +
+      ": function_call expects at least one operand");


Above we require exactly two operands - could both of these DATA_INVARIANTs be fused into one, at the beginning of the method?

Yes, I opted to go with the stricter version (the one requiring exactly two operands) of this invariant, given that I find that both operands are being used at various points of this function.

tautschnig · 2018-09-05T19:32:14Z

src/goto-programs/goto_convert_side_effect.cpp

@@ -445,7 +430,7 @@ void goto_convertt::remove_cpp_delete(
  side_effect_exprt &expr,
  goto_programt &dest)
 {
-  assert(expr.operands().size()==1);
+  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expected 1 operand");


Let's spell out "one", for consistency. Or change all of them to numerals. There's ample inconsistency in this PR as far as this is concerned.

Agreed. I will handle all of the cases in this PR.

tautschnig · 2018-09-05T19:38:21Z

src/goto-programs/goto_program.cpp

-                     "size of target list");
+      DATA_INVARIANT(
+        instruction.targets.size() == exception_list.size(),
+        "size of target list");


Hmm, what's wrong with the size?

NlightNFotis · 2018-09-08T20:11:17Z

src/goto-programs/goto_convert_side_effect.cpp

-         statement==ID_postdecrement);
+  DATA_INVARIANT(
+    statement == ID_postincrement || statement == ID_postdecrement,
+    " expected postincrement or postdecrement");


Here's also a spurious space at the beginning of the error message, which I have gone ahead and removed.

NlightNFotis · 2018-09-08T20:15:36Z

src/goto-programs/goto_convert_side_effect.cpp

+  DATA_INVARIANT(
+    !expr.operands().empty(),
+    expr.find_source_location().as_string() +
+      ": function_call expects at least one operand");


Yes, I opted to go with the stricter version (the one requiring exactly two operands) of this invariant, given that I find that both operands are being used at various points of this function.

NlightNFotis · 2018-09-08T20:17:38Z

src/goto-programs/goto_convert_side_effect.cpp

@@ -445,7 +430,7 @@ void goto_convertt::remove_cpp_delete(
  side_effect_exprt &expr,
  goto_programt &dest)
 {
-  assert(expr.operands().size()==1);
+  DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expected 1 operand");


Agreed. I will handle all of the cases in this PR.

NlightNFotis · 2018-09-08T20:33:42Z

src/goto-programs/goto_program.cpp

@@ -235,23 +237,23 @@ void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
 {
  if(src.id()==ID_dereference)
  {
-    assert(src.operands().size()==1);
+    PRECONDITION(src.operands().size() == 1);


I figured this would go very well with the changes suggested in #2902, so I went ahead to change all of these, by removing the duplicate preconditions and converting the untyped expressions into the correct types with the typecast expressions.

NlightNFotis · 2018-09-08T20:51:15Z

@tautschnig I have fixed your comments, and I also figured out that some of the changes suggested in a previous PR of mine (#2902) were applicable here, so I removed some of the preconditions and substituted them for a finer typing of exprs at the appropriate places.

allredj

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

src/goto-programs/goto_convert_exceptions.cpp

src/goto-programs/goto_convert_side_effect.cpp

src/goto-programs/goto_program.cpp

tautschnig

Looks ok to me.

allredj

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

NlightNFotis added the do not merge label Sep 5, 2018

NlightNFotis self-assigned this Sep 5, 2018

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

This was referenced Sep 5, 2018

Convert asserts and throws to INVARIANTs for files starting with g #2836

Closed

Cleanup of throws and asserts of goto_convert.cpp #2905

Merged

allredj reviewed Sep 5, 2018

View reviewed changes

tautschnig reviewed Sep 5, 2018

View reviewed changes

NlightNFotis commented Sep 8, 2018

View reviewed changes

NlightNFotis force-pushed the 2836_takeover branch from 8654b36 to 57a04a7 Compare September 8, 2018 20:49

NlightNFotis force-pushed the 2836_takeover branch 2 times, most recently from 9b6d01a to 612ef30 Compare September 14, 2018 15:46

allredj reviewed Sep 14, 2018

View reviewed changes

peterschrammel reviewed Sep 17, 2018

View reviewed changes

Andreas Paschos and others added 2 commits September 19, 2018 12:28

Convert asserts and throws to INVARIANTs for files starting with g

fe4a218

Remove some preconditions and appropriately type the expressions.

c952f55

NlightNFotis force-pushed the 2836_takeover branch from 612ef30 to c952f55 Compare September 19, 2018 14:48

tautschnig approved these changes Sep 19, 2018

View reviewed changes

NlightNFotis removed the do not merge label Sep 19, 2018

allredj reviewed Sep 19, 2018

View reviewed changes

NlightNFotis force-pushed the 2836_takeover branch from 410dfaf to c952f55 Compare September 20, 2018 10:55

NlightNFotis merged commit a04da2e into diffblue:develop Sep 20, 2018

NlightNFotis deleted the 2836_takeover branch September 20, 2018 11:25

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

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

Uh oh!

Conversation

NlightNFotis commented Sep 5, 2018

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Sep 8, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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

Uh oh!