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 efmc.verifytools.common.ast import Expr, Stmt
from efmc.verifytools.common.parser import parse_formula
from efmc.verifytools.common.util import simplify

Common AST

Base classes for abstract syntax trees:

from 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 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 efmc.verifytools.boogie.ast import BoogieProgram, Procedure
from 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 efmc.verifytools.boogie.bb import BasicBlockAnalyzer

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

Static Single Assignment (SSA)

from efmc.verifytools.boogie.ssa import to_ssa

ssa_program = to_ssa(program)

Predicate Transformers

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

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

Z3 Integration

from 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 efmc.verifytools.tools.vc_check import check_vc

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

Try-and-Verify Strategy

from efmc.verifytools.tools.tryAndVerify import TryAndVerify

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

Desugaring

from efmc.verifytools.tools.desugar import desugar_program

simplified = desugar_program(program)

Format Conversions

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

Daikon Integration

The daikon subpackage provides integration with the Daikon invariant detector:

from efmc.verifytools.daikon.inv_grammar import InvGrammar
from 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 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 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 efmc.verifytools.common.ast.AstNode(*args)

Bases: object

Base class for AST nodes with structural equality and hashing.

efmc.verifytools.common.ast.reduce_nodes(node, cb)

Reduce nodes using callback function cb.

efmc.verifytools.common.ast.replace(ast, m)

Replace AST nodes according to mapping m.

Parser base classes for expression parsing.

class efmc.verifytools.common.parser.InfixExprParser

Bases: Parser

Parser for infix expressions.

onAtom(prod, st, loc, toks)

Handle atom production.

onLABinOp(prod, st, loc, toks)

Handle left-associative binary operator production.

onNABinOp(prod, st, loc, toks)

Handle non-associative binary operator production.

onRABinOp(prod, st, loc, toks)

Handle right-associative binary operator production.

onUnaryOp(prod, st, loc, toks)

Handle unary operator production.

class efmc.verifytools.common.parser.Parser

Bases: object

Base parser class.

Common utility functions.

efmc.verifytools.common.util.average(vals)

Calculate the average of a list of values.

efmc.verifytools.common.util.error(*args)

Print error message to stderr.

efmc.verifytools.common.util.fatal(*args)

Print error message and exit with error code.

efmc.verifytools.common.util.flattenList(s)

Flatten a list of lists into a single list.

efmc.verifytools.common.util.flattenSet(s)

Flatten a set of sets into a single set.

efmc.verifytools.common.util.nodups(s)

Remove duplicates from a sequence.

efmc.verifytools.common.util.nonempty(lst)

Filter out the empty elements of a list (where empty is len(x) == 0).

efmc.verifytools.common.util.powerset(s)

Return the powerset of a set s.

efmc.verifytools.common.util.pp_exc(f)

Wrap a function to catch, pretty print the exception and re-raise it.

efmc.verifytools.common.util.randomToken(l)

Generate a random alphanumeric token of length l.

efmc.verifytools.common.util.split(pred, itr)

Split a list based on a predicate function.

efmc.verifytools.common.util.unique(iterable, msg='')

Assert that iterable has one element and return it.

class efmc.verifytools.boogie.ast.AstAssert(expr)

Bases: AstOneExprStmt

class efmc.verifytools.boogie.ast.AstAssignment(lhs, rhs)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstAssume(expr)

Bases: AstOneExprStmt

class efmc.verifytools.boogie.ast.AstBinExpr(lhs, op, rhs)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstBinding(names, typ)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstBlock(stmts)

Bases: AstStmt

class efmc.verifytools.boogie.ast.AstBody(bindings, stmts)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstBuilder

Bases: BoogieParser

onAssert(prod, st, loc, toks)

onAssignment(prod, st, loc, toks)

onAssume(prod, st, loc, toks)

onAtom(prod, st, loc, toks)

Handle atom production.

onBlock(prod, st, loc, toks)

onBody(prod, st, loc, toks)

onGoto(prod, st, loc, toks)

onHavoc(prod, st, loc, toks)

onImplementationDecl(prod, st, loc, toks)

onLABinOp(prod, st, loc, toks)

Handle left-associative binary operator production.

onLabeledStatement(prod, st, loc, toks)

onLocalVarDecl(prod, st, loc, toks)

onNABinOp(prod, st, loc, toks)

Handle non-associative binary operator production.

onProgram(prod, st, loc, toks)

onRABinOp(prod, st, loc, toks)

Handle right-associative binary operator production.

onReturn(prod, st, loc, toks)

onType(prod, st, loc, toks)

onUnaryOp(prod, st, loc, toks)

Handle unary operator production.

onWhile(prod, st, loc, toks)

class efmc.verifytools.boogie.ast.AstFalse

Bases: AstNode

class efmc.verifytools.boogie.ast.AstFuncExpr(funcName, *ops)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstGoto(labels)

Bases: AstStmt

class efmc.verifytools.boogie.ast.AstHavoc(ids)

Bases: AstStmt

class efmc.verifytools.boogie.ast.AstId(name)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstImplementation(name, signature, body)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstIntType

Bases: AstNode

class efmc.verifytools.boogie.ast.AstLabel(label, stmt)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstNumber(num)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstOneExprStmt(expr)

Bases: AstStmt

class efmc.verifytools.boogie.ast.AstProgram(decls)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstReturn

Bases: AstStmt

class efmc.verifytools.boogie.ast.AstStmt(*args)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstTrue

Bases: AstNode

class efmc.verifytools.boogie.ast.AstUnExpr(op, expr)

