diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java
index 3960684b..cb1009c8 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/DoubleInvocation.java
@@ -4,6 +4,7 @@
import de.uzl.its.swat.common.exceptions.SWATAssert;
import de.uzl.its.swat.common.exceptions.ValueConversionException;
import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.PlaceHolder;
import de.uzl.its.swat.symbolic.value.Value;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue;
@@ -12,6 +13,7 @@
import de.uzl.its.swat.symbolic.value.reference.ObjectValue;
import de.uzl.its.swat.symbolic.value.reference.lang.DoubleObjectValue;
import org.objectweb.asm.Type;
+import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
@@ -56,32 +58,7 @@ public class DoubleInvocation {
*/
private static IntValue compare(DoubleValue d1, DoubleValue d2) {
SolverContext ctx = d1.context;
- FloatingPointFormulaManager fpmgr = ctx.getFormulaManager().getFloatingPointFormulaManager();
- BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager();
- IntegerFormulaManager imgr = ctx.getFormulaManager().getIntegerFormulaManager();
-
- // Check for NaN cases first
- BooleanFormula d1IsNaN = fpmgr.isNaN(d1.formula);
- BooleanFormula d2IsNaN = fpmgr.isNaN(d2.formula);
-
- // Regular comparisons (when neither is NaN)
- BooleanFormula isEqual = fpmgr.equalWithFPSemantics(d1.formula, d2.formula);
- BooleanFormula isLess = fpmgr.lessThan(d1.formula, d2.formula);
-
- // Build the result:
- // - If both are NaN: return 0
- // - If only d1 is NaN: return 1 (NaN > anything)
- // - If only d2 is NaN: return -1 (anything < NaN)
- // - If equal: return 0
- // - If d1 < d2: return -1
- // - Otherwise: return 1
- NumeralFormula.IntegerFormula normalResult = bmgr.ifThenElse(isEqual, imgr.makeNumber(0),
- bmgr.ifThenElse(isLess, imgr.makeNumber(-1), imgr.makeNumber(1)));
-
- NumeralFormula.IntegerFormula result = bmgr.ifThenElse(bmgr.and(d1IsNaN, d2IsNaN), imgr.makeNumber(0),
- bmgr.ifThenElse(d1IsNaN, imgr.makeNumber(1),
- bmgr.ifThenElse(d2IsNaN, imgr.makeNumber(-1), normalResult)));
-
+ BitvectorFormula result = BitvectorEncoding.javaCompare(ctx.getFormulaManager(), d1.formula, d2.formula);
return new IntValue(ctx, Double.compare(d1.concrete, d2.concrete), result);
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java
index 28c72d6b..d35fc532 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/FloatInvocation.java
@@ -15,6 +15,7 @@
import de.uzl.its.swat.common.exceptions.SWATAssert;
import de.uzl.its.swat.common.exceptions.ValueConversionException;
import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.PlaceHolder;
import de.uzl.its.swat.symbolic.value.Value;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue;
@@ -75,32 +76,7 @@ public class FloatInvocation {
*/
private static IntValue compare(FloatValue f1, FloatValue f2) {
SolverContext ctx = f1.context;
- FloatingPointFormulaManager fpmgr = ctx.getFormulaManager().getFloatingPointFormulaManager();
- BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager();
- IntegerFormulaManager imgr = ctx.getFormulaManager().getIntegerFormulaManager();
-
- // Check for NaN cases first
- BooleanFormula f1IsNaN = fpmgr.isNaN(f1.formula);
- BooleanFormula f2IsNaN = fpmgr.isNaN(f2.formula);
-
- // Regular comparisons (when neither is NaN)
- BooleanFormula isEqual = fpmgr.equalWithFPSemantics(f1.formula, f2.formula);
- BooleanFormula isLess = fpmgr.lessThan(f1.formula, f2.formula);
-
- // Build the result using IntegerFormula (will be converted to bitvector by IntValue constructor):
- // - If both are NaN: return 0
- // - If only f1 is NaN: return 1 (NaN > anything)
- // - If only f2 is NaN: return -1 (anything < NaN)
- // - If equal: return 0
- // - If f1 < f2: return -1
- // - Otherwise: return 1
- NumeralFormula.IntegerFormula normalResult = bmgr.ifThenElse(isEqual, imgr.makeNumber(0),
- bmgr.ifThenElse(isLess, imgr.makeNumber(-1), imgr.makeNumber(1)));
-
- NumeralFormula.IntegerFormula result = bmgr.ifThenElse(bmgr.and(f1IsNaN, f2IsNaN), imgr.makeNumber(0),
- bmgr.ifThenElse(f1IsNaN, imgr.makeNumber(1),
- bmgr.ifThenElse(f2IsNaN, imgr.makeNumber(-1), normalResult)));
-
+ BitvectorFormula result = BitvectorEncoding.javaCompare(ctx.getFormulaManager(), f1.formula, f2.formula);
return new IntValue(ctx, Float.compare(f1.concrete, f2.concrete), result);
}
/**
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/BitvectorEncoding.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/BitvectorEncoding.java
new file mode 100644
index 00000000..f49831aa
--- /dev/null
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/BitvectorEncoding.java
@@ -0,0 +1,222 @@
+package de.uzl.its.swat.symbolic.value.primitive.numeric;
+
+import java.math.BigInteger;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import org.sosy_lab.java_smt.api.BitvectorFormula;
+import org.sosy_lab.java_smt.api.BitvectorFormulaManager;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.BooleanFormulaManager;
+import org.sosy_lab.java_smt.api.FloatingPointFormula;
+import org.sosy_lab.java_smt.api.FloatingPointFormulaManager;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.FunctionDeclaration;
+import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
+import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor;
+
+/**
+ * Converts Integer-sorted formulas to bit-vectors without mixing the two sorts where possible.
+ *
+ * {@link #toBitvector} returns a formula that is equal to {@code (_ int_to_bv width) f} in every
+ * model, but built over bit-vectors where {@code f} allows it:
+ *
+ *
+ * - numerals become bit-vector constants (modulo 2^width),
+ *
- {@code ite}, {@code +}, {@code -}, {@code *} and unary minus are rebuilt over bit-vectors
+ * ({@code int_to_bv} is a ring homomorphism modulo 2^width),
+ *
- {@code bv2int} (signed or unsigned) of a bit-vector is replaced by that bit-vector,
+ * extracted or extended to the width.
+ *
+ *
+ * Anything else (string lengths, {@code str.to_code}, division, ...) keeps its {@code int_to_bv}.
+ *
+ * Z3 handles {@code int_to_bv} badly: a query over {@code int_to_bv(ite(fp.lt x c, 1, -1))}
+ * (a DCMP result) may not return at all, while the same query over bit-vector constants is decided
+ * at once.
+ */
+public final class BitvectorEncoding {
+
+ /** Deeper Integer terms keep their int_to_bv rather than risk a deep recursion. */
+ private static final int MAX_DEPTH = 64;
+
+ private BitvectorEncoding() {}
+
+ /**
+ * Returns a bit-vector of the given width equal to {@code (_ int_to_bv width) f}.
+ *
+ * @param fmgr the formula manager
+ * @param f the Integer-sorted formula
+ * @param width the bit width of the result
+ * @return the bit-vector formula
+ */
+ public static BitvectorFormula toBitvector(FormulaManager fmgr, IntegerFormula f, int width) {
+ return new Lowering(fmgr, width).lower(f, 0);
+ }
+
+ /**
+ * Returns the three-way comparison result {@code eq ? 0 : (gt ? 1 : -1)} as a bit-vector of the
+ * given width, as LCMP/FCMP/DCMP and the compare methods produce it.
+ *
+ * @param fmgr the formula manager
+ * @param eq the equality condition
+ * @param gt the greater-than condition
+ * @param width the bit width
+ * @return the bit-vector formula
+ */
+ public static BitvectorFormula compareResult(
+ FormulaManager fmgr, BooleanFormula eq, BooleanFormula gt, int width) {
+ BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+ BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
+ return bmgr.ifThenElse(
+ eq,
+ bvmgr.makeBitvector(width, 0),
+ bmgr.ifThenElse(gt, bvmgr.makeBitvector(width, 1), bvmgr.makeBitvector(width, -1)));
+ }
+
+ /**
+ * Returns {@code Double.compare(a, b)} (or {@code Float.compare}) as a 32-bit bit-vector: NaN is
+ * equal to itself and greater than every other value, and -0.0 is less than 0.0.
+ *
+ * @param fmgr the formula manager
+ * @param a the first value
+ * @param b the second value
+ * @return the bit-vector formula, -1, 0 or 1
+ */
+ public static BitvectorFormula javaCompare(FormulaManager fmgr, FloatingPointFormula a, FloatingPointFormula b) {
+ BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager();
+ BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
+ FloatingPointFormulaManager fpmgr = fmgr.getFloatingPointFormulaManager();
+ BitvectorFormula minus = bvmgr.makeBitvector(32, -1);
+ BitvectorFormula zero = bvmgr.makeBitvector(32, 0);
+ BitvectorFormula one = bvmgr.makeBitvector(32, 1);
+ BooleanFormula aNaN = fpmgr.isNaN(a);
+ BooleanFormula bNaN = fpmgr.isNaN(b);
+ BooleanFormula aNeg = fpmgr.isNegative(a);
+ BooleanFormula bNeg = fpmgr.isNegative(b);
+ // Equal in FP terms but not as bits: -0.0 and 0.0
+ BitvectorFormula equal = bmgr.ifThenElse(
+ bmgr.and(aNeg, bmgr.not(bNeg)),
+ minus,
+ bmgr.ifThenElse(bmgr.and(bNeg, bmgr.not(aNeg)), one, zero));
+ BitvectorFormula ordered = bmgr.ifThenElse(
+ fpmgr.lessThan(a, b), minus, bmgr.ifThenElse(fpmgr.greaterThan(a, b), one, equal));
+ return bmgr.ifThenElse(
+ aNaN,
+ bmgr.ifThenElse(bNaN, zero, one),
+ bmgr.ifThenElse(bNaN, minus, ordered));
+ }
+
+ private static final class Lowering {
+ private final FormulaManager fmgr;
+ private final BitvectorFormulaManager bvmgr;
+ private final BooleanFormulaManager bmgr;
+ private final int width;
+ private final BigInteger modulus;
+ private final Map done = new HashMap<>();
+
+ Lowering(FormulaManager fmgr, int width) {
+ this.fmgr = fmgr;
+ this.bvmgr = fmgr.getBitvectorFormulaManager();
+ this.bmgr = fmgr.getBooleanFormulaManager();
+ this.width = width;
+ this.modulus = BigInteger.ONE.shiftLeft(width);
+ }
+
+ BitvectorFormula lower(IntegerFormula f, int depth) {
+ BitvectorFormula known = done.get(f);
+ if (known != null) {
+ return known;
+ }
+ BitvectorFormula result =
+ depth > MAX_DEPTH ? bvmgr.makeBitvector(width, f) : fmgr.visit(f, visitor(f, depth));
+ done.put(f, result);
+ return result;
+ }
+
+ private DefaultFormulaVisitor visitor(IntegerFormula f, int depth) {
+ return new DefaultFormulaVisitor<>() {
+ @Override
+ protected BitvectorFormula visitDefault(Formula formula) {
+ return bvmgr.makeBitvector(width, f);
+ }
+
+ @Override
+ public BitvectorFormula visitConstant(Formula formula, Object value) {
+ if (value instanceof BigInteger v) {
+ return bvmgr.makeBitvector(width, v.mod(modulus));
+ }
+ return visitDefault(formula);
+ }
+
+ @Override
+ public BitvectorFormula visitFunction(
+ Formula formula, List args, FunctionDeclaration decl) {
+ switch (decl.getKind()) {
+ case ITE:
+ if (args.size() == 3
+ && args.get(0) instanceof BooleanFormula cond
+ && args.get(1) instanceof IntegerFormula a
+ && args.get(2) instanceof IntegerFormula b) {
+ return bmgr.ifThenElse(cond, lower(a, depth + 1), lower(b, depth + 1));
+ }
+ break;
+ case ADD:
+ case SUB:
+ case MUL:
+ if (args.size() >= 2 && allInteger(args)) {
+ BitvectorFormula acc = lower((IntegerFormula) args.get(0), depth + 1);
+ for (Formula arg : args.subList(1, args.size())) {
+ BitvectorFormula next = lower((IntegerFormula) arg, depth + 1);
+ acc = switch (decl.getKind()) {
+ case ADD -> bvmgr.add(acc, next);
+ case SUB -> bvmgr.subtract(acc, next);
+ default -> bvmgr.multiply(acc, next);
+ };
+ }
+ return acc;
+ }
+ break;
+ case UMINUS:
+ if (args.size() == 1 && args.get(0) instanceof IntegerFormula a) {
+ return bvmgr.negate(lower(a, depth + 1));
+ }
+ break;
+ case UBV_TO_INT:
+ case SBV_TO_INT:
+ if (args.size() == 1 && args.get(0) instanceof BitvectorFormula bv) {
+ return resize(bv, decl.getKind() == FunctionDeclarationKind.SBV_TO_INT);
+ }
+ break;
+ default:
+ break;
+ }
+ return visitDefault(formula);
+ }
+ };
+ }
+
+ /** int_to_bv(bv2int(bv)) at this width: bv itself, its low bits, or bv extended. */
+ private BitvectorFormula resize(BitvectorFormula bv, boolean signed) {
+ int length = bvmgr.getLength(bv);
+ if (length == width) {
+ return bv;
+ }
+ if (length > width) {
+ return bvmgr.extract(bv, width - 1, 0);
+ }
+ return bvmgr.extend(bv, width - length, signed);
+ }
+
+ private static boolean allInteger(List args) {
+ for (Formula arg : args) {
+ if (!(arg instanceof IntegerFormula)) {
+ return false;
+ }
+ }
+ return true;
+ }
+ }
+}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/NumericalValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/NumericalValue.java
index 8de636d7..ba5e0ed8 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/NumericalValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/NumericalValue.java
@@ -130,7 +130,7 @@ protected FloatingPointFormula intToFpFormula(
BitvectorFormulaManager bvmgr = context.getFormulaManager().getBitvectorFormulaManager();
// Step 1: Convert integer to signed bitvector
- BitvectorFormula bv = bvmgr.makeBitvector(sourceBitWidth, intFormula);
+ BitvectorFormula bv = BitvectorEncoding.toBitvector(context.getFormulaManager(), intFormula, sourceBitWidth);
// Step 2: Cast bitvector to floating-point using RNE rounding (Java's default)
FloatingPointFormula fpFormula = fpmgr.castFrom(
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java
index 0bacd823..7ae669fe 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/DoubleValue.java
@@ -12,6 +12,7 @@
import org.sosy_lab.java_smt.api.NumeralFormula;
import org.sosy_lab.java_smt.api.SolverContext;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.ByteValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue;
@@ -236,7 +237,6 @@ private IntValue DCMP(DoubleValue f, int nanResult) {
}
BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager();
- IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager();
FloatingPointFormulaManager fmgr = context.getFormulaManager().getFloatingPointFormulaManager();
BooleanFormula isNaN1 = fmgr.isNaN(formula);
@@ -246,18 +246,12 @@ private IntValue DCMP(DoubleValue f, int nanResult) {
BooleanFormula gtCond = fmgr.greaterThan(formula, f.formula);
BooleanFormula eqCond = fmgr.equalWithFPSemantics(formula, f.formula);
- NumeralFormula.IntegerFormula res = bmgr.ifThenElse(
+ // Built over bit-vectors: Z3 decides int_to_bv over FP comparisons badly.
+ BitvectorFormulaManager bvmgr = context.getFormulaManager().getBitvectorFormulaManager();
+ BitvectorFormula res = bmgr.ifThenElse(
isNaN,
- imgr.makeNumber(nanResult),
- bmgr.ifThenElse(
- gtCond,
- imgr.makeNumber(1),
- bmgr.ifThenElse(
- eqCond,
- imgr.makeNumber(0),
- imgr.makeNumber(-1)
- )
- )
+ bvmgr.makeBitvector(32, nanResult),
+ BitvectorEncoding.compareResult(context.getFormulaManager(), eqCond, gtCond, 32)
);
return new IntValue(context, c, res);
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java
index 2f14df0e..b113f7c0 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/floatingpoint/FloatValue.java
@@ -12,6 +12,7 @@
import org.sosy_lab.java_smt.api.NumeralFormula;
import org.sosy_lab.java_smt.api.SolverContext;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.ByteValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.CharValue;
@@ -276,49 +277,56 @@ public LongValue F2L() {
/**
* Compares two floats and returns: 0 if both values are equal; 1 if this float is greater or
- * either float is NaN; -1 if the parameter is greater ToDo (Nils): This method is not validated
+ * either float is NaN; -1 if the parameter is greater
*
* @param f The other FloatValue
* @return The resulting IntValue with the boolean conditions
*/
public IntValue FCMPG(FloatValue f) {
- if (concrete.isNaN() || f.concrete.isNaN()) {
- return new IntValue(context, 1);
- }
- return FCMP(f);
+ return FCMP(f, 1);
}
/**
* Compares two floats and returns: 0 if both values are equal 1 if this float is greater -1 if
- * the parameter is greater or either float is NaN ToDo (Nils): This method is not validated
+ * the parameter is greater or either float is NaN
*
* @param f The other FloatValue
* @return The resulting IntValue with the boolean conditions
*/
public IntValue FCMPL(FloatValue f) {
- if (concrete.isNaN() || f.concrete.isNaN()) {
- return new IntValue(context, -1);
- }
- return FCMP(f);
+ return FCMP(f, -1);
}
/**
- * Compares two floats and returns: 0 if both values are equal 1 if this float is greater -1 if
- * the parameter is greater
+ * Compares two floats as FCMPG/FCMPL do: 0 if both values are equal (also -0.0 and 0.0), 1 if
+ * this float is greater, -1 if the parameter is greater, and nanResult if either is NaN
*
* @param f The other FloatValue
+ * @param nanResult The result if either float is NaN
* @return The resulting IntValue with the boolean conditions
*/
- private IntValue FCMP(FloatValue f) {
- int c = concrete.compareTo(f.concrete);
+ private IntValue FCMP(FloatValue f, int nanResult) {
+ int c;
+ if (Float.isNaN(concrete) || Float.isNaN(f.concrete)) {
+ c = nanResult;
+ } else if (concrete > f.concrete) {
+ c = 1;
+ } else if (concrete.floatValue() == f.concrete.floatValue()) {
+ // Explicit unboxing: 'concrete' is a boxed Float, so '==' would compare references
+ c = 0;
+ } else {
+ c = -1;
+ }
BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager();
- IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager();
+ BooleanFormula isNaN = bmgr.or(fmgr.isNaN(formula), fmgr.isNaN(f.formula));
BooleanFormula eqCond = fmgr.equalWithFPSemantics(formula, f.formula);
BooleanFormula gtCond = fmgr.greaterThan(formula, f.formula);
- NumeralFormula.IntegerFormula tmp =
- bmgr.ifThenElse(gtCond, imgr.makeNumber(1), imgr.makeNumber(-1));
- NumeralFormula.IntegerFormula res = bmgr.ifThenElse(eqCond, imgr.makeNumber(0), tmp);
+ // Built over bit-vectors: Z3 decides int_to_bv over FP comparisons badly.
+ BitvectorFormula res = bmgr.ifThenElse(
+ isNaN,
+ context.getFormulaManager().getBitvectorFormulaManager().makeBitvector(32, nanResult),
+ BitvectorEncoding.compareResult(context.getFormulaManager(), eqCond, gtCond, 32));
return new IntValue(context, c, res);
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/BooleanValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/BooleanValue.java
index 16a21333..2bfaf99f 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/BooleanValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/BooleanValue.java
@@ -114,11 +114,11 @@ public BooleanFormula getBounds(boolean upper) {
@Override
public IntValue asIntValue() {
- imgr = context.getFormulaManager().getIntegerFormulaManager();
+ BitvectorFormulaManager bvmgr = context.getFormulaManager().getBitvectorFormulaManager();
return new IntValue(
context,
concrete ? 1 : 0,
- bmgr.ifThenElse(formula, imgr.makeNumber(1), imgr.makeNumber(0)));
+ bmgr.ifThenElse(formula, bvmgr.makeBitvector(32, 1), bvmgr.makeBitvector(32, 0)));
}
@Override
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ByteValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ByteValue.java
index c3db10b1..c7c902f5 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ByteValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ByteValue.java
@@ -1,5 +1,6 @@
package de.uzl.its.swat.symbolic.value.primitive.numeric.integral;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue;
@@ -67,8 +68,8 @@ public ByteValue(SolverContext context, byte concrete, NumeralFormula.IntegerFor
this.bvmgr = context.getFormulaManager().getBitvectorFormulaManager();
this.imgr = context.getFormulaManager().getIntegerFormulaManager();
this.concrete = concrete;
- // Convert IntegerFormula to BitvectorFormula
- this.formula = bvmgr.makeBitvector(BIT_WIDTH, intFormula);
+ // Convert IntegerFormula to BitvectorFormula, over bit-vectors where it allows
+ this.formula = BitvectorEncoding.toBitvector(context.getFormulaManager(), intFormula, BIT_WIDTH);
}
/**
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/CharValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/CharValue.java
index a5219b5f..d06cd5ff 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/CharValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/CharValue.java
@@ -1,5 +1,6 @@
package de.uzl.its.swat.symbolic.value.primitive.numeric.integral;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue;
@@ -83,8 +84,8 @@ public CharValue(SolverContext context, char concrete, NumeralFormula.IntegerFor
this.bvmgr = context.getFormulaManager().getBitvectorFormulaManager();
this.imgr = context.getFormulaManager().getIntegerFormulaManager();
this.concrete = concrete;
- // Convert IntegerFormula to BitvectorFormula
- this.formula = bvmgr.makeBitvector(BIT_WIDTH, intFormula);
+ // Convert IntegerFormula to BitvectorFormula, over bit-vectors where it allows
+ this.formula = BitvectorEncoding.toBitvector(context.getFormulaManager(), intFormula, BIT_WIDTH);
}
/**
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/IntValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/IntValue.java
index 632e32c0..39e50db6 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/IntValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/IntValue.java
@@ -1,6 +1,7 @@
package de.uzl.its.swat.symbolic.value.primitive.numeric.integral;
import de.uzl.its.swat.common.exceptions.SWATAssert;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue;
@@ -65,8 +66,8 @@ public IntValue(SolverContext context, int concrete, NumeralFormula.IntegerFormu
this.bvmgr = context.getFormulaManager().getBitvectorFormulaManager();
this.imgr = context.getFormulaManager().getIntegerFormulaManager();
this.concrete = concrete;
- // Convert IntegerFormula to BitvectorFormula
- this.formula = bvmgr.makeBitvector(BIT_WIDTH, intFormula);
+ // Convert IntegerFormula to BitvectorFormula, over bit-vectors where it allows
+ this.formula = BitvectorEncoding.toBitvector(context.getFormulaManager(), intFormula, BIT_WIDTH);
}
/**
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java
index 36c157ef..011e0784 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/LongValue.java
@@ -1,5 +1,6 @@
package de.uzl.its.swat.symbolic.value.primitive.numeric.integral;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue;
@@ -268,16 +269,11 @@ public LongValue LXOR(LongValue l) {
public IntValue LCMP(LongValue l) {
int c = concrete.compareTo(l.concrete);
- BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager();
- IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager();
-
// Use signed comparison for bitvectors
BooleanFormula eqCond = bvmgr.equal(formula, l.formula);
BooleanFormula gtCond = bvmgr.greaterThan(formula, l.formula, true); // true = signed
- NumeralFormula.IntegerFormula tmp =
- bmgr.ifThenElse(gtCond, imgr.makeNumber(1), imgr.makeNumber(-1));
- NumeralFormula.IntegerFormula res = bmgr.ifThenElse(eqCond, imgr.makeNumber(0), tmp);
+ BitvectorFormula res = BitvectorEncoding.compareResult(context.getFormulaManager(), eqCond, gtCond, 32);
return new IntValue(context, c, res);
}
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java
index 16645268..34cdf015 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/integral/ShortValue.java
@@ -1,5 +1,6 @@
package de.uzl.its.swat.symbolic.value.primitive.numeric.integral;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue;
import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue;
@@ -69,8 +70,8 @@ public ShortValue(SolverContext context, short concrete, NumeralFormula.IntegerF
this.bvmgr = context.getFormulaManager().getBitvectorFormulaManager();
this.imgr = context.getFormulaManager().getIntegerFormulaManager();
this.concrete = concrete;
- // Convert IntegerFormula to BitvectorFormula
- this.formula = bvmgr.makeBitvector(BIT_WIDTH, intFormula);
+ // Convert IntegerFormula to BitvectorFormula, over bit-vectors where it allows
+ this.formula = BitvectorEncoding.toBitvector(context.getFormulaManager(), intFormula, BIT_WIDTH);
}
/**
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/DoubleObjectValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/DoubleObjectValue.java
index afd1e0a1..b849dffc 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/DoubleObjectValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/DoubleObjectValue.java
@@ -5,6 +5,7 @@
import de.uzl.its.swat.common.exceptions.NotImplementedException;
import de.uzl.its.swat.common.exceptions.SWATAssert;
import de.uzl.its.swat.common.exceptions.ValueConversionException;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.PlaceHolder;
import de.uzl.its.swat.symbolic.value.Value;
import de.uzl.its.swat.symbolic.value.VoidValue;
@@ -267,18 +268,9 @@ public BooleanFormula getBounds(boolean upper) {
DoubleObjectValue other = args[0].asDoubleObjectValue();
int result = val.concrete.compareTo(other.val.concrete);
- // Use floating point formula managers for proper symbolic handling
- BooleanFormula equal = fpfm.equalWithFPSemantics(val.formula, other.val.formula);
- BooleanFormula greater = fpfm.greaterThan(val.formula, other.val.formula);
-
- // Create the symbolic result using if-then-else logic
- var imgr = context.getFormulaManager().getIntegerFormulaManager();
- var symbolicResult = context.getFormulaManager().getBooleanFormulaManager().ifThenElse(equal,
- imgr.makeNumber(0),
- context.getFormulaManager().getBooleanFormulaManager().ifThenElse(greater,
- imgr.makeNumber(1),
- imgr.makeNumber(-1)));
-
+ // Double.compareTo semantics: NaN is greater than everything, -0.0 is less than 0.0
+ var symbolicResult = BitvectorEncoding.javaCompare(context.getFormulaManager(), val.formula, other.val.formula);
+
return new IntValue(context, result, symbolicResult);
} else {
return PlaceHolder.instance;
diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/FloatObjectValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/FloatObjectValue.java
index 8df3ffde..98b92dfa 100644
--- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/FloatObjectValue.java
+++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/FloatObjectValue.java
@@ -11,6 +11,7 @@
import de.uzl.its.swat.common.exceptions.NotImplementedException;
import de.uzl.its.swat.common.exceptions.SWATAssert;
import de.uzl.its.swat.common.exceptions.ValueConversionException;
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding;
import de.uzl.its.swat.symbolic.value.PlaceHolder;
import de.uzl.its.swat.symbolic.value.Value;
import de.uzl.its.swat.symbolic.value.VoidValue;
@@ -264,18 +265,9 @@ public String MAKE_SYMBOLIC() throws NullPointerException {
FloatObjectValue other = args[0].asFloatObjectValue();
int result = val.concrete.compareTo(other.val.concrete);
- // Use floating point formula managers for proper symbolic handling
- BooleanFormula equal = fpfm.equalWithFPSemantics(val.formula, other.val.formula);
- BooleanFormula greater = fpfm.greaterThan(val.formula, other.val.formula);
-
- // Create the symbolic result using if-then-else logic
- var imgr = context.getFormulaManager().getIntegerFormulaManager();
- var symbolicResult = context.getFormulaManager().getBooleanFormulaManager().ifThenElse(equal,
- imgr.makeNumber(0),
- context.getFormulaManager().getBooleanFormulaManager().ifThenElse(greater,
- imgr.makeNumber(1),
- imgr.makeNumber(-1)));
-
+ // Float.compareTo semantics: NaN is greater than everything, -0.0 is less than 0.0
+ var symbolicResult = BitvectorEncoding.javaCompare(context.getFormulaManager(), val.formula, other.val.formula);
+
return new IntValue(context, result, symbolicResult);
} else {
return PlaceHolder.instance;
diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/BitvectorEncodingTest.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/BitvectorEncodingTest.groovy
new file mode 100644
index 00000000..825f3b13
--- /dev/null
+++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/BitvectorEncodingTest.groovy
@@ -0,0 +1,245 @@
+package de.uzl.its.value.primitive.numeric
+
+import de.uzl.its.swat.symbolic.value.primitive.numeric.BitvectorEncoding
+import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue
+import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue
+import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.BooleanValue
+import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue
+import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.LongValue
+import org.sosy_lab.common.ShutdownManager
+import org.sosy_lab.common.configuration.Configuration
+import org.sosy_lab.common.log.BasicLogManager
+import org.sosy_lab.java_smt.SolverContextFactory
+import org.sosy_lab.java_smt.api.BitvectorFormula
+import org.sosy_lab.java_smt.api.BooleanFormula
+import org.sosy_lab.java_smt.api.FormulaType
+import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula
+import org.sosy_lab.java_smt.api.SolverContext
+import spock.lang.Specification
+
+/**
+ * BitvectorEncoding.toBitvector must equal int_to_bv in every model, and must not use int_to_bv
+ * where the Integer formula is built from numerals, ite, ring operations and bv2int.
+ */
+class BitvectorEncodingTest extends Specification {
+
+ SolverContext context
+ def fmgr, bmgr, bvmgr, imgr, fpmgr, smgr
+
+ def setup() {
+ context = SolverContextFactory.createSolverContext(
+ Configuration.defaultConfiguration(),
+ BasicLogManager.create(Configuration.defaultConfiguration()),
+ ShutdownManager.create().getNotifier(),
+ SolverContextFactory.Solvers.Z3)
+ fmgr = context.getFormulaManager()
+ bmgr = fmgr.getBooleanFormulaManager()
+ bvmgr = fmgr.getBitvectorFormulaManager()
+ imgr = fmgr.getIntegerFormulaManager()
+ fpmgr = fmgr.getFloatingPointFormulaManager()
+ smgr = fmgr.getStringFormulaManager()
+ }
+
+ def cleanup() {
+ context.close()
+ }
+
+ /**
+ * Whether a and b are equal under many concrete assignments of their variables. (Proving it for
+ * all models is the kind of int_to_bv query Z3 does not return on.)
+ */
+ boolean equivalent(BitvectorFormula a, BitvectorFormula b) {
+ def vars = new LinkedHashMap(fmgr.extractVariables(a))
+ vars.putAll(fmgr.extractVariables(b))
+ def random = new Random(42)
+ def doubles = [0.0d, -0.0d, 1.0d, 2.0d, -1.5d, 1e300d, Double.NaN, Double.POSITIVE_INFINITY, Double.NEGATIVE_INFINITY]
+ for (int round = 0; round < 40; round++) {
+ def prover = context.newProverEnvironment()
+ try {
+ vars.each { String n, def v ->
+ def type = fmgr.getFormulaType(v)
+ if (type.isBitvectorType()) {
+ int w = type.getSize()
+ def value = round < 4 ? [0G, 1G, (1G << w) - 1G, 1G << (w - 1)][round] : new BigInteger(w, random)
+ prover.addConstraint(bvmgr.equal(v, bvmgr.makeBitvector(w, value)))
+ } else if (type.isFloatingPointType()) {
+ double d = round < doubles.size() ? doubles[round] : random.nextGaussian() * 4
+ prover.addConstraint(fpmgr.assignment(v, fpmgr.makeNumber(d, type)))
+ } else if (type.isStringType()) {
+ def str = (0.. ws.collect { w -> [n, w] } }
+ }
+
+ def "keeps int_to_bv for #name, still equal"() {
+ when:
+ def f = build(name)
+ def lowered = BitvectorEncoding.toBitvector(fmgr, f, 32)
+
+ then:
+ equivalent(lowered, bvmgr.makeBitvector(32, f))
+
+ where:
+ name << ["a string length", "a division", "a length minus one"]
+ }
+
+ def "DCMP, FCMP and LCMP results are bit-vectors and match the Integer encoding (#kind)"() {
+ given:
+ def oldEncoding = { BooleanFormula isNaN, int nanResult, BooleanFormula gt, BooleanFormula eq ->
+ def ite = bmgr.ifThenElse(eq, num(0), bmgr.ifThenElse(gt, num(1), num(-1)))
+ bvmgr.makeBitvector(32, isNaN == null ? ite : bmgr.ifThenElse(isNaN, num(nanResult), ite))
+ }
+
+ when:
+ IntValue result
+ BitvectorFormula expected
+ switch (kind) {
+ case "DCMPL":
+ case "DCMPG":
+ def a = new DoubleValue(context, 1.0d); a.MAKE_SYMBOLIC("0")
+ def b = new DoubleValue(context, 2.0d); b.MAKE_SYMBOLIC("1")
+ result = kind == "DCMPL" ? a.DCMPL(b) : a.DCMPG(b)
+ expected = oldEncoding(bmgr.or(fpmgr.isNaN(a.formula), fpmgr.isNaN(b.formula)),
+ kind == "DCMPL" ? -1 : 1,
+ fpmgr.greaterThan(a.formula, b.formula), fpmgr.equalWithFPSemantics(a.formula, b.formula))
+ break
+ case "FCMPL":
+ def a = new FloatValue(context, 1.0f); a.MAKE_SYMBOLIC("0")
+ def b = new FloatValue(context, 2.0f); b.MAKE_SYMBOLIC("1")
+ result = a.FCMPL(b)
+ expected = oldEncoding(null, 0,
+ fpmgr.greaterThan(a.formula, b.formula), fpmgr.equalWithFPSemantics(a.formula, b.formula))
+ break
+ default:
+ def a = new LongValue(context, 1L); a.MAKE_SYMBOLIC("0")
+ def b = new LongValue(context, 2L); b.MAKE_SYMBOLIC("1")
+ result = a.LCMP(b)
+ expected = oldEncoding(null, 0,
+ bvmgr.greaterThan(a.formula, b.formula, true), bvmgr.equal(a.formula, b.formula))
+ }
+
+ then:
+ result.concrete == -1
+ !mixesSorts(result.formula)
+ equivalent(result.formula, expected)
+
+ where:
+ kind << ["DCMPL", "DCMPG", "FCMPL", "LCMP"]
+ }
+
+ def "boolean to int is a bit-vector ite"() {
+ given:
+ def b = new BooleanValue(context, true)
+ b.MAKE_SYMBOLIC("0")
+
+ when:
+ def i = b.asIntValue()
+
+ then:
+ i.concrete == 1
+ !mixesSorts(i.formula)
+ equivalent(i.formula, bvmgr.makeBitvector(32, bmgr.ifThenElse(b.formula, num(1), num(0))))
+ }
+
+ def "javaCompare matches Double.compare and Float.compare"() {
+ given:
+ def values = [Double.NaN, Double.NEGATIVE_INFINITY, -1.5d, -0.0d, 0.0d, Double.MIN_VALUE, 2.0d, Double.POSITIVE_INFINITY]
+
+ expect:
+ [FormulaType.getDoublePrecisionFloatingPointType(), FormulaType.getSinglePrecisionFloatingPointType()].each { type ->
+ def a = fpmgr.makeVariable("a", type)
+ def b = fpmgr.makeVariable("b", type)
+ def cmp = BitvectorEncoding.javaCompare(fmgr, a, b)
+ for (double x : values) {
+ for (double y : values) {
+ int expected = type.getMantissaSize() == 52 ? Double.compare(x, y) : Float.compare((float) x, (float) y)
+ def prover = context.newProverEnvironment()
+ prover.addConstraint(fpmgr.assignment(a, fpmgr.makeNumber(x, type)))
+ prover.addConstraint(fpmgr.assignment(b, fpmgr.makeNumber(y, type)))
+ prover.addConstraint(bmgr.not(bvmgr.equal(cmp, bvmgr.makeBitvector(32, expected))))
+ assert prover.isUnsat(): "compare($x, $y) should be $expected"
+ prover.close()
+ }
+ }
+ }
+ }
+}
diff --git a/symbolic-explorer/solver/Int2BvLifting.py b/symbolic-explorer/solver/Int2BvLifting.py
new file mode 100644
index 00000000..ba2a51b5
--- /dev/null
+++ b/symbolic-explorer/solver/Int2BvLifting.py
@@ -0,0 +1,330 @@
+"""
+Rewrites bit-vector comparisons over int_to_bv of bounded Integer terms into Integer comparisons.
+
+The executor encodes Java ints, chars, ... as bit-vectors, and String lengths, indices and char
+codes come from the string theory as Integers, so a query such as `s.length() > 2` reads
+`(bvsgt ((_ int_to_bv 32) (str.len s)) (_ bv2 32))`. Z3 decides such mixed queries badly: trivially
+satisfiable ones with a few chars and lengths run for minutes. When the Integer term is known to lie
+in the range of the bit-vector, int_to_bv is a bijection there and the comparison can be made over
+the Integers instead, where Z3 is fast.
+
+`lift(e, signed)` finds an Integer term t with e == int_to_bv(t) whose value lies in the signed
+(or unsigned) range of e's width, built from:
+- bit-vector numerals,
+- int_to_bv of an Integer term with a known range (numerals, str.len, str.indexof, str.to_code,
+ ubv_to_int, + - * and ite of those),
+- bvadd/bvsub/bvneg/bvmul/ite of liftable terms, as long as the range still fits,
+- zero/sign extension of liftable terms.
+A char code (str.to_code, in [-1, max char]) does not fit 16 bits; it is lifted as
+ite(t < 0, t + 2^16, ite(t < 2^16, t, t mod 2^16)), which is exact.
+
+`rewrite(e)` replaces every comparison (=, distinct, bvs*, bvu*) between two liftable bit-vectors that
+involves int_to_bv by the Integer comparison of their lifts, and ubv_to_int of a liftable term by its
+lift. Everything else is left as it is.
+
+The ranges of str.len and str.indexof assume that every string has at most 2^31 - 1 chars, as Java
+strings do. `rewrite` records the strings whose length it relied on; `lift_query` adds the bound for
+each of them to the query, so that the rewritten query is equivalent to the original one under that
+bound in every model (and its models are models of the original query).
+"""
+
+import z3
+
+JAVA_MAX_STRING_LENGTH = 2 ** 31 - 1
+# Upper bound of str.to_code; Z3's char sort is never larger than Unicode.
+MAX_CHAR_CODE = 0x10FFFF
+
+_SIGNED_CMP = {z3.Z3_OP_SLEQ, z3.Z3_OP_SLT, z3.Z3_OP_SGEQ, z3.Z3_OP_SGT}
+_UNSIGNED_CMP = {z3.Z3_OP_ULEQ, z3.Z3_OP_ULT, z3.Z3_OP_UGEQ, z3.Z3_OP_UGT}
+_INT_CMP = {
+ z3.Z3_OP_SLEQ: lambda a, b: a <= b, z3.Z3_OP_ULEQ: lambda a, b: a <= b,
+ z3.Z3_OP_SLT: lambda a, b: a < b, z3.Z3_OP_ULT: lambda a, b: a < b,
+ z3.Z3_OP_SGEQ: lambda a, b: a >= b, z3.Z3_OP_UGEQ: lambda a, b: a >= b,
+ z3.Z3_OP_SGT: lambda a, b: a > b, z3.Z3_OP_UGT: lambda a, b: a > b,
+}
+
+
+def _kind(e):
+ return e.decl().kind() if z3.is_app(e) else None
+
+
+def _view_range(width, signed):
+ return (-(2 ** (width - 1)), 2 ** (width - 1) - 1) if signed else (0, 2 ** width - 1)
+
+
+class Int2BvLifting:
+ """Rewrites expressions of one Z3 context; caches results across queries.
+
+ The caches are keyed by AST id. Z3 reuses the id of an AST that has been freed, so every
+ expression that serves as a key is kept alive in self._alive.
+ """
+
+ def __init__(self):
+ self._alive = []
+ self._rewritten = {}
+ self._lifted = {}
+ self._ranges = {}
+ self._mentions_int2bv = {}
+ # Strings whose length bound a rewrite relied on, by expression id
+ self._bounded = {}
+ self._needs = {}
+
+ # Integer ranges
+
+ def int_range(self, t):
+ """(lo, hi) such that lo <= t <= hi in every model (under the string length bound), or None.
+ Records the strings whose length bound the range relies on in self._needs[t]."""
+ key = t.get_id()
+ if key in self._ranges:
+ return self._ranges[key]
+ self._alive.append(t)
+ r, needs = self._int_range(t)
+ self._ranges[key] = r
+ self._needs[key] = needs if r is not None else ()
+ return r
+
+ def _needs_of(self, *terms):
+ out = []
+ for t in terms:
+ out.extend(self._needs.get(t.get_id(), ()))
+ return tuple(out)
+
+ def _int_range(self, t):
+ v = _int_const(t)
+ if v is not None:
+ return (v, v), ()
+ k = _kind(t)
+ args = t.children() if z3.is_app(t) else []
+ if k == z3.Z3_OP_SEQ_LENGTH:
+ return (0, JAVA_MAX_STRING_LENGTH), (args[0],)
+ if k == z3.Z3_OP_SEQ_INDEX:
+ return (-1, JAVA_MAX_STRING_LENGTH), (args[0],)
+ if k == z3.Z3_OP_STR_TO_CODE:
+ return (-1, MAX_CHAR_CODE), ()
+ if k == z3.Z3_OP_BV2INT:
+ return (0, 2 ** args[0].size() - 1), ()
+ if k == z3.Z3_OP_SBV2INT:
+ return _view_range(args[0].size(), True), ()
+ if k in (z3.Z3_OP_ADD, z3.Z3_OP_SUB, z3.Z3_OP_MUL) and args:
+ ranges = [self.int_range(a) for a in args]
+ if any(r is None for r in ranges):
+ return None, ()
+ lo, hi = ranges[0]
+ for (l2, h2) in ranges[1:]:
+ if k == z3.Z3_OP_ADD:
+ lo, hi = lo + l2, hi + h2
+ elif k == z3.Z3_OP_SUB:
+ lo, hi = lo - h2, hi - l2
+ else:
+ products = [lo * l2, lo * h2, hi * l2, hi * h2]
+ lo, hi = min(products), max(products)
+ return (lo, hi), self._needs_of(*args)
+ if k == z3.Z3_OP_UMINUS:
+ r = self.int_range(args[0])
+ return (None, ()) if r is None else ((-r[1], -r[0]), self._needs_of(args[0]))
+ if k == z3.Z3_OP_ITE:
+ ra, rb = self.int_range(args[1]), self.int_range(args[2])
+ if ra is None or rb is None:
+ return None, ()
+ return (min(ra[0], rb[0]), max(ra[1], rb[1])), self._needs_of(args[1], args[2])
+ return None, ()
+
+ # Bit-vector lifting
+
+ def lift(self, e, signed):
+ """(t, needs): an Integer term with e == int_to_bv(t) and t in the signed/unsigned range of
+ e's width, and the strings whose length bound that relies on; or None."""
+ key = (e.get_id(), signed)
+ if key not in self._lifted:
+ self._alive.append(e)
+ self._lifted[key] = self._lift(e, signed)
+ return self._lifted[key]
+
+ def _lift(self, e, signed):
+ width = e.size()
+ lo_view, hi_view = _view_range(width, signed)
+ if z3.is_bv_value(e):
+ return (z3.IntVal(e.as_signed_long() if signed else e.as_long(), e.ctx), ())
+ k = _kind(e)
+ args = e.children() if z3.is_app(e) else []
+ if k == z3.Z3_OP_INT2BV:
+ t = self.rewrite(args[0])
+ r = self.int_range(args[0])
+ if r is None:
+ return None
+ needs = self._needs.get(args[0].get_id(), ()) + self.needs(args[0])
+ wrapped = _wrap(t, r, lo_view, hi_view, 2 ** width)
+ return None if wrapped is None else (wrapped, needs)
+ if k in (z3.Z3_OP_BADD, z3.Z3_OP_BSUB, z3.Z3_OP_BMUL) and args:
+ parts = [self._lift_ranged(a, signed) for a in args]
+ if any(p is None for p in parts):
+ return None
+ t, (lo, hi), needs = parts[0]
+ for (t2, (l2, h2), n2) in parts[1:]:
+ if k == z3.Z3_OP_BADD:
+ t, lo, hi = t + t2, lo + l2, hi + h2
+ elif k == z3.Z3_OP_BSUB:
+ t, lo, hi = t - t2, lo - h2, hi - l2
+ else:
+ products = [lo * l2, lo * h2, hi * l2, hi * h2]
+ t, lo, hi = t * t2, min(products), max(products)
+ needs = needs + n2
+ wrapped = _wrap(t, (lo, hi), lo_view, hi_view, 2 ** width)
+ return None if wrapped is None else (wrapped, needs)
+ if k == z3.Z3_OP_BNEG:
+ p = self._lift_ranged(args[0], signed)
+ if p is None:
+ return None
+ t, (lo, hi), needs = p
+ wrapped = _wrap(-t, (-hi, -lo), lo_view, hi_view, 2 ** width)
+ return None if wrapped is None else (wrapped, needs)
+ if k == z3.Z3_OP_ITE:
+ a, b = self.lift(args[1], signed), self.lift(args[2], signed)
+ if a is None or b is None:
+ return None
+ return z3.If(self.rewrite(args[0]), a[0], b[0]), a[1] + b[1] + self.needs(args[0])
+ if k in (z3.Z3_OP_ZERO_EXT, z3.Z3_OP_SIGN_EXT):
+ inner = self.lift(args[0], k == z3.Z3_OP_SIGN_EXT)
+ if inner is None:
+ return None
+ # The inner value fits the inner width's range, so it fits both views of the
+ # extended width, except a negative value in the unsigned view.
+ if not signed and k == z3.Z3_OP_SIGN_EXT:
+ return None
+ return inner
+ return None
+
+ def _lift_ranged(self, e, signed):
+ """(t, (lo, hi), needs) for a liftable e, with the range of its lift."""
+ lifted = self.lift(e, signed)
+ if lifted is None:
+ return None
+ t, needs = lifted
+ # The lift lies in the view's range by construction; its own range may be tighter.
+ lo, hi = _view_range(e.size(), signed)
+ r = self.int_range(t)
+ if r is not None:
+ lo, hi = max(lo, r[0]), min(hi, r[1])
+ needs = needs + self._needs.get(t.get_id(), ())
+ return t, (lo, hi), needs
+
+ # Rewriting
+
+ def mentions_int2bv(self, e):
+ key = e.get_id()
+ if key not in self._mentions_int2bv:
+ self._alive.append(e)
+ self._mentions_int2bv[key] = z3.is_app(e) and (
+ _kind(e) == z3.Z3_OP_INT2BV or any(self.mentions_int2bv(c) for c in e.children()))
+ return self._mentions_int2bv[key]
+
+ def rewrite(self, e):
+ """e with comparisons over int_to_bv of bounded terms made over the Integers."""
+ key = e.get_id()
+ if key in self._rewritten:
+ return self._rewritten[key]
+ self._alive.append(e)
+ result, needs = e, ()
+ if z3.is_app(e) and self.mentions_int2bv(e):
+ result, needs = self._rewrite_app(e)
+ self._rewritten[key] = result
+ self._bounded[key] = needs
+ return result
+
+ def needs(self, e):
+ """The strings whose length bound rewrite(e) relies on."""
+ self.rewrite(e)
+ return self._bounded[e.get_id()]
+
+ def _rewrite_app(self, e):
+ k = _kind(e)
+ args = e.children()
+ equality = k in (z3.Z3_OP_EQ, z3.Z3_OP_DISTINCT)
+ if len(args) == 2 and z3.is_bv(args[0]) and (equality or k in _SIGNED_CMP or k in _UNSIGNED_CMP):
+ views = [True, False] if equality else [k in _SIGNED_CMP]
+ for signed in views:
+ a, b = self.lift(args[0], signed), self.lift(args[1], signed)
+ if a is not None and b is not None:
+ if equality:
+ cmp = (lambda x, y: x == y) if k == z3.Z3_OP_EQ else (lambda x, y: x != y)
+ else:
+ cmp = _INT_CMP[k]
+ return cmp(a[0], b[0]), a[1] + b[1]
+ if k == z3.Z3_OP_BV2INT:
+ a = self.lift(args[0], False)
+ if a is not None:
+ return a
+ if k == z3.Z3_OP_SBV2INT:
+ a = self.lift(args[0], True)
+ if a is not None:
+ return a
+ if k == z3.Z3_OP_ITE:
+ x = _signed_bv2int_operand(e)
+ if x is not None:
+ a = self.lift(x, True)
+ if a is not None:
+ return a
+ children = [self.rewrite(c) for c in args]
+ needs = tuple(n for c in args for n in self._bounded[c.get_id()])
+ if all(c.eq(o) for c, o in zip(children, args)):
+ return e, needs
+ return e.decl()(*children), needs
+
+
+def _wrap(t, r, lo_view, hi_view, m):
+ """The value of int_to_bv(t) in the view [lo_view, hi_view] (of size m), for t in r = (lo, hi):
+ t itself where it lies in the view, else t shifted by m (or reduced modulo m, if the range is
+ wider than that), as an ite with only the cases r allows. None if t can lie below the view by
+ more than m."""
+ lo, hi = r
+ if lo < lo_view - m:
+ return None
+ result = t
+ if hi > hi_view:
+ high = t - m if hi <= hi_view + m else (t - lo_view) % m + lo_view
+ result = z3.If(t <= hi_view, t, high)
+ if lo < lo_view:
+ result = z3.If(t < lo_view, t + m, result)
+ return result
+
+
+def _int_const(e):
+ """The value of an Integer numeral, also when written as (- n); else None."""
+ if z3.is_int_value(e):
+ return e.as_long()
+ if _kind(e) == z3.Z3_OP_UMINUS and z3.is_int_value(e.arg(0)):
+ return -e.arg(0).as_long()
+ return None
+
+
+def _signed_bv2int_operand(e):
+ """x if e is the signed bv2int ite(bvsle(0, x), ubv_to_int(x), ubv_to_int(x) - 2^w) (in the
+ forms JavaSMT builds it), else None."""
+ cond, then, other = e.children()
+ if _kind(cond) != z3.Z3_OP_SLEQ or _kind(then) != z3.Z3_OP_BV2INT:
+ return None
+ zero, x = cond.children()
+ if not (z3.is_bv_value(zero) and zero.as_long() == 0 and then.arg(0).eq(x)):
+ return None
+ m = 2 ** x.size()
+ if _kind(other) == z3.Z3_OP_ADD and other.num_args() == 2:
+ a, b = other.children()
+ for u, c in ((a, b), (b, a)):
+ if u.eq(then) and _int_const(c) == -m:
+ return x
+ if _kind(other) == z3.Z3_OP_SUB and other.num_args() == 2:
+ a, b = other.children()
+ if a.eq(then) and _int_const(b) == m:
+ return x
+ return None
+
+
+def lift_query(lifting, exprs):
+ """The rewritten expressions, plus the length bounds of the strings they rely on."""
+ out = [lifting.rewrite(x) for x in exprs]
+ strings = {}
+ for x in exprs:
+ for s in lifting.needs(x):
+ strings[s.get_id()] = s
+ out.extend(z3.Length(s) <= JAVA_MAX_STRING_LENGTH for s in strings.values())
+ return out
diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py
index 8e781a72..3a32f171 100755
--- a/symbolic-explorer/solver/SolverHandler.py
+++ b/symbolic-explorer/solver/SolverHandler.py
@@ -379,6 +379,23 @@ def write_optimizer_to_file(optimizer: Optimize, output_dir: str = "smt_files")
return filepath
+ @staticmethod
+ def lift_int2bv(cache, assertions: list) -> list:
+ """The assertions with comparisons over int_to_bv of string lengths, indices and char codes
+ made over the Integers (see Int2BvLifting), which Z3 decides much faster. Equivalent for
+ Java strings (at most 2^31 - 1 chars); on any error, the assertions as they are."""
+ from solver.Int2BvLifting import Int2BvLifting, lift_query
+ try:
+ lifting = getattr(cache, 'int2bv_lifting', None)
+ if lifting is None:
+ lifting = cache.int2bv_lifting = Int2BvLifting()
+ if not any(lifting.mentions_int2bv(a) for a in assertions):
+ return assertions
+ return lift_query(lifting, assertions)
+ except Exception as e:
+ logger.warning(f"[SOLVER] int_to_bv lifting failed, solving the query as it is: {e}")
+ return assertions
+
@staticmethod
def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000, rlimit: int | None = None) -> Tuple[SATResult, Dict[str, Any]]:
"""
@@ -425,14 +442,10 @@ def solve(node: Any, path_constraints: list, timeout_ms: int | None = 60 * 1000,
# The FIRST set of expressions are from the node constraint - we need to NEGATE them
# (We're looking for a solution that takes a different path)
if len(node_exprs) > 0:
- # Negate all node constraint expressions and add them
- for expr in node_exprs:
- negated = Not(expr)
- solver.add(negated)
-
- # Add all path constraint expressions (already parsed and cached)
- for i, path_expr in enumerate(all_exprs[len(node_exprs):]):
- solver.add(path_expr)
+ # Negate all node constraint expressions, then add all path constraint expressions
+ # (already parsed and cached)
+ assertions = [Not(expr) for expr in node_exprs] + all_exprs[len(node_exprs):]
+ solver.add(*Z3Handler.lift_int2bv(cache, assertions))
# Building the solver is Z3 work (SMT-LIB parsing on cache misses, assertion
# construction), so it counts towards the SMT solver stage rather than the
diff --git a/symbolic-explorer/tests/test_int2bv_lifting.py b/symbolic-explorer/tests/test_int2bv_lifting.py
new file mode 100644
index 00000000..2b39618b
--- /dev/null
+++ b/symbolic-explorer/tests/test_int2bv_lifting.py
@@ -0,0 +1,165 @@
+"""
+Unit tests for solver/Int2BvLifting: comparisons over int_to_bv of bounded Integer terms are made over
+the Integers, with the same truth value under every assignment.
+
+Needs z3, so run it with the harness venv, from symbolic-explorer/:
+ ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_int2bv_lifting -v
+"""
+
+import os
+import random
+import sys
+import unittest
+
+import z3
+
+sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..'))
+
+from solver.Int2BvLifting import Int2BvLifting, lift_query, JAVA_MAX_STRING_LENGTH
+
+
+def mixes_sorts(e):
+ s = e.sexpr()
+ return 'int_to_bv' in s or 'ubv_to_int' in s or 'int2bv' in s or 'bv2int' in s
+
+
+class Terms:
+ """Random terms over a string s, an 8-bit x and a 32-bit y, as the executor builds them."""
+
+ def __init__(self, rnd):
+ self.rnd = rnd
+ self.s = z3.String('s')
+ self.x = z3.BitVec('x', 8)
+ self.y = z3.BitVec('y', 32)
+
+ def int_leaf(self):
+ r = self.rnd
+ return r.choice([
+ lambda: z3.Length(self.s),
+ lambda: z3.IndexOf(self.s, z3.StringVal('a'), z3.IntVal(r.randint(-1, 2))),
+ lambda: z3.StrToCode(z3.SubString(self.s, z3.IntVal(r.randint(-1, 2)), z3.IntVal(1))),
+ lambda: z3.BV2Int(self.x),
+ lambda: z3.BV2Int(self.y),
+ lambda: z3.IntVal(r.choice([0, 1, -1, 3, 65535, 65536, 2 ** 31 - 1, 2 ** 31, -2 ** 31, 2 ** 32 - 1])),
+ ])()
+
+ def int_term(self, depth):
+ r = self.rnd
+ if depth == 0 or r.random() < 0.3:
+ return self.int_leaf()
+ a, b = self.int_term(depth - 1), self.int_term(depth - 1)
+ return r.choice([
+ lambda: a + b,
+ lambda: a - b,
+ lambda: a * z3.IntVal(r.choice([-1, 2, 3])),
+ lambda: -a,
+ lambda: z3.If(self.bool_term(depth - 1), a, b),
+ ])()
+
+ def bv_term(self, width, depth):
+ r = self.rnd
+ if depth == 0 or r.random() < 0.25:
+ return r.choice([
+ lambda: z3.Int2BV(self.int_term(2), width),
+ lambda: z3.BitVecVal(r.randint(0, 2 ** width - 1), width),
+ lambda: z3.BitVecVal(2 ** width - 1, width),
+ ])()
+ a, b = self.bv_term(width, depth - 1), self.bv_term(width, depth - 1)
+ options = [
+ lambda: a + b,
+ lambda: a - b,
+ lambda: -a,
+ lambda: a * z3.BitVecVal(r.choice([2, 3, 2 ** width - 1]), width),
+ lambda: z3.If(self.bool_term(depth - 1), a, b),
+ ]
+ if width > 8:
+ narrow = 8 if width == 16 else 16
+ options.append(lambda: z3.ZeroExt(width - narrow, self.bv_term(narrow, depth - 1)))
+ options.append(lambda: z3.SignExt(width - narrow, self.bv_term(narrow, depth - 1)))
+ return r.choice(options)()
+
+ def bool_term(self, depth):
+ r = self.rnd
+ width = r.choice([8, 16, 32])
+ a, b = self.bv_term(width, max(depth - 1, 0)), self.bv_term(width, max(depth - 1, 0))
+ return r.choice([
+ lambda: a == b, lambda: a != b,
+ lambda: a <= b, lambda: a < b, lambda: a >= b, lambda: a > b,
+ lambda: z3.ULE(a, b), lambda: z3.ULT(a, b), lambda: z3.UGE(a, b), lambda: z3.UGT(a, b),
+ lambda: z3.BV2Int(a) == z3.IntVal(r.randint(0, 300)),
+ ])()
+
+ def assignment(self):
+ r = self.rnd
+ chars = ['a', 'b', 'ÿ', '', '\U0001F600']
+ s = ''.join(r.choice(chars) for _ in range(r.randint(0, 3)))
+ x = r.choice([0, 1, 127, 128, 255, r.randint(0, 255)])
+ y = r.choice([0, 1, 2 ** 31 - 1, 2 ** 31, 2 ** 32 - 1, r.randint(0, 2 ** 32 - 1)])
+ return [(self.s, z3.StringVal(s)), (self.x, z3.BitVecVal(x, 8)), (self.y, z3.BitVecVal(y, 32))]
+
+
+def evaluate(e, assignment):
+ v = z3.simplify(z3.substitute(e, *assignment))
+ if not (z3.is_true(v) or z3.is_false(v)):
+ raise AssertionError(f'{e} does not evaluate to a constant: {v}')
+ return z3.is_true(v)
+
+
+class LiftingTest(unittest.TestCase):
+
+ def test_random_comparisons_keep_their_truth_value(self):
+ rnd = random.Random(7)
+ terms = Terms(rnd)
+ lifted = 0
+ for _ in range(150):
+ e = terms.bool_term(3)
+ lifting = Int2BvLifting()
+ r = lifting.rewrite(e)
+ lifted += not r.eq(e)
+ for _ in range(12):
+ a = terms.assignment()
+ self.assertEqual(evaluate(e, a), evaluate(r, a), f'\n{e}\nrewritten to\n{r}\nunder {a}')
+ self.assertGreater(lifted, 50)
+
+ def test_string_length_comparisons_become_integer_comparisons(self):
+ s = z3.String('s')
+ length = z3.Int2BV(z3.Length(s), 32)
+ e = z3.And(z3.Not(length <= z3.BitVecVal(2, 32)),
+ z3.Int2BV(z3.StrToCode(z3.SubString(s, z3.IntVal(1), z3.IntVal(1))), 16) != z3.BitVecVal(38, 16))
+ out = lift_query(Int2BvLifting(), [e])
+ self.assertFalse(any(mixes_sorts(x) for x in out))
+ # The length bound the rewrite relies on is part of the query.
+ self.assertTrue(any(x.eq(z3.Length(s) <= JAVA_MAX_STRING_LENGTH) for x in out))
+ solver = z3.Solver()
+ solver.add(*out)
+ self.assertEqual(solver.check(), z3.sat)
+ self.assertTrue(z3.is_true(solver.model().eval(e, model_completion=True)))
+
+ def test_overflowing_length_arithmetic_wraps(self):
+ # s.length() + 3 overflows for long strings: the lift must keep the wrap.
+ s = z3.String('s')
+ e = z3.BitVecVal(0, 32) > z3.Int2BV(z3.Length(s) + 3, 32)
+ r = Int2BvLifting().rewrite(e)
+ self.assertFalse(mixes_sorts(r))
+ # (A model would need a string of 2^31 chars, so evaluate at given lengths instead.)
+ for n, holds in [(0, False), (2 ** 31 - 4, False), (2 ** 31 - 3, True), (2 ** 31 - 1, True)]:
+ v = z3.simplify(z3.substitute(r, (z3.Length(s), z3.IntVal(n))))
+ self.assertEqual(z3.is_true(v), holds, f'length {n}: {v}')
+
+ def test_signed_bv2int_of_a_length_is_the_length(self):
+ # JavaSMT's signed bv2int: ite(0 <= x, ubv_to_int(x), ubv_to_int(x) - 2^32)
+ s = z3.String('s')
+ x = z3.Int2BV(z3.Length(s), 32) + z3.BitVecVal(2 ** 32 - 1, 32)
+ signed = z3.If(z3.BitVecVal(0, 32) <= x, z3.BV2Int(x), z3.IntVal(-2 ** 32) + z3.BV2Int(x))
+ e = z3.SubString(s, signed, z3.IntVal(1)) == z3.StringVal('a')
+ out = lift_query(Int2BvLifting(), [e])
+ self.assertFalse(any(mixes_sorts(x) for x in out))
+
+ def test_terms_without_int2bv_are_left_alone(self):
+ y = z3.BitVec('y', 32)
+ e = z3.And(y + 1 > z3.BitVecVal(3, 32), z3.BV2Int(y) < 7)
+ self.assertTrue(Int2BvLifting().rewrite(e).eq(e))
+
+
+if __name__ == '__main__':
+ unittest.main()