-
Notifications
You must be signed in to change notification settings - Fork 29
Angelic Verifier
Documentation about the Angelic Verification (AV) tool!
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
This is the basic engine (sometimes called AVN). 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
This is a Boogie-To-Boogie transformation (sometimes called AVH). 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 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
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.
There are several example properties described here https://github.com/boogie-org/corral/tree/master/AddOns/PropInst/PropInst/ExampleProperties.
We describe details of the property language in the next section.
These are some annotations on the input Boogie file that are understood by the different AV modules.
{:scalar} tag on variable declarations: AVH only instruments non-scalar variables to be angelic non-determinism. In particular, AVH will treat all non-scalar globals and non-scalar parameters as angelic input. Thus, adding the {:scalar} annotation reduces the set of blocking clauses that AV can infer (=> more bugs).
Update: The scalar tag on globals and parameters is currently ignored. It is only used on return parameters of stubs.
{:ref "string"} tag on formal variables of procedures without a body. This is used to signify an out value. For example,
procedure foo({:ref "M"} x: int);
means that foo may possibly return a value through the heap. AVH creates a body for this procedure that looks like:
procedure foo(x: int) {
call M[x] := unknown();
}
Note: "M" must refer to a valid map in the program.
When a C procedure (without a body available in the module) has a parameter that is a double pointer, e.g.,
void bar(T **x);
Then add the annotation {:ref "M"} on the declaration of formal x, where M is the map that will index *x, i.e., imagine that bar assign to (*x).
{:entrypoint} tag on procedure declaration. This means that the procedure is a possible entrypoint. There can be multiple entrypoints. The flag /useEntryPoints must be used to activate this annotation, otherwise it is ignored.
{:AllocatorVar} tag on global variable declaration: This indicates a special Boogie instrumentation variable (not a C variable). Use this tag on the global variable used by "malloc" for doing allocation. The variable is called "alloc" in HAVOC/SDV files.
{:allocator} tag on procedure declaration. Use this on "malloc" and its variants.
{:ProgramInitialization} tag on a procedure. Used to constrain initial state of the memory. In Angelic Verification, given that we start exploration of the code from any procedure in the program, we drop the static initialization of global variables. However, in many applications of AV to SDV, we do need to retain some amount of "default" initialization of the memory. Any procedure tagged with {:ProgramInitialization} is called before AV starts exploration. (This is done by AvHarnessInstrumentation. AngelicVerification.exe does not understand this flag or concepts as static initialization of memory.) The flag /delayInitialization delays the initialization after assigning non-deterministic values to the unknowns.
{:allocator} tag on procedure declaration. Use this on "malloc" and its variants.
{:aliasingQuery} tag on functions. These functions must take two arguments of the same type and return bool. Any use of such functions, say "f(x,y)" will get resolved to "false" if x and y do not alias, and will get resolved to "x == y" if they may possibly alias.
(For most part, we do not have to worry about running AV directly. We will always be running AVH first.)
{:entrypoint} tag on procedure declaration. Marks the unique entrypoint of the program. Must be used.
{:AngelicUnknown} tag on a procedure without a body. Such procedures must have a single OUT parameter. The return value is assumed to be angelic. AV only constrains angelic values. Everything else (all other sources of non-determinism) are considered demonic.
{:ReachableStates} tag on a function. The function must be bool -> bool. For example,
function {:ReachableStates} MustReach(bool) : bool;
Inserting "assume MustReach(e);" means that the program must have at least one execution that reaches this statement and satisfies e. In other words, "assert !e" must not be provable.
{:propertyMap} tag is used to denote that a map is used for specification, and distinguish it from maps present in the input boogie file. This is interpreted by AV to infer specifications.
var {:propertyMap} validFree : [int] bool;
A quick introduction to AVP language is present here https://github.com/boogie-org/corral/wiki/AV-Property-(AVP)-Language.
There are two sets of unit tests:
-
Basic AV regressions: See examples in: https://github.com/boogie-org/corral/tree/master/AddOns/AngelicVerifierNull/test/avn-regressions The script run.bat runs these regressions.
-
AV with Property instrumentation: See examples in: https://github.com/boogie-org/corral/tree/master/AddOns/AngelicVerifierNull/test//propinst-regressions The script run.bat runs these regressions.