search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

Write a symbolically executed term to a file #1113

Open weaversa opened 3 years ago

weaversa commented 3 years ago

I have a parameterized property that I want to prove for a bunch of different concrete parameters. For example:

prop : [32] -> [32] -> Bit
prop a b = ...

And I want to prove prop for all a, but where b is a set of concrete values. So, prove \a -> prop a 10 and \a -> prop a 87 and ...

If I put the concrete values of b in a list and do the prove command in a loop, the term to be proved is symbolically executed every call to prove, and symbolic execution takes quite some time, whereas the call to the solver is quick. Is there some way to dump a symbolically executed term to SMTLIB2 and then add some extra constraints, so that symbolic execution is only done once? I have looked at doing this manually (dumping the SMTLIB2 and trying to change the symbolic bits for b to constants, but the SMTLIB2 produced by saw doesn't make the symbols for b readily available.

atomb commented 3 years ago

It may be that being able to store and re-load a term in either SAWCore or What4 external syntax could provide a solution to this. But #1112 shows that there are some bugs in the SAWCore external format that prevent that from working for this use case at the moment.