The exact mechanism of mapping WhyML into SMT logi

Question

Good day, auto deduction and verification hackers!

In order to gain a deeper understanding of how exactly WhyML provides proofs for ACSL-annotated C programs I am trying to manually "reproduce" the job Why3 does with WhyML program while translating it into SMT logic and feeding it into Z3 prover.

Lets say we have the following C fragment:

const int L = 3;
int a[L] = {0};
int i = 0;
while (i < L) {
  a[i] = i;
  i++;
}
assert (a[1] == 1);

I am trying to encode it into SMT logic like this:

(set-logic AUFNIRA)
(define-sort _array () (Array Int Int))
(declare-const ar _array)
(declare-fun set_a_i (_array Int Int) _array)
(assert (forall ((ar0 _array) (i Int) (j Int)) 
    (ite (< i j)   
                 (= (set_a_i ar0 i j) 
                    (set_a_i (store ar0 i i) (+ i 1) j))
                 (= (set_a_i ar0 i i) ar0) ))) 

(assert (= (select (set_a_i ar 0 3) 1) 1))
(check-sat)

Z3 gives "unknown".

This is probably because of quantification used in specifing set_a_i function. But I see no other ways to specify it.

I am aware of the following statements:

• SMT solvers in general are not able to (or do it in a bad way) handle quantifications over arrays.
• WhyML is able to prove such programs if I supply pre & post condition and loop invariant.
• WhyML is able to prove such programs even when backend is set to Z3, so SMT solver itself is not an issue.
• WhyML can produce z3 smt file, but to understand it is a great toil partly because of the automatic nature of whyML->smt translation (it doest not preserve variable names for example)

I read nearly all supplied materials for WhyML, Frama-C WP plugin and Z3. I also read several papers on verifing C code but found nothing regarding C --> SMT translation techniques.

Which materials should I study to gain this understanding? Could you please provide insights and/or links to papers describing this machinery of translating imperative code into multi-sorted first order logic.

I will appreciate any comments. Thanks!

Good luck, Evgeniy.

Answer 1

The WP 0.8 plugin manual and the paper "Why3: Shepherd Your Herd of Provers" provide a high-level overview of how annotated C code is transformed into Why logic, and how the Why logic is then transformed into the input logic of a theorem prover.

As described in section 1.3 of the WP plugin manual, start by considering Hoare's triples:

{P} stmt {Q}

which is read: whenever preconditions P hold, then after running stmt, the postconditions Q hold. The WP plugin considers the weakest precondition as a function over stmt and the postconditions such that the following Hoare triple holds:

{wp(stmt, Q)} stmt {Q}

The weakest precondition is, in a sense, the simplest property that must hold before the execution of stmt such that Q holds after the execution of stmt.

As an example, consider the case where stmt is x = x + 1 and {Q} is {x > 0}. By the assignment rule of Hoare calculus, we know that {x + 1 > 0} x = x + 1 {x > 0} holds. {x + 1 > 0} is, in fact, the weakest precondition of x = x + 1 and {x > 0}.

More generally, it is possible to determine the weakest precondition for any statement and any postcondition.

Now suppose that you have a function f annotated with preconditions P and postconditions Q:

{P} f {Q}

Define W = wp(f, Q). We know by definition of wp that the following Hoare triple holds:

{W} f {Q}

If we are able to prove that P ⇒ W (this is what is submitted to the theorem prover), then the validity of properties P and Q for f is established.

The WP plugin generates Why logic. As described in section 4 of the "Why3: Shepherd Your Herd of Provers" paper, the operation of Why3 is described as processing proof tasks, which are a sequence of declarations ending with a goal. This is how the Why logic is converted to the input logic of a particular theorem prover.

For a concrete example, the paper gives an overview of transforming Why logic to Z3. Not only is the input language different (Z3 uses SMT-LIB2 syntax), there are significant differences in the logic of Why and Z3. The paper gives the examples that Z3 does not support polymorphism or inductive predicates.

In order to transform Why logic into the input logic of a theorem prover, Why3 uses a series of transformations that gradually transform the Why logic into the target input logic. Why3 uses configuration files known as drivers to define all of the transformations, a pretty printer which outputs the prover's native input format, and regular expressions for interpreting the output of the prover.

Assuming you have run why3config, you can take a look at the automatically-generated .why3.conf config file in your home directory to determine which driver Why3 uses for a particular prover. For example, on my system Why3 uses ~/.opam/system/share/why3/drivers/z3_432.drv when using Z3. z3_432.drv imports the smt-libv2.drv driver as a base driver for SMT-LIB2-compatible provers.

I know that you are aware of examining the generated SMT2, but I figured that I would mention how to do this for anyone who is interested. If you pass the -wp-out DIR and -wp-proof-trace options to frama-c, then WP will save the output from running the prover on individual properties. You can then locate the corresponding .err file for the property of interest. In my case, it's main_assert_final_a_Why3_z3.err. Opening that file in a text editor, you will see something like:

Call_provers: command is: /Users/dtrebbien/.opam/system/lib/why3/why3-cpulimit
  10 1000 -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false
  smt.random_seed=42
  /var/folders/1v/2nkqhkgx0qnfwd75h0p3fcsc0000gn/T/why_9f8a52_main_Why3_ide-T-WP.smt2

This .smt2 file contains the SMT-LIB2 input to Z3 that Why3 generated.

You can run the command if you would like. In my case, I see:

WARNING: pattern does contain any variable.
WARNING: pattern does contain any variable.
WARNING: pattern does contain any variable.
WARNING: pattern does contain any variable.
unsat
why3cpulimit time : 0.020000 s

Although slightly counterintuitive, unsat means that the validity of the property is established.