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

[Artem Dergachev via cfe-dev]

Assertions are already modeled by core.builtin.NoReturnFunctions.

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.


On 8/7/18 12:26 AM, Henry Wong via cfe-dev wrote:
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180807/32318291/attachment.html>