Skip to content

Commit 77a4e6f

Browse files
butterunderflowbutterunderflow
committed
type.symbolic instruction
1 parent e1d7fc8 commit 77a4e6f

File tree

3 files changed

+120
-16
lines changed

3 files changed

+120
-16
lines changed

‎headers/wasm/symbolic_rt.hpp

Lines changed: 56 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,19 @@
1010
#include <variant>
1111
#include <vector>
1212

13-
class Symbolic {};
13+
class Symbolic {
14+
public:
15+
Symbolic() {} // TODO: remove this default constructor later
16+
virtual ~Symbolic() = default; // Make Symbolic polymorphic
17+
};
18+
19+
class Symbol : public Symbolic {
20+
public:
21+
Symbol(int id) : id(id) {}
22+
23+
private:
24+
int id;
25+
};
1426

1527
class SymConcrete : public Symbolic {
1628
public:
@@ -26,6 +38,11 @@ struct SymVal {
2638
SymVal() : symptr(nullptr) {}
2739
SymVal(std::shared_ptr<Symbolic> symptr) : symptr(symptr) {}
2840

41+
// data structure operations
42+
SymVal makeSymbolic() const;
43+
44+
// arithmetic operations
45+
SymVal is_zero() const;
2946
SymVal add(const SymVal &other) const;
3047
SymVal minus(const SymVal &other) const;
3148
SymVal mul(const SymVal &other) const;
@@ -54,39 +71,53 @@ struct SymBinary : Symbolic {
5471
};
5572

5673
inline SymVal SymVal::add(const SymVal &other) const {
57-
return SymVal(std::make_shared<SymBinary>(ADD, this, other));
74+
return SymVal(std::make_shared<SymBinary>(ADD, *this, other));
5875
}
5976

6077
inline SymVal SymVal::minus(const SymVal &other) const {
61-
return SymVal(std::make_shared<SymBinary>(SUB, this, other));
78+
return SymVal(std::make_shared<SymBinary>(SUB, *this, other));
6279
}
6380

6481
inline SymVal SymVal::mul(const SymVal &other) const {
65-
return SymVal(std::make_shared<SymBinary>(MUL, this, other));
82+
return SymVal(std::make_shared<SymBinary>(MUL, *this, other));
6683
}
6784

6885
inline SymVal SymVal::div(const SymVal &other) const {
69-
return SymVal(std::make_shared<SymBinary>(DIV, this, other));
86+
return SymVal(std::make_shared<SymBinary>(DIV, *this, other));
7087
}
7188

7289
inline SymVal SymVal::eq(const SymVal &other) const {
73-
return SymVal(std::make_shared<SymBinary>(EQ, this, other));
90+
return SymVal(std::make_shared<SymBinary>(EQ, *this, other));
7491
}
7592

7693
inline SymVal SymVal::neq(const SymVal &other) const {
77-
return SymVal(std::make_shared<SymBinary>(NEQ, this, other));
94+
return SymVal(std::make_shared<SymBinary>(NEQ, *this, other));
7895
}
7996
inline SymVal SymVal::lt(const SymVal &other) const {
80-
return SymVal(std::make_shared<SymBinary>(LT, this, other));
97+
return SymVal(std::make_shared<SymBinary>(LT, *this, other));
8198
}
8299
inline SymVal SymVal::leq(const SymVal &other) const {
83-
return SymVal(std::make_shared<SymBinary>(LEQ, this, other));
100+
return SymVal(std::make_shared<SymBinary>(LEQ, *this, other));
84101
}
85102
inline SymVal SymVal::gt(const SymVal &other) const {
86-
return SymVal(std::make_shared<SymBinary>(GT, this, other));
103+
return SymVal(std::make_shared<SymBinary>(GT, *this, other));
87104
}
88105
inline SymVal SymVal::geq(const SymVal &other) const {
89-
return SymVal(std::make_shared<SymBinary>(GEQ, this, other));
106+
return SymVal(std::make_shared<SymBinary>(GEQ, *this, other));
107+
}
108+
inline SymVal SymVal::is_zero() const {
109+
return SymVal(std::make_shared<SymBinary>(EQ, *this, Concrete(I32V(0))));
110+
}
111+
112+
inline SymVal SymVal::makeSymbolic() const {
113+
auto concrete = dynamic_cast<SymConcrete *>(symptr.get());
114+
if (concrete) {
115+
// If the symbolic value is a concrete value, use it to create a symbol
116+
return SymVal(std::make_shared<Symbol>(concrete->value.toInt()));
117+
} else {
118+
throw std::runtime_error(
119+
"Cannot make symbolic a non-concrete symbolic value");
120+
}
90121
}
91122

92123
class SymStack_t {
@@ -173,11 +204,11 @@ struct Node {
173204
int Node::current_id = 0;
174205

175206
struct IfElseNode : Node {
176-
Symbolic cond;
207+
SymVal cond;
177208
std::unique_ptr<NodeBox> true_branch;
178209
std::unique_ptr<NodeBox> false_branch;
179210

180-
IfElseNode(Symbolic cond)
211+
IfElseNode(SymVal cond)
181212
: cond(cond), true_branch(std::make_unique<NodeBox>()),
182213
false_branch(std::make_unique<NodeBox>()) {}
183214

@@ -263,7 +294,7 @@ class ExploreTree_t {
263294
public:
264295
explicit ExploreTree_t()
265296
: root(std::make_unique<NodeBox>()), cursor(root.get()) {}
266-
std::monostate fillIfElseNode(Symbolic cond) {
297+
std::monostate fillIfElseNode(SymVal cond) {
267298
// fill the current node with an ifelse branch node
268299
cursor->node = std::make_unique<IfElseNode>(cond);
269300
return std::monostate();
@@ -300,4 +331,15 @@ class ExploreTree_t {
300331

301332
static ExploreTree_t ExploreTree;
302333

334+
class SymEnv_t {
335+
public:
336+
Num read(SymVal sym) {
337+
// Read a symbolic value from the symbolic environment
338+
// For now, we just return a zero
339+
return Num(0);
340+
}
341+
};
342+
343+
static SymEnv_t SymEnv;
344+
303345
#endif // WASM_SYMBOLIC_RT_HPP

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

Lines changed: 60 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,15 @@ trait StagedWasmEvaluator extends SAIOps {
5757
case NumType(F32Type) => 4
5858
case NumType(F64Type) => 8
5959
}
60+
61+
def toTagger: (Rep[Num], Rep[SymVal]) => StagedNum = {
62+
ty match {
63+
case NumType(I32Type) => I32
64+
case NumType(I64Type) => I64
65+
case NumType(F32Type) => F32
66+
case NumType(F64Type) => F64
67+
}
68+
}
6069
}
6170

6271
case class Context(
@@ -121,6 +130,14 @@ trait StagedWasmEvaluator extends SAIOps {
121130
case WasmConst(num) =>
122131
val newCtx = Stack.push(toStagedNum(num))
123132
eval(rest, kont, mkont, trail)(newCtx)
133+
case Symbolic(ty) =>
134+
val (id, newCtx1) = Stack.pop()
135+
val symVal = id.makeSymbolic()
136+
val concVal = SymEnv.read(symVal)
137+
val tagger = ty.toTagger
138+
val value = tagger(concVal, symVal)
139+
val newCtx2 = Stack.push(value)(newCtx1)
140+
eval(rest, kont, mkont, trail)(newCtx2)
124141
case LocalGet(i) =>
125142
val newCtx = Stack.push(Frames.get(i))
126143
eval(rest, kont, mkont, trail)(newCtx)
@@ -326,6 +343,10 @@ trait StagedWasmEvaluator extends SAIOps {
326343
val (v, newCtx) = Stack.pop()
327344
println(v.toInt)
328345
eval(rest, kont, mkont, trail)(newCtx)
346+
case Import("console", "assert", _) =>
347+
val (v, newCtx) = Stack.pop()
348+
runtimeAssert(v.toInt != 0)
349+
eval(rest, kont, mkont, trail)(newCtx)
329350
case Import(_, _, _) => throw new Exception(s"Unknown import at $funcIndex")
330351
case _ => throw new Exception(s"Definition at $funcIndex is not callable")
331352
}
@@ -414,6 +435,10 @@ trait StagedWasmEvaluator extends SAIOps {
414435
evalTop(temp, main)
415436
}
416437

438+
def runtimeAssert(b: Rep[Boolean]): Rep[Unit] = {
439+
"assert-true".reflectCtrlWith[Unit](b)
440+
}
441+
417442
// stack operations
418443
object Stack {
419444
def shift(offset: Int, size: Int)(ctx: Context): Context = {
@@ -598,6 +623,12 @@ trait StagedWasmEvaluator extends SAIOps {
598623
}
599624
}
600625

626+
object SymEnv {
627+
def read(sym: Rep[SymVal]): Rep[Num] = {
628+
"sym-env-read".reflectCtrlWith[Num](sym)
629+
}
630+
}
631+
601632
// runtime Num type
602633
implicit class StagedNumOps(num: StagedNum) {
603634

@@ -622,6 +653,10 @@ trait StagedWasmEvaluator extends SAIOps {
622653
case I64(x_c, x_s) => I64("popcnt".reflectCtrlWith[Num](x_c), "sym-popcnt".reflectCtrlWith[SymVal](x_s))
623654
}
624655

656+
def makeSymbolic(): Rep[SymVal] = {
657+
"make-symbolic".reflectCtrlWith[SymVal](num.s)
658+
}
659+
625660
def +(rhs: StagedNum): StagedNum = {
626661
(num, rhs) match {
627662
case (I32(x_c, x_s), I32(y_c, y_s)) => I32("binary-add".reflectCtrlWith[Num](x_c, y_c), "sym-binary-add".reflectCtrlWith[SymVal](x_s, y_s))
@@ -778,6 +813,7 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
778813
override def mayInline(n: Node): Boolean = n match {
779814
case Node(_, "stack-pop", _, _)
780815
| Node(_, "stack-peek", _, _)
816+
| Node(_, "sym-stack-pop", _, _)
781817
=> false
782818
case _ => super.mayInline(n)
783819
}
@@ -874,8 +910,6 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
874910
shallow(s_num); emit(".is_zero()")
875911
case Node(_, "binary-add", List(lhs, rhs), _) =>
876912
shallow(lhs); emit(" + "); shallow(rhs)
877-
case Node(_, "sym-binary-add", List(lhs, rhs), _) =>
878-
shallow(lhs); emit(" + "); shallow(rhs)
879913
case Node(_, "binary-sub", List(lhs, rhs), _) =>
880914
shallow(lhs); emit(" - "); shallow(rhs)
881915
case Node(_, "binary-mul", List(lhs, rhs), _) =>
@@ -908,8 +942,32 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
908942
shallow(lhs); emit(" >= "); shallow(rhs)
909943
case Node(_, "relation-geu", List(lhs, rhs), _) =>
910944
shallow(lhs); emit(" >= "); shallow(rhs)
945+
case Node(_, "sym-binary-add", List(lhs, rhs), _) =>
946+
shallow(lhs); emit(".add("); shallow(rhs); emit(")")
947+
case Node(_, "sym-binary-mul", List(lhs, rhs), _) =>
948+
shallow(lhs); emit(".mul("); shallow(rhs); emit(")")
949+
case Node(_, "sym-binary-div", List(lhs, rhs), _) =>
950+
shallow(lhs); emit(".div("); shallow(rhs); emit(")")
951+
case Node(_, "sym-relation-le", List(lhs, rhs), _) =>
952+
shallow(lhs); emit(".leq("); shallow(rhs); emit(")")
953+
case Node(_, "sym-relation-leu", List(lhs, rhs), _) =>
954+
shallow(lhs); emit(".leu("); shallow(rhs); emit(")")
955+
case Node(_, "sym-relation-ge", List(lhs, rhs), _) =>
956+
shallow(lhs); emit(".ge("); shallow(rhs); emit(")")
957+
case Node(_, "sym-relation-geu", List(lhs, rhs), _) =>
958+
shallow(lhs); emit(".geu("); shallow(rhs); emit(")")
959+
case Node(_, "sym-relation-eq", List(lhs, rhs), _) =>
960+
shallow(lhs); emit(".eq("); shallow(rhs); emit(")")
961+
case Node(_, "sym-relation-ne", List(lhs, rhs), _) =>
962+
shallow(lhs); emit(".neq("); shallow(rhs); emit(")")
911963
case Node(_, "num-to-int", List(num), _) =>
912964
shallow(num); emit(".toInt()")
965+
case Node(_, "make-symbolic", List(num), _) =>
966+
shallow(num); emit(".makeSymbolic()")
967+
case Node(_, "sym-env-read", List(sym), _) =>
968+
emit("SymEnv.read("); shallow(sym); emit(")")
969+
case Node(_, "assert-true", List(cond), _) =>
970+
emit("assert("); shallow(cond); emit(")")
913971
case Node(_, "tree-fill-if-else", List(s), _) =>
914972
emit("ExploreTree.fillIfElseNode("); shallow(s); emit(")")
915973
case Node(_, "tree-move-cursor", List(b), _) =>

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,4 +30,8 @@ class TestStagedConcolicEval extends FunSuite {
3030
}
3131

3232
test("ack-cpp") { testFileToCpp("./benchmarks/wasm/ack.wat", Some("real_main"), expect=Some(List(7))) }
33+
34+
test("bug-finding") {
35+
testFileToCpp("./benchmarks/wasm/branch-strip-buggy.wat", Some("real_main"))
36+
}
3337
}

0 commit comments

Comments
 (0)