Add support for path exploration to CBMC/JBMC, in addition to full bounded model checking by karkhaz · Pull Request #1641 · diffblue/cbmc

karkhaz · 2017-11-29T18:25:13Z

CBMC can now model-check each path of a program one at a time, displaying the verification result for that path before continuing to symbolically execute other paths. This functionality is similar to what the symex tool provides, but uses the goto-symex core that is already used by CBMC rather than having a disjoint symbolic execution codebase. This functionality is enabled by passing the --paths flag to CBMC or JBMC.

When --paths is passed, CBMC does not perform path merging when it encounters a program join point. Instead, whenever it encounters a conditional goto instruction, it saves the state of the symbolic executor onto a workqueue and executes one of the branches. Once symbolic execution has finished and the verification result printed out, CBMC pops the workqueue and resumes executing the untaken branch.

This is all integrated with the existing bmc and goto_symext classes, with no change in CBMC's original model-checking functionality. Without the --paths flag, CBMC's full-program model-checking behaviour is an edge-case of path exploration, whereby no goto branch-points are saved and so the entire program is only symbolically executed once.

The main patch in this patchset is [path explore 5/6] Support path-based exploration. Other commits are fairly small and introduce features that are necessary for path exploration, but which are also desirable changes by themselves.

martin-cs · 2017-11-29T18:52:05Z

Thanks for this patch set; it looks really exciting.

Paging @theyoucheng who has a similar patch set and @bjowac who was the original author of symex. Also cross linking against #749 for my last attempt at getting everyone who cared about per-path symex talking to each other so we didn't duplicate work.

karkhaz · 2017-11-29T21:44:37Z

@martin-cs thanks for the comment. This is a complete implementation and is working well, but I'd like to braindump a few future refinements here for the record:

Different heuristics for deciding which path to execute next. The implementation in this pull request is a simple FIFO, i.e. whenever we get to a branch point, we save the path that we don't execute for now, and resume paths in the order that they were saved. It turns out that this isn't a great strategy. I should have better ones in the next few weeks.
Multithreaded CBMC. This is exciting! Every path that is symbolically executed could be done in a different thread. The only data structure that needs to be shared is the workqueue where upcomming paths are saved, so we'd need to lock that (and it's potentially a fairly hot data structure). Mark Tuttle suggests that to remedy this, we could experiment with every thread having its own local queue of paths to execute next, and pull paths from the global workqueue only when the local one gets emptied (and of course, every thread should contribute paths to resume to the global workqueue).
Another way to avoid this issue entirely is to have all symbolic execution happen in the main thread, but fork off the SAT solver in a different thread or process (so that CBMC is symbolically executing one path while the SAT solver checks another).
In either case, thread/process control would be done entirely from the method bmct::do_language_agnostic_bmc, which is a method that is introduced in this patchset. I expect that doing this wouldn't be too invasive, but we'd need to add an implementation of a thread or process pool to the codebase.

cheers!

smowton

Some comments. Mostly doxy comments, style and some inconsistency in how the arguments are described. Most substantively I'd appreciate comments where appropriate about why namespaces are being re-initialised to point at different symbol tables, and at what stage they point to different places (therefore, if a future coder is editing goto_symext and adds an ns.lookup, what tables do they think they're referring to? Is it outright invalid (uninitialised) at any point?)

smowton · 2017-11-30T10:06:31Z

src/cbmc/bmc.cpp

Take by reference?

smowton · 2017-11-30T10:07:41Z

src/cbmc/bmc.cpp

Recommend making a "should" statement here, as otherwise it's often confusing whether the statement says what should have been or what went wrong.

smowton · 2017-11-30T10:08:57Z

src/cbmc/bmc.cpp

Recommend throwing structured errors rather than plain strings wherever possible

@smowton this catch is to deal with a throw from cbmc_solverst, i.e. it's code that predates this patchset. As far as I can see, that code only ever throws the number 0 (and it prints a message to messaget::error() just before it throws). I'm not familiar with cprover's error handling, what sort of error would you recommend that I throw from cbmc_solvert instead of 0? Or should I just leave that there?

