Document and refactor goto check #4611

xbauch · 2019-05-03T10:02:13Z

If you go commit-by-commit it's not so horrible. There is not functional change only a bit of rewording.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
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).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

xbauch · 2019-05-03T10:42:45Z

src/analyses/goto_check.cpp

-    throw msg;
-  }
+  INVARIANT(
+    !if_expr.cond().is_boolean(),


Should have been negated: sorry. Will be fixed.

tautschnig

This does need cleanup as indicated in the comments, but is overall a good refactoring.

tautschnig · 2019-05-06T08:56:21Z

src/analyses/goto_check.cpp

@@ -102,6 +102,8 @@ class goto_checkt
  ///   operands (or their negations) for recursively calls)
  void check_rec_logical_op(const exprt &expr, guardt &guard);

+  void check_rec_if(const exprt &expr, guardt &guard);


I think this should just take an if_exprt instead of doing the check within the method.

tautschnig · 2019-05-06T08:57:20Z

src/analyses/goto_check.cpp

@@ -110,6 +110,8 @@ class goto_checkt
  ///   the) if-condition for recursively calls)
  void check_rec_if(const exprt &expr, guardt &guard);

+  void check_rec_member(const exprt &expr, guardt &guard);


Should just take a member_exprt

tautschnig · 2019-05-06T08:58:48Z

src/analyses/goto_check.cpp

-      guard.add(not_exprt(op));
-    else
-      guard.add(op);
+    guard.add(expr.id() == ID_or ? not_exprt(op) : op);


If you are touching this, I'd suggest to use boolean_negate(op) instead of not_exprt(op)

tautschnig · 2019-05-06T09:00:12Z

src/analyses/goto_check.cpp

-      return;
-    }
+    check_rec_member(expr, guard);
+    return;


This return doesn't seem correct to me. I think you should remove it, and also remove the final forall_operands from check_rec_member.

The return is there only to prevent the forall_operands loop in case the check_rec_member was existed via an explicit return. But it seems to be only an optimisation so I did what you asked for.

I take it back. Avoiding the recursive call on the member expression operands may be just an optimisation but one of our regression tests (Malloc23) requires exactly 4 failing assertions. If we change this section so that the recursion is always called, this test fails.

Which ... might be a bugfix? Does it generate more assertions or is it missing some?

Doesn't seem so:

struct A { int x; int y; }; int main() { struct A *p=malloc(sizeof(int)); p->x=0; // OK p->y=0; // out of bounds ..

Unless we skip the recursive call, we would generate a pointer check for p->ok=0 which, on it's own, would fail.

But still the behaviour before and after isn't the same: previously, we only returned in some cases, now we always return early.

Yes, but since I included the recursive call on sub-expressions in rec_check_member the only thing we skip by returning early is the remaining case analyses none of which can succeed (since we know that expr.id()==ID_member).

Fair enough, I was just a bit worried that one day someone would add a case. But I suppose testing (or rather: failing tests) should catch that. So it seems fine as is.

I thought about it a bit and tried having the check_rec_member return a Boolean indicating if the subsequent analysis should be attempted or not: d6f7f05.

tautschnig · 2019-05-06T09:03:43Z

src/analyses/goto_check.cpp

+  ///   NaN (for floating point numbers).
+  /// \param expr: the expression to be checked
+  /// \param guard: the condition for the check (unmodified here)
+  void check_rec_div(const exprt &expr, guardt &guard);


Should take a div_exprt

tautschnig · 2019-05-06T09:08:41Z

src/analyses/goto_check.cpp

-    guarded_expr = implies_exprt(guard.as_expr(), std::move(simplified_expr));
+  exprt guarded_expr =
+    guard.is_true()
+      ? simplified_expr


std::move(simplified_expr)

tautschnig · 2019-05-06T09:10:29Z

src/analyses/goto_check.cpp

+      enable_assert_to_assume ? goto_programt::make_assumption(
+                                  std::move(guarded_expr), source_location)
+                              : goto_programt::make_assertion(
+                                  std::move(guarded_expr), source_location));


There is another instance of this pattern (around line 1800) - just search for "ASSUME". Could you please fix this as well?

tautschnig · 2019-05-06T09:14:14Z

src/analyses/goto_check.cpp

-      it=next;
+        it = assertions.erase(it);
+      else
+        ++it;
    }


What about using std::remove_if (until we can use erase_if with C++20)?

