[cfe-dev] [GSOC 2018] Integrate with Z3 SMT solver

[Ashish Gahlot via cfe-dev]

Hello,

I am having some doubts regarding the z3 constraint manager:

1) what is the correct way of invoking the z3 constraint on a c++/c file.
Right now I am using *clang -cc1 -analyzer-constraints=z3 -analyze
-analyzer-checker=core,unix,debug.ExprInspection -verify
/root/clang-llvm/llvm/tools/clang/test/Analysis/region-store.c *which
reports



*WARNING: unknown parameter 'timeout'Legal parameters are:  auto_config
(bool) (default: true)  debug_ref_count (bool) (default: false)*


*                 ...<snip>...*
I also tried the syntax mentioned in the last comment here
<https://reviews.llvm.org/D28952#652894> but it gives the same error
mentioned above.

2) when I remove *timeout *option from *Z3Config(), *the output is null. Is
it the correct behavior?
3) how can I test the performance of the analyzer when I make changes in


*Z3ConstraintManager.cpp?*
Thank you very much,
Ashish Kumar Gahlot

On Sat, Mar 10, 2018 at 1:13 AM, George Karpenkov <ekarpenkov at apple.com>
wrote:

>
>
> On Mar 9, 2018, at 7:22 AM, Ashish Gahlot via cfe-dev <
> cfe-dev at lists.llvm.org> wrote:
>
> Hello,
>
> Thank you for the detailed explanation.
>
> On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <dan at su-root.co.uk> wrote:
>
>>
>> @Dominic: On a related note. If you remember, a while back we spoke
>> about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their
>> performance characteristics and radically different (Z3_mk_solver()
>> being much faster most of the time for us in KLEE [1]).
>> I've just noticed that you're using `Z3_solver_push()` and
>> `Z3_solver_pop()`. We don't use that in KLEE and that might be we why
>> you had performance regressions when you tried switching to
>> `Z3_mk_solver()`. When you use Z3_solver_push(),
>> Z3 switches to a slower incremental solver internally [2,3]. You might
>> find that if you remove the pushes and pops and use `Z3_mk_solver()`
>> that things work better.
>>
>
> I read the issue [2] and it explains that it when we use (push), z3 tries
> to
> use the second solver. I think it would be a good idea to remove
> Solver.push()
> from Z3ConstraintManager.
>
>>
>> [1] https://github.com/Z3Prover/z3/issues/1035
>> [2] https://github.com/Z3Prover/z3/issues/1459
>> [3] https://github.com/Z3Prover/z3/issues/1053
>>
>
> Sorry for a noob question but is it possible to test the changes that I
> make to
> Z3ConstraintManager.cpp without having to compile the whole clang every
> time?
>
>
> It does not recompile everything, whenever you type “ninja clang” (or
> “make clang”)
> from the build folder it only recompiles the changed file and does the
> relinking.
> Headers are a different story — then it has to recompile all the files
> that transitively include that header,
> unfortunately, nothing that can be done there.
>
>
> Thank you very much,
> Ashish Kumar Gahlot
>
> --
> Ashish Kumar Gahlot
> IV year, UG
> Govt. Engg. College, Ajmer, India
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>
>


-- 
Ashish Kumar Gahlot
IV year, UG
Govt. Engg. College, Ajmer, India
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180311/3d28e45c/attachment.html>