Verifying a simple C function using CPAChecker

[Dominic Mulligan]

Hi,

I have the following simple C function, which I have already managed to prove correct using Frama-C and has also been proved correct in Coq with CompCert-VST:

  /*@ requires \valid(start+(0 .. limit-1));
    @ ensures  \forall size_t i; 0 <= i < limit ==> *(start + i) == 0;
    @ assigns  start[0..(limit-1)];
    @*/
  void mem_zero_fill(uint8_t * const start, size_t limit)
  {
    /*@ loop assigns   i, start[0..(limit-1)];
      @ loop invariant \forall size_t j; 0 <= j < i ==> *(start + j) == 0;
      @ loop variant   limit - i;
      @*/
    for(size_t i = 0; i < limit; ++i)
    {
      *(start + i) = 0;
    }
  }

I would now like to use CPAChecker (Git HEAD as of yesterday) to prove this function correct too to compare and contrast the approaches.  So I write the following testbench (omitting the definition of mem_zero_fill):

  #include <stdint.h>
  #include <stdlib.h>

  extern void __VERIFIER_error() __attribute__ ((__noreturn__));
  #define __VERIFIER_assert(e) { if(!(e)) { ERROR: __VERIFIER_error(); } }

  extern size_t __VERIFIER_nondet_size_t(void);
  extern int    __VERIFIER_assume(int);

  void mem_zero_fill(uint8_t * const start, size_t limit)
  {
    ...
  }

  int main(int argc, char** argv)
  {
    size_t   size   = __VERIFIER_nondet_size_t();
    uint8_t* buffer = malloc(sizeof(uint8_t) * size);
 
    if(!buffer) return -1;
 
    mem_zero_fill(buffer, size);
 
    size_t   idx    = __VERIFIER_nondet_size_t();
    __VERIFIER_assume(idx < size);
    __VERIFIER_assert(buffer[idx] == 0);
 
    return 0;
  }

And try to run CPAChecker using predicateAnalysis:

  $ ./scripts/cpa.sh -preprocess  -predicateAnalysis ~/Desktop/mem_zero_fill.c

which gives me an unknown result due to failure of interpolation during refinement, as splitting AB-mixed terms is not supported.  So I try another configuration:

  $ ./scripts/cpa.sh -preprocess -config ./config/predicateAnalysis-slicing.properties ~/Desktop/mem_zero_fill.c

and this time CPAChecker informs me that the verification result is FALSE.  Opening up the counterexample file, I see that the tool has spotted that there's a feasible path to an ERROR label, but to reach that point it had to have ignored my __VERIFIER_assume() function.  Searching the archives of this list, I apparently have to tell CPAChecker that __VERIFIER_assume() is indeed a means of introducing assumptions.  So I try the following:

   $ ./scripts/cpa.sh -preprocess -config ./config/predicateAnalysis-slicing.properties ~/Desktop/mem_zero_fill.c -setprop cfa.assumeFunctions={"__VERIFIER_assume"}

and the verification result is ... still FALSE.  Reopening the counterexample file I see that this time the CFA includes __VERIFIER_assume on an edge, but there's still apparently a feasible path to an ERROR label.  Searching more, it appears that I must change the specification that I am using so that assumptions are taken into account.  So, I look in the ./config/specification/ directory and there's a few with promising names.  So I try the following:

  $ ./scripts/cpa.sh -preprocess -config ./config/predicateAnalysis-slicing.properties -spec ./config/specification/Assertion.spc ~/Desktop/mem_zero_fill.c -setprop cfa.assumeFunctions={"__VERIFIER_assume"}

and now the verification result is TRUE.  Great.  But now I'm not really sure what precisely it is that I have verified as correct!  So I try to sanity check the testbench, by flipping the "less than" to a "greater than" in the __VERIFIER_assume() above.  Running CPAChecker again, the verification result is still TRUE.

