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

[Benjamin Schulz]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1


Firstly, thanks for the clarification.

> (source code and the analyzer site are the best sources of documentation).

I've taken a look at these.  As a lead-in to my next question, I wanted
to make sure that I so far understand the overall structure of the analyzer.

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?

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

My questions are: (1) Has this possibility already been considered?  (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?


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