diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index e2572ab820..06b6b53e9d 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -15,6 +15,7 @@ import java.math.BigInteger; import java.util.HashMap; import java.util.Map; +import org.sosy_lab.common.MoreStrings; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -25,6 +26,7 @@ import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; /** @@ -258,6 +260,14 @@ protected abstract TFormulaInfo castFromImpl( @Override public FloatingPointFormula fromIeeeBitvector( BitvectorFormula pNumber, FloatingPointType pTargetType) { + BitvectorType bvType = (BitvectorType) formulaCreator.getFormulaType(pNumber); + Preconditions.checkArgument( + bvType.getSize() == pTargetType.getTotalSize(), + MoreStrings.lazyString( + () -> + String.format( + "The total size %s of type %s has to match the size %s of type %s.", + pTargetType.getTotalSize(), pTargetType, bvType.getSize(), bvType))); return wrap(fromIeeeBitvectorImpl(extractInfo(pNumber), pTargetType)); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java index 248f6a55a8..1dbf7f7821 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java @@ -10,13 +10,13 @@ import com.google.common.collect.ImmutableList; import edu.stanford.CVC4.BitVector; -import edu.stanford.CVC4.BitVectorExtract; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.FloatingPoint; import edu.stanford.CVC4.FloatingPointConvertSort; import edu.stanford.CVC4.FloatingPointSize; import edu.stanford.CVC4.FloatingPointToFPFloatingPoint; +import edu.stanford.CVC4.FloatingPointToFPIEEEBitVector; import edu.stanford.CVC4.FloatingPointToFPSignedBitVector; import edu.stanford.CVC4.FloatingPointToFPUnsignedBitVector; import edu.stanford.CVC4.FloatingPointToSBV; @@ -358,20 +358,10 @@ protected Expr isNegative(Expr pParam) { @Override protected Expr fromIeeeBitvectorImpl(Expr bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Expr signExtract = exprManager.mkConst(new BitVectorExtract(size - 1, size - 1)); - Expr exponentExtract = exprManager.mkConst(new BitVectorExtract(size - 2, mantissaSize)); - Expr mantissaExtract = exprManager.mkConst(new BitVectorExtract(mantissaSize - 1, 0)); - - Expr sign = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, signExtract, bitvector); - Expr exponent = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, exponentExtract, bitvector); - Expr mantissa = exprManager.mkExpr(Kind.BITVECTOR_EXTRACT, mantissaExtract, bitvector); - - return exprManager.mkExpr(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); + // This is just named weird, but the CVC4 doc say this is IEEE BV -> FP + FloatingPointConvertSort fpConvertSort = new FloatingPointConvertSort(getFPSize(pTargetType)); + Expr op = exprManager.mkConst(new FloatingPointToFPIEEEBitVector(fpConvertSort)); + return exprManager.mkExpr(op, bitvector); } @Override diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java index 883a8a1f8a..34b895cec6 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java @@ -408,29 +408,20 @@ protected Term isNegative(Term pParam) { } @Override - protected Term fromIeeeBitvectorImpl(Term bitvector, FloatingPointType pTargetType) { - int mantissaSize = pTargetType.getMantissaSize(); - int exponentSize = pTargetType.getExponentSize(); - int size = pTargetType.getTotalSize(); - assert size == mantissaSize + exponentSize + 1; - - Op signExtract; - Op exponentExtract; - Op mantissaExtract; + protected Term fromIeeeBitvectorImpl(Term pBitvector, FloatingPointType pTargetType) { try { - signExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 1, size - 1); - exponentExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, size - 2, mantissaSize); - mantissaExtract = termManager.mkOp(Kind.BITVECTOR_EXTRACT, mantissaSize - 1, 0); - } catch (CVC5ApiException e) { - throw new IllegalArgumentException( - "You tried creating a invalid bitvector extract in term " + bitvector + ".", e); + return termManager.mkTerm( + termManager.mkOp( + Kind.FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + pTargetType.getExponentSize(), + pTargetType.getMantissaSize() + 1), // add sign bit + pBitvector); + } catch (CVC5ApiException cvc5ApiException) { + // This seems to only be thrown for wrong exponent and mantissa sizes (e.g. negative + // numbers, size not equal to BV size etc.). We check for this beforehand, so this should + // not be thrown. + throw new IllegalArgumentException(cvc5ApiException); } - - Term sign = termManager.mkTerm(signExtract, bitvector); - Term exponent = termManager.mkTerm(exponentExtract, bitvector); - Term mantissa = termManager.mkTerm(mantissaExtract, bitvector); - - return termManager.mkTerm(Kind.FLOATINGPOINT_FP, sign, exponent, mantissa); } @Override diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 3dd541d780..b05abdad53 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -1098,6 +1098,27 @@ public void checkString2FpConversion64() throws SolverException, InterruptedExce fpmgr.makeNumber(Double.toString(pDouble), doublePrecType))); } + @Test + public void checkErrorOnInvalidSize_IeeeBv2FpConversion() { + BitvectorFormula bv = bvmgr.makeBitvector(9, 123); + + var exSingle = + assertThrows( + IllegalArgumentException.class, () -> fpmgr.fromIeeeBitvector(bv, singlePrecType)); + assertThat(exSingle.getMessage()) + .contains( + "The total size 32 of type FloatingPoint " + + "has to match the size 9 of type Bitvector<9>."); + + var exDouble = + assertThrows( + IllegalArgumentException.class, () -> fpmgr.fromIeeeBitvector(bv, doublePrecType)); + assertThat(exDouble.getMessage()) + .contains( + "The total size 64 of type FloatingPoint " + + "has to match the size 9 of type Bitvector<9>."); + } + @Test public void checkIeeeBv2FpConversion32() throws SolverException, InterruptedException { proveForAll(