[klee-dev] How to avoid calling the solver if the branch is known at run-time

[Andrew Santosa]

 Hi Charitha,

I think you would need to do the modification in Executor::fork().
You would notice within that function there is the following three lines:

solver->setTimeout(timeout);
bool success = solver->evaluate(current, condition, res);
solver->setTimeout(0);

I would try to replace those with:

res=Solver::Unknown;
success=true;

So that every time KLEE would think that the solver has been invoked
successfully and it is not known that the current condition is valid or
unsatisfiable, which means it is only known to be satisfiable, tricking
KLEE into always forking a new state.

I hope that works.

Best,
Andrew

    On Saturday, 5 May 2018, 1:19:26 am GMT+8, Charitha Saumya <cgusthin at purdue.edu> wrote:  
 
 Hi,

I want to implement a search strategy in KLEE.

If I know some branch is feasible from prior knowledge (say I learn that 
for a some br instruction the true branch is always feasible),

How can I change KLEE to avoid calling the solver in Executor.cpp (in 
Instruction::Br)

and just guide the execution to next basic block?

Please help!

Thanks,

Charitha Saumya


_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  
-------------- next part --------------
HTML attachment scrubbed and removed