<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:492373370;
mso-list-template-ids:-1589983936;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=HU link=blue vlink=purple style='word-wrap:break-word'><div class=WordSection1><p class=MsoNormal><span style='mso-fareast-language:EN-US'>Oh my bad. I thought it was about the SMT solver. Now I’m even more engaged if we plan to focus on practical usability and performance instead of doing this for academic research.<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-US'>Sorry for the confusion I might have caused.<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-US'><o:p> </o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-US'>Thanks, Valeriy!<br><br><o:p></o:p></span></p><div><div style='border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm'><p class=MsoNormal><b><span lang=EN-US>From:</span></b><span lang=EN-US> Valeriy Savchenko <vsavchenko@apple.com> <br><b>Sent:</b> 2021. április 9., péntek 11:40<br><b>To:</b> Balázs Benics <benicsbalazs@gmail.com><br><b>Cc:</b> Manas <manas18244@iiitd.ac.in>; cfe-dev@lists.llvm.org<br><b>Subject:</b> Re: [cfe-dev] [GSoC] Re: CSA constraint solver improvements<o:p></o:p></span></p></div></div><p class=MsoNormal><o:p> </o:p></p><p class=MsoNormal>Hi Manas,<o:p></o:p></p><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>Great to see some interest for the project!<o:p></o:p></p></div><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>The solver in question is fully located in <b>RangeConstraintManager.cpp</b>. There we try our best to provide useful ranges for symbolic expressions AND do it real fast. The last part is probably the most important thing here. This solver works every time we see a condition in code and when we tried using <b>z3</b> for this instead, it degraded performance so drastically that the analyzer is not useable (e.g 10min --> 25h). <o:p></o:p></p></div><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>However, we have found another application for <b>z3 </b>- refute produced warnings. When we are about to report a new warning, we can check that constraints are <b>sat/unsat</b> and discard the warning in the latter case. This happens way less frequently and good in terms of performance. Alas, the majority of users have static analyzer build without <b>z3</b>, and some false positives warnings sneak in.<o:p></o:p></p></div><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>So, there are two main directions that I see:<o:p></o:p></p></div><div><ul type=disc><li class=MsoNormal style='mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo1'>Figure out cases when <b>z3 </b>refutation works better than the built-in fast solver. <br>Run the analyzer in both modes and analyze the difference. Usually it’s under 10 warnings, so it won’t be very tedious.<o:p></o:p></li><li class=MsoNormal style='mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo1'>Add reasoning about range-based binary operations. <br>If we know ranges for symbols or symbolic expressions <b>x </b>and <b>y</b>, we can often reason about possible ranges for <b>x OP y</b>, where <b>OP</b> is some binary operator. At the moment, we have support for <b>&, |, </b>and <b>% </b>(it’s a bit weird set of operators, but it was driven by reported false positives).<o:p></o:p></li></ul><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>We are open for other suggestions and algorithms in this component, but I guess it’s valuable to start with the first bullet point to have a good motivation for improvements.<o:p></o:p></p></div><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>@Balazs, sorry for confusion. Here is a short description of the project I suggested for this year: <a href="https://llvm.org/OpenProjects.html#static_analyzer_constraint_solver">https://llvm.org/OpenProjects.html#static_analyzer_constraint_solver</a><o:p></o:p></p></div><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>It’s a logical continuation of my work:<o:p></o:p></p></div><div><p class=MsoNormal>D86465, D82445, D83286, D82381, D80117, D79434, and D79336<o:p></o:p></p></div><div><p class=MsoNormal><o:p> </o:p></p></div><div><p class=MsoNormal>Cheers,<o:p></o:p></p></div><div><p class=MsoNormal>Valeriy<o:p></o:p></p></div><div><p class=MsoNormal><br><br><o:p></o:p></p><blockquote style='margin-top:5.0pt;margin-bottom:5.0pt'><div><p class=MsoNormal>On 9 Apr 2021, at 11:37, via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> wrote:<o:p></o:p></p></div><p class=MsoNormal><o:p> </o:p></p><div><div><p class=MsoNormal>Good to hear that someone is interested in the SMT Solver part of the analyzer.<br><br>Mikhail Ramalho is probably the primary driving factor in this direction, but I try to participate/help as much as I can.<br>You probably already know, Artem Dergachev is the code owner of the CSA, so I guess, you can count on him as well.<br><br>Unfortunately, the SMT solver is not maintained, thus it is in pretty bad shape. It can not pass the tests for various reasons.<br>I planned to improve the situation, but it was always a low priority for me. My primary concern is the Z3 solver for bugreport refutation for the range-based solver.<br><br>I recommend you have a look at patches in the past using git blame.<br>AFAIK these three are the most important patches which not landed yet:<br>D83677, D83660, D85528<br><br>Regards, Balazs.<br><br>-----Original Message-----<br>From: cfe-dev <<a href="mailto:cfe-dev-bounces@lists.llvm.org">cfe-dev-bounces@lists.llvm.org</a>> On Behalf Of Manas via cfe-dev<br>Sent: 2021. április 9., péntek 10:01<br>To: clang-front-end mailing list <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>><br>Subject: [cfe-dev] [GSoC] Re: CSA constraint solver improvements<br><br>Hi everyone, <br><br>I am a pre-final year undergraduate in computer science. I am interested in "Clang Static Analyzer: constraint solver improvements" project.<br><br>I have around 8 months of experience with LLVM/Clang during my compilers class where I also implemented some dataflow analysis techniques for LLVM IR. I am also in middle of completing my decision procedures course at university. This course has helped me in gaining fundamental knowledge about solvers. I am familiar with range-based logic. Along with these, I have tried z3 while learning about solvers, and I think I can learn more about it fairly quickly.<br><br>I think this project fits for me. It will also help me in improving my knowledge further. I have started working on my proposal.<br><br>Can you give me further directions regarding the proposal for this project?<br><br>Thank you<br>--<br>Manas<br>CSAM Undergraduate | 2022<br>IIIT-Delhi, India<br>_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a><br><a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><br><br>_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a><br><a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><o:p></o:p></p></div></div></blockquote></div><p class=MsoNormal><o:p> </o:p></p></div></div></body></html>