diff --git a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java index e209cd2f33..4b47016cde 100644 --- a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java @@ -266,6 +266,18 @@ BooleanFormula greaterOrEquals( */ BitvectorFormula shiftLeft(BitvectorFormula number, BitvectorFormula toShift); + /** + * This method returns a term representing the right rotation of number by toRotate. The result + * has the same length as the given number. + */ + BitvectorFormula rotateRight(BitvectorFormula number, BitvectorFormula toRotate); + + /** + * This method returns a term representing the left shift of number by toRotate. The result has + * the same length as the given number. + */ + BitvectorFormula rotateLeft(BitvectorFormula number, BitvectorFormula toRotate); + /** Concatenate two bitvectors. */ BitvectorFormula concat(BitvectorFormula prefix, BitvectorFormula suffix); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java index becaf0204f..b01ab32c8b 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java @@ -314,6 +314,28 @@ public BitvectorFormula shiftLeft(BitvectorFormula pNumber, BitvectorFormula toS protected abstract TFormulaInfo shiftLeft(TFormulaInfo pExtract, TFormulaInfo pExtract2); + /** Return a term representing the right rotation of number by toRotate. */ + @Override + public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula toRotate) { + TFormulaInfo param1 = extractInfo(pNumber); + TFormulaInfo param2 = extractInfo(toRotate); + + return wrap(rotateRight(param1, param2)); + } + + protected abstract TFormulaInfo rotateRight(TFormulaInfo pNumber, TFormulaInfo toRotate); + + /** Return a term representing the left rotation of number by toRotate. */ + @Override + public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula toRotate) { + TFormulaInfo param1 = extractInfo(pNumber); + TFormulaInfo param2 = extractInfo(toRotate); + + return wrap(rotateLeft(param1, param2)); + } + + protected abstract TFormulaInfo rotateLeft(TFormulaInfo pNumber, TFormulaInfo toRotate); + @Override public final BitvectorFormula concat(BitvectorFormula pNumber, BitvectorFormula pAppend) { TFormulaInfo param1 = extractInfo(pNumber); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBitvectorFormulaManager.java index 9eaf002844..a55baa3c4c 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBitvectorFormulaManager.java @@ -178,6 +178,18 @@ public BitvectorFormula shiftLeft(BitvectorFormula pNumber, BitvectorFormula pTo return delegate.shiftLeft(pNumber, pToShift); } + @Override + public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula pToRotate) { + stats.bvOperations.getAndIncrement(); + return delegate.rotateRight(pNumber, pToRotate); + } + + @Override + public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula pToRotate) { + stats.bvOperations.getAndIncrement(); + return delegate.rotateLeft(pNumber, pToRotate); + } + @Override public BitvectorFormula concat(BitvectorFormula pNumber, BitvectorFormula pAppend) { stats.bvOperations.getAndIncrement(); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBitvectorFormulaManager.java index 4d0fb77481..5968c0f7d4 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBitvectorFormulaManager.java @@ -204,6 +204,20 @@ public BitvectorFormula shiftLeft(BitvectorFormula pNumber, BitvectorFormula pTo } } + @Override + public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula pToRotate) { + synchronized (sync) { + return delegate.rotateRight(pNumber, pToRotate); + } + } + + @Override + public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula pToRotate) { + synchronized (sync) { + return delegate.rotateLeft(pNumber, pToRotate); + } + } + @Override public BitvectorFormula concat(BitvectorFormula pNumber, BitvectorFormula pAppend) { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java index 4a83f55327..4e11af9a61 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java @@ -16,6 +16,8 @@ import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_neg; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_not; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_or; +import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_rol; +import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_ror; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sdiv; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sext; import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sgt; @@ -187,6 +189,16 @@ public Long shiftLeft(Long bitVec, Long toShift) { return boolector_sll(btor, bitVec, toShift); } + @Override + protected Long rotateRight(Long pNumber, Long toRotate) { + return boolector_ror(btor, pNumber, toRotate); + } + + @Override + protected Long rotateLeft(Long pNumber, Long toRotate) { + return boolector_rol(btor, pNumber, toRotate); + } + @Override public Long concat(Long bitVec, Long bitVecAppend) { return boolector_concat(btor, bitVec, bitVecAppend); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java index 649dcc01cc..96e194c5b0 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java @@ -84,6 +84,24 @@ protected Expr shiftLeft(Expr pParam1, Expr pParam2) { return exprManager.mkExpr(Kind.BITVECTOR_SHL, pParam1, pParam2); } + @Override + protected Expr rotateRight(Expr pNumber, Expr toRotate) { + // cvc4 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber + // toRotate) (bvshl pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Expr size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate))); + } + + @Override + protected Expr rotateLeft(Expr pNumber, Expr toRotate) { + // cvc4 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber + // toRotate) (bvlshr pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Expr size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), false)); + } + @Override protected Expr not(Expr pParam1) { return exprManager.mkExpr(Kind.BITVECTOR_NOT, pParam1); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java index e68040c4cb..57acdc0afb 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java @@ -16,6 +16,7 @@ import io.github.cvc5.Term; import java.math.BigInteger; import java.util.List; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; public class CVC5BitvectorFormulaManager @@ -125,6 +126,24 @@ protected Term shiftLeft(Term pParam1, Term pParam2) { return solver.mkTerm(Kind.BITVECTOR_SHL, pParam1, pParam2); } + @Override + protected Term rotateRight(Term pNumber, Term toRotate) { + // cvc5 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber + // toRotate) (bvshl pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Term size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate))); + } + + @Override + protected Term rotateLeft(Term pNumber, Term toRotate) { + // cvc5 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber + // toRotate) (bvlshr pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Term size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), false)); + } + @Override protected Term not(Term pParam1) { return solver.mkTerm(Kind.BITVECTOR_NOT, pParam1); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java index ed0c4be854..b7302ddd9e 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java @@ -38,6 +38,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_to_bv; import java.math.BigInteger; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; /** Mathsat Bitvector Theory, build out of Bitvector*Operations. */ @@ -125,6 +126,24 @@ public Long shiftLeft(Long number, Long toShift) { return msat_make_bv_lshl(mathsatEnv, number, toShift); } + @Override + protected Long rotateRight(Long pNumber, Long toRotate) { + // MathSAT5 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber + // toRotate) (bvshl pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Long size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate))); + } + + @Override + protected Long rotateLeft(Long pNumber, Long toRotate) { + // MathSAT5 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber + // toRotate) (bvlshr pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Long size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), false)); + } + @Override public Long not(Long pBits) { return msat_make_bv_not(mathsatEnv, pBits); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java index dfb1f2ed30..cfda3bf657 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java @@ -16,6 +16,7 @@ import ap.types.Sort$; import com.google.common.base.Preconditions; import java.math.BigInteger; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; import scala.Option; @@ -177,6 +178,24 @@ protected IExpression shiftLeft(IExpression pExtract, IExpression pExtract2) { return ModuloArithmetic$.MODULE$.bvshl((ITerm) pExtract, (ITerm) pExtract2); } + @Override + protected IExpression rotateRight(IExpression pNumber, IExpression toRotate) { + // Princess does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber + // toRotate) (bvshl pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final IExpression size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate))); + } + + @Override + protected IExpression rotateLeft(IExpression pNumber, IExpression toRotate) { + // Princess does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber + // toRotate) (bvlshr pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final IExpression size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), false)); + } + @Override protected IExpression concat(IExpression number, IExpression pAppend) { return ModuloArithmetic$.MODULE$.concat((ITerm) number, (ITerm) pAppend); diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java index 295d1caa4c..3f97121f69 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java @@ -41,6 +41,7 @@ import com.google.common.base.Preconditions; import com.google.common.base.Strings; import java.math.BigInteger; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager; public class Yices2BitvectorFormulaManager @@ -191,6 +192,24 @@ protected Integer shiftLeft(Integer pNumber, Integer pToShift) { return yices_bvshl(pNumber, pToShift); } + @Override + protected Integer rotateRight(Integer pNumber, Integer toRotate) { + // Yices2 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber + // toRotate) (bvshl pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Integer size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate))); + } + + @Override + protected Integer rotateLeft(Integer pNumber, Integer toRotate) { + // Yices2 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber + // toRotate) (bvlshr pNumber (bvsub size toRotate))) + final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize(); + final Integer size = this.makeBitvectorImpl(bitsize, bitsize); + return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), false)); + } + @Override protected Integer concat(Integer pNumber, Integer pAppend) { return yices_bvconcat2(pNumber, pAppend); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java index c87b4c3b1f..fb7e1887a8 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3BitvectorFormulaManager.java @@ -82,6 +82,16 @@ public Long shiftLeft(Long number, Long toShift) { return Native.mkBvshl(z3context, number, toShift); } + @Override + protected Long rotateRight(Long pNumber, Long toRotate) { + return Native.mkExtRotateRight(z3context, pNumber, toRotate); + } + + @Override + protected Long rotateLeft(Long pNumber, Long toRotate) { + return Native.mkExtRotateLeft(z3context, pNumber, toRotate); + } + @Override public Long not(Long pBits) { return Native.mkBvnot(z3context, pBits); diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index a3a27aa153..2498552d1f 100644 --- a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java @@ -397,4 +397,29 @@ public void bvVarDistinct() throws SolverException, InterruptedException { assertThatFormula(bvmgr.distinct(List.of(a, a))).isUnsatisfiable(); assertThatFormula(bvmgr.distinct(List.of(num3, num3))).isUnsatisfiable(); } + + @Test + public void bvRotateLeft() throws SolverException, InterruptedException { + // (ROL 0001 0010) == 0100 + // (ROL 0100 0010) == 0001 + BitvectorFormula bf1 = bvmgr.makeBitvector(4, BigInteger.ONE); + BitvectorFormula bf2 = bvmgr.makeBitvector(4, BigInteger.TWO); + BitvectorFormula bf3 = bvmgr.makeBitvector(4, BigInteger.valueOf(4)); + + assertThatFormula(bvmgr.equal(bvmgr.rotateLeft(bf1, bf2), bf3)).isTautological(); + assertThatFormula(bvmgr.equal(bvmgr.rotateLeft(bf3, bf2), bf1)).isTautological(); + } + + @Test + public void bvRotateRight() throws SolverException, InterruptedException { + // (ROR 0001 0011) == 0010 + // (ROR 0010 0011) == 0100 + BitvectorFormula bf1 = bvmgr.makeBitvector(4, BigInteger.ONE); + BitvectorFormula bf2 = bvmgr.makeBitvector(4, BigInteger.valueOf(3)); + BitvectorFormula bf3 = bvmgr.makeBitvector(4, BigInteger.TWO); + BitvectorFormula bf4 = bvmgr.makeBitvector(4, BigInteger.valueOf(4)); + + assertThatFormula(bvmgr.equal(bvmgr.rotateRight(bf1, bf2), bf3)).isTautological(); + assertThatFormula(bvmgr.equal(bvmgr.rotateRight(bf3, bf2), bf4)).isTautological(); + } }