Load memory snapshot into cbmc

[danpoe]

This is a basic first version of loading a concrete memory snapshot (represented as a JSON symbol table) to initialize goto symex with, and then start symex from a given program location.

This is done in goto symex (as opposed to generating a goto program harness) as this will allow to potentially make the stack part of the snapshot in the future, which would allow to return from functions that have been called during the concrete execution.

• 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).
• n/a 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.

[kroening]

Sure this can't be done by building a harness, in goto-instrument? The symbolic execution engine appears to be the wrong place for that.

[danpoe]

@kroening There was a discussion about this with @tautschnig on the respective Slack channel. If we just want to model check a single function (and its callees) in a specific context it would be possible via a harness. But if we want to be able to model check a program starting from a concrete snapshot theoretically until the end of the program this seems hard to do that way. For that we will also need to initialize the symex call stack from a concrete call stack snapshot in order to be able to return from functions that have been called during the concrete execution. I'm not sure if it's possible to build a harness that can do that.

[smowton]

For stack snapshotting, would it be best to create a GOTO program with specialisations of the functions on the stack? For example I would add a prefix that declares and sets local variable values, then jumps to the point where the snapshot was taken (subsequent execution will use the real GOTO program)

That way the snapshot isn't tied into symex, but rather is a general concept that can be subject to any GOTO program analysis / transformation.

[danpoe]

@smowton Yes, I think that would work. Basically we'd add a boolean variable func_init_done for every function on the stack in the snapshot. When a function is entered for the first time func_init_done will be false and we'd do the local init code, set the variable to true, and then jump to the call of the next function on the call stack.

@tautschnig Would you be ok too with doing the memory snapshot loading via instrumentation?

[tautschnig]

@danpoe My apologies for leaving this on my stack for this long. The suggestion from @smowton seemed very good, but you might have gone down a different route now?

[danpoe]

@tautschnig No problem, I think we have resolved this in a Slack conversation back then anyways. So the plan is to move this into the goto-harness tool that @hannes-steffenhagen-diffblue and @NlightNFotis have been working on and do it via instrumentation.

[tautschnig]

@danpoe Yes, going via goto-harness will be cool, I think a big chunk of the code in this PR can remain in place as you've put together very nice tests already. The extra bit of work will be to translate the JSON-loaded symbol table to a harness rather than into a state to symex from.

[danpoe]

Closed in favor of #4150.