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]

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.