"Pretty crap," in brief ;) If it's old code you're catching from, I guess you intend to catch everything? In that case I'd catch const char * and const std::string & (perhaps mergable if exception catching permits implicit construction to catch, but I doubt it) and then catch(...) to catch other errors. If you specifically intend to catch some things but let others get by then you should at least document your intent in comments, and probably change the throwing code to throw something more specific.

#include "martin_comment_about_catch_all_vs_invariants.h"

If you are going to catch (...) please exit and / or throw upwards; many exceptions are non-recoverable.

smowton · 2017-11-30T10:10:19Z

src/cbmc/bmc.cpp

If there are this many args, probably clearest to break after ( and then list one argument per line

smowton · 2017-11-30T10:10:49Z

src/cbmc/bmc.cpp

Please add function-level doxy comments

The prevalent style seems to be having the doxy comments in header files, right? I already have one there, but it's a bit brief so I'll expand it.

smowton · 2017-11-30T10:40:44Z

src/goto-symex/symex_goto.cpp

If this is a debug message, guard with #ifdef DEBUG_GOTO_SYMEX or something (and the same for iostream include above). Otherwise, use a messaget or get one passed in.

If #1625 gets merged in before this, symext will have a messaget mutable member as you suggested so I'll rebase and use that

FWIW I'll merge #1625 as soon as CI completes.

smowton · 2017-11-30T10:41:02Z

src/goto-symex/symex_goto.cpp

Space before && and ||

smowton · 2017-11-30T10:41:44Z

src/goto-symex/symex_goto.cpp

As above, suggest using an enum type

smowton · 2017-11-30T10:42:40Z

src/goto-symex/symex_goto.cpp

Another use of std streams

smowton · 2017-11-30T10:44:25Z

src/goto-symex/symex_main.cpp

As above, could you comment why namespaces are being re-initialised to point at different tables like this? What tables will ns refer to and at what stage in proceedings?

smowton · 2017-11-30T10:52:28Z

Also edited title to the usual "voice" for such things :)

karkhaz · 2017-11-30T15:12:18Z

@smowton thanks so much for the prompt review, I'll try and get this done within the next few days.

martin-cs · 2017-12-01T08:34:48Z

@karkhaz Multi-threading certainly is exciting but may I add a small note of caution. SAT solvers are very sensitive to memory latency and cache sizes. Given parts of the memory subsystem are shared between cores, running a SAT solver in one core can adversely affect the performance of a SAT solver running in another. Before you start work, I'd recommend trying the following experiment.

*. Pick a benchmark that takes at least 30 seconds and uses at least at least 50 MB of memory in the SAT solver.
*. Try running 1, 2, ..., $NUMBER_OF_CORES copies simultaneously and record the wall clock time taken to finish the complete run.
*. Plot total time and total time / N (work-rate) against N and see where they peak.

If total time is flat and work-rate peaks at N; brilliant, my warning no longer applies. If the peak is elsewhere and the lower it is, consider if it is worth the investment of time to multi-thread stuff.

( Also, a seeded pseudo-random queuing policy, run as a portfolio could also give a lower bound / estimate on the performance of the multi-threading.)

The other exciting topic, with @DanielNeville can provide input on is when to merge and when to queue. I'm told that "merge forwards branches and queue backwards ones" does interesting things...

karkhaz · 2017-12-01T15:54:41Z

@martin-cs thanks for this information! I'd certainly be interested in better merging heuristics. Something that I have working (not in this patchset) is the ability to put __CPROVER_begin_path_explore() and __CPROVER_end_path_explore() dummy function calls in the target codebase. The idea is to be able to do merging up until a point, and then do path exploration from that point onward, and switch merging back on. Or, the other way round. This very coarse-grained approach seems to work nicely for particular "shapes" of codebases. But obviously an automatic decision on when to merge would be extremely welcome.

Hopefully there's a lot of experimenting to be done here: what are the best heuristics for deciding when to merge, and what are the best heuristics for deciding on which path to explore next. I'm planning to gather some amount of empirical data about this, and would be very interested to read data gathered by others also.

martin-cs

[2/8] YES.
[3/8] Sure.
[4/8] Yes; we should have done this when JBMC was first forked.
[5/8] Yes, MUCH better with explanations.
[6/8] Maybe? It seems like this is adding names for two particular search heuristics, "depth-first-take-goto" and "depth-first-ignore-goto". To be honest I'd rather see a more general option / infrastructure that can easily be extended or otherwise I fear we will see a profusion of options like this that do similar-but-not-the-same things.
[7/8] Thanks for fixing.
[8/8] YES.

martin-cs · 2018-02-20T22:02:56Z

src/cbmc/bmc.h

This feels a bit clunky and not really in keeping with how the rest of the code base does extensions of functionality. Is there a simpler way of doing this? Also the apparent use-case for this (loop unwinding for the Java front-end) may be going away / getting transformed, maybe @mgudemann or @smowton might be able to say more.

I think this should be cleaned up in the course of #1869

martin-cs · 2018-02-20T22:12:50Z

src/cbmc/bmc.cpp

+1 what he said.

martin-cs · 2018-02-20T22:18:00Z

src/goto-symex/goto_symex.h

Should this be guard coded? I realise it was before...

I don't understand the question, sorry: do you mean hard-coded? If so, what would be the alternative, is there some kind of symbolic constant for this?

martin-cs · 2018-02-20T22:20:27Z

src/goto-symex/symex_target_equation.h

Why are you removing the output method?

Because I removed the ns member, which is needed for that function. This was all part of my effort to clarify what classes own what objects, but I'm afraid I don't recall exactly why ns was a member of this class (perhaps @tautschnig could elaborate? I think we discussed this and I forgot...)

