[klee-dev] identify multiple executions of the same branch instruction

[Qiao Kang]

Hi Jianxiong and Cardar:

Yes, I solved this! Thanks for the help.

Qiao

On Mon, Aug 12, 2019 at 5:27 AM Cadar, Cristian <c.cadar at imperial.ac.uk>
wrote:

> Hi Qiao,
>
> I hope you've solved this by now.  It should be quite easy to get the
> file & line number for the instruction you're interested in (if you
> compiled with debug info), just look at KInstruction::getSourceLocation().
>
> Best,
> Cristian
>
> On 27/07/2019 18:40, Qiao Kang wrote:
> > Hi,
> >
> > I'm hacking KLEE to run a program that has an N-iteration loop and an
> > if-else branch inside the loop. The if-else branch will be hit for
> > multiple times. I'm trying to capture each branch instruction and
> > identify if it is executing this particular if-else branch, i.e., this
> > particular line of code.
> >
> > For instance:
> >
> > // N is constant
> > loop N times:
> >     if (cond):
> >           // do something, might change cond
> >     else
> >          // do something else, might change cond
> >
> > Along the execution, this if-else branch will be hit multiple times. How
> > do I capture all executions of this branch and identify them that they
> > are all from this if-else branch, but not other code? A simple use case
> > would be to count how many times this if-else branch was hit along the
> > execution.
> >
> > I now can hijack all branch instructions
> > in Executor::executeInstruction, it has a switch case called
> > "Instruction::Br". I can also extract the corresponding path constraint
> > (i.e., cond). However, I don't know how to identify which if-else branch
> > they are executing. Note that this cond is subject to change, so I
> > cannot simply use this cond as the key to classfity them. One the other
> > hand, the line of code would be an appropriate key. Can we extract code
> > line information?
> >
> > Any advice will be greatly appreciated!
> >
> > Thanks,
> > Qiao
> >
> >
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at imperial.ac.uk
> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> >
> _______________________________________________
> 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