# AACalysto

AACalysto is an unsound static checker for C assertions, based on the ideas of Calysto. Using AAL to handle references and AAProver as theorem prover, it tries to prove all C assertions present in the input. (See thesis for more details.)

It is implemented as an LLVM pass and available for download. Note that it is not able to handle all LLVM input (e.g. support for exceptions or certain builtin functions is missing).

It is implemented as an LLVM pass and available for download. Note that it is not able to handle all LLVM input (e.g. support for exceptions or certain builtin functions is missing).

## Example 1

As a first example I'd like to prove that a function for counting the amount of bits set never returns a higher value than 32 or less than zero.
1: int unconstrained;
2: void recurse() {
3: recurse();
4: unconstrained++;
5: }
6:
7: int bitCount(unsigned x) {
8: unsigned res = x - ((x >> 1) & 033333333333)
9: - ((x >> 2) & 011111111111);
10: return ((res + (res >> 3)) & 030707070707) % 63;
11: }
12:
13: int main() {
14: recurse(); // Small trick to cheat the tool and
15: // making 'unconstrained' unconstrained.
16: int res = bitCount(unconstrained);
17: assert(res <= 32);
18: assert(res >= 0);
19:
20: assert(res > 0);
21: assert(res < 32);
22:
23: return 0;
24: }

AACalysto is able to prove both assertions on line 17 and 18. However it fails when trying to prove the remaining two assertions. Even better, it is able to give a contradicting assignment for those two (in the first case unconstrained must be zero, in the second case it must be the signed integer -1).## Example 2

This example is here to demonstrate the (partial) path-sensitivity of AACalysto.
1: int unconstrained;
2: void recurse() {
3: recurse();
4: unconstrained++;
5: }
6:
7: int main() {
8: recurse(); // Same trick as above
9: int someValue = unconstrained;
10:
11: int x;
12: if (someValue == 42)
13: x = 42;
14: else
15: x = 0;
16:
17: assert(someValue - x != 42);
18: assert(someValue != 42);
19:
20: return 0;
21: }

Thanks to path-sensitivity, AACalysto is able to prove the first assertion. The second assertion is there to show that someValue can indeed be 42 and AACalysto is of course unable to prove this assertion.