Different concrete values generated for the same constraints on different runs

[Alan Wang]

Hi, 

I'm trying to make path exploration in S2E demterministic.

After switching to a DFS-style path selection algorithm, I found that the initial concrete values generated for the same path could be different on different S2E runs. 

This would cause path exploration to change its order at a later point (because the different initial values may lead to different paths at a later forking point).

I think this non-determinism might be an issue in Z3, because the constraints passed to Z3 look the same. But it also seems complicated because in most cases, Z3 will return the same concrete values for the same constraints. 

So I'm quite confused. And I found  a link on StackOverflow:

"Randomness in Z3 Results"

https://stackoverflow.com/questions/15731179/randomness-in-z3-results

It says the reason could be due to different internal IDs generated by Z3.

But since all the queries passed to Z3 are the same on different runs, so I don't know why it would cause any difference. 

I would greatly appreciate it if you could share any ideas on this.

Thanks,

Zhongjie

[Vitaly Chipounov]

Hi,

Unfortunately, I don't know how Z3 internals work and how this could be fixed.
Perhaps something you could try is to record the SMT queries, then feed them into Z3 directly. It should be easier to debug this way.
Maybe you could somehow reset the internal state of Z3 to a known initial state before running each query. I hope it doesn't use any non-deterministic constructs inside.

Vitaly

--
--
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev

---
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/d5c3e76d-c4c0-41a8-b589-a8ae085401dfn%40googlegroups.com.

[Alan Wang]

Hi Vitaly, 

Thanks for the super fast reply! 

I have tried to feed a single query (the one that has different results in S2E) directly to Z3 and there was no non-determinism observed. 

Maybe there was some difference in the intermediate states in Z3. I will probably try to replay all the queries to Z3. 

And I will also try to reset the internal state of Z3. 

Thanks, 

Zhongjie

[Vitaly Chipounov]

Hi,

There is a --per-state-solver flag that allows to have a separate solver instance in each state. See SolverManager.cpp.
Maybe setting it to true will help.

Vitaly

To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/7a22551c-05e9-42d1-92cd-dfa70a7637a5n%40googlegroups.com.

[Alan Wang]

Hi Vitaly, 

Thanks. I think I have figured out the reason. 

The different concrete values were indeed due to different internal IDs in Z3. 

When an AST node in Z3 was deleted, its internal ID was recycled and later used by another AST node. 

And, in KLEE, when a query is finished, it resets its Z3BuilderCache, which will delete Z3 nodes in the cache.

Specifically, an unordered_map "cons_arrays_" in the cache was cleared. Since it's unordered, the Z3 nodes in it are deleted in a non-deterministic order. 

Therefore the recycled internal IDs are also in non-deterministic order, which will cause the ID assignment for later nodes to be non-deterministic. 

And different internal IDs lead to different concrete values generated as described in "Randomness in Z3 Results" (https://stackoverflow.com/questions/15731179/randomness-in-z3-results)

A simple solution will be disabling internal ID recycling by comment out "#define RECYCLE_FREE_AST_INDICES" in ast/ast.h in Z3, so it will use increamental internal IDs for new nodes. 

Best,

Zhongjie