diff --git a/build.gradle.kts b/build.gradle.kts index 2c18f970d5..55720ecd32 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "1.4.2" + version = "1.4.3" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/subprojects/cfa/README.md b/subprojects/cfa/README.md index 790f4504f1..1d68e2e9da 100644 --- a/subprojects/cfa/README.md +++ b/subprojects/cfa/README.md @@ -51,7 +51,7 @@ Expressions of the CFA include the following. - Arithmetic, e.g., `+`, `-`, `/`, `*`, `mod`, `rem`. - Conditional: `if . then . else .` - Array read (`a[i]`) and write (`a[i <- v]`). -- Bitvector specific operators, e.g., `&`, `|`, `^`, `<<`, `>>`, `~`. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._ +- Bitvector specific operators, e.g., `&`, `|`, `^`, `<<`, `>>`, `>>>`, `<<~`, `~>>`, `~`. _This is an experimental feature with currently limited algorithmic support. See the [details](doc/bitvectors.md) for more information._ ### Textual representation (DSL) diff --git a/subprojects/cfa/doc/bitvectors.md b/subprojects/cfa/doc/bitvectors.md index 02a32ba7a5..aef30c121e 100644 --- a/subprojects/cfa/doc/bitvectors.md +++ b/subprojects/cfa/doc/bitvectors.md @@ -81,8 +81,11 @@ These operations are specific to bitvectors only. These operations require that - **Bitwise and**: Ands two bitvectors; `a & b` - **Bitwise or**: Ors two bitvectors; `a | b` - **Bitwise xor**: XORs two bitvectors; `a ^ b` -- **Bitwise shift left**: Shifts a to left with b; `a << b` -- **Bitwise shift right**: Shifts a to right with b; `a >> b` +- **Bitwise shift left**: Shifts *a* to the left with *b*; `a << b` +- **Bitwise arithmetic shift right**: Shifts *a* arithmetically to the right with *b*; `a >> b` +- **Bitwise logical shift right**: Shifts *a* logically to the right with *b*; `a >>> b` +- **Bitwise rotate left**: Rotates *a* to the left with *b*; `a <<~ b` +- **Bitwise rotate right**: Rotates *a* to the right with *b*; `a ~>> b` - **Bitwise not:** Negates all the bits in bitvectors; `~a` ### Relational operations diff --git a/subprojects/cfa/src/main/antlr/CfaDsl.g4 b/subprojects/cfa/src/main/antlr/CfaDsl.g4 index 341e61d99f..e5cba34923 100644 --- a/subprojects/cfa/src/main/antlr/CfaDsl.g4 +++ b/subprojects/cfa/src/main/antlr/CfaDsl.g4 @@ -223,7 +223,7 @@ bitwiseAndExpr ; bitwiseShiftExpr - : leftOp=additiveExpr (oper=(BITWISE_SHIFT_LEFT | BITWISE_SHIFT_RIGHT) rightOp=additiveExpr)? + : leftOp=additiveExpr (oper=(BITWISE_SHIFT_LEFT | BITWISE_ARITH_SHIFT_RIGHT | BITWISE_LOGIC_SHIFT_RIGHT | BITWISE_ROTATE_LEFT | BITWISE_ROTATE_RIGHT) rightOp=additiveExpr)? ; additiveExpr @@ -410,10 +410,22 @@ BITWISE_SHIFT_LEFT : LT LT ; -BITWISE_SHIFT_RIGHT +BITWISE_ARITH_SHIFT_RIGHT : GT GT ; +BITWISE_LOGIC_SHIFT_RIGHT + : GT GT GT + ; + +BITWISE_ROTATE_LEFT + : LT LT BITWISE_NOT + ; + +BITWISE_ROTATE_RIGHT + : BITWISE_NOT GT GT + ; + BITWISE_NOT : '~' ; diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java index dd80016fc0..1238c93c65 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java +++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java @@ -366,8 +366,14 @@ public Expr visitBitwiseShiftExpr(final BitwiseShiftExprContext ctx) { switch (ctx.oper.getType()) { case BITWISE_SHIFT_LEFT: return BvExprs.ShiftLeft(leftOp, rightOp); - case BITWISE_SHIFT_RIGHT: - return BvExprs.ShiftRight(leftOp, rightOp); + case BITWISE_ARITH_SHIFT_RIGHT: + return BvExprs.ArithShiftRight(leftOp, rightOp); + case BITWISE_LOGIC_SHIFT_RIGHT: + return BvExprs.LogicShiftRight(leftOp, rightOp); + case BITWISE_ROTATE_LEFT: + return BvExprs.RotateLeft(leftOp, rightOp); + case BITWISE_ROTATE_RIGHT: + return BvExprs.RotateRight(leftOp, rightOp); default: throw new AssertionError(); } diff --git a/subprojects/cfa/src/test/resources/bv3.cfa b/subprojects/cfa/src/test/resources/bv3.cfa new file mode 100644 index 0000000000..fc018fed9d --- /dev/null +++ b/subprojects/cfa/src/test/resources/bv3.cfa @@ -0,0 +1,17 @@ +main process cfa { + var x : bv[4] + + init loc L0 + loc L1 + loc L2 + loc L3 + final loc END + error loc ERR + + L0 -> L1 { x := 4'b0001 ~>> 4'd1 } + L1 -> L2 { assume x = 4'b1000 } + L1 -> ERR { assume not (x = 4'b1000) } + L2 -> L3 { x := (x >> 4'd1) >>> 4'd1 } + L3 -> END { assume x = 4'b0110 } + L3 -> ERR { assume not (x = 4'b0110) } +} \ No newline at end of file diff --git a/subprojects/core/src/main/antlr/CoreDsl.g4 b/subprojects/core/src/main/antlr/CoreDsl.g4 index d742f6400e..51b485b306 100644 --- a/subprojects/core/src/main/antlr/CoreDsl.g4 +++ b/subprojects/core/src/main/antlr/CoreDsl.g4 @@ -171,7 +171,7 @@ bitwiseAndExpr ; bitwiseShiftExpr - : leftOp=additiveExpr (oper=(BITWISE_SHIFT_LEFT | BITWISE_SHIFT_RIGHT) rightOp=additiveExpr)? + : leftOp=additiveExpr (oper=(BITWISE_SHIFT_LEFT | BITWISE_ARITH_SHIFT_RIGHT | BITWISE_LOGIC_SHIFT_RIGHT | BITWISE_ROTATE_LEFT | BITWISE_ROTATE_RIGHT) rightOp=additiveExpr)? ; additiveExpr @@ -344,10 +344,22 @@ BITWISE_SHIFT_LEFT : LT LT ; -BITWISE_SHIFT_RIGHT +BITWISE_ARITH_SHIFT_RIGHT : GT GT ; +BITWISE_LOGIC_SHIFT_RIGHT + : GT GT GT + ; + +BITWISE_ROTATE_LEFT + : LT LT BITWISE_NOT + ; + +BITWISE_ROTATE_RIGHT + : BITWISE_NOT GT GT + ; + BITWISE_NOT : '~' ; diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java index 98510bccee..6ffef43623 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java @@ -20,6 +20,7 @@ import static com.google.common.base.Preconditions.checkState; import static hu.bme.mit.theta.common.Utils.singleElementOf; import static hu.bme.mit.theta.core.decl.Decls.Param; +import static hu.bme.mit.theta.core.dsl.gen.CoreDslParser.*; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Div; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; @@ -47,6 +48,7 @@ import static hu.bme.mit.theta.core.type.inttype.IntExprs.Mod; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Rem; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; import static java.util.stream.Collectors.toList; import java.util.Collection; @@ -54,6 +56,9 @@ import java.util.List; import java.util.stream.Stream; +import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.*; +import hu.bme.mit.theta.core.type.bvtype.BvExprs; +import hu.bme.mit.theta.core.type.bvtype.BvType; import org.antlr.v4.runtime.Token; import com.google.common.collect.ImmutableList; @@ -66,31 +71,6 @@ import hu.bme.mit.theta.core.dsl.DeclSymbol; import hu.bme.mit.theta.core.dsl.gen.CoreDslBaseVisitor; import hu.bme.mit.theta.core.dsl.gen.CoreDslParser; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.AccessContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.AccessorExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.AdditiveExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.AndExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.ArrayAccessContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.DeclListContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.EqualityExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.ExistsExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.FalseExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.ForallExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.FuncAccessContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.FuncLitExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.IdExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.IffExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.ImplyExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.IntLitExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.IteExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.MultiplicativeExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.NegExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.NotExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.OrExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.ParenExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.RatLitExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.RelationExprContext; -import hu.bme.mit.theta.core.dsl.gen.CoreDslParser.TrueExprContext; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.abstracttype.AddExpr; @@ -308,6 +288,88 @@ public Expr visitRelationExpr(final RelationExprContext ctx) { //// + @Override + public Expr visitBitwiseOrExpr(final BitwiseOrExprContext ctx) { + if (ctx.rightOp != null) { + final Expr leftOp = castBv(ctx.leftOp.accept(this)); + final Expr rightOp = castBv(ctx.rightOp.accept(this)); + + switch (ctx.oper.getType()) { + case BITWISE_OR: + return BvExprs.Or(List.of(leftOp, rightOp)); + default: + throw new AssertionError(); + } + + } else { + return visitChildren(ctx); + } + } + + @Override + public Expr visitBitwiseXorExpr(final BitwiseXorExprContext ctx) { + if (ctx.rightOp != null) { + final Expr leftOp = castBv(ctx.leftOp.accept(this)); + final Expr rightOp = castBv(ctx.rightOp.accept(this)); + + switch (ctx.oper.getType()) { + case BITWISE_XOR: + return BvExprs.Xor(List.of(leftOp, rightOp)); + default: + throw new AssertionError(); + } + + } else { + return visitChildren(ctx); + } + } + + @Override + public Expr visitBitwiseAndExpr(final BitwiseAndExprContext ctx) { + if (ctx.rightOp != null) { + final Expr leftOp = castBv(ctx.leftOp.accept(this)); + final Expr rightOp = castBv(ctx.rightOp.accept(this)); + + switch (ctx.oper.getType()) { + case BITWISE_AND: + return BvExprs.And(List.of(leftOp, rightOp)); + default: + throw new AssertionError(); + } + + } else { + return visitChildren(ctx); + } + } + + @Override + public Expr visitBitwiseShiftExpr(final BitwiseShiftExprContext ctx) { + if (ctx.rightOp != null) { + final Expr leftOp = castBv(ctx.leftOp.accept(this)); + final Expr rightOp = castBv(ctx.rightOp.accept(this)); + + switch (ctx.oper.getType()) { + case BITWISE_SHIFT_LEFT: + return BvExprs.ShiftLeft(leftOp, rightOp); + case BITWISE_ARITH_SHIFT_RIGHT: + return BvExprs.ArithShiftRight(leftOp, rightOp); + case BITWISE_LOGIC_SHIFT_RIGHT: + return BvExprs.LogicShiftRight(leftOp, rightOp); + case BITWISE_ROTATE_LEFT: + return BvExprs.RotateLeft(leftOp, rightOp); + case BITWISE_ROTATE_RIGHT: + return BvExprs.RotateRight(leftOp, rightOp); + default: + throw new AssertionError(); + } + + } else { + return visitChildren(ctx); + } + } + + //// + @Override public Expr visitAdditiveExpr(final AdditiveExprContext ctx) { if (ctx.ops.size() > 1) { diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvShiftRightExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvArithShiftRightExpr.java similarity index 62% rename from subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvShiftRightExpr.java rename to subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvArithShiftRightExpr.java index d5230eb6c1..30a850d645 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvShiftRightExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvArithShiftRightExpr.java @@ -6,23 +6,23 @@ import static hu.bme.mit.theta.core.utils.TypeUtils.*; -public class BvShiftRightExpr extends BinaryExpr { +public class BvArithShiftRightExpr extends BinaryExpr { private static final int HASH_SEED = 965; private static final String OPERATOR_LABEL = ">>"; - private BvShiftRightExpr(final Expr leftOp, final Expr rightOp) { + private BvArithShiftRightExpr(final Expr leftOp, final Expr rightOp) { super(leftOp, rightOp); checkAllTypesEqual(leftOp, rightOp); } - public static BvShiftRightExpr of(final Expr leftOp, final Expr rightOp) { - return new BvShiftRightExpr(leftOp, rightOp); + public static BvArithShiftRightExpr of(final Expr leftOp, final Expr rightOp) { + return new BvArithShiftRightExpr(leftOp, rightOp); } - public static BvShiftRightExpr create(final Expr leftOp, final Expr rightOp) { + public static BvArithShiftRightExpr create(final Expr leftOp, final Expr rightOp) { final Expr newLeftOp = castBv(leftOp); final Expr newRightOp = castBv(rightOp); - return BvShiftRightExpr.of(newLeftOp, newRightOp); + return BvArithShiftRightExpr.of(newLeftOp, newRightOp); } @Override @@ -34,25 +34,25 @@ public BvType getType() { public BvLitExpr eval(final Valuation val) { final BvLitExpr leftOpVal = (BvLitExpr) getLeftOp().eval(val); final BvLitExpr rightOpVal = (BvLitExpr) getRightOp().eval(val); - return leftOpVal.shiftRight(rightOpVal); + return leftOpVal.arithShiftRight(rightOpVal); } @Override - public BvShiftRightExpr with(final Expr leftOp, final Expr rightOp) { + public BvArithShiftRightExpr with(final Expr leftOp, final Expr rightOp) { if (leftOp == getLeftOp() && rightOp == getRightOp()) { return this; } else { - return BvShiftRightExpr.of(leftOp, rightOp); + return BvArithShiftRightExpr.of(leftOp, rightOp); } } @Override - public BvShiftRightExpr withLeftOp(final Expr leftOp) { + public BvArithShiftRightExpr withLeftOp(final Expr leftOp) { return with(leftOp, getRightOp()); } @Override - public BvShiftRightExpr withRightOp(final Expr rightOp) { + public BvArithShiftRightExpr withRightOp(final Expr rightOp) { return with(getLeftOp(), rightOp); } @@ -60,8 +60,8 @@ public BvShiftRightExpr withRightOp(final Expr rightOp) { public boolean equals(final Object obj) { if (this == obj) { return true; - } else if (obj instanceof BvShiftRightExpr) { - final BvShiftRightExpr that = (BvShiftRightExpr) obj; + } else if (obj instanceof BvArithShiftRightExpr) { + final BvArithShiftRightExpr that = (BvArithShiftRightExpr) obj; return this.getLeftOp().equals(that.getLeftOp()) && this.getRightOp().equals(that.getRightOp()); } else { return false; diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvExprs.java index d801533402..58a51053a4 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvExprs.java @@ -66,8 +66,20 @@ public static BvShiftLeftExpr ShiftLeft(final Expr leftOp, final Expr leftOp, final Expr rightOp) { - return BvShiftRightExpr.of(leftOp, rightOp); + public static BvArithShiftRightExpr ArithShiftRight(final Expr leftOp, final Expr rightOp) { + return BvArithShiftRightExpr.of(leftOp, rightOp); + } + + public static BvLogicShiftRightExpr LogicShiftRight(final Expr leftOp, final Expr rightOp) { + return BvLogicShiftRightExpr.of(leftOp, rightOp); + } + + public static BvRotateLeftExpr RotateLeft(final Expr leftOp, final Expr rightOp) { + return BvRotateLeftExpr.of(leftOp, rightOp); + } + + public static BvRotateRightExpr RotateRight(final Expr leftOp, final Expr rightOp) { + return BvRotateRightExpr.of(leftOp, rightOp); } public static BvEqExpr Eq(final Expr leftOp, final Expr rightOp) { diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java index 522cafcc7a..e8aa328228 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java @@ -125,7 +125,7 @@ public BvLitExpr shiftLeft(final BvLitExpr that) { return Bv(shifted, getType().isSigned()); } - public BvLitExpr shiftRight(final BvLitExpr that) { + public BvLitExpr arithShiftRight(final BvLitExpr that) { checkArgument(this.getType().equals(that.getType())); boolean[] shifted = Arrays.copyOf(this.getValue(), this.getValue().length); @@ -139,6 +139,48 @@ public BvLitExpr shiftRight(final BvLitExpr that) { return Bv(shifted, getType().isSigned()); } + public BvLitExpr logicShiftRight(final BvLitExpr that) { + checkArgument(this.getType().equals(that.getType())); + + boolean[] shifted = Arrays.copyOf(this.getValue(), this.getValue().length); + boolean insert = false; + for(BigInteger i = BigInteger.ZERO; i.compareTo(BvUtils.bvLitExprToBigInteger(that)) < 0; i = i.add(BigInteger.ONE)) { + for(int j = shifted.length - 1; j > 0; j--) { + shifted[j] = shifted[j - 1]; + } + shifted[0] = insert; + } + return Bv(shifted, getType().isSigned()); + } + + public BvLitExpr rotateLeft(final BvLitExpr that) { + checkArgument(this.getType().equals(that.getType())); + + boolean[] shifted = Arrays.copyOf(this.getValue(), this.getValue().length); + for(BigInteger i = BigInteger.ZERO; i.compareTo(BvUtils.bvLitExprToBigInteger(that)) < 0; i = i.add(BigInteger.ONE)) { + boolean rotated = shifted[0]; + for(int j = 0; j < shifted.length - 1; j++) { + shifted[j] = shifted[j + 1]; + } + shifted[shifted.length - 1] = rotated; + } + return Bv(shifted, getType().isSigned()); + } + + public BvLitExpr rotateRight(final BvLitExpr that) { + checkArgument(this.getType().equals(that.getType())); + + boolean[] shifted = Arrays.copyOf(this.getValue(), this.getValue().length); + for(BigInteger i = BigInteger.ZERO; i.compareTo(BvUtils.bvLitExprToBigInteger(that)) < 0; i = i.add(BigInteger.ONE)) { + boolean rotated = shifted[shifted.length - 1]; + for(int j = shifted.length - 1; j > 0; j--) { + shifted[j] = shifted[j - 1]; + } + shifted[0] = rotated; + } + return Bv(shifted, getType().isSigned()); + } + public BvLitExpr mod(final BvLitExpr that) { checkArgument(this.getType().equals(that.getType())); // Always positive semantics: @@ -157,27 +199,19 @@ public BvLitExpr mod(final BvLitExpr that) { public BvLitExpr rem(final BvLitExpr that) { // Semantics: // 5 rem 3 = 2 - // 5 rem -3 = -2 - // -5 rem 3 = 1 + // 5 rem -3 = 2 + // -5 rem 3 = -1 // -5 rem -3 = -1 BigInteger thisInt = BvUtils.bvLitExprToBigInteger(this); BigInteger thatInt = BvUtils.bvLitExprToBigInteger(that); BigInteger thisAbs = thisInt.abs(); BigInteger thatAbs = thatInt.abs(); if (thisInt.compareTo(BigInteger.ZERO) < 0 && thatInt.compareTo(BigInteger.ZERO) < 0) { - BigInteger result = thisAbs.mod(thatAbs); - if (result.compareTo(BigInteger.ZERO) != 0) { - result = result.subtract(thatAbs); - } - return BvUtils.bigIntegerToBvLitExpr(result, getType().getSize(), getType().isSigned()); - } else if (thisInt.compareTo(BigInteger.ZERO) >= 0 && thatInt.compareTo(BigInteger.ZERO) < 0) { return BvUtils.bigIntegerToBvLitExpr(thisAbs.mod(thatAbs).negate(), getType().getSize(), getType().isSigned()); + } else if (thisInt.compareTo(BigInteger.ZERO) >= 0 && thatInt.compareTo(BigInteger.ZERO) < 0) { + return BvUtils.bigIntegerToBvLitExpr(thisAbs.mod(thatAbs), getType().getSize(), getType().isSigned()); } else if (thisInt.compareTo(BigInteger.ZERO) < 0 && thatInt.compareTo(BigInteger.ZERO) >= 0) { - BigInteger result = thisAbs.mod(thatAbs); - if (result.compareTo(BigInteger.ZERO) != 0) { - result = thatAbs.subtract(result); - } - return BvUtils.bigIntegerToBvLitExpr(result, getType().getSize(), getType().isSigned()); + return BvUtils.bigIntegerToBvLitExpr(thisAbs.mod(thatAbs).negate(), getType().getSize(), getType().isSigned()); } else { return BvUtils.bigIntegerToBvLitExpr(thisInt.mod(thatInt), getType().getSize(), getType().isSigned()); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLogicShiftRightExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLogicShiftRightExpr.java new file mode 100644 index 0000000000..3c3b11da88 --- /dev/null +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLogicShiftRightExpr.java @@ -0,0 +1,81 @@ +package hu.bme.mit.theta.core.type.bvtype; + +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.BinaryExpr; +import hu.bme.mit.theta.core.type.Expr; + +import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; +import static hu.bme.mit.theta.core.utils.TypeUtils.checkAllTypesEqual; + +public class BvLogicShiftRightExpr extends BinaryExpr { + private static final int HASH_SEED = 962; + private static final String OPERATOR_LABEL = ">>>"; + + private BvLogicShiftRightExpr(final Expr leftOp, final Expr rightOp) { + super(leftOp, rightOp); + checkAllTypesEqual(leftOp, rightOp); + } + + public static BvLogicShiftRightExpr of(final Expr leftOp, final Expr rightOp) { + return new BvLogicShiftRightExpr(leftOp, rightOp); + } + + public static BvLogicShiftRightExpr create(final Expr leftOp, final Expr rightOp) { + final Expr newLeftOp = castBv(leftOp); + final Expr newRightOp = castBv(rightOp); + return BvLogicShiftRightExpr.of(newLeftOp, newRightOp); + } + + @Override + public BvType getType() { + return getOps().get(0).getType(); + } + + @Override + public BvLitExpr eval(final Valuation val) { + final BvLitExpr leftOpVal = (BvLitExpr) getLeftOp().eval(val); + final BvLitExpr rightOpVal = (BvLitExpr) getRightOp().eval(val); + return leftOpVal.logicShiftRight(rightOpVal); + } + + @Override + public BvLogicShiftRightExpr with(final Expr leftOp, final Expr rightOp) { + if (leftOp == getLeftOp() && rightOp == getRightOp()) { + return this; + } else { + return BvLogicShiftRightExpr.of(leftOp, rightOp); + } + } + + @Override + public BvLogicShiftRightExpr withLeftOp(final Expr leftOp) { + return with(leftOp, getRightOp()); + } + + @Override + public BvLogicShiftRightExpr withRightOp(final Expr rightOp) { + return with(getLeftOp(), rightOp); + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj instanceof BvLogicShiftRightExpr) { + final BvLogicShiftRightExpr that = (BvLogicShiftRightExpr) obj; + return this.getLeftOp().equals(that.getLeftOp()) && this.getRightOp().equals(that.getRightOp()); + } else { + return false; + } + } + + @Override + protected int getHashSeed() { + return HASH_SEED; + } + + @Override + public String getOperatorLabel() { + return OPERATOR_LABEL; + } +} \ No newline at end of file diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvRotateLeftExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvRotateLeftExpr.java new file mode 100644 index 0000000000..ca36396619 --- /dev/null +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvRotateLeftExpr.java @@ -0,0 +1,81 @@ +package hu.bme.mit.theta.core.type.bvtype; + +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.BinaryExpr; +import hu.bme.mit.theta.core.type.Expr; + +import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; +import static hu.bme.mit.theta.core.utils.TypeUtils.checkAllTypesEqual; + +public class BvRotateLeftExpr extends BinaryExpr { + private static final int HASH_SEED = 4282; + private static final String OPERATOR_LABEL = "<<~"; + + private BvRotateLeftExpr(final Expr leftOp, final Expr rightOp) { + super(leftOp, rightOp); + checkAllTypesEqual(leftOp, rightOp); + } + + public static BvRotateLeftExpr of(final Expr leftOp, final Expr rightOp) { + return new BvRotateLeftExpr(leftOp, rightOp); + } + + public static BvRotateLeftExpr create(final Expr leftOp, final Expr rightOp) { + final Expr newLeftOp = castBv(leftOp); + final Expr newRightOp = castBv(rightOp); + return BvRotateLeftExpr.of(newLeftOp, newRightOp); + } + + @Override + public BvType getType() { + return getOps().get(0).getType(); + } + + @Override + public BvLitExpr eval(final Valuation val) { + final BvLitExpr leftOpVal = (BvLitExpr) getLeftOp().eval(val); + final BvLitExpr rightOpVal = (BvLitExpr) getRightOp().eval(val); + return leftOpVal.rotateLeft(rightOpVal); + } + + @Override + public BvRotateLeftExpr with(final Expr leftOp, final Expr rightOp) { + if (leftOp == getLeftOp() && rightOp == getRightOp()) { + return this; + } else { + return BvRotateLeftExpr.of(leftOp, rightOp); + } + } + + @Override + public BvRotateLeftExpr withLeftOp(final Expr leftOp) { + return with(leftOp, getRightOp()); + } + + @Override + public BvRotateLeftExpr withRightOp(final Expr rightOp) { + return with(getLeftOp(), rightOp); + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj instanceof BvRotateLeftExpr) { + final BvRotateLeftExpr that = (BvRotateLeftExpr) obj; + return this.getLeftOp().equals(that.getLeftOp()) && this.getRightOp().equals(that.getRightOp()); + } else { + return false; + } + } + + @Override + protected int getHashSeed() { + return HASH_SEED; + } + + @Override + public String getOperatorLabel() { + return OPERATOR_LABEL; + } +} diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvRotateRightExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvRotateRightExpr.java new file mode 100644 index 0000000000..6126ddf7a8 --- /dev/null +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvRotateRightExpr.java @@ -0,0 +1,81 @@ +package hu.bme.mit.theta.core.type.bvtype; + +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.BinaryExpr; +import hu.bme.mit.theta.core.type.Expr; + +import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; +import static hu.bme.mit.theta.core.utils.TypeUtils.checkAllTypesEqual; + +public class BvRotateRightExpr extends BinaryExpr { + private static final int HASH_SEED = 2564; + private static final String OPERATOR_LABEL = "~>>"; + + private BvRotateRightExpr(final Expr leftOp, final Expr rightOp) { + super(leftOp, rightOp); + checkAllTypesEqual(leftOp, rightOp); + } + + public static BvRotateRightExpr of(final Expr leftOp, final Expr rightOp) { + return new BvRotateRightExpr(leftOp, rightOp); + } + + public static BvRotateRightExpr create(final Expr leftOp, final Expr rightOp) { + final Expr newLeftOp = castBv(leftOp); + final Expr newRightOp = castBv(rightOp); + return BvRotateRightExpr.of(newLeftOp, newRightOp); + } + + @Override + public BvType getType() { + return getOps().get(0).getType(); + } + + @Override + public BvLitExpr eval(final Valuation val) { + final BvLitExpr leftOpVal = (BvLitExpr) getLeftOp().eval(val); + final BvLitExpr rightOpVal = (BvLitExpr) getRightOp().eval(val); + return leftOpVal.rotateRight(rightOpVal); + } + + @Override + public BvRotateRightExpr with(final Expr leftOp, final Expr rightOp) { + if (leftOp == getLeftOp() && rightOp == getRightOp()) { + return this; + } else { + return BvRotateRightExpr.of(leftOp, rightOp); + } + } + + @Override + public BvRotateRightExpr withLeftOp(final Expr leftOp) { + return with(leftOp, getRightOp()); + } + + @Override + public BvRotateRightExpr withRightOp(final Expr rightOp) { + return with(getLeftOp(), rightOp); + } + + @Override + public boolean equals(final Object obj) { + if (this == obj) { + return true; + } else if (obj instanceof BvRotateRightExpr) { + final BvRotateRightExpr that = (BvRotateRightExpr) obj; + return this.getLeftOp().equals(that.getLeftOp()) && this.getRightOp().equals(that.getRightOp()); + } else { + return false; + } + } + + @Override + protected int getHashSeed() { + return HASH_SEED; + } + + @Override + public String getOperatorLabel() { + return OPERATOR_LABEL; + } +} diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/package-info.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/package-info.java index c63f42918f..7c3897afed 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/package-info.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/package-info.java @@ -20,7 +20,10 @@ * - {@link hu.bme.mit.theta.core.type.bvtype.BvOrExpr}: bitwise or * - {@link hu.bme.mit.theta.core.type.bvtype.BvXorExpr}: bitwise xor * - {@link hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr}: shift left - * - {@link hu.bme.mit.theta.core.type.bvtype.BvShiftRightExpr}: shift right + * - {@link hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr}: arithmetic shift right + * - {@link hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr}: logical shift right + * - {@link hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr}: rotate left + * - {@link hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr}: rotate right * * - {@link hu.bme.mit.theta.core.type.bvtype.BvEqExpr}: equal * - {@link hu.bme.mit.theta.core.type.bvtype.BvNeqExpr}: not equal diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/BvTestUtils.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/BvTestUtils.java new file mode 100644 index 0000000000..df3e21ebd4 --- /dev/null +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/BvTestUtils.java @@ -0,0 +1,135 @@ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.core.type.bvtype.*; + +import java.util.Arrays; +import java.util.Collection; +import java.util.List; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.bvtype.BvExprs.*; +import static hu.bme.mit.theta.core.utils.BvUtils.sint16ToBvLitExpr; +import static hu.bme.mit.theta.core.utils.BvUtils.uint16ToBvLitExpr; + +public class BvTestUtils { + public static Collection BasicOperations() { + return Arrays.asList(new Object[][] { + /* Unsigned basic operations */ + { BvAddExpr.class, UBv16(4), Add(List.of(UBv16(1), UBv16(3))) }, + { BvSubExpr.class, UBv16(1), Sub(UBv16(4), UBv16(3)) }, + { BvMulExpr.class, UBv16(12), Mul(List.of(UBv16(4), UBv16(3))) }, + { BvDivExpr.class, UBv16(4), Div(UBv16(12), UBv16(3)) }, + { BvModExpr.class, UBv16(1), Mod(UBv16(13), UBv16(3)) }, + { BvRemExpr.class, UBv16(1), Rem(UBv16(13), UBv16(3)) }, + + /* Signed basic operations (positive) */ + { BvAddExpr.class, SBv16(4), Add(List.of(SBv16(1), SBv16(3))) }, + { BvSubExpr.class, SBv16(1), Sub(SBv16(4), SBv16(3)) }, + { BvMulExpr.class, SBv16(12), Mul(List.of(SBv16(4), SBv16(3))) }, + { BvDivExpr.class, SBv16(4), Div(SBv16(12), SBv16(3)) }, + { BvModExpr.class, SBv16(1), Mod(SBv16(13), SBv16(3)) }, + { BvRemExpr.class, SBv16(1), Rem(SBv16(13), SBv16(3)) }, + + /* Signed basic operations (negative) */ + { BvAddExpr.class, SBv16(4), Add(List.of(SBv16(-1), SBv16(5))) }, + { BvSubExpr.class, SBv16(-2), Sub(SBv16(4), SBv16(6)) }, + { BvMulExpr.class, SBv16(-12), Mul(List.of(SBv16(-4), SBv16(3))) }, + { BvDivExpr.class, SBv16(-4), Div(SBv16(12), SBv16(-3)) }, + { BvModExpr.class, SBv16(2), Mod(SBv16(-13), SBv16(3)) }, + { BvRemExpr.class, SBv16(1), Rem(SBv16(13), SBv16(3)) }, + { BvRemExpr.class, SBv16(1), Rem(SBv16(13), SBv16(-3)) }, + { BvRemExpr.class, SBv16(-1), Rem(SBv16(-13), SBv16(3)) }, + { BvRemExpr.class, SBv16(-1), Rem(SBv16(-13), SBv16(-3)) }, + { BvNegExpr.class, SBv16(-13), Neg(SBv16(13)) }, + + /* Signed basic operations (overflow) */ + { BvAddExpr.class, SBv16(-32768), Add(List.of(SBv16(32767), SBv16(1))) }, + { BvSubExpr.class, SBv16(32767), Sub(SBv16(-32768), SBv16(1)) }, + { BvMulExpr.class, SBv16(-32768), Mul(List.of(SBv16(16384), SBv16(2))) }, + }); + } + + public static Collection BitvectorOperations() { + return Arrays.asList(new Object[][] { + /* Unsigned bitvector specific operations */ + { BvAndExpr.class, UBv16(1), And(List.of(UBv16(7), UBv16(9))) }, + { BvXorExpr.class, UBv16(14), Xor(List.of(UBv16(7), UBv16(9))) }, + { BvOrExpr.class, UBv16(15), Or(List.of(UBv16(7), UBv16(9))) }, + { BvShiftLeftExpr.class, UBv16(56), ShiftLeft(UBv16(7), UBv16(3)) }, + { BvArithShiftRightExpr.class, UBv16(3), ArithShiftRight(UBv16(7), UBv16(1)) }, + { BvLogicShiftRightExpr.class, UBv16(3), LogicShiftRight(UBv16(7), UBv16(1)) }, + { BvRotateLeftExpr.class, UBv16(13), RotateLeft(UBv16(16387), UBv16(2)) }, + { BvRotateRightExpr.class, UBv16(16387), RotateRight(UBv16(13), UBv16(2)) }, + + /* Signed bitvector specific operations (positive) */ + { BvAndExpr.class, SBv16(1), And(List.of(SBv16(7), SBv16(9))) }, + { BvXorExpr.class, SBv16(14), Xor(List.of(SBv16(7), SBv16(9))) }, + { BvOrExpr.class, SBv16(15), Or(List.of(SBv16(7), SBv16(9))) }, + { BvShiftLeftExpr.class, SBv16(56), ShiftLeft(SBv16(7), SBv16(3)) }, + { BvArithShiftRightExpr.class, SBv16(3), ArithShiftRight(SBv16(7), SBv16(1)) }, + { BvLogicShiftRightExpr.class, SBv16(3), LogicShiftRight(SBv16(7), SBv16(1)) }, + { BvRotateLeftExpr.class, SBv16(13), RotateLeft(SBv16(16387), SBv16(2)) }, + { BvRotateRightExpr.class, SBv16(16387), RotateRight(SBv16(13), SBv16(2)) }, + + /* Signed bitvector specific operations (negative) */ + { BvAndExpr.class, SBv16(9), And(List.of(SBv16(-7), SBv16(9))) }, + { BvXorExpr.class, SBv16(-16), Xor(List.of(SBv16(-7), SBv16(9))) }, + { BvOrExpr.class, SBv16(-7), Or(List.of(SBv16(-7), SBv16(9))) }, + { BvShiftLeftExpr.class, SBv16(-28), ShiftLeft(SBv16(-7), SBv16(2)) }, + { BvArithShiftRightExpr.class, SBv16(-2), ArithShiftRight(SBv16(-7), SBv16(2)) }, + { BvLogicShiftRightExpr.class, SBv16(16382), LogicShiftRight(SBv16(-7), SBv16(2)) }, + { BvRotateLeftExpr.class, SBv16(14), RotateLeft(SBv16(-32765), SBv16(2)) }, + { BvRotateRightExpr.class, SBv16(-32765), RotateRight(SBv16(14), SBv16(2)) }, + { BvNotExpr.class, SBv16(-8), Not(SBv16(7)) }, + }); + } + + public static Collection RelationalOperations() { + return Arrays.asList(new Object[][] { + /* Unsigned relational operations */ + { BvEqExpr.class, True(), Eq(UBv16(4), UBv16(4)) }, + { BvEqExpr.class, False(), Eq(UBv16(4), UBv16(5)) }, + { BvNeqExpr.class, False(), Neq(UBv16(4), UBv16(4)) }, + { BvNeqExpr.class, True(), Neq(UBv16(4), UBv16(5)) }, + { BvLtExpr.class, True(), Lt(UBv16(4), UBv16(5)) }, + { BvLtExpr.class, False(), Lt(UBv16(4), UBv16(4)) }, + { BvLtExpr.class, False(), Lt(UBv16(4), UBv16(3)) }, + { BvLeqExpr.class, True(), Leq(UBv16(4), UBv16(5)) }, + { BvLeqExpr.class, True(), Leq(UBv16(4), UBv16(4)) }, + { BvLeqExpr.class, False(), Leq(UBv16(4), UBv16(3)) }, + { BvGtExpr.class, False(), Gt(UBv16(4), UBv16(5)) }, + { BvGtExpr.class, False(), Gt(UBv16(4), UBv16(4)) }, + { BvGtExpr.class, True(), Gt(UBv16(4), UBv16(3)) }, + { BvGeqExpr.class, False(), Geq(UBv16(4), UBv16(5)) }, + { BvGeqExpr.class, True(), Geq(UBv16(4), UBv16(4)) }, + { BvGeqExpr.class, True(), Geq(UBv16(4), UBv16(3)) }, + + /* Signed relational operations */ + { BvEqExpr.class, True(), Eq(SBv16(4), SBv16(4)) }, + { BvEqExpr.class, False(), Eq(SBv16(4), SBv16(5)) }, + { BvNeqExpr.class, False(), Neq(SBv16(4), SBv16(4)) }, + { BvNeqExpr.class, True(), Neq(SBv16(4), SBv16(5)) }, + { BvLtExpr.class, True(), Lt(SBv16(4), SBv16(5)) }, + { BvLtExpr.class, False(), Lt(SBv16(4), SBv16(4)) }, + { BvLtExpr.class, False(), Lt(SBv16(4), SBv16(3)) }, + { BvLeqExpr.class, True(), Leq(SBv16(4), SBv16(5)) }, + { BvLeqExpr.class, True(), Leq(SBv16(4), SBv16(4)) }, + { BvLeqExpr.class, False(), Leq(SBv16(4), SBv16(3)) }, + { BvGtExpr.class, False(), Gt(SBv16(4), SBv16(5)) }, + { BvGtExpr.class, False(), Gt(SBv16(4), SBv16(4)) }, + { BvGtExpr.class, True(), Gt(SBv16(4), SBv16(3)) }, + { BvGeqExpr.class, False(), Geq(SBv16(4), SBv16(5)) }, + { BvGeqExpr.class, True(), Geq(SBv16(4), SBv16(4)) }, + { BvGeqExpr.class, True(), Geq(SBv16(4), SBv16(3)) }, + }); + } + + private static BvLitExpr UBv16(int integer) { + return uint16ToBvLitExpr(integer); + } + + private static BvLitExpr SBv16(int integer) { + return sint16ToBvLitExpr(integer); + } +} diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index b6ffe0a42b..266260acea 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -169,7 +169,13 @@ public final class ExprSimplifier { .addCase(BvShiftLeftExpr.class, ExprSimplifier::simplifyBvShiftLeft) - .addCase(BvShiftRightExpr.class, ExprSimplifier::simplifyBvShiftRight) + .addCase(BvArithShiftRightExpr.class, ExprSimplifier::simplifyBvArithShiftRight) + + .addCase(BvLogicShiftRightExpr.class, ExprSimplifier::simplifyBvLogicShiftRight) + + .addCase(BvRotateLeftExpr.class, ExprSimplifier::simplifyBvRotateLeft) + + .addCase(BvRotateRightExpr.class, ExprSimplifier::simplifyBvRotateRight) .addCase(BvEqExpr.class, ExprSimplifier::simplifyBvEq) @@ -1264,14 +1270,53 @@ private static Expr simplifyBvShiftLeft(final BvShiftLeftExpr expr, fina return expr.with(leftOp, rightOp); } - private static Expr simplifyBvShiftRight(final BvShiftRightExpr expr, final Valuation val) { + private static Expr simplifyBvArithShiftRight(final BvArithShiftRightExpr expr, final Valuation val) { + final Expr leftOp = simplify(expr.getLeftOp(), val); + final Expr rightOp = simplify(expr.getRightOp(), val); + + if (leftOp instanceof BvLitExpr && rightOp instanceof BvLitExpr) { + final BvLitExpr leftLit = (BvLitExpr) leftOp; + final BvLitExpr rightLit = (BvLitExpr) rightOp; + return leftLit.arithShiftRight(rightLit); + } + + return expr.with(leftOp, rightOp); + } + + private static Expr simplifyBvLogicShiftRight(final BvLogicShiftRightExpr expr, final Valuation val) { + final Expr leftOp = simplify(expr.getLeftOp(), val); + final Expr rightOp = simplify(expr.getRightOp(), val); + + if (leftOp instanceof BvLitExpr && rightOp instanceof BvLitExpr) { + final BvLitExpr leftLit = (BvLitExpr) leftOp; + final BvLitExpr rightLit = (BvLitExpr) rightOp; + return leftLit.logicShiftRight(rightLit); + } + + return expr.with(leftOp, rightOp); + } + + private static Expr simplifyBvRotateLeft(final BvRotateLeftExpr expr, final Valuation val) { + final Expr leftOp = simplify(expr.getLeftOp(), val); + final Expr rightOp = simplify(expr.getRightOp(), val); + + if (leftOp instanceof BvLitExpr && rightOp instanceof BvLitExpr) { + final BvLitExpr leftLit = (BvLitExpr) leftOp; + final BvLitExpr rightLit = (BvLitExpr) rightOp; + return leftLit.rotateLeft(rightLit); + } + + return expr.with(leftOp, rightOp); + } + + private static Expr simplifyBvRotateRight(final BvRotateRightExpr expr, final Valuation val) { final Expr leftOp = simplify(expr.getLeftOp(), val); final Expr rightOp = simplify(expr.getRightOp(), val); if (leftOp instanceof BvLitExpr && rightOp instanceof BvLitExpr) { final BvLitExpr leftLit = (BvLitExpr) leftOp; final BvLitExpr rightLit = (BvLitExpr) rightOp; - return leftLit.shiftRight(rightLit); + return leftLit.rotateRight(rightLit); } return expr.with(leftOp, rightOp); diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/BvTypeTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/BvTypeTest.java new file mode 100644 index 0000000000..3528b039ea --- /dev/null +++ b/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/BvTypeTest.java @@ -0,0 +1,60 @@ +package hu.bme.mit.theta.core.type; + +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.utils.BvTestUtils; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.util.Collection; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import static org.junit.Assert.*; + +@RunWith(Parameterized.class) +public class BvTypeTest { + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameterized.Parameters(name = "expr: {0}, expected: {1}, actual: {2}") + public static Collection operations() { + return Stream.concat( + BvTestUtils.BasicOperations().stream(), + Stream.concat( + BvTestUtils.BitvectorOperations().stream(), + BvTestUtils.RelationalOperations().stream() + ) + ).collect(Collectors.toUnmodifiableList()); + } + + @Test + public void testBV() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + Valuation val = ImmutableValuation.builder().build(); + assertEquals(expected.eval(val), actual.eval(val)); + } +} diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvBasicOperationTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvBasicOperationTest.java deleted file mode 100644 index 5cfd359cf9..0000000000 --- a/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvBasicOperationTest.java +++ /dev/null @@ -1,86 +0,0 @@ -package hu.bme.mit.theta.core.type.bvtype; - -import hu.bme.mit.theta.core.model.ImmutableValuation; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.type.Expr; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; - -import java.util.*; - -import static hu.bme.mit.theta.core.utils.BvUtils.sint16ToBvLitExpr; -import static hu.bme.mit.theta.core.utils.BvUtils.uint16ToBvLitExpr; -import static hu.bme.mit.theta.core.type.bvtype.BvExprs.*; -import static org.junit.Assert.*; -import static org.junit.runners.Parameterized.*; - -@RunWith(Parameterized.class) -public class BvBasicOperationTest { - private final Class bvExpr; - private final Expr lhs; - private final Expr rhs; - - @Parameters - public static Collection operations() { - return Arrays.asList(new Object[][] { - /* Unsigned basic operations */ - { BvAddExpr.class, UBv16(4), Add(List.of(UBv16(1), UBv16(3))) }, - { BvSubExpr.class, UBv16(1), Sub(UBv16(4), UBv16(3)) }, - { BvMulExpr.class, UBv16(12), Mul(List.of(UBv16(4), UBv16(3))) }, - { BvDivExpr.class, UBv16(4), Div(UBv16(12), UBv16(3)) }, - { BvModExpr.class, UBv16(1), Mod(UBv16(13), UBv16(3)) }, - { BvRemExpr.class, UBv16(1), Rem(UBv16(13), UBv16(3)) }, - - /* Signed basic operations (positive) */ - { BvAddExpr.class, SBv16(4), Add(List.of(SBv16(1), SBv16(3))) }, - { BvSubExpr.class, SBv16(1), Sub(SBv16(4), SBv16(3)) }, - { BvMulExpr.class, SBv16(12), Mul(List.of(SBv16(4), SBv16(3))) }, - { BvDivExpr.class, SBv16(4), Div(SBv16(12), SBv16(3)) }, - { BvModExpr.class, SBv16(1), Mod(SBv16(13), SBv16(3)) }, - { BvRemExpr.class, SBv16(1), Rem(SBv16(13), SBv16(3)) }, - - /* Signed basic operations (negative) */ - { BvAddExpr.class, SBv16(4), Add(List.of(SBv16(-1), SBv16(5))) }, - { BvSubExpr.class, SBv16(-2), Sub(SBv16(4), SBv16(6)) }, - { BvMulExpr.class, SBv16(-12), Mul(List.of(SBv16(-4), SBv16(3))) }, - { BvDivExpr.class, SBv16(-4), Div(SBv16(12), SBv16(-3)) }, - { BvModExpr.class, SBv16(2), Mod(SBv16(-13), SBv16(3)) }, - { BvRemExpr.class, SBv16(-1), Rem(SBv16(13), SBv16(-3)) }, - { BvNegExpr.class, SBv16(-13), Neg(SBv16(13)) }, - - /* Signed basic operations (overflow) */ - { BvAddExpr.class, SBv16(-32768), Add(List.of(SBv16(32767), SBv16(1))) }, - { BvSubExpr.class, SBv16(32767), Sub(SBv16(-32768), SBv16(1)) }, - { BvMulExpr.class, SBv16(-32768), Mul(List.of(SBv16(16384), SBv16(2))) }, - }); - } - - public BvBasicOperationTest(Class bvExpr, Expr lhs, Expr rhs) { - this.bvExpr = bvExpr; - this.lhs = lhs; - this.rhs = rhs; - } - - @Test - public void testOperationEquals() { - Valuation val = ImmutableValuation.builder().build(); - assertNotNull(bvExpr); - assertEquals(lhs.eval(val), rhs.eval(val)); - } - - @Test - public void testOperationNotEquals() { - Valuation val = ImmutableValuation.builder().build(); - assertNotNull(bvExpr); - assertNotEquals((rhs.getType().isSigned() ? SBv16(0) : UBv16(0)).eval(val), rhs.eval(val)); - } - - private static BvLitExpr UBv16(int integer) { - return uint16ToBvLitExpr(integer); - } - - private static BvLitExpr SBv16(int integer) { - return sint16ToBvLitExpr(integer); - } -} diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvBitvectorOperationTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvBitvectorOperationTest.java deleted file mode 100644 index e87485b0a5..0000000000 --- a/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvBitvectorOperationTest.java +++ /dev/null @@ -1,78 +0,0 @@ -package hu.bme.mit.theta.core.type.bvtype; - -import hu.bme.mit.theta.core.model.ImmutableValuation; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.type.Expr; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; - -import java.util.*; - -import static hu.bme.mit.theta.core.utils.BvUtils.sint16ToBvLitExpr; -import static hu.bme.mit.theta.core.utils.BvUtils.uint16ToBvLitExpr; -import static hu.bme.mit.theta.core.type.bvtype.BvExprs.*; -import static org.junit.Assert.*; -import static org.junit.runners.Parameterized.*; - -@RunWith(Parameterized.class) -public class BvBitvectorOperationTest { - private final Class bvExpr; - private final Expr lhs; - private final Expr rhs; - - @Parameters - public static Collection operations() { - return Arrays.asList(new Object[][] { - /* Unsigned bitvector specific operations */ - { BvAndExpr.class, UBv16(1), And(List.of(UBv16(7), UBv16(9))) }, - { BvXorExpr.class, UBv16(14), Xor(List.of(UBv16(7), UBv16(9))) }, - { BvOrExpr.class, UBv16(15), Or(List.of(UBv16(7), UBv16(9))) }, - { BvShiftLeftExpr.class, UBv16(56), ShiftLeft(UBv16(7), UBv16(3)) }, - { BvShiftRightExpr.class, UBv16(3), ShiftRight(UBv16(7), UBv16(1)) }, - - /* Signed bitvector specific operations (positive) */ - { BvAndExpr.class, SBv16(1), And(List.of(SBv16(7), SBv16(9))) }, - { BvXorExpr.class, SBv16(14), Xor(List.of(SBv16(7), SBv16(9))) }, - { BvOrExpr.class, SBv16(15), Or(List.of(SBv16(7), SBv16(9))) }, - { BvShiftLeftExpr.class, SBv16(56), ShiftLeft(SBv16(7), SBv16(3)) }, - { BvShiftRightExpr.class, SBv16(3), ShiftRight(SBv16(7), SBv16(1)) }, - - /* Signed bitvector specific operations (negative) */ - { BvAndExpr.class, SBv16(9), And(List.of(SBv16(-7), SBv16(9))) }, - { BvXorExpr.class, SBv16(-16), Xor(List.of(SBv16(-7), SBv16(9))) }, - { BvOrExpr.class, SBv16(-7), Or(List.of(SBv16(-7), SBv16(9))) }, - { BvShiftLeftExpr.class, SBv16(-28), ShiftLeft(SBv16(-7), SBv16(2)) }, - { BvShiftRightExpr.class, SBv16(-2), ShiftRight(SBv16(-7), SBv16(2)) }, - { BvNotExpr.class, SBv16(-8), Not(SBv16(7)) }, - }); - } - - public BvBitvectorOperationTest(Class bvExpr, Expr lhs, Expr rhs) { - this.bvExpr = bvExpr; - this.lhs = lhs; - this.rhs = rhs; - } - - @Test - public void testOperationEquals() { - Valuation val = ImmutableValuation.builder().build(); - assertNotNull(bvExpr); - assertEquals(lhs.eval(val), rhs.eval(val)); - } - - @Test - public void testOperationNotEquals() { - Valuation val = ImmutableValuation.builder().build(); - assertNotNull(bvExpr); - assertNotEquals((rhs.getType().isSigned() ? SBv16(0) : UBv16(0)).eval(val), rhs.eval(val)); - } - - private static BvLitExpr UBv16(int integer) { - return uint16ToBvLitExpr(integer); - } - - private static BvLitExpr SBv16(int integer) { - return sint16ToBvLitExpr(integer); - } -} diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvRelationalOperationTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvRelationalOperationTest.java deleted file mode 100644 index 8a60bf5e7a..0000000000 --- a/subprojects/core/src/test/java/hu/bme/mit/theta/core/type/bvtype/BvRelationalOperationTest.java +++ /dev/null @@ -1,88 +0,0 @@ -package hu.bme.mit.theta.core.type.bvtype; - -import hu.bme.mit.theta.core.model.ImmutableValuation; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; - -import java.util.Arrays; -import java.util.Collection; -import java.util.List; -import java.util.function.BiFunction; - -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; -import static hu.bme.mit.theta.core.type.bvtype.BvExprs.*; -import static hu.bme.mit.theta.core.utils.BvUtils.sint16ToBvLitExpr; -import static hu.bme.mit.theta.core.utils.BvUtils.uint16ToBvLitExpr; -import static org.junit.Assert.*; -import static org.junit.runners.Parameterized.Parameters; - -@RunWith(Parameterized.class) -public class BvRelationalOperationTest { - private final Expr lhs; - private final boolean result; - - @Parameters - public static Collection operations() { - return Arrays.asList(new Object[][] { - /* Unsigned relational operations */ - { Eq(UBv16(4), UBv16(4)), true }, - { Eq(UBv16(4), UBv16(5)), false }, - { Neq(UBv16(4), UBv16(4)), false }, - { Neq(UBv16(4), UBv16(5)), true }, - { Lt(UBv16(4), UBv16(5)), true }, - { Lt(UBv16(4), UBv16(4)), false }, - { Lt(UBv16(4), UBv16(3)), false }, - { Leq(UBv16(4), UBv16(5)), true }, - { Leq(UBv16(4), UBv16(4)), true }, - { Leq(UBv16(4), UBv16(3)), false }, - { Gt(UBv16(4), UBv16(5)), false }, - { Gt(UBv16(4), UBv16(4)), false }, - { Gt(UBv16(4), UBv16(3)), true }, - { Geq(UBv16(4), UBv16(5)), false }, - { Geq(UBv16(4), UBv16(4)), true }, - { Geq(UBv16(4), UBv16(3)), true }, - - /* Signed relational operations */ - { Eq(SBv16(4), SBv16(4)), true }, - { Eq(SBv16(4), SBv16(5)), false }, - { Neq(SBv16(4), SBv16(4)), false }, - { Neq(SBv16(4), SBv16(5)), true }, - { Lt(SBv16(4), SBv16(5)), true }, - { Lt(SBv16(4), SBv16(4)), false }, - { Lt(SBv16(4), SBv16(3)), false }, - { Leq(SBv16(4), SBv16(5)), true }, - { Leq(SBv16(4), SBv16(4)), true }, - { Leq(SBv16(4), SBv16(3)), false }, - { Gt(SBv16(4), SBv16(5)), false }, - { Gt(SBv16(4), SBv16(4)), false }, - { Gt(SBv16(4), SBv16(3)), true }, - { Geq(SBv16(4), SBv16(5)), false }, - { Geq(SBv16(4), SBv16(4)), true }, - { Geq(SBv16(4), SBv16(3)), true }, - }); - } - - public BvRelationalOperationTest(Expr lhs, Boolean result) { - this.lhs = lhs; - this.result = result; - } - - @Test - public void testOperationEquals() { - Valuation val = ImmutableValuation.builder().build(); - assertEquals(result ? True() : False(), lhs.eval(val)); - } - - private static BvLitExpr UBv16(int integer) { - return uint16ToBvLitExpr(integer); - } - - private static BvLitExpr SBv16(int integer) { - return sint16ToBvLitExpr(integer); - } -} diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java index 4e447d88aa..ef4b9b3718 100644 --- a/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java +++ b/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java @@ -63,7 +63,6 @@ import hu.bme.mit.theta.core.type.bvtype.BvType; import hu.bme.mit.theta.core.type.inttype.IntExprs; import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.core.type.arraytype.ArrayExprs; import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; import org.junit.Test; @@ -583,7 +582,7 @@ public void testBvShift() { assertEquals( Bv(new boolean[] {false, false, false, true}, true), - simplify(BvExprs.ShiftRight( + simplify(BvExprs.ArithShiftRight( Bv(new boolean[] {false, true, false, false}, true), Bv(new boolean[] {false, false, true, false}, true) )) @@ -591,7 +590,7 @@ public void testBvShift() { assertEquals( Bv(new boolean[] {true, true, true, false}, true), - simplify(BvExprs.ShiftRight( + simplify(BvExprs.ArithShiftRight( Bv(new boolean[] {true, true, false, false}, true), Bv(new boolean[] {false, false, false, true}, true) )) diff --git a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index 5f0aa7014c..f74c4fa79c 100644 --- a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -205,7 +205,13 @@ public Z3ExprTransformer(final Z3TransformationManager transformer, final Contex .addCase(BvShiftLeftExpr.class, this::transformBvShiftLeft) - .addCase(BvShiftRightExpr.class, this::transformBvShiftRight) + .addCase(BvArithShiftRightExpr.class, this::transformBvArithShiftRight) + + .addCase(BvLogicShiftRightExpr.class, this::transformBvLogicShiftRight) + + .addCase(BvRotateLeftExpr.class, this::transformBvRotateLeft) + + .addCase(BvRotateRightExpr.class, this::transformBvRotateRight) .addCase(BvEqExpr.class, this::transformBvEq) @@ -656,15 +662,32 @@ private com.microsoft.z3.Expr transformBvShiftLeft(final BvShiftLeftExpr expr) { return context.mkBVSHL(leftOpTerm, rightOpTerm); } - private com.microsoft.z3.Expr transformBvShiftRight(final BvShiftRightExpr expr) { + private com.microsoft.z3.Expr transformBvArithShiftRight(final BvArithShiftRightExpr expr) { final com.microsoft.z3.BitVecExpr leftOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getLeftOp()); final com.microsoft.z3.BitVecExpr rightOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getRightOp()); - if(expr.getType().isSigned()) { - return context.mkBVASHR(leftOpTerm, rightOpTerm); - } else { - return context.mkBVLSHR(leftOpTerm, rightOpTerm); - } + return context.mkBVASHR(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformBvLogicShiftRight(final BvLogicShiftRightExpr expr) { + final com.microsoft.z3.BitVecExpr leftOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.BitVecExpr rightOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getRightOp()); + + return context.mkBVLSHR(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformBvRotateLeft(final BvRotateLeftExpr expr) { + final com.microsoft.z3.BitVecExpr leftOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.BitVecExpr rightOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getRightOp()); + + return context.mkBVRotateLeft(leftOpTerm, rightOpTerm); + } + + private com.microsoft.z3.Expr transformBvRotateRight(final BvRotateRightExpr expr) { + final com.microsoft.z3.BitVecExpr leftOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getLeftOp()); + final com.microsoft.z3.BitVecExpr rightOpTerm = (com.microsoft.z3.BitVecExpr) toTerm(expr.getRightOp()); + + return context.mkBVRotateRight(leftOpTerm, rightOpTerm); } private com.microsoft.z3.Expr transformBvGeq(final BvGeqExpr expr) { diff --git a/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverBVTest.java b/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverBVTest.java new file mode 100644 index 0000000000..8f7cf917af --- /dev/null +++ b/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverBVTest.java @@ -0,0 +1,68 @@ +package hu.bme.mit.theta.solver.z3; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.utils.BvTestUtils; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; + +import java.util.Collection; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import static org.junit.Assert.*; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class Z3SolverBVTest { + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameters(name = "expr: {0}, expected: {1}, actual: {2}") + public static Collection operations() { + return Stream.concat( + BvTestUtils.BasicOperations().stream(), + Stream.concat( + BvTestUtils.BitvectorOperations().stream(), + BvTestUtils.RelationalOperations().stream() + ) + ).collect(Collectors.toUnmodifiableList()); + } + + @Test + public void testOperationEquals() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + final Solver solver = Z3SolverFactory.getInstance().createSolver(); + solver.push(); + + solver.add(EqExpr.create2(expected, actual)); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + } +} diff --git a/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java b/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java index ba39fe009d..02a2159834 100644 --- a/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java +++ b/subprojects/solver-z3/src/test/java/hu/bme/mit/theta/solver/z3/Z3SolverTest.java @@ -400,7 +400,7 @@ public void testBV12() { solver.push(); solver.add(BvExprs.Eq(cy.getRef(), Bv(new boolean[] {false, true, false, false}, false))); - solver.add(BvExprs.Eq(BvExprs.ShiftRight(cy.getRef(), Bv(new boolean[] {false, false, false, true}, false)), cx.getRef())); + solver.add(BvExprs.Eq(BvExprs.ArithShiftRight(cy.getRef(), Bv(new boolean[] {false, false, false, true}, false)), cx.getRef())); SolverStatus status = solver.check(); assertTrue(status.isSat());