Hello,
I am trying to use KLEE on some of my source base and it looks like KLEE
doesn't like some common data structures. For example, the combination of
symbolic nodes in linked-lists and recursion puts it in a bad state.
I am asking you guys to validate my assumptions here, and perhaps give some
handy tips.
See below for snippet of code w/ errors (and LLVM IR).
What happens is the following; everything is fine at first, but when we
enter the recursive loop and the second load instruction (in ?bb? of
dump_list) is hit (we are now on an error path?), we get to klee::Executor::
executeMemoryOperation() which in turn runs klee::AddressSpace::resolve().
In the ?while (oi!=begin)? loop a big number of resolutions is generated
(several hundred) which means that executeMemoryOperation() will run many
forks.
After this we basically crawl and spend all our time in the solver. For
example; running further memory instructions (in the loop) we get ?stuck? in
klee::AddressSpace::resolveOne().
Here is a snipped of code as a simplified example;
---(C Code)------------------------------------------------
#include <stdio.h>
#include <malloc.h>
struct node {
int data;
struct node *child;
};
typedef struct node n;
n* new_node(int data)
{
n *tmp = malloc(sizeof(n));
tmp->data = data;
tmp->child = 0;
return tmp;
}
n* new_child(n *node, int data)
{
if (node->child == 0)
return node->child = new_node(data);
else
return 0;
}
void dump_list(n *node, int depth)
{
int i;
if (node == 0)
return;
if (node->child != 0)
dump_list(node->child, depth+1);
printf("(%d) %d\n", depth, node->data);
}
void dump_list2(n *node, int depth)
{
while (node) {
printf("%d\n", node->data);
node = node->child;
}
}
int main(int argc, char *argv[])
{
n* root_heap;
root_heap = new_node(1);
klee_make_symbolic(root_heap, sizeof(n), "root_heap");
printf("00\n");
new_child(root_heap, 2);
printf("01\n");
dump_list(root_heap, 0);
printf("02\n");
}
---(LLVM IR)------------------------------------------------
define void @dump_list(%struct.n* %node, i32 %depth) nounwind {
entry:
%node_addr = alloca %struct.n* ; <%struct.n**> [#uses=5]
%depth_addr = alloca i32 ; <i32*> [#uses=3]
%i = alloca i32 ; <i32*> [#uses=0]
%"alloca point" = bitcast i32 0 to i32 ; <i32> [#uses=0]
store %struct.n* %node, %struct.n** %node_addr
store i32 %depth, i32* %depth_addr
%0 = load %struct.n** %node_addr, align 4 ; <%struct.n*> [#uses=1]
%1 = icmp eq %struct.n* %0, null ; <i1> [#uses=1]
br i1 %1, label %bb3, label %bb
bb: ; preds = %entry
%2 = load %struct.n** %node_addr, align 4 ; <%struct.n*> [#uses=1]
%3 = getelementptr inbounds %struct.n* %2, i32 0, i32 1 ; <%struct.n**>
[#uses=1]
%4 = load %struct.n** %3, align 4 ; <%struct.n*> [#uses=1]
%5 = icmp ne %struct.n* %4, null ; <i1> [#uses=1]
br i1 %5, label %bb1, label %bb2
bb1: ; preds = %bb
%6 = load i32* %depth_addr, align 4 ; <i32> [#uses=1]
%7 = add nsw i32 %6, 1 ; <i32> [#uses=1]
%8 = load %struct.n** %node_addr, align 4 ; <%struct.n*> [#uses=1]
%9 = getelementptr inbounds %struct.n* %8, i32 0, i32 1 ; <%struct.n**>
[#uses=1]
%10 = load %struct.n** %9, align 4 ; <%struct.n*> [#uses=1]
call void @dump_list(%struct.n* %10, i32 %7) nounwind
br label %bb2
bb2: ; preds = %bb1, %bb
%11 = load %struct.n** %node_addr, align 4 ; <%struct.n*> [#uses=1]
%12 = getelementptr inbounds %struct.n* %11, i32 0, i32 0 ; <i32*>
[#uses=1]
%13 = load i32* %12, align 4 ; <i32> [#uses=1]
%14 = load i32* %depth_addr, align 4 ; <i32> [#uses=1]
%15 = call i32 (i8*, ...)* @printf(i8* noalias getelementptr inbounds ([9
x i8]* @.str, i32 0, i32 0), i32 %14, i32 %13) nounwind ; <i32> [#uses=0]
br label %bb3
bb3: ; preds = %bb2, %entry
br label %return
return: ; preds = %bb3
ret void
}
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20091208/bc458189/attachment.html
