about summary refs log tree commit diff homepage
path: root/test/Feature/KleePtreeBogus.test
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2023-03-24 21:14:02 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-12 12:00:35 +0000
commit19b6ae578b0658115d15848604a28434845bb3e3 (patch)
tree31d52545929760ad725385bd1cdc1153b710fc75 /test/Feature/KleePtreeBogus.test
parentfc83f06b17221bf5ef20e30d9da1ccff927beb17 (diff)
downloadklee-19b6ae578b0658115d15848604a28434845bb3e3.tar.gz
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.
Diffstat (limited to 'test/Feature/KleePtreeBogus.test')
-rw-r--r--test/Feature/KleePtreeBogus.test65
1 files changed, 65 insertions, 0 deletions
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