Frontends

The frontends module provides parsers for various input formats, converting them into EFMC’s internal transition system representation.

Supported Formats

EFMC supports the following input formats:

1. CHC (Constrained Horn Clauses) - .smt2

2. SyGuS (Syntax-Guided Synthesis) - .sy, .sl

3. Boogie - .bpl

4. C - .c

5. VMT - .vmt (planned)

6. Btor2 - .btor2 (planned)

Architecture

efmc/frontends/
├── chc_parser.py          # CHC format parser
├── mini_sygus_parser.py   # SyGuS format parser
├── boogie2efmc.py         # Boogie frontend
├── c2efmc.py              # C frontend
├── c2chc.py               # C to CHC converter
├── chc2c.py               # CHC to C converter
├── btor2chc.py            # Btor2 to CHC converter
├── chc_parser.py          # CHC parser utilities
└── chc2c/                 # CHC2C subpackage
    ├── BaseCHC2C.py       # Base class
    ├── LinearCHC2C.py     # Linear CHC handling
    ├── NonLinearCHC2C.py  # Non-linear CHC handling
    └── chc2c.py           # Main converter

CHC Parser

The CHC (Constrained Horn Clauses) parser handles SMT-LIB files with constrained Horn clauses.

Usage

from efmc.frontends import parse_chc

# Parse CHC file
all_vars, init, trans, post = parse_chc("program.smt2", to_real_type=False)

# Create transition system
from efmc.sts import TransitionSystem
sts = TransitionSystem()
sts.from_z3_cnts([all_vars, init, trans, post])

CHC Format

A typical CHC file has the following structure:

(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)

; Init: x = 0
(assert (= x 0))

; Transition: y' = y + x, x' = x + 1
(assert (=> true (= y (+ y x))))

; Query: y < 0
(query (=> true (< y 0)))

The CHC representation consists of: - all_vars: All variables in the system - init: Initial state predicate - trans: Transition relation - post: Post-condition (query)

SyGuS Parser

The SyGuS parser handles Syntax-Guided Synthesis files, specifically the invariant track.

Usage

from efmc.frontends import parse_sygus

# Parse SyGuS file
all_vars, init, trans, post = parse_sygus("invariant.sy", to_real_type=False)

SyGuS Format

A typical SyGuS invariant file:

(set-logic QF_LIA)
(set-option :syntax-restrictions :inv)
(declare-fun x () Int)
(declare-fun inv ((x Int)) Bool)
(assert (inv 0))
(assert (forall ((x Int)) (=> (inv x) (inv (+ x 1)))))
(check-synth)

Boogie Frontend

The Boogie frontend handles Boogie intermediate verification language files.

Usage

from efmc.frontends import parse_boogie

# Parse Boogie file
sts = parse_boogie("program.bpl")

Boogie Format

A typical Boogie program:

var x: int;
var y: int;

procedure main()
  requires x >= 0;
  ensures y >= 0;
{
  y := x;
  while (x > 0)
    invariant y >= 0;
  {
    y := y - 1;
    x := x - 1;
  }
}

C Frontend

The C frontend parses C programs with annotations for verification.

Usage

from efmc.frontends import parse_c

# Parse C file
sts = parse_c("program.c")

C Format

A typical annotated C program:

/*@
  requires x >= 0;
  ensures \result >= 0;
@*/
int foo(int x) {
  int y = x;
  while (x > 0) {
    x = x - 1;
  }
  return y;
}

Conversion Tools

C to CHC

Convert C programs to Constrained Horn Clauses:

from efmc.frontends.c2chc import C2CHC

converter = C2CHC()
converter.convert("program.c", "output.smt2")

CHC to C

Convert CHC back to C:

from efmc.frontends.chc2c import CHC2C

converter = CHC2C()
converter.convert("program.smt2", "output.c")

Btor2 to CHC

Convert Btor2 (hardware description) to CHC:

from efmc.frontends.btor2chc import Btor2CHC

converter = Btor2CHC()
converter.convert("design.btor2", "output.smt2")

API Reference

Wrappers for the frontends - Constraint Horn Clause (CHC) - SyGuS invariant track - VMT: TBD - Btor2: TBD

efmc.frontends.parse_boogie(filename: str, to_real_type: bool = False)

Parse Boogie file

efmc.frontends.parse_c(filename: str, to_real_type: bool = False)

Parse C file

efmc.frontends.parse_chc(filename: str, to_real_type: bool)

Parse CHC file

efmc.frontends.parse_sygus(filename: str, to_real_type: bool)

Parse SyGuS file

Parser for Constraint Horn Clause (CHC) files based on Z3’s Python API

NOTE: this file provides a few other functionalities. For example,

we also support replacing “inv” by a function body

class efmc.frontends.chc_parser.CHCParser(inputs: str, to_real: bool)

Bases: object

NOTE: we assume that the input strictly follows the SyGuS(invariant) style

