Verification Tools

The verifytools module provides supporting infrastructure for verification, including intermediate representations, verification condition generation, and integration with external tools.

Architecture

efmc/verifytools/
├── common/               # Common utilities and AST
│   ├── ast.py           # Abstract syntax tree definitions
│   ├── parser.py        # Common parser utilities
│   └── util.py          # Utility functions
├── boogie/              # Boogie-specific tooling
│   ├── ast.py           # Boogie AST
│   ├── bb.py            # Basic block analysis
│   ├── eval.py          # Expression evaluation
│   ├── grammar.py       # Boogie grammar
│   ├── interp.py        # Interpreter
│   ├── paths.py         # Path analysis
│   ├── predicate_transformers.py  # Predicate transformers
│   ├── ssa.py           # Static single assignment
│   ├── analysis.py      # Static analysis
│   ├── inv_networks.py  # Invariant networks
│   └── z3_embed.py      # Z3 embedding
├── tools/               # Verification tools
│   ├── vc_check.py      # Verification condition checking
│   ├── desugar.py       # Desugaring utilities
│   ├── tryAndVerify.py  # Try-and-verify strategy
│   ├── conversions.py   # Format conversions
│   ├── boogie_loops.py  # Loop extraction
│   ├── levels.py        # Level management
│   ├── run_ice.py       # ICE-based generation
│   ├── run_invgen.py    # Invariant generation runner
│   └── run_daikon.py    # Daikon integration
├── daikon/              # Daikon invariant detector
│   ├── inv_ast.py       # Invariant AST
│   └── inv_grammar.py   # Invariant grammar
├── cpachecker/          # CPAchecker integration
│   └── dummy.h          # Stub header
└── invgen/              # Invariant generation utilities

Common Utilities

The common subpackage provides shared utilities:

from aria.efmc.verifytools.common.ast import Expr, Stmt
from aria.efmc.verifytools.common.parser import parse_formula
from aria.efmc.verifytools.common.util import simplify

Common AST

Base classes for abstract syntax trees:

from aria.efmc.verifytools.common.ast import (
    Expr,      # Base expression class
    Stmt,      # Base statement class
    Var,       # Variable reference
    Const,     # Constant
    BinOp,     # Binary operation
    UnOp,      # Unary operation
)

# Create expressions
x = Var("x")
expr = BinOp("+", x, Const(1))

Common Parser

Utility functions for parsing formulas:

from aria.efmc.verifytools.common.parser import parse_formula

# Parse from string
formula = parse_formula("x + y > 0")

Boogie Frontend Tools

The boogie subpackage provides tools for working with Boogie programs:

AST and Interpretation

from aria.efmc.verifytools.boogie.ast import BoogieProgram, Procedure
from aria.efmc.verifytools.boogie.interp import BoogieInterpreter

# Parse Boogie program
program = BoogieProgram.from_file("program.bpl")

# Run interpreter
interp = BoogieInterpreter(program)
result = interp.run_procedure("main")

Basic Block Analysis

from aria.efmc.verifytools.boogie.bb import BasicBlockAnalyzer

analyzer = BasicBlockAnalyzer(program)
blocks = analyzer.get_basic_blocks("procedure_name")

Static Single Assignment (SSA)

from aria.efmc.verifytools.boogie.ssa import to_ssa

ssa_program = to_ssa(program)

Predicate Transformers

from aria.efmc.verifytools.boogie.predicate_transformers import (
    wp,  # Weakest precondition
    sp,  # Strongest postcondition
)

# Compute weakest precondition
wp_expr = wp(statement, postcondition)

Z3 Integration

from aria.efmc.verifytools.boogie.z3_embed import BoogieToZ3

converter = BoogieToZ3()
z3_expr = converter.convert(boogie_expr)

Verification Condition Generation

The tools subpackage provides verification condition generation:

Verification Condition Checking

from aria.efmc.verifytools.tools.vc_check import check_vc

result = check_vc(vc_formula, solver="z3")

Try-and-Verify Strategy

from aria.efmc.verifytools.tools.tryAndVerify import TryAndVerify

strategy = TryAndVerify(max_iterations=100)
result = strategy.verify(transition_system)

Desugaring

from aria.efmc.verifytools.tools.desugar import desugar_program

simplified = desugar_program(program)

Format Conversions

from aria.efmc.verifytools.tools.conversions import (
    chc_to_smtlib,
    smtlib_to_chc,
)

Daikon Integration

The daikon subpackage provides integration with the Daikon invariant detector:

from aria.efmc.verifytools.daikon.inv_grammar import InvGrammar
from aria.efmc.verifytools.daikon.inv_ast import Invariant

# Create invariant grammar
grammar = InvGrammar()

