Angelic Verifier

Documentation about the Angelic Verification (AV) tool!

Modules

AV is comprised of the following high-level modules:

The Substring "Null" in the name of the executables is unfortunate. There is nothing specific to null-checking.

These modules can be built by building AddOns\AngelicVerifierNull\AngelicVerifierNull.sln

AngelicVerifierNull.exe

This is the basic engine. It is a wrapper around Corral. It takes a Boogie file as input with a single declared entrypoint. It performs "angelic" reachability, starting from the entrypoint, looking for assertion violations. It distinguishes between demonic non-determinism (which is the default non-determinism in Boogie) and angelic non-determinism. The latter is obtained by declaring a procedure (without an implementation) as:

procedure {:AngelicUnknown} unknown(a:int) returns (b:int);

Then the command:

call r := unknown(1) ;

Will create an angelic value. AV tries to find values of these angelic unknowns such that the assertion is not reachable.

The idea is to keep AngelicVerifierNull.exe completely independent of source language semantics. It only knows Boogie semantics. Just like Corral.

TODO: Default flags

AvHarnessInstrumentation.exe

This is a Boogie-To-Boogie transformation. It performs instrumentation to get a program ready for AngelicVerifierNull.exe. The idea is to use this as a bridge between programs produced by a compiler and the program that is fed to AngelicVerifierNull.exe. This is not very complicated. We are allowed to make this compiler specific.

It adds a new procedure (called "CorralMain" currently) that is marked as an entrypoint. It includes a large switch statement that jumps to every possible implementation in the input program. It also creates "AngelicUnknown" procedures and uses them to make the return value of stubs (procedures without an implementation in the input program) angelic.

See usage in AddOns\AngelicVerifierNull\test\avn-regressions\runtest.bat

The script first runs AvHarnessInstrumentation and then calls AngelicVerifierNull on the resulting file.

AvHarnessInstrumentation also runs AliasAnalysis (AddOns\AliasAnalysis) to prune away assertions that can be proved statically.

TODO: Default flags

FastAVN.exe

FastAVN is an wrapper around AngelicVerifierNull and AvHarnessInstrumentation, and can be invoked on a Boogie file.

It takes a program, and runs AvHarnessInstrument on it. If the input program had N procedures with implementation (so harness instrumentation includes a main with a dispatch to all these N procedures) then FastAvn splits the program produced by AvHarnessInstrumentation into N programs, one for each procedure. It runs AngelicVerifierNull.exe on these N programs in parallel, depending on the number of available cores.

TODO: Default flags

PropInst.exe

The property instrumentation tool PropInst.exe takes as input (a) a Boogie file, and (b) an AV property (AVP) file (.avp extension) and produces a new Boogie file where the properties are instrumented. We describe details of the property language in the next section.

AV annotations

AV Property (AVP) language

AV Regressions

There are two sets of unit tests:

1. Basic AV regressions: See examples in: AddOns/AngelicVerifierNull/test/avn-regressions/*.bpl The script run.bat runs these regressions.

2. AV with Property instrumentation: See examples in: AddOns/AngelicVerifierNull/test/propinst-regressions/ The script run.bat runs these regressions.