Revision as of 15:36, 17 December 2012

Getting Cascade

Miscellaneous setup

• Packages that may need to be installed:
  • sun-java6-jdk
  • sun-java6-jre
  • maven
  • eclipse
  • eclipse maven plugin
  • subclipse plugin
• Until the bug is fixed!
  • You may need to disable gnome_keyring in ~/.subversion/config.
  • To do this set "password-stores = " .

Build and Install CVC4

• Please check the instructions on visit the Getting CVC4. Note that, the directory I used to install CVC4 is "/Users/Wei/Workspace/target/cvc4".
• For Linux, add library to the LD_LIBRARY_PATH (DYLD_LIBRARY_PATH for Mac) in ~/.bashrc (or profile).

    export LD_LIBRARY_PATH=/Users/Wei/Workspace/target/cvc4/lib:$LD_LIBRARY_PATH

Configure maven

Here is a copy of my ~/.m2/settings.xml.

Build and Install Cascade

• Use eclipse or svn to check out each of these as top level projects from the svn repository.
  • c
  • core
  • cvc4-plugin

• Build "core"

    cd /Users/Wei/Workspace/cascade-cvc4/core
    mvn package
    mvn install

• Build "cvc4-plugin"

    cd /Users/Wei/Workspace/cascade-cvc4/cvc4-plugin
    mvn package
    mvn install

• Build "c"

    cd /Users/Wei/Workspace/cascade-cvc4/c
    mvn package
    mvn install

Using Cascade

These instructions assume you have followed the installation instructions.

Command line

• Make sure LD_LIBRARY_PATH (DYLD_LIBRARY_PATH for Mac) includes the directory the cvc4jni library and the cvc4 library are installed

   export LD_LIBRARY_PATH=/Users/Wei/Workspace/target/cvc4/lib:$LD_LIBRARY_PATH

• If you are For the cascade
• The cascade tool can be run using "c/target/cascade.sh". Use "--help" to determine options. This file is generated during the mvn package/install process.
• The cascade.sh tool does the following:
  • Defines variables for library locations using the settings from ~/.m2/settings.xml (at the time of mvn install).
  • Attempts to set the LD_LIBRARY_PATH variable. Note: I need to set LD_LIBRARY_PATH before cascade.sh. The part of the shell that is intended to set this does not seem to accomplish its task.
  • Passes the appropriate arguments to java for the correct classpath and runs the "edu.nyu.cascade.c.Main" class.
• As an alternative to cascade.sh, you can run java directly. An example is below.

 java -ea -cp /Users/Wei/Workspace/cascade-cvc4/c/target/cascade-c-0.0.2-SNAPSHOT-r1282-jar-with-dependencies.jar: \
 /Users/Wei/Workspace/cascade-cvc4/c/target/cascade-c-0.0.2-SNAPSHOT-r1282.jar edu.nyu.cascade.c.Main /Users/Wei/Workspace/cascade-\
 cvc4/c/src/test/resources/c/test/minicase_bug/minus_test.ctrl

• If you are not in the c/ directory when you run this, you may see the warning messages:

 Can't read plugins directory: ../cvc4-plugin/target
 Can't read plugins directory: /Users/Wei/Workspace/.cascade/plugins

Eclipse

• In the Package Explorer, Select c > src/main/java > edu.nyu.cascade.c > Main.java .
• Right-click Main.java. Select Run As > Run Configurations...
• Select the Environment tab
• Click New
• Enter Name: "LD_LIBRARY_PATH" (DYLD_LIBRARY_PATH for Mac) and Value: "/Users/Wei/Workspace/target/cvc4/lib/jni"
• Select the Arguments tab
• Add "-ea" to the VM arguments
• Set the Program arguments tab as you would the arguments to cascade.sh. For example: "--help" or "/Users/Wei/Workspace/cascade-cvc4/c/src/test/resources/c/test/minicase_bug/funcCall_test.ctrl"

Options

Cascade provides a number of options, and we introduce the ones often be used. The complete list of them are attached in cascade_options.