When I wanted to create the branch_pointt class (consisting of an equation and a state), I tried to remove all members that would point to objects that might become stale, since we need to resume the equation and state later and stale/out-of-scope references led to segfaults. I think the ns member was one of the victims of this purge, and so was the dirtyt member (that's why I changed it from a pointer to a member)...

I think we weren't able to figure out why ns should possibly be a member here. Indeed @martin-cs is right that output needs review. We should have a method that is explicitly passed a namespacet as an argument. That implies that the operator<< declarations should go away as well (their definitions have been removed!). I'd suggest to re-instantiate the output method exactly as it was defined before, except that it should take an additional namespacet parameter.

OK, will push that in a few minutes

martin-cs · 2018-02-20T22:42:50Z

I realise this has been going on for some while and fear we are trying @karkhaz 's considerable patience ... BUT ... can I say "accept everything apart from 6/8"?

My objection to 6/8 isn't ideological, if it gets accepted, it gets accepted. I just think it will get changed pretty soon and we could easily get it right now and save hassle later. Symbolic execution heuristics (just "which path next, not even 'should I merge' or 'when should I feasibility check') are (somehow still?) an active research topic (@DanielNeville @cesaro @theyoucheng and others may be able to comment). It's one of the obvious low-hanging fruit with this. Many of these will require non-orthogonal changes to the branch taken behaviour "ignore forwards branches, follow backwards branches", "follow backwards branches but only the first 2 times", "take everything that looks like an error path because no-one checks those", "pick at random because I want to pretend I'm fuzzier than I am" which feel kind of hard to square with the proposed 6/8 solution. So what I would /suggest/ (I'm not going to demand) is that you swap it out for a more general "heuristic" option that not only picks which way to go but also sorts the work queue. The two options would then be depth-first-follow-goto and depth-first-ignore-goto or something.

karkhaz · 2018-02-20T22:52:39Z

@martin-cs there's two separate "sites" where we chose what to do next. The first site is deciding which path to put onto the workqueue (this is what is controlled by the command line option in 6/8), and the second site is deciding what to take off the workqueue (which is what I believe you're talking about).

You're totally correct that the choice of what to take off the workqueue will change soon, and can be decided by advanced heuristics. I'm working on this now, and that code will go into bmct::do_language_agnostic_bmc() (since this is where we resume executing new paths, so this is where we should decide which path to resume). However, at the point where we're saving new paths, there are literally only ever going to be two choices, because goto instructions have a one target instruction and one next instruction. The --goto-priority flag is about choosing between the goto's target and the goto's next instruction to push onto the workqueue, and this will remain the case even when we come up with cool heuristics for deciding what to pop off the workqueue. Does this make sense?

I wonder whether you're advocating for heuristics to control both pushing onto the queue and popping off? I suppose I could try that as well, if that's what you mean...

martin-cs · 2018-02-20T23:01:00Z

@karkhaz From an implementation point of view, yes it makes complete sense. However I think it might be good to think about things a little more theoretically. Per-path symex generates a (likely infinite) tree. Any heuristic (including parallel exploration!) is then an ordering of nodes in the tree (i.e. an ordering with the tree as a sub-order). In implementation terms, it's like you add both new states to the work queue, and then pick the next state from the work queue. If you're working depth-first then it will be one of the two (well... assuming a step-based notion of depth) but maybe you want to be able to explore breadth first or some kind of beam search.

I'm not going to block things over this but it seems like any of the more advanced heuristics, even depth-first ones, will want to control both of the locations you describe, so having a flag that fixes the behaviour at one seems a bit limiting.

The operators &= and |= can now be used between two safety_checkert::resultt objects. They return the "best" or "worst" of two results, and additionally assign that result to the LHS. The assignment operators are useful when repeatedly performing a safety check and wanting to return a single error code that either describes the best or worst outcome of all the safety checks combined.

The CBMC and JBMC frontends included identical code for running BMC after the language-specific preprocessing. This commit moves that common code into a static method of bmct. Parse options and help text related to bounded model checking are defined in bmc.h.

tautschnig · 2018-02-20T23:11:56Z

@karkhaz Just state whether you'd like to review the code and make changes right away in light of @martin-cs' comments.

@martin-cs & @karkhaz: I'd like to merge this relatively soon to have a first implementation in place for everyone to use and then iterate to improve it.

karkhaz · 2018-02-20T23:15:20Z

@tautschnig sorry, I pushed right before I saw your comment. @martin-cs I've removed 6/8, and I'll add a more general flag once I have my heuristics ready and it's more clear what the implementation will look like. Does that work?

martin-cs · 2018-02-20T23:15:43Z

@tautschnig I think my question about what's happened to the output method is probably more of a blocker than the 6/8 question.

martin-cs · 2018-02-20T23:19:09Z

@karkhaz Thank you that is most considerate of you.

This commit introduces the --paths flag to CBMC, which makes CBMC model-check each individual path of the program rather than merging paths and model-checking the entire program. The overall strategy involves allowing the "state" of symbolic execution---i.e., a pair of goto_symex_statet and symex_target_equationt ---to be saved during an execution, and for an execution to be resumed from a saved pair. By saving the state at every branch point and disabling path merging, symbolic execution only runs along one path but populates a worklist of saved states that should be executed later. At the top level, CBMC or JBMC loops while the worklist of saved states is non-empty, creating a new bmct object to resume executing each saved path. This commit includes the following supporting changes: - goto_symex_statet now owns a symbol table, separate from the one supporting the goto_program, which is used for dynamically created objects during symbolic execution. goto_symex was previously using a symbol table that was passed to it by reference for this purpose, but that symbol table is needed when resuming symbolic execution from a saved point and so ought properly to be part of the symbolic execution state. - goto_symex_statet now has a pointer to a symex_target_equationt, which can be updated with an equation from a previously-saved symbolic execution run. While equations are also conceptually part of the state of symbolic execution, they are heavily used after symbolic execution has completed (and the symex state has been deallocated) and so the equation is not owned by the state. An explicit copy constructor has been added to goto_symex_statet that initializes the equation member, so that symbolic execution can proceed either with an empty equation or with an equation that was earlier saved. - goto_symex_statet no longer has a pointer to a dirtyt, as this was hindering it from being copied.

cpplint now complains if a derived-class declaration is formatted as class derived: base rather than complaining if it is formatted as class derived : base (with a space on both sides of the colon). The latter style is the one enforced by clang-format, meaning that the two linters were inconsistent.

karkhaz · 2018-02-20T23:56:18Z

Just pushed: removed the formatting fix, and reinstated the output method with a new namespacet argument. Not sure what to do about the hard-coded guard identifier, and I'm not sure how I would have implemented the bmc customization differently; it does appear to need some kind of callback as it currently stands. If the use-case is going away then we can simply omit that callback parameter from bmct::do_language_agnostic_bmc() when that happens, it shouldn't be a difficult change, but why not keep it for now---I think the avoidance of code duplication that do_language_agnostic_bmc gives us more than makes up for any custom callbacks that we need to pass into that function.

karkhaz · 2018-02-20T23:59:49Z

Also, going to sleep now, I have a flight tomorrow that I need to wake up for...should have time to make any additional changes tomorrow early morning if needed.

tautschnig · 2018-02-21T00:03:37Z

@karkhaz Thanks a lot for all those updates! I'm inclined to merge once CI passes, unless @martin-cs tells me otherwise?

martin-cs · 2018-02-21T08:05:12Z

I don't understand the question, sorry: do you mean hard-coded?

Yes; sorry.

If so, what would be the alternative, is there some kind of symbolic constant for this?

Not yet but have a look at util/cprover_prefix.h for the current direction of travel of this sort of thing. This one isn't urgent or blocking as it's not your change.

martin-cs

@tautschnig Nah; I think we're good here.

tautschnig · 2018-02-21T09:20:26Z

CI has passed successfully, just need @martin-cs to give the green light.

karkhaz · 2018-02-21T10:22:20Z

Thanks so much everyone for the detailed reviews and suggestions! Looking forward to continuing work on this.

peterschrammel · 2018-02-21T13:32:13Z

src/cbmc/bmc.h

    message_handlert &_message_handler,
-    prop_convt &_prop_conv)
+    prop_convt &_prop_conv,
+    goto_symext::branch_worklistt &_branch_worklist)


