Skip to content

Commit 2143050

Browse files
butterunderflowbutterunderflow
committed
maintain a symbolic stack during the execution
1 parent 27e3e32 commit 2143050

File tree

5 files changed

+152
-13
lines changed

5 files changed

+152
-13
lines changed

‎headers/wasm.hpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,6 @@
22
#define WASM_HEADERS
33

44
#include "wasm/concrete_rt.hpp"
5+
#include "wasm/symbolic_rt.hpp"
56

67
#endif

‎headers/wasm/concrete_rt.hpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
#ifndef WASM_CONCRETE_RT_HPP
2+
#define WASM_CONCRETE_RT_HPP
3+
14
#include <cassert>
25
#include <cstdint>
36
#include <cstdio>
@@ -200,4 +203,6 @@ struct Memory_t {
200203
}
201204
};
202205

203-
static Memory_t Memory(1); // 1 page memory
206+
static Memory_t Memory(1); // 1 page memory
207+
208+
#endif // WASM_CONCRETE_RT_HPP

‎headers/wasm/symbolic_rt.hpp

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
#ifndef WASM_SYMBOLIC_RT_HPP
2+
#define WASM_SYMBOLIC_RT_HPP
3+
4+
#include "concrete_rt.hpp"
5+
#include <variant>
6+
7+
class SymVal {
8+
public:
9+
SymVal operator+(const SymVal &other) const {
10+
// Define how to add two symbolic values
11+
// Not implemented yet
12+
return SymVal();
13+
}
14+
15+
SymVal is_zero() const {
16+
// Check if the symbolic value is zero
17+
// Not implemented yet
18+
return SymVal();
19+
}
20+
};
21+
22+
class SymStack_t {
23+
public:
24+
void push(SymVal val) {
25+
// Push a symbolic value to the stack
26+
// Not implemented yet
27+
}
28+
29+
SymVal pop() {
30+
// Pop a symbolic value from the stack
31+
// Not implemented yet
32+
return SymVal();
33+
}
34+
35+
SymVal peek() { return SymVal(); }
36+
};
37+
38+
static SymStack_t SymStack;
39+
40+
class SymFrames_t {
41+
public:
42+
void pushFrame(int size) {
43+
// Push a new frame with the given size
44+
// Not implemented yet
45+
}
46+
std::monostate popFrame(int size) {
47+
// Pop the frame of the given size
48+
// Not implemented yet
49+
return std::monostate();
50+
}
51+
52+
SymVal get(int index) {
53+
// Get the symbolic value at the given index
54+
// Not implemented yet
55+
return SymVal();
56+
}
57+
58+
void set(int index, SymVal val) {
59+
// Set the symbolic value at the given index
60+
// Not implemented yet
61+
}
62+
};
63+
64+
static SymFrames_t SymFrames;
65+
66+
static SymVal Concrete(Num num) {
67+
// Convert a concrete number to a symbolic value
68+
// Not implemented yet
69+
return SymVal();
70+
}
71+
72+
#endif // WASM_SYMBOLIC_RT_HPP

‎src/main/scala/wasm/StagedConcolicMiniWasm.scala

