<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<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 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="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>
</body>
</html>