[klee-dev] Logging the Symbolic Values of Variables

[Nowack, Martin]

Hi Luke,

As KLEE builds on LLVM, the value is either part of an SSA register or a heap/global allocation.

In the first case, the register’s value can be accessed via `eval()`, i.e.
for a Load instruction (https://github.com/klee/klee/blob/3ca81c2dc3881aec0bbf94646c73a148d706c76d/lib/Core/Executor.cpp#L2788)
the result will be stored in the SSA register from the load as part of the `executeMemoryOperation` using the `bindLocal` operation.
You just need to retrieve the result afterwards, i.e. `getDestCell(state, ki).value`.

For the second case, the memory object needs to be resolved first, before retrieving the assocated ObjectState and accessing the values of interest.
Have a look at `executeMemoryOperation` for an example how to load/store memory.

Please keep in mind, depending on the actual optimisation used by the compiler, LLVM version and so on, those are not necessarily representing variables
from the source code.

Best,
Martin




> On 2. Feb 2024, at 17:02, Luke Dramko <lukedram at andrew.cmu.edu> wrote:
> 
> Hello,
> 
> My research group is looking to output the value of each variable's symbolic representation after the execution of each line in the source program. Alternatively, the symbolic values of only the variables whose values are modified on that line would be sufficient as well.
> 
> For example, given the following function is being executed symbolically:
> 
> 1. int fn(int x) {
> 2.     if (x > 1) {
> 3.         x++;
> 4.         x = x * x;
> 5.     }
> 6.     return x;
> 7. }
> 
> We would like to know that
> - after line 2 (on the true branch) that x is constrained by x > 1.
> - after line 3, that x is constrained by x > 2.
> - after line 4, that x is constrained by x = y * 2 where y > 2.
> etc.
> 
> (The above ignores overflow semantics but constraints that capture them would be welcome.)
> 
> Is there a way to do this with Klee? If not, what part of the codebase should we modify to add this capability?
> 
> Thank you for your help!
> 
> Best regards,
> Luke
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev