[cfe-dev] Checking Model Used by 'ArrayBoundV2'

[Anna Zaks]

On Dec 3, 2011, at 2:32 PM, Benjamin Schulz wrote:

> The SA developer manual states that: "Each time the analyzer engine
> explores a new statement, it notifies each checker registered to listen
> for that statement, giving it an opportunity to either report a bug or
> modify the state.  (As a rule of thumb, the checker itself should be
> stateless.)"
> 
> Am I correct to read this as indicating that each active checker is
> invoked each time a statement is symbolically executed, with each
> checker reading the same symbolic store and context through accessors at
> each invocation?
The SA developer manual is still rather weak (thus the red "under construction" sign:)). 

Each checker can choose to register for the events it is interested in through implementing callbacks (See http://clang.llvm.org/doxygen/classento_1_1CheckerDocumentation.html). This allows the checkers to report bugs or/and modify the program state (for example, a checker can add it's own information to the state for bookkeeping). Suppose, several checkers (C1, C2, C3) register for the same event, say checkPostStmt for a function call. In order to allow each checker to examine/modify the state, we chain them together. Specifically, we might add a chain of nodes (State_after_call, Loc_X) -> (State_C1, Loc_X)  -> (State_C2, Loc_X) -> (State_C3, Loc_X) to the symbolic execution graph, where State_Ci is the state produced by checker Ci.

> 
>> Currently, the main limitations are the lack of interprocedural analysis
>> and a rather weak solver ( ex: it doesn't correctly model truncation)
>> Feel free to file bugs for issues if you are unsure.
> 
> Given that all of the above is true, I have a hypothesis that Jones and
> Kelly's runtime checking scheme [1] could be adapted or weakened to
> produce a symbolically executed check that could overcome some of the
> present checker's limitations.  The main difficulty is that it would not
> be sufficient to just write a new checker; the symbolic execution engine
> would also need a modest extension.

All of the mentioned weaknesses lie within the analyzer core engine. The general design idea is that the core engine does most of the work and only the check specific rules are implemented within each checker.

> 
> My questions are: (1) Has this possibility already been considered?

The parer discusses a runtime checking technique (similarly to AddressSanitizer, SAFECode), so only some of the presented ideas would be applicable. 

For example, as I mentioned earlier, the analyzer does not have interprocedural analysis, which means that when we symbolically execute a function call, we completely abstract it to say that we do not know what happened to the variables which could have been modified by the call. Also, we assume that we do not know anything about the input parameters to functions. There are ways to solve these issues by implementing interprocedural analysis (inlining or summary based) or/and adding annotations on function arguments. However, none have been implemented yet.

On the other hand, I suspect there could be checks mentioned in the paper that the ArrayBoundV2 checker does not have. 

I only briefly looked at the paper. Do you have other suggestions?

>  (2)
> What's the likelihood that such an addition would represent a change
> that's too big or ambitious for Clang/LLVM's accepted practice of small,
> incremental changes?

Even big additions can be executed as a sequence of small steps. As long as we have a clear picture of what we are trying to achieve and how it fits into the bigger setting.

Cheers,
Anna. 

> 
> 
> Thanks,
> 
> - --Benjamin Schulz
> 
> * * *
> 
> [1] Richard W. M. Jones and Paul H. J. Kelly.  "Backwards-Compatible
> Bounds Checking for Arrays and Pointers in C Programs."  AADEBUG'97.
> Available here:
> http://www.doc.ic.ac.uk/~phjk/phjk-Publications.html#Jones:Kelly:BC:97
> 
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.10 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
> 
> iQEcBAEBAgAGBQJO2qOBAAoJECT8Sbi31ptpWbkIAM4a8iJ6ci+rnzxlhAnW7NU4
> eoGQ6Au8qCxsvz2LasSOFt2gYdjKzDbKK2Q4QQ31BM/W8+tKUzgVfob0kQj5RtO5
> NJu1kuVpZ6K9jPthkkBAGiMiyawY58YmS1gHsU3FgMrq3fTBZ1IT2iea9Iib11Jk
> yqfJxiPM2n8CcrI1n0RpRTFx6KCqQl5t2KREkG7RxK60DDFElxV8faZ5SzRLt4fa
> 6dGkzqebh1gULb1oJL5U3dIbnyZmOor+gnnyXs1wwdlvqAifz52bGLWVJJBiZ7cx
> gu7AcBKsxG8ewh6+JP24hwuHcBPv5/30OkO4c4lSNcLXH4ReHF+Nps1Gx0ZhGSQ=
> =rXqa
> -----END PGP SIGNATURE-----
> 
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev

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