View source for Cascade User Manual

From CVC4
You do not have permission to edit this page, for the following reason:
The action you have requested is limited to users in the group: Users.
You can view and copy the source of this page.
= Getting Cascade =

== Miscellaneous setup ==

* Packages that may need to be installed:
** [http://www.oracle.com/technetwork/java/javase/downloads/index.html sun-java6-jdk]
** [http://www.oracle.com/technetwork/java/javase/downloads/index.html sun-java6-jre]
** [http://maven.apache.org/download.html maven]
** [http://www.eclipse.org/downloads/packages/release/indigo/sr2 eclipse]
** [http://eclipse.org/m2e/download/ eclipse maven plugin]
** [http://subclipse.tigris.org/servlets/ProjectProcess?pageID=p4wYuA 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 [http://cvc4.cs.nyu.edu/wiki/User_Manual#Getting_CVC4 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 [https://subversive.cims.nyu.edu/cascade/trunk/ 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 ''wayPoint''s 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 ''wayPoint''s 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 ''function''s 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 ''wayPoint''s 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 ''loop''s 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 here.
  __allocated_list(next, root, 2)
It means a list with length 2 and starts with root has been created.
Return to Cascade User Manual.
Retrieved from "http://cvc4.stanford.edu/wiki/Cascade_User_Manual"
View source for Cascade User Manual

Navigation menu

Views

Personal tools

CVC4

For CVC4 Developers

Cascade

Meta

Wiki

Search

Tools
