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

[Henry Wong via cfe-dev]

Hi Aleksei,

Thank you for pointing out the right direction!

I originally wanted to figure out, through `SourceLocation`, which code extends from `assert(condition)`. But your `__assert_fail` approach is more straightforward and easier to implement. Thanks!

Henry Wong
Qihoo 360 Codesafe Team
________________________________
From: Aleksei Sidorin <a.sidorin at samsung.com>
Sent: Tuesday, August 7, 2018 18:08
To: Henry Wong; cfe-dev at lists.llvm.org
Subject: Re: [cfe-dev] [Analyzer] How to model `assert(condition)`?

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<mailto:cfe-dev at lists.llvm.org>
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



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





 [cid:cafe_image_0 at s-core.co.kr]



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