search

tracer-x / TracerX

TracerX Symbolic Virtual Machine
https://tracer-x.github.io/
Other
31 stars 11 forks source link

WIP: Speculation #323

Closed rasoolmaghareh closed 5 years ago

rasoolmaghareh commented 6 years ago

The two latest commits are adding a check before creating an speculation node.

In general, the speculation node should be created when an infeasible path is detected. However, the fork function is called in several occasions such as when a memory operation is performed.

In such cases, if the executing the memory operation needs an internal node to be created an internal node is created by the fork function.

In order to avoid mistaking not-created internal nodes with infeasible-path nodes, we check if the prevPC is pointing to a BR instruction.

Moreover, in order to stop creating a speculation node at the target we check the BR instruction is not jumping to cond.false (target of klee_assert).

rasoolmaghareh commented 6 years ago

At the current moment the next steps that you should be implemented are:

1- Implementing back-jump in case speculation fails. 2- In case an error node is reached while doing speculation, it should not be reported and speculation should fail.