For more backwards compatibility, would it have been possible to provide a constructor that initialises branch_worklist to a default value here?

I'm not sure default values and references would be compatible?

smowton · 2018-02-27T17:17:22Z

@karkhaz just coming to rebase my own work on top of this; a couple of questions:

At the moment this looks like it will interact oddly with any of the reporting options (show-vcc, program-only, symex-coverage-report) by outputting a report each time bmc is run. Is that intentional, or should the iterative symex-then-bmc run until "done", then only run end-of-day reporting once?
How should this interact with the (default) all-properties mode or with --cover, both of which try to cover multiple goals? At present it is only merging a single safe / not-safe return value, which feels as if it's designed for use with --stop-on-fail, and with --cover it would presumably repeatedly print reports saying that (for a particular symex path) goals X, Y and Z were reached, then for another path goals A, B and C were... and so on. Should we declare --paths currently only for use with --stop-on-fail, or is there pending work to merge the goal map to produce a single coherent report later?

karkhaz · 2018-02-28T09:12:50Z

@smowton: not sure if I have a good answer for these questions, I'm not actually that familiar with many of CBMC's command line options.

I'm not sure why anybody would pass --paths together with reporting options like --program-only? If you want to do --program-only, you presumably want to symex the whole program at once without doing any checks, rather than doing one path at a time, right? Perhaps I'm not understanding the use-case here, but it seems to me that you would only want to pass --paths if you're actually interested in checking properties.
I'm not sure what the "goal map" is. I wasn't using --paths with --stop-on-fail, I was indeed reading the diagnostic output from the BMC result one at a time while the loop was spinning. Admittedly this is not at all elegant, and it would be great to have some sort of unified report at the end that collects the BMC results of all paths seen so far. So again I'm not totally sure if I understand the question, but I would not be opposed to making --paths imply --stop-on-fail for now until I come up with a cleaner way of presenting the results from all paths. I suppose that I'd trap SIGINT or whatever and print a report before exiting.

