Invariant cleanup in goto programs i* #2952

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Closed

hannes-steffenhagen-diffblue wants to merge 5 commits into diffblue:develop from hannes-steffenhagen-diffblue:invariant_cleanup-goto-programs-i_r

Contributor

hannes-steffenhagen-diffblue commented Sep 14, 2018 •

edited

Loading

This PR is part of the invariant cleanup work, for the files in goto-programs starting with i.

This entails replacing asserts with cprover style invariants, using structured exception types and using to_XXX_expr style conversions instead of 'structure' asserts for expressions.

hannes-steffenhagen-diffblue added the work in progress label

hannes-steffenhagen-diffblue requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners

September 14, 2018 10:14

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

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

xbauch reviewed

View reviewed changes

src/goto-programs/interpreter_class.h Outdated

                   if(v.size()!=1)
-                    throw "invalid boolean value";
+                    throw interpreter_errort("invalid boolean value");

Contributor

xbauch Sep 20, 2018

I wonder if this shouldn't be an invariant. The input expr is always the path condition of the interpreted program and I don't think the user is directly responsible for what the interpreter chooses to be a path condition.

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto-programs-i_r branch 2 times, most recently from 129444d to cd0bd66 Compare

September 21, 2018 11:17

tautschnig assigned hannes-steffenhagen-diffblue

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto-programs-i_r branch from cd0bd66 to dec77b7 Compare

October 3, 2018 13:50

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto-programs-i_r branch from dec77b7 to 79efa6d Compare

October 11, 2018 09:40

hannes-steffenhagen-diffblue added 4 commits

October 11, 2018 12:00


          Use structured exceptions in initialize_goto_model

4ff7318


          Replace throws with structured throws or invariant in interpreter

c842c01


          Add pointer_offset_exprt

d8f8cf3


          Use structured invariant in interpreter_class.h

c8329fb

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto-programs-i_r branch from 79efa6d to 11af196 Compare

October 11, 2018 11:07

hannes-steffenhagen-diffblue commented

View reviewed changes

src/goto-programs/initialize_goto_model.cpp

-                      msg.error() << "failed to figure out type of file" << messaget::eom;
-                      throw 0;
+                      throw invalid_source_file_exceptiont(
+                        "Failed to figure out type of file `" + filename + '\'');

Contributor Author

hannes-steffenhagen-diffblue Oct 11, 2018

This should arguably happen before the check whether the file can be opened, but that's a minor point and not really within the spirit of this PR

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

