Preparation to make goto-analyzer work with the goto_verifiert framework #4703

hannes-steffenhagen-diffblue · 2019-05-24T10:15:10Z

Make ai_baset work with abstract_goto_modelt rather than goto_modelt
Add a version of static_verifier that works with abstract_goto_modelt and propertiest

This will (eventually) allow us to use the goto-checker stuff in goto-analyzer, which will be useful to make reporting of results and things like that more consistent with the rest of CPROVER.

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-24T10:32:38Z

src/goto-analyzer/static_verifier.cpp

+    auto &property_status = property.second.status;
+    auto const &property_location = property.second.pc;
+    auto condition = property_location->get_condition();
+    auto const predecessor = ai.abstract_state_before(property_location);


It is not obvious to me why we want to evaluate the condition in the preceding state, rather than the current one? Is it possible that evaluating the property will change the value of the condition?

xbauch

It's not really used here, but it seems to do what it claims to be doing.

owen-mc-diffblue

The first commit is fine. I didn't review the second one as I know nothing about goto-analyzer.

allredj

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

allredj

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

peterschrammel · 2019-05-28T13:02:20Z

src/goto-analyzer/static_verifier.cpp

+    }
+    else if(condition.is_false())
+    {
+      property_status = property_statust::FAIL;


Is this a definite fail? If not, then it should be UNKNOWN.

Yes, if a condition is false that means that using domain information it could be simplified to false, i.e. definite fail.

peterschrammel · 2019-05-28T13:03:21Z

src/goto-analyzer/static_verifier.cpp

+    }
+    else
+    {
+      property_status = property_statust::UNKNOWN;


How can this happen? If the location is never assigned a value then it should be NOT_REACHED.

This means the condition could not be simplified to true or false using domain information (so it's neither definite fail or success) and the domain state at the location is not bottom so the location is reachable (edit: or rather, potentially reachable), therefore it is unknown.

It would be helpful to have this commentary on the various states in the code as well, and not just in the PR :-)

I added some comments explaining what was going on

tautschnig · 2019-05-28T13:57:11Z

src/goto-analyzer/static_verifier.h

@@ -9,6 +9,8 @@ Author: Martin Brain, [email protected]
 #ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H
 #define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H

+#include <goto-checker/properties.h>
+#include <goto-programs/abstract_goto_model.h>


Wouldn't a forward declaration be sufficient?

Do you mean just for abstract_goto_modelt?

tautschnig · 2019-05-28T13:59:33Z

src/goto-analyzer/static_verifier.cpp

+  const ai_baset &ai,
+  propertiest &properties)
+{
+  auto const ns = namespacet{abstract_goto_model.get_symbol_table()};


I have complained about this before and I'll keep doing so: why is the above better than const namespacet ns{abstract_goto_model.get_symbol_table()};? To me it seems that would be shorter and avoid any doubt about 1) the type of the object and 2) whether some operator= is being invoked or not. And if "consistency" is part of the rationale: in fact the above is the only case of auto that's not in violation of our current coding guidelines...

I keep going after this, because I'm worried that we will at some point arrive at write-only code. Explicitly spelling out types may seem like a nuisance to the person writing the code, but they are really helpful to any reader. In the code below, I actually have no idea what the types of property_status or predecessor are. Alas I'm actually unable to judge whether (not) using references is the right thing.

I have to say I share the concerns of @tautschnig too, though he's put them more eloquently than I probably would have done. I'm not a huge fan of auto in anything other than very trivial contexts.

I don't omit the types here because I don't care about readability, but rather because in my opinion they're not very useful for readability; I did another scan over the code and tried to clarify as much a possible, adding types where I thought they're useful. I kept the auto in the for loop and for property_status - the former because it'd otherwise just be propertiest::value_type which IMHO doesn't really add much useful information, and the latter because the type would be property_statust which again doesn't really communicate anything over the variable name.

(Side note: operator= is never involved in initialisation)

romainbrenguier · 2019-05-29T06:53:05Z

src/goto-analyzer/static_verifier.h

@@ -23,4 +25,9 @@ bool static_verifier(
  message_handlert &,
  std::ostream &);

+void static_verifier(


This should be documented. And it's a bit confusing to use a noun for a function which is returning void. (for me "verifier" here should imply you return an object which has a verify method)

This is doing more or less the same thing as the other static_verifier function that already is in this file, the only difference is that it writes the result to the propertiest passed in rather than writing them to stdout or to a file.

The "return" value here is the properties parameter (it's an in/out parameter, we read some information from each property and write its verification status back to it)

tautschnig · 2019-05-30T08:36:27Z

@hannes-steffenhagen-diffblue Please rebase now that #4729 is in to make CI happy.

There is no need to restrict it to goto_modelt, this makes it easier to use in some contexts.

This will make it easier to use with static_verifiert going forward.

codecov-io · 2019-06-03T11:17:31Z

Codecov Report

❗ No coverage uploaded for pull request base (develop@f175f75). Click here to learn what that means.
The diff coverage is 26.31%.

@@            Coverage Diff             @@
##             develop    #4703   +/-   ##
==========================================
  Coverage           ?   68.44%           
==========================================
  Files              ?     1270           
  Lines              ?   104817           
  Branches           ?        0           
==========================================
  Hits               ?    71744           
  Misses             ?    33073           
  Partials           ?        0

Impacted Files	Coverage Δ
src/goto-analyzer/static_verifier.cpp	`45.16% <0%> (ø)`
src/analyses/ai.h	`59.15% <100%> (ø)`

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update f175f75...0f4a362. Read the comment docs.

allredj

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

hannes-steffenhagen-diffblue requested review from chrisr-diffblue, danpoe, martin-cs, owen-mc-diffblue, peterschrammel, smowton and thk123 as code owners May 24, 2019 10:15

xbauch reviewed May 24, 2019

View reviewed changes

xbauch approved these changes May 24, 2019

View reviewed changes

owen-mc-diffblue approved these changes May 24, 2019

View reviewed changes

allredj reviewed May 24, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature/goto-analyzer-usability branch from 4b0eb7f to fadb25a Compare May 24, 2019 14:55

allredj reviewed May 24, 2019

View reviewed changes

peterschrammel approved these changes May 28, 2019

View reviewed changes

tautschnig reviewed May 28, 2019

View reviewed changes

tautschnig assigned hannes-steffenhagen-diffblue May 28, 2019

hannes-steffenhagen-diffblue force-pushed the feature/goto-analyzer-usability branch 2 times, most recently from da3dd1d to 80daeef Compare May 28, 2019 18:11

romainbrenguier reviewed May 29, 2019

View reviewed changes

hannes-steffenhagen-diffblue force-pushed the feature/goto-analyzer-usability branch from 80daeef to 17d4503 Compare May 29, 2019 10:54

tautschnig added the Needs rebase label May 30, 2019

hannes-steffenhagen-diffblue added 2 commits June 3, 2019 11:17

Make ai_baset::operator() work with abstract_goto_modelt

c1b3ffb

There is no need to restrict it to goto_modelt, this makes it easier to use in some contexts.

Add a version of static_verifier that works with propertiest

0f4a362

This will make it easier to use with static_verifiert going forward.

hannes-steffenhagen-diffblue force-pushed the feature/goto-analyzer-usability branch from 17d4503 to 0f4a362 Compare June 3, 2019 10:17

tautschnig removed the Needs rebase label Jun 3, 2019

allredj reviewed Jun 3, 2019

View reviewed changes

tautschnig merged commit 798f651 into diffblue:develop Jun 3, 2019

Preparation to make goto-analyzer work with the goto_verifiert framework #4703

Preparation to make goto-analyzer work with the goto_verifiert framework #4703

Uh oh!

Conversation

hannes-steffenhagen-diffblue commented May 24, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch left a comment

Choose a reason for hiding this comment

Uh oh!

owen-mc-diffblue 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!

hannes-steffenhagen-diffblue May 28, 2019 • 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!

hannes-steffenhagen-diffblue May 28, 2019 • 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!

hannes-steffenhagen-diffblue May 29, 2019 • 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!

tautschnig commented May 30, 2019

Uh oh!

codecov-io commented Jun 3, 2019

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue May 28, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 28, 2019 •

edited

Loading

hannes-steffenhagen-diffblue May 29, 2019 •

edited

Loading