DC Verifier for AC Programs

DC is a program verifier for the Appendix C programming language (AC), which is specifically designed to for this verification approach. The verification is based on symbolic execution and the assertion language supports separation logic. AC itself supports loops and mutable structured memory, so simple algorithms can be implemented.

For example a program calculating a Fibonacci numbers:

struct num {n: int} in
struct tuple {fib0: int, fib1: int} in
let n := malloc(num, 10) in
let fib := malloc(tuple, 0, 1) in
  (@ invariant !n.n >= 0 ** !fib.fib0 >= 0 ** !fib.fib1 >= 0 @
  while !n.n > 0 do
    !n.n := !n.n - 1;
    let x := !fib.fib0 + !fib.fib1 in
      !fib.fib1 := !fib.fib0;
      !fib.fib0 := x;
      @ !fib.fib0 >= !fib.fib1 @
  );
  !fib.fib0;
  @ result >= 0 @

Usage

In general DC only requires one positional argument, a path to an AC program. However, it is possible to print the AST or disable specific functionality like type checking.

DC Verifier for AC programs

Usage: /home/lurch/VSCodeProjects/appendix_c_verifier/_build/install/default/bin/dc <file> [--no-type-check] [--no-verify] [--no-interpret] [--print-ast]
  --no-preprocessing disables preprocessing step for bringing the AST in SSA form
  --no-type-check disables type checker
  --no-verify disables symbolic execution and verification
  --no-interpret disables program interpretation, so the input program is not executed
  --print-ast prints the AST after parsing
  -help  Display this list of options
  --help  Display this list of options

Building and Running

Dependencies can be installed by running:

# if you want a local opam switch run:
#opam switch create .
opam install . --deps-only --with-test --with-doc

The project can be built by running:

dune build
# or
opam exec -- dune build

The program can be started by running:

./dc program.ac
# or
dune exec dc -- program.ac
# or
opam exec -- dune exec dc -- program.ac

The tests can be executed by running:

dune test
# or
opam exec -- dune test

More verbose exception and trace printing can be enabled by setting an environment variable:

export OCAMLRUNPARAM=b

Documentation for the implemented modules can be generated by running:

dune build @doc-private
# or
opam exec -- dune build @doc-private

AC Programming Language

AC has terms, expressions, and commands. The terms are a subset of the expressions and the expressions are a subset of the commands. There are example programs in folder programs folder. In the following all terms, expressions, and commands are listed with simple examples.

All terms:

Term	Example
integer	42
boolean	true
negation for boolean	not false
negation for integer	-5
paranthesis around expression	(1 + 2)
dereferencing field f	!x.f

All expressions:

Expression	Example
and	a && b
or	a || b
separation conjunction	a ** b
addition	a + b
subtraction	a - b
multiplication	a * b
division	a / b
equality	a == b
inequality	a != b
less than	a < b
less than or equal to	a <= b
greater than	a < b
greater than or equal to	a >= b
term	5

All commands:

Command	Example
let	let x := 5 in x + 3
conditional	if x > 0 then 5 else 3
structure definition	struct point2d {x: int, y: int, b: bool} in ...
memory allocation	let p := malloc(point2d, 3, 7, false) in !p.x
assignment	!p.y := 13
freeing memory	mfree(p)
paranthesis around command	(if cond then 5 else 2) + 1
sequence	!p.y := 13; !p.x + !p.y
assertion (result is the return value of the previous command)	@ result >= 5 @
while loop	while !n.n > 0 do !n.n := !n.n - 1
while loop with invariant	@ invariant !n.n >= 0 @ while !n.n > 0 do !n.n := !n.n - 1
expression	64 / 2