smowton · 2018-02-28T10:33:26Z

Re: #1, it would potentially be useful if you wanted to see the equation before each run, which is indeed what would currently happen, but in such a case we should somehow prepend each report with a header identifying a path.

Re #2, the three options 'cover', 'fault-localization' and the default all-properties mode all build a list of all the assertions they're trying to satisfy, then make repeated solver runs to try to satisfy different goals. I guess with --paths we should probably stop trying to target a particular goal once it has been found using a particular path? So the goal list would be maintained outside the twin iterations over goals and paths, and goals incrementally reported either hit or covered as we go, before finally reporting ones we couldn't reach? Or am I getting the wrong end of the stick, and it's actually interesting to check if I can violate goal A via both paths X and Y?

martin-cs · 2018-03-01T14:57:39Z

( Unsolicited opinions on what the options should do)

--paths --show-vcc prints each formula instead of running the solver
--paths --show-program prints each path condition instead of running the solver
--paths --all-properties tries to prove every property using the per-path approach
--paths --cover tries to cover each location using the per-path approach
--paths --fault-localization ask David Landsberg or @theyoucheng

karkhaz requested review from cesaro, chrisr-diffblue, kroening, martin-cs, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners November 29, 2017 18:25

karkhaz force-pushed the kk-big-6-6 branch 4 times, most recently from 3050f65 to 0924fa7 Compare November 29, 2017 21:32

smowton reviewed Nov 30, 2017

View reviewed changes

smowton changed the title ~~CBMC now supports path exploration in addition to full bounded model checking~~ Add support for path exploration to CBMC/JBMC, in addition to full bounded model checking Nov 30, 2017

tautschnig assigned karkhaz Nov 30, 2017

karkhaz force-pushed the kk-big-6-6 branch 7 times, most recently from b4b8520 to 892b7ae Compare December 3, 2017 21:41

karkhaz requested a review from forejtv as a code owner December 3, 2017 21:41

karkhaz force-pushed the kk-big-6-6 branch from 6b2107d to 87140d7 Compare February 19, 2018 21:07

martin-cs reviewed Feb 20, 2018

View reviewed changes

karkhaz added 3 commits February 20, 2018 23:06

[path explore 2/7] Ignore jbmc binary

c53d630

karkhaz force-pushed the kk-big-6-6 branch from 87140d7 to f3a4c32 Compare February 20, 2018 23:12

karkhaz added 3 commits February 20, 2018 23:50

[path explore 7/7] Path exploration documentation

d67fa60

karkhaz force-pushed the kk-big-6-6 branch from f3a4c32 to d67fa60 Compare February 20, 2018 23:51

martin-cs approved these changes Feb 21, 2018

View reviewed changes

peterschrammel reviewed Feb 21, 2018

View reviewed changes

karkhaz mentioned this pull request Mar 31, 2018

Make CBMC more fun #1989

Closed

Conversation

karkhaz commented Nov 29, 2017

Uh oh!

martin-cs commented Nov 29, 2017

Uh oh!

karkhaz commented Nov 29, 2017

Uh oh!

smowton left a comment • 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!

karkhaz Dec 1, 2017 • 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!

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!

smowton commented Nov 30, 2017

Uh oh!

karkhaz commented Nov 30, 2017

Uh oh!

martin-cs commented Dec 1, 2017

Uh oh!

karkhaz commented Dec 1, 2017

Uh oh!

martin-cs 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!

tautschnig Feb 20, 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!

martin-cs commented Feb 20, 2018

Uh oh!

karkhaz commented Feb 20, 2018

Uh oh!

smowton left a comment •

edited

Loading

karkhaz Dec 1, 2017 •

edited

Loading

tautschnig Feb 20, 2018 •

edited

Loading