wyil.builders

Class VerificationConditionGenerator

java.lang.Object

wyil.builders.VerificationConditionGenerator

public class VerificationConditionGenerator
extends Object

Responsible for generating verification conditions from a given WyIL file. A verification condition is a logical condition which must be shown to hold in order for the underlying WyIL program to considered "correct". The Verification Condition Generator (VCG) examines in turn each function or method in a given WyIL file. The VCG traverses each control-flow graph emitting verification conditions as it discovers them. The following illustrates:

 function abs(int x) -> (int r)
 ensures r >= 0:
     //
     if x >= 0:
        return x
     else:
        return -x
 

The above function can be viewed in a slightly more precise fashion as follows, where the block structure is indicated:

 +-----------------------------+ (1)
 |function abs(int x) -> (int r)
 |ensures r >= 0:
 |  +--------------------------+ (2)
 |  |  //
 |  |  if x >= 0:
 |  |   +----------------------+ (3)
 |  |   | return x
 |  |   +----------------------+
 |  |  else:
 |  |   +----------------------+ (4)
 |  |   | return -x
 |  |   +----------------------+
 |  +--------------------------+
 +-----------------------------+
 

The VCG will generate exactly two verification conditions from this function corresponding to the paths "1,2,3" and "1,2,4". These verification conditions are required to ensure that, given the information know at the point of each return, we can establish the post-condition holds. The two verification conditions are:

• 1,2,3: x >= 0 ==> x >= 0. This verification corresponds to the case where the if condition is known to be true.
• 1,2,4: x < 0 ==> -x >= 0. This verification corresponds to the case where the if condition is known to be false.

The VCG attempts to generate verification conditions which are easier to read by making use of macros as much as possible. For example, each clause of a function/method's precondition or postcondition is turned into a distinct (named) macro.

Author:

David J. Pearce

Constructor Summary

Constructors

Constructor and Description
VerificationConditionGenerator(wyal.lang.WyalFile wyalFile, Wyil2WyalBuilder builder)

Method Summary

Modifier and Type	Method and Description
wyal.lang.WyalFile.Stmt.Block	buildVerificationCondition(WyilFile.FunctionOrMethod declaration, wyil.builders.VerificationConditionGenerator.GlobalEnvironment environment, wyil.builders.VerificationConditionGenerator.VerificationCondition vc) Construct a fully typed and quantified expression for representing a verification condition.
static int[]	flattern(int[][] groups)
void	freeVariables(wyal.lang.SyntacticItem e, Set<wyal.lang.WyalFile.VariableDeclaration> freeVars) Determine all free variables which are used within the given expression.
SyntaxTree.Location<Bytecode.VariableDeclaration>	getVariableDeclaration(SyntaxTree.Location<?> decl)
wyal.lang.WyalFile.Expr	invertCondition(wyal.lang.WyalFile.Expr expr, SyntaxTree.Location<?> elem) Generate the logically inverted expression corresponding to a given comparator.
wyal.lang.WyalFile.Expr[]	invertConditions(wyal.lang.WyalFile.Expr[] expr, SyntaxTree.Location<?> elem)
WyilFile.FunctionOrMethodOrProperty	lookupFunctionOrMethodOrProperty(wybs.lang.NameID name, Type.FunctionOrMethod fun, SyntaxTree.Location<?> stmt) Lookup a given function or method.
wyal.lang.WyalFile	translate(WyilFile wyilFile) Translate a WyilFile into a WyalFile which contains the verification conditions necessary to establish that all functions and methods in the WyilFile meet their specifications, and that no array-out-of-bounds or division-by-zero exceptions are possible (amongst other things).

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

VerificationConditionGenerator

public VerificationConditionGenerator(wyal.lang.WyalFile wyalFile,
                                      Wyil2WyalBuilder builder)

Method Detail

translate

public wyal.lang.WyalFile translate(WyilFile wyilFile)

Translate a WyilFile into a WyalFile which contains the verification conditions necessary to establish that all functions and methods in the WyilFile meet their specifications, and that no array-out-of-bounds or division-by-zero exceptions are possible (amongst other things).

Parameters:

wyilFile - The input file to be translated

Returns:

buildVerificationCondition

public wyal.lang.WyalFile.Stmt.Block buildVerificationCondition(WyilFile.FunctionOrMethod declaration,
                                                                wyil.builders.VerificationConditionGenerator.GlobalEnvironment environment,
                                                                wyil.builders.VerificationConditionGenerator.VerificationCondition vc)

Construct a fully typed and quantified expression for representing a verification condition. Aside from flattening the various components, it must also determine appropriate variable types, including those for aliased variables.

Parameters:

vc -

environment -

Returns:

freeVariables

public void freeVariables(wyal.lang.SyntacticItem e,
                          Set<wyal.lang.WyalFile.VariableDeclaration> freeVars)

Determine all free variables which are used within the given expression. A free variable is one which is not bound within the expression itself.

Parameters:

e -

freeVars -

lookupFunctionOrMethodOrProperty

public WyilFile.FunctionOrMethodOrProperty lookupFunctionOrMethodOrProperty(wybs.lang.NameID name,
                                                                            Type.FunctionOrMethod fun,
                                                                            SyntaxTree.Location<?> stmt)
                                                                     throws Exception

Lookup a given function or method. This maybe contained in the same file, or in a different file. This may require loading that file in memory to access this information.

Parameters:

name - --- Fully qualified name of function

fun - --- Type of fucntion.

block - --- Enclosing block (for debugging purposes).

branch - --- Enclosing branch (for debugging purposes).

Returns:

Throws:

Exception

invertCondition

public wyal.lang.WyalFile.Expr invertCondition(wyal.lang.WyalFile.Expr expr,
                                               SyntaxTree.Location<?> elem)

Generate the logically inverted expression corresponding to a given comparator. For example, inverting "<=" gives ">", inverting "==" gives "!=", etc.

Parameters:

test - --- the binary comparator being inverted.

Returns:

invertConditions

public wyal.lang.WyalFile.Expr[] invertConditions(wyal.lang.WyalFile.Expr[] expr,
                                                  SyntaxTree.Location<?> elem)

flattern

public static int[] flattern(int[][] groups)

getVariableDeclaration

public SyntaxTree.Location<Bytecode.VariableDeclaration> getVariableDeclaration(SyntaxTree.Location<?> decl)