Path exploration goodies

[karkhaz]

Most of this daunting pull request is tests, I promise. 😇

• Implement @martin-cs's suggestion that control of which path to continue executing be moved out of goto_symex/symex_goto.cpp entirely. My previous implementation always saved one path on the queue and continued executing the other, meaning that every symex run ended at the end of a path. We now save both paths and halt symbolic execution, returning control to the caller, who can choose which path to execute (either of the two paths that were just saved, or even any of the paths that were saved earlier). This implies that a symex run shouldn't always be followed by a safety check, since we may not have finished executing a path; thus, I added safety_checkert::resultt::SUSPENDED to indicate that symex was suspended half-way through and the resulting equation has not been safety-checked.

• The path workqueue now has a custom data type instead of being a std::list, with push(), peek(), and pop() methods. The data type is subclassable for implementing different strategies. peek() is intentionally not marked const, so that the data type can lazily search for the next path to return only when peek() is called rather than modifying its state every time push() is called; I anticipate that future strategies might be time-consuming.

• There's a data structure called path_strategy_choosert which is both a factory for path exploration strategies, and also holds their stringified names and help texts all in the same place, so that there's a uniform way of setting the path exploration strategy from all the frontends without duplication.

• Two strategies are implemented: FIFO and progressive FIFO. The paths that FIFO returns will always alternate between the next instruction of a goto, and the target of that same goto, followed by the next and target of another goto, etc. Progressive FIFO will always return the jump targets of all gotos that have been pushed, and only start returning next instructions when the jump targets have all been executed---the idea being to prefer making forward progress rather than dwelling inside loops.

• Tests for all of this, courtesy of the Department of Overengineered Solutions. In order to test the functional correctness of strategies, we not only need to test the verification result, but also the order in which paths are popped. This means multi-line regexes in the test suite, but even for short test cases these regexes are hundreds of bytes long---tedious to write and impossible to understand. I therefore wrote an interpreter for a human-friendly language representing the pushes and pops of a path queue. Test writers should write what paths they expect to see in what order in the comments section of a test.in file, from which a test.desc file gets generated by scripts/make_descs.py. For example, writing this test.in file:

CORE
main.c
--unwind 2
activate-multi-line-match
SIGNAL=0
EXIT=10
--
^warning: ignoring
--
This strategy differs from 'fifo' because the failed path is the second
one, not the last one.

Test that the following happens in order:
execute line 6
save next 7
save jump 9

// We skip the loop first with this strategy. This path is infeasible,
// since x is 1 so we must have entered the loop; so the solver is happy.
any lines
execute line 6
resume jump 9
execute line 9
any lines
path is successful

// We now enter the loop and execute it; we then save "entering the loop
// twice" and "bailing out after the first spin".
any lines
execute line 6
resume next 7
execute line 7
any lines
save next 7
save jump 9

// Since the just saved "bailing out after the first spin" is a jump,
// execute that path. That path makes the assertion fail, since we
// decremented x from 1 to 0.
any lines
execute line 6
resume jump 9
execute line 9
any lines
path is unsuccessful

// Finally, execute "entering the loop twice". This path is infeasible
// because we cannot actually have entered the loop twice if x was only
// 1 to begin with, so the solver is happy.
any lines
execute line 6
resume next 7
execute line 7
any lines
path is successful
end

generates this test.desc:

