<html>
<head>
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
</head>
<body text="#000000" bgcolor="#FFFFFF">
Assertions are already modeled by core.builtin.NoReturnFunctions.<br>
<br>
Having assertions work in NDEBUG builds is an open problem and it's
not easy, which is why we write it in the user guide to only use the
analyzer on debug builds.<br>
<br>
<br>
<div class="moz-cite-prefix">On 8/7/18 12:26 AM, Henry Wong via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:PS1PR04MB28718CB33079B53FBE6867C6A4270@PS1PR04MB2871.apcprd04.prod.outlook.com">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
Hi all,</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
I want to know if anyone has tried to model `assert()`? Or has
some thoughts on it?</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
`assert()` is a macro defined as follows:</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<span> #ifdef NDEBUG<br>
</span>
<div><span style=" background-color: rgb(255, 255, 255);
display: inline !important"> <span> <span style="
background-color: rgb(255, 255, 255); display: inline
!important"> <span> </span></span></span></span>#define
assert(condition) ((void)0)<br>
</div>
<div><span style=" background-color: rgb(255, 255, 255);
display: inline !important"> <span> </span></span>#else<br>
</div>
<div><span style=" background-color: rgb(255, 255, 255);
display: inline !important"> <span> </span></span><span
style=" background-color: rgb(255, 255, 255); display:
inline !important"> <span> </span></span>#define
assert(condition) /*implementation defined*/<br>
</div>
<span><span style=" background-color: rgb(255, 255, 255);
display: inline !important"> <span> </span></span>#endif</span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<span><br>
</span></div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
It's difficult for analyzer to figure out which part is expanded
from macro `assert()`. The ways I can think of immediately are
as follows.</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
(1) Use some clang-based rewrit tools to replace
`assert(condition)` with `if (!condition) exit(0)`. </div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
This way will loose the semantics of `assert()` and only
gurantee the `condition` must be true after the `assert` is
evaluated.</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
(2) Add two CFGElement kinds, `AssertBegin` and `AssertEnd`,
like `ScopeBegin` and `ScopeEnd`. In this way, analyzer can
easily figure out whether the current program point is in
`assert()`.</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
(3) Use `checkPreStmt(const Expr *)` and `checkPostStmt(const
Expr *)` to figure out whether the current Stmt is expanded
from `assert`.</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
Once the `assert()` part is located, the rest of the work is
modeling. Like `__builtin_assume` in <a
href="https://reviews.llvm.org/D33092" id="LPlnk708287"
moz-do-not-send="true">https://reviews.llvm.org/D33092</a>, we
can use `ProgramState::assume` to get two states, one is a sink
state corresponding to the assertion failure and the other is
the valid state.</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
Any suggestions?</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
Thanks in advance!</div>
<div style="font-family: Calibri, Helvetica, sans-serif;
font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div style="font-family:Calibri,Helvetica,sans-serif;
font-size:12pt; color:rgb(0,0,0)">
Henry Wong</div>
<div style="font-family:Calibri,Helvetica,sans-serif;
font-size:12pt; color:rgb(0,0,0)">
Qihoo 360 Codesafe Team</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>