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

sonodtt · 2018-09-06T14:45:40Z

Cleanup of asserts - replaced with invariants.

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

hannes-steffenhagen-diffblue · 2018-09-06T14:53:22Z

Contains minor refactoring of related code.

hannes-steffenhagen-diffblue · 2018-09-06T14:54:32Z

src/util/simplify_expr_int.cpp

-  if(!is_bitvector_type(op0_type))
-    return true;
+  PRECONDITION(expr.id() == ID_extractbit);
+  auto &extractbit_expr = to_extractbit_expr(expr);


Should be auto const&

tautschnig · 2018-09-06T14:58:36Z

src/util/simplify_expr_int.cpp

+      INVARIANT(
+        !bytes.empty(),
+        "bytes is not empty because we just pushed just as many elements on "
+        "top of it as we are popping now");


May I suggest to move this out of the loop and instead check that at least as many elements are contained in bytes?

@tautschnig I'm inclined to feel that the invariant here is checking for UB in case someone makes an error in the loop condition.
Moving the invariant out of the loop would seem to check something that is trivially true (I think...).

Ok, not a big deal, I personally would have thought we don't need to guard against all possible future errors, but figuring out where exactly to draw this line is hard. Surely not a blocker here.

tautschnig · 2018-09-06T15:35:46Z

src/util/simplify_expr_int.cpp

+    INVARIANT(
+      constant_found,
+      "c_sizeof_type is only set to a non-nil value "
+      "if a constant has been found");


Hmm, having two entangled variables is questionable - I know, not your design choice, but still worth looking into I'd say.

The redesign of this section to disentangle these two variables might be considered not in the scope of the PR.

tautschnig · 2018-09-06T15:36:40Z

src/util/simplify_expr_int.cpp

@@ -439,6 +445,8 @@ bool simplify_exprt::simplify_mod(exprt &expr)

 bool simplify_exprt::simplify_plus(exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_plus);


There's a plus_exprt, let's use this here.

You mean to_plus_exprt instead of the PRECONDITION? I don't like that too much, the PRECONDITION here makes it clear we're expecting a plus_exprt whereas calling to_plus_exprt instead might be read as us just forgetting to check if it actually is...

I was meaning to suggest that the function take a plus_exprt &expr as parameter. Will discuss further with extractbit below.

tautschnig · 2018-09-06T15:37:07Z

src/util/simplify_expr_int.cpp

@@ -597,14 +603,14 @@ bool simplify_exprt::simplify_plus(exprt &expr)

 bool simplify_exprt::simplify_minus(exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_minus);


Use minus_exprt.

tautschnig · 2018-09-06T15:38:35Z

src/util/simplify_expr_int.cpp

-  if(!is_bitvector_type(op0_type))
-    return true;
+  PRECONDITION(expr.id() == ID_extractbit);
+  auto &extractbit_expr = to_extractbit_expr(expr);


Pass extractbit_exprt as parameter, and let to_extractbit_expr do all the work (at the call site) - no need for duplication.

This can't take an extractbit_exprt because the parameter is an in/out parameter, and the result is not always going to be another extractbit_exprt

We have this problem across all simplifier functions. The cleanest approach might be changing the return type from bool to something more elaborate so that we can return the modified expression, and would instead take a const reference as argument. Thus far, the workaround was using swap instead of direct assignments. I think it's important to get rid of the duplicate checks on input parameters (there should only be a check at the call site).

@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)

#2939 (comment)

tautschnig · 2018-09-06T15:39:50Z

src/util/simplify_expr_int.cpp

+  {
+    return true;
+  }
+  mp_integer index_as_int = index_converted_to_int.has_value();


That's ... trivially true? You might have wanted .value() instead of has_value?

tautschnig · 2018-09-06T15:41:11Z

src/util/simplify_expr_int.cpp


-  mp_integer i;
+  std::size_t src_bit_width = to_bitvector_type(src_type).get_width();


tautschnig · 2018-09-06T15:41:49Z

src/util/simplify_expr_int.cpp

    return true;
+  }


I believe this check is unnecessary as the subsequent numeric_cast<mp_integer> would catch this case anyway.

tautschnig · 2018-09-06T15:43:48Z

src/util/simplify_expr_int.cpp

    return true;