Unfortunately, std::remove_if requires the iterator to be MoveAssignable. Will have to wait for this one.

Ah, ok, too bad.

peterschrammel

lgtm modulo squashing promised

peterschrammel · 2019-05-18T20:50:42Z

src/analyses/goto_check.cpp

+  /// \param source_location: the source location of the original expression
+  /// \param src_expr: the original expression to be included in the comment
+  /// \param guard: the condition under which the asserted expression should be
+  ///   taken into account
  void add_guarded_claim(


While we are here, can we rename claim to property since we have replaced that terminology in other places in the codebase?

peterschrammel · 2019-05-18T20:52:46Z

src/analyses/goto_check.cpp

@@ -194,6 +199,10 @@ class goto_checkt
  typedef std::set<exprt> assertionst;
  assertionst assertions;

+  /// Remove all assertions containing they symbol in \p lhs as well as all


they -> the

from check_rec into stand-alone function. Getting rid of the flag.

Using the checks inside to_expr methods.

into a stand-alone function.

Using invariants instead of exceptions.

into add_guarded_property.

Using invariants, to-conversion and a bit of clang-formatting.

Only clang-format, inline expr-construction, and for-each loop.

Into check_rec_div and check_rec_arithmetic_op.

Using the initializer-list constructor for sets and and standard idiom for erase_if.

instead of instructiont constructor.

to negate boolean expression and to get address_of expression.

to collect_allocations, check_rec, and check.

for the bits we touched in this PR.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d62fe0a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/112345526
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

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

xbauch requested review from chrisr-diffblue, danpoe, martin-cs, owen-mc-diffblue, peterschrammel, smowton and thk123 as code owners May 3, 2019 10:02

NlightNFotis approved these changes May 3, 2019

View reviewed changes

xbauch commented May 3, 2019

View reviewed changes

tautschnig approved these changes May 6, 2019

View reviewed changes

tautschnig added the cleanup label May 6, 2019

tautschnig assigned peterschrammel and chrisr-diffblue May 6, 2019

xbauch force-pushed the refactor/goto-check branch from 91b9614 to 5289c58 Compare May 6, 2019 14:15

peterschrammel approved these changes May 18, 2019

View reviewed changes

peterschrammel assigned xbauch and unassigned peterschrammel May 18, 2019

xbauch force-pushed the refactor/goto-check branch from d6f7f05 to aa16fd6 Compare May 19, 2019 07:18

petr-bauch added 12 commits May 19, 2019 09:17

Separate checking address-of expressions

60e119d

from check_rec into stand-alone function. Getting rid of the flag.

Clean-up and document check_rec_address

a3f70a7

Using the checks inside to_expr methods.

Separate checking logical operators

41f7f46

into a stand-alone function.

Clean-up and document check_rec_logical_op

102b5b0

Using invariants instead of exceptions.

Refactor, rename, and document add_guarded_claim

1f105fe

into add_guarded_property.

Separate and refactor checking if

d74ef71

Using invariants, to-conversion and a bit of clang-formatting.

Separate and refactor checking member

266f00b

Only clang-format, inline expr-construction, and for-each loop.

Separate and document checking arithmetic ops

2662f2b

Into check_rec_div and check_rec_arithmetic_op.

Document and refactor invalidate

f931965

Using the initializer-list constructor for sets and and standard idiom for erase_if.

Use make_assumption/assertion wrappers

c7c94b2

instead of instructiont constructor.

Use built-in methods

cecc289

to negate boolean expression and to get address_of expression.

Add documentation

e0eab84

to collect_allocations, check_rec, and check.

Clang-formatting

b5060ee

for the bits we touched in this PR.

xbauch force-pushed the refactor/goto-check branch from d62fe0a to b5060ee Compare May 19, 2019 08:17

allredj reviewed May 19, 2019

View reviewed changes

xbauch merged commit 230e525 into diffblue:develop May 19, 2019

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Document and refactor goto check #4611

Document and refactor goto check #4611

xbauch commented May 3, 2019

xbauch May 3, 2019

tautschnig left a comment

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 7, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

xbauch May 6, 2019

tautschnig May 6, 2019

peterschrammel left a comment

peterschrammel May 18, 2019

xbauch May 19, 2019

peterschrammel May 18, 2019

xbauch May 19, 2019

allredj left a comment

allredj left a comment

Document and refactor goto check #4611

Document and refactor goto check #4611

Conversation

xbauch commented May 3, 2019

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment