From 19b6ae578b0658115d15848604a28434845bb3e3 Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Fri, 24 Mar 2023 21:14:02 +0000
Subject: new: persistent ptree (-write-ptree) and klee-ptree

Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
     and tracks information such as branch type, termination
     type or source location (asm) in nodes. Enabled with
     -write-ptree

ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.
---
 test/CMakeLists.txt                           |  2 +-
 test/Feature/KleePtreeBogus.test              | 65 ++++++++++++++++++++++
 test/Feature/WritePtree.c                     | 78 +++++++++++++++++++++++++++
 test/Feature/ptree-dbs/duplicated_node.csv    |  5 ++
 test/Feature/ptree-dbs/empty_db.csv           |  1 +
 test/Feature/ptree-dbs/invalid_btype.csv      |  4 ++
 test/Feature/ptree-dbs/invalid_ttype.csv      |  4 ++
 test/Feature/ptree-dbs/loop.csv               |  5 ++
 test/Feature/ptree-dbs/missing_after_max.csv  |  5 ++
 test/Feature/ptree-dbs/missing_before_max.csv |  5 ++
 test/Feature/ptree-dbs/node_id0.csv           |  6 +++
 test/Feature/ptree-dbs/not_a.db               |  1 +
 test/lit.cfg                                  |  9 ++++
 test/lit.site.cfg.in                          |  3 ++
 14 files changed, 192 insertions(+), 1 deletion(-)
 create mode 100644 test/Feature/KleePtreeBogus.test
 create mode 100644 test/Feature/WritePtree.c
 create mode 100644 test/Feature/ptree-dbs/duplicated_node.csv
 create mode 100644 test/Feature/ptree-dbs/empty_db.csv
 create mode 100644 test/Feature/ptree-dbs/invalid_btype.csv
 create mode 100644 test/Feature/ptree-dbs/invalid_ttype.csv
 create mode 100644 test/Feature/ptree-dbs/loop.csv
 create mode 100644 test/Feature/ptree-dbs/missing_after_max.csv
 create mode 100644 test/Feature/ptree-dbs/missing_before_max.csv
 create mode 100644 test/Feature/ptree-dbs/node_id0.csv
 create mode 100644 test/Feature/ptree-dbs/not_a.db

(limited to 'test')

diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index b4716dae..ae038b80 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -147,7 +147,7 @@ file(GENERATE
 
 add_custom_target(systemtests
   COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}"
-  DEPENDS klee kleaver klee-replay kleeRuntest ktest-gen ktest-randgen
+  DEPENDS klee kleaver klee-ptree klee-replay kleeRuntest ktest-gen ktest-randgen
   COMMENT "Running system tests"
   USES_TERMINAL
 )
diff --git a/test/Feature/KleePtreeBogus.test b/test/Feature/KleePtreeBogus.test
new file mode 100644
index 00000000..11fe87c8
--- /dev/null
+++ b/test/Feature/KleePtreeBogus.test
@@ -0,0 +1,65 @@
+REQUIRES: sqlite3
+
+fail on broken db (not sqlite)
+RUN: not %klee-ptree tree-info %S/ptree-dbs/not_a.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-CORRUPT -input-file=%t.err %s
+CHECK-CORRUPT: Can't prepare read statement: file is not a database
+
+empty tree
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/empty_db.csv nodes" 
+RUN: %klee-ptree tree-info %t.db > %t.err
+RUN: FileCheck -check-prefix=CHECK-EMPTY -input-file=%t.err %s
+CHECK-EMPTY: Empty tree.
+
+fail on tree with duplicate node IDs
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/duplicated_node.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-DUP -input-file=%t.err %s
+CHECK-DUP: PTree DB contains duplicate child reference or circular structure. Affected node: 2
+
+fail on invalid branch type
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_btype.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-BTYPE -input-file=%t.err %s
+CHECK-BTYPE: PTree DB contains unknown branch type (123) in node 1
+
+fail on invalid termination type
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_ttype.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-TTYPE -input-file=%t.err %s
+CHECK-TTYPE: PTree DB contains unknown termination type (123) in node 3
+
+fail on tree with looping nodes
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/loop.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-LOOP -input-file=%t.err %s
+CHECK-LOOP: PTree DB contains duplicate child reference or circular structure. Affected node: 1
+
+fail on tree with missing node (child node ID > max. ID)
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_after_max.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-MISSA -input-file=%t.err %s
+CHECK-MISSA: PTree DB contains references to non-existing nodes (> max. ID) in node 3
+
+fail on tree with missing node (child node ID < max. ID)
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_before_max.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-MISSB -input-file=%t.err %s
+CHECK-MISSB: PTree DB references undefined node. Affected node: 4
+
+fail on illegal node ID (0)
+RUN: rm -f %t.db
+RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/node_id0.csv nodes" 
+RUN: not %klee-ptree tree-info %t.db 2> %t.err
+RUN: FileCheck -check-prefix=CHECK-ID0 -input-file=%t.err %s
+CHECK-ID0: PTree DB contains illegal node ID (0)
+
+cleanup
+RUN rm -f %t.db
diff --git a/test/Feature/WritePtree.c b/test/Feature/WritePtree.c
new file mode 100644
index 00000000..e7bf59ce
--- /dev/null
+++ b/test/Feature/WritePtree.c
@@ -0,0 +1,78 @@
+// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee -write-ptree --output-dir=%t.klee-out %t.bc
+// RUN: %klee-ptree branches %t.klee-out/ptree.db | FileCheck --check-prefix=CHECK-BRANCH %s
+// RUN: %klee-ptree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s
+// RUN: %klee-ptree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s
+// RUN: %klee-ptree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s
+// RUN: %klee-ptree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s
+// RUN: %klee-ptree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s
+// RUN: not %klee-ptree dot %t.klee-out/ptree-doesnotexist.db
+
+#include "klee/klee.h"
+
+#include <stddef.h>
+
+int main(void) {
+  int a = 42;
+  int c0, c1, c2, c3;
+  klee_make_symbolic(&c0, sizeof(c0), "c0");
+  klee_make_symbolic(&c1, sizeof(c1), "c1");
+  klee_make_symbolic(&c2, sizeof(c2), "c2");
+  klee_make_symbolic(&c3, sizeof(c3), "c3");
+
+  if (c0) {
+    a += 17;
+  } else {
+    a -= 4;
+  }
+
+  if (c1) {
+    klee_assume(!c1);
+  } else if (c2) {
+    char *p = NULL;
+    p[4711] = '!';
+  } else if (c3) {
+    klee_silent_exit(0);
+  } else {
+    return a;
+  }
+
+  return 0;
+}
+
+// CHECK-BRANCH: branch type,count
+// CHECK-BRANCH: Conditional,7
+
+// CHECK-DEPTH: depth,count
+// CHECK-DEPTH: 3,2
+// CHECK-DEPTH: 4,2
+// CHECK-DEPTH: 5,4
+
+// CHECK-INSTR: asm line,branches,terminations,termination types
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,User(2)
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Ptr(2)
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,SilentExit(2)
+// CHECK-INSTR-DAG: {{[0-9]+}},0,2,Exit(2)
+
+// CHECK-TERM: termination type,count
+// CHECK-TERM-DAG: Exit,2
+// CHECK-TERM-DAG: Ptr,2
+// CHECK-TERM-DAG: User,2
+// CHECK-TERM-DAG: SilentExit,2
+
+// CHECK-DOT: strict digraph PTree {
+// CHECK-DOT: node[shape=point,width=0.15,color=darkgrey];
+// CHECK-DOT: edge[color=darkgrey];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Conditional\nnode: {{[0-9]+}}\nstate: 0\nasm: {{[0-9]+}}"];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Exit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=green];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="SilentExit\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=orange];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Ptr\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=red];
+// CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="User\nnode: {{[0-9]+}}\nstate: {{[0-9]+}}\nasm: {{[0-9]+}}",color=blue];
+// CHECK-DOT-DAG: N{{[0-9]+}}->{N{{[0-9]+}} N{{[0-9]+}}};
+// CHECK-DOT-DAG: }
+
+// CHECK-TINFO: nodes: 15
+// CHECK-TINFO: leaf nodes: 8
+// CHECK-TINFO: max. depth: 5
+// CHECK-TINFO: avg. depth: 4.2
diff --git a/test/Feature/ptree-dbs/duplicated_node.csv b/test/Feature/ptree-dbs/duplicated_node.csv
new file mode 100644
index 00000000..7882b911
--- /dev/null
+++ b/test/Feature/ptree-dbs/duplicated_node.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,2,62,1
+4,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/empty_db.csv b/test/Feature/ptree-dbs/empty_db.csv
new file mode 100644
index 00000000..4dac8a17
--- /dev/null
+++ b/test/Feature/ptree-dbs/empty_db.csv
@@ -0,0 +1 @@
+ID,stateID,leftID,rightID,asmLine,kind
diff --git a/test/Feature/ptree-dbs/invalid_btype.csv b/test/Feature/ptree-dbs/invalid_btype.csv
new file mode 100644
index 00000000..01ee428c
--- /dev/null
+++ b/test/Feature/ptree-dbs/invalid_btype.csv
@@ -0,0 +1,4 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,123
+2,0,0,0,61,36
+3,1,0,0,61,1
diff --git a/test/Feature/ptree-dbs/invalid_ttype.csv b/test/Feature/ptree-dbs/invalid_ttype.csv
new file mode 100644
index 00000000..0d185bee
--- /dev/null
+++ b/test/Feature/ptree-dbs/invalid_ttype.csv
@@ -0,0 +1,4 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,0,0,61,123
diff --git a/test/Feature/ptree-dbs/loop.csv b/test/Feature/ptree-dbs/loop.csv
new file mode 100644
index 00000000..4fc2b9f2
--- /dev/null
+++ b/test/Feature/ptree-dbs/loop.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,1,62,1
+4,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/missing_after_max.csv b/test/Feature/ptree-dbs/missing_after_max.csv
new file mode 100644
index 00000000..16e99a35
--- /dev/null
+++ b/test/Feature/ptree-dbs/missing_after_max.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,5,62,1
+4,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/missing_before_max.csv b/test/Feature/ptree-dbs/missing_before_max.csv
new file mode 100644
index 00000000..2131ea56
--- /dev/null
+++ b/test/Feature/ptree-dbs/missing_before_max.csv
@@ -0,0 +1,5 @@
+ID,stateID,leftID,rightID,asmLine,kind
+1,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,5,62,1
+5,1,0,0,63,80
diff --git a/test/Feature/ptree-dbs/node_id0.csv b/test/Feature/ptree-dbs/node_id0.csv
new file mode 100644
index 00000000..51a31e49
--- /dev/null
+++ b/test/Feature/ptree-dbs/node_id0.csv
@@ -0,0 +1,6 @@
+ID,stateID,leftID,rightID,asmLine,kind
+0,0,2,3,44,1
+2,0,0,0,61,36
+3,1,4,5,62,1
+4,1,0,0,63,80
+5,2,0,0,63,36
diff --git a/test/Feature/ptree-dbs/not_a.db b/test/Feature/ptree-dbs/not_a.db
new file mode 100644
index 00000000..d81cc071
--- /dev/null
+++ b/test/Feature/ptree-dbs/not_a.db
@@ -0,0 +1 @@
+42
diff --git a/test/lit.cfg b/test/lit.cfg
index cb47d3d4..8abf7012 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -116,6 +116,11 @@ config.substitutions.append(
   ('%libkleeruntest', config.libkleeruntest)
 )
 
