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: 'Behavior' id ':' behaviorBody ;
behaviorBody: behaviorClause+;
behaviorClause: assumes | requires | simple ;
completeness: 'Complete' (id (',' id)*)? 
            | 'Disjoint' (id (',' id)*)? 
            ;

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

• 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);
    behavior send:
      depends writes(buf);
      assigns nothing;
    behavior receive:
      depends access(deref(buf));
      assigns deref(buf);
  {
    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:
  }