This is the point where I turn to this mailing list:

  1. How does a newcomer actually learn to use CPAChecker effectively?  Other tools we are already using/evaluating like CBMC, Frama-C and so on seem to have a fairly structured path to take a newcomer from knowing nothing about the tool to using it fairly productively.  After searching, I have not found any tutorial material on CPAChecker, however.  Is there any?  If not, what is the best way of actually learning to use the tool and understand what all the settings do barring sitting down with an already-expert user?

  2. What is an AB-mixed term and why is -predicateAbstraction failing on my C code above?  How can I look at my C code and predict that this will fail?  I notice that a few other bundled *.properties files seem to fail for this reason (and some for various other reasons), and I'm wondering what is causing this and how we can structure our C to avoid problems like this.

  3. What combination of specification and configuration do I need to use with CPAChecker to get it to check my testbench above?

  4. What is predicateAbstraction-slicing.properties and Assertion.spc actually checking above, and why is it returning the same verification result even if the assumption is flipped?  Moreover, how do I convince myself from looking at a .properties and a .spc file that CPAChecker is correctly checking the property that I am interested in?  Other tools like CBMC have a much smaller configuration space and therefore it is easier for a user (and other engineers) to be convinced that relevant properties are indeed being checked.  However, with CPAchecker the configuration space appears to be so huge that it's easy to silently check the wrong thing.  Is there any suggested guidance here?

The last question above may sound trollish, but we are evaluating various verification tools for prospective use on a large industrial code-base (CBMC is already being used) and it's important that we are able to understand and communicate to other members of our team who are not formal methods experts what exactly it is that is being checked and, perhaps more importantly, what is not.

Many thanks,

Dominic

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Hi Dominic,

thank you for your interest in CPAchecker!

Am 03.08.2018 um 10:45 schrieb 'Dominic Mulligan' via CPAchecker Users:

> And try to run CPAChecker using predicateAnalysis:
>
> $ ./scripts/cpa.sh -preprocess -predicateAnalysis
> ~/Desktop/mem_zero_fill.c

In the attached file you have inverted the condition in the assume.
I can confirm this only if I revert the assumption to "idx < size"
(which is also the correct way of writing this assumption).

> which gives me an unknown result due to failure of interpolation
> during refinement, as splitting AB-mixed terms is not supported.

This means that the SMT solver which this analysis relies on failed.
The message about AB-mixed terms is produced directly by the SMT solver.
The underlying cause here is that the required reasoning about arrays
and quantifiers is too hard for the SMT solver.
I tried with the other SMT solvers that CPAchecker can use, but none
of these can solve the required queries.

Unfortunately, such queries about quantifiers and arrays are often too
hard for any SMT solver that we know of, so while CPAchecker's
predicate analysis could verify this program in theory, it can't in
practice.
We are working on finding alternative strategies that require less
from the SMT solver, but this is ongoing research.

There are also ways to work around this by manually supplying some
helpful predicates, but as I guess you are interested in an automatic
solution, I won't go into more detail here.

> So I try another configuration:
>
> $ ./scripts/cpa.sh -preprocess -config
> ./config/predicateAnalysis-slicing.properties
> ~/Desktop/mem_zero_fill.c
>
> and this time CPAChecker informs me that the verification result is
> FALSE. Opening up the counterexample file, I see that the tool has
> spotted that there's a feasible path to an ERROR label, but to
> reach that point it had to have ignored my __VERIFIER_assume()
> function.

It doesn't ignore __VERIFIER_assume it, you should see it being
converted into branching in the control-flow automaton ([idx < size]).
This has exactly the desired effect.

The counterexample that CPAchecker finds in fact has size=2 and idx=1,
so it does not violate the assumption.

It seems that this (new and experimental) slicing configuration is too
imprecise for your example, it seems that it slices away too much.

> Searching the archives of this list, I apparently have to tell
> CPAChecker that __VERIFIER_assume() is indeed a means of
> introducing assumptions. So I try the following:
>
> $ ./scripts/cpa.sh -preprocess -config
> ./config/predicateAnalysis-slicing.properties
> ~/Desktop/mem_zero_fill.c -setprop
> cfa.assumeFunctions={"__VERIFIER_assume"}
>
> and the verification result is ... still FALSE. Reopening the
> counterexample file I see that this time the CFA includes
> __VERIFIER_assume on an edge, but there's still apparently a
> feasible path to an ERROR label.

You would need to use
- -setprop cfa.assumeFunctions=__VERIFIER_assume (no curly braces),
but this is actually the default, so just omit it.

In fact, with your option CPAchecker warns you that __VERIFIER_assume
has no (side-)effect:
Assuming external function __VERIFIER_assume to be a pure function.

> Searching more, it appears that I must change the specification
> that I am using so that assumptions are taken into account.

Not sure where you read that, the specification and assumptions given
with __VERIFIER_assume are not related.