+# Add a substition for sqlite3
+config.substitutions.append(
+  ('%sqlite3', os.path.abspath(config.sqlite3))
+)
+
 # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line
 # e.g. llvm-lit --param klee_opts=--help
 klee_extra_params = lit_config.params.get('klee_opts',"")
@@ -134,6 +139,7 @@ if len(kleaver_extra_params) != 0:
 # If a tool's name is a prefix of another, the longer name has
 # to come first, e.g., klee-replay should come before klee
 subs = [ ('%kleaver', 'kleaver', kleaver_extra_params),
+         ('%klee-ptree', 'klee-ptree', ''),
          ('%klee-replay', 'klee-replay', ''),
          ('%klee-stats', 'klee-stats', ''),
          ('%klee-zesti', 'klee-zesti', ''),
@@ -233,3 +239,6 @@ config.available_features.add('{}32bit-support'.format('' if config.have_32bit_s
 config.available_features.add('{}asan'.format('' if config.have_asan else 'not-'))
 config.available_features.add('{}ubsan'.format('' if config.have_ubsan else 'not-'))
 config.available_features.add('{}msan'.format('' if config.have_msan else 'not-'))
+
+# SQLite
+config.available_features.add('{}sqlite3'.format('' if config.have_sqlite3 else 'not-'))
diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in
index c7063057..d82b8a2c 100644
--- a/test/lit.site.cfg.in
+++ b/test/lit.site.cfg.in
@@ -26,6 +26,8 @@ config.cxx = "@NATIVE_CXX@"
 #       test/Concrete/CMakeLists.txt
 config.O0opt = "-O0 -Xclang -disable-O0-optnone"
 
+config.sqlite3 = "@SQLITE_CLI@"
+
 # Features
 config.enable_uclibc = True if @SUPPORT_KLEE_UCLIBC@ == 1 else False
 config.enable_posix_runtime = True if @ENABLE_POSIX_RUNTIME@ == 1 else False
@@ -39,6 +41,7 @@ config.have_asan = True if @IS_ASAN_BUILD@ == 1 else False
 config.have_ubsan = True if @IS_UBSAN_BUILD@ == 1 else False
 config.have_msan = True if @IS_MSAN_BUILD@ == 1 else False
 config.have_32bit_support = True if @M32_SUPPORTED@ == 1 else False
+config.have_sqlite3 = True if "@SQLITE_CLI@".strip() != "" else False
 
 # Add sanitizer list
 config.environment['LSAN_OPTIONS'] = "suppressions=@KLEE_UTILS_DIR@/sanitizers/lsan.txt"
-- 
cgit 1.4.1