Merge pull request #62 from ftsrg/bitvector-extras

Additional bitvector operations
ftsrg · Jul 30, 2020 · aafb6d8 · aafb6d8
2 parents d4519c9 + 001d25b
commit aafb6d8
Show file tree

Hide file tree

Showing 25 changed files with 813 additions and 331 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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) }
+}
diff --git 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
@@ -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,13 +48,17 @@
 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;
 import java.util.Collections;
 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<BvType> leftOp = castBv(ctx.leftOp.accept(this));
+			final Expr<BvType> 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<BvType> leftOp = castBv(ctx.leftOp.accept(this));
+			final Expr<BvType> 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<BvType> leftOp = castBv(ctx.leftOp.accept(this));
+			final Expr<BvType> 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<BvType> leftOp = castBv(ctx.leftOp.accept(this));
+			final Expr<BvType> 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/...ta/core/type/bvtype/BvShiftRightExpr.java → ...re/type/bvtype/BvArithShiftRightExpr.java b/...ta/core/type/bvtype/BvShiftRightExpr.java → ...re/type/bvtype/BvArithShiftRightExpr.java
@@ -6,23 +6,23 @@
 
 import static hu.bme.mit.theta.core.utils.TypeUtils.*;
 
-public class BvShiftRightExpr extends BinaryExpr<BvType, BvType> {
+public class BvArithShiftRightExpr extends BinaryExpr<BvType, BvType> {
     private static final int HASH_SEED = 965;
     private static final String OPERATOR_LABEL = ">>";
 
-    private BvShiftRightExpr(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
+    private BvArithShiftRightExpr(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
         super(leftOp, rightOp);
         checkAllTypesEqual(leftOp, rightOp);
     }
 
-    public static BvShiftRightExpr of(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
-        return new BvShiftRightExpr(leftOp, rightOp);
+    public static BvArithShiftRightExpr of(final Expr<BvType> leftOp, final Expr<BvType> 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<BvType> newLeftOp = castBv(leftOp);
         final Expr<BvType> newRightOp = castBv(rightOp);
-        return BvShiftRightExpr.of(newLeftOp, newRightOp);
+        return BvArithShiftRightExpr.of(newLeftOp, newRightOp);
     }
 
     @Override
@@ -34,34 +34,34 @@ 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<BvType> leftOp, final Expr<BvType> rightOp) {
+    public BvArithShiftRightExpr with(final Expr<BvType> leftOp, final Expr<BvType> 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<BvType> leftOp) {
+    public BvArithShiftRightExpr withLeftOp(final Expr<BvType> leftOp) {
         return with(leftOp, getRightOp());
     }
 
     @Override
-    public BvShiftRightExpr withRightOp(final Expr<BvType> rightOp) {
+    public BvArithShiftRightExpr withRightOp(final Expr<BvType> rightOp) {
         return with(getLeftOp(), rightOp);
     }
 
     @Override
     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
@@ -66,8 +66,20 @@ public static BvShiftLeftExpr ShiftLeft(final Expr<BvType> leftOp, final Expr<Bv
         return BvShiftLeftExpr.of(leftOp, rightOp);
     }
 
-    public static BvShiftRightExpr ShiftRight(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
-        return BvShiftRightExpr.of(leftOp, rightOp);
+    public static BvArithShiftRightExpr ArithShiftRight(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
+        return BvArithShiftRightExpr.of(leftOp, rightOp);
+    }
+
+    public static BvLogicShiftRightExpr LogicShiftRight(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
+        return BvLogicShiftRightExpr.of(leftOp, rightOp);
+    }
+
+    public static BvRotateLeftExpr RotateLeft(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
+        return BvRotateLeftExpr.of(leftOp, rightOp);
+    }
+
+    public static BvRotateRightExpr RotateRight(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {
+        return BvRotateRightExpr.of(leftOp, rightOp);
     }
 
     public static BvEqExpr Eq(final Expr<BvType> leftOp, final Expr<BvType> rightOp) {