• -D, --debug: run in debug mode.
• --counter-example: enable counter example generation when Cascade failed to prove.
• --feasibility: check path feasibility for runs.
• --order-alloc: use an ordered allocation model (unsound). It assumes that there's no aliasing, overlapping between regions in the memory in an unsound way that keeps an arbitrary order of memory cells. It is enabled in the running of all the following examples.
• --sound-alloc: use a sound allocation model (may be slow). It assumes that there's no aliasing, overlapping between regions in the memory in a sound way. However, it generates a very large formula involves many case-splitting, and thus the verification in the theorem prover maybe slow.
• --resource-limit <N>: set resource limit for the theorem prover to N level.
• --time-limit <N>: set time limit for the theorem prover to N sec.
• --cvc4-stats: show statistics of the theorem prover.
• --iter-times <N>: default iteration times of loop unrolling.

Control Flow Annotation

Instead of inserting annotations in the source code, Cascade keeps them in a control file in order to leaves the source code clean. The control file is in the simple XML format, which serves as the guidance of verification. In this section, we will introduce the elements included control files by showing how to verify some sample codes in Cascade.

Basic Structure

Every control file starts with sourceFile sections that specify the files to be analyzed. Each source file has two attributes: name contains the path to the file, and fileId attaches a unique id to it. After sourceFile, one or more run sections are specified, which describe the runs to be checked. Each run starts with a single startPosition and endPosition to give the start point and the end point respectively, and in between, one or more wayPoints may be inserted optionally to indicate the positions should be passed through.

Let's discuss it more with a simple example abs.c. This program returns the absolute value of parameter x.

abs1.ctrl is the control file for it, in which the sourceFile indicates the path to abs.c and assigns an id 1 for it. For the execution path to check, we simply use the start and end line number of abs.c as startPosition and endPosition. Since there's a conditional statement if-else, we use a wayPoint to select one to check. Normally, a wayPoint is often the first line of the chosen code. Note that the fileId is all assigned to 1 in the startPosition, endPosition and wayPoint, which means these positions are all in abs.c (whose id is 1).

As mentioned above, multiple paths can be specified in one control file. In abs2.ctrl, two possible alternative runs of abs.c are considered together.

Function Call

Cascade supports functions by inlining. The locality of the parameters and the non-static local variables are preserved by attaching them with their scopes. Cascade can perform inlining and and thus parameters passing automatically. We'll see it in the example pow2.c and pow2.ctrl.

If the function contains branches and loops and we need to check a specific execution path in it, the annotation function will be helpful, as shown in example absext.c and absext.ctrl. The function section is nested under the wayPoint where it is called. It has an attribute funcName, whose value is name of the function, and the wayPoints of the path in that function is nested under it.

If multiple functions are called at the same line of code, we could nested multiple functions under the wayPoint, and differentiate them with the attribute funcId if the funcName are same, as in absext2.c and absext2.ctrl.

Loop

Cascade supports loop unwinding, which is unrolling the loops by finite number of times. It means the user must specify a bound by the attribute iterTimes in the anotation loop. Cascade will then unwind the loops up to that bound, and we can check if the number is correct or not by using option --feasibility (which is used to check the specific path is feasible or not). As an example, consider log2.c and log2.ctrl (note that the loop is nested in the function).

If there's a conditional statement inside the loop, we also can specify wayPoints in it. In addition, if different rounds of iteration have different execution paths, which means we need to specify them separately, we would nested multiple loops under one wayPoint. We will be clear about it with an example gcd.c and gcd.ctrl.

Cascade Command

In addition to execution path, we could specify some commands in control files, which involves adding assertions, assumptions and memory allocations. These commands are in the following format:

 <command>
   <cascadeFunction> cascade_cmd </cascadeFunction>
     <argument> arg_expr1 </argument>
     <argument><![CDATA[
     arg_expr2
     ]]>
     </argument>
 </command>

Logic Operators and Predicates

Before we go further into specific commands, let's talk a little about the argument expressions. They are valid C expressions, and a CDATA section can be used to allow regular C syntax within the XML format document. All variables referenced in the argument expression should be in scope at this position. Besides, Cascade provides a number of C extension that can be used within argument expressions to enable more expressive reasoning.

