Skip to content

Commit

Permalink
add closure that can change the behavior of serialization
Browse files Browse the repository at this point in the history
  • Loading branch information
@ekiwi
ekiwi committed Nov 14, 2023
1 parent b716f56 commit 27566b2
Showing 1 changed file with 86 additions and 70 deletions.
156 changes: 86 additions & 70 deletions src/ir/serialize.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,13 +18,22 @@ pub trait SerializableIrNode {

impl SerializableIrNode for Expr {
fn serialize(&self, ctx: &Context, writer: &mut impl Write) -> std::io::Result<()> {
serialize_expr(&self, ctx, writer)
serialize_expr(&self, ctx, writer, &|_, _, _| false)
}
}

/// Internal serialize function for expressions that can be specialized depending on how we want
/// to treat sub-expressions.
fn serialize_expr(expr: &Expr, ctx: &Context, writer: &mut impl Write) -> std::io::Result<()> {
fn serialize_expr<F, W>(
expr: &Expr,
ctx: &Context,
writer: &mut W,
serialize_child: &F,
) -> std::io::Result<()>
where
F: Fn(&ExprRef, &Context, &mut W) -> bool,
W: Write,
{
match expr {
Expr::BVSymbol { name, .. } => write!(writer, "{}", ctx.get(*name)),
Expr::BVLiteral { value, width } => {
Expand All @@ -36,16 +45,18 @@ fn serialize_expr(expr: &Expr, ctx: &Context, writer: &mut impl Write) -> std::i
}
Expr::BVZeroExt { e, by, .. } => {
write!(writer, "zext(")?;
serialize_expr_ref(e, ctx, writer)?;
if (serialize_child)(e, ctx, writer) {
serialize_expr_ref(e, ctx, writer, serialize_child)?;
}
write!(writer, ", {by})")
}
Expr::BVSignExt { e, by, .. } => {
write!(writer, "sext(")?;
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
write!(writer, ", {by})")
}
Expr::BVSlice { e, hi, lo, .. } => {
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
if hi == lo {
write!(writer, "[{hi}]")
} else {
Expand All @@ -54,234 +65,239 @@ fn serialize_expr(expr: &Expr, ctx: &Context, writer: &mut impl Write) -> std::i
}
Expr::BVNot(e, _) => {
write!(writer, "not(")?;
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVNegate(e, _) => {
write!(writer, "neg(")?;
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVReduceOr(e) => {
write!(writer, "redor(")?;
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVReduceAnd(e) => {
write!(writer, "redand(")?;
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVReduceXor(e) => {
write!(writer, "redxor(")?;
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVEqual(a, b) => {
write!(writer, "eq(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVImplies(a, b) => {
write!(writer, "implies(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVGreater(a, b) => {
write!(writer, "ugt(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVGreaterSigned(a, b) => {
write!(writer, "sgt(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVGreaterEqual(a, b) => {
write!(writer, "ugte(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVGreaterEqualSigned(a, b) => {
write!(writer, "sgte(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVConcat(a, b, _) => {
write!(writer, "concat(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVAnd(a, b, _) => {
write!(writer, "and(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVOr(a, b, _) => {
write!(writer, "or(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVXor(a, b, _) => {
write!(writer, "xor(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVShiftLeft(a, b, _) => {
write!(writer, "logical_shift_left(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVArithmeticShiftRight(a, b, _) => {
write!(writer, "arithmetic_shift_right(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVShiftRight(a, b, _) => {
write!(writer, "logical_shift_right(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVAdd(a, b, _) => {
write!(writer, "add(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVMul(a, b, _) => {
write!(writer, "mul(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVSignedDiv(a, b, _) => {
write!(writer, "sdiv(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVUnsignedDiv(a, b, _) => {
write!(writer, "udiv(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVSignedMod(a, b, _) => {
write!(writer, "smod(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVSignedRem(a, b, _) => {
write!(writer, "srem(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVUnsignedRem(a, b, _) => {
write!(writer, "urem(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVSub(a, b, _) => {
write!(writer, "sub(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::BVArrayRead { array, index, .. } => {
serialize_expr_ref(array, ctx, writer)?;
serialize_expr_ref(array, ctx, writer, serialize_child)?;
write!(writer, "[")?;
serialize_expr_ref(index, ctx, writer)?;
serialize_expr_ref(index, ctx, writer, serialize_child)?;
write!(writer, "]")
}
Expr::BVIte {
cond, tru, fals, ..
} => {
write!(writer, "ite(")?;
serialize_expr_ref(cond, ctx, writer)?;
serialize_expr_ref(cond, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(tru, ctx, writer)?;
serialize_expr_ref(tru, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(fals, ctx, writer)?;
serialize_expr_ref(fals, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::ArraySymbol { name, .. } => write!(writer, "{}", ctx.get(*name)),
Expr::ArrayConstant { e, index_width, .. } => {
write!(writer, "([")?;
serialize_expr_ref(e, ctx, writer)?;
serialize_expr_ref(e, ctx, writer, serialize_child)?;
write!(writer, "] x 2^{index_width})")
}
Expr::ArrayEqual(a, b) => {
write!(writer, "eq(")?;
serialize_expr_ref(a, ctx, writer)?;
serialize_expr_ref(a, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(b, ctx, writer)?;
serialize_expr_ref(b, ctx, writer, serialize_child)?;
write!(writer, ")")
}
Expr::ArrayStore { array, index, data } => {
serialize_expr_ref(array, ctx, writer)?;
serialize_expr_ref(array, ctx, writer, serialize_child)?;
write!(writer, "[")?;
serialize_expr_ref(index, ctx, writer)?;
serialize_expr_ref(index, ctx, writer, serialize_child)?;
write!(writer, " := ")?;
serialize_expr_ref(data, ctx, writer)?;
serialize_expr_ref(data, ctx, writer, serialize_child)?;
write!(writer, "]")
}
Expr::ArrayIte { cond, tru, fals } => {
write!(writer, "ite(")?;
serialize_expr_ref(cond, ctx, writer)?;
serialize_expr_ref(cond, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(tru, ctx, writer)?;
serialize_expr_ref(tru, ctx, writer, serialize_child)?;
write!(writer, ", ")?;
serialize_expr_ref(fals, ctx, writer)?;
serialize_expr_ref(fals, ctx, writer, serialize_child)?;
write!(writer, ")")
}
}
}

/// De-reference and serialize.
#[inline]
fn serialize_expr_ref(
fn serialize_expr_ref<F, W>(
expr: &ExprRef,
ctx: &Context,
writer: &mut impl Write,
) -> std::io::Result<()> {
serialize_expr(ctx.get(*expr), ctx, writer)
writer: &mut W,
serialize_child: &F,
) -> std::io::Result<()>
where
F: Fn(&ExprRef, &Context, &mut W) -> bool,
W: Write,
{
serialize_expr(ctx.get(*expr), ctx, writer, serialize_child)
}

impl SerializableIrNode for ExprRef {
Expand Down

0 comments on commit 27566b2

Please sign in to comment.