# Detect invariants from traces
invariants = grammar.detect(traces)

CPAchecker Integration

The cpachecker subpackage provides integration with CPAchecker:

from aria.efmc.verifytools.cpachecker import run_cpachecker

result = run_cpachecker(
    program="program.c",
    spec="safety.prp",
    timeout=300
)

ICE-based Invariant Generation

The ICE (Counterexample-Driven, Consistency, Efficiency) learning strategy:

from aria.efmc.verifytools.tools.run_ice import ICEGenerator

generator = ICEGenerator()
invariants = generator.learn(
    transition_system,
    max_samples=1000
)

API Reference

AST node base class and utility functions.

class aria.efmc.verifytools.common.ast.AstNode(*args)[source]

Bases: object

Base class for AST nodes with structural equality and hashing.

aria.efmc.verifytools.common.ast.reduce_nodes(node, cb)[source]: Reduce nodes using callback function cb.

aria.efmc.verifytools.common.ast.replace(ast, m)[source]: Replace AST nodes according to mapping m.

Parser base classes for expression parsing.

class aria.efmc.verifytools.common.parser.InfixExprParser[source]

Bases: Parser

Parser for infix expressions.

onAtom(prod, st, loc, toks)[source]: Handle atom production.

onLABinOp(prod, st, loc, toks)[source]: Handle left-associative binary operator production.

onNABinOp(prod, st, loc, toks)[source]: Handle non-associative binary operator production.

onRABinOp(prod, st, loc, toks)[source]: Handle right-associative binary operator production.

onUnaryOp(prod, st, loc, toks)[source]: Handle unary operator production.

class aria.efmc.verifytools.common.parser.Parser[source]

Bases: object

Base parser class.

Common utility functions.

aria.efmc.verifytools.common.util.average(vals)[source]: Calculate the average of a list of values.

aria.efmc.verifytools.common.util.error(*args)[source]: Print error message to stderr.

aria.efmc.verifytools.common.util.fatal(*args)[source]: Print error message and exit with error code.

aria.efmc.verifytools.common.util.flattenList(s)[source]: Flatten a list of lists into a single list.

aria.efmc.verifytools.common.util.flattenSet(s)[source]: Flatten a set of sets into a single set.

aria.efmc.verifytools.common.util.nodups(s)[source]: Remove duplicates from a sequence.

aria.efmc.verifytools.common.util.nonempty(lst)[source]: Filter out the empty elements of a list (where empty is len(x) == 0).

aria.efmc.verifytools.common.util.powerset(s)[source]: Return the powerset of a set s.

aria.efmc.verifytools.common.util.pp_exc(f)[source]: Wrap a function to catch, pretty print the exception and re-raise it.

aria.efmc.verifytools.common.util.randomToken(l)[source]: Generate a random alphanumeric token of length l.

aria.efmc.verifytools.common.util.split(pred, itr)[source]: Split a list based on a predicate function.

aria.efmc.verifytools.common.util.unique(iterable, msg='')[source]: Assert that iterable has one element and return it.

class aria.efmc.verifytools.boogie.ast.AstAssert(expr)[source]: Bases: AstOneExprStmt

class aria.efmc.verifytools.boogie.ast.AstAssignment(lhs, rhs)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstAssume(expr)[source]: Bases: AstOneExprStmt

class aria.efmc.verifytools.boogie.ast.AstBinExpr(lhs, op, rhs)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstBinding(names, typ)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstBlock(stmts)[source]: Bases: AstStmt

class aria.efmc.verifytools.boogie.ast.AstBody(bindings, stmts)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstBuilder[source]

Bases: BoogieParser

onAssert(prod, st, loc, toks)[source]

onAssignment(prod, st, loc, toks)[source]

onAssume(prod, st, loc, toks)[source]

onAtom(prod, st, loc, toks)[source]: Handle atom production.

onBlock(prod, st, loc, toks)[source]

onBody(prod, st, loc, toks)[source]

onGoto(prod, st, loc, toks)[source]

onHavoc(prod, st, loc, toks)[source]

onImplementationDecl(prod, st, loc, toks)[source]

onLABinOp(prod, st, loc, toks)[source]: Handle left-associative binary operator production.

onLabeledStatement(prod, st, loc, toks)[source]

onLocalVarDecl(prod, st, loc, toks)[source]

onNABinOp(prod, st, loc, toks)[source]: Handle non-associative binary operator production.

onProgram(prod, st, loc, toks)[source]

onRABinOp(prod, st, loc, toks)[source]: Handle right-associative binary operator production.

onReturn(prod, st, loc, toks)[source]

onType(prod, st, loc, toks)[source]

onUnaryOp(prod, st, loc, toks)[source]: Handle unary operator production.

onWhile(prod, st, loc, toks)[source]

