Coverage guided search strategy

.github/workflows/scala.yml

@@ -78,6 +78,7 @@ jobs:
         sbt 'testOnly gensym.TestImpCPSGS'
         sbt 'testOnly gensym.TestImpCPSGS_Z3'
         sbt 'testOnly gensym.TestLibrary'
+        sbt 'testOnly gensym.CoverageGraphTest'
         sbt 'testOnly gensym.wasm.TestEval'
         sbt 'testOnly gensym.wasm.TestScriptRun'
         sbt 'testOnly gensym.wasm.TestConcolic'

benchmarks/demo-benchmarks/coverage_guided_assert.c

@@ -0,0 +1,116 @@
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+
+void make_symbolic(void *addr, size_t byte_size, ...);
+void gs_assert_eager(bool condition, ...);
+
+#if defined(__clang__) || defined(__GNUC__)
+#define NOINLINE __attribute__((noinline))
+#else
+#define NOINLINE
+#endif
+
+/*
+ * This benchmark deliberately separates new coverage from path count.
+ * warm_up_coverage() visits every block in decoy() and guarded_dispatch()
+ * before symbolic execution begins.  Consequently, a state sent to decoy()
+ * can create 2^24 paths but cannot discover a new block.  The all-ones route
+ * through guarded_dispatch(), on the other hand, is the shortest route to the
+ * one block which warm-up does not visit: the failing assertion.
+ */
+static NOINLINE uint32_t decoy(uint32_t bits) {
+  volatile uint32_t value = 0x9e3779b9u;
+
+#define DECOY_STEP(N)                                                        \
+  do {                                                                       \
+    if (bits & (1u << (N)))                                                  \
+      value = (value << 5) + value + (uint32_t)(N) + 1u;                    \
+    else                                                                     \
+      value = (value ^ (0x45d9f3bu + (uint32_t)(N))) * 33u;                 \
+  } while (0)
+
+  DECOY_STEP(0);
+  DECOY_STEP(1);
+  DECOY_STEP(2);
+  DECOY_STEP(3);
+  DECOY_STEP(4);
+  DECOY_STEP(5);
+  DECOY_STEP(6);
+  DECOY_STEP(7);
+  DECOY_STEP(8);
+  DECOY_STEP(9);
+  DECOY_STEP(10);
+  DECOY_STEP(11);
+  DECOY_STEP(12);
+  DECOY_STEP(13);
+  DECOY_STEP(14);
+  DECOY_STEP(15);
+  DECOY_STEP(16);
+  DECOY_STEP(17);
+  DECOY_STEP(18);
+  DECOY_STEP(19);
+  DECOY_STEP(20);
+  DECOY_STEP(21);
+  DECOY_STEP(22);
+  DECOY_STEP(23);
+
+#undef DECOY_STEP
+  return value;
+}
+
+static NOINLINE void hidden_bug(uint32_t key) {
+  if (key == 0xc0def00du)
+    gs_assert_eager(false, "coverage-guided benchmark reached the hidden bug");
+}
+
+static NOINLINE uint32_t guarded_dispatch(uint32_t selector,
+                                          uint32_t payload,
+                                          uint32_t key) {
+  if (!(selector & 0x01u)) return decoy(payload);
+  if (!(selector & 0x02u)) return decoy(payload);
+  if (!(selector & 0x04u)) return decoy(payload);
+  if (!(selector & 0x08u)) return decoy(payload);
+  if (!(selector & 0x10u)) return decoy(payload);
+  if (!(selector & 0x20u)) return decoy(payload);
+  if (!(selector & 0x40u)) return decoy(payload);
+  if (!(selector & 0x80u)) return decoy(payload);
+  if (!(selector & 0x100u)) return decoy(payload);
+  if (!(selector & 0x200u)) return decoy(payload);
+
+  hidden_bug(key);
+  return 0;
+}
+
+static NOINLINE void warm_up_coverage(void) {
+  /* Visit both sides of every decoy branch without creating symbolic paths. */
+  (void)decoy(0u);
+  (void)decoy(UINT32_MAX);
+
+  /* Visit every early-exit block in guarded_dispatch(). */
+  (void)guarded_dispatch(0u, 0u, 0u);
+  (void)guarded_dispatch(1u, 0u, 0u);
+  (void)guarded_dispatch(3u, 0u, 0u);
+  (void)guarded_dispatch(7u, 0u, 0u);
+  (void)guarded_dispatch(15u, 0u, 0u);
+  (void)guarded_dispatch(31u, 0u, 0u);
+  (void)guarded_dispatch(63u, 0u, 0u);
+  (void)guarded_dispatch(127u, 0u, 0u);
+  (void)guarded_dispatch(255u, 0u, 0u);
+  (void)guarded_dispatch(511u, 0u, 0u);
+
+  /* Cover hidden_bug()'s safe path, leaving only its assertion block new. */
+  (void)guarded_dispatch(1023u, 0u, 0u);
+}
+
+int main(void) {
+  uint32_t selector;
+  uint32_t payload;
+
+  warm_up_coverage();
+  make_symbolic(&selector, sizeof(selector), "selector");
+  make_symbolic(&payload, sizeof(payload), "payload");
+
+  (void)guarded_dispatch(selector, payload, 0xc0def00du);
+  return 0;
+}