CORE
main.c
--unwind 2
activate-multi-line-match
SIGNAL=0
EXIT=10
BMC at file[^\n]+line 6 function \w+\nSaving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION SUCCESSFUL(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+Saving next instruction 'file[^\n]+line 7 function \w+'\nSaving jump target 'file[^\n]+line 9 function \w+'(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from jump target 'file[^\n]+line 9 function \w+'\nBMC at file[^\n]+line 9 function \w+(.|\n)+VERIFICATION FAILED(.|\n)+BMC at file[^\n]+line 6 function \w+\nResuming from next instruction 'file[^\n]+line 7 function \w+'\nBMC at file[^\n]+line 7 function \w+(.|\n)+VERIFICATION SUCCESSFUL\n[^.]
--
^warning: ignoring
--
This strategy differs from 'fifo' because the failed path is the second
one, not the last one.

WARNING: This test.desc file is automatically generated
from the test.in file in this directory. Do not modify
this file.

[karkhaz]

Also, you might suppose that the code formatting is a bit bizarre in the constructor for path_strategy_choosert (it contains a literal map from strings to literal pairs of strings and lambda thunks). That's what clang-format told me to do, but I'm happy to change it if anybody else wants it a particular way.

[thk123]

TG pointer bump (due to change in bmc.cpp) diffblue/test-gen#1567

[karkhaz]

@thk123 Not sure what that issue is, as it's private: should I know what this is about, or is it just for diffblue folks?

[romainbrenguier]

I think tmp_result shouldn't be declared here

[romainbrenguier]

tmp_result should be const declared here

[romainbrenguier]

this could be a PRECONDITION

[thk123]

@karkhaz Hi sorry should have explained - it is a PR on a private repo to verify this change doesn't require changes on our end to incorporate it. Nothing to worry about, I'll post here when it has passed but I'd appreciate if we could hold off merging until that check is complete 🙂

[thk123]

Sorry - there are compile errors on our end, blocking until we've had a chance to get this working.

[thk123]

Could I ask for a rebase as I think I'm getting some unrelated compile errors that I think a rebase would fix. (I think I've fixed the real compile errors but would like to check).

[karkhaz]

@thk123 I have rebased and also applied @romainbrenguier's suggestion.

[thk123]

@karkhaz thanks, got it compiling locally, will let you know once our CI is passing.

[smowton]

Might as well document the existing ones while you're there!

[tautschnig]

(done)

[thk123]

Hi it is failing our CI so until we've investigated can I ask we continue holding off on merging this.

[karkhaz]

@thk123 please let me know if there's anything I can help with. I'm quite surprised, as I believe that I've only changed aspects of symex that run when --paths is passed...

@tautschnig suggested an improvement to the test structure today, so please don't merge this until I've pushed that up (I'll do that tomorrow morning).

@martin-cs would you mind seeing if you're happy with this approach? This patchset implements your suggestion that symex should save both potential paths rather than saving one and continuing with the other.

[thk123]

@karkhaz yup looks like entirely our problem, but could I ask for another rebase, sorry.

[karkhaz]

@thk123 rebased, cheers.

[thk123]

@karkhaz thanks - updated the bump 👍

[karkhaz]

Ping @smowton, @thk123---does this look good to everyone? I'm experimenting with new strategies locally, but I don't want to get too out-of-sync if there are many more changes required from this PR...

[thk123]

Updating the pointer bump now - note I've not really reviewed the PR

[smowton]

Re-reviewed the tests -- this looks excellent, thanks very much for the extra work! Only one nitpick, a Makefile has some funky tab/space combo at the moment. No need for re-review from me.

[smowton]

Alignment looks odd --mix of spaces and tabs?

[thk123]

Sorry to create extra work - but could I ask for a rebase as this has fallen behind develop.

[karkhaz]

@smowton fixed the nit, thanks!

@thk123 rebased to ToT.

All tests are passing.

[thk123]

Apologies - we had a number of breaking changes this week that got merged after your last rebase. Can I ask for another rebase (I'm optimistic it will be the last!)

[karkhaz]

@thk123 rebased, cheers.

[thk123]

🎉 TG pointer bump passes @karkhaz I assume you'd like this merged post-haste? still waiting for approval from I honestly don't know who - something that even @tautschnig or @smowton don't have permission to wave through?

[tautschnig]

@chrisr-diffblue @martin-cs @peterschrammel A review would be greatly appreciated!

[chrisr-diffblue]

Looks good to me - many thanks for all the efforts to get this through PR.

[chrisr-diffblue]

Minor nit: This should probably have been a separate PR... but I won't block the PR :-)

[karkhaz]

@chrisr-diffblue I'll put minor commits in a separate PR from now on, IIRC I kept that commit in because the PR was failing the doxygen check that that commit fixes.

Thanks so much for all the reviews!