<div dir="ltr"><div>(Adding Artem as he is very knowledgeable in this topic)</div><div><br></div><div>Oh, I see. In case it is known that you have a bounded number of paths it is not entirely unreasonable to use symbolic execution to achieve what you want.</div><div><br></div><div>Unfortunately, this is not a use-case that the static analyzer was designed for. I think it should be possible to tweak it but I have no idea how much work would that be. </div><div><br></div><div>But even though it might be possible to tweak the analyzer I am not sure if this would be the right thing to do. Some questions that might help:<br><br>1. How much control-flow awareness do you need? Do you really need path-sensitivity or flow-sensitive is sufficient? Or maybe lexical scoping is enough?</div><div><br></div><div>You only need path sensitive check if you want to avoid false positives in the form of:</div><div>if (cond)<br> lock();</div><div>// ...</div><div>if (cond)</div><div> unlock();</div><div><br></div><div>It looks like you already have some constraints on the coding style in the code you want to check. So I guess there is a chance that users are not allowed to do locking using complex patterns like the one above. If that is the case, flow-sensitive analysis might be a better fit as it is easier to make that exhaustive and will perform much better.</div><div>Or in case RAII style locking would be sufficient but you do not have dtors in C, you can have syntactic checks that enforce hand-written RAII style resource management.</div><div><br></div><div>2. Do you need interprocedural analysis? If so, do you have recursion? Do you need context sensitivity? Can you add annotations to help guide the analysis?</div><div><br></div><div>3. How complex is the task that you want to accomplish? Are locks reentrant? Do you have to support more complex try_lock style APIs? Or is it sufficient to only check the order of the API calls?</div><div><br></div><div>In case you can add annotations and you do not need path sensitivity you could take a look at Thread Safety Analysis: <a href="https://clang.llvm.org/docs/ThreadSafetyAnalysis.html">https://clang.llvm.org/docs/ThreadSafetyAnalysis.html</a></div><div><br></div><div>Cheers,</div><div>Gabor</div><div><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jan 15, 2020 at 8:48 AM Fernandez, Matthew <<a href="mailto:matthew.fernandez@intel.com">matthew.fernandez@intel.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 lang="EN-US">
<div class="gmail-m_3781478804956320713WordSection1">
<p class="MsoNormal">Hi Gabor,<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thanks for your reply. The checker I’m implementing is similar to PthreadLockChecker. It knows the correct acquire/release patterns for certain primitives and checks for them. If analysis fails to reach the end of a function, the checker
cannot warn for e.g. unreleased locks.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">This is a somewhat unorthodox case as I know the target code to which this will be applied. All functions are <500LoC and the only loops are statically bounded. It is observable statically that all functions terminate and there are a finite
number of paths.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">I was hoping to use CSA for this because it handles path enumeration and constructing the exploded graph very nicely. Someone suggested to me I might have to move to KLEE, but that would be a shame because I’d need to introduce some code
instrumentation/annotation to achieve what I want. Another option would be to use an AST visitor to enumerate the paths myself, but it would be nice to leverage LLVM’s existing functionality for this.<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
<p class="MsoNormal">Matthew<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<div style="border-top:none;border-right:none;border-bottom:none;border-left:1.5pt solid blue;padding:0in 0in 0in 4pt">
<div>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(225,225,225);padding:3pt 0in 0in">
<p class="MsoNormal"><b>From:</b> Gábor Horváth <<a href="mailto:xazax@google.com" target="_blank">xazax@google.com</a>> <br>
<b>Sent:</b> Wednesday, January 15, 2020 08:13<br>
<b>To:</b> Fernandez, Matthew <<a href="mailto:matthew.fernandez@intel.com" target="_blank">matthew.fernandez@intel.com</a>><br>
<b>Cc:</b> <a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<b>Subject:</b> Re: [cfe-dev] exhaustiveness of CSA checkers<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<p class="MsoNormal">Hi!<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">The clang static analyzer does not give you any guarantees regarding the coverage/exhaustiveness. There is no way to ensure exhaustive analysis (such analysis is likely to be unbounded for most non-trivial programs, so this is not only
about runtime, but also termination). For this reason all the checks have to be implemented with non-exhaustiveness in mind.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Could you share what you are trying to achieve? Maybe symbolic execution is not the right tool for that problem. <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Cheers,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Gabor<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal">On Wed, Jan 15, 2020 at 12:58 AM Fernandez, Matthew via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>> wrote:<u></u><u></u></p>
</div>
<blockquote style="border-top:none;border-right:none;border-bottom:none;border-left:1pt solid rgb(204,204,204);padding:0in 0in 0in 6pt;margin-left:4.8pt;margin-right:0in">
<div>
<div>
<p class="MsoNormal">Hello cfe-dev,<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">In prototyping a custom checker for the Clang Static Analyzer, I’ve found analysis terminates at some complexity limit. That is, when your target function exceeds some complexity
bound, CSA stops path traversal and your checker does not receive callbacks for any remaining unvisited nodes. The two specific scenarios where I’ve run into this are high-iteration-count loops and complex conditionals (multiple short circuiting && and ||
operators). The first I can work around by rephrasing the target loops or something like -analyzer-max-loop, but I can’t find a way to affect the behavior of the second. To compound the situation, I cannot see how the checker can detect that path exploration
was incomplete.<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Is there a way to control the complexity limit enforced for conditionals? Or, failing that, to detect within the checker when path exploration was incomplete?<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">To give some more context, my checker is an experiment and not something I am intending to upstream. Runtime is not an issue; I am fine with the analyzer taking multiple hours for
a single run. Though I understand why the existing CSA bound choices have been made, as most users do not want their compiler to run for this long.<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Please CC me in replies as I’m not subscribed.<u></u><u></u></p>
<p class="MsoNormal"> <u></u><u></u></p>
<p class="MsoNormal">Thanks,<u></u><u></u></p>
<p class="MsoNormal">Matthew<u></u><u></u></p>
</div>
</div>
<p class="MsoNormal">_______________________________________________<br>
cfe-dev mailing list<br>
<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a><u></u><u></u></p>
</blockquote>
</div>
</div>
</div>
</div>
</blockquote></div></div>