<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Hi Yitzhak,</div><div><br></div><div>Yay, finally happening! I 100% support these efforts and feel free to add me as a reviewer to the patches, design documents etc. </div><div>I have some questions/comments inline.</div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 12 Oct 2021 at 08:32, Yitzhak Mandelbaum <<a href="mailto:yitzhakm@google.com">yitzhakm@google.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div style="font-family:arial,helvetica,sans-serif"><span style="background-color:transparent;color:rgb(0,0,0);font-family:Arial;font-size:20pt;white-space:pre-wrap">Summary</span><br></div><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We propose a new static analysis framework for implementing Clang bug<span class="gmail_default" style="font-family:arial,helvetica,sans-serif">-</span>finding and refactoring tools (including ClangTidy checks) based on <span class="gmail_default" style="font-family:arial,helvetica,sans-serif">a</span> dataflow algorithm.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Some ClangTidy checks and core compiler warnings are already dataflow<span class="gmail_default" style="font-family:arial,helvetica,sans-serif"> </span>based. However, due to a lack of a reusable framework, all reimplement common dataflow<span class="gmail_default" style="font-family:arial,helvetica,sans-serif">-</span>analysis and CFG<span class="gmail_default" style="font-family:arial,helvetica,sans-serif">-</span>traversal algorithms. <span class="gmail_default" style="font-family:arial,helvetica,sans-serif">In addition to supporting new checks, t</span>he framework should allow us to clean up those parts of Clang and ClangTidy.</span></p></span></div></blockquote><div><br></div><div>We do have some helpers to make writing ad-hoc dataflow analyses somewhat easier, e.g., see <a href="https://github.com/llvm/llvm-project/blob/main/clang/include/clang/Analysis/FlowSensitive/DataflowWorklist.h">llvm-project/DataflowWorklist.h at main · llvm/llvm-project (github.com)</a></div><div>But I do agree there is a lot of room for improvement and having a full-fledged framework could be a great way forward.</div><div><br>There is a nice summary of some of the ad-hoc solutions we have in Clang in this survey: <a href="https://lists.llvm.org/pipermail/cfe-dev/2020-October/066937.html">[cfe-dev] A survey of dataflow analyses in Clang (llvm.org)</a></div><div>Do you plan to replace the ad-hoc solutions in the long run?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We intend that the new framework should have a learning curve similar to AST matchers and not require prior expertise in static analysis. Our goal is a simple API that isolates the user from the dataflow algorithm itself. The initial version of the framework combines support for classic dataflow analyses</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> over the Clang CFG with symbolic evaluation of the code and a simple model of local variables and the heap. A number of useful checks can be expressed solely in terms of this model, saving their implementers from having to reimplement modeling of the semantics of C++ AST nodes. Ultimately, we want to extend this convenience to a wide variety of checks, so that they can be written in terms of the abstract semantics of the program (as modeled by the framework), while only matching and modeling AST nodes for key parts of their domain (e.g., custom data types or functions).</span></p></span></div></blockquote><div><br></div><div>Just to reiterate, you want to abstract away both from the dataflow algorithm and the semantics of C++. E.g., the user might not need to handle the myriad of ways someone can assign a value to a variable (overloaded operator=, output argument, primitive assignment, etc), only a single abstract concept of assignment.</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><h1 dir="ltr" style="line-height:1.38;margin-top:20pt;margin-bottom:6pt"><span style="font-size:20pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Motivation</span></h1><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Clang has a few subsystems that greatly help with implementing bug-finding and refactoring tools:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">AST matchers</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> allow one to easily find program fragments whose AST matches a given pattern. This works well for finding program fragments whose desired semantics translates to a small number of possible syntactic expressions (e.g., "find a call to </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">strlen()</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> where the argument is a null pointer constant"). Note that patterns expressed by AST matchers often check program properties that hold for </span><span style="font-size:11pt;background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">all</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> execution paths.</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Clang Static Analyzer</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> can find program paths that end in a state that satisfies a specific user-defined property, regardless of how the code was expressed syntactically (e.g., "find a call to </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">strlen()</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> where the argument is dynamically equal to null"). CSA abstracts from the syntax of the code, letting analyses focus on its semantics. While not completely eliding syntax, symbolic evaluation abstracts over many syntactic details. Semantically equivalent program fragments result in equivalent program states computed by the CSA.</span></p></li></ul><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">When implementing certain bug-finding and refactoring tools, it is often necessary to find program fragments where a given property holds on all execution paths, while placing as few demands as possible on how the user writes their code. The proposed dataflow analysis framework aims to satisfy both of these needs simultaneously.</span></p><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Example: Ensuring that </span><span style="font-size:16pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::optional</span><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> is used safely</span></h2><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Consider implementing a static analysis tool that proves that every time a </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::optional</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> is unwrapped, the program has ensured that the precondition of the unwrap operation (</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">the optional has a value</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">) is satisfied.</span></p><br><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">has_value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">())</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestWithWarning</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(69,90,100);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">// warning: unchecked access to optional value</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p></td></tr></tbody></table></div><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">If we implemented this check in CSA, it would likely find the bug in </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestWithWarning</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">, and would not report anything in </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. However, CSA did not prove the desired property (all optional unwraps are checked on all paths) for </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">; CSA just could not find a path through </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> where this property is violated.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">A simple function like </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> only has two paths and would be completely explored by the CSA. However, when loops are involved, CSA uses heuristics to decide when to stop exploring paths in a function. As a result, CSA would miss this bug:</span></p><br><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">MissedBugByCSA</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">for</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">int</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> i </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">=</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(197,57,41);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">0</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">;</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> i </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(197,57,41);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">10</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">;</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> i</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">++)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">i </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(197,57,41);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">5</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">i</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">else</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(69,90,100);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">// CSA does not report a warning</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p></td></tr></tbody></table></div><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">If we implemented this check with AST matchers (as typically done in ClangTidy), we would have to enumerate way too many syntactic patterns. Consider just a couple coding variations that users expect this analysis to understand to be safe:</span></p><br><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">has_value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">()</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">==</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">true</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(!</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">has_value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">())</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(197,57,41);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">0</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">else</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TestOK</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(!</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">has_value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">())</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">return</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">use</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p></td></tr></tbody></table></div><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">To summarize, CSA can find </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">some</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> optional-unwrapping bugs, but it does not prove that the code performs a check on </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">all</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> paths. AST matchers can prove it for a finite set of hard-coded syntactic cases. But, when the set of safe patterns is infinite, as is often the case, AST matchers can only capture a subset. Capturing the full set requires building a framework like the one presented in this document.</span></p></span></div></blockquote><div><br></div><div>While most of the checks in CSA are using symbolic execution, there are also some syntactic rules. One dilemma of implementing a new check is where to put it (CSA? Tidy? Warnings?). While it would be great to get rid of this dilemma, I think we want to keep all of the options open. I just wanted to make it explicit what kinds of layering constraints we have. It should be possible to add CSA checks/features using the new dataflow framework.</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Comparison</span></h2><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse;table-layout:fixed;width:468pt"><colgroup><col><col><col><col></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><br></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">AST Matchers Library</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Clang Static Analyzer</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Dataflow Analysis Framework</span></p></td></tr><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Proves that a property holds on all execution paths</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Possible, depends on the matcher</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">No</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Yes</span></p></td></tr><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Checks can be written in terms of program semantics</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">No</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Yes</span></p></td><td style="border-width:1pt;border-style:solid;border-color:rgb(0,0,0);vertical-align:top;padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.2;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Yes</span></p></td></tr></tbody></table></div><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"></span></h2></span></div></blockquote><div><br></div><div>Another example where the forward symbolic execution of CSA falls short is backwards reasoning, e.g.:<br><br><font face="monospace">void f(int *p)</font></div><div><font face="monospace">{<br>  *p = 5;<br>  if (p) // Should warn: redundant null check or null dereference above.<br>  {<br>    ...</font></div><div><font face="monospace">  }<br>} </font></div><div><br></div><div>CSA will not warn on the code snippet above because it is assumed p is never null at the first dereference (to avoid noise) and it is really hard to revise old assumptions given new evidence. Such problems can be found using dataflow analysis.</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Further Examples</span></h2><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">While we have started with a </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::optional</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> checker, we have a number of further use cases where this framework can help. Note that some of these are already implemented in complex, specialized checks, either directly in the compiler or as clang-tidy checks. A key goal of our framework is to simplify the implementation of such checks in the future.</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“the pointer may be null when dereferenced”, “the pointer is always null when dereferenced”,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">"unnecessary null check on a pointer passed to delete/free",</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“this raw pointer variable could be refactored into a </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::unique_ptr</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">”,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“expression always evaluates to a constant”, “if condition always evaluates to true/false”,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“basic block is never executed”, “loop is executed at most once”, </span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“assigned value is always overwritten”,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“value was used after having been moved”,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“value guarded by a lock was used without taking the lock”,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">“unnecessary existence check before inserting a value into a std::map”.</span></p></li></ul><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Some of these use cases are covered by existing ClangTidy checks that are implemented with pattern matching. We believe there is an opportunity to simplify their implementation by refactoring them to use the dataflow framework, and simultaneously improve the coverage and precision of how they model C++ semantics.</span></p><h1 dir="ltr" style="line-height:1.38;margin-top:20pt;margin-bottom:6pt"><span style="font-size:20pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Overview</span></h1><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The initial version of our framework provides the following key features:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a forward dataflow algorithm, parameterized by a user-defined value domain and a transfer function, which describes how program statements modify domain values.</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a built-in model of local variables and the heap. This model provides two benefits to users: it tracks the flow of values, accounting for a wide variety of C++ language constructs, in a way that is reusable across many different analyses; it discriminates value approximations based on path conditions, allowing for higher precision than dataflow alone.</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">an interface to an SMT solver to verify safety of operations like dereferencing a pointer,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">test infrastructure for validating results of the dataflow algorithm.</span></p></li></ul></span></div></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Dataflow Algorithm</span></h2><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Our framework solves forward dataflow equations over a product of a user-defined value domain and a built-in model of local variables and the heap, called the </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">environment</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. The user implements the transfer function for their value domain, while the framework implements the transfer function that operates on the environment, only requiring a user-defined widening operator to avoid infinite growth of the environment model. We intend to expand the framework to also support backwards dataflow equations at some point in the future. The limitation to the forward direction is not essential.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">In more detail, the algorithm is parameterized by:</span></p><br><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a user-defined, finite-height partial order, with a join function and maximal element,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">an initial element from the user-defined lattice,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a (monotonic) transfer function for statements, which maps between lattice elements,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">comparison and merge functions for environment values.</span></p></li></ul></span></div></blockquote><div><br></div><div>What kind of control will the user have over the environment? E.g. could we add checks/extensions that model the effects of certain functions (e.g. std::swap) in the environment?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We expand on the first three elements here and return to the comparison and merge functions in the next section.</span></p><h3 dir="ltr" style="line-height:1.38;margin-top:16pt;margin-bottom:4pt"><span style="font-size:14pt;font-family:Arial;color:rgb(67,67,67);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The Lattice and Analysis Abstractions</span></h3><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We start with a representation of a lattice:</span></p><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">class</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">public</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">:</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">friend</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">bool</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">operator</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">==(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> lhs</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">                         </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> rhs</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">friend</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">bool</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">operator</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><=(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> lhs</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">                         </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> rhs</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">static</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Top</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">();</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">enum</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">class</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">JoinEffect</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Changed</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Unchanged</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">};</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">JoinEffect</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Join</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> element</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">};</span></p></td></tr></tbody></table></div><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Not all of these declarations are necessary. Specifically,  </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">operator==</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> and </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">operator<=</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> can be implemented in terms of </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Join</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> and </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Top</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> isn’t used by the dataflow algorithm. We include the operators because direct implementations are likely more efficient, and </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Top</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> because it provides evidence of a well-founded bounded join semi-lattice.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Join</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> operation is unusual in its choice of mutating the object instance and returning an indication of whether the join resulted in any changes. A key step of the fixpoint algorithm is code like </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">j = Join(x, y); if (j == x) …</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. This formulation of </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Join</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> allows us to express this code instead as </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if (x.Join(y) == Unchanged)...</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. For lattices whose instances are expensive to create or compare, we expect this formulation to improve the performance of the dataflow analysis.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Based on the lattice abstraction, our analysis is similarly traditional:</span></p><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">class</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">DataflowAnalysis</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">public</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">:</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">using</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">=</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">…;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">InitialElement</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">();</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">TransferStmt</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Stmt</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> stmt</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">BoundedJoinSemiLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> element</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Environment</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> environment</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">};</span></p></td></tr></tbody></table></div><br></span></div></blockquote><div> </div><div>Do you plan to provide building blocks to help users build lattices? E.g.,  I really like <a href="https://github.com/facebook/SPARTA">SPARTA</a>. They added some helpers to encode finite abstract domains, see <a href="https://github.com/facebook/SPARTA/blob/main/include/FiniteAbstractDomain.h">SPARTA/FiniteAbstractDomain.h at main · facebook/SPARTA (github.com)</a> for details.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Environment: A Built-in Lattice</span></h2><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">All user-defined operations have access to an </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">environment</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">, which encapsulates the program context of whatever program element is being considered. It contains:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a </span><span style="font-size:11pt;background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">path condition</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a storage model (which models both local variables and the heap).</span></p></li></ul><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The built-in transfer functions model the effects of C++ language constructs (for example, variable declarations, assignments, pointer dereferences, arithmetic etc.) by manipulating the environment, saving the user from doing so in custom transfer functions.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The path condition accumulates the set of boolean conditions that are known to be true on every path from function entry to the current program point.</span></p></span></div></blockquote><div><br></div><div>I am a bit opposed to using the term path-condition, as users might confuse this with similar terms used in path-sensitive analyses. What about flow-condition?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The environment maintains the maps from program declarations and pointer values to storage locations. It also maintains the map of storage locations to abstract values. Storage locations can be atomic (“scalar”) or aggregate multiple sublocations:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">ScalarStorageLocation</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> is a storage location that is not subdivided further for the purposes of abstract interpretation, for example </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">bool</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">, </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">int*</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">AggregateStorageLocation</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> is a storage location which can be subdivided into smaller storage locations that can be independently tracked by abstract interpretation. For example, a struct with public members.</span></p></li></ul></span></div></blockquote><div><br></div><div>Could you elaborate on the storage model? How do you plan to deal with aliasing? How do you represent arrays (with potentially unknown lengths)?</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">In addition to this storage structure, our model tracks three kinds of values: basic values (like integers and booleans), pointers (which reify storage location into the value space) and records with named fields, where each field is itself a value. For aggregate values, we ensure coherence between the structure represented in storage locations and that represented in the values: for a given aggregate storage location L</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><span style="font-size:0.6em;vertical-align:sub">agg</span></span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> with child </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">f</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">:</span></p><ul style="margin-top:0px;margin-bottom:0px"><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">valueAt(L</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><span style="font-size:0.6em;vertical-align:sub">agg</span></span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">) is a record, and</span></p></li><li dir="ltr" style="list-style-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt" role="presentation"><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">valueAt(child(L</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><span style="font-size:0.6em;vertical-align:sub">agg</span></span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">, </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">f</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)) = child(valueAt(L</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><span style="font-size:0.6em;vertical-align:sub">agg</span></span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">), </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">f</span><span style="font-size:11pt;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">), </span></p></li></ul><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">where </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">valueAt</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> maps storage locations to values.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">In our first iteration, the only basic values that we will track are boolean values. Additional values and variables may be relevant, but only in so far as they constitute part of a boolean expression that we care about. For example, </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if (x > 5) { … }</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> will result in our tracking </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x > 5</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">, but not any particular knowledge about the integer-valued variable </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">x</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The path conditions and the model refer to the same sets of values and locations.</span></p><h3 dir="ltr" style="line-height:1.38;margin-top:16pt;margin-bottom:4pt"><span style="font-size:14pt;font-family:Arial;color:rgb(67,67,67);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Accounting for infinite height</span></h3><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Despite the simplicity of our storage model, its elements can grow infinitely large: for example, path conditions on loop back edges, records when modeling linked lists, and even just the number of locations for a simple for-loop.  Therefore, we provide the user with two opportunities to interpret the abstract values so as to bound it: comparison of abstract values and a merge operation at control-flow joins.</span></p><br><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(69,90,100);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">// Compares values from two different environments for semantic equivalence.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">bool</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Compare</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> value1</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Environment</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> env1</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> value2</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Environment</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> env2</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(69,90,100);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">// Given `value1` (w.r.t. `env1`) and `value2` (w.r.t. `env2`), returns a</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(69,90,100);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">// `Value` (w.r.t. `merged_env`) that approximates `value1` and `value2`. This</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(69,90,100);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">// could be a strict lattice join, or a more general widening operation.</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Merge</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> value1</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Environment</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> env1</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> value2</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Environment</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> env2</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">      clang</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">dataflow</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Environment</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> merged_env</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">);</span></p></td></tr></tbody></table></div><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Verification by SAT Solver</span></h2><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">The path conditions are critical in refining our approximation of the local variables and heap. At an abstract level, they don’t need to directly influence the execution of the dataflow analysis. Instead, we can imagine that, once concluded, our results are annotated with/incorporate path conditions, which in turn allows us to make more precise conclusions about our program from the analysis results.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">For example, if the analysis concludes that a variable conditionally holds a non-null pointer, and, for a given program point, the path condition implies said condition, we can conclude that a dereference of the pointer at that point is safe. In this sense, the verification of the safety of a deference is separate from the analysis, which models memory states with formulae. That said, invocation of the solver need not wait until after the analysis has concluded. It can also be used during the analysis, for example, in defining the widening operation in </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Merge</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">With that, we can see the role of an SAT solver: to solve questions of the form “Does the path condition satisfy the pre-condition computed for this pointer variable at this program point”? To that end, we include an API for asking such questions of a SAT solver. The API is compatible with Z3 and we also include our own (simple) SAT solver, for users who may not want to integrate with Z3.</span></p></span></div></blockquote><div><br></div><div>What representation do you use for the path condition? Using the syntactic forms, like `x > 5` might not be sufficient as `x` might have different values at different program points.  E.g.,<br><br><font face="monospace">void f(int x)<br>{<br>  assert(x > 0);<br>  ...<br>  x = -1;<br>  funcWithPreconditionXIsPositive(x); // Wants to execute the SAT query here.<br>}</font></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><h2 dir="ltr" style="line-height:1.38;margin-top:18pt;margin-bottom:6pt"><span style="font-size:16pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Testing dataflow analysis</span></h2><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We provide test infrastructure that allows users to easily write tests that make assertions about a program state computed by dataflow analysis at any code point. Code is annotated with labels on points of interest and then test expectations are written with respect to the labeled points.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">For example, consider an analysis that computes the state of </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> values. </span></p><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">ExpectDataflowAnalysis</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">OptionalChecker</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">>(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">R</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">"(</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void f(std::optional<int> opt) {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  if (opt.has_value()) {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    // [[true-branch]]</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  } else {</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    // [[false-branch]]</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  }</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">})"</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">[](</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">const</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">auto</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">&</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> results</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  EXPECT_LE</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">results</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">ValueAtCodePoint</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">"true-branch"</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">),</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">OptionalLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Engaged</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">  EXPECT_LE</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">results</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">ValueAtCodePoint</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">"false-branch"</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">),</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">OptionalLattice</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(51,103,214);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">NullOpt</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">());</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">});</span></p></td></tr></tbody></table></div><br><h1 dir="ltr" style="line-height:1.38;margin-top:20pt;margin-bottom:6pt"><span style="font-size:20pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Timeline</span></h1><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We have a fully working implementation of the framework as proposed here. We also are interested in contributing a clang-tidy checker for </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::optional</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> and related types as soon as possible, given its demonstrated efficacy and interest from third parties.  To that end, as soon as we have consensus for starting this work in the clang repository, we plan to start sending patches for review. Given that the framework is relatively small, we expect it will fit within 5 (largish) patches, meaning we can hope to have it available by December 2021.</span></p><h1 dir="ltr" style="line-height:1.38;margin-top:20pt;margin-bottom:6pt"><span style="font-size:20pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Future Work</span></h1><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">We consider our first version of the framework as experimental. It suits the needs of a number of particular checks that we’ve been writing, but it has some obvious limitations with respect to general use.  After we commit our first version, here are some planned areas of improvement and investigation.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Backwards analyses.</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> The framework only solves forward dataflow equations. This clearly prevents implementing some very familiar and useful analyses, like variable liveness. We intend to expand the framework to also support backwards dataflow equations. There’s nothing inherent to our framework that limits it to forwards.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Reasoning about non-boolean values.</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> Currently, we can symbolically model equality of booleans, but nothing else. Yet, for locations on the store that haven’t changed, we can understand which values are identical (because the input value object is passed by the transfer function to the output). For example,</span></p><div dir="ltr" style="margin-left:0pt" align="left"><table style="border:none;border-collapse:collapse"><colgroup></colgroup><tbody><tr style="height:0pt"><td style="border-width:1pt;border-style:solid;border-color:rgb(224,224,224);vertical-align:top;background-color:rgb(250,250,250);padding:5pt;overflow:hidden"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">void</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> f</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">bool</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">,</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">bool</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">*</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">b</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    std</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">::</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">optional</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(15,157,88);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><int></span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> opt</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">;</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">==</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> b</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> opt </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">=</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(197,57,41);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">42</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">;</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">    </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(156,39,176);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">if</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">(</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">==</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> b</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">)</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">{</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> opt</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">value</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">();</span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> </span><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:10pt;font-family:Consolas,sans-serif;color:rgb(97,97,97);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">}</span></p></td></tr></tbody></table></div><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Since neither </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> nor </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">b</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> have changed, we can reason that the two occurrences of the expression </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">a == b</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> evaluate to the same value (even though we don't know the exact value). We intend to improve the framework to support this increased precision, given that it will not cost us any additional complexity.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Improve<span class="gmail_default" style="font-family:arial,helvetica,sans-serif">d</span> model of program state.</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> A major obstacle to writing high-quality checks for C++ code is the complexity of C++’s semantics.  In writing our framework, we’ve come to see the value of shielding the user from the need to handle these directly by modeling program state and letting the user express their check in terms of that model, after it has been solved for each program point. As is, our model currently supports a number of checks, including the </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::optional</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> check and another that infers which pointer parameters are out parameters. We intend to expand the set of such checks, with improvements to the model and the API for expressing domain-specific semantics relevant to a check. Additionally, we are considering explicitly tracking other abstract program properties, like reads and writes to local variables and memory, so that users need not account for all the syntactic variants of these operations.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Refactoring existing checks.</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> Once the framework is more mature and stable, we would like to refactor existing checks that use custom, ad-hoc implementations of dataflow to use this framework.</span></p></span></div></blockquote><div><br></div><div>Is inter-procedural analysis out of scope (e.g., using summaries)?  </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><span id="gmail-m_6363276251667500755gmail-docs-internal-guid-92538444-7fff-e16c-5bde-24e022f427e9"><h1 dir="ltr" style="line-height:1.38;margin-top:20pt;margin-bottom:6pt"><span style="font-size:20pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Conclusion</span></h1><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"><span class="gmail_default" style="font-family:arial,helvetica,sans-serif">We have</span> proposed an addition to the Clang repository of a new static analysis framework targeting </span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-style:italic;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">all-paths</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> analyses. The intended clients of such analyses are code-checking and transformation tools like clang-tidy, where sound analyses can support sound transformations of code. We discussed the key features and APIs of our framework and how they fit together into a new analysis framework. Moreover, our proposal is based on experience with a working implementation that supports a number of practical, high-precision analyses, including one for safe use of types like </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::optional</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> and another that finds missed opportunities for use of </span><span style="font-size:11pt;font-family:Consolas,sans-serif;color:rgb(13,144,79);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">std::move</span><span style="font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p></span><br><div style="font-family:arial,helvetica,sans-serif"></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div>
</blockquote></div></div></div></div></div></div>