headers/gensym/branch.hpp

@@ -5,9 +5,10 @@
 
 inline std::monostate async_exec_block(
     std::monostate (*f)(SS&, std::function<std::monostate(SS&, PtrVal)>),
-    SS ss, std::function<std::monostate(SS&, PtrVal)> k) {
+    BlockLabel target_block, SS ss, std::function<std::monostate(SS&, PtrVal)> k) {
   if (can_par_tp()) {
-    tp.add_task(ss.get_ssid(), [f, ss=std::move(ss), k]{ return f((SS&)ss, k); });
+    auto task_id = ss.get_ssid();
+    tp.add_task(task_id, target_block, [f, ss=std::move(ss), k]{ return f((SS&)ss, k); });
     return std::monostate{};
   }
   return f(ss, k);
@@ -55,6 +56,7 @@ sym_exec_br(SS& ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond,
 
 inline std::monostate
 sym_exec_br_k(SS& ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond,
+              BlockLabel t_block, BlockLabel f_block,
               std::function<std::monostate(SS&, std::function<std::monostate(SS&, PtrVal)>)> tf,
               std::function<std::monostate(SS&, std::function<std::monostate(SS&, PtrVal)>)> ff,
               std::function<std::monostate(SS&, PtrVal)> k) {
@@ -69,11 +71,13 @@ sym_exec_br_k(SS& ss, unsigned int block_id, PtrVal t_cond, PtrVal f_cond,
     tbr_ss.add_PC(t_cond);
     fbr_ss.add_PC(f_cond);
     if (can_par_tp()) {
-      tp.add_task(tbr_ss.get_ssid(), [tf, block_id, tbr_ss=std::move(tbr_ss), k]{
+      auto t_task_id = tbr_ss.get_ssid();
+      auto f_task_id = fbr_ss.get_ssid();
+      tp.add_task(t_task_id, t_block, [tf, block_id, tbr_ss=std::move(tbr_ss), k]{
         cov().inc_branch(block_id, 0);
         return tf((SS&)tbr_ss, k);
       });
-      tp.add_task(fbr_ss.get_ssid(), [ff, block_id, fbr_ss=std::move(fbr_ss), k]{
+      tp.add_task(f_task_id, f_block, [ff, block_id, fbr_ss=std::move(fbr_ss), k]{
         cov().inc_branch(block_id, 1);
         return ff((SS&)fbr_ss, k);
       });
@@ -110,7 +114,7 @@ br_k(SS& ss, PtrVal t_cond, PtrVal f_cond,
     else return ff(ss, k);
   }
   // FIXME: pass correct current block id
-  return sym_exec_br_k(ss, 0, t_cond, f_cond, tf, ff, k);
+  return sym_exec_br_k(ss, 0, t_cond, f_cond, unknown_block_id, unknown_block_id, tf, ff, k);
 }
 
 inline immer::flex_vector<std::pair<SS, PtrVal>>
@@ -178,7 +182,9 @@ array_lookup_k(SS& ss, PtrVal base, PtrVal offset, size_t esize,
       auto new_loc = baseloc + (offset_val*esize);
       auto new_ss = (1 == cnt) ? ss.add_PC(t_cond) : ss.fork().add_PC(t_cond);
       if (can_par_tp()) {
-        tp.add_task(new_ss.get_ssid(), [new_loc=std::move(new_loc), new_ss=std::move(new_ss), k]{ return k((SS&)new_ss, new_loc); });
+        auto task_block = new_ss.current_block();
+        auto task_id = new_ss.get_ssid();
+        tp.add_task(task_id, task_block, [new_loc=std::move(new_loc), new_ss=std::move(new_ss), k]{ return k((SS&)new_ss, new_loc); });
       } else {
         k(new_ss, new_loc);
       }

headers/gensym/cli.hpp

@@ -55,6 +55,8 @@ inline void set_searcher(std::string& searcher) {
     searcher_kind = SearcherKind::randomPath;
   } else if ("random-weight" == searcher) {
     searcher_kind = SearcherKind::randomWeight;
+  } else if ("coverage-guided" == searcher) {
+    searcher_kind = SearcherKind::coverageGuided;
   } else {
     ABORT("unknown searcher");
   }
@@ -97,6 +99,8 @@ inline void print_help(char* main_name) {
           printf("={stp,z3,disable}");
         } else if (key == "symloc-strategy") {
           printf("={one,feasible,all}");
+        } else if (key == "search-strategy") {
+          printf("={random-path,random-weight,coverage-guided}");
         } else {
           // TODO: doc for other options
           printf("=<value>");

headers/gensym/defs.hpp

@@ -7,6 +7,7 @@ inline std::mutex dt_lock;
 inline duration<double, std::micro> debug_time = microseconds::zero();
 
 using BlockLabel = int;
+inline constexpr BlockLabel unknown_block_id = -1;
 using Id = int;
 using Addr = unsigned int;
 using IntData = int64_t;
@@ -128,7 +129,7 @@ inline std::ofstream gs_log;
 // Disable output log in stdout
 inline bool stdout_log = true;
 
-enum class SearcherKind { randomPath, randomWeight };
+enum class SearcherKind { randomPath, randomWeight, coverageGuided };
 // The path searcher to be used
 inline SearcherKind searcher_kind = SearcherKind::randomWeight;
 

headers/gensym/external_imp.hpp

@@ -347,7 +347,9 @@ inline std::monostate __llvm_memcpy(SS& state, List<PtrVal>& args, __Cont<std::m
         non_positive_num = 1;
         SS neg_ss = state.copy().add_PC(neg_cond);
         if (can_par_tp()) {
-          tp.add_task(neg_ss.get_ssid(), [neg_ss=std::move(neg_ss), dest, k]{ return k((SS&)neg_ss, dest); });
+          auto task_block = neg_ss.current_block();
+          auto task_id = neg_ss.get_ssid();
+          tp.add_task(task_id, task_block, [neg_ss=std::move(neg_ss), dest, k]{ return k((SS&)neg_ss, dest); });
         } else {
           k(neg_ss, dest);
         }
@@ -361,7 +363,9 @@ inline std::monostate __llvm_memcpy(SS& state, List<PtrVal>& args, __Cont<std::m
         auto conc_args = List<PtrVal>{dest, src, conc_size};
         SS conc_state = curr_state.copy().add_PC(result[i].first);
         if (can_par_tp()) {
-          tp.add_task(conc_state.get_ssid(), [conc_state=std::move(conc_state), conc_args=std::move(conc_args), k]{ return __llvm_memcpy((SS&)conc_state, (List<PtrVal>&)conc_args, k); });
+          auto task_block = conc_state.current_block();
+          auto task_id = conc_state.get_ssid();
+          tp.add_task(task_id, task_block, [conc_state=std::move(conc_state), conc_args=std::move(conc_args), k]{ return __llvm_memcpy((SS&)conc_state, (List<PtrVal>&)conc_args, k); });
         } else {
           __llvm_memcpy(conc_state, conc_args, k);
         }
@@ -412,7 +416,9 @@ inline std::monostate __llvm_memcpy(SS& state, List<PtrVal>& args, __Cont<std::m
       SS conc_state = curr_state.copy().add_PC(result[i].first);
 
       if (can_par_tp()) {
-        tp.add_task(conc_state.get_ssid(), [conc_state=std::move(conc_state), conc_args=std::move(conc_args), k]{ return __llvm_memcpy((SS&)conc_state, (List<PtrVal>&)conc_args, k); });
+        auto task_block = conc_state.current_block();
+        auto task_id = conc_state.get_ssid();
+        tp.add_task(task_id, task_block, [conc_state=std::move(conc_state), conc_args=std::move(conc_args), k]{ return __llvm_memcpy((SS&)conc_state, (List<PtrVal>&)conc_args, k); });
       } else {
         __llvm_memcpy(conc_state, conc_args, k);
       }
@@ -485,7 +491,9 @@ inline std::monostate __llvm_memcpy(SS& state, List<PtrVal>& args, __Cont<std::m
       SS conc_state = curr_state.copy().add_PC(result[i].first);
 
       if (can_par_tp()) {
-        tp.add_task(conc_state.get_ssid(), [conc_state=std::move(conc_state), conc_args=std::move(conc_args), k]{ return __llvm_memcpy((SS&)conc_state, (List<PtrVal>&)conc_args, k); });
+        auto task_block = conc_state.current_block();
+        auto task_id = conc_state.get_ssid();
+        tp.add_task(task_id, task_block, [conc_state=std::move(conc_state), conc_args=std::move(conc_args), k]{ return __llvm_memcpy((SS&)conc_state, (List<PtrVal>&)conc_args, k); });
       } else {
         __llvm_memcpy(conc_state, conc_args, k);
       }

headers/gensym/libcpolyfill.hpp

@@ -7,9 +7,9 @@ inline std::monostate gs_dummy(SS&, Args, Cont) {
   std::cout << "Warning: invoking gs_dummy, some path is not continued!\n";
   return std::monostate{};
 }
-inline std::monostate start_gs_main(SS& state, Args args, Cont cont) {
+inline std::monostate start_gs_main(SS& state, Args args, Cont cont, BlockLabel entry_block) {
   if (can_par_tp()) {
-    add_task(1, [=] () mutable { return gs_main(state, args, cont); });
+    add_task(1, entry_block, [=] () mutable { return gs_main(state, args, cont); });
     return std::monostate{};
   }
   return gs_main(state, args, cont);

headers/gensym/metadata.hpp

@@ -5,13 +5,19 @@ class MetaData: public Printable {
 public:
     uint64_t ssid;
     BlockLabel bb;
+    BlockLabel current_bb;
     bool has_cover_new;
     List<SymObj> sym_objs;
     List<PtrVal> preferred_cex;
 
     MetaData(uint64_t ssid, BlockLabel bb, bool covernew, List<SymObj> sym_objs, List<PtrVal> preferred_cex) :
-      ssid(ssid), bb(bb), has_cover_new(covernew), sym_objs(sym_objs), preferred_cex(preferred_cex) {}
-    MetaData fork() { return MetaData(ss_fork(ssid), bb, false, sym_objs, preferred_cex); }
+      ssid(ssid), bb(bb), current_bb(unknown_block_id), has_cover_new(covernew),
+      sym_objs(sym_objs), preferred_cex(preferred_cex) {}
+    MetaData fork() {
+      MetaData result(ss_fork(ssid), bb, false, sym_objs, preferred_cex);
+      result.current_bb = current_bb;
+      return result;
+    }
     // XXX(GW): what count_name does? just check existence?
     int count_name(const std::string& name) {
       for (auto symobj : sym_objs) {
@@ -24,6 +30,7 @@ class MetaData: public Printable {
       ss << "MetaData(" <<
         "ssid : " << ssid << ", " <<
         "bb : " << bb << ", " <<
+        "current_bb : " << current_bb << ", " <<
         "has_cover_new : " << has_cover_new << ", " <<
         "sym_objs : " << vec_to_string<List, SymObj>(sym_objs) <<
         "preferred_cex : " << vec_to_string<List, PtrVal>(preferred_cex) << ")";
@@ -32,8 +39,8 @@ class MetaData: public Printable {
 
     void add_incoming_block(BlockLabel blabel) { bb = blabel; }
     void cover_block(BlockLabel new_bb) {
-      bool is_cover_new = cov().is_uncovered(new_bb);
-      cov().inc_block(new_bb);
+      current_bb = new_bb;
+      bool is_cover_new = cov().inc_block(new_bb);
       has_cover_new = has_cover_new | is_cover_new;
     }
     void add_symbolic(const std::string& name, int size, bool is_whole) {