From 22dce63f0287e63a06843a0a7e44dd037b73c317 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:59:50 +0000 Subject: [PATCH 1/3] Build comparison results and Integer-to-bit-vector conversions over bit-vectors DCMP/FCMP/LCMP and boolean-to-int built their -1/0/1 results as Integer ite terms wrapped in int_to_bv. Z3 does not return on queries that mix int_to_bv with FP comparisons (a two-branch DCMP query that is UNSAT in 0.0 s over bit-vector constants stays unknown after minutes). Build those results over bit-vectors directly, and route every Integer-to-bit-vector constructor (Int/Short/Byte/CharValue, int-to-FP casts) through BitvectorEncoding.toBitvector, which rebuilds numerals, ite, +, -, * and bv2int over bit-vectors and keeps int_to_bv only for terms it cannot rewrite (string lengths, str.to_code, division). The result equals int_to_bv in every model. Co-Authored-By: Claude Opus 5.5 --- .../primitive/numeric/BitvectorEncoding.java | 187 +++++++++++++++ .../primitive/numeric/NumericalValue.java | 2 +- .../numeric/floatingpoint/DoubleValue.java | 18 +- .../numeric/floatingpoint/FloatValue.java | 8 +- .../numeric/integral/BooleanValue.java | 4 +- .../primitive/numeric/integral/ByteValue.java | 5 +- .../primitive/numeric/integral/CharValue.java | 5 +- .../primitive/numeric/integral/IntValue.java | 5 +- .../primitive/numeric/integral/LongValue.java | 8 +- .../numeric/integral/ShortValue.java | 5 +- .../numeric/BitvectorEncodingTest.groovy | 222 ++++++++++++++++++ 11 files changed, 435 insertions(+), 34 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/BitvectorEncoding.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/BitvectorEncodingTest.groovy 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..eae53b30 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/primitive/numeric/BitvectorEncoding.java @@ -0,0 +1,187 @@ +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.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: + * + *

+ * + * 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))); + } + + 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..c9e6b224 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; @@ -312,13 +313,10 @@ public IntValue FCMPL(FloatValue f) { private IntValue FCMP(FloatValue f) { int c = concrete.compareTo(f.concrete); - BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager(); - IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); 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 = 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/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..78d59403 --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/value/primitive/numeric/BitvectorEncodingTest.groovy @@ -0,0 +1,222 @@ +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)))) + } +} From 634d6f7e639b5c0419aa7b3f531e167a2dc931da Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 22:30:28 +0000 Subject: [PATCH 2/3] Solve comparisons over int_to_bv of string lengths and char codes over the Integers String lengths, indices and char codes are Integers in the string theory, while Java ints and chars are bit-vectors, so s.length() > 2 reaches Z3 as (bvsgt ((_ int_to_bv 32) (str.len s)) #x00000002). Z3 runs for minutes on small satisfiable queries of that kind. Before each check, rewrite every bit-vector comparison between int_to_bv of a bounded Integer term (str.len, str.indexof, str.to_code, ubv_to_int, numerals, + - * ite of those) and another such term into the Integer comparison of their values. Where the range does not fit the bit-vector, the value keeps the wrap as an ite (modulo only for char codes), so the rewrite is exact. The ranges rely on strings having at most 2^31 - 1 chars, as Java strings do; that bound is added to the query for each string it relied on. Co-Authored-By: Claude Opus 5.5 --- symbolic-explorer/solver/Int2BvLifting.py | 330 ++++++++++++++++++ symbolic-explorer/solver/SolverHandler.py | 29 +- .../tests/test_int2bv_lifting.py | 165 +++++++++ 3 files changed, 516 insertions(+), 8 deletions(-) create mode 100644 symbolic-explorer/solver/Int2BvLifting.py create mode 100644 symbolic-explorer/tests/test_int2bv_lifting.py 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() From 339a71ca9584067190b196749f3410ac99d3974d Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 23:20:47 +0000 Subject: [PATCH 3/3] Encode NaN and signed zeros in FCMP and the compare/compareTo models FCMPG/FCMPL returned a concrete result when an operand was NaN, and a symbolic result that ignored NaN otherwise (-1 for both instructions); the concrete result used Float.compareTo, which orders -0.0 below 0.0. Encode them like DCMP: nanResult if either operand is NaN, else the FP three-way comparison. Double/Float.compare and Double/Float.compareTo now share BitvectorEncoding.javaCompare, which follows the JDK: NaN equals itself and is greater than everything, -0.0 is less than 0.0. The compareTo models had neither. With bit-vector comparison results the solver picks NaN and signed zeros more often, which made these models diverge. Co-Authored-By: Claude Opus 5.5 --- .../invoke/java/lang/DoubleInvocation.java | 29 ++------------ .../invoke/java/lang/FloatInvocation.java | 28 +------------ .../primitive/numeric/BitvectorEncoding.java | 35 ++++++++++++++++ .../numeric/floatingpoint/FloatValue.java | 40 ++++++++++++------- .../reference/lang/DoubleObjectValue.java | 16 ++------ .../reference/lang/FloatObjectValue.java | 16 ++------ .../numeric/BitvectorEncodingTest.groovy | 23 +++++++++++ 7 files changed, 96 insertions(+), 91 deletions(-) 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 index eae53b30..f49831aa 100644 --- 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 @@ -8,6 +8,8 @@ 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; @@ -74,6 +76,39 @@ public static BitvectorFormula compareResult( 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; 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 c9e6b224..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 @@ -277,46 +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(); + 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); // Built over bit-vectors: Z3 decides int_to_bv over FP comparisons badly. - BitvectorFormula res = BitvectorEncoding.compareResult(context.getFormulaManager(), eqCond, gtCond, 32); + 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/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 index 78d59403..825f3b13 100644 --- 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 @@ -219,4 +219,27 @@ class BitvectorEncodingTest extends Specification { !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() + } + } + } + } }