Cascade User Manual

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. No modular approach is done. If there's a function call in the execution path specified in the control file, Cascade could automatically find the function definition, pass values from arguments to parameters, and return the result to the caller. 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.

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, as example.

Cascade Command

Each position (start point, end point and way point) can further include a command, which include: (1) cascade_assume, which takes a source code expression and adds it as an assumption; (2) cascade_check, which takes a source code expression and checks whether it is valid at the given position.

Cascade_check

Let's go futher of the example of abs.c. One property should be hold in it is

   result >= 0

In abs3.ctrl, such expression is an argument of command cascade_check. Cascade can prove its validity in both runs, which means it is indeed guaranteed to hold in both branches.

Cascade_assume

Sometimes, we need to add assumptions at some points of the execution path to let Cascade ignore certain cases that would otherwise lead to invalid proof, in order to narrow down the check to more specific senario. Let's illustrate it in another 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.