From 790c6ccc3e5818f535150ce4c551fe2abd89c724 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Tue, 25 Aug 2020 12:45:26 +0200 Subject: [PATCH] Add bitvector and array literal support for ExprWriter --- .../mit/theta/core/dsl/impl/ExprWriter.java | 109 ++++++++++++++++++ 1 file changed, 109 insertions(+) diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java index 1251cb9a71..67a399f147 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprWriter.java @@ -23,6 +23,9 @@ import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.anytype.PrimeExpr; import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; import hu.bme.mit.theta.core.type.booltype.AndExpr; @@ -35,6 +38,30 @@ import hu.bme.mit.theta.core.type.booltype.OrExpr; import hu.bme.mit.theta.core.type.booltype.TrueExpr; import hu.bme.mit.theta.core.type.booltype.XorExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAddExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAndExpr; +import hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvDivExpr; +import hu.bme.mit.theta.core.type.bvtype.BvEqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvGeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvGtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvModExpr; +import hu.bme.mit.theta.core.type.bvtype.BvMulExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNegExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNotExpr; +import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; +import hu.bme.mit.theta.core.type.bvtype.BvRemExpr; +import hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; +import hu.bme.mit.theta.core.type.bvtype.BvToIntExpr; +import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; import hu.bme.mit.theta.core.type.inttype.IntAddExpr; import hu.bme.mit.theta.core.type.inttype.IntDivExpr; import hu.bme.mit.theta.core.type.inttype.IntEqExpr; @@ -47,6 +74,7 @@ import hu.bme.mit.theta.core.type.inttype.IntNegExpr; import hu.bme.mit.theta.core.type.inttype.IntNeqExpr; import hu.bme.mit.theta.core.type.inttype.IntSubExpr; +import hu.bme.mit.theta.core.type.inttype.IntToBvExpr; import hu.bme.mit.theta.core.type.inttype.IntToRatExpr; import hu.bme.mit.theta.core.type.inttype.IntModExpr; import hu.bme.mit.theta.core.type.inttype.IntRemExpr; @@ -63,6 +91,9 @@ import hu.bme.mit.theta.core.type.rattype.RatNeqExpr; import hu.bme.mit.theta.core.type.rattype.RatSubExpr; +import java.util.Arrays; +import java.util.stream.Collectors; + public final class ExprWriter { private final DispatchTable table; @@ -132,6 +163,8 @@ private ExprWriter() { .addCase(IntToRatExpr.class, e -> prefixUnary(e, "(rat)")) + .addCase(IntToBvExpr.class, e -> e.getType().toString()) + // Rational .addCase(RatAddExpr.class, e -> infixMultiary(e, " + ")) @@ -158,12 +191,70 @@ private ExprWriter() { .addCase(RatLitExpr.class, e -> e.getNum() + "%" + e.getDenom()) + // Bitvector + + .addCase(BvAddExpr.class, e -> infixMultiary(e, " + ")) + + .addCase(BvSubExpr.class, e -> infixBinary(e, " - ")) + + .addCase(BvMulExpr.class, e -> infixMultiary(e, " * ")) + + .addCase(BvDivExpr.class, e -> infixBinary(e, " / ")) + + .addCase(BvModExpr.class, e -> infixBinary(e, " mod ")) + + .addCase(BvRemExpr.class, e -> infixBinary(e, " rem ")) + + // TODO: BvPosExpr + + .addCase(BvNegExpr.class, e -> prefixUnary(e, "-")) + + .addCase(BvAndExpr.class, e -> infixMultiary(e, " & ")) + + .addCase(BvOrExpr.class, e -> infixMultiary(e, " | ")) + + .addCase(BvXorExpr.class, e -> infixMultiary(e, " ^ ")) + + .addCase(BvNotExpr.class, e -> prefixUnary(e, "~")) + + .addCase(BvShiftLeftExpr.class, e -> infixBinary(e, " << ")) + + .addCase(BvArithShiftRightExpr.class, e -> infixBinary(e, " >> ")) + + .addCase(BvLogicShiftRightExpr.class, e -> infixBinary(e, " >>> ")) + + .addCase(BvRotateLeftExpr.class, e -> infixBinary(e, " <<~ ")) + + .addCase(BvRotateRightExpr.class, e -> infixBinary(e, " ~>> ")) + + .addCase(BvEqExpr.class, e -> infixBinary(e, " = ")) + + .addCase(BvNeqExpr.class, e -> infixBinary(e, " /= ")) + + .addCase(BvLtExpr.class, e -> infixBinary(e, " < ")) + + .addCase(BvLeqExpr.class, e -> infixBinary(e, " <= ")) + + .addCase(BvGtExpr.class, e -> infixBinary(e, " > ")) + + .addCase(BvGeqExpr.class, e -> infixBinary(e, " >= ")) + + .addCase(BvToIntExpr.class, e -> prefixUnary(e, "(int)")) + + .addCase(BvLitExpr.class, this::bvLit) + // Array .addCase(ArrayReadExpr.class, this::arrayRead) .addCase(ArrayWriteExpr.class, this::arrayWrite) + .addCase(ArrayEqExpr.class, e -> infixBinary(e, " = ")) + + .addCase(ArrayNeqExpr.class, e -> infixBinary(e, " /= ")) + + .addCase(ArrayLitExpr.class, this::arrayLit) + // General .addCase(RefExpr.class, e -> e.getDecl().getName()) @@ -241,4 +332,22 @@ private String ite(final IteExpr expr) { return sb.toString(); } + private String bvLit(final BvLitExpr expr) { + var value = Arrays.toString(expr.getValue()) + .replace("true", "1") + .replace("false", "0") + .replace("[", "") + .replace("]", "") + .replace(",", "") + .replace(" ", ""); + return expr.getType().getSize() + "'" + (expr.getType().isSigned() ? "s" : "u") + "b" + value; + } + + private String arrayLit(final ArrayLitExpr expr) { + return "[" + + expr.getElements().stream().map(e -> write(e.get1()) + " <- " + write(e.get2())).collect(Collectors.joining(", ")) + + "<" + expr.getType().getIndexType().toString() + ">default" + " <- " + write(expr.getElseElem()) + + "]"; + } + }