Allow saving VM snapshots with symbolic data

[vitalych]

It should be possible to dump any state to a file in order to resume it later or ship it to a different machine.

One option is to extend QEMU's snapshot mechanism to save symbolic data and constraints contained in the state. Snapshots can already handle concrete system state for cpu, disk, and devices. We could add a special virtual device that would handle serialized symbolic data. This issue could be split in two parts:

• Implement concrete snapshot. Calling savevm path1 should make QEMU save a concrete snapshot as it would normally do. This snapshot should then be resumable in vanilla QEMU.
• Add symbolic data on top. The concrete part would still be saved as usual, except that now, there would be a fake symbolic device in QEMU that would ask libs2e to serialize any symbolic data that there is in the system and add that data to the snapshot.

We need a way to efficiently store symbolic expressions (no duplication).

[Lambda2023]

S²E supports state-of-the-art program analysis techniques Efficient navigation through large state spaces with concolic and symbolic execution, state merging, static analysis, function summaries, incremental constraint solving. This great idea is kind of like the function summary technique. So, how to dis/enable or ues the function summary for a user-specified function in s2e?

[vitalych]

This question is not related to the issue. Please ask on the s2e-dev mailing list.