The first assertion: pre The second assertion: trans The third assertion (or “goal”): post

Besides, the goal should be in the form of

inv => post

Instead of

inv and P => post (this can be transformed to the above form)

fmls = []

get_transition_system()

parse_chc_string(chc: str)

solve_with_pdr()

efmc.frontends.chc_parser.ground_quantifier(qexpr)

Seems this can only handle exists x . fml, or forall x.fml?

efmc.frontends.chc_parser.test_parse()

efmc.frontends.chc_parser.test_parse2()

efmc.frontends.chc_parser.test_parse3(filename)

Parser for SyGuS files based on a simple S-expression parser

NOTE: I only this file for inputs in the style of the SyGuS invariant track. It could be used for SyGuS(PBE). To keep this file independent, I do not important other files in this project.

This parser handles: - S-expression parsing - Grammar extraction - Transition system conversion - Support for multiple data types (Int, Real, Array, BitVec)

exception efmc.frontends.mini_sygus_parser.SyGuSParsingError

Bases: Exception

Custom exception for SyGuS parsing errors

class efmc.frontends.mini_sygus_parser.SyGusInVParser(inputs: str, to_real: bool)

Bases: object

Parser for SyGuS Invariant Track problems.

get_transition_system()

Return the format of our trivial transition system

init_symbols(inputs: str)

TODO: this is not robust (as an sexpr can have several lines)

process_func(slist)

Process a ‘define-fun’ command to extract function bodies and variables.

to_sexpr(lines: List[str])

to_sexpr_misc(lines: List[str])

E.g., [‘and’, [‘=’, ‘x’, 1], [‘=’, ‘y’, 1]] [‘and’, [‘=’, ‘x!’, [‘+’, ‘x’, ‘y’]], [‘=’, ‘y!’, [‘+’, ‘x’, ‘y’]]]

efmc.frontends.mini_sygus_parser.atom(token: str) → Union[str, int, float]

Numbers become numbers; every other token is a symbol.

efmc.frontends.mini_sygus_parser.demo_parser()

efmc.frontends.mini_sygus_parser.get_grammar(lines: List[str])

efmc.frontends.mini_sygus_parser.get_nonterminals(cmd)

efmc.frontends.mini_sygus_parser.get_start(cmd) → str

efmc.frontends.mini_sygus_parser.get_terms_prods(cmd)

efmc.frontends.mini_sygus_parser.input_to_list(string: str) → List[str]

Parse a .sl file into a list of S-Expressions.

efmc.frontends.mini_sygus_parser.parse_sexpression(program: str) → Union[str, int, float, List]

Read an S-expression from a string.

efmc.frontends.mini_sygus_parser.read_from_tokens(tokens: list) → Union[str, int, float, List]

Read an expression from a sequence of tokens.

efmc.frontends.mini_sygus_parser.tokenize(chars: str) → list

Convert a string of characters into a list of tokens.

Boogie to EFMC Transition System Converter

This module converts Boogie programs (specifically loops) to EFMC’s transition system format, allowing verification using EFMC’s engines.

class efmc.frontends.boogie2efmc.BoogieToEFMCConverter

Bases: object

Converts Boogie programs to EFMC transition systems.

This converter focuses on extracting loops from Boogie programs and converting them to transition systems that can be verified using EFMC’s engines.

convert_file_to_transition_system(filename: str) → TransitionSystem

Convert a Boogie file to a transition system (main entry point).

convert_loop_to_transition_system(loop: Loop, bbs: Dict[str, BB], variables: Optional[List[str]] = None) → TransitionSystem

Convert a single Boogie loop to an EFMC transition system.

extract_loops_from_program(ast_program: AstProgram) → Tuple[List[Loop], Dict[str, BB]]

Extract loops from a Boogie program AST.

parse_boogie_file(filename: str) → AstProgram

Parse a Boogie file and return the AST.

efmc.frontends.boogie2efmc.boogie_to_efmc(filename: str) → TransitionSystem

Convenience function to convert a Boogie file to EFMC transition system.

C to EFMC transition system converter.

This frontend parses a (loop-centric) C program with pycparser and builds an EFMC TransitionSystem. The translation is lightweight and currently focuses on integer variables and the first loop encountered in the selected function (default: main).

class efmc.frontends.c2efmc.CToEFMCConverter

Bases: object

Convert simple C programs into EFMC transition systems.

convert_file_to_transition_system(filename: str, function: Optional[str] = None, use_cpp: bool = False, cpp_args: Optional[List[str]] = None) → TransitionSystem

Main entry point for converting a C file.

parse_c_file(filename: str, use_cpp: bool = False, cpp_args: Optional[List[str]] = None) → FileAST

Parse a C file into a pycparser AST.

efmc.frontends.c2efmc.c_to_efmc(filename: str) → TransitionSystem

Convenience wrapper mirroring boogie_to_efmc().