• Logic implication: _implies(P, Q). It formally means ((!P) || Q).
• Universal quantification: _forall(v, u, E). It means for every value v and u, E is true. For example, the assertion

   x > 1 && _forall(i, _implies(1 < i && i < x, x % i != 0))

• Existential quantification: _exists(v, u, E). It means for some value v and u, E is true. For example, the assertion

   _exists(i, _implies(1 < i && i < N, b[i] == 0))

• Valid address predicate: _valid(p). It means that p is a valid address in the memory, which has been allocated and not been freed yet.

   _forall(i, _implies(0 <= i && i < N, _valid(&b[i])))

• Reachability predicate: _reach(f, a, b). It means that a can reach b via f-path. This predicate captures the unbounded number of dynamically allocated cells present in a linked list. For a given cell a, it characterizes the set of cells {a, a.f, a.f.f, ...} reachable from u via f-path using the transitive closure (will be discussed later in details).

   _implies(_reach(f, a, b) && _reach(f, b, c), _reach(f, a, c))

• Heap allocation predicate: _allocated(p, size). It is used to assume that a region with size 4 has been allocated at p. This predicate is very helpful for modular verification, particularly of a function with pointers, arrays or structures as input arguments. As an example, consider strlen.c and strlen.ctrl.

   _allocated(str, 4*sizeof(char))

• Singly linked acyclic list creation predicate: _create_acyclic_list(f, root, length). It is used to assume that a singly acyclic list with particular length and root has been created. This predicate is very helpful for modular verification of linked data structure manipulation functions, which takes linked lists as parameters.

   _create_acyclic_list(f, l1, 3)

• Singly linked cyclic list creation predicate: _create_cyclic_list(f, root, length).

   _create_cyclic_list(f, l2, 4)

Now, let's go through those Cascade commands. They could be added at each position in the specific run, such as start point, end point and way point. The effect of them would be same as modifying the C source file to insert the statement at the exact position.

Cascade_check

The effect of this command is the same as the assert statement. Cascade would check if the argument expression is true at the particular position. Let's go back to the example of abs.c to see how to use it. Clearly, one desired property expected to hold at the end point of this program is

   result >= 0

In abs3.ctrl, such expression is an argument of command cascade_check. Run Cascade, it is proved to be "valid" in both runs, which means it is guaranteed to hold in both branches.

Cascade_assume

Sometimes, we want Cascade to ignore certain cases that would otherwise lead to invalid proof, in order to narrow down the check to more specific senario. We can do it by inserting assume statement at specific points of the run in the control file, as shown in the example div.c. This program computes the quotient and remainder from the division of numerator by denominator, returning the result in a structure of type "div_t". In the corresponding control file div.ctrl, an assumption

   denom != 0

is inserted at the start point, which excludes the possiblity of division by zero. Without this assumption, Cascade would fail to prove the asserted formula. The reason behind this is that division by zero is undefined in mathematics, and thus "result.quote" is an arbitrary value.

   num == div_result.quot * denom + div_result.rem

In fact, every statement along the execution path of the program is also an assumption, and the backend theorem prover is to prove if all assumptions hold, all assertions will also hold.

Reachability

In this section, we will discuss how to use Cascade to reason about reachability of linked data structure in details. Currently, we only support reason about linked list with single field. As discussed above, the predicate _reach(f, a, b) is used to indicate that b is reachable from a by repeatedly visiting the field f, and it is the key of our reasoning. list.c contains a number of functions of singly linked list, and we give a sample control file list_create.ctrl for the first function create(). A new section theory is created after sourceFile, and it defines the theory used in the reasoning. The attribute qname gives the name of the theory. In the assertion

 _reach(next, root, 0)

indicates that root can reach NULL (which defines as 0 in list.c) finally, which means that the created list is an acyclic list.

Another sample control file list_contains.ctrl is for the function contains(). Note that, the predicate _create_acyclic_list(f, root, length) is used to assume a list linked by field next, with length 2 and starts with node root.

 __allocated_list(next, root, 2)