How to know which parts of an ACSL predicate are failing?

Question

I have an ACSL predicate that is ~37 lines long (the predicate returns whether the passed struct is in a valid state). It is a series of conditions &&'d together.

When I assert the predicate:

//@ assert MyPredicate(myArg);

and the verification fails, I do not know which of the &&'d conditions is failing.

How can I know which part(s) of the predicate are failing?

When there is a verification failure, I open the C file with frama-c-gui -wp -wp-rte myfile.c. I more often run frama-c with the same args, but I use the GUI to help investigate failures.

$ frama-c-gui --version
24.0 (Chromium)

If the predicate was never going to change, I might be fine manually breaking it out into separate /*@ assert ... */ sections, but I am regularly updating the predicate as I work on the program, and would prefer not to keep the predicate and the block of asserts in sync.

If the prover versions are relevant:

$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
Found prover Z3 version 4.8.9 (alternative: counterexamples)
Found prover Z3 version 4.8.9, OK.
Found prover Z3 version 4.8.9 (alternative: noBV)
4 prover(s) added

I separated the conditions of the predicate into a series of asserts. I learned that even when the predicate can be verified, the same conditions as individual asserts can fail at the same point of the program. This is discouraging. — Costava, Sep 18 '22 at 19:42

Ksass'Peuk · Accepted Answer · 2022-09-19T15:03:31.407

There are very different ways of proving a predicate, and sometimes, the problem is not that a subpart of the predicate cannot be proved. That explain for example why you can sometimes prove the predicate without being able to prove the separate elements of the conjunction. For example, if you have something like:

/*@
  predicate P(integer a) = R(a) && Q(a) && ...
  lemma l{L1, L2}: \forall a ; P{L1}(a) ==> Z{L1, L2}(a) ==> P{L2}(a) ;
*/

//@ requires P(a);
void foo(int a){
  ...
  //@ assert Z{Pre,Here}(a);
  //@ assert P(a);
}

Proving P(a) is direct thanks to the lemma. Proving the separate elements of P(a) at least requires to unfold the definition (and if you have several levels of unfolding to perform, this might fail). SMT solvers are not all good at unfolding definitions. From my experience, CVC4 is a little better than Alt-Ergo and Z3 at this game, but no matter the SMT solver, there will always be a depth where no SMT solver will continue unfolding the definitions.

In such a situation, using lemma functions can help extract the part of the predicate that is interesting for you. For example :

/*@ ghost
  /@ requires P(a);
     assigns \nothing ;
     ensures R(a);
  @/
  void lemma_P_means_R(int a){}
*/

Once you have this function you can use it wherever you need to extract R from knowing P.

Now, assuming that you need to find the subpart of a predicate that fails during a proof. In the process of identifying which part of a predicate fails to prove, I would use the interactive theorem prover embedded in the WP GUI. Let us use the following code snippet as an example:

/*@ axiomatic Ax {
      predicate A ;
      predicate B ;
    }
    predicate AB = A && B ;
*/

int main(void){
  //@ assert AB ;
}

Once the assertion has failed, one can select the goal in the GUI, and then apply the definition tactic to unfold the goal:

Then, you can split the resulting goal:

That will result in two different sub-goals to prove:

Again, once you know which part is hard to prove and how to get them proved, adding the right assertions and lemma function call might help the proof. Otherwise, you can also save the resulting proof script to replay it later. (the name of the proved on the command line is script).

How to know which parts of an ACSL predicate are failing?

1 Answers1