> So, I look in the ./config/specification/ directory and there's a
> few with promising names. So I try the following:
>
> $ ./scripts/cpa.sh -preprocess -config
> ./config/predicateAnalysis-slicing.properties -spec
> ./config/specification/Assertion.spc ~/Desktop/mem_zero_fill.c
> -setprop cfa.assumeFunctions={"__VERIFIER_assume"}
>
> and now the verification result is TRUE. Great. But now I'm not
> really sure what precisely it is that I have verified as correct!
> So I try to sanity check the testbench, by flipping the "less than"
> to a "greater than" in the __VERIFIER_assume() above. Running
> CPAChecker again, the verification result is still TRUE.

Assertion.spc (btw., you can shorten this to "-spec Assertion") tells
CPAchecker to look for assertions, but there are none in your program,
so the result will always be TRUE.

> 1. How does a newcomer actually learn to use CPAChecker
> effectively? Other tools we are already using/evaluating like CBMC,
> Frama-C and so on seem to have a fairly structured path to take a
> newcomer from knowing nothing about the tool to using it fairly
> productively. After searching, I have not found any tutorial
> material on CPAChecker, however. Is there any? If not, what is
> the best way of actually learning to use the tool and understand
> what all the settings do barring sitting down with an
> already-expert user?

We are planning on writing a longer tutorial, but we do not have it
currently, so we have only the short one in README.md.

Of course you are always welcome to ask on this list.

> 2. What is an AB-mixed term and why is -predicateAbstraction
> failing on my C code above?

Answered above.

> How can I look at my C code and predict that this will fail? I
> notice that a few other bundled *.properties files seem to fail for
> this reason (and some for various other reasons), and I'm wondering
> what is causing this and how we can structure our C to avoid
> problems like this.

Predicting this in general is hard, but one instance where this will
certainly appear is if quantifiers are necessary to verify a program,
as in your example.

> 3. What combination of specification and configuration do I need to
> use with CPAChecker to get it to check my testbench above?

The easy part is the choice of the specification.
You need to tell CPAchecker what it should consider a specification
violation.
As mentioned in the readme, the default specification will let
CPAchecker look for reachability of labels named "ERROR" and assertion
violations.
As mentioned above (and in the file itself), the file Assertion.spc
will let CPAchecker look only for assertion violations.
Another commonly used used specification is
"-spec sv-comp-reachability", which will let CPAchecker look for
reachability of calls to the function __VERIFIER_error.

In your example, you have both a label named ERROR and a call to
__VERIFIER_error in the same place, so both the default specification
as well as sv-comp-reachability will have the correct (desired) effect.


The choice of the configuration is more difficult.
In general, our default configuration "-default" or
"-predicateAnalysis" are the best that we have. "-default" even
consists of a selection of individual analyses actually and attempts
to use the best one for the current task.
Of course, not for all tasks these configurations are optimal,
but finding a better one can be difficult and in general requires a
lot of knowledge about the individual configurations.
So the best thing to do in case none of these configurations work
would indeed be do ask on the mailing list like you did.


For your specific example, I do not know any configuration of
CPAchecker that would be able to verify it without manual help.

> 4. What is predicateAbstraction-slicing.properties and
> Assertion.spc actually checking above, and why is it returning the
> same verification result even if the assumption is flipped?

Answered above: they check only for assertion violations, of which
none are present.

> Moreover, how do I convince myself from looking at a .properties
> and a .spc file that CPAChecker is correctly checking the property
> that I am interested in?

This is actually an open research question on which we are working,
so we do not have a full answer yet.

If you are using -predicateAnalysis, some information can be gained
from looking at output/predmap.txt: it contains all the facts that
CPAchecker needed to reason about while verifying the task.
If it is empty or contains only trivial facts, then either the task
was pretty easy (e.g., no loops) or you might have used a wrong
specification.
If you want to make sure that CPAchecker has indeed detected your
"target code" as reachable (and there is no problem like a forgotten
call from the main function, for example), you can generate a coverage
report (like for test coverage) by using the command from the readme:
genhtml output/coverage.info --output-directory output --legend

If you are still unsure, inverting the assertion and checking again is
also a good idea, but of course this can still give the same result if
e.g. the whole code part is unreachable.

> Other tools like CBMC have a much smaller configuration space and
> therefore it is easier for a user (and other engineers) to be
> convinced that relevant properties are indeed being checked.
> However, with CPAchecker the configuration space appears to be so
> huge that it's easy to silently check the wrong thing. Is there
> any suggested guidance here?

