<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=koi8-r">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Hi Aleksei,</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);">
Thank you for pointing out the right direction!<br>
</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);">
I originally wanted to figure out, through `SourceLocation`, which code extends from `assert(condition)`. But your `<span style="color: rgb(0, 0, 0); font-family: Calibri, Helvetica, sans-serif; font-size: 12pt;">__assert_fail</span>` approach is more straightforward
and easier to implement. Thanks!</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>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Aleksei Sidorin <a.sidorin@samsung.com><br>
<b>Sent:</b> Tuesday, August 7, 2018 18:08<br>
<b>To:</b> Henry Wong; cfe-dev@lists.llvm.org<br>
<b>Subject:</b> Re: [cfe-dev] [Analyzer] How to model `assert(condition)`?</font>
<div> </div>
</div>
<meta content="text/html; charset=utf-8">
<div style="background-color:#FFFFFF">
<div class="x_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"><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">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="x_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="x_mimeAttachmentHeader"></fieldset> <br>
<pre>_______________________________________________
cfe-dev mailing list
<a class="x_moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="x_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="x_moz-signature" cols="72">--
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics
</pre>
<table id="x_bannersignimg">
<tbody>
<tr>
<td>
<p> </p>
</td>
</tr>
</tbody>
</table>
<table id="x_confidentialsignimg">
<tbody>
<tr>
<td>
<p> <img style="border:0px solid currentColor; width:520px; height:144px; display:inline-block" data-outlook-trace="F:1|T:1" src="cid:cafe_image_0@s-core.co.kr"> </p>
</td>
</tr>
</tbody>
</table>
<img border="0" width="0" height="0" style="display:none" src="http://ext.w1.samsung.net/mail/ext/v1/external/status/update?userid=a.sidorin&do=bWFpbElEPTIwMTgwODA3MTAwODQ2ZXVjYXMxcDEwNWZkYWU0OTAwYTBkNzE4NTZkZjcyMjZlM2ZjYjM2ZiZyZWNpcGllbnRBZGRyZXNzPW1vdmlldHJhdmVsY29kZUBvdXRsb29rLmNvbQ__"></div>
</body>
</html>