Bases: AstNode

class efmc.verifytools.boogie.ast.AstWhile(condition, invariants, body)

Bases: AstStmt

efmc.verifytools.boogie.ast.ast_and(exprs)

efmc.verifytools.boogie.ast.ast_boolean_exprs(n)

efmc.verifytools.boogie.ast.ast_constants(n)

efmc.verifytools.boogie.ast.ast_group_bin(exprs, op, default)

efmc.verifytools.boogie.ast.ast_or(exprs)

efmc.verifytools.boogie.ast.ast_primitive_boolean_exprs(n)

efmc.verifytools.boogie.ast.expr_read(ast)

efmc.verifytools.boogie.ast.normalize(ast)

efmc.verifytools.boogie.ast.parseAst(s)

efmc.verifytools.boogie.ast.parseExprAst(s)

efmc.verifytools.boogie.ast.stmt_changed(ast)

efmc.verifytools.boogie.ast.stmt_read(ast)

efmc.verifytools.tools.vc_check.conservative_tautology(q)

efmc.verifytools.tools.vc_check.generalizeConstTraceVars(lvl)

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.

efmc.verifytools.tools.vc_check.loopInvOverfittedCtrex(loop, invs, bbs, timeout=None)

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.

efmc.verifytools.tools.vc_check.loopInvSafetyCtrex(loop, invs, bbs, timeout=None)

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.

efmc.verifytools.tools.vc_check.substitutions(expr, replMs)

efmc.verifytools.tools.vc_check.traceConstantVars(lvl)

efmc.verifytools.tools.vc_check.tryAndVerify(bbs, loop, splitterPreds, partialInvs, userInvs, otherInvs, replMaps, timeout=None)

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

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.

efmc.verifytools.tools.vc_check.tryAndVerifyWithSplitterPreds(bbs, loop, old_sound_invs, boogie_invs, splitterPreds, partialInvs, timeout=None)

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

efmc.verifytools.tools.vc_check.tryAndVerify_impl(bbs, loop, old_sound_invs, invs, timeout=None)

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 efmc.verifytools.daikon.inv_ast.AstBinExpr(lhs, op, rhs)

Bases: AstNode

AST node for binary expressions.

class efmc.verifytools.daikon.inv_ast.AstBuilder

Bases: DaikonInvParser

AST builder for Daikon invariants.

onAtom(prod, st, loc, toks)

Handle atom production.

onLABinOp(prod, st, loc, toks)

Handle left-associative binary operator production.

onNABinOp(prod, st, loc, toks)

Handle non-associative binary operator production.

onRABinOp(prod, st, loc, toks)

Handle right-associative binary operator production.

onTernaryOp(prod, st, loc, toks)

Handle ternary operator production.

onUnaryOp(prod, st, loc, toks)

Handle unary operator production.

onVariaryOp(prod, st, loc, toks)

Handle variary operator production.

class efmc.verifytools.daikon.inv_ast.AstFalse

Bases: AstNode

AST node for false literal.

class efmc.verifytools.daikon.inv_ast.AstHasValues(expr, values)

Bases: AstNode

AST node for has-values check.

class efmc.verifytools.daikon.inv_ast.AstId(name)

Bases: AstNode

AST node for identifier.

class efmc.verifytools.daikon.inv_ast.AstInRange(lower, expr, upper)

Bases: AstNode

AST node for range check.

class efmc.verifytools.daikon.inv_ast.AstIsBoolean(expr)

Bases: AstNode

AST node for boolean check.

class efmc.verifytools.daikon.inv_ast.AstIsConstMod(expr, remainder, modulo)

Bases: AstNode

AST node for constant modulo check.

class efmc.verifytools.daikon.inv_ast.AstIsEven(expr)

Bases: AstNode

AST node for even check.

class efmc.verifytools.daikon.inv_ast.AstIsOneOf(expr, options)

Bases: AstNode

AST node for one-of check.

class efmc.verifytools.daikon.inv_ast.AstIsPow2(expr)

Bases: AstNode

AST node for power-of-2 check.

class efmc.verifytools.daikon.inv_ast.AstNumber(num)

Bases: AstNode

AST node for number literal.

class efmc.verifytools.daikon.inv_ast.AstTrue

Bases: AstNode

AST node for true literal.

class efmc.verifytools.daikon.inv_ast.AstUnExpr(op, expr)

Bases: AstNode

AST node for unary expressions.

efmc.verifytools.daikon.inv_ast.parse_expr_ast(s)

Parse a Daikon invariant expression string into an AST.

Grammar parser for Daikon invariants.

class efmc.verifytools.daikon.inv_grammar.DaikonInvParser

Bases: InfixExprParser

Parser for Daikon invariant expressions.

onAtom(prod, st, loc, toks)

Handle atom production - to be overridden by subclasses.

onLABinOp(prod, st, loc, toks)

Handle left-associative binary operator production - to be overridden by subclasses.

onNABinOp(prod, st, loc, toks)

Handle non-associative binary operator production - to be overridden by subclasses.

onRABinOp(prod, st, loc, toks)

Handle right-associative binary operator production - to be overridden by subclasses.

onTernaryOp(prod, st, loc, toks)

Handle ternary operator production - to be overridden by subclasses.

onUnaryOp(prod, st, loc, toks)

Handle unary operator production - to be overridden by subclasses.

onVariaryOp(prod, st, loc, toks)

Handle variary operator production - to be overridden by subclasses.

parse(st)

Parse a Daikon invariant string.