C Frontend for EFMC

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

Overview

The EFMC C frontend enables you to:

Parse C 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.c2efmc import c_to_efmc

# Convert a C file to a transition system
ts = c_to_efmc("program.c")

# 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.c2efmc import CToEFMCConverter

# Create converter instance
converter = CToEFMCConverter()

# Parse C file
ast = converter.parse_c_file("program.c")

# Convert to transition system (defaults to main function)
ts = converter.convert_file_to_transition_system("program.c")

# Or specify a different function
ts = converter.convert_file_to_transition_system("program.c", function="my_function")

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

Supported C Features

The C frontend currently focuses on loop-centric verification:

Integer Variables: Support for integer arithmetic operations
Loops: While loops, for loops
Assignments: Variable assignments
Conditions: Boolean conditions for loops and branches
Arithmetic Operations: Addition, subtraction, multiplication, division, modulo
Comparison Operations: Equality, inequality, less than, greater than, etc.

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
Function Selection: Defaults to the main function

Example C Programs

Simple Counter

int main() {
    int x = 10;
    while (x > 0) {
        x = x - 1;
    }
    assert(x == 0);
    return 0;
}

Fibonacci Computation

int main() {
    int n = 10;
    int a = 0, b = 1;
    while (n > 0) {
        int temp = a + b;
        a = b;
        b = temp;
        n = n - 1;
    }
    assert(a >= 0);
    assert(b >= 0);
    return 0;
}

Verification Workflow

Parse C Program: The frontend parses the C file using pycparser and builds an AST
Extract Function: Selects the target function (default: main)
Detect Loop: Identifies loops in the function
Extract Variables: Collects all variables used in the loop
Build Transition System: Creates initial conditions, transition relations, and post conditions
Verify: Uses 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 = c_to_efmc("program.c")
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

Command-Line Usage

You can use the C frontend directly from the command line:

efmc --file program.c --lang c --engine ef --template interval

The --lang c option tells EFMC to use the C frontend. If not specified, EFMC will auto-detect the language based on the file extension.

Future Enhancements

Support for nested loops
Array and pointer support
Support for more C language features
Multiple function verification
Support for floating-point arithmetic

Error Handling

The frontend includes robust error handling:

Graceful parsing failures with detailed error messages
Warning messages for unsupported features
Comprehensive logging for debugging

Testing

Test files are provided to validate the implementation:

test_c2efmc.py: Basic functionality tests

Run tests with:

python -m pytest efmc/tests/test_c2efmc.py