Boogie Frontend for EFMC

This document describes the Boogie frontend for EFMC, which allows you to convert Boogie programs (specifically loops) to EFMC transition systems for verification.

Overview

Microsoft Boogie is an intermediate verification language that serves as a common target for multiple program verifiers. The EFMC Boogie frontend enables you to:

Parse Boogie programs and extract loops
Convert loops to EFMC transition systems
Verify the converted programs using EFMC’s verification engines
Generate CHC (Constrained Horn Clause) format for external solvers

Usage

Basic Usage

from aria.efmc.frontends.boogie2efmc import boogie_to_efmc

# Convert a Boogie file to a transition system
ts = boogie_to_efmc("program.bpl")

# The transition system can now be used with EFMC engines
print(f"Variables: {[str(v) for v in ts.variables]}")
print(f"Initial condition: {ts.init}")
print(f"Transition relation: {ts.trans}")
print(f"Post condition: {ts.post}")

Advanced Usage

from aria.efmc.frontends.boogie2efmc import BoogieToEFMCConverter

# Create converter instance
converter = BoogieToEFMCConverter()

# Parse and extract loops
ast_program = converter.parse_boogie_file("program.bpl")
loops, bbs = converter.extract_loops_from_program(ast_program)

# Convert specific loop to transition system
ts = converter.convert_loop_to_transition_system(loops[0], bbs)

# Generate CHC format for external verification
chc_str = ts.to_chc_str()
with open("program.smt2", "w") as f:
    f.write(chc_str)

Supported Boogie Features

Statements

Assignments: x := expr;
Assumptions: assume expr;
Assertions: assert expr;
Havoc: havoc x, y; (non-deterministic assignment)
Goto: goto label1, label2;
Labels: label:

Expressions

Arithmetic: +, -, *, div, mod
Comparison: ==, !=, <, <=, >, >=
Boolean: &&, ||, ==>, !
Literals: integers, true, false
Variables: identifiers

Data Types

Currently supports integer variables (int)
Boolean expressions for conditions

Example Boogie Programs

Simple Counter

implementation Counter()
{
    var x, count: int;

    entry:
        assume x >= 0;
        count := 0;
        goto loop_header;

    loop_header:
        goto loop_body, loop_exit;

    loop_body:
        assume x > 0;
        x := x - 1;
        count := count + 1;
        goto loop_header;

    loop_exit:
        assume x <= 0;
        assert count >= 0;
        return;
}

Fibonacci Computation

implementation Fibonacci()
{
    var n, a, b, temp: int;

    entry:
        assume n >= 0;
        a := 0;
        b := 1;
        goto loop_header;

    loop_header:
        goto loop_body, loop_exit;

    loop_body:
        assume n > 0;
        temp := a + b;
        a := b;
        b := temp;
        n := n - 1;
        goto loop_header;

    loop_exit:
        assume n <= 0;
        assert a >= 0;
        assert b >= 0;
        return;
}

Verification Workflow

Parse Boogie Program: The frontend parses the Boogie file and builds an AST
Extract Basic Blocks: Convert the AST to a control flow graph of basic blocks
Detect Loops: Identify loops in the control flow graph
Extract Variables: Collect all variables used in the loop
Build Transition System: Create initial conditions, transition relations, and post conditions
Verify: Use EFMC engines or external solvers to verify the safety properties

Generated Transition System

The converter creates a transition system with:

Variables: Current state variables (e.g., x, y)
Prime Variables: Next state variables (e.g., x!, y!)
Initial Condition: Entry condition for the loop
Transition Relation: How variables change in one loop iteration
Post Condition: Safety properties to verify (from assertions)

Integration with EFMC Engines

The generated transition systems can be used with various EFMC verification engines:

Template-based (EF): Constraint-based invariant generation
PDR/IC3: Property-directed reachability analysis
K-induction: Inductive verification
Houdini: Iterative invariant inference

CHC Format Generation

The frontend can generate CHC (Constrained Horn Clause) format compatible with SMT solvers:

ts = boogie_to_efmc("program.bpl")
chc_str = ts.to_chc_str()

# Save for external verification
with open("program.smt2", "w") as f:
    f.write(chc_str)

# Verify with Z3
# z3 program.smt2

Limitations

Single Loop: Currently focuses on programs with a single loop
Integer Variables: Primarily supports integer arithmetic
Simple Control Flow: Works best with structured loops
Manual Loop Detection: Falls back to heuristic loop detection when automatic detection fails

Future Enhancements

Support for nested loops
Array and pointer support
More sophisticated loop detection
Integration with more Boogie language features
Support for concurrent programs

Error Handling

The frontend includes robust error handling:

Graceful parsing failures with detailed error messages
Fallback loop detection when automatic detection fails
Warning messages for unsupported features
Comprehensive logging for debugging

Testing

Test files are provided to validate the implementation:

test_boogie_converter.py: Basic functionality tests
example_boogie_verification.py: End-to-end verification examples

Run tests with:

python test_boogie_converter.py
python example_boogie_verification.py