From 658bc3eeed9b4f9a36cd4794f077e193782e1cd6 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Tue, 10 Mar 2026 22:12:46 -0400 Subject: [PATCH 1/3] support float point load/store (but assuming the symbolic value is concrete) --- headers/wasm/sym_rt.hpp | 10 ++++++++++ src/main/scala/wasm/StagedConcolicMiniWasm.scala | 12 ++++++++++++ 2 files changed, 22 insertions(+) diff --git a/headers/wasm/sym_rt.hpp b/headers/wasm/sym_rt.hpp index 6849f39c..dc9eaa23 100644 --- a/headers/wasm/sym_rt.hpp +++ b/headers/wasm/sym_rt.hpp @@ -396,6 +396,16 @@ class SymMemory_t { return std::monostate{}; } + std::monostate storeSymFloat(int32_t base, int32_t offset, SymVal value) { + assert(value.is_concrete() && "Currently only support concrete symbolic value for float-point values"); + return storeSym(base, offset, value); + } + + std::monostate storeSymDouble(int32_t base, int32_t offset, SymVal value) { + assert(value.is_concrete() && "Currently only support concrete symbolic value for float-point values"); + return storeSymLong(base, offset, value); + } + std::monostate storeSymByte(int32_t addr, SymVal value) { // assume the input value is 8-bit symbolic value bool exists; diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 49361367..1a4dd0cb 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -1085,11 +1085,15 @@ trait StagedMemory extends SAIOps with StagedWasmValueDomains with Continuations def loadC(ty: ValueType, base: Rep[Int], offset: Int): StagedConcreteNum = ty match { case NumType(I32Type) => StagedConcreteNum(NumType(I32Type), "I32V".reflectCtrlWith[Num]("memory-load-int".reflectCtrlWith[Int](base, offset))) case NumType(I64Type) => StagedConcreteNum(NumType(I64Type), "I64V".reflectCtrlWith[Num]("memory-load-long".reflectCtrlWith[Long](base, offset))) + case NumType(F32Type) => StagedConcreteNum(NumType(F32Type), "F32V".reflectCtrlWith[Num]("memory-load-float".reflectCtrlWith[Float](base, offset))) + case NumType(F64Type) => StagedConcreteNum(NumType(F64Type), "F64V".reflectCtrlWith[Num]("memory-load-double".reflectCtrlWith[Double](base, offset))) } def loadS(ty: ValueType, base: Rep[Int], offset: Int): StagedSymbolicNum = ty match { case NumType(I32Type) => StagedSymbolicNum(NumType(I32Type), "sym-load-int".reflectCtrlWith[SymVal](base, offset)) case NumType(I64Type) => StagedSymbolicNum(NumType(I64Type), "sym-load-long".reflectCtrlWith[SymVal](base, offset)) + case NumType(F32Type) => StagedSymbolicNum(NumType(F32Type), "sym-load-float".reflectCtrlWith[SymVal](base, offset)) + case NumType(F64Type) => StagedSymbolicNum(NumType(F64Type), "sym-load-double".reflectCtrlWith[SymVal](base, offset)) } // Returns the previous memory size on success, or -1 if the memory cannot be grown. @@ -2256,6 +2260,10 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { emit("Memory.loadInt("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "memory-load-long", List(base, offset), _) => emit("Memory.loadLong("); shallow(base); emit(", "); shallow(offset); emit(")") + case Node(_, "memory-load-float", List(base, offset), _) => + emit("Memory.loadFloat("); shallow(base); emit(", "); shallow(offset); emit(")") + case Node(_, "memory-load-double", List(base, offset), _) => + emit("Memory.loadDouble("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "memory-grow", List(delta), _) => emit("Memory.grow("); shallow(delta); emit(")") case Node(_, "stack-size", _, _) => @@ -2269,6 +2277,10 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { emit("SymMemory.loadSym("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "sym-load-long", List(base, offset), _) => emit("SymMemory.loadSymLong("); shallow(base); emit(", "); shallow(offset); emit(")") + case Node(_, "sym-load-float", List(base, offset), _) => + emit("SymMemory.loadSymFloat("); shallow(base); emit(", "); shallow(offset); emit(")") + case Node(_, "sym-load-double", List(base, offset), _) => + emit("SymMemory.loadSymDouble("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "sym-memory-grow", List(delta), _) => emit("SymMemory.grow("); shallow(delta); emit(")") // Globals From 075b3ea4b39fe23e201e73da6c69c3839a6dc816 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Tue, 10 Mar 2026 22:37:42 -0400 Subject: [PATCH 2/3] fix memory-initialize with hex escapes in data segments --- src/main/scala/wasm/StagedConcolicMiniWasm.scala | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 1a4dd0cb..7c6330af 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -2039,6 +2039,13 @@ trait StagedWasmEvaluator extends SAIOps func(()) } + // Convert WAT-style hex escapes (\XX) to C++-style (\xXX) + // WAT uses \00, \80 etc. but C++ interprets \8 as invalid octal + def convertWatEscapesToCpp(s: String): String = { + val hexEscape = """\\([0-9a-fA-F]{2})""".r + hexEscape.replaceAllIn(s, m => "\\\\x" + m.group(1)) + } + def initMemory(): Rep[Unit] = { def initMemoryTopFun = topFun((_: Rep[Unit]) => { info("Initializing memory...") @@ -2051,7 +2058,7 @@ trait StagedWasmEvaluator extends SAIOps evalSeq(offsetInstr::Nil, (_: Context) => forwardKont, ((_: Context) => forwardKont)::Nil) val offsetC = Stack.popC(NumType(I32Type)) Stack.popS(NumType(I32Type)) - "memory-initialize".reflectCtrlWith[Unit](offsetC.toInt, bytes) + "memory-initialize".reflectCtrlWith[Unit](offsetC.toInt, convertWatEscapesToCpp(bytes)) case _ => () } } From 09b0f90e8af014802fe34b2f352e78febe6a80d6 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 11 Mar 2026 00:30:00 -0400 Subject: [PATCH 3/3] load sym float & some binary operations --- headers/wasm/concrete_num.hpp | 22 ++++++++++ headers/wasm/sym_rt.hpp | 40 +++++++++++++++++-- headers/wasm/symbolic_decl.hpp | 8 +++- headers/wasm/symbolic_impl.hpp | 18 +++++++++ headers/wasm/symval_decl.hpp | 9 +++++ headers/wasm/symval_factory.hpp | 6 +++ headers/wasm/symval_impl.hpp | 12 ++++++ .../scala/wasm/StagedConcolicMiniWasm.scala | 36 +++++++++++------ 8 files changed, 135 insertions(+), 16 deletions(-) diff --git a/headers/wasm/concrete_num.hpp b/headers/wasm/concrete_num.hpp index 80a7fef0..6a2eafc5 100644 --- a/headers/wasm/concrete_num.hpp +++ b/headers/wasm/concrete_num.hpp @@ -2,6 +2,7 @@ #define WASM_CONCRETE_NUM_HPP #include "wasm/profile.hpp" #include "wasm/utils.hpp" +#include #include struct Num { @@ -877,6 +878,27 @@ struct Num { return Num(static_cast(r_bits)); } + inline Num trunc_f64_to_i32_u() const { + uint64_t bits = toUInt64(); + double value = f64_from_bits(bits); + + if (std::isnan(value)) { + throw std::runtime_error("i32.trunc_f64_u: NaN"); + } + if (std::isinf(value)) { + throw std::runtime_error("i32.trunc_f64_u: Infinity"); + } + if (value < 0.0 || value >= 4294967296.0) { + throw std::runtime_error("i32.trunc_f64_u: Out of range"); + } + + double truncated = std::trunc(value); + uint32_t result = static_cast(truncated); + Num res(static_cast(result)); + debug_print("i32.trunc_f64_u", *this, *this, res); + return res; + } + // f64.min / f64.max: follow wasm-ish semantics: if either is NaN, return // NaN (propagate) inline Num f64_min(const Num &other) const { diff --git a/headers/wasm/sym_rt.hpp b/headers/wasm/sym_rt.hpp index dc9eaa23..efc49ad5 100644 --- a/headers/wasm/sym_rt.hpp +++ b/headers/wasm/sym_rt.hpp @@ -354,7 +354,39 @@ class SymMemory_t { SymVal s7 = (it != memory.end()) ? it->second : SVFactory::ZeroByte; #endif - return s7.concat(s6).concat(s5).concat(s4).concat(s3).concat(s2).concat(s1).concat(s0); + return s7.concat(s6) + .concat(s5) + .concat(s4) + .concat(s3) + .concat(s2) + .concat(s1) + .concat(s0); + } + + SymVal loadSymFloat(int32_t base, int32_t offset) { + // For simplicity, we treat float as concrete value for now + auto symbv = loadSym(base, offset); + assert(symbv.is_concrete() && "Currently only support concrete symbolic " + "value for float-point values"); + if (auto concrete = dynamic_cast(symbv.symptr.get())) { + auto value = concrete->value; + return SVFactory::make_concrete_fp(value, 32); + } else { + assert(false && "unreachable"); + } + } + + SymVal loadSymDouble(int32_t base, int32_t offset) { + // For simplicity, we treat double as concrete value for now + auto symbv = loadSymLong(base, offset); + assert(symbv.is_concrete() && "Currently only support concrete symbolic " + "value for float-point values"); + if (auto concrete = dynamic_cast(symbv.symptr.get())) { + auto value = concrete->value; + return SVFactory::make_concrete_fp(value, 64); + } else { + assert(false && "unreachable"); + } } // when loading a symval, we need to concat 4 symbolic values @@ -397,12 +429,14 @@ class SymMemory_t { } std::monostate storeSymFloat(int32_t base, int32_t offset, SymVal value) { - assert(value.is_concrete() && "Currently only support concrete symbolic value for float-point values"); + assert(value.is_concrete() && "Currently only support concrete symbolic " + "value for float-point values"); return storeSym(base, offset, value); } std::monostate storeSymDouble(int32_t base, int32_t offset, SymVal value) { - assert(value.is_concrete() && "Currently only support concrete symbolic value for float-point values"); + assert(value.is_concrete() && "Currently only support concrete symbolic " + "value for float-point values"); return storeSymLong(base, offset, value); } diff --git a/headers/wasm/symbolic_decl.hpp b/headers/wasm/symbolic_decl.hpp index ed4a34fb..8ce89dd0 100644 --- a/headers/wasm/symbolic_decl.hpp +++ b/headers/wasm/symbolic_decl.hpp @@ -10,6 +10,7 @@ enum BinOperation { SUB, // Subtraction MUL, // Multiplication DIV, // Division + DIV_U, // Unsigned division AND, // Logical AND OR, // Logical OR EQ_BOOL, // Equal (return a boolean) TODO: remove bv version of comparison ops @@ -17,10 +18,12 @@ enum BinOperation { LT_BOOL, // Less than (return a boolean) LTU_BOOL, // Unsigned less than (return a boolean) LEQ_BOOL, // Less than or equal (return a boolean) + LEU_BOOL, // Unsigned less than or equal (return a boolean) GT_BOOL, // Greater than (return a boolean) GTU_BOOL, // Unsigned greater than (return a boolean) GEQ_BOOL, // Greater than or equal (return a boolean) GEU_BOOL, // Unsigned greater than or equal (return a boolean) + SHL, // Shift left SHR_U, // Shift right unsigned SHR_S, // Shift right signed REM_U, // Unsigned remainder @@ -33,7 +36,7 @@ enum BinOperation { enum UnaryOperation { NOT, // bool not BOOL2BV, // bool to bitvector, - EXTEND, // bitvector extension, extend i32 to i64 + EXTEND, // bitvector extension, extend i32 to i64 }; enum ValueKind { KindBV, KindBool, KindFP }; @@ -145,6 +148,8 @@ struct SymBinary : public Symbolic { case SUB: case MUL: case DIV: + case DIV_U: + case SHL: case SHR_U: case SHR_S: case REM_U: @@ -166,6 +171,7 @@ struct SymBinary : public Symbolic { case LT_BOOL: case LTU_BOOL: case LEQ_BOOL: + case LEU_BOOL: case GT_BOOL: case GTU_BOOL: case GEQ_BOOL: diff --git a/headers/wasm/symbolic_impl.hpp b/headers/wasm/symbolic_impl.hpp index fe27908a..8c6fb067 100644 --- a/headers/wasm/symbolic_impl.hpp +++ b/headers/wasm/symbolic_impl.hpp @@ -76,6 +76,9 @@ inline z3::expr Symbolic::build_z3_expr_aux() { case LEQ_BOOL: { return left <= right; } + case LEU_BOOL: { + return z3::ule(left, right); + } case GT_BOOL: { return left > right; } @@ -85,6 +88,18 @@ inline z3::expr Symbolic::build_z3_expr_aux() { case GEU_BOOL: { return z3::uge(left, right); } + case SHL: { + if (bit_width == 32) { + z3::expr shift_mask = global_z3_ctx().bv_val(0x1F, bit_width); + return z3::shl(left, right & shift_mask); + } else if (bit_width == 64) { + z3::expr shift_mask = global_z3_ctx().bv_val(0x3F, bit_width); + return z3::shl(left, right & shift_mask); + } else { + throw std::runtime_error("Unsupported bit width for SHL: " + + std::to_string(bit_width)); + } + } case SHR_U: { return z3::lshr(left, right); } @@ -109,6 +124,9 @@ inline z3::expr Symbolic::build_z3_expr_aux() { case DIV: { return left / right; } + case DIV_U: { + return z3::udiv(left, right); + } case B_AND: { return left & right; } diff --git a/headers/wasm/symval_decl.hpp b/headers/wasm/symval_decl.hpp index af828e24..8f9ac1a3 100644 --- a/headers/wasm/symval_decl.hpp +++ b/headers/wasm/symval_decl.hpp @@ -28,6 +28,7 @@ struct SymVal { SymVal minus(const SymVal &other) const; SymVal mul(const SymVal &other) const; SymVal div(const SymVal &other) const; + SymVal div_u(const SymVal &other) const; SymVal eq_bool(const SymVal &other) const; SymVal neq_bool(const SymVal &other) const; SymVal land(const SymVal &other) const; @@ -37,10 +38,12 @@ struct SymVal { SymVal lt(const SymVal &other) const; SymVal ltu(const SymVal &other) const; SymVal le(const SymVal &other) const; + SymVal leu(const SymVal &other) const; SymVal gt(const SymVal &other) const; SymVal gtu(const SymVal &other) const; SymVal ge(const SymVal &other) const; SymVal geu(const SymVal &other) const; + SymVal shl(const SymVal &other) const; SymVal shr_u(const SymVal &other) const; SymVal shr_s(const SymVal &other) const; SymVal bv_negate() const; @@ -83,4 +86,10 @@ template inline bool allConcrete(const Args &...args) { inline SymVal Concrete(Num num, int width); +[[noreturn]] inline SymVal debug_unreachable(const char* msg) { + std::cerr << "unreachable: " << msg << '\n'; + assert(false && "unreachable reached"); + std::abort(); +} + #endif // WASM_SYMVAL_HPP diff --git a/headers/wasm/symval_factory.hpp b/headers/wasm/symval_factory.hpp index f7a1af00..31f3041b 100644 --- a/headers/wasm/symval_factory.hpp +++ b/headers/wasm/symval_factory.hpp @@ -365,6 +365,12 @@ inline SymVal make_binary(BinOperation op, const SymVal &lhs, if (lhs_width == 64 && rhs_width == 64) return make_eval_bool(lhs_value.i64_lt_u(rhs_value)); break; + case LEU_BOOL: + if (lhs_width == 32 && rhs_width == 32) + return make_eval_bool(lhs_value.i32_le_u(rhs_value)); + if (lhs_width == 64 && rhs_width == 64) + return make_eval_bool(lhs_value.i64_le_u(rhs_value)); + break; case GTU_BOOL: if (lhs_width == 32 && rhs_width == 32) return make_eval_bool(lhs_value.i32_gt_u(rhs_value)); diff --git a/headers/wasm/symval_impl.hpp b/headers/wasm/symval_impl.hpp index ae0f5c21..b7b3684c 100644 --- a/headers/wasm/symval_impl.hpp +++ b/headers/wasm/symval_impl.hpp @@ -21,6 +21,10 @@ inline SymVal SymVal::div(const SymVal &other) const { return SVFactory::make_binary(DIV, *this, other); } +inline SymVal SymVal::div_u(const SymVal &other) const { + return SVFactory::make_binary(DIV_U, *this, other); +} + inline SymVal SymVal::land(const SymVal &other) const { return SVFactory::make_binary(AND, *this, other); } @@ -70,6 +74,10 @@ inline SymVal SymVal::le(const SymVal &other) const { return SVFactory::make_binary(LEQ_BOOL, *this, other); } +inline SymVal SymVal::leu(const SymVal &other) const { + return SVFactory::make_binary(LEU_BOOL, *this, other); +} + inline SymVal SymVal::gt(const SymVal &other) const { return SVFactory::make_binary(GT_BOOL, *this, other); } @@ -86,6 +94,10 @@ inline SymVal SymVal::geu(const SymVal &other) const { return SVFactory::make_binary(GEU_BOOL, *this, other); } +inline SymVal SymVal::shl(const SymVal &other) const { + return SVFactory::make_binary(SHL, *this, other); +} + inline SymVal SymVal::shr_u(const SymVal &other) const { return SVFactory::make_binary(SHR_U, *this, other); } diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala index 7c6330af..b06eb028 100644 --- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala +++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala @@ -555,6 +555,10 @@ trait ConcreteOps extends StagedWasmValueDomains with ValueCreation { case NumType(I64Type) => StagedConcreteNum(NumType(F64Type), "i64-convert-to-f64-u".reflectCtrlWith[Num](num.i)) } + def truncF64ToI32U(): StagedConcreteNum = num.tipe match { + case NumType(F64Type) => StagedConcreteNum(NumType(I32Type), "f64-trunc-to-i32-u".reflectCtrlWith[Num](num.i)) + } + def assert(): Rep[Unit] = { "assert-true".reflectCtrlWith[Unit](num.toInt != 0) } @@ -1458,7 +1462,7 @@ trait StagedWasmEvaluator extends SAIOps val newCtx3 = newCtx2.push(resTy) eval(rest, kont, trail)(newCtx3) case Convert(cvt) => - withBlock { + val newCtx2 = withBlock { val (ty, newCtx) = ctx.pop() val num = Stack.popC(ty) val sym = Stack.popS(ty) @@ -1466,7 +1470,9 @@ trait StagedWasmEvaluator extends SAIOps val newSym = evalCvtOpS(cvt, sym, newNum) Stack.pushC(newNum) Stack.pushS(newSym) + newCtx.push(newNum.tipe) } + eval(rest, kont, trail)(newCtx2) case WasmBlock(ty, inner) => // no need to modify the stack when entering a block // the type system guarantees that we will never take more than the input size from the stack @@ -1950,17 +1956,17 @@ trait StagedWasmEvaluator extends SAIOps case ConvertTo(NumType(I32Type), NumType(F64Type), ZX) => value.convertI32ToF64U() case ConvertTo(NumType(I64Type), NumType(F64Type), SX) => value.convertI64ToF64S() case ConvertTo(NumType(I64Type), NumType(F64Type), ZX) => value.convertI64ToF64U() + case TruncTo(NumType(F64Type),NumType(I32Type),ZX) => value.truncF64ToI32U() case _ => throw new UnsupportedOperationException(s"Unsupported concrete conversion $op") } def evalCvtOpS(op: CvtOp, value: StagedSymbolicNum, c: StagedConcreteNum): StagedSymbolicNum = { - var res = c.toStagedSymbolicNum.s - if (!allConcrete(value)) { - op match { - case Extend(NumType(I32Type), NumType(I64Type), ZX) => value.extend().s - case _ => "debug-assert".reflectCtrlWith[SymVal](false, "All runtime float point must be concrete values") - } - } + val res = if (allConcrete(value)) { + c.toStagedSymbolicNum.s + } else (op match { + case _ => StagedSymbolicNum(NumType(I32Type) /* Just a place holder here */, + "debug-unreachable".reflectCtrlWith[SymVal]("All runtime converted value must be concrete values")) + }).s StagedSymbolicNum(c.tipe, res) } @@ -2268,9 +2274,9 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { case Node(_, "memory-load-long", List(base, offset), _) => emit("Memory.loadLong("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "memory-load-float", List(base, offset), _) => - emit("Memory.loadFloat("); shallow(base); emit(", "); shallow(offset); emit(")") + emit("Memory.loadInt("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "memory-load-double", List(base, offset), _) => - emit("Memory.loadDouble("); shallow(base); emit(", "); shallow(offset); emit(")") + emit("Memory.loadLong("); shallow(base); emit(", "); shallow(offset); emit(")") case Node(_, "memory-grow", List(delta), _) => emit("Memory.grow("); shallow(delta); emit(")") case Node(_, "stack-size", _, _) => @@ -2419,6 +2425,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { emit("("); shallow(num); emit(".convert_i64_to_f64_s())") case Node(_, "i64-convert-to-f64-u", List(num), _) => emit("("); shallow(num); emit(".convert_i64_to_f64_u())") + case Node(_, "f64-trunc-to-i32-u", List(num), _) => + emit("("); shallow(num); emit(".trunc_f64_to_i32_u())") case Node(_, "f32-binary-add", List(lhs, rhs), _) => shallow(lhs); emit(".f32_add("); shallow(rhs); emit(")") case Node(_, "f64-binary-add", List(lhs, rhs), _) => @@ -2467,6 +2475,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { shallow(lhs); emit(".mul("); shallow(rhs); emit(")") case Node(_, "sym-binary-div", List(lhs, rhs), _) => shallow(lhs); emit(".div("); shallow(rhs); emit(")") + case Node(_, "sym-binary-div-u", List(lhs, rhs), _) => + shallow(lhs); emit(".div_u("); shallow(rhs); emit(")") case Node(_, "sym-binary-and", List(lhs, rhs), _) => shallow(lhs); emit(".bitwise_and("); shallow(rhs); emit(")") case Node(_, "sym-relation-le", List(lhs, rhs), _) => @@ -2495,6 +2505,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { shallow(lhs); emit(".gtu("); shallow(rhs); emit(").bool2bv()") case Node(_, "sym-relation-les", List(lhs, rhs), _) => shallow(lhs); emit(".le("); shallow(rhs); emit(").bool2bv()") + case Node(_, "sym-binary-shl", List(lhs, rhs), _) => + shallow(lhs); emit(".shl("); shallow(rhs); emit(")") case Node(_, "sym-binary-shr-u", List(lhs, rhs), _) => shallow(lhs); emit(".shr_u("); shallow(rhs); emit(")") case Node(_, "sym-binary-shr-s", List(lhs, rhs), _) => @@ -2517,8 +2529,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase { emit("make_symbolic("); shallow(num); emit(", "); shallow(width); emit(")") case Node(_, "sym-env-read", List(sym), _) => emit("SymEnv.read("); shallow(sym); emit(")") - case (Node(_, "debug-assert", List(cond, msg), _)) => - emit("assert("); shallow(cond); emit(" && "); shallow(msg); emit(")") + case (Node(_, "debug-unreachable", List(msg), _)) => + emit("debug_unreachable("); shallow(msg); emit(")") case Node(_, "assert-true", List(cond), _) => emit("GENSYM_ASSERT("); shallow(cond); emit(")") case Node(_, "sym-assert-true", List(s_cond), _) =>