class aria.efmc.verifytools.boogie.ast.AstFalse[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstFuncExpr(funcName, *ops)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstGoto(labels)[source]: Bases: AstStmt

class aria.efmc.verifytools.boogie.ast.AstHavoc(ids)[source]: Bases: AstStmt

class aria.efmc.verifytools.boogie.ast.AstId(name)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstImplementation(name, signature, body)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstIntType[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstLabel(label, stmt)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstNumber(num)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstOneExprStmt(expr)[source]: Bases: AstStmt

class aria.efmc.verifytools.boogie.ast.AstProgram(decls)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstReturn[source]: Bases: AstStmt

class aria.efmc.verifytools.boogie.ast.AstStmt(*args)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstTrue[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstUnExpr(op, expr)[source]: Bases: AstNode

class aria.efmc.verifytools.boogie.ast.AstWhile(condition, invariants, body)[source]: Bases: AstStmt

aria.efmc.verifytools.boogie.ast.ast_and(exprs)[source]

aria.efmc.verifytools.boogie.ast.ast_boolean_exprs(n)[source]

aria.efmc.verifytools.boogie.ast.ast_constants(n)[source]

aria.efmc.verifytools.boogie.ast.ast_group_bin(exprs, op, default)[source]

aria.efmc.verifytools.boogie.ast.ast_or(exprs)[source]

aria.efmc.verifytools.boogie.ast.ast_primitive_boolean_exprs(n)[source]

aria.efmc.verifytools.boogie.ast.expr_read(ast)[source]

aria.efmc.verifytools.boogie.ast.normalize(ast)[source]

aria.efmc.verifytools.boogie.ast.parseAst(s)[source]

aria.efmc.verifytools.boogie.ast.parseExprAst(s)[source]

aria.efmc.verifytools.boogie.ast.stmt_changed(ast)[source]

aria.efmc.verifytools.boogie.ast.stmt_read(ast)[source]

aria.efmc.verifytools.tools.vc_check.conservative_tautology(q)[source]

aria.efmc.verifytools.tools.vc_check.generalizeConstTraceVars(lvl)[source]: Given an expression and a set of pairs (Var, Num) where Var is always equal to Num in the traces presented to the user, add all variations of expr with Num substituded for Var and vice-versa. Note we don’t do combinations of multiple substitutions where that is possible.

aria.efmc.verifytools.tools.vc_check.loopInvOverfittedCtrex(loop, invs, bbs, timeout=None)[source]: Given a candidate loop invariant inv find ‘overfittedness’ counterexamples. I.e. find counterexamples to “precondition ==> inv”. Returns a potentially empty set of environments (dicts) that the invariant should satisfy.

aria.efmc.verifytools.tools.vc_check.loopInvSafetyCtrex(loop, invs, bbs, timeout=None)[source]: Given a candidate loop invariant inv find ‘safety’ counterexamples. I.e. find counterexamples to “inv ==> post” or “inv ==> assert”. Returns a potentially empty set of environments (dicts) that the invariant should satisfy.

aria.efmc.verifytools.tools.vc_check.substitutions(expr, replMs)[source]

aria.efmc.verifytools.tools.vc_check.traceConstantVars(lvl)[source]

aria.efmc.verifytools.tools.vc_check.tryAndVerify(bbs, loop, splitterPreds, partialInvs, userInvs, otherInvs, replMaps, timeout=None)[source]

aria.efmc.verifytools.tools.vc_check.tryAndVerifyLvl(lvl, userInvs, otherInvs, timeout=None, useSplitters=True, addSPs=True, generalizeUserInvs=False)[source]

Try and verify a given Lvl.

lvl - level to verify userInvs - invariant candidate from the user otherInvs - invariant candidates from other sources (e.g. previous

users). Note: We will keep userInvs and otherInvs separate in the results.

timeout - if specified, the z3 timeout for each query useSplitters - if the level supports splitter predicates, whether to

use them or not.

addSPs - if true, try to propagte SP through the loop and add the: results as invariants. For example if before the loop we have “assert n>0;” and n is not modified in the loop, we can determine that”n>0” holds through the loop and add that to our cnadidate invariants.
generalizeUserInvs - if true, for any invariant I involving a: constant C, where one of the variables V shown to the user was always equal to C in the traces, try substituting C with V. For example if in the level always n=4, and the user entered i<=4, the generalizaition would also try i<=n.

aria.efmc.verifytools.tools.vc_check.tryAndVerifyWithSplitterPreds(bbs, loop, old_sound_invs, boogie_invs, splitterPreds, partialInvs, timeout=None)[source]

Wrapper around tryAndVerify_impl that adds implication with the splitter predicates to all candidate invariants. Returns

((p1_overfit, p2_overfit), (p1_nonindg, p2_nonind), sound, violations)

Where

p1_overfit, p2_ovefit are lists of pairs of overfittted invariants
and their respective counterexamples from passes 1 and 2

p1_nonind, p2_ovefit are lists of pairs of noninductive invariants
and their respective counterexamples from passes 1 and 2

sound is a set of sound invariants violations is a list of any safety violations permitted by the sound invariants

aria.efmc.verifytools.tools.vc_check.tryAndVerify_impl(bbs, loop, old_sound_invs, invs, timeout=None)[source]: Wrapper around checkInvNetwork for the case of a function with a single loop and no pre- post- conditions. Returns a tuple (overfitted, nonind, sound, violations) where

overfitted, nonind are each a list of tuples (inv, Violation) sound is a set of sound invariants violations is a (potentially empty) list of safety Violations

for the sound invariants.

AST classes for Daikon invariants.

class aria.efmc.verifytools.daikon.inv_ast.AstBinExpr(lhs, op, rhs)[source]

Bases: AstNode

AST node for binary expressions.

class aria.efmc.verifytools.daikon.inv_ast.AstBuilder[source]

Bases: DaikonInvParser

AST builder for Daikon invariants.

onAtom(prod, st, loc, toks)[source]: Handle atom production.

onLABinOp(prod, st, loc, toks)[source]: Handle left-associative binary operator production.

onNABinOp(prod, st, loc, toks)[source]: Handle non-associative binary operator production.

onRABinOp(prod, st, loc, toks)[source]: Handle right-associative binary operator production.

onTernaryOp(prod, st, loc, toks)[source]: Handle ternary operator production.

onUnaryOp(prod, st, loc, toks)[source]: Handle unary operator production.

onVariaryOp(prod, st, loc, toks)[source]: Handle variary operator production.

class aria.efmc.verifytools.daikon.inv_ast.AstFalse[source]

Bases: AstNode

AST node for false literal.

class aria.efmc.verifytools.daikon.inv_ast.AstHasValues(expr, values)[source]

Bases: AstNode

AST node for has-values check.

class aria.efmc.verifytools.daikon.inv_ast.AstId(name)[source]

Bases: AstNode

AST node for identifier.

class aria.efmc.verifytools.daikon.inv_ast.AstInRange(lower, expr, upper)[source]

Bases: AstNode

AST node for range check.

class aria.efmc.verifytools.daikon.inv_ast.AstIsBoolean(expr)[source]

Bases: AstNode

AST node for boolean check.

class aria.efmc.verifytools.daikon.inv_ast.AstIsConstMod(expr, remainder, modulo)[source]

Bases: AstNode

AST node for constant modulo check.

class aria.efmc.verifytools.daikon.inv_ast.AstIsEven(expr)[source]

Bases: AstNode

AST node for even check.

class aria.efmc.verifytools.daikon.inv_ast.AstIsOneOf(expr, options)[source]

Bases: AstNode

AST node for one-of check.

class aria.efmc.verifytools.daikon.inv_ast.AstIsPow2(expr)[source]

Bases: AstNode

AST node for power-of-2 check.

class aria.efmc.verifytools.daikon.inv_ast.AstNumber(num)[source]

Bases: AstNode

AST node for number literal.

class aria.efmc.verifytools.daikon.inv_ast.AstTrue[source]

Bases: AstNode

AST node for true literal.

class aria.efmc.verifytools.daikon.inv_ast.AstUnExpr(op, expr)[source]

Bases: AstNode

AST node for unary expressions.

aria.efmc.verifytools.daikon.inv_ast.parse_expr_ast(s)[source]: Parse a Daikon invariant expression string into an AST.

Grammar parser for Daikon invariants.

class aria.efmc.verifytools.daikon.inv_grammar.DaikonInvParser[source]

Bases: InfixExprParser

Parser for Daikon invariant expressions.

onAtom(prod, st, loc, toks)[source]: Handle atom production - to be overridden by subclasses.

onLABinOp(prod, st, loc, toks)[source]: Handle left-associative binary operator production - to be overridden by subclasses.

onNABinOp(prod, st, loc, toks)[source]: Handle non-associative binary operator production - to be overridden by subclasses.

onRABinOp(prod, st, loc, toks)[source]: Handle right-associative binary operator production - to be overridden by subclasses.

onTernaryOp(prod, st, loc, toks)[source]: Handle ternary operator production - to be overridden by subclasses.

onUnaryOp(prod, st, loc, toks)[source]: Handle unary operator production - to be overridden by subclasses.

onVariaryOp(prod, st, loc, toks)[source]: Handle variary operator production - to be overridden by subclasses.

parse(st)[source]: Parse a Daikon invariant string.