@@ -152,6 +152,21 @@ trait StagedWasmEvaluator extends SAIOps {
152152 ()
153153 }
154154
155+ def evalSymbolic (ty : ValueType ,
156+ rest : List [Instr ],
157+ kont : Context => Rep [Cont [Unit ]],
158+ mkont : Rep [MCont [Unit ]],
159+ trail : Trail [Unit ])(implicit ctx : Context ) = {
160+ Stack .popC(ty)
161+ val id = Stack .popS(ty)
162+ val symVal = id.makeSymbolic(ty)
163+ val num = SymEnv .read(symVal.s)
164+ Stack .pushC(StagedConcreteNum (ty, num))
165+ Stack .pushS(symVal)
166+ val newCtx = ctx.pop()._2.push(ty)
167+ eval(rest, kont, mkont, trail)(newCtx)
168+ }
169+
155170 def eval (insts : List [Instr ],
156171 kont : Context => Rep [Cont [Unit ]],
157172 mkont : Rep [MCont [Unit ]],
@@ -174,15 +189,7 @@ trait StagedWasmEvaluator extends SAIOps {
174189 Stack .pushS(toStagedSymbolicNum(num))
175190 val newCtx = ctx.push(num.tipe(module))
176191 eval(rest, kont, mkont, trail)(newCtx)
177- case Symbolic (ty) =>
178- Stack .popC(ty)
179- val id = Stack .popS(ty)
180- val symVal = id.makeSymbolic(ty)
181- val num = SymEnv .read(symVal.s)
182- Stack .pushC(StagedConcreteNum (ty, num))
183- Stack .pushS(symVal)
184- val newCtx = ctx.pop()._2.push(ty)
185- eval(rest, kont, mkont, trail)(newCtx)
192+ case Symbolic (ty) => evalSymbolic(ty, rest, kont, mkont, trail)(ctx)
186193 case LocalGet (i) =>
187194 Stack .pushC(Frames .getC(i))
188195 Stack .pushS(Frames .getS(i))
@@ -530,7 +537,15 @@ trait StagedWasmEvaluator extends SAIOps {
530537 val s = Stack .popS(ty)
531538 runtimeAssert(v.toInt != 0 )
532539 eval(rest, kont, mkont, trail)(newCtx)
533- case Import (_, _, _) => throw new Exception (s " Unknown import at $funcIndex" )
540+ case Import (" i32" , " symbolic" , _) =>
541+ evalSymbolic(NumType (I32Type ), rest, kont, mkont, trail)(ctx)
542+ case Import (" i32" , " sym_assume" , _) =>
543+ // TODO: implement sym_assume
544+ eval(rest, kont, mkont, trail)(ctx.pop()._2)
545+ case Import (" i32" , " sym_assert" , _) =>
546+ // TODO: implement sym_assert
547+ eval(rest, kont, mkont, trail)(ctx.pop()._2)
548+ case Import (m, f, _) => throw new Exception (s " Unknown import $m. $f at $funcIndex" )
534549 case _ => throw new Exception (s " Definition at $funcIndex is not callable " )
535550 }
536551 }
0 commit comments