Uninit ptr (#34)

* BST test

* Added fixed BST test

* added test case for uninit ptr

* Partial implementation of fix for null deref aborting the whole program instead of a single path

* Instead of aborting on null pointder deref, abort only the current path and create a test

* some pointer testcases

* updated uninitV on cpp end, made pointer arithmetic state-aware, attempted to throw exception for symvite pointers since they are uninit and possibly null

* reorg test case

* ptr_add has to know complete type SS

* fix test cases

* test both stp and z3

* try simplify backend ptr_add

* move ptr_add back to value_ops.hpp

* Added expected nPath for faultyBst, added additional cases to SS::update() to handle invalid pointers

* added uninit ptr update and some code

* finished update for uninit pointers by adding update_symloc

* merged with Ruiqi's changes

* argv separate test

* fixed condition in get_sym_string_at

* append null byte to arguments instead of uninitv

* reverted unintentional value_ops changs, updated FaultyBST expected paths

* reverted condition to fix argvConc, which has been fixed by a different change

* Fixed flexAddr, added comments about assume

* fix for assume.c, made calloc actually zero

* made __calloc zero memory for PureGS

* made stack arrays a different symbolic value for each index, fixed some other tests

* added copynative2state constraints in PureGS to fix printf.c

* Fixed bad test :/

* work on putting symbolic uninit behind a flag

* fixed test with flags

* made compile symbolicUninit imply runtime symbolicUninit

* made tests set symbolicUninit correctly with a hack

* refactor config

* set symbolicUninit to false after test case

* updated a test case for symbolicUninit

* fixed final symbolicUninit test :/

* cleaned up symbolicUninit testcases

* fixed duplicate test names

* removed external_test.cpp

---------

Co-authored-by: Mikail Khan <mikail@mikail-khan.com>

benchmarks/demo-benchmarks/bst.c

@@ -7,6 +7,8 @@
 #include "klee/klee.h"
 #endif
 
+// Note that this test must be run with --thread=1
+
 #define SIZE 4
 
 typedef struct node_s {
@@ -86,7 +88,7 @@ int main() {
     klee_make_symbolic(data, sizeof(data), "data");
     klee_make_symbolic(&key, sizeof(int), "key");
 #else
-    make_symbolic(data, sizeof(int) * SIZE);
+    make_symbolic(data, sizeof(int) * SIZE, "data");
     make_symbolic(&key, sizeof(int), "key");
 #endif
 

benchmarks/demo-benchmarks/faulty_bst.c

@@ -0,0 +1,100 @@
+#include <stdio.h>
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+#include <stdio.h>
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+
+#define SIZE 4
+
+typedef struct node_s {
+    struct node_s* left;
+    struct node_s* right;
+    int val;
+} Node;
+
+Node* init_node(int val) {
+    Node* new_node = malloc(sizeof(Node));
+    new_node->val = val;
+
+    // Because these are left uninitialized,
+    // there may be an error in insert and find
+    /* new_node->left = NULL; */
+    /* new_node->right = NULL; */
+
+    return new_node;
+}
+
+Node* bst_insert(Node* root, int val) {
+    if (root == NULL) {
+        return init_node(val);
+    } 
+
+    assert(root != NULL);
+    if (root->val == -1) {
+        return init_node(val);
+    }
+
+    if (val > root->val) {
+        root->right = bst_insert(root->right, val);
+        return root;
+    } else {
+        root->left = bst_insert(root->left, val);
+        return root;
+    }
+}
+
+Node* bst_from_list(int* arr, int len) {
+    Node* root = NULL;
+    for (int i = 0; i < len; i += 1) {
+        root = bst_insert(root, arr[i]);
+    }
+
+    return root;
+}
+
+/* void bst_print_aux(Node* root) { */
+/*     if (root != NULL) { */
+/*         printf("%d ", root->val); */
+/*         bst_print_aux(root->left); */
+/*         bst_print_aux(root->right); */
+/*     } */
+/* } */
+
+/* void bst_print(Node* root) { */
+/*     bst_print_aux(root); */
+/*     printf("\n"); */
+/* } */
+
+bool bst_find(Node* root, int key) {
+    if (root == NULL || root->val == -1) {
+        return false;
+    } else if (key == root->val) {
+        return true;
+    } else if (key > root->val) {
+        return bst_find(root->right, key);
+    } else {
+        return bst_find(root->left, key);
+    }
+}
+
+int main() {
+    int data[SIZE];
+    int key;
+    /* for (int i = 0; i < SIZE; i += 1) { */
+    /*     data[i] = i; */
+    /* } */
+#ifdef KLEE
+    klee_make_symbolic(data, sizeof(data), "data");
+    klee_make_symbolic(&key, sizeof(int), "key");
+#else
+    make_symbolic(data, sizeof(int) * SIZE, "data");
+    make_symbolic(&key, sizeof(int), "key");
+#endif
+
+    Node* tree = bst_from_list(data, SIZE);
+    /* bst_print(tree); */
+    bst_find(tree, key);
+}

benchmarks/external-lib/assume.c

@@ -3,6 +3,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <unistd.h>
+#include <string.h>
 
 int main() {
   int x, y, z;
@@ -21,6 +22,7 @@ int main() {
   int ememb = 11;
   int *p1 = calloc(ememb, sizeof(int));    // allocate and zero out an array of ememb int
   int *p2 = calloc(1, sizeof(int[ememb])); // same, naming the array type directly
+
   for (int i=0;i<ememb;i++) {
     gs_assert_eager(p1[i] == p2[i]);
     gs_assert_eager(0 == p1[i]);

benchmarks/llvm/memchallenge.c

@@ -16,7 +16,7 @@ typedef struct {
 void gs_assert_eager(bool);
 
 int main() {
-    do {
+    do { // TODO: fails
         int64_t val = 0x1234567890abcdef;
         pair_t *st = &val;
         int16_t tmp = st->b;
@@ -38,4 +38,4 @@ int main() {
         memcpy(&p2, &p1, sizeof(p2));
     } while(0);
     return 0;
-}
+}

benchmarks/llvm/sym_pointer.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+#ifdef KLEE
+#include "klee/klee.h"
+#endif
+
+int main() {
+    int* ptr;
+
+#ifdef KLEE
+    klee_make_symbolic(&ptr, sizeof(int*), "ptr");
+#else
+    make_symbolic(&ptr, sizeof(int*), "ptr");
+#endif
+
+    if (ptr == NULL) {
+        return 0;
+    } else {
+        return *ptr;
+    }
+}

benchmarks/llvm/uninit_ptr.c

@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+// This test must be run with --thread=1
+// so that the NullDerefException is caught
+
+int main() {
+  int* ptr;
+  return *ptr;
+}

benchmarks/llvm/uninit_ptr_cond.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+// This test must be run with --thread=1
+// so that the NullDerefException is caught
+
+int main() {
+    int* ptr;
+
+    if (ptr == NULL) {
+        return 0;
+    } else {
+        return *ptr;
+    }
+}

benchmarks/llvm/uninit_ptr_update.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+
+// This test must be run with --thread=1
+// so that the NullDerefException is caught
+
+int main() {
+  int* ptr;
+  *ptr = 10;
+  return *ptr;
+}

headers/gensym/args.hpp

@@ -79,7 +79,7 @@ inline List<List<PtrVal>> parse_args(std::string argstrings) {
   immer::flex_vector_transient<List<PtrVal>> result;
   while (std::getline(ss, s, ' ')) {
     if (!s.empty()) {
-      result.push_back(to_chars(match_arg(s)).push_back(make_UnInitV()));
+      result.push_back(to_chars(match_arg(s)).push_back(make_IntV(0, 8)));
     }
   }
   return result.persistent();

headers/gensym/defs.hpp

@@ -114,6 +114,8 @@ inline unsigned int max_sym_array_size = 0;
 inline unsigned int max_size_bound = 400;
 // Use simplification when constructing SymV values
 inline bool use_symv_simplify = false;
+// Let uninitialized memory be set to symbolic values
+inline bool symbolic_uninit = false;
 
 // Output directory name
 inline std::string output_dir_str = std::string("gensym-") + get_current_datetime();
@@ -248,4 +250,4 @@ inline std::string float_op2string(fOP op) {
   return "unknown op";
 }
 
-#endif
+#endif

headers/gensym/external_imp.hpp

@@ -207,7 +207,7 @@ inline T __calloc(SS& state, List<PtrVal>& args, __Cont<T> k) {
   IntData nmemb = proj_IntV(args.at(0));
   IntData size = proj_IntV(args.at(1));
   ASSERT(size > 0 && nmemb > 0, "Invalid nmemb and size");
-  auto emptyMem = List<PtrVal>(nmemb * size, make_UnInitV());
+  auto emptyMem = List<PtrVal>(nmemb * size, make_IntV(0, 8));
   PtrVal memLoc = make_LocV(state.heap_size(), LocV::kHeap, nmemb * size);
   if (exlib_failure_branch)
     return k(state.heap_append(emptyMem), memLoc) + k(state, make_LocV_null());
@@ -572,7 +572,17 @@ inline void copy_native2state(SS& state, PtrVal ptr, char* buf, int size) {
       ASSERT(bytes_num > 0, "Invalid bytes");
       // Do not over-write symbolic variable
       if (old_val->to_SymV()) {
-        i = i + bytes_num;
+        #ifdef GENSYM_SYMBOLIC_UNINIT
+            // add constraint on symbolic variable to be equal to concrete
+            for (int j = 0; j < bytes_num; j++) {
+              auto eq_constraint = int_op_2(iOP::op_eq, state.at_simpl(ptr + i), make_IntV(buf[i], 8));
+              state.add_PC(eq_constraint);
+              i++;
+              if (i >= size) break;
+            }
+        #else
+            i += bytes_num;
+        #endif
       } else {
         for (int j = 0; j < bytes_num; j++) {
           state.update_simpl(ptr + i, make_IntV(buf[i], 8));

headers/gensym/external_pure.hpp

@@ -239,7 +239,7 @@ inline T __calloc(SS& state, List<PtrVal>& args, __Cont<T> k) {
   IntData nmemb = proj_IntV(args.at(0));
   IntData size = proj_IntV(args.at(1));
   ASSERT(size > 0 && nmemb > 0, "Invalid nmemb and size");
-  auto emptyMem = List<PtrVal>(nmemb * size, make_UnInitV());
+  auto emptyMem = List<PtrVal>(nmemb * size, make_IntV(0, 8));
 
   PtrVal memLoc = make_LocV(state.heap_size(), LocV::kHeap, nmemb * size);
   if (exlib_failure_branch)
@@ -362,8 +362,17 @@ inline SS copy_native2state(SS state, PtrVal ptr, char* buf, int size) {
       ASSERT(bytes_num > 0, "Invalid bytes");
       // All bytes must be concrete IntV
       if (std::dynamic_pointer_cast<SymV>(old_val)) {
-        // Todo: should we overwrite symbolic variables?
-        i = i + bytes_num;
+        #ifdef GENSYM_SYMBOLIC_UNINIT
+            // add constraint on symbolic variable to be equal to concrete
+            for (int j = 0; j < bytes_num; j++) {
+              auto eq_constraint = int_op_2(iOP::op_eq, state.at_simpl(ptr + i), make_IntV(buf[i], 8));
+              res = res.add_PC(eq_constraint);
+              i++;
+              if (i >= size) break;
+            }
+        #else
+            i += bytes_num;
+        #endif
       } else {
         for (int j = 0; j < bytes_num; j++) {
           res = res.update_simpl(ptr + i, make_IntV(buf[i], 8));

headers/gensym/state_tsnt.hpp

@@ -31,7 +31,7 @@ class PreMem {
       return move_this();
     }
     M&& alloc(size_t size) {
-      mem.append(List<V>(size, make_UnInitV()).transient());
+      mem.append(make_UnInitList(size));
       return move_this();
     }
     M&& take(size_t keep) {
@@ -401,13 +401,21 @@ class SS {
           if (loc->l + size > heap.size()) throw NullDerefException { immer::box<SS>(*this) };
           return heap.at(loc->l, size);
         }
+      } else if (auto symloc = std::dynamic_pointer_cast<SymLocV>(addr)) {
+        return at_symloc(symloc, size);
+      } else if (auto symvite = addr->to_SymV()) {
+        if (iOP::op_ite == symvite->rator) {
+          return ite((*symvite)[0], at((*symvite)[1], size), at((*symvite)[2], size));
+        } else {
+          // Now the location value is a general symbolic value other than `ite`/`SymLocV`,
+          // which means the pointer is uninitialized anyway.
+          std::cout << "Symbolic Case\n";
+          throw NullDerefException { immer::box<SS>(*this) };
+        }
       }
-      if (auto symloc = std::dynamic_pointer_cast<SymLocV>(addr)) return at_symloc(symloc, size);
-      if (auto symvite = addr->to_SymV()) {
-        ASSERT(iOP::op_ite == symvite->rator, "Invalid memory read by symv index");
-        return ite((*symvite)[0], at((*symvite)[1], size), at((*symvite)[2], size));
-      }
-      ABORT("dereferenceing a nullptr");
+      // Default case: considered as an invalid memory access
+      std::cout << "Default Case\n";
+      throw NullDerefException { immer::box<SS>(*this) };
     }
     PtrVal at_struct(PtrVal addr, size_t size) {
       auto loc = addr->to_LocV();
@@ -454,37 +462,49 @@ class SS {
         heap.update(loc->l, val);
       return std::move(*this);
     }
-    SS&& update_symloc(PtrVal addr, PtrVal val, size_t size) {
-      auto symloc = std::dynamic_pointer_cast<SymLocV>(addr);
+    SS&& update_symloc(simple_ptr<SymLocV> symloc, PtrVal val, size_t size) {
       ASSERT(symloc != nullptr && symloc->size >= size, "Lookup an non-address value");
       auto offsym = symloc->off->to_SymV();
       ASSERT(offsym && (offsym->get_bw() == addr_index_bw), "Invalid sym offset");
 
       auto low_cond = int_op_2(iOP::op_sge, offsym, make_IntV(0, addr_index_bw));
       auto high_cond = int_op_2(iOP::op_sle, offsym, make_IntV(symloc->size - size, addr_index_bw));
+
       auto pc2 = pc;
       pc2.add(low_cond).add(high_cond);
       auto res = get_sat_value(pc2, offsym);
-      ASSERT(res.first, "no feasible offset\n");
 
-      // Todo (Ruiqi): Maybe use Intdata?
-      int offset_val = res.second;
-      auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw()));
+      if (res.first) {
+        // Todo (Ruiqi): Maybe use Intdata?
+        int offset_val = res.second;
+        auto t_cond = int_op_2(iOP::op_eq, offsym, make_IntV(offset_val, offsym->get_bw()));
+        // Todo (Ruiqi): should we add this?
+        pc.add(t_cond);
+
+        update(make_LocV(symloc->base, symloc->k, symloc->size, offset_val), val, size);
+        return std::move(*this);
+      } else {
+        throw NullDerefException { immer::box<SS>(*this) };
+      }
 
-      // Todo (Ruiqi): should we add this?
-      pc.add(t_cond);
-      update(make_LocV(symloc->base, symloc->k, symloc->size, offset_val), val, size);
       return std::move(*this);
     }
     SS&& update(PtrVal addr, PtrVal val, size_t size) {
       if (auto loc = addr->to_LocV()) {
-        if (loc->k == LocV::kStack) stack.update(loc->l, val, size);
+        if (loc->k == LocV::kStack) stack.update(loc->l, val, size); 
         else heap.update(loc->l, val, size);
       } else if (auto symloc = std::dynamic_pointer_cast<SymLocV>(addr)) {
-        update_symloc(symloc, val, size);
-      } else {
-        ABORT("dereferenceing a nullptr");
+          update_symloc(symloc, val, size);
+      } else if (auto symvite = addr->to_SymV()){
+          if (iOP::op_ite == symvite->rator) {
+              auto cond = (*symvite)[0];
+              SS s1 = update((*symvite)[1], ite(cond, val, at((*symvite)[1], size)), size);
+              return s1.update((*symvite)[2], ite(cond, val, at((*symvite)[2], size)), size);
+          } else {
+              throw NullDerefException { immer::box<SS>(*this) };
+          }
       }
+
       return std::move(*this);
     }
     SS&& update_seq(PtrVal addr, List<PtrVal> vals) {