diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/SinCosUF.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/SinCosUF.java deleted file mode 100644 index 5422a5a2..00000000 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/SinCosUF.java +++ /dev/null @@ -1,94 +0,0 @@ -package de.uzl.its.swat.symbolic.UFs; - -import de.uzl.its.swat.common.exceptions.NoThreadContextException; -import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; -import de.uzl.its.swat.thread.ThreadHandler; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.stream.Collectors; - -import org.sosy_lab.java_smt.api.*; - -public class SinCosUF { - private final FormulaType.FloatingPointType DoubleType = FormulaType.getDoublePrecisionFloatingPointType(); - private final FunctionDeclaration sinUF; - private final FunctionDeclaration cosUF; - private final UFManager ufmgr; - private final BooleanFormulaManager bmgr; - private final FloatingPointFormulaManager fmgr; - - private final ArrayList inputValues; - - public SinCosUF(SolverContext ctx) throws NoThreadContextException { - SymbolicTraceHandler sth = ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()); - FormulaManager frml_mgr = ctx.getFormulaManager(); - ufmgr = frml_mgr.getUFManager(); - bmgr = frml_mgr.getBooleanFormulaManager(); - fmgr = frml_mgr.getFloatingPointFormulaManager(); - - sinUF = ufmgr.declareUF("sin", DoubleType, DoubleType); - cosUF = ufmgr.declareUF("cos", DoubleType, DoubleType); - - final double PI = Math.PI; - inputValues = new ArrayList(Arrays.asList( - 0.0, 0.5 * PI, 1.0 * PI, 1.5 * PI, 2.0 * PI, - -0.0, -0.5 * PI, -1.0 * PI, -1.5 * PI, -2.0 * PI, - 1.0, 2.0, 3.0, 4.0)); - int initialSize = inputValues.size(); - for (int i = 0; i < initialSize; i++) { - var out = Math.sin(inputValues.get(i)); - if (!inputValues.contains(out)) - inputValues.add(out); - - out = Math.cos(inputValues.get(i)); - if (!inputValues.contains(out)) - inputValues.add(out); - } - - for (double concreteIn : inputValues) { - var symIn = fmgr.makeNumber(concreteIn, DoubleType); - var symOut = fmgr.makeNumber(Math.sin(concreteIn), DoubleType); - sth.addConstraint(fmgr.equalWithFPSemantics(ufmgr.callUF(sinUF, symIn), symOut)); - - symIn = fmgr.makeNumber(concreteIn, DoubleType); - symOut = fmgr.makeNumber(Math.cos(concreteIn), DoubleType); - sth.addConstraint(fmgr.equalWithFPSemantics(ufmgr.callUF(cosUF, symIn), symOut)); - } - } - - public FloatingPointFormula applySin(FloatingPointFormula symIn) throws NoThreadContextException { - var symOut = ufmgr.callUF(sinUF, symIn); - - SymbolicTraceHandler sth = ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()); - sth.addConstraint(bmgr.and( // Output is between -1 and 1. - fmgr.greaterOrEquals(symOut, fmgr.makeNumber(-1.0, DoubleType)), - fmgr.lessOrEquals(symOut, fmgr.makeNumber(1.0, DoubleType)))); - - // Input must be one of the known inputValues, otherwise the solver can just "make up" any result. - // This loses soundness, but that's okay, because UFs cause precision loss anyway and thus we will never - // give a SAFE verdict. We can however find some VIOLATIONs this way. - sth.addConstraint( - bmgr.or(inputValues.stream().map(v -> fmgr.equalWithFPSemantics(symIn, fmgr.makeNumber(v, DoubleType))) - .collect(Collectors.toList()))); - - return symOut; - } - - public FloatingPointFormula applyCos(FloatingPointFormula symIn) throws NoThreadContextException { - var symOut = ufmgr.callUF(cosUF, symIn); - - SymbolicTraceHandler sth = ThreadHandler.getSymbolicTraceHandler(Thread.currentThread().getId()); - sth.addConstraint(bmgr.and( // Output is between -1 and 1. - fmgr.greaterOrEquals(symOut, fmgr.makeNumber(-1.0, DoubleType)), - fmgr.lessOrEquals(symOut, fmgr.makeNumber(1.0, DoubleType)))); - - // Input must be one of the known inputValues, otherwise the solver can just "make up" any result. - // This loses soundness, but that's okay, because UFs cause precision loss anyway and thus we will never - // give a SAFE verdict. We can however find some VIOLATIONs this way. - sth.addConstraint( - bmgr.or(inputValues.stream().map(v -> fmgr.equalWithFPSemantics(symIn, fmgr.makeNumber(v, DoubleType))) - .collect(Collectors.toList()))); - - return symOut; - } -} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java index 639b2752..3f76b9c4 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/UFHandler.java @@ -7,7 +7,6 @@ public class UFHandler { private EqualsIgnoreCaseUF equalsIgnoreCaseUF; private ToLowerCaseUF toLowerCaseUF; - private SinCosUF sinCosUF; public EqualsIgnoreCaseUF getEqualsIgnoreCaseUF() throws NoThreadContextException { if (equalsIgnoreCaseUF == null) { @@ -22,11 +21,4 @@ public ToLowerCaseUF getToLowerCaseUF() throws NoThreadContextException { } return toLowerCaseUF; } - - public SinCosUF getSinCosUF() throws NoThreadContextException { - if (sinCosUF == null) { - sinCosUF = new SinCosUF(ThreadHandler.getSolverContext(currentThread().getId())); - } - return sinCosUF; - } } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/MathInvocation.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/MathInvocation.java index 69dc5e6d..cb2f0fea 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/MathInvocation.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/MathInvocation.java @@ -3,7 +3,6 @@ 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.UFs.SinCosUF; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; import de.uzl.its.swat.symbolic.value.PlaceHolder; import de.uzl.its.swat.symbolic.value.Value; @@ -12,7 +11,6 @@ import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.LongValue; -import de.uzl.its.swat.thread.ThreadHandler; import org.objectweb.asm.Type; import org.sosy_lab.java_smt.api.*; @@ -37,8 +35,6 @@ public class MathInvocation { SymbolicTraceHandler symbolicTraceHandler, boolean strict) throws NotImplementedException, ValueConversionException { return switch (name) { - case "sin" -> invokeSin(args); - case "cos" -> invokeCos(args); case "abs" -> invokeAbs(args); case "max" -> invokeMax(args); case "min" -> invokeMin(args); @@ -51,6 +47,9 @@ public class MathInvocation { case "toRadians" -> scale(args, 0.017453292519943295, strict ? StrictMath::toRadians : Math::toRadians); case "toDegrees" -> scale(args, 57.29577951308232, strict ? StrictMath::toDegrees : Math::toDegrees); case "getExponent" -> invokeGetExponent(args); + case "signum" -> invokeSignum(args); + case "floorDiv" -> invokeFloorDivMod(args, false); + case "floorMod" -> invokeFloorDivMod(args, true); case "pow" -> SampledMath.binary("pow" + (strict ? "/strict" : ""), args, strict ? StrictMath::pow : Math::pow, // inverses: pow(x, y0) = t at x = t^(1/y0), pow(x0, y) = t at y = log(t) / log(x0) (t, y0) -> y0 == 0 ? Double.NaN : Math.pow(t, 1 / y0), @@ -101,88 +100,53 @@ public class MathInvocation { return PlaceHolder.instance; } - /** - * Invocation handler for Math.sin(double a). - * Uses an UF. - * - * @see Math.sin(double a) - */ - private static Value invokeSin(Value[] args) { - SWATAssert.enforce(args.length == 1, "Wrong argument counts"); - SWATAssert.enforce(args[0] instanceof DoubleValue, "Wrong argument type"); - return sin((DoubleValue) args[0]); - } - - /** - * Symbolic wrapper for Math.sin(double a). - * Uses an UF. - * - * @see Math.sin(double a) - */ - private static DoubleValue sin(DoubleValue a) { - SolverContext ctx = a.context; - - // Fast path: concrete value only - if (!a.isSymbolic()) { - return new DoubleValue(ctx, Math.sin(a.concrete)); - // potentially we could do an addConstraint to remember this concrete case for the UF or other trigonometric UFs - } - - try { - SinCosUF uf = ThreadHandler.getUFHandler(Thread.currentThread().getId()).getSinCosUF(); - - // The symbolic result - var ufResult = uf.applySin(a.formula); - - // Return with concrete result for concolic steering - return new DoubleValue(ctx, Math.sin(a.concrete), ufResult); - - } catch (Exception e) { - // Fallback to concrete-only if UF setup fails - return new DoubleValue(ctx, Math.sin(a.concrete)); + /** Math.signum: the argument itself for zeros and NaN, otherwise 1.0 with its sign. */ + private static Value invokeSignum(Value[] args) { + if (args.length != 1) return PlaceHolder.instance; + if (args[0] instanceof DoubleValue d) { + return new DoubleValue(d.context, Math.signum(d.concrete), signum(d.context, d.formula, new DoubleValue(d.context, 1.0).formula)); + } else if (args[0] instanceof FloatValue f) { + return new FloatValue(f.context, Math.signum(f.concrete), signum(f.context, f.formula, new FloatValue(f.context, 1.0f).formula)); } + return PlaceHolder.instance; } - /** - * Invocation handler for Math.cos(double a). - * Uses an UF. - * - * @see Math.cos(double a) - */ - private static Value invokeCos(Value[] args) { - SWATAssert.enforce(args.length == 1, "Wrong argument counts"); - SWATAssert.enforce(args[0] instanceof DoubleValue, "Wrong argument type"); - return cos((DoubleValue) args[0]); + private static FloatingPointFormula signum(SolverContext ctx, FloatingPointFormula x, FloatingPointFormula one) { + FloatingPointFormulaManager fpfm = ctx.getFormulaManager().getFloatingPointFormulaManager(); + BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); + return bmgr.ifThenElse(bmgr.or(fpfm.isZero(x), fpfm.isNaN(x)), x, + bmgr.ifThenElse(fpfm.isNegative(x), fpfm.negate(one), one)); } /** - * Symbolic wrapper for Math.cos(double a). - * Uses an UF. - * - * @see Math.cos(double a) + * Math.floorDiv and floorMod of two ints or two longs, for a concrete non-zero divisor. With a + * symbolic divisor the ArithmeticException for zero would need a branch of its own, so that + * case stays unmodelled. */ - private static DoubleValue cos(DoubleValue a) { - SolverContext ctx = a.context; - - // Fast path: concrete value only - if (!a.isSymbolic()) { - return new DoubleValue(ctx, Math.cos(a.concrete)); - // potentially we could do an addConstraint to remember this concrete case for the UF or other trigonometric UFs + private static Value invokeFloorDivMod(Value[] args, boolean mod) { + if (args.length != 2) return PlaceHolder.instance; + if (args[0] instanceof LongValue x && args[1] instanceof LongValue y) { + if (y.isSymbolic() || y.concrete == 0) return PlaceHolder.instance; + BitvectorFormula r = floorDivMod(x.context, x.formula, y.formula, 64, mod); + return new LongValue(x.context, mod ? Math.floorMod(x.concrete, y.concrete) : Math.floorDiv(x.concrete, y.concrete), r); + } else if (args[0] instanceof IntValue x && args[1] instanceof IntValue y) { + if (y.isSymbolic() || y.concrete == 0) return PlaceHolder.instance; + BitvectorFormula r = floorDivMod(x.context, x.formula, y.formula, 32, mod); + return new IntValue(x.context, mod ? Math.floorMod(x.concrete, y.concrete) : Math.floorDiv(x.concrete, y.concrete), r); } + return PlaceHolder.instance; + } - try { - SinCosUF uf = ThreadHandler.getUFHandler(Thread.currentThread().getId()).getSinCosUF(); - - // The symbolic result - var ufResult = uf.applyCos(a.formula); - - // Return with concrete result for concolic steering - return new DoubleValue(ctx, Math.cos(a.concrete), ufResult); - - } catch (Exception e) { - // Fallback to concrete-only if UF setup fails - return new DoubleValue(ctx, Math.cos(a.concrete)); - } + /** As the JDK: q = x / y, minus one if the signs differ and the division is not exact; mod = x - q * y. */ + private static BitvectorFormula floorDivMod(SolverContext ctx, BitvectorFormula x, BitvectorFormula y, int width, boolean mod) { + BitvectorFormulaManager bvmgr = ctx.getFormulaManager().getBitvectorFormulaManager(); + BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); + BitvectorFormula q = bvmgr.divide(x, y, true); + BooleanFormula adjust = bmgr.and( + bvmgr.lessThan(bvmgr.xor(x, y), bvmgr.makeBitvector(width, 0), true), + bmgr.not(bvmgr.equal(bvmgr.multiply(q, y), x))); + BitvectorFormula floorQ = bmgr.ifThenElse(adjust, bvmgr.subtract(q, bvmgr.makeBitvector(width, 1)), q); + return mod ? bvmgr.subtract(x, bvmgr.multiply(floorQ, y)) : floorQ; } private static Value invokeAbs(Value[] args) throws NotImplementedException, ValueConversionException { @@ -222,11 +186,9 @@ private static DoubleValue cos(DoubleValue a) { BooleanFormulaManager bfm = args[0].context.getFormulaManager().getBooleanFormulaManager(); if (args[0] instanceof FloatValue v && args[1] instanceof FloatValue w) { - FloatingPointFormulaManager fpfm = v.context.getFormulaManager().getFloatingPointFormulaManager(); - return new FloatValue(v.context, Math.max(v.concrete, w.concrete), fpfm.max(v.formula, w.formula)); + return new FloatValue(v.context, Math.max(v.concrete, w.concrete), fpMinMax(v.context, v.formula, w.formula, true)); } else if (args[0] instanceof DoubleValue v && args[1] instanceof DoubleValue w) { - FloatingPointFormulaManager fpfm = v.context.getFormulaManager().getFloatingPointFormulaManager(); - return new DoubleValue(v.context, Math.max(v.concrete, w.concrete), fpfm.max(v.formula, w.formula)); + return new DoubleValue(v.context, Math.max(v.concrete, w.concrete), fpMinMax(v.context, v.formula, w.formula, true)); } else if (args[0] instanceof LongValue v && args[1] instanceof LongValue w) { BitvectorFormulaManager bvmgr = v.context.getFormulaManager().getBitvectorFormulaManager(); return new LongValue(v.context, Math.max(v.concrete, w.concrete), bfm.ifThenElse( @@ -251,11 +213,9 @@ private static DoubleValue cos(DoubleValue a) { BooleanFormulaManager bfm = args[0].context.getFormulaManager().getBooleanFormulaManager(); if (args[0] instanceof FloatValue v && args[1] instanceof FloatValue w) { - FloatingPointFormulaManager fpfm = v.context.getFormulaManager().getFloatingPointFormulaManager(); - return new FloatValue(v.context, Math.min(v.concrete, w.concrete), fpfm.min(v.formula, w.formula)); + return new FloatValue(v.context, Math.min(v.concrete, w.concrete), fpMinMax(v.context, v.formula, w.formula, false)); } else if (args[0] instanceof DoubleValue v && args[1] instanceof DoubleValue w) { - FloatingPointFormulaManager fpfm = v.context.getFormulaManager().getFloatingPointFormulaManager(); - return new DoubleValue(v.context, Math.min(v.concrete, w.concrete), fpfm.min(v.formula, w.formula)); + return new DoubleValue(v.context, Math.min(v.concrete, w.concrete), fpMinMax(v.context, v.formula, w.formula, false)); } else if (args[0] instanceof LongValue v && args[1] instanceof LongValue w) { BitvectorFormulaManager bvmgr = v.context.getFormulaManager().getBitvectorFormulaManager(); return new LongValue(v.context, Math.min(v.concrete, w.concrete), bfm.ifThenElse( @@ -273,6 +233,24 @@ private static DoubleValue cos(DoubleValue a) { } } + /** + * Math.max and min of two floats or doubles as the JDK computes them: NaN if either argument is + * NaN, and +0.0 (max) or -0.0 (min) for two zeros of different sign. SMT-LIB's fp.max and fp.min + * differ in both: they return the other argument for one NaN and either zero for two zeros. + */ + private static FloatingPointFormula fpMinMax(SolverContext ctx, FloatingPointFormula a, FloatingPointFormula b, boolean max) { + FloatingPointFormulaManager fpfm = ctx.getFormulaManager().getFloatingPointFormulaManager(); + BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); + // max: if (a != a) a; else if (a, b zero and a = -0.0) b; else a >= b ? a : b + // min: if (a != a) a; else if (a, b zero and b = -0.0) b; else a <= b ? a : b + BooleanFormula negZero = max + ? bmgr.and(fpfm.isZero(a), fpfm.isNegative(a)) + : bmgr.and(fpfm.isZero(b), fpfm.isNegative(b)); + return bmgr.ifThenElse(fpfm.isNaN(a), a, + bmgr.ifThenElse(bmgr.and(fpfm.isZero(a), fpfm.isZero(b), negZero), b, + bmgr.ifThenElse(max ? fpfm.greaterOrEquals(a, b) : fpfm.lessOrEquals(a, b), a, b))); + } + private static Value invokeSqrt(Value[] args) throws NotImplementedException, ValueConversionException { SWATAssert.enforce(args.length == 1, "Wrong argument counts"); SWATAssert.enforce(args[0] instanceof DoubleValue, "Wrong argument type"); @@ -290,7 +268,7 @@ private static DoubleValue cos(DoubleValue a) { * - NaN returns 0 * - Negative infinity or values <= MIN_VALUE return MIN_VALUE * - Positive infinity or values >= MAX_VALUE return MAX_VALUE - * - Otherwise, round to nearest integer + * - Otherwise, round to the nearest integer, ties toward positive infinity * * Note: SMT's fp.to_sbv has undefined behavior for NaN/infinity, so we must * explicitly encode Java's semantics with if-then-else. @@ -329,7 +307,7 @@ private static DoubleValue cos(DoubleValue a) { fpfm.greaterOrEquals(v.formula, maxThreshold)); // Normal case: round and convert to int - FloatingPointFormula rounded = fpfm.round(v.formula, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + FloatingPointFormula rounded = roundHalfUp(v.context, v.formula, new FloatValue(v.context, 0.5f).formula, new FloatValue(v.context, 1.0f).formula); BitvectorFormula normalResult = fpfm.castTo(rounded, true, FormulaType.getBitvectorTypeWithSize(32), FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); @@ -374,7 +352,7 @@ private static DoubleValue cos(DoubleValue a) { fpfm.greaterOrEquals(v.formula, maxThreshold)); // Normal case: round and convert to long - FloatingPointFormula rounded = fpfm.round(v.formula, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); + FloatingPointFormula rounded = roundHalfUp(v.context, v.formula, new DoubleValue(v.context, 0.5).formula, new DoubleValue(v.context, 1.0).formula); BitvectorFormula normalResult = fpfm.castTo(rounded, true, FormulaType.getBitvectorTypeWithSize(64), FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN); @@ -392,6 +370,19 @@ private static DoubleValue cos(DoubleValue a) { return PlaceHolder.instance; } } + /** + * The integer closest to x, ties toward positive infinity, as Math.round rounds: floor(x), plus + * one if x - floor(x) >= 0.5. The difference is exact wherever it can reach 0.5 (Sterbenz; for x + * in (-0.5, 0) it is above 0.5 and rounding keeps it there), and beyond 2^52 (2^23) x is + * integral, so floor(x) + 1 is only formed where it is exact. + */ + private static FloatingPointFormula roundHalfUp(SolverContext ctx, FloatingPointFormula x, FloatingPointFormula half, FloatingPointFormula one) { + FloatingPointFormulaManager fpfm = ctx.getFormulaManager().getFloatingPointFormulaManager(); + BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); + FloatingPointFormula floor = fpfm.round(x, FloatingPointRoundingMode.TOWARD_NEGATIVE); + return bmgr.ifThenElse(fpfm.greaterOrEquals(fpfm.subtract(x, floor), half), fpfm.add(floor, one), floor); + } + /* * * private static IntValue invokeMax(IntValue a, IntValue b) { diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SampledMath.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SampledMath.java index 6b449766..228fadea 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SampledMath.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/invoke/java/lang/SampledMath.java @@ -5,34 +5,48 @@ 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; +import java.util.ArrayList; +import java.util.Arrays; import java.util.LinkedHashMap; +import java.util.List; import java.util.Map; import java.util.concurrent.ConcurrentHashMap; +import java.util.concurrent.atomic.AtomicInteger; import java.util.function.DoubleBinaryOperator; import java.util.function.DoubleUnaryOperator; 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.FormulaManager; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; import org.sosy_lab.java_smt.api.SolverContext; /** - * Approximate symbolic models of transcendental Math functions (tan, log, pow, ...), which have no - * exact encoding in floating-point SMT. + * Approximate symbolic models of transcendental Math functions (sin, tan, log, pow, ...), which have + * no exact encoding in floating-point SMT. * - *

The model is a lookup table: exact at a fixed set of sample inputs, and the concrete result of - * this execution everywhere else. Where the result was concrete before, it still is, so the model - * never constrains a path more than concretization did; but the solver can now pick a sample - * input to reach a branch that needs a particular result. Samples are "nice" inputs plus inputs at - * which the function hits "nice" outputs, found through its inverse. + *

Each call is an application of its own uninterpreted function, {@code math__(x)}, + * defined by a trace constraint as a lookup table: exact at a fixed set of sample inputs, and the + * concrete result of this execution everywhere else. Where the result was concrete before, it + * still is, so the model never constrains a path more than concretization did; but the solver can + * now pick a sample input to reach a branch that needs a particular result. Samples are "nice" + * inputs plus inputs at which the function hits "nice" outputs, found through its inverse. * - *

Using a model records precision loss: an exhausted search is then no proof of safety. + *

The function application keeps the approximation visible: a branch constraint that contains + * one is reported as precision loss (see DTOBuilder), so an exhausted search proves nothing, and + * the explorer can tell which queries depend on a guess. A result that never reaches a branch + * leaves the explored paths exact, so it costs no precision. Every call has its own function, so + * definitions never constrain each other: each one can always be satisfied by its own function + * value, whatever the inputs, and leaves the queries that do not mention it unchanged. */ final class SampledMath { private static final double[] NICE_INPUTS = { 0.0, -0.0, 0.5, -0.5, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 10, -10, 100, -100, 1000, 0.1, -0.1, - Math.PI, -Math.PI, Math.PI / 2, -Math.PI / 2, Math.PI / 3, Math.PI / 4, -Math.PI / 4, Math.PI / 6, Math.E + Math.PI, -Math.PI, Math.PI / 2, -Math.PI / 2, Math.PI / 3, Math.PI / 4, -Math.PI / 4, Math.PI / 6, Math.E, + 1.5 * Math.PI, -1.5 * Math.PI, 2 * Math.PI, -2 * Math.PI }; private static final double[] NICE_OUTPUTS = {0.0, 0.5, -0.5, 1, -1, 2, -2, 3, -3, 5, -5, 10, -10, 100}; @@ -42,20 +56,30 @@ final class SampledMath { private record Unary(DoubleUnaryOperator f, DoubleUnaryOperator strictF, DoubleUnaryOperator inverse) {} - private static final Map UNARY = Map.of( - "tan", new Unary(Math::tan, StrictMath::tan, Math::atan), - "atan", new Unary(Math::atan, StrictMath::atan, Math::tan), - "asin", new Unary(Math::asin, StrictMath::asin, Math::sin), - "acos", new Unary(Math::acos, StrictMath::acos, Math::cos), - "log", new Unary(Math::log, StrictMath::log, Math::exp), - "log10", new Unary(Math::log10, StrictMath::log10, t -> Math.pow(10, t)), - "log1p", new Unary(Math::log1p, StrictMath::log1p, Math::expm1), - "exp", new Unary(Math::exp, StrictMath::exp, Math::log), - "expm1", new Unary(Math::expm1, StrictMath::expm1, Math::log1p), - "cbrt", new Unary(Math::cbrt, StrictMath::cbrt, t -> t * t * t)); + private static final Map UNARY = Map.ofEntries( + Map.entry("sin", new Unary(Math::sin, StrictMath::sin, Math::asin)), + Map.entry("cos", new Unary(Math::cos, StrictMath::cos, Math::acos)), + Map.entry("tan", new Unary(Math::tan, StrictMath::tan, Math::atan)), + Map.entry("atan", new Unary(Math::atan, StrictMath::atan, Math::tan)), + Map.entry("asin", new Unary(Math::asin, StrictMath::asin, Math::sin)), + Map.entry("acos", new Unary(Math::acos, StrictMath::acos, Math::cos)), + Map.entry("log", new Unary(Math::log, StrictMath::log, Math::exp)), + Map.entry("log10", new Unary(Math::log10, StrictMath::log10, t -> Math.pow(10, t))), + Map.entry("log1p", new Unary(Math::log1p, StrictMath::log1p, Math::expm1)), + Map.entry("exp", new Unary(Math::exp, StrictMath::exp, Math::log)), + Map.entry("expm1", new Unary(Math::expm1, StrictMath::expm1, Math::log1p)), + Map.entry("cbrt", new Unary(Math::cbrt, StrictMath::cbrt, t -> t * t * t))); private static final Map SAMPLES = new ConcurrentHashMap<>(); + /** Prefix of the functions the models are built from; the explorer recognises them by it. */ + static final String UF_PREFIX = "math_"; + + private static final FormulaType.FloatingPointType DOUBLE = FormulaType.getDoublePrecisionFloatingPointType(); + + /** Numbers the calls of this execution, so that every call has its own function. */ + private static final AtomicInteger CALLS = new AtomicInteger(); + private SampledMath() {} static Value unary(String name, boolean strict, Value[] args, SymbolicTraceHandler sth) throws NotImplementedException { @@ -64,9 +88,9 @@ private SampledMath() {} DoubleUnaryOperator f = strict ? u.strictF() : u.f(); double result = f.applyAsDouble(x.concrete); if (!x.isSymbolic()) return new DoubleValue(x.context, result); - double[] samples = SAMPLES.computeIfAbsent(name + (strict ? "/strict" : ""), k -> samples(f, u.inverse())); - sth.recordSymbolicPrecisionLoss(); - return new DoubleValue(x.context, result, table(x.context, x.formula, f, samples, result)); + String key = name + (strict ? "_strict" : ""); + double[] samples = SAMPLES.computeIfAbsent(key, k -> samples(f, u.inverse())); + return new DoubleValue(x.context, result, define(x.context, key, sth, table(x.context, x.formula, f, samples, result), x.formula)); } /** @@ -81,31 +105,47 @@ private SampledMath() {} SolverContext ctx = a.context; double result = f.applyAsDouble(a.concrete, b.concrete); if (!a.isSymbolic() && !b.isSymbolic()) return new DoubleValue(ctx, result); - sth.recordSymbolicPrecisionLoss(); + FloatingPointFormula table; if (!b.isSymbolic()) { double second = b.concrete; DoubleUnaryOperator g = v -> f.applyAsDouble(v, second); double[] samples = SAMPLES.computeIfAbsent(key + "/1/" + Double.doubleToRawLongBits(second), k -> samples(g, t -> inverseFirst.applyAsDouble(t, second))); - return new DoubleValue(ctx, result, table(ctx, a.formula, g, samples, result)); - } - if (!a.isSymbolic()) { + table = table(ctx, a.formula, g, samples, result); + } else if (!a.isSymbolic()) { double first = a.concrete; DoubleUnaryOperator g = v -> f.applyAsDouble(first, v); double[] samples = SAMPLES.computeIfAbsent(key + "/2/" + Double.doubleToRawLongBits(first), k -> samples(g, t -> inverseSecond.applyAsDouble(t, first))); - return new DoubleValue(ctx, result, table(ctx, b.formula, g, samples, result)); - } - FloatingPointFormulaManager fpfm = ctx.getFormulaManager().getFloatingPointFormulaManager(); - BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); - FloatingPointFormula table = constant(ctx, result); - for (double x : GRID) { - for (double y : GRID) { - BooleanFormula at = bmgr.and(fpfm.assignment(a.formula, constant(ctx, x)), fpfm.assignment(b.formula, constant(ctx, y))); - table = bmgr.ifThenElse(at, constant(ctx, f.applyAsDouble(x, y)), table); + table = table(ctx, b.formula, g, samples, result); + } else { + FloatingPointFormulaManager fpfm = ctx.getFormulaManager().getFloatingPointFormulaManager(); + BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); + table = constant(ctx, result); + for (double x : GRID) { + for (double y : GRID) { + BooleanFormula at = bmgr.and(fpfm.assignment(a.formula, constant(ctx, x)), fpfm.assignment(b.formula, constant(ctx, y))); + table = bmgr.ifThenElse(at, constant(ctx, f.applyAsDouble(x, y)), table); + } } } - return new DoubleValue(ctx, result, table); + return new DoubleValue(ctx, result, define(ctx, key, sth, table, a.formula, b.formula)); + } + + /** + * A fresh function {@code math__} applied to {@code args}, defined as {@code value} by a + * trace constraint. + */ + private static FloatingPointFormula define(SolverContext ctx, String key, SymbolicTraceHandler sth, + FloatingPointFormula value, FloatingPointFormula... args) { + FormulaManager fmgr = ctx.getFormulaManager(); + List> argTypes = new ArrayList<>(); + for (FloatingPointFormula arg : args) argTypes.add(DOUBLE); + FunctionDeclaration uf = fmgr.getUFManager() + .declareUF(UF_PREFIX + key + "_" + CALLS.getAndIncrement(), DOUBLE, argTypes); + FloatingPointFormula application = fmgr.getUFManager().callUF(uf, Arrays.asList(args)); + sth.addConstraint(fmgr.getFloatingPointFormulaManager().assignment(application, value)); + return application; } /** ite(x = s1, f(s1), ite(x = s2, f(s2), ... otherwise)), comparing bit patterns so -0.0 and NaN are their own samples. */ diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java index 51f5bb55..756c2e69 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTrace.java @@ -25,9 +25,10 @@ class SymbolicTrace { // If true, an invocation occurred that was not instrumented but received symbolic arguments. private boolean symbolicContextLoss = false; - // If true, a model was used that is only approximate, e.g. a sampled transcendental function. - // Branch constraints with UFs are detected as precision loss separately. Also sent on its own - // (TraceDTO.approximateModel), so the explorer can expect divergences from such traces. + // If true, a model was used that is only approximate, e.g. object array elements tracked at the + // concrete index only. Branch constraints with UFs (which include the sampled Math functions) + // are detected as precision loss separately. Also sent on its own (TraceDTO.approximateModel), + // so the explorer can expect divergences from such traces. private boolean symbolicPrecisionLoss = false; // If true, reference equality semantics may have changed due to comparing user-de-interned strings. diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java index bc99d00f..329fdf39 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/dto/TraceDTO.java @@ -31,8 +31,10 @@ public class TraceDTO { private boolean symbolicPrecisionLoss = false; @SuppressWarnings("unused") private boolean referenceSemanticChange = false; - // Whether an approximate model (a sampled Math function) was used. Unlike symbolicPrecisionLoss, - // which also covers exact UF-based models, solutions from such a trace are only guesses. + // Whether an approximate model was used that is precision loss wherever it is used (e.g. object + // array elements at the concrete index). Unlike symbolicPrecisionLoss, which also covers exact + // UF-based models, solutions from such a trace are only guesses. Sampled Math functions are + // recognised per query instead, by their function names. @SuppressWarnings("unused") private boolean approximateModel = false; diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/MathInvocationSpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/MathInvocationSpec.groovy new file mode 100644 index 00000000..ba04bb3f --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/invoke/MathInvocationSpec.groovy @@ -0,0 +1,161 @@ +package de.uzl.its.swat.symbolic.invoke + +import de.uzl.its.swat.symbolic.invoke.java.lang.MathInvocation +import de.uzl.its.swat.symbolic.value.Value +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.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.* +import spock.lang.Shared +import spock.lang.Specification + +/** + * The exact Math models agree with the JDK on every input: for symbolic arguments fixed to the + * input, the model's result can only be the JDK's result (bit for bit, so NaN and -0.0 count). + */ +class MathInvocationSpec extends Specification { + + @Shared SolverContext context + @Shared FloatingPointFormulaManager fpmgr + @Shared BitvectorFormulaManager bvmgr + + static final List DOUBLES = [0.0d, -0.0d, 0.5d, -0.5d, 1.5d, -1.5d, 2.5d, -2.5d, 0.49999999999999994d, + -0.49999999999999994d, 1e-300d, -1e-20d, 3.7d, -3.7d, 4503599627370495.5d, 4503599627370497d, + 9.223372036854775807E18d, -9.223372036854775808E18d, 1e300d, Double.MIN_VALUE, Double.MAX_VALUE, + Double.POSITIVE_INFINITY, Double.NEGATIVE_INFINITY, Double.NaN] + static final List FLOATS = [0.0f, -0.0f, 0.5f, -0.5f, 2.5f, -2.5f, 0.49999997f, -1e-20f, 3.7f, -3.7f, + 8388607.5f, 2.14748365E9f, -2.14748365E9f, Float.MIN_VALUE, Float.MAX_VALUE, + Float.POSITIVE_INFINITY, Float.NEGATIVE_INFINITY, Float.NaN] + static final List INTS = [0, 1, -1, 7, -7, 3, -3, Integer.MAX_VALUE, Integer.MIN_VALUE] + static final List LONGS = [0L, 1L, -1L, 7L, -7L, 3L, -3L, Long.MAX_VALUE, Long.MIN_VALUE] + + def setupSpec() { + context = SolverContextFactory.createSolverContext( + Configuration.defaultConfiguration(), + BasicLogManager.create(Configuration.defaultConfiguration()), + ShutdownManager.create().getNotifier(), + SolverContextFactory.Solvers.Z3) + fpmgr = context.getFormulaManager().getFloatingPointFormulaManager() + bvmgr = context.getFormulaManager().getBitvectorFormulaManager() + } + + def cleanupSpec() { + context.close() + } + + private int vars = 0 + + /** A symbolic argument fixed to the value v by the returned constraint. */ + private List symbolic(Object v) { + String name = "X" + (vars++) + if (v instanceof Double) { + def x = fpmgr.makeVariable(name, FormulaType.getDoublePrecisionFloatingPointType()) + return [new DoubleValue(context, v, x), fpmgr.assignment(x, constant(v))] + } else if (v instanceof Float) { + def x = fpmgr.makeVariable(name, FormulaType.getSinglePrecisionFloatingPointType()) + return [new FloatValue(context, v, x), fpmgr.assignment(x, constant(v))] + } else if (v instanceof Long) { + def x = bvmgr.makeVariable(64, name) + return [new LongValue(context, v, x), bvmgr.equal(x, bvmgr.makeBitvector(64, v))] + } else { + def x = bvmgr.makeVariable(32, name) + return [new IntValue(context, v as int, x), bvmgr.equal(x, bvmgr.makeBitvector(32, v as int))] + } + } + + private Formula constant(Object v) { + if (v instanceof Double) return v.isNaN() ? fpmgr.makeNaN(FormulaType.getDoublePrecisionFloatingPointType()) : new DoubleValue(context, v).formula + if (v instanceof Float) return v.isNaN() ? fpmgr.makeNaN(FormulaType.getSinglePrecisionFloatingPointType()) : new FloatValue(context, v).formula + if (v instanceof Long) return bvmgr.makeBitvector(64, v) + return bvmgr.makeBitvector(32, v as int) + } + + /** Whether the model of name on the arguments agrees with expected, symbolically and concretely. */ + private boolean agrees(String name, List args, Object expected) { + def fixed = args.collect { symbolic(it) } + Value result = MathInvocation.invokeStaticMethod(name, fixed.collect { it[0] } as Value[], null, null, false) + def bmgr = context.getFormulaManager().getBooleanFormulaManager() + def differs = result.formula instanceof FloatingPointFormula + ? bmgr.not(fpmgr.assignment(result.formula, constant(expected))) + : bmgr.not(bvmgr.equal(result.formula, constant(expected))) + def prover = context.newProverEnvironment() + try { + fixed.each { prover.addConstraint(it[1]) } + prover.addConstraint(differs) + boolean concreteOk = (expected instanceof Double || expected instanceof Float) + ? Double.compare(((Number) result.concrete).doubleValue(), ((Number) expected).doubleValue()) == 0 + : result.concrete == expected + return prover.isUnsat() && concreteOk + } finally { + prover.close() + } + } + + def "round(double) rounds ties toward positive infinity and saturates"() { + expect: + DOUBLES.every { agrees("round", [it], Math.round(it)) } + } + + def "round(float) rounds ties toward positive infinity and saturates"() { + expect: + FLOATS.every { agrees("round", [it], Math.round(it)) } + } + + def "max and min of doubles keep NaN and order the zeros"() { + expect: + [DOUBLES, DOUBLES].combinations().every { a, b -> + agrees("max", [a, b], Math.max(a, b)) && agrees("min", [a, b], Math.min(a, b)) + } + } + + def "max and min of floats keep NaN and order the zeros"() { + expect: + [FLOATS, FLOATS].combinations().every { a, b -> + agrees("max", [a, b], Math.max(a, b)) && agrees("min", [a, b], Math.min(a, b)) + } + } + + def "signum"() { + expect: + DOUBLES.every { agrees("signum", [it], Math.signum(it)) } + FLOATS.every { agrees("signum", [it], Math.signum(it)) } + } + + def "floorDiv and floorMod for a concrete divisor"() { + expect: + [INTS, INTS.findAll { it != 0 }].combinations().every { a, b -> + agreesWithConcreteDivisor("floorDiv", a, b, Math.floorDiv(a, b)) && agreesWithConcreteDivisor("floorMod", a, b, Math.floorMod(a, b)) + } + [LONGS, LONGS.findAll { it != 0 }].combinations().every { a, b -> + agreesWithConcreteDivisor("floorDiv", a, b, Math.floorDiv(a, b)) && agreesWithConcreteDivisor("floorMod", a, b, Math.floorMod(a, b)) + } + } + + private boolean agreesWithConcreteDivisor(String name, Object a, Object b, Object expected) { + def (x, fixed) = symbolic(a) + def y = b instanceof Long ? new LongValue(context, b) : new IntValue(context, b as int) + Value result = MathInvocation.invokeStaticMethod(name, [x, y] as Value[], null, null, false) + def prover = context.newProverEnvironment() + try { + prover.addConstraint(fixed) + prover.addConstraint(context.getFormulaManager().getBooleanFormulaManager().not(bvmgr.equal(result.formula, constant(expected)))) + return prover.isUnsat() && result.concrete == expected + } finally { + prover.close() + } + } + + def "floorDiv with a symbolic divisor stays unmodelled"() { + given: + def (x, fx) = symbolic(7) + def (y, fy) = symbolic(2) + + expect: + !(MathInvocation.invokeStaticMethod("floorDiv", [x, y] as Value[], null, null, false) instanceof IntValue) + } +} diff --git a/symbolic-explorer/SymbolicExplorer.py b/symbolic-explorer/SymbolicExplorer.py index be21affd..a6b3a933 100755 --- a/symbolic-explorer/SymbolicExplorer.py +++ b/symbolic-explorer/SymbolicExplorer.py @@ -137,6 +137,7 @@ def init_args(parser: argparse.ArgumentParser): parser.add_argument("--sa-no-callback-targets", action="store_true", help="Do not count library calls as possible asserts when application code that library code may call back (overrides of library methods, lambdas) can reach an assert. Unsound: an assert reached only through such a callback can then give a false SAFE", default=False) parser.add_argument("--sa-rank-distance", action="store_true", help="Try branches closest to an assert (by static pre-analysis graph distance) first, instead of in plain DFS order", default=False) parser.add_argument("--solver-rlimit", type=int, default=0, help="Z3 resource limit (rlimit) for the first query of each branch in sv-comp mode; a branch that runs out is retried later with a growing limit. 0 (default): unlimited") + parser.add_argument("--approximate-rlimit", type=int, default=250_000_000, help="Z3 resource limit for a query over an approximate Math model in sv-comp mode (about one to one and a half minutes); one that runs out is given up on, which rules out SAFE as the model does anyway. 0: no limit beyond --solver-rlimit") parser.add_argument("--parallel-sa", action="store_true", help="Run the static pre-analysis in the background and use it once it is ready (sv-comp mode). By default exploration waits for it: running it in parallel makes runs nondeterministic", default=False) # SV-COMP witness arguments: the explorer writes the violation witness from the trace of the diff --git a/symbolic-explorer/data/BinaryExecutionTree/Tree.py b/symbolic-explorer/data/BinaryExecutionTree/Tree.py index 978dc99e..c782ceca 100755 --- a/symbolic-explorer/data/BinaryExecutionTree/Tree.py +++ b/symbolic-explorer/data/BinaryExecutionTree/Tree.py @@ -33,7 +33,7 @@ def __init__(self, endpoint_id: Union[str, int]): self.symbolic_context_loss = False self.symbolic_precision_loss = False self.reference_semantic_change = False - # Traces that used an approximate model (a sampled Math function). A solution built from one + # Traces that used an approximate model (TraceDTO.approximateModel). A solution built from one # is a guess, so the next run may take another path than predicted without anything being wrong. self.approximate_traces: Set[str] = set() # How often the next run did take another path than such a guessed solution predicted. diff --git a/symbolic-explorer/driver/SVCompDriver.py b/symbolic-explorer/driver/SVCompDriver.py index a6c70f11..a57e66f7 100644 --- a/symbolic-explorer/driver/SVCompDriver.py +++ b/symbolic-explorer/driver/SVCompDriver.py @@ -368,7 +368,8 @@ def solve_candidates(self, candidates: list[Node]) -> tuple[Node | None, dict, b alone = retry and len(pending) == 1 for branch in pending: rlimit = None if alone else self.solver_rlimit_for(branch) - sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None, solver_rlimit=rlimit) + sat, sol = StrategyService.solve_branch(branch, solver_timeout_ms=None, solver_rlimit=rlimit, + approximate_rlimit=getattr(self.args, 'approximate_rlimit', None)) self.nr_solver_calls += 1 if sat == SATResult.SAT: return branch, sol, gave_up @@ -411,7 +412,13 @@ def retrieve_solution(self): logger.info(f'[SYMBOLIC EXPLORATION] Found solution for branch {branch.id} {"skipped" if branch.skipped is None else "branched"}') # remember which branch we want to explore self.state.branch_to_explore = branch - self.state.solution_is_guess = Database.instance().is_approximate_trace(ENDPOINT_ID, branch.trace_id) + # A solution is a guess if its trace used an approximate model, which is precision loss, or + # if its query is over a sampled Math function: that function is in a branch constraint of + # the trace, so the trace is precision loss as well. In both cases a divergence cannot lead + # to a false SAFE. A solution from a trace whose Math results never reach the query is + # exact, and a divergence from it is an error. + self.state.solution_is_guess = (Database.instance().is_approximate_trace(ENDPOINT_ID, branch.trace_id) + or StrategyService.is_approximate_query(branch)) sol_viz = [f'{key}: {val["plain_value"]}' for key, val in sol.items()] logger.info(f'[SYMBOLIC EXPLORATION] SAT solution: {sol}') diff --git a/symbolic-explorer/parse/DataTransferObjects.py b/symbolic-explorer/parse/DataTransferObjects.py index 68be5da1..60d78744 100644 --- a/symbolic-explorer/parse/DataTransferObjects.py +++ b/symbolic-explorer/parse/DataTransferObjects.py @@ -91,7 +91,8 @@ class ConstraintRequest(BaseModel): symbolicContextLoss: bool symbolicPrecisionLoss: bool referenceSemanticChange: bool = False - # An approximate model (a sampled Math function) was used: solutions from this trace are guesses. + # An approximate model was used that is precision loss wherever it is used: solutions from this + # trace are guesses. Queries over sampled Math functions are recognised by their function names. approximateModel: bool = False diff --git a/symbolic-explorer/solver/SolverHandler.py b/symbolic-explorer/solver/SolverHandler.py index 8e781a72..ab13dc8d 100755 --- a/symbolic-explorer/solver/SolverHandler.py +++ b/symbolic-explorer/solver/SolverHandler.py @@ -260,6 +260,9 @@ def extract_and_encode_values(model: Any) -> Dict[str, Dict[str, Union[str, int] for var_decl in model.decls(): # Extract the variable (as an expression) and its value name = str(var_decl.name()) + # Functions (e.g. the executor's Math models, math_tan_3) are not inputs + if var_decl.arity() > 0: + continue # Updated regex to match array names like "[I_0" as well as regular names if not re.match(r'(\[?[\w\/]+)_(\d+)', name): continue diff --git a/symbolic-explorer/strategy/StrategyService.py b/symbolic-explorer/strategy/StrategyService.py index 9afe6927..d9daaa9a 100755 --- a/symbolic-explorer/strategy/StrategyService.py +++ b/symbolic-explorer/strategy/StrategyService.py @@ -1,6 +1,8 @@ +import functools import json import math import logging +import re import time from data.BinaryExecutionTree.Node import Node @@ -12,6 +14,19 @@ logger = logging.getLogger(__name__) +# A declaration of a function with at least one argument, i.e. an uninterpreted function rather +# than a variable: "(declare-fun f ( ...) )". +_UF_DECLARATION = re.compile(r'\(declare-fun\s+(\|[^|]*\||[^\s()]+)\s+\(\s*[^\s)]') + +# Prefix of the functions the executor builds approximate Math models from (SampledMath.UF_PREFIX). +APPROXIMATE_UF_PREFIX = 'math_' + + +@functools.lru_cache(maxsize=4096) +def declared_ufs(smt: str) -> frozenset[str]: + """The uninterpreted functions an SMT-LIB string declares.""" + return frozenset(name.strip("|") for name in _UF_DECLARATION.findall(smt)) + class StrategyService: @@ -94,23 +109,89 @@ def collect_uf_definitions(node: Node) -> list(): uf_definitions.append(uf.definition) return uf_definitions + @staticmethod + def slice_uf_definitions(definitions: list, query: list) -> tuple[list, set[str]]: + """The definitions the query needs, and the uninterpreted functions it then contains. + + A definition is needed if it mentions a function the query or another needed definition + contains, or no function at all. The others only constrain functions that occur nowhere + else in the query; the executor gives every model call its own function, so each of them + can be satisfied by its function's value whatever the inputs, and leaving it out changes + neither satisfiability nor the inputs of any model. + """ + needed = set() + for smt in query: + needed |= declared_ufs(smt) + pending = [(d, declared_ufs(d)) for d in definitions] + sliced = [] + changed = True + while changed: + changed = False + rest = [] + for d, ufs in pending: + if not ufs or ufs & needed: + sliced.append(d) + needed |= ufs + changed = True + else: + rest.append((d, ufs)) + pending = rest + # Keep the order in which the executor recorded them. + order = {d: i for i, d in enumerate(definitions)} + sliced.sort(key=lambda d: order[d]) + return sliced, needed + + @staticmethod + def collect_query(node: Node) -> tuple[list, set[str]]: + """The constraints of the query for the unexplored side of the branch, besides its own + constraint, and the uninterpreted functions the query contains.""" + path_constraints = StrategyService.collect_path_constrains(node) + path_constraints.extend(StrategyService.collect_input_constrains(node)) + node_constraint = node.constraint.get(node.trace_id, '') + definitions, ufs = StrategyService.slice_uf_definitions( + StrategyService.collect_uf_definitions(node), path_constraints + [node_constraint]) + path_constraints.extend(definitions) + return path_constraints, ufs + + @staticmethod + def is_approximate(ufs) -> bool: + """Whether a query with these functions depends on an approximate Math model. Only a branch + constraint brings one in, and the executor reports such a trace as precision loss.""" + return any(uf.startswith(APPROXIMATE_UF_PREFIX) for uf in ufs) + + @staticmethod + def is_approximate_query(node: Node) -> bool: + """Whether the query for the unexplored side of the branch depends on an approximate Math model.""" + return StrategyService.is_approximate(StrategyService.collect_query(node)[1]) + @staticmethod def solve_branch(possible_branch: Node, endpoint_id=None, solver_timeout_ms: int | None = 60 * 1000, - solver_rlimit: int | None = None): + solver_rlimit: int | None = None, approximate_rlimit: int | None = None): """Solves for the unexplored side of the branch. LIMIT (the rlimit ran out) records nothing, - so the branch stays a candidate and can be retried with a larger limit.""" - db = Database.instance() + so the branch stays a candidate and can be retried with a larger limit. - path_constraints = StrategyService.collect_path_constrains(possible_branch) - - path_constraints.extend(StrategyService.collect_input_constrains(possible_branch)) + A query over an approximate Math model can only give a guess, and a branch whose search + depends on one never ends in SAFE (the executor reports precision loss). With + approximate_rlimit, such a query gets at most that resource limit, and running out of it is + UNKNOWN (given up), not LIMIT.""" + db = Database.instance() - path_constraints.extend(StrategyService.collect_uf_definitions(possible_branch)) + path_constraints, ufs = StrategyService.collect_query(possible_branch) inputs = possible_branch.inputs + capped = False + if approximate_rlimit and StrategyService.is_approximate(ufs): + if solver_rlimit is None or solver_rlimit >= approximate_rlimit: + solver_rlimit = approximate_rlimit + capped = True + sat, sol = Z3Handler.solve(possible_branch, path_constraints, timeout_ms=solver_timeout_ms, rlimit=solver_rlimit) + if sat == SATResult.LIMIT and capped: + logger.info(f'[SOLVER] Query over an approximate model for branch {possible_branch.id} ran out of resource limit {solver_rlimit}, giving up on it') + sat = SATResult.UNKNOWN + if sat == SATResult.SAT: db.add_solution(branch_id=possible_branch.gid, sol=sol, inputs=inputs, endpoint_id=endpoint_id) diff --git a/symbolic-explorer/tests/test_math_models.py b/symbolic-explorer/tests/test_math_models.py new file mode 100644 index 00000000..a39fea79 --- /dev/null +++ b/symbolic-explorer/tests/test_math_models.py @@ -0,0 +1,111 @@ +""" +Unit tests for the explorer side of the approximate Math models: definitions of model functions +are sliced to the ones a query needs, and a query over a model gets a bounded resource limit. + +Needs the explorer's dependencies, so run it with the harness venv, from symbolic-explorer/: + ../targets/sv-comp/scripts/.venv/bin/python3 -m unittest tests.test_math_models -v +""" + +import os +import sys +import unittest +from types import SimpleNamespace +from unittest import mock + +sys.path.insert(0, os.path.join(os.path.dirname(__file__), '..')) + +from solver.SolverHandler import SATResult +from strategy import StrategyService as ss +from strategy.StrategyService import StrategyService, declared_ufs + +FP = '(_ FloatingPoint 11 53)' +DECL_X = f'(declare-fun D_0 () {FP})' + + +def uf(name, arity=1): + return f'(declare-fun {name} ({" ".join([FP] * arity)}) {FP})' + + +def definition(name, arg='D_0', *nested): + return '\n'.join([DECL_X, *[uf(n) for n in nested], uf(name), f'(assert (= ({name} {arg}) (fp #b0 #b01111111111 #x0000000000000)))']) + + +def branch_on(name): + return '\n'.join([DECL_X, uf(name), f'(assert (fp.gt ({name} D_0) (fp #b0 #b00000000000 #x0000000000000)))']) + + +class DeclaredUfsTest(unittest.TestCase): + + def test_variables_are_not_functions(self): + self.assertEqual(declared_ufs(DECL_X), frozenset()) + self.assertEqual(declared_ufs(DECL_X + uf('math_tan_3') + uf('|math_pow_4|', 2)), {'math_tan_3', 'math_pow_4'}) + self.assertEqual(declared_ufs('(declare-fun toLowerCase (Int) Int)'), {'toLowerCase'}) + + +class SliceTest(unittest.TestCase): + + def test_unrelated_definitions_are_left_out(self): + tan, log = definition('math_tan_0'), definition('math_log_1') + sliced, ufs = StrategyService.slice_uf_definitions([tan, log], [branch_on('math_log_1')]) + self.assertEqual(sliced, [log]) + self.assertEqual(ufs, {'math_log_1'}) + + def test_nested_definitions_are_followed_in_order(self): + # math_pow_2's argument is math_log10_0(D_0); a query on math_pow_2 needs both. + inner = definition('math_log10_0') + outer = definition('math_pow_2', '(math_log10_0 D_0)', 'math_log10_0') + other = definition('math_tan_1') + sliced, ufs = StrategyService.slice_uf_definitions([inner, other, outer], [branch_on('math_pow_2')]) + self.assertEqual(sliced, [inner, outer]) + self.assertEqual(ufs, {'math_pow_2', 'math_log10_0'}) + + def test_constraints_without_functions_are_kept(self): + bound = f'{DECL_X}(assert (fp.lt D_0 (fp #b0 #b10000000000 #x0000000000000)))' + sliced, ufs = StrategyService.slice_uf_definitions([bound, definition('math_tan_0')], [DECL_X]) + self.assertEqual(sliced, [bound]) + self.assertEqual(ufs, set()) + + +class ApproximateLimitTest(unittest.TestCase): + + def solve(self, constraint, ufs, result, **kwargs): + node = SimpleNamespace(id=7, gid=7, trace_id='t', constraint={'t': constraint}, inputs=[], + ufs=[SimpleNamespace(definition=d) for d in ufs], parent=None) + db = mock.Mock() + with mock.patch.object(ss.Database, 'instance', return_value=db), \ + mock.patch.object(ss.Z3Handler, 'solve', return_value=(result, {})) as solve: + sat, _ = StrategyService.solve_branch(node, solver_timeout_ms=None, **kwargs) + return sat, solve.call_args.kwargs['rlimit'] + + def test_query_over_a_model_is_capped_and_given_up(self): + sat, rlimit = self.solve(branch_on('math_tan_0'), [definition('math_tan_0')], SATResult.LIMIT, + approximate_rlimit=100) + self.assertEqual((sat, rlimit), (SATResult.UNKNOWN, 100)) + + def test_smaller_base_limit_still_escalates(self): + sat, rlimit = self.solve(branch_on('math_tan_0'), [definition('math_tan_0')], SATResult.LIMIT, + solver_rlimit=10, approximate_rlimit=100) + self.assertEqual((sat, rlimit), (SATResult.LIMIT, 10)) + + def test_exact_query_is_not_capped(self): + # The trace has a model call, but this branch does not depend on it. + sat, rlimit = self.solve(f'{DECL_X}(assert (fp.isZero D_0))', [definition('math_tan_0')], SATResult.UNSAT, + approximate_rlimit=100) + self.assertEqual((sat, rlimit), (SATResult.UNSAT, None)) + + +class ModelValuesTest(unittest.TestCase): + + def test_model_functions_are_not_inputs(self): + from z3 import Solver, FP, Float64, Function, fpLT, FPVal, sat + from solver.SolverHandler import Z3Handler + x = FP('D_0', Float64()) + f = Function('math_tan_0', Float64(), Float64()) + s = Solver() + s.add(fpLT(FPVal(1.0, Float64()), f(x)), fpLT(x, FPVal(2.0, Float64()))) + self.assertEqual(s.check(), sat) + self.assertEqual(set(Z3Handler.extract_and_encode_values(s.model())), {'D_0'}) + + +if __name__ == '__main__': + unittest.main() diff --git a/symbolic-explorer/tests/test_solver_rlimit.py b/symbolic-explorer/tests/test_solver_rlimit.py index 288d0e7f..5e7bfcc9 100644 --- a/symbolic-explorer/tests/test_solver_rlimit.py +++ b/symbolic-explorer/tests/test_solver_rlimit.py @@ -30,7 +30,7 @@ class FakeSolver: def __init__(self, needed, results): self.needed, self.results, self.calls = needed, results, [] - def __call__(self, b, solver_timeout_ms=None, solver_rlimit=None): + def __call__(self, b, solver_timeout_ms=None, solver_rlimit=None, approximate_rlimit=None): self.calls.append((b.gid, solver_rlimit)) if solver_rlimit is not None and solver_rlimit < self.needed.get(b.gid, 0): return SATResult.LIMIT, {}