This PR failed Diffblue compatibility checks (cbmc commit: 79efa6d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87615645
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

xbauch approved these changes

View reviewed changes

Contributor

xbauch left a comment

It might be a little bit more readable if the variable renaming was in a separate commit. But other than that, it looks good to me.

martin-cs approved these changes

View reviewed changes

Collaborator

martin-cs left a comment

Thanks for the clean-up. Comments are mostly opinions on what kind of error conditions these are.

src/goto-programs/interpreter.cpp

@@ @@ -69,12 +69,12 @@ void interpretert::initialize(bool init) @@
                   main_it=goto_functions.function_map.find(goto_functionst::entry_point());
                 if(main_it==goto_functions.function_map.end())
-                  throw "main not found";
+                  throw analysis_exceptiont("main not found");

Collaborator

martin-cs Oct 11, 2018

Is this actually a structural invariant on goto-programs?

Contributor Author

hannes-steffenhagen-diffblue Oct 11, 2018

I wasn't sure about this one, because you might have goto programs without an entry point (libraries mostly). I suppose it could be a precondition if we assume that a caller should've checked for an entry point before calling this.

Collaborator

martin-cs Oct 11, 2018

It is getting in to the heart of why we need to check that goto-programs are well formed and to clarify what "normal forms" exist for them. If it has been linked and is a complete goto program then it should have an entry point which is a function in the map. If it is only partially built (goto-cc -c for example) then it may not do. It is not immediately clear to me whose fault it would be to try to interpret a n "object file" rather than an "executable".

src/goto-programs/interpreter.cpp

                 const goto_functionst::goto_functiont &goto_function=main_it->second;
                 if(!goto_function.body_available())
-                  throw "main has no body";
+                  throw analysis_exceptiont("main has no body");

Collaborator

martin-cs Oct 11, 2018

As above.

src/goto-programs/interpreter.cpp

-                    throw "RETURN without call"; // NOLINT(readability/throw)
+                  {
+                    throw analysis_exceptiont(
+                      "RETURN without call"); // NOLINT(readability/throw)

Collaborator

martin-cs Oct 11, 2018

I think this is an INVARIANT as if the interpreter is working as it should, then this should never happen.

Contributor Author

hannes-steffenhagen-diffblue Oct 11, 2018

I was thinking this could happen in a nonsensical goto program that has returns in unexpected places, such as __CPROVER_initialize. Is that wrong?

Collaborator

martin-cs Oct 11, 2018

If I understand the code correctly (and it is possible I don't) then the INVARIANT is that the number of RETURNS executed should never exceed the number of functions started. So this should always hold.

src/goto-programs/interpreter.cpp

@@ @@ -317,19 +320,23 @@ void interpretert::step() @@
                 case START_THREAD:
                   trace_step.type=goto_trace_stept::typet::SPAWN;
-                  throw "START_THREAD not yet implemented"; // NOLINT(readability/throw)
+                  throw analysis_exceptiont(
+                    "START_THREAD not yet implemented"); // NOLINT(readability/throw)

Collaborator

martin-cs Oct 11, 2018

UNIMPLEMENTED ? Also below.

src/goto-programs/interpreter.cpp

@@ @@ -359,7 +366,7 @@ void interpretert::step() @@
                 case CATCH:
                   break;
                 default:
-                  throw "encountered instruction with undefined instruction type";
+                  UNREACHABLE; // I'm assuming we'd catch such a thing before this point

Collaborator

martin-cs Oct 11, 2018

Sounds like you're saying it is a consequence of the goto program being well-formed ;-)

src/goto-programs/interpreter.cpp

@@ @@ -724,15 +730,15 @@ void interpretert::assign( @@
               void interpretert::execute_assume()
               {
                 if(!evaluate_boolean(pc->guard))
-                  throw "assumption failed";
+                  throw analysis_exceptiont("assumption failed");

Collaborator

martin-cs Oct 11, 2018

Unrelated to this; I'm not sure this is the right way of handling this case. I think it should just terminate correctly.


          Invariant cleanup in interpreter_evaluate.cpp

ce7f792

This mostly entails using to_XXX_expr in place of using ad hoc asserts.
At the same time, some minor cleanup work is done to improve the
readability of the affected code

hannes-steffenhagen-diffblue force-pushed the invariant_cleanup-goto-programs-i_r branch from 11af196 to ce7f792 Compare

October 11, 2018 13:32

Contributor Author

hannes-steffenhagen-diffblue commented Oct 11, 2018

@martin-cs Yes, since I'm not super familiar with this code myself I was a bit unclear in many cases about whether INVARIANT or exception is the better 'mechanism' to use. I'll have another look over the cases you pointed out.

Collaborator

martin-cs commented Oct 11, 2018

@hannes-steffenhagen-diffblue : The test I tend to you is : if there are a set of user controllable flags and a non-corrupted / incorrect program that can cause it to happen, it is a potential user error and should be an exception. If the only way it can happen is if there are one or more bugs in CPROVER, then it should be an invariant of some kind.

Contributor Author

hannes-steffenhagen-diffblue commented Oct 11, 2018

@martin-cs I completely agree with that, it's just difficult to judge on a case by case basis sometimes.

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

This PR failed Diffblue compatibility checks (cbmc commit: 11af196).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87644100
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

Contributor Author

hannes-steffenhagen-diffblue commented Oct 11, 2018 •

edited

Loading

Heads up, I'm a bit uncomfortable with putting these changes in as the interpreter seems to be broken and untested atm.

I'll extract the initialize_goto_model stuff as that seems to be unrelated

allredj reviewed

View reviewed changes

Contributor

allredj left a comment

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

Collaborator

martin-cs commented Oct 11, 2018

@hannes-steffenhagen-diffblue : It is difficult to judge; this is why I try to phrase my comments on these as "IMHO it should be".

As regards the interpreter; it didn't use to be in a great state but I thought someone at Diffblue had taken over it's care and feeding. I have a vague feeling that @dcattaruzza was asking about it at one point...

tautschnig approved these changes

View reviewed changes

Collaborator

tautschnig left a comment

Looks ok to me (with one comment below); but really this should be checked against TG, where I believe some interpreter tests exist.

src/goto-programs/interpreter_class.h

                   if(v.size()!=1)
-                    throw "invalid boolean value";
+                    throw analysis_exceptiont("invalid boolean value");

Collaborator

tautschnig Oct 12, 2018

I would drop the FIXME and turn this into an INVARIANT. People will start complaining if it's not actually an invariant... :-)

Contributor Author

hannes-steffenhagen-diffblue commented Oct 17, 2018

I extracted the initialize_goto_model bit because that is tested, short, and fairly trivial (no changing of conditions, just different exception types) #3190

hannes-steffenhagen-diffblue closed this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

martin-cs martin-cs approved these changes

allredj allredj left review comments

tautschnig tautschnig approved these changes

xbauch xbauch approved these changes

kroening Awaiting requested review from kroening kroening is a code owner

peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

pkesseli Awaiting requested review from pkesseli

smowton Awaiting requested review from smowton

Labels

work in progress