Note that CPAchecker is a framework that incorporates a whole range of
analyses. For example, what CBMC does corresponds more or less to one
configuration of CPAchecker (named "-bmc").
And this bounded model checking will not be able to verify the given
program, too, because in general it can't verify unbounded loops.

Greetings, Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQIcBAEBCAAGBQJbZC0tAAoJEGLA94wxqd6MxfAQAJjnWWth1RWiFv2MZrwpi6Xy
grmHaUX6d4zReGFvxstUg1ZAyHE6K5U0Z3040EV7JO5u2QayUFJ3e2dPpigrYmqd
JHn1eAaqYFxJ3fIvj1476GjhIC+3SWkL8niAitib5U4UDiCMBrm/35Ek8tIiHS48
r7Q4qxa/AXr4rut1YHDEIxn3NhiW4Le98Xa5vFKbx6MIDbgQoHD1a/i63gKfsDCX
kXwBh98ForU8lzYzpgRkHv/M8SqN/Nwg/SsisHtgXMQ3eLv2kf+fS30SzceciC+S
9Y1A+RLOw0ArIi8HFRvES6Z6nZ8A5ltdihZJg3VWiW3QLFpxQZ6ru+pcz2hl3ykS
5lF9JOaiyZ9ko7oEaCbYwU4e+yR9d1OCO5OD5d6kzP0jEAxYRwwC0XcmsRYoYCnb
TRdl8Wngx2ChXYXMMxLENtiR9QACewIkefbgrbvGQ268shbRP0BbbEVaiS8dvdps
aFZX6wtl+PRaSB6f9Y4DnpgWfyLNePrX7ClJqRVyP1EHRSeo3ovNkMJ7juN9cqTt
fa+I0zGktSJa3iPshPWvUnbvYjm3FcgnwZsd1LENi9kUI9Uap9z4T6Ga5FBZot/t
6aRTYVEk9KV8wiHI7hBdTKhh0GWJDiWanD/fifoOykQu1phjB/IM+dNbDtrpb/h4
ayjfx2ni9ZWI1aAi4oi3
=8juE
-----END PGP SIGNATURE-----

[Dominic Mulligan]

Dear Philipp,

Many thanks for your detailed reply.

> In the attached file you have inverted the condition in the assume.
> I can confirm this only if I revert the assumption to "idx < size"
> (which is also the correct way of writing this assumption).

Yes, this was just me sending the wrong version of the file.

> This means that the SMT solver which this analysis relies on failed.
> The message about AB-mixed terms is produced directly by the SMT solver.
> The underlying cause here is that the required reasoning about arrays
> and quantifiers is too hard for the SMT solver.
> I tried with the other SMT solvers that CPAchecker can use, but none
> of these can solve the required queries.
>
> Unfortunately, such queries about quantifiers and arrays are often too
> hard for any SMT solver that we know of, so while CPAchecker's
> predicate analysis could verify this program in theory, it can't in
> practice.
> We are working on finding alternative strategies that require less
> from the SMT solver, but this is ongoing research.

I see, thanks.

> There are also ways to work around this by manually supplying some
> helpful predicates, but as I guess you are interested in an automatic
> solution, I won't go into more detail here.

An automatic solution would be our ideal, but we are not completely
ruling out manual intervention (even evaluating Coq and Isabelle).
What predicates need to be supplied, how can you do this, and how can
you infer which ones are missing?

> Assertion.spc (btw., you can shorten this to "-spec Assertion") tells
> CPAchecker to look for assertions, but there are none in your program,
> so the result will always be TRUE.

I'm not sure how to understand this. To me, __VERIFIER_assert() is an
assertion. Do you mean it looks for assertions from assert.h from the
C standard library, or something else?

> Note that CPAchecker is a framework that incorporates a whole range of
> analyses. For example, what CBMC does corresponds more or less to one
> configuration of CPAchecker (named "-bmc").
> And this bounded model checking will not be able to verify the given
> program, too, because in general it can't verify unbounded loops.

Yes, of course. We at present either make "clever" use of CBMC's
uninterpreted functions where it allows us to provide an unbounded
verification or only provide a bounded verification of our code
otherwise. CPAchecker's potential for providing an unbounded
verification, and thereby allow us to either strengthen or simplify
our current approach, is what motivated us to give the tool a try.

