AV Property (AVP) Language

AV supports a language AVP (Angelic Verification Property language) for users to provide specifications that get checked with the AV toolchain. Such a property can be specified in a filename with .avp extension.

We will informally sketch the AVP language here. A formal description will follow soon!

Structure of an AVP file

At a high-level, a property file allows to define a set of Boogie to Boogie source transformations on a given input Boogie (.bpl extension) file. These rules are specified as a set of pattern matching rules on the Statements of a Boogie file and the corresponding instrumentation for any pattern matches.

We will use the following example as a running example https://github.com/boogie-org/corral/blob/master/AddOns/PropInst/PropInst/ExampleProperties/useafterfree-razzle.avp

An AVP file consists of four sections:

Global Declarations

GlobalDeclarations
{
    //(Global) Variable declarations 
    var validFree : [int] bool;

    //Procedure declarations 
    procedure  freedNondetFn() returns (r:bool);

    //Auxiliary Procedure definitions
    procedure {:corralExtraInitExtension} cEIE() {
       assume (forall x:int :: validFree[x]); 
    }
}

This section can be used to define well-formed Boogie declarations, definitions, axioms, constants, functions that are copied verbatim to the output instrumented file at the global level.

Template Variable Declarations

This section is used to declare template variables that are used to define the source code "patterns" in the input Boogie file. The template variables will be matched against expressions, procedures of the same "type".

TemplateVariables
{
    // Matches any expression of type int
    var p : int;

    // Matches any procedure that takes an int type as argument and returns a bool type
    procedure anyProc({:pointer} q : int) returns(r: bool);
}

Statement Instrumentation Rules

There can be a set of statement instrumentation rules that are enclosed within a CmdRule{lhsCmds} --> {rhsCmds} scope. Both lhsCmds and rhsCmds are a sequence of Boogie statements.

CmdRule
{
  // the sequence of statements to match
  assume {:nonnull} p != NULL;
}
-->
{
  // the replacement statements
  #this;
  assert (validFree[p] || p == 0); 
}

The commands left of the "-->" (lhsCmds) are the commands to match. These are matched to the same Boogie command in the instrumented program. The lhsCmds commands should be read as disjoined, i.e., if at least one of the statements in the sequence matches, the rule triggers. In case there is a match, the lhsCmds are replaced with rhsCmds after suitable substitutions.

If there are several matches (in the same rule or in different rules), the first match is taken, the rest are skipped.

A variable matches an variable with the same name, an NAryExpr matches an NAryExpr with the same function name and arguments that match, and so on. If the lhsCmds use a template variable, then such variables can match anything that has the same type (may be function type, map type, etc.).

The statement #this is interpreted specially. It will be replaced with the matched command as it appeared in the original boogie program. This is the only extension beyond legal Boogie statements supported in rhsCmds.

Procedure Definition Instrumentation Rules

There can be a set of procedure definition instrumentation rules that are enclosed within a ProcedureRule{procedureDecls} --> {rhsCmds} scope. Here procedureDecls is a sequence of procedure declarations and rhsCmds is a sequence of Boogie statements.

ProcedureRule
{
    procedure {:#ReplaceImplementation}  {:#NoImplementation} ExFreePool({:pointer} p : int);
}
-->
{
    validFree[p] := if (p == 0) then validFree[p] else false;
    call aliases(p);
    return;
}

Note that rhsCmds can insert entire procedure calls as statements. The definition of such procedures has to be defined/declared in the input Boogie file, or within the GlobalDeclarations.

For each of the procedure declarations in procDecls that match, the rhsCmds (after substitution) are inserted at the start of the procedure definition. If the definition of the procedure does not exist, it creates a definition with rhsCmds.

Note that the procedure declarations in lhsCmds are not template variables. We match procedures by their type and name (unless {:NameMatches regex} is used).

Attributes understood by AVP

Coming soon!