Re: [klee-dev] Use of --optimize flag

2016-06-23 Thread Sean Bartell 

RAJDEEP MUKHERJEE on 2016-06-23:

In default mode, klee uses dfs search strategy with incremental solving.
What additional optimisations does Klee perform with the --optimize switch ?


The --optimize switch causes KLEE to run standard compiler optimizations on the 
subject program before starting to execute it. It's similar to compiling the 
subject program with an option like -O2. One difference is that if you tell 
KLEE to link the subject with uclibc or the POSIX runtime, KLEE will do 
optimization *after* linking, which gives extra opportunities for inlining.
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Use of --optimize flag

2016-06-23 Thread Daniel Guo 
There is an Optimize.cpp in which various optimizing llvm passes are
created, e.g., CFGSimplification, ConstantPropagation, InstructionCombining
...
You can find all the passes there, and check how they are created and
applied.


On Thu, Jun 23, 2016 at 10:14 AM, RAJDEEP MUKHERJEE <
rajdeep.mukherje...@gmail.com> wrote:

>
> Hi,
>
> I recently ran some experiments with klee with the --optimize switch
> and without --optimize switch. It seems that the solving using --optimize
> switch is much faster than without it.
>
> In default mode, klee uses dfs search strategy with incremental solving.
> What additional optimisations does Klee perform with the --optimize switch
> ?
>
> Any help is appreciated.
>
> Best regards,
> Rajdeep
>
>
> ___
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev