The contracts specification of CIVL-C is based on ACSL, with additional primitives and constructs for various purposes, such as function guard, function dependency, MPI function behavior, etc.

overview

The grammar for the contract specification of a function is as follows:

contract: requires* terminates? decreases? simple* behavior* completeness* ;
requires: 'requires' e ';' ;
...
simple: ensures | assumes | assigns | reads | guards | depends | ... ;
ensures: 'ensures' e ';' ;
assumes: 'assumes' e ';' ;
assigns: 'assigns' e (',' e)* ';' ;
reads: 'reads' e (',' e)* ';' ;
depends: 'depends' e (',' e)* ';' ;
...
behavior: 'begin behavior' id ':' behaviorBody 'end behavior';
behaviorBody: behaviorClause+;
behaviorClause: assumes | requires | simple ;
completeness: 'complete' (id (',' id)*)? 
            | 'disjoint' (id (',' id)*)? 
            ;

Example

fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
  reads deref(buf);
  begin behavior send:
    depends writes(buf);
    assigns nothing;
  end behavior
  begin behavior receive:
    depends access(deref(buf));
    assigns deref(buf);
  end behavior
{
  begin choose
  when eq(cmd, 0)
     do CALL send, <buf, ...>; goto L1;
  when eq(cmd, 1)
    do CALL recv, <buf, ...>; goto L1;
  when and(neq(cmd, 0), neq(cmd, 1))
    do NOOP; goto L1;
  end choose
L1:
}

contract clauses

• requires e;: precondition, e has Bool type and should hold at the entry of the function
• terminates e;: e has Bool type and if e holds then the function should terminate eventually
• decreases e ; or decreases e for r;: decreases clause, where e is an expression of type T and r is an relation over T
• simple clauses:
  • ensures e;: postcondition, e has Bool type and should hold when the function terminates
  • assumes e;: assumption, e has Bool type
  • assigns e0, e1, ...;: side-effects, e0, e1, ... have Mem type
    • absence of Assigns clause does NOT mean that the function has no side-effects
    • assigns nothing: means that the function has no side-effects
  • allocates e0, e1, ...;: memory units allocated by the function, e0, e1, ... have Mem type
  • frees e0, e1, ...;: memory units deallocated by the function, e0, e1, ... have Mem type
  • guards e;: guard of the function, where e has Bool type
  • reads e0, e1, ...;: memory access, where e0, e1, ... have Mem type
    • similar to assigns
    • absence of Reads clause does NOT mean that the function does NOT read anything
    • reads nothing: means that the function does NOT read the memory
  • depends e0, e1, ...;: dependency relation, where e0, e1, ... have Mem type
  • Note: guards, depends and reads are CIVL extension for ACSL
• named behavior:
  • begin behavior id : c0; c1; c2; ... end behavior, where id is the name of this behavior, c0, c1, c2, ... are behavior clauses
  • behavior clause: a clause that can be used in the body of a behavior, and could be one of the following:
    • assumes clause
    • requires clause
    • simple clause
• completeness clause
  • complete; or complete (id0, id1, ...);:
  • disjoint; or disjoint (id0, id1, ...);

depends clause and actions

• action expressions:
  • read(e): e has type Mem. The function reads the memory units specified by e.
  • write(e): e has type Mem. The function writes the memory units specified by e.
  • call(f, <e1, ...>): f has type Function. The function calls f with parameters e1, ....
  • noaction: no action
  • anyaction: all actions
  • act_union(ma0, ma1): the union of the two memory set actions ma0 and ma1.
  • act_comp(ma0, ma1): action complement (everything not in ma1)
  • act_isect(ma0, ma1): action intersection

• depends clause: depends action0, action1, action2, ...
  • Example: depends act_union(act_comp(read(n), call(inc, <x>))), call(dec, <y>))
  • absence of depends clause: there is no information about the dependency of the function, which means that the analysis needs to figure it out by itself.
• some facts about assigns-or-reads clause
  • absence of reads/assigns clause: there is no assumption about the read/assign access of the function, i.e., the function could read/assign anything
    • absence of assigns clause: similar to the absence of reads clause
  • reads/assigns nothing doesn’t necessarily means that the function never reads or assigns any variable. The function could still reads/assigns its “local” variables, including function parameters and any variable declared inside the function body. check it

• For an independent function which has depends coaction, usually we also need to specify reads nothing, for the purpose of reachability analysis.

e.g.,

/* Returns the size of the given bundle b. */
bundle_size(Bundle b): Integer
  depends nothing
  reads b
  ;

• Example of a function declaration with contracts:

  fun[atomic] sendRecv(Int cmd, Pointer buf): Integer
    reads deref(buf);
    begin behavior send:
      depends writes(buf);
      assigns nothing;
    end behavior
    begin behavior receive:
      depends access(deref(buf));
      assigns deref(buf);
    end behavior
  {
    begin choose
    when eq(cmd, 0)
       do CALL send, <buf, ...>; goto L1;
    when eq(cmd, 1)
      do CALL recv, <buf, ...>; goto L1;
    when and(neq(cmd, 0), neq(cmd, 1))
      do NOOP; goto L1;
    end choose
  L1:
  }