-  bool bit=(id2string(value)[width-integer2size_t(i)-1]=='1');
+  bool bit =
+    (id2string(src_value)


Do id2string earlier on as doing src_value.size() will also require building the string.

allredj

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: d12acb3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84135814
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-27T10:45:53Z

src/util/simplify_expr_int.cpp

+
+    //May I suggest to move this out of the loop and instead check that at least as many elements are contained in bytes?
+      // this invariant protects against someone modifying the loop
+        // expression - a bit pointless for it to be outside the loop.


I don't think this belongs in here?

tautschnig · 2018-09-27T10:46:19Z

src/util/simplify_expr_int.cpp

-      // this invariant protects against someone modifying the loop
-        // expression - a bit pointless for it to be outside the loop.
+    // this invariant protects against someone modifying the loop
+    // expression - a bit pointless for it to be outside the loop.


I'd get rid of this.

Apologies @tautschnig - this was an internal note for a colleague for a second opinion.
I was used to a workflow where I'd push to get CI going, review, then re-add reviewers to flag ready for re-review.
You often re-review quite quickly - in future will push after local checks.

Oh don't worry, I was just naively assuming this was ready for re-review.

allredj

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

allredj

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

hannes-steffenhagen-diffblue · 2018-10-01T15:04:56Z

@tautschnig Can you rereview? There is a clang-format failure that I can't fix at the moment

~~(I'm not at my usual workstation and the version of clang-format I have here seems to disagree with what's running on travis), so I wouldn't merge it yet, but I could just easily fix that tomorrow~~

NVM the above part, it's been rightfully pointed out to me that not having a one line change be done automatically for you is a stupid reason to delay it.

* C-style asserts are deprecated in favor of CBMCs INVARIANT macros * Some minor refactoring that was relevant to the cleanup.

allredj

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

tautschnig

Just a few minor suggestions.

tautschnig · 2018-10-01T18:01:40Z

src/util/simplify_expr_int.cpp

@@ -604,43 +604,42 @@ bool simplify_exprt::simplify_plus(exprt &expr)

 bool simplify_exprt::simplify_minus(exprt &expr)
 {
+  auto const &minus_expr = to_minus_expr(expr);


The lines after this one still use expr, not minus_expr

I've made the functions use them where it seemed reasonable.

tautschnig · 2018-10-01T18:03:09Z

src/util/simplify_expr_int.cpp

@@ -446,6 +446,8 @@ bool simplify_exprt::simplify_mod(exprt &expr)

 bool simplify_exprt::simplify_plus(exprt &expr)
 {
+  // only used to check structural invariants
+  (void)to_plus_expr(expr);


Maybe still use this, in particular the const version thereof, in the next lines? Doing .type() on a const expression is cheaper, thus beneficial.

* Use to_minus_expr instead of asserting the expression id * Rename the local variables for easier readability

to_plus_expr should check if an expression is a plus_exprt, this avoids duplicating checks across the codebase

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 07f7d1e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86591624
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: 69e5c2d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86592975

sonodtt requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners September 6, 2018 14:45

hannes-steffenhagen-diffblue approved these changes Sep 6, 2018

View reviewed changes

tautschnig requested changes Sep 6, 2018

View reviewed changes

allredj reviewed Sep 6, 2018

View reviewed changes

tautschnig mentioned this pull request Sep 7, 2018

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

Merged

allredj reviewed Sep 7, 2018

View reviewed changes

sonodtt force-pushed the invariant-cleanup-util_dir-s_files-part2 branch from d12acb3 to 3ef24a2 Compare September 21, 2018 08:22

tautschnig assigned sonodtt Sep 24, 2018

tautschnig reviewed Sep 27, 2018

View reviewed changes

sonodtt mentioned this pull request Sep 27, 2018

Refactor simplify floatbv typecast #2939

Closed

sonodtt force-pushed the invariant-cleanup-util_dir-s_files-part2 branch 4 times, most recently from b34cee7 to 05debde Compare September 27, 2018 15:07

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-s_files-part2 branch from 05debde to d3a148d Compare September 27, 2018 16:25

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

allredj reviewed Sep 27, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-s_files-part2 branch 2 times, most recently from 5083a53 to bd2558b Compare October 1, 2018 11:38

allredj reviewed Oct 1, 2018

View reviewed changes

Cleanup asserts & throws - replace with invariants

4924fb8

* C-style asserts are deprecated in favor of CBMCs INVARIANT macros * Some minor refactoring that was relevant to the cleanup.

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-s_files-part2 branch from bd2558b to d5837ad Compare October 1, 2018 15:19

allredj reviewed Oct 1, 2018

View reviewed changes

tautschnig approved these changes Oct 1, 2018

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-s_files-part2 branch from d5837ad to 07f7d1e Compare October 2, 2018 10:37

hannes-steffenhagen-diffblue added 2 commits October 2, 2018 11:49

Refactor simplify_minus

fdc4680

* Use to_minus_expr instead of asserting the expression id * Rename the local variables for easier readability

Use to_plus_expr instead of assert in simplify_plus

69e5c2d

to_plus_expr should check if an expression is a plus_exprt, this avoids duplicating checks across the codebase

hannes-steffenhagen-diffblue force-pushed the invariant-cleanup-util_dir-s_files-part2 branch from 07f7d1e to 69e5c2d Compare October 2, 2018 10:50

allredj reviewed Oct 2, 2018

View reviewed changes

tautschnig merged commit 2d63171 into diffblue:develop Oct 2, 2018


		mp_integer i;
		std::size_t src_bit_width = to_bitvector_type(src_type).get_width();

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

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

Uh oh!

Conversation

sonodtt commented Sep 6, 2018

Uh oh!

hannes-steffenhagen-diffblue commented Sep 6, 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!

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 27, 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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sonodtt Sep 27, 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!

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

Uh oh!

sonodtt Sep 27, 2018 •

edited

Loading

sonodtt Sep 27, 2018 •

edited

Loading

hannes-steffenhagen-diffblue commented Oct 1, 2018 •

edited

Loading