<div dir="ltr"><div><div><div>Hi George,<br></div><div><br>Thanks for the references,
after watching them and a few more videos, I sort of have a high level
idea on how z3 will be useful for the static analyzer:<br></div></div><br>1. For all the feasible paths reported by the bug reporter, initiate z3 solver. <br></div><div>2. Use the ProgramState to add constraints to the z3 solver as we step through the path<br></div><div>3.
If at any point the z3 solver returns false (i.e. the constraints
cannot be satisfied), the path is infeasible and hence should be flagged
as a false positive. <br><br></div><div>The above procedure is assuming
that the bug reporter returns feasible paths, but I am actually still
confused about what the bug reporter reports. Does it report bugs?
infeasible paths or feasible paths of the program? I am also wondering
how the bug reporter and constraint manager interact with each other.<br></div><br><div>Moreover,
on the project description, it says that z3 is useful in "complicated
branches that the constraint manager cannot reason about". From the bug
reports, or other objects in the static analyzer, how would I know
whether the constraint manager can/cannot reason about? <br><br></div><div>Thanks for all your help and I look forward to hear from you,<br></div><div>Brenda</div><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Mar 16, 2018 at 8:52 PM, Brenda So <span dir="ltr"><<a href="mailto:so@cooper.edu" target="_blank">so@cooper.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Hi George,<br></div><div><br>Thanks for the references, after watching them and a few more videos, I sort of have a high level idea on how z3 will be useful for the static analyzer:<br></div></div><br>1. For all the feasible paths reported by the bug reporter, initiate z3 solver. <br></div><div>2. Use the ProgramState to add constraints to the z3 solver as we step through the path<br></div><div>3. If at any point the z3 solver returns false (i.e. the constraints cannot be satisfied), the path is infeasible and hence should be flagged as a false positive. <br><br></div><div>The above procedure is assuming that the bug reporter returns feasible paths, but I am actually still confused about what the bug reporter reports. Does it report bugs? infeasible paths or feasible paths of the program? I am also wondering how the bug reporter and constraint manager interact with each other.<br></div><br><div>Moreover, on the project description, it says that z3 is useful in "complicated branches that the constraint manager cannot reason about". From the bug reports, or other objects in the static analyzer, how would I know whether the constraint manager can/cannot reason about? <br><br></div><div>Thanks for all your help and I look forward to hear from you,<br></div><div>Brenda<br></div><div><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 14, 2018 at 10:16 PM, 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">Hi Brenda,<div><br></div><div>Great that you are interested in the project! </div><div>I’m reposting this to cfe-dev as Clang development is discussed there (please direct all future email to that list).</div><div><br></div><div>As to your question, I think I have answered it in the following email: <a href="http://lists.llvm.org/pipermail/cfe-dev/2018-March/057067.html" target="_blank">http://lists.llvm.org/p<wbr>ipermail/cfe-dev/2018-March/05<wbr>7067.html</a></div><div>(yes, lack of easily searchable/browsable archives is a problem..)</div><div><br></div><div>Regards,</div><div>George</div><div><div><br><blockquote type="cite"><div><div class="m_7938125634778224125h5"><div>On Mar 14, 2018, at 6:37 PM, Brenda So via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a>> wrote:</div><br class="m_7938125634778224125m_-1182452024940543549Apple-interchange-newline"></div></div><div><div><div class="m_7938125634778224125h5"><div dir="ltr"><div>Hi all,</div><div><br></div><div>I am a fourth year EE bachelors student who is very interested in compilers. I have taken the only compilers course offered in my school and did an independent study with my CS professor. Although I'll begin to work in a couple of months, I definitely want to pursue my interest in compiler design and optimization as a PhD in the future. I am very interested in the z3 SMT solver project detailed on the LLVM website and have been doing some research about it. </div><div><br></div>From what I understand, the current analyzer <font face="arial, helvetica, sans-serif"><span style="line-height:107%">traces the program, and at each branch, it branches out into the true
branch and the false branch. The true and false branch causes certain
constraints on the values. If the conditions on the branch causes a constraint
to be unsatisfiable, the path is considered to be infeasible. </span>
<span style="line-height:107%">traces the program, and at each branch, it branches out into the true
branch and the false branch. The true and false branch causes certain
constraints on the values. If the conditions on the branch causes a constraint
to be unsatisfiable, the path is considered to be infeasible. In that case, z3 would be useful in proving whether a branch is definitely true or false (i.e. whether the constraints are satisfiable), thus preventing exponential blowup of the analysis. </span></font><div><br></div><div>However, when I was looking through the github version of LLVM, it seems like z3 is already incorporated: </div><div><a href="https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp" target="_blank">https://github.com/llvm-mirror<wbr>/clang/blob/master/lib/StaticA<wbr>nalyzer/Core/Z3ConstraintManag<wbr>er.cpp</a> <br></div><div><br></div><div>I guess my question is, what would the project contribute on top of the z3 manager that is currently implemented for LLVM?</div><div><br></div><div>Thanks!</div><div>Brenda</div></div></div></div>
______________________________<wbr>_________________<br>LLVM Developers mailing list<br><a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a><br><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/llvm-dev</a><br></div></blockquote></div><br></div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>