<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi Henry,<br>
<br>
The main problem here is that this macro disappears without a
trace in case of release builds (or builds without assertions
enabled). In such case, we don't know if the related code even
existed because it is not present in the AST.<br>
In other cases, macro expansion works pretty well. CSA has
core.builtin.NoReturnFunctions checker. It handles some functions
used to terminate the execution on the 'false' branch of assert
macro. The macro itself usually looks like this:<br>
<br>
# define assert(expr) \<br>
((expr) \<br>
? __ASSERT_VOID_CAST (0) \<br>
: __assert_fail (__STRING(expr), __FILE__, __LINE__,
__ASSERT_FUNCTION))<br>
<br>
So, this checker just needs to model the `__assert_fail` function
by generating a sink. The name of this function is
implementation-dependent but the common approach is to just add
the function in this checker's list if it is not present.<br>
<br>
<br>
<br>
07.08.2018 10:26, Henry Wong via cfe-dev пишет:<br>
</div>
<blockquote type="cite"
cite="mid:PS1PR04MB28718CB33079B53FBE6867C6A4270@PS1PR04MB2871.apcprd04.prod.outlook.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<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>
<br>
<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>
<p><br>
</p>
<pre class="moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>
<table id=bannersignimg data-cui-lock="true" namo_lock><tr><td><p> </p>
</td></tr></table><table id=confidentialsignimg data-cui-lock="true" namo_lock><tr><td><p> <img style="border: 0px solid currentColor; border-image: none; width: 520px; height: 144px; display: inline-block;" unselectable="on" data-cui-image="true" src="cid:cafe_image_0@s-core.co.kr"> </p>
</td></tr></table></body>
</html>
<img src='http://ext.w1.samsung.net/mail/ext/v1/external/status/update?userid=a.sidorin&do=bWFpbElEPTIwMTgwODA3MTAwODQ2ZXVjYXMxcDEwNWZkYWU0OTAwYTBkNzE4NTZkZjcyMjZlM2ZjYjM2ZiZyZWNpcGllbnRBZGRyZXNzPWNmZS1kZXZAbGlzdHMubGx2bS5vcmc_' border=0 width=0 height=0 style='display:none'>