llvm dev - Mar 2018 - [GSoC 2018] Integrate with Z3 SMT solver to reduce false positives.

Hi all,

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.
>From what I understand, the current analyzer 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. 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.

However, when I was looking through the github version of LLVM, it seems
like z3 is already incorporated:
https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp


I guess my question is, what would the project contribute on top of the z3
manager that is currently implemented for LLVM?

Thanks!
Brenda
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20180314/d594e46f/attachment.html>

Hi Brenda,

Great that you are interested in the project! 
I’m reposting this to cfe-dev as Clang development is discussed there (please
direct all future email to that list).

As to your question, I think I have answered it in the following email:
http://lists.llvm.org/pipermail/cfe-dev/2018-March/057067.html
<http://lists.llvm.org/pipermail/cfe-dev/2018-March/057067.html>
(yes, lack of easily searchable/browsable archives is a problem..)

Regards,
George
> On Mar 14, 2018, at 6:37 PM, Brenda So via llvm-dev <llvm-dev at
lists.llvm.org> wrote:
> 
> Hi all,
> 
> 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.
> 
> From what I understand, the current analyzer 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. 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.
> 
> However, when I was looking through the github version of LLVM, it seems
like z3 is already incorporated:
>
https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
<https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp>
> 
> I guess my question is, what would the project contribute on top of the z3
manager that is currently implemented for LLVM?
> 
> Thanks!
> Brenda
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20180314/35aa6815/attachment.html>