[klee-dev] Which optimizations that KLEE used on the bitcode, and where they are?

[Sangharatna Godboley]

Hi Sang,

Originally KLEE explores all possible paths and create an execution tree.
But yeah there are some options which optimize the execution tree.
During our experiment for a project related to MC/DC, we have noticed such
optimization and we had not used that default optimization option.
Please check if it works for your case or not.
1. Navigate to:    lib/Module/KModule.cpp
 2.  Comment the line:  "pm3.add(createCFGSimplificationPass());"
[Line number 368 in my code]

These steps will avoid simplifying the CFG. It is very useful when you have
complex Boolean expressions with AND (&&) and OR (||) logical operators.

Also, there may be some more simplifications and optimizations by default
in KLEE which must have some useful objectives but you may choose to use
them or to ignore.

Thanks,
Sanghu

On Fri, Oct 26, 2018 at 7:05 AM Sang Phan <phanquocsang at gmail.com> wrote:

> Hello,
>
> The assembly.ll that KLEE generates is much more optimized than the one
> generated by opt.
>
> So what optimization that KLEE uses before the execution, and where in the
> source that I can them?
>
> Thank you,
> Sang
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>


-- 
Thanks & Regards,

Dr. Sangharatna Godboley, Ph.D.
Postdoctoral Research Fellow, NUS Singapore.
-------------- next part --------------
HTML attachment scrubbed and removed