Verify Programs with Contracts

The CIVL contract system is based on ACSL (​http://frama-c.com/acsl.html), and it contains four categories:

• Contracts for sequential programs
• Contracts for MPI
• Contracts for state space reduction (see ContractReduction)
• Loop invariants

Note that the first three are also called function contracts, while the last is called loop contract.

Additional primitives that extend ACSL include:

• contract primitives for MPI
  • MPI collective contract
  • remote expressions
• contract primitives for dependency relation
  • depends clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis
  • \calls(fun, arg0, arg1, ...): a set of actions that invokes the function with the specified arguments
  • \noact: empty set of actions
  • \anyact: any action sets
  • set of memory actions: \read(mu-list), \write(mu-list)
  • action set operations: + union, - complement, & intersect
  • reads clause: specify memory locations read by the function, the syntax of which is similar to assigns clause
• malicious primitives
  • wildcard term: ...
• additional parameter for allocates clause: specify the scope of the heap for allocation; if absent then the root scope is used
• extension for range with steps: lo .. hi # step

The contract grammar could be found bellow:

function-contract ::= requires-clause∗ terminates-clause? decreases-clause? guards-clause?
                      simple-clause∗  named-behavior∗ completeness-clause∗ 
requires-clause ::= requires pred ;
terminates-clause ::= terminates pred ;
decreases-clause  ::= decreases term (for id)? ;
guards-clause ::= guards pred ;
simple-clause ::= assigns-clause | ensures-clause 
                | allocation-clause | abrupt-clause-fn
                | reads-clause | depends-clause
assigns-clause ::= assigns tsets ;
tsets ::= location (, location) ∗
ensures-clause ::= ensures pred ;
allocation-clause ::= allocates tsets (, scope)? ; | frees tsets ;
reads-clause ::= reads tsets;
depends-clause := depends event (, event)*;
named-behavior ::= behavior id : behavior-body
behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗
assumes-clause ::= assumes pred ;
completeness-clause ::= complete behaviors (id (, id)∗)? ;
                      | disjoint behaviors (id (, id)∗)? ;
term ::= \old ( term ) | \result | \nothing | ...
pred ::= \old ( pred )

tset ::= \empty
       | tset -> id 
       | tset . id * tset
       | & tset
       | tset [ tset ]
       | term? .. term?
       | \union ( tset (, tset)∗ )
       | \inter ( tset (, tset)∗ )
       | tset + tset
       | ( tset )
       | { tset | binders (; pred)? }
       | { term } term

literal ::= \true | \false | integer | real | string | character

bin-op ::= + | - | * | / | % | << | >>
         | == | != | <= | >= | > | <
         | && | || | ^^
         | & | | | --> | <--> | ^

unary-op ::= + | - | ! | ~ | * | & 

term ::= literal | id | unary-op term | term bin-op term | term [ term ]
       | { term \with [ term ] = term } 
       | term . id
       | {term \with.id =term }
       | term -> id
       | ( type-expr ) term
       | id ( term (, term)∗ )
       | (term)
       | term ? term : term
       | \let id = term ; term sizeof ( term )
       | sizeof ( C-type-name )
       | id : term 
       | string : term

Contracts for Sequential Programs

Sequential contracts are based on the theory of Hoare Logic. Contracts only state sequential properties on either the pre-state or post-state of the given procedure. All sequential contract constructors are inherited from ACLS, CIVL will start from supporting part of them.

MPI contracts

MPI contracts are contracts stating specific properties of MPI programs. Since there is much difference between sequential and concurrent programs, checking and reasoning MPI programs requires a unique system. Obviously the two states (pre- and post-) system is not suitable for concurrent programs.

Notations of MPI contracts

MPI-Collective-Block

Collective-signature ::= "\mpi_collective(MPI_Comm, COLLECTIVE_KIND)";
Collective-body ::= (ACSL-clause)* ;
Collective-block ::= Collective-signature : Collective-body;

MPI-Empty-In && MPI-Empty-Out expressions

Pointers & Alias

Pointers can be asserted as valid pointers via using ACSL constructor \valid. ACSL allows programmers specify a set of valid pointers which requires CIVL to be able to represent a set.

CIVL has a typing rule: pointer PLUS CIVL_Range ==> An array of pointers . Other sets of different types may have the similar typing rule.

For CIVL, coping with a \valid expression is tricky. For \valid expressions appear in assurances, one can implement the evaluation semantics on a specific state. However, \valid appears in requirements brings problems, it heavily affects how CIVL constructs an initial state.

For example:

/*@ requires (\valid(p) || !\valid(p) ) && \valid(q);
*/
foo(int * p, int * q);

The construction of an initial state seems to be irrelevant to if the pointer p is valid or not, but when CIVL recursively analyzes the requirement predicate, it's hard to know if it's relevant or not. Thus my rough solution is :

1. Making \valid expressions uninterpreted functions;
2. Pointer "p" should be valid initially only if requirement => valid_of_p ;
3. Vice versa, pointer "p" should be undefined initially only if requirement => !valid_of_p ;
4. Otherwise, it's a non-deterministic choice.

Considering pointer alias, I'm planning such an approach:

First, there is an outer scope outside of the source function which is going to be verified. It can be used to represent a set of all visible scopes from the source function. Thus, for each pointer argument, creating a unique unconstraint array element in the outer scope.

$input int X[2];  // one for each pointer

/*@ requires \valid(p) && \valid(q);
*/
foo(int *p, int *q);

For this example, considering aliasing, the context can be

( ( \valid(p) && \valid(q) ) => \valid(p) ) => (exists i, 0 <= i < 2 such that *p == X[i] );