<div dir="ltr"><div><div><div><div><div><div>Hello,<br><br></div>I am having some doubts regarding the z3 constraint manager:<br><br></div>1) what is the correct way of invoking the z3 constraint on a c++/c file. Right now I am using <b>clang -cc1 -analyzer-constraints=z3 -analyze -analyzer-checker=core,unix,debug.ExprInspection -verify /root/clang-llvm/llvm/tools/clang/test/Analysis/region-store.c </b>which reports <b>WARNING: unknown parameter 'timeout'<br>Legal parameters are:<br>  auto_config (bool) (default: true)<br>  debug_ref_count (bool) (default: false)<br></b></div><b>                 ...<snip>...<br><br></b></div><div>I also tried the syntax mentioned in the last comment <a href="https://reviews.llvm.org/D28952#652894">here</a> but it gives the same error mentioned above. <br></div><div><b><br></b></div>2) when I remove <i>timeout </i>option from <i>Z3Config(), </i>the output is null. Is it the correct behavior?<br></div>3) how can I test the performance of the analyzer when I make changes in <i>Z3ConstraintManager.cpp?<br><br><br></i></div>Thank you very much,<br>Ashish Kumar Gahlot <br><div><div><div><div><b></b></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 10, 2018 at 1:13 AM, George Karpenkov <span dir="ltr"><<a href="mailto:ekarpenkov@apple.com" target="_blank">ekarpenkov@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space"><br><div><span class=""><br><blockquote type="cite"><div>On Mar 9, 2018, at 7:22 AM, Ashish Gahlot via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>> wrote:</div><br class="m_7674361682098815510Apple-interchange-newline"><div><div dir="ltr"><div>Hello,<br><br></div>Thank you for the detailed explanation.<br><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 9, 2018 at 3:16 AM, Dan Liew <span dir="ltr"><<a href="mailto:dan@su-root.co.uk" target="_blank">dan@su-root.co.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
@Dominic: On a related note. If you remember, a while back we spoke<br>
about `Z3_mk_simple_solver()` vs `Z3_mk_solver()` and how their<br>
performance characteristics and radically different (Z3_mk_solver()<br>
being much faster most of the time for us in KLEE [1]).<br>
I've just noticed that you're using `Z3_solver_push()` and<br>
`Z3_solver_pop()`. We don't use that in KLEE and that might be we why<br>
you had performance regressions when you tried switching to<br>
`Z3_mk_solver()`. When you use Z3_solver_push(),<br>
Z3 switches to a slower incremental solver internally [2,3]. You might<br>
find that if you remove the pushes and pops and use `Z3_mk_solver()`<br>
that things work better.<br></blockquote><div> </div><div>I read the issue [2] and it explains that it when we use (push), z3 tries to<br></div><div>use the second solver. I think it would be a good idea to remove Solver.push()<br></div><div>from Z3ConstraintManager.<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
[1] <a href="https://github.com/Z3Prover/z3/issues/1035" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3<wbr>/issues/1035</a><br>
[2] <a href="https://github.com/Z3Prover/z3/issues/1459" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3<wbr>/issues/1459</a><br>
[3] <a href="https://github.com/Z3Prover/z3/issues/1053" rel="noreferrer" target="_blank">https://github.com/Z3Prover/z3<wbr>/issues/1053</a><br>
</blockquote></div><br></div><div class="gmail_extra">Sorry for a noob question but is it possible to test the changes that I make to <br></div><div class="gmail_extra">Z3ConstraintManager.cpp without having to compile the whole clang every time?<br></div></div></div></div></div></blockquote><div><br></div></span><div>It does not recompile everything, whenever you type “ninja clang” (or “make clang”)</div><div>from the build folder it only recompiles the changed file and does the relinking.</div><div>Headers are a different story — then it has to recompile all the files that transitively include that header,</div><div>unfortunately, nothing that can be done there.</div><br><blockquote type="cite"><div><span class=""><div dir="ltr"><div><div><div class="gmail_extra"><br>Thank you very much,<br>Ashish Kumar Gahlot</div><div class="gmail_extra"><br>-- <br><div class="m_7674361682098815510gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>Ashish Kumar Gahlot</div><div>IV year, UG</div><div>Govt. Engg. College, Ajmer, India</div></div></div></div></div>
</div></div></div></div></span><span class="">
______________________________<wbr>_________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/cfe-dev</a><br></span></div></blockquote></div><br></div></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>Ashish Kumar Gahlot</div><div>IV year, UG</div><div>Govt. Engg. College, Ajmer, India</div></div></div></div></div>
</div>