The Control File
Unlike some verification systems, Cascade does not rely on annotated C code. Rather, a separate control file is used to guide the symbolic execution. Control files use XML and support the constructs detailed below.
Basic structure
Every control file begins with a sourceFile section that gives the paths to the source files. This is followed by one or more run sections, each defining a symbolic run of the program. Each run start with a single startPosition and ends with a single endPosition to give respectively the start point and end point of the run. A run may optionally include one or more wayPoint commands to indicate the positions that the considered run should pass through.
Sample code: abs.c and abs.ctrl
|
|
int abs(int x) {
int result;
if ( x >= 0 )
result = x;
else
result = x;
return result;
}
|
<!-- abs.ctrl -->
<controlFile>
<sourceFile name="abs.c" id="1" />
<run>
<startPosition fileId="1" line="1" />
<wayPoint fileId="1" line="4" />
<endPosition fileId="1" line="8" />
</run>
<sourceFile name="abs.c" id="1" />
<run>
<startPosition fileId="1" line="1" />
<wayPoint fileId="1" line="6" />
<endPosition fileId="1" line="8" />
</run>
</controlFile>
|
Function call
Function calls is supported via inlining. Cascade can perform inlining and parameter passing automatically. If users wish to specify a particular path in the function is called. Then a function section can be embedded with the wayPoint command which provides an attribute funcName, as well as the wayPoints of the desired path inside the function. Even if multiple functions are called at the same line of code, this can be handled by nesting multiple function sections under the wayPoint command for that line of code.
Sample codes: pow2.c and pow2.ctrl (automatic inlining)
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
|
int pow2(int x) {
return x*x;
}
int main() {
int a, b, result;
a = 2;
b = 3;
result = pow2(a) + pow2(b);
return result;
}
|
<!-- pow2.ctrl -->
<controlFile>
<sourceFile name="pow2.c" id="1" />
<run>
<startPosition fileId="1" line="5" />
<endPosition fileId="1" line="10" />
</run>
</controlFile>
|
Sample code: absext2.c and absext2.ctrl (multiple function calls)
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
|
int abs(int x) {
int result;
if ( x >= 0 )
result = x;
else
result = x;
return result;
}
int main() {
int a, result;
a = -4;
result = abs(a) - abs(-a);
return result;
}
|
<!-- absext2.ctrl -->
<controlFile>
<sourceFile name="absext2.c" id="1" />
<run>
<startPosition fileId="1" line="10" />
<wayPoint fileId="1" line="13" />
<function funcName="abs" funcId="1" />
<wayPoint fileId="1" line="6" />
</function/>
<function funcName="abs" funcId="2" />
<wayPoint fileId="1" line="4" />
</function/>
</wayPoint>
<endPosition fileId="1" line="15" />
</run>
</controlFile>
|
Loop
By default, loops are eliminated using bounded loop unrolling. A default number of unrolls can be specified on the command line, and a specific number of iterations for a particular loop can be specified using iterta loop command. Alternatively, a loop invariant can be specified using the invariant command as shown in the sample codes. The invariants are specified using C expressions.
Sample code: log2.c and log2.ctrl (loop unrolling)
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
|
int log2(int num) {
int result, i;
result = 0;
for(i=num; i>1; i=i/2) {
result++;
}
return result;
}
int main() {
int num, result;
num = 1024;
result = log2(num);
return result;
}
|
<!-- log2.ctrl -->
<controlFile>
<sourceFile name="log2.c" id="1" />
<run>
<startPosition fileId="1" line="10" />
<wayPoint fileId="1" line="13" >
<function funcName="log2" >
<wayPoint fileId="1" line="4" />
<loop iterTimes="10" />
</wayPoint>
</function/>
</wayPoint>
<endPosition fileId="1" line="15" />
</run>
</controlFile>
|
Sample code: sum.c and sum.ctrl (loop invariant)
|
|
int main() {
int sum = 0;
for (int i = 0; i<=10; i++) {
sum = sum + i;
}
return result;
}
|
<!-- sum.ctrl -->
<controlFile>
<sourceFile name="sum.c" id="1" />
<run>
<startPosition fileId="1" line="1" />
<wayPoint fileId="1" line="4" >
<loop>
<invariant><![CDATA[
sum == (i-1) * i / 2 && i >= 0 && i <= 11
]]>
</invariant>
</loop>
</wayPoint>
<endPosition fileId="1" line="7" />
</run>
</controlFile>
|
Command
Two commands cascade_assume and cascade_check are provided, each of which takes a C expresion as an argument. cascade_assume is used to constrain the set of possible states being considered to those satisfying the argument provided. cascade_check generates a verification condition to check that the symbolic execution up to this point satisfies the argument provided. Both commands can be nested inside one of startPosition, wayPoint and endPosition.
Cascade provides a number of extensions that can be embedded within C expressions to enable more expressive reasoning. These are listed below
- implies(P, Q): logical implication.
- forall(v, u, E): universal quantification.
- exists(v, u, E): existential quantification.
- allocated(p, size): heap allocation predicate, which is used to assume that a region with particular size has been allocated at p.
- valid(p): valid address predicate, which asserts p is a valid address in the memory, and is useful to check potential violations of memory safety such as double free or illegal memory access.
- reach(f, a, b): reachability predicate. This means that a can reach b via a path of field accesses using the field f.
- create_acyclic_list(root, length): list creation predicates to create singly, acyclic linked list with root as the first node and a particular length.
- create_cyclic_list(root, length): list creation predicates to create singly, cyclic linked list with root as the first node and a particular length.
- create_acyclic_dlist(root, length): list creation predicates to create doubly, acyclic linked list with root as the first node and a particular length.
- create_cyclic_dlist(root, length): list creation predicates to create doubly, cyclic linked list with root as the first node and a particular length.
Sample code: strlen.c and strlen.ctrl (memory safety reasoning)
|
|
int strlen(const char* str) {
int i;
i = 0; {
while(str[i] != '\0')
++i;
return result;
}
|
<!-- strlen.ctrl -->
<controlFile>
<sourceFile name="strlen.c" id="1" />
<run>
<startPosition fileId="1" line="1" />
<command>
<cascadeFunction> cascade_assume </cascadeFunction>
<argument><[CDATA[
allocated(str, 4*sizeof(char)
]]>
</argument>
</command>
</startPosition>
<wayPoint fileId="1" line="4" >
<loop iterTimes="3" />
</wayPoint>
<endPosition fileId="1" line="6" />
<command>
<cascadeFunction> cascade_check </cascadeFunction>
<argument><[CDATA[
forall(j, implies(j >= 0 && j <= i, valid(&str[i])))
]]>
</argument>
</command>
</endPosition>
</run>
</controlFile>
|
Sample code: list_append.c and list_append.ctrl (reasoning of linked list)
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
16.
17.
18.
19.
20.
21.
22.
|
#define NULL 0;
typedef struct NodeStruct {
struct NodeStruct *next;
int data;
} Node
void append(Node *l1, Node *l2) {
Node *l = l1;
Node *e = l1;
Node *last = NULL;
while(e) {
last = e;
e = e->next;
}
if(!last)
l = l2;
else
last->next = l2;
}
|
<!-- list_append.ctrl -->
<controlFile>
<sourceFile name="list_append.c" id="1" />
<run>
<startPosition fileId="1" line="8" />
<command>
<cascadeFunction> cascade_assume </cascadeFunction>
<argument><[CDATA[
create_acyclic_list(l1, 5) && create_acyclic_list(l2, 5)
]]>
</argument>
</command>
</startPosition>
<wayPoint fileId="1" line="13" >
<loop iterTimes="5" />
</wayPoint>
<wayPoint fileId="1" line="21" >
<endPosition fileId="1" line="22" />
<command>
<cascadeFunction> cascade_check </cascadeFunction>
<argument><[CDATA[
reach(next, l1, l2)
]]>
</argument>
</command>
</endPosition>
</run>
</controlFile>
|