Lines changed: 40 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ trait StagedWasmEvaluator extends SAIOps {
4040
case class F32(i: Rep[Num], s: Rep[SymVal]) extends StagedNum
4141
case class F64(i: Rep[Num], s: Rep[SymVal]) extends StagedNum
4242

43-
implicit def toStagedNum(num: Num): StagedNum = {
43+
def toStagedNum(num: Num): StagedNum = {
4444
num match {
4545
case I32V(_) => I32(num, Concrete(num))
4646
case I64V(_) => I64(num, Concrete(num))
@@ -118,7 +118,7 @@ trait StagedWasmEvaluator extends SAIOps {
118118
val (_, newCtx) = Stack.pop()
119119
eval(rest, kont, mkont, trail)(newCtx)
120120
case WasmConst(num) =>
121-
val newCtx = Stack.push(num)
121+
val newCtx = Stack.push(toStagedNum(num))
122122
eval(rest, kont, mkont, trail)(newCtx)
123123
case LocalGet(i) =>
124124
val newCtx = Stack.push(Frames.get(i))
@@ -155,7 +155,10 @@ trait StagedWasmEvaluator extends SAIOps {
155155
case MemorySize => ???
156156
case MemoryGrow =>
157157
val (delta, newCtx1) = Stack.pop()
158-
val newCtx2 = Stack.push(Values.I32V(Memory.grow(delta.toInt)))(newCtx1)
158+
val ret = Memory.grow(delta.toInt)
159+
val retNum = Values.I32V(ret)
160+
val retSym = "Concrete".reflectCtrlWith[SymVal](retNum)
161+
val newCtx2 = Stack.push(I32(retNum, retSym))(newCtx1)
159162
eval(rest, kont, mkont, trail)(newCtx2)
160163
case MemoryFill => ???
161164
case Unreachable => unreachable()
@@ -220,6 +223,7 @@ trait StagedWasmEvaluator extends SAIOps {
220223
val newRestCtx = Stack.shift(offset, funcTy.out.size)(restCtx)
221224
eval(rest, kont, mk, trail)(newRestCtx)
222225
})
226+
// TODO: put the cond.s to path condition
223227
if (cond.toInt != 0) {
224228
eval(thn, restK _, mkont, restK _ :: trail)(newCtx)
225229
} else {
@@ -232,6 +236,7 @@ trait StagedWasmEvaluator extends SAIOps {
232236
case BrIf(label) =>
233237
val (cond, newCtx) = Stack.pop()
234238
info(s"The br_if(${label})'s condition is ", cond.toInt)
239+
// TODO: put the cond.s to path condition
235240
if (cond.toInt != 0) {
236241
info(s"Jump to $label")
237242
trail(label)(newCtx)(mkont)
@@ -320,7 +325,7 @@ trait StagedWasmEvaluator extends SAIOps {
320325
}
321326

322327
def evalTestOp(op: TestOp, value: StagedNum): StagedNum = op match {
323-
case Eqz(_) => Values.I32V(if (value.toInt == 0) 1 else 0)
328+
case Eqz(_) => value.isZero
324329
}
325330

326331
def evalUnaryOp(op: UnaryOp, value: StagedNum): StagedNum = op match {
@@ -523,6 +528,7 @@ trait StagedWasmEvaluator extends SAIOps {
523528
I32("I32V".reflectCtrlWith[Num]("memory-load-int".reflectCtrlWith[Int](base, offset)), "sym-load-int-todo".reflectCtrlWith[SymVal](base, offset))
524529
}
525530

531+
// Returns the previous memory size on success, or -1 if the memory cannot be grown.
526532
def grow(delta: Rep[Int]): Rep[Int] = {
527533
"memory-grow".reflectCtrlWith[Int](delta)
528534
}
@@ -539,12 +545,12 @@ trait StagedWasmEvaluator extends SAIOps {
539545

540546
// runtime values
541547
object Values {
542-
def I32V(i: Rep[Int]): StagedNum = {
543-
I32("I32V".reflectCtrlWith[Num](i), "Concrete".reflectCtrlWith[SymVal]("I32V".reflectCtrlWith[Num](i)))
548+
def I32V(i: Rep[Int]): Rep[Num] = {
549+
"I32V".reflectCtrlWith[Num](i)
544550
}
545551

546-
def I64V(i: Rep[Long]): StagedNum = {
547-
I64("I64V".reflectCtrlWith[Num](i), "Concrete".reflectCtrlWith[SymVal]("I64V".reflectCtrlWith[Num](i)))
552+
def I64V(i: Rep[Long]): Rep[Num] = {
553+
"I64V".reflectCtrlWith[Num](i)
548554
}
549555
}
550556

@@ -574,6 +580,10 @@ trait StagedWasmEvaluator extends SAIOps {
574580

575581
def toInt: Rep[Int] = "num-to-int".reflectCtrlWith[Int](num.i)
576582

583+
def isZero(): StagedNum = num match {
584+
case I32(x_c, x_s) => I32(Values.I32V("is-zero".reflectCtrlWith[Int](num.toInt)), "sym-is-zero".reflectCtrlWith[SymVal](x_s))
585+
}
586+
577587
def clz(): StagedNum = num match {
578588
case I32(x_c, x_s) => I32("clz".reflectCtrlWith[Num](x_c), "sym-clz".reflectCtrlWith[SymVal](x_s))
579589
case I64(x_c, x_s) => I64("clz".reflectCtrlWith[Num](x_c), "sym-clz".reflectCtrlWith[SymVal](x_s))
@@ -750,13 +760,16 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
750760
else if (m.toString.endsWith("Global")) "Global"
751761
else if (m.toString.endsWith("I32V")) "I32V"
752762
else if (m.toString.endsWith("I64V")) "I64V"
763+
else if (m.toString.endsWith("SymVal")) "SymVal"
764+
753765
else super.remap(m)
754766
}
755767

756-
// for now, the traverse/shallow is same as the scala backend's
757768
override def traverse(n: Node): Unit = n match {
758769
case Node(_, "stack-push", List(value), _) =>
759770
emit("Stack.push("); shallow(value); emit(");\n")
771+
case Node(_, "sym-stack-push", List(s_value), _) =>
772+
emit("SymStack.push("); shallow(s_value); emit(");\n")
760773
case Node(_, "stack-drop", List(n), _) =>
761774
emit("Stack.drop("); shallow(n); emit(");\n")
762775
case Node(_, "stack-init", _, _) =>
@@ -765,12 +778,14 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
765778
emit("Stack.print();\n")
766779
case Node(_, "frame-push", List(i), _) =>
767780
emit("Frames.pushFrame("); shallow(i); emit(");\n")
781+
case Node(_, "sym-frame-push", List(i), _) =>
782+
emit("SymFrames.pushFrame("); shallow(i); emit(");\n")
768783
case Node(_, "frame-pop", List(i), _) =>
769784
emit("Frames.popFrame("); shallow(i); emit(");\n")
770-
case Node(_, "frame-putAll", List(args), _) =>
771-
emit("Frames.putAll("); shallow(args); emit(");\n")
772785
case Node(_, "frame-set", List(i, value), _) =>
773786
emit("Frames.set("); shallow(i); emit(", "); shallow(value); emit(");\n")
787+
case Node(_, "sym-frame-set", List(i, s_value), _) =>
788+
emit("SymFrames.set("); shallow(i); emit(", "); shallow(s_value); emit(");\n")
774789
case Node(_, "global-set", List(i, value), _) =>
775790
emit("Global.globalSet("); shallow(i); emit(", "); shallow(value); emit(");\n")
776791
// Note: The following code is copied from the traverse of CppBackend.scala, try to avoid duplicated code
@@ -787,10 +802,11 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
787802
case _ => super.traverse(n)
788803
}
789804

790-
// code generation for pure nodes
791805
override def shallow(n: Node): Unit = n match {
792806
case Node(_, "frame-get", List(i), _) =>
793807
emit("Frames.get("); shallow(i); emit(")")
808+
case Node(_, "sym-frame-get", List(i), _) =>
809+
emit("SymFrames.get("); shallow(i); emit(")")
794810
case Node(_, "stack-drop", List(n), _) =>
795811
emit("Stack.drop("); shallow(n); emit(")")
796812
case Node(_, "stack-push", List(value), _) =>
@@ -799,10 +815,16 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
799815
emit("Stack.shift("); shallow(offset); emit(", "); shallow(size); emit(")")
800816
case Node(_, "stack-pop", _, _) =>
801817
emit("Stack.pop()")
818+
case Node(_, "sym-stack-pop", _, _) =>
819+
emit("SymStack.pop()")
802820
case Node(_, "frame-pop", List(i), _) =>
803821
emit("Frames.popFrame("); shallow(i); emit(")")
822+
case Node(_, "sym-frame-pop", List(i), _) =>
823+
emit("SymFrames.popFrame("); shallow(i); emit(")")
804824
case Node(_, "stack-peek", _, _) =>
805825
emit("Stack.peek()")
826+
case Node(_, "sym-stack-peek", _, _) =>
827+
emit("SymStack.peek()")
806828
case Node(_, "stack-take", List(n), _) =>
807829
emit("Stack.take("); shallow(n); emit(")")
808830
case Node(_, "slice-reverse", List(slice), _) =>
@@ -817,8 +839,14 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
817839
emit("Stack.size()")
818840
case Node(_, "global-get", List(i), _) =>
819841
emit("Global.globalGet("); shallow(i); emit(")")
842+
case Node(_, "is-zero", List(num), _) =>
843+
emit("(0 == "); shallow(num); emit(")")
844+
case Node(_, "sym-is-zero", List(s_num), _) =>
845+
shallow(s_num); emit(".is_zero()")
820846
case Node(_, "binary-add", List(lhs, rhs), _) =>
821847
shallow(lhs); emit(" + "); shallow(rhs)
848+
case Node(_, "sym-binary-add", List(lhs, rhs), _) =>
849+
shallow(lhs); emit(" + "); shallow(rhs)
822850
case Node(_, "binary-sub", List(lhs, rhs), _) =>
823851
shallow(lhs); emit(" - "); shallow(rhs)
824852
case Node(_, "binary-mul", List(lhs, rhs), _) =>

‎src/test/scala/genwasym/TestStagedConcolicEval.scala

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
package gensym.wasm
2+
3+
import org.scalatest.FunSuite
4+
5+
import lms.core.stub.Adapter
6+
7+
import gensym.wasm.miniwasm.{ModuleInstance}
8+
import gensym.wasm.parser._
9+
import gensym.wasm.stagedconcolicminiwasm._
10+
11+
class TestStagedConcolicEval extends FunSuite {
12+
def testFileToCpp(filename: String, main: Option[String] = None, expect: Option[List[Float]]=None) = {
13+
val moduleInst = ModuleInstance(Parser.parseFile(filename))
14+
val cppFile = s"$filename.cpp"
15+
val exe = s"$cppFile.exe"
16+
WasmToCppCompiler.compileToExe(moduleInst, main, cppFile, exe, true)
17+
18+
import sys.process._
19+
val result = s"./$exe".!!
20+
println(result)
21+
22+
expect.map(vs => {
23+
val stackValues = result
24+
.split("Stack contents: \n")(1)
25+
.split("\n")
26+
.map(_.toFloat)
27+
.toList
28+
assert(vs == stackValues)
29+
})
30+
}
31+
32+
test("ack-cpp") { testFileToCpp("./benchmarks/wasm/ack.wat", Some("real_main"), expect=Some(List(7))) }
33+
}

0 commit comments

Comments
 (0)