[cfe-dev] [Analyzer] How to model `assert(condition)`?

[Aleksei Sidorin via cfe-dev]

Hi Henry,

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.
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:

# define assert(expr)                            \
   ((expr)                                \
    ? __ASSERT_VOID_CAST (0)                        \
    : __assert_fail (__STRING(expr), __FILE__, __LINE__, __ASSERT_FUNCTION))

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.



07.08.2018 10:26, Henry Wong via cfe-dev пишет:
> Hi all,
> I want to know if anyone has tried to model `assert()`? Or has some 
> thoughts on it?
>
> `assert()` is a macro defined as follows:
>     #ifdef NDEBUG
> #define assert(condition) ((void)0)
> #else
> #define assert(condition) /*implementation defined*/
> #endif
>
> 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.
>
> (1) Use some clang-based rewrit tools to replace `assert(condition)` 
> with `if (!condition) exit(0)`.
> This way will loose the semantics of `assert()` and only gurantee the 
> `condition` must be true after the `assert` is evaluated.
>
> (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()`.
>
> (3) Use `checkPreStmt(const Expr *)` and `checkPostStmt(const Expr *)` 
> to figure out whether the current Stmt is expanded from `assert`.
>
> Once the `assert()` part is located, the rest of the work is modeling. 
> Like `__builtin_assume` in https://reviews.llvm.org/D33092, 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.
>
> Any suggestions?
>
> Thanks in advance!
>
> Henry Wong
> Qihoo 360 Codesafe Team
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


-- 
Best regards,
Aleksei Sidorin,
SRR, Samsung Electronics

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180807/db4981e1/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: image/gif
Size: 13168 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180807/db4981e1/attachment.gif>