branch in brtable

Author: butterunderflow

benchmarks/wasm/staged/brtable_concolic.wat

@@ -0,0 +1,22 @@
+(module $brtable
+  (global (;0;) (mut i32) (i32.const 1048576))
+  (type (;0;) (func (param i32)))
+  (func (;0;) (type 1) (result i32)
+    i32.const 2
+    (block
+      (block
+        (block
+          i32.const 0
+          i32.symbolic
+          br_table 0 1 2 0 ;; br_table will consume an element from the stack
+        )
+        i32.const 1
+        call 1
+        br 1
+      )
+      i32.const 0
+      call 1
+    )
+  )
+  (import "console" "assert" (func (type 0)))
+  (start 0))

headers/wasm/smt_solver.hpp

@@ -46,7 +46,7 @@ class Solver {
           if (id >= result.size()) {
             result.resize(id + 1);
           }
-          result[id] = Num(value.get_numeral_int());
+          result[id] = Num(value.get_numeral_int64());
         } else {
           std::cout << "Find a variable that is not created by GenSym: " << name
                     << std::endl;

src/main/scala/wasm/StagedConcolicMiniWasm.scala

@@ -17,6 +17,7 @@ import gensym.wasm.symbolic.{SymVal}
 import gensym.lmsx.{SAIDriver, StringOps, SAIOps, SAICodeGenBase, CppSAIDriver, CppSAICodeGenBase}
 import gensym.wasm.symbolic.Concrete
 import gensym.wasm.symbolic.ExploreTree
+import gensym.structure.freer.Explore
 
 @virtualize
 trait StagedWasmEvaluator extends SAIOps {
@@ -270,12 +271,20 @@ trait StagedWasmEvaluator extends SAIOps {
         }
         ()
       case BrTable(labels, default) =>
-        val (cond, newCtx) = Stack.pop()
+        val (label, newCtx) = Stack.pop()
         def aux(choices: List[Int], idx: Int): Rep[Unit] = {
           if (choices.isEmpty) trail(default)(newCtx)(mkont)
           else {
-            if (cond.toInt == idx) trail(choices.head)(newCtx)(mkont)
-            else aux(choices.tail, idx + 1)
+            val cond = (label - toStagedNum(I32V(idx))).isZero()
+            ExploreTree.fillWithIfElse(cond.s)
+            if (cond.toInt != 0) {
+              ExploreTree.moveCursor(true)
+              trail(choices.head)(newCtx)(mkont)
+            }
+            else {
+              ExploreTree.moveCursor(false)
+              aux(choices.tail, idx + 1)
+            }
           }
         }
         aux(labels, 0)
@@ -959,6 +968,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
       shallow(lhs); emit(" >= "); shallow(rhs)
     case Node(_, "sym-binary-add", List(lhs, rhs), _) =>
       shallow(lhs); emit(".add("); shallow(rhs); emit(")")
+    case Node(_, "sym-binary-sub", List(lhs, rhs), _) =>
+      shallow(lhs); emit(".minus("); shallow(rhs); emit(")")
     case Node(_, "sym-binary-mul", List(lhs, rhs), _) =>
       shallow(lhs); emit(".mul("); shallow(rhs); emit(")")
     case Node(_, "sym-binary-div", List(lhs, rhs), _) =>

src/test/scala/genwasym/TestStagedConcolicEval.scala

@@ -35,4 +35,8 @@ class TestStagedConcolicEval extends FunSuite {
   test("bug-finding") {
     testFileToCpp("./benchmarks/wasm/branch-strip-buggy.wat", Some("real_main"))
   }
+
+  test("brtable-bug-finding") {
+    testFileToCpp("./benchmarks/wasm/staged/brtable_concolic.wat")
+  }
 }