Out of interest, is there support in CPAchecker for uninterpreted
functions, as in CBMC? Even if we can only replay what we are
currently doing in CBMC with CPAchecker there is still some merit for
us in not having to rely on/trust a single tool.

Thanks,
Dominic

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Hello Dominic,

Am 07.08.2018 um 17:01 schrieb 'Dominic Mulligan' via CPAchecker Users:

>> There are also ways to work around this by manually supplying
>> some helpful predicates, but as I guess you are interested in an
>> automatic solution, I won't go into more detail here.
>
> An automatic solution would be our ideal, but we are not
> completely ruling out manual intervention (even evaluating Coq and
> Isabelle). What predicates need to be supplied, how can you do
> this, and how can you infer which ones are missing?

I do not have any experience in supplying manual predicates myself,
so I can't really tell you which predicates would be necessary here.
Probably these predicates would need to contain quantifiers, though,
so I am not sure how well the SMT solvers would handle them.

Supplying predicates would be done by writing them in an SMT-LIB-like
format and specifying the file as additional input.

Because we never worked in this direction, there is also currently no
help in inferring which ones are missing, but in general you would
need to supply loop invariants, or building blocks for loop invariants.

>> Assertion.spc (btw., you can shorten this to "-spec Assertion")
>> tells CPAchecker to look for assertions, but there are none in
>> your program, so the result will always be TRUE.
>
> I'm not sure how to understand this. To me, __VERIFIER_assert() is
> an assertion. Do you mean it looks for assertions from assert.h
> from the C standard library, or something else?

__VERIFIER_assert is just a function that you named and declared,
CPAchecker cannot know that you consider this function as a way of
specifying assertions (CPAchecker doesn't try to guess semantics of
functions from their names, except when semantics are defined in a
standards document).

So when we say "assertion", we refer to assert() from assert.h.

> Out of interest, is there support in CPAchecker for uninterpreted
> functions, as in CBMC? Even if we can only replay what we are
> currently doing in CBMC with CPAchecker there is still some merit
> for us in not having to rely on/trust a single tool.

Sure.
By default, CPAchecker assumes that all functions for which no body is
present are "pure", i.e., return the same output if called again with
the same inputs. This will also be visible in CPAchecker's output.
If you want to define that functions have non-deterministic return
values, list them in the following configuration option:

- -setprop cpa.predicate.nondetFunctions=sscanf,random,...

Both kinds of functions are assumed to have no further side effects,
i.e., not modifying any values reachable via pointer parameters.

Greetings, Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQIcBAEBCAAGBQJba/9nAAoJEGLA94wxqd6MU2sP/30Aqjb0xqzGcyf+Pgw7MmeI
3rmfVht9UpgxCvym6e2DMW24E8TCdWPY8MmWuR3S380jwQlnaVqT8msJKMGCs509
i8NIvCzuEnGi0D40W2iZ1N86FonV4eFuCHn1o5YeH50f7p8iCT9CySBsBJ9dTw9c
y/Z5hC+VasV9wgpUl/NpJKAD2jYuMaz8hUPIs9T0ovvYTxdyZNLCNOObCNOZ2+Jf
3Ki7JxMs158upgtQrY6x2BoVX9AwG618yqAeXHFAv35WD2pH0NPipvCRn6ziksGF
J37FptNN4j+YCPZZrk+rgXh635rDqmmU9ottsjpimlHKVeX9sg09xliJvG9y2u23
emuKCq2eBEfTaK+gRxyV9tLS1WGXEJW8S6px6t4H0VtF8QwsESgjAlRc9hKJVxdW
0Ly8fS+gMVlIqFOZFZRKsB1qRIStHw/iUuVIzmVGG5bsoENl7hOYlaZEdivd7i26
JXtueJsGgBFIodLuNcMotjCz2Jh9gfzBCEg85eVy5+NSaNjvPqXZ2Ze2rvZ3tXcW
Pug8ZPj07OaWyTvx0WZfmZXvu9B5gzxRZsvRa/ZzUNLAlfn3OPdpPx9keeSzy+H/
qIpHbLfhBx3wHXJfEd/mXlQjtwa7gWST7RHRwDRDkAmTnpQseZ5yEjnVnTENtwy7
UNLJIua5Pia1XZuEM3/y
=C3ST
-----END PGP SIGNATURE-----