Open sebastian-kunze opened 7 years ago
@sekunze The problem you are observing here is that unfortunately the solver backend doesn't know how to handle multi arity maps.
i.e.
type IntHeap = [Ref, Int] int;
The solver backend does know how to handle nested single arity maps.
type IntHeap = [Ref][Int] int;
however.
This is an unfortunate limitation which I never hit before because the benchmarks I used only single arity maps (sometimes nested). Fixing this would be a matter teaching the SMTLIBQueryPrinter
to encode multi arity maps like it encodes nested maps. Unfortunately Symbooglix's solver backend is a bit of a mess so this might not be very easy.
As for your question on traces Symbooglix doesn't current record execution traces. This could and should be implemented though as this is a very basic and useful feature. At what granularity do you need a trace? When sketched out the idea I imagined the trace should be a trie of basic block labels so try and keep memory usage as low as possible. Alternatively the trace could be a sequence of branch decisions.
I am mostly interested in how methods interact with each other, i.e., what call sequences uncover a certain behaviour. Therefore, a tree structure would be most qualified.
I want to run Symbooglix to generate traces that show the interaction between two given methods. In the following example, procedure
a
simply checks the given conditionc
and returns an outputo
. The variablev
within the abstracted heap is set to2
if conditionc
holds; otherwise the abstracted heap remains unchanged. When executing procedureb
, the variablev
is checked for its value, which results in different calls to procedurea
:When I run the example using Symbooglix with procedure
b
as an entry point, I receive the following exception though:Does Symbooglix allow to identify the trace that procedure
a
has to be called before procedureb
in order to satisfy the conditional statement within procedureb
and am I doing it right?