From f55b477adf2418c9bf10acc2794752b384c1c24f Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:38:56 +0000 Subject: [PATCH 1/2] Decide precision loss by symbol kind instead of by name DTOBuilder flagged a branch constraint as imprecise when one of its symbols did not match the name pattern [A-Z].*_[0-9].*. Array base symbols ([I_0) and the exact UFs of the String models (trimStart, trimEnd, commonPrefixLength, lastIndexOf) failed it, so SAFE was downgraded for constraints that are encoded exactly. Symbols are now declared with their kind where they are created (SymbolRegistry): inputs, other symbolic values, array base symbols, exact model functions and approximate model functions. A constraint is imprecise if it mentions an approximate model function or a symbol nobody declared. Array base symbols get their own namespace (_alloc), so an input array of the same prefix and index cannot share them. lastIndexOf(int) with a symbolic char records precision loss: chars outside the BMP, and negative ones, are not modelled. Co-Authored-By: Claude Opus 5.5 --- .../its/swat/symbolic/trace/DTOBuilder.java | 46 +++---- .../swat/symbolic/trace/SymbolRegistry.java | 57 +++++++++ .../symbolic/trace/SymbolicTraceHandler.java | 1 + .../de/uzl/its/swat/symbolic/value/Value.java | 5 + .../reference/array/AbstractArrayValue.java | 17 ++- .../reference/array/ArrayArrayValue.java | 3 +- .../value/reference/lang/StringValue.java | 18 ++- .../symbolic/trace/SymbolRegistrySpec.groovy | 116 ++++++++++++++++++ 8 files changed, 235 insertions(+), 28 deletions(-) create mode 100644 symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolRegistry.java create mode 100644 symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/trace/SymbolRegistrySpec.groovy diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java index e272cf71..2a80c35d 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/DTOBuilder.java @@ -102,15 +102,8 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage ufs.add(new UFDTO(formula)); } logger.trace("Parsing constraints..."); - // A constraint over anything but the inputs (e.g. an uninterpreted function) means the - // model is approximate. Input names usually match the pattern below, but String inputs - // (java/lang/String_0) do not, so they are accepted by name. - Set inputNames = new HashSet<>(); - for (InputElement ie : symbolicTrace.getInputs()) { - inputNames.add(ie.getName()); - } - java.util.function.Predicate isInput = - name -> inputNames.contains(name) || name.matches("[A-Z].*_[0-9].*"); + // A constraint over an approximate model function, or over a symbol no model declared, + // means the encoding may be imprecise (see SymbolRegistry). boolean symbolicPrecisionLoss = symbolicTrace.isSymbolicPrecisionLoss(); for (Element el : symbolicTrace.getTrace()) { if (el instanceof BranchElement be) { @@ -122,25 +115,13 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage constraint = "(assert true)"; } else { constraint = String.valueOf(fmgr.dumpFormula(f)); - if (!fmgr.extractVariablesAndUFs(f).isEmpty() && - !fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(isInput)) { - symbolicPrecisionLoss = true; - } + symbolicPrecisionLoss |= hasImpreciseSymbol(fmgr, f); } - //fmgr.extractVariablesAndUFs(f).keySet().forEach(System.out::println); - // assert fmgr.extractVariablesAndUFs(f).keySet().stream() - // .allMatch(s -> s.matches("[A-Z].*_[0-9].*")): "[SWAT] UF introduced in: " + constraint; - } catch (InterruptedException e) { BooleanFormula f = be.getConstraint(); logger.warn("Error while simplifying formula", e); constraint = String.valueOf(fmgr.dumpFormula(f)); - //fmgr.extractVariablesAndUFs(f).keySet().forEach(System.out::println); - // assert fmgr.extractVariablesAndUFs(f).keySet().stream() - // .allMatch(s -> s.matches("[A-Z].*_[0-9].*")): "[SWAT] UF introduced in: " + constraint; - if (!fmgr.extractVariablesAndUFs(f).keySet().stream().allMatch(isInput)) { - symbolicPrecisionLoss = true; - } + symbolicPrecisionLoss |= hasImpreciseSymbol(fmgr, f); } trace.add(new BranchDTO(be.getIid(), constraint, be.isBranched(), be.isConcreteOnly()) .place(be.getKey(), be.getPops(), be.getPushes(), be.isCallback())); @@ -152,6 +133,25 @@ private static TraceDTO buildTraceDTO(SymbolicTrace symbolicTrace, StatsStorage symbolicTrace.isSymbolicPrecisionLoss()); } + /** Symbols already reported as undeclared, so each is logged once. */ + private static final Set reportedUndeclared = java.util.concurrent.ConcurrentHashMap.newKeySet(); + + /** + * Whether the formula mentions a symbol whose constraints are not encoded precisely: an + * approximate model function, or a symbol that was never declared in the {@link SymbolRegistry}. + */ + static boolean hasImpreciseSymbol(FormulaManager fmgr, Formula f) { + boolean imprecise = false; + for (String name : fmgr.extractVariablesAndUFs(f).keySet()) { + if (SymbolRegistry.isPrecise(name)) continue; + if (SymbolRegistry.kindOf(name) == null && reportedUndeclared.add(name)) { + logger.warn("Undeclared symbol {} in a branch constraint; treating it as imprecise", name); + } + imprecise = true; + } + return imprecise; + } + protected static String encodeCoverage(InstrCoverage instrCoverage) throws JsonProcessingException { return buildRequestBody(buildInstrCoverageDTO(instrCoverage)); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolRegistry.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolRegistry.java new file mode 100644 index 00000000..4191fdd1 --- /dev/null +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolRegistry.java @@ -0,0 +1,57 @@ +package de.uzl.its.swat.symbolic.trace; + +import java.util.Map; +import java.util.concurrent.ConcurrentHashMap; + +/** + * Records, where a symbol is declared, what kind of symbol it is. The {@link DTOBuilder} uses it + * to decide whether a branch constraint is encoded precisely: a constraint over a symbol that is + * approximate, or that was never declared here, is a precision loss. + * + *

A precise symbol may still be under-constrained (a fresh value, an array base outside the + * stored range, a partially defined model function). That only over-approximates: an UNSAT query + * stays a proof, and a guessed model that does not reach its branch is caught as a divergence. + * A model whose constraints may exclude real behaviour must be declared {@link + * Kind#APPROXIMATE_MODEL_FUNCTION}, and must also call {@link + * SymbolicTraceHandler#recordSymbolicPrecisionLoss()} where it adds such a constraint, since the + * constraint reaches every query whether or not a branch mentions the function. + */ +public final class SymbolRegistry { + + public enum Kind { + /** A Verifier input, solved for by the explorer. */ + INPUT, + /** A symbolic value of the program that is not an input (e.g. a havocked field). */ + VALUE, + /** The base symbol of an allocated array, overwritten by its initial contents. */ + ARRAY_BASE, + /** A model function whose definition holds for every argument. */ + MODEL_FUNCTION, + /** A model function whose encoding may exclude real behaviour. */ + APPROXIMATE_MODEL_FUNCTION + } + + private static final Map kinds = new ConcurrentHashMap<>(); + + private SymbolRegistry() {} + + /** + * Declares the kind of a symbol. An input stays an input; an approximate model function stays + * approximate. + */ + public static void declare(String name, Kind kind) { + kinds.merge(name, kind, (old, k) -> + old == Kind.INPUT || old == Kind.APPROXIMATE_MODEL_FUNCTION ? old : k); + } + + /** Returns the kind of the symbol, or null if it was never declared. */ + public static Kind kindOf(String name) { + return kinds.get(name); + } + + /** Whether constraints over the symbol are encoded precisely (see the class comment). */ + public static boolean isPrecise(String name) { + Kind kind = kinds.get(name); + return kind != null && kind != Kind.APPROXIMATE_MODEL_FUNCTION; + } +} diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java index d8e1b62c..ed18a20b 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/trace/SymbolicTraceHandler.java @@ -129,6 +129,7 @@ public void recordInvocation(long iid, String inst) { public void addInput(String name, Value value) { logger.info("Input with name: {} and value: {} registered", name, value); symbolicTrace.addInputElement(new InputElement(name, value)); + SymbolRegistry.declare(name, SymbolRegistry.Kind.INPUT); } /** diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/Value.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/Value.java index 09ab749e..d0a17b03 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/Value.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/Value.java @@ -7,6 +7,7 @@ import de.uzl.its.swat.common.exceptions.SWATAssert; import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.common.logging.GlobalLogger; +import de.uzl.its.swat.symbolic.trace.SymbolRegistry; 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,19 +70,23 @@ protected void initSymbolic(String namePrefix) { SWATAssert.enforce(namePrefix != null, "Name prefix cannot be null"); name = namePrefix + "_" + symbol; symbol = symbol + inc; + SymbolRegistry.declare(name, SymbolRegistry.Kind.VALUE); } //Todo: this is a hotfix... protected void initSymbolicWithoutIdx(String symbolicName) { SWATAssert.enforce(symbolicName != null, "Name prefix cannot be null"); name = symbolicName; + SymbolRegistry.declare(name, SymbolRegistry.Kind.VALUE); } protected void initSymbolic(String namePrefix, long idx) { name = namePrefix + "_" + idx; + SymbolRegistry.declare(name, SymbolRegistry.Kind.VALUE); } protected void initSymbolic(String namePrefix, String idx) { name = namePrefix + "_" + idx; + SymbolRegistry.declare(name, SymbolRegistry.Kind.VALUE); } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java index 361c8f06..10841604 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/AbstractArrayValue.java @@ -4,6 +4,7 @@ import de.uzl.its.swat.common.exceptions.NotImplementedException; import de.uzl.its.swat.common.exceptions.NotSupportedException; import de.uzl.its.swat.config.Config; +import de.uzl.its.swat.symbolic.trace.SymbolRegistry; import de.uzl.its.swat.symbolic.value.Value; import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue; import de.uzl.its.swat.symbolic.value.reference.ObjectValue; @@ -60,12 +61,11 @@ public AbstractArrayValue( super(context, address); this.context = context; this.amgr = context.getFormulaManager().getArrayFormulaManager(); - Value.symbol = Value.symbol + Value.inc; this.indexFormulaType = indexFormulaType; this.elementFormulaType = elementFormulaType; formulaType = FormulaType.getArrayType(indexFormulaType, elementFormulaType); - this.formula = amgr.makeArray(symbolicPrefix + "_" + (Value.symbol - Value.inc), formulaType); + this.formula = makeBaseArray(amgr, symbolicPrefix, formulaType); this.size = size; this.parentRefIdx = null; this.parentRef = null; @@ -88,6 +88,19 @@ public AbstractArrayValue( this.size = size; } + /** + * Creates the base symbol of an allocated array, which its initial contents are stored over. + * Its name is outside the input namespace ({@code _}): an input array of the same + * prefix and index would otherwise share, and constrain, the allocated array's contents. + */ + protected static ArrayFormula makeBaseArray( + ArrayFormulaManager amgr, String symbolicPrefix, FormulaType.ArrayFormulaType type) { + String name = symbolicPrefix + "_alloc" + Value.symbol; + Value.symbol = Value.symbol + Value.inc; + SymbolRegistry.declare(name, SymbolRegistry.Kind.ARRAY_BASE); + return amgr.makeArray(name, type); + } + /** * Returns the default value for the type of array. * diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ArrayArrayValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ArrayArrayValue.java index 1b03526f..2a6847a8 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ArrayArrayValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/array/ArrayArrayValue.java @@ -46,8 +46,7 @@ public ArrayArrayValue( } this.dims = dims; this.desc = desc; - Value.symbol = Value.symbol + Value.inc; - this.formula = amgr.makeArray("A_" + (Value.symbol - Value.inc), formulaType); + this.formula = makeBaseArray(amgr, "A", formulaType); this.parentRefIdx = parentRefIdx; this.parentRef = parentRef; initSymbolicArray(); diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java index b273156a..5bcac052 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/value/reference/lang/StringValue.java @@ -6,6 +6,7 @@ import de.uzl.its.swat.common.exceptions.ValueConversionException; import de.uzl.its.swat.config.Config; import de.uzl.its.swat.symbolic.UFs.EqualsIgnoreCaseUF; +import de.uzl.its.swat.symbolic.trace.SymbolRegistry; import de.uzl.its.swat.symbolic.value.PlaceHolder; import de.uzl.its.swat.symbolic.value.Value; import de.uzl.its.swat.symbolic.value.VoidValue; @@ -356,6 +357,7 @@ public BooleanFormula getBounds(boolean upper) { // prefixes up to k agree, and k is the end of one string or the chars at k differ. FunctionDeclaration lcp = context.getFormulaManager().getUFManager() .declareUF("commonPrefixLength", FormulaType.IntegerType, FormulaType.StringType, FormulaType.StringType); + SymbolRegistry.declare("commonPrefixLength", SymbolRegistry.Kind.MODEL_FUNCTION); NumeralFormula.IntegerFormula k = context.getFormulaManager().getUFManager().callUF(lcp, formula, other.formula); BooleanFormula kInsideBoth = bmgr.and(imgr.lessThan(k, len), imgr.lessThan(k, otherLen)); addDefinition(bmgr.and( @@ -371,6 +373,15 @@ public BooleanFormula getBounds(boolean upper) { return new IntValue(context, result, cmp); } + /** Records that a model is only approximate, so an exhausted search proves nothing. */ + private static void recordPrecisionLoss() { + try { + ThreadHandler.getSymbolicTraceHandler(currentThread().getId()).recordSymbolicPrecisionLoss(); + } catch (Exception e) { + throw new IllegalStateException("No symbolic trace handler for the current thread", e); + } + } + /** Adds a constraint that defines the UFs a model introduced; it holds on every path and is never negated. */ private static void addDefinition(BooleanFormula definition) { try { @@ -775,11 +786,13 @@ private static void addDefinition(BooleanFormula definition) { if (desc[0].getSort() == Type.INT) { IntValue ch = args[0].asIntValue(); // Supplementary code points are two chars in a Java string but one in the solver's, so - // only BMP chars are modelled exactly (the UF below flags the result as imprecise anyway). + // only BMP chars are modelled exactly. A symbolic char may leave that range (and a + // negative one becomes the empty string), so the model is then approximate. if (ch.concrete < 0 || ch.concrete > Character.MAX_VALUE) return PlaceHolder.instance; target = new StringValue(context, String.valueOf((char) (int) ch.concrete), smgr.fromCodePoint(ch.asIntegerFormula()), -1); result = concrete.lastIndexOf(ch.concrete, from.concrete); + if (ch.isSymbolic()) recordPrecisionLoss(); } else if (args[0] instanceof StringValue str) { target = str; result = concrete.lastIndexOf(str.concrete, from.concrete); @@ -796,6 +809,7 @@ private static void addDefinition(BooleanFormula definition) { NumeralFormula.IntegerFormula last = bmgr.ifThenElse(imgr.lessThan(fromF, maxStart), fromF, maxStart); FunctionDeclaration uf = ufmgr.declareUF("lastIndexOf", FormulaType.IntegerType, FormulaType.StringType, FormulaType.StringType, FormulaType.IntegerType); + SymbolRegistry.declare("lastIndexOf", SymbolRegistry.Kind.MODEL_FUNCTION); NumeralFormula.IntegerFormula r = ufmgr.callUF(uf, formula, target.formula, last); // Matches starting at or before `last` are the occurrences of target in the window s[0, last + tlen). // (Encoded with contains rather than indexOf, which Z3 solves much faster.) @@ -1332,6 +1346,8 @@ private static void addDefinition(BooleanFormula definition) { // being made of chars <= ' ' only, and by the kept part, if any, not starting or ending in one. FunctionDeclaration loUF = ufmgr.declareUF("trimStart", FormulaType.IntegerType, FormulaType.StringType); FunctionDeclaration hiUF = ufmgr.declareUF("trimEnd", FormulaType.IntegerType, FormulaType.StringType); + SymbolRegistry.declare("trimStart", SymbolRegistry.Kind.MODEL_FUNCTION); + SymbolRegistry.declare("trimEnd", SymbolRegistry.Kind.MODEL_FUNCTION); NumeralFormula.IntegerFormula lo = ufmgr.callUF(loUF, formula); NumeralFormula.IntegerFormula hi = ufmgr.callUF(hiUF, formula); NumeralFormula.IntegerFormula len = smgr.length(formula); diff --git a/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/trace/SymbolRegistrySpec.groovy b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/trace/SymbolRegistrySpec.groovy new file mode 100644 index 00000000..3fd63b8c --- /dev/null +++ b/symbolic-executor/src/test/groovy/de/uzl/its/swat/symbolic/trace/SymbolRegistrySpec.groovy @@ -0,0 +1,116 @@ +package de.uzl.its.swat.symbolic.trace + +import de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue +import de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue +import de.uzl.its.swat.symbolic.value.reference.array.IntArrayValue +import de.uzl.its.swat.symbolic.value.reference.lang.StringValue +import de.uzl.its.swat.thread.ThreadHandler +import org.objectweb.asm.Type +import org.sosy_lab.java_smt.api.FormulaManager +import org.sosy_lab.java_smt.api.FormulaType +import org.sosy_lab.java_smt.api.SolverContext +import spock.lang.Specification + +import static java.lang.Thread.currentThread + +class SymbolRegistrySpec extends Specification { + + SolverContext context + FormulaManager fmgr + + def setup() { + ThreadHandler.init() + if (ThreadHandler.hasThreadContext(currentThread().id)) { + ThreadHandler.removeThreadContext(currentThread().id) + } + ThreadHandler.addThreadContext(currentThread().id, "Test-Thread", -2) + context = ThreadHandler.getSolverContext(currentThread().id) + fmgr = context.formulaManager + } + + def cleanup() { + context.close() + ThreadHandler.removeThreadContext(currentThread().id) + } + + private boolean tracePrecisionLoss() { + ThreadHandler.getSymbolicTraceHandler(currentThread().id).symbolicTrace.symbolicPrecisionLoss + } + + def "an input and an allocated array's base symbol are precise"() { + given: + IntValue i = new IntValue(context, 1) + String name = i.MAKE_SYMBOLIC(7L) + ThreadHandler.getSymbolicTraceHandler(currentThread().id).addInput(name, i) + IntArrayValue arr = new IntArrayValue(context, new IntValue(context, 3), 1) + + when: + def read = arr.getElement(i) + def f = fmgr.bitvectorFormulaManager.equal(read.formula, fmgr.bitvectorFormulaManager.makeBitvector(32, 0)) + def base = fmgr.extractVariables(arr.formula).keySet() + + then: + SymbolRegistry.kindOf(name) == SymbolRegistry.Kind.INPUT + base.size() == 1 + SymbolRegistry.kindOf(base[0]) == SymbolRegistry.Kind.ARRAY_BASE + // outside the input namespace, so an input array [I_ cannot share it + !(base[0] ==~ /\[I_\d+/) + !DTOBuilder.hasImpreciseSymbol(fmgr, f) + } + + def "an exact String model function is precise"() { + given: + StringValue s = new StringValue(context, " a ", 1) + s.MAKE_SYMBOLIC(3L) + + when: + StringValue t = s.invokeMethod("trim", [] as Type[], [] as IntValue[]) as StringValue + def f = fmgr.stringFormulaManager.equal(t.formula, fmgr.stringFormulaManager.makeString("a")) + + then: + fmgr.extractVariablesAndUFs(f).keySet().containsAll(["trimStart", "trimEnd"]) + !DTOBuilder.hasImpreciseSymbol(fmgr, f) + !tracePrecisionLoss() + } + + def "an approximate model function is a precision loss"() { + given: + DoubleValue d = new DoubleValue(context, 0.5d) + d.MAKE_SYMBOLIC(4L) + + when: + def sin = ThreadHandler.getUFHandler(currentThread().id).getSinCosUF().applySin(d.formula) + def f = fmgr.floatingPointFormulaManager.lessThan(sin, fmgr.floatingPointFormulaManager.makeNumber(0.1d, DoubleValue.precision)) + + then: + SymbolRegistry.kindOf("sin") == SymbolRegistry.Kind.APPROXIMATE_MODEL_FUNCTION + DTOBuilder.hasImpreciseSymbol(fmgr, f) + tracePrecisionLoss() + } + + def "an undeclared function is a precision loss"() { + given: + def uf = fmgr.UFManager.declareUF("someUndeclaredFunction", FormulaType.IntegerType, FormulaType.IntegerType) + IntValue i = new IntValue(context, 1) + i.MAKE_SYMBOLIC(5L) + + when: + def call = fmgr.UFManager.callUF(uf, i.asIntegerFormula()) + def f = fmgr.integerFormulaManager.equal(call, fmgr.integerFormulaManager.makeNumber(0)) + + then: + DTOBuilder.hasImpreciseSymbol(fmgr, f) + } + + def "an input or approximate declaration is not weakened by a later one"() { + when: + SymbolRegistry.declare("Spec_input_0", SymbolRegistry.Kind.INPUT) + SymbolRegistry.declare("Spec_input_0", SymbolRegistry.Kind.VALUE) + SymbolRegistry.declare("specApprox", SymbolRegistry.Kind.APPROXIMATE_MODEL_FUNCTION) + SymbolRegistry.declare("specApprox", SymbolRegistry.Kind.MODEL_FUNCTION) + + then: + SymbolRegistry.kindOf("Spec_input_0") == SymbolRegistry.Kind.INPUT + !SymbolRegistry.isPrecise("specApprox") + } +} From db4cd1efb8b327d545c056459ff3df33818e4754 Mon Sep 17 00:00:00 2001 From: Nils Loose Date: Sun, 18 Oct 2026 21:38:56 +0000 Subject: [PATCH 2/2] Declare the approximate UF models and record their precision loss sin/cos, toLowerCase and equalsIgnoreCase are approximate model functions. sin/cos restrict their argument to the sample points, and the guarded toLowerCase restricts chars to printable ASCII. Both constraints reach every query, so they record precision loss where they are added, not only when a branch mentions the function. Co-Authored-By: Claude Opus 5.5 --- .../de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java | 2 ++ .../src/main/java/de/uzl/its/swat/symbolic/UFs/SinCosUF.java | 5 +++++ .../java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java | 4 ++++ 3 files changed, 11 insertions(+) diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java index a49cb167..5b7a7728 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/EqualsIgnoreCaseUF.java @@ -1,6 +1,7 @@ package de.uzl.its.swat.symbolic.UFs; import de.uzl.its.swat.common.exceptions.NoThreadContextException; +import de.uzl.its.swat.symbolic.trace.SymbolRegistry; import org.sosy_lab.java_smt.api.*; import java.util.ArrayList; @@ -32,6 +33,7 @@ public EqualsIgnoreCaseUF(SolverContext ctx) throws NoThreadContextException { FormulaType.BooleanType, FormulaType.StringType, FormulaType.StringType); + SymbolRegistry.declare("equalsIgnoreCase", SymbolRegistry.Kind.APPROXIMATE_MODEL_FUNCTION); } public BooleanFormula getUFCall(StringFormula s1, StringFormula s2) { 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 index 5422a5a2..8f0151b5 100644 --- 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 @@ -2,6 +2,7 @@ import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; +import de.uzl.its.swat.symbolic.trace.SymbolRegistry; import de.uzl.its.swat.thread.ThreadHandler; import java.util.ArrayList; import java.util.Arrays; @@ -28,6 +29,8 @@ public SinCosUF(SolverContext ctx) throws NoThreadContextException { sinUF = ufmgr.declareUF("sin", DoubleType, DoubleType); cosUF = ufmgr.declareUF("cos", DoubleType, DoubleType); + SymbolRegistry.declare("sin", SymbolRegistry.Kind.APPROXIMATE_MODEL_FUNCTION); + SymbolRegistry.declare("cos", SymbolRegistry.Kind.APPROXIMATE_MODEL_FUNCTION); final double PI = Math.PI; inputValues = new ArrayList(Arrays.asList( @@ -70,6 +73,7 @@ public FloatingPointFormula applySin(FloatingPointFormula symIn) throws NoThread sth.addConstraint( bmgr.or(inputValues.stream().map(v -> fmgr.equalWithFPSemantics(symIn, fmgr.makeNumber(v, DoubleType))) .collect(Collectors.toList()))); + sth.recordSymbolicPrecisionLoss(); return symOut; } @@ -88,6 +92,7 @@ public FloatingPointFormula applyCos(FloatingPointFormula symIn) throws NoThread sth.addConstraint( bmgr.or(inputValues.stream().map(v -> fmgr.equalWithFPSemantics(symIn, fmgr.makeNumber(v, DoubleType))) .collect(Collectors.toList()))); + sth.recordSymbolicPrecisionLoss(); return symOut; } diff --git a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java index cb197486..664b00b6 100644 --- a/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java +++ b/symbolic-executor/src/main/java/de/uzl/its/swat/symbolic/UFs/ToLowerCaseUF.java @@ -2,6 +2,7 @@ import de.uzl.its.swat.common.exceptions.NoThreadContextException; import de.uzl.its.swat.symbolic.trace.SymbolicTraceHandler; +import de.uzl.its.swat.symbolic.trace.SymbolRegistry; import de.uzl.its.swat.thread.ThreadHandler; import edu.umd.cs.findbugs.annotations.Nullable; import org.sosy_lab.java_smt.api.*; @@ -20,6 +21,7 @@ public ToLowerCaseUF(SolverContext ctx) throws NoThreadContextException { bmgr = fmgr.getBooleanFormulaManager(); toLowerUF = ufmgr.declareUF("toLowerCase", FormulaType.IntegerType, FormulaType.IntegerType); + SymbolRegistry.declare("toLowerCase", SymbolRegistry.Kind.APPROXIMATE_MODEL_FUNCTION); // A..Z -> a..z for (int c = 'A'; c <= 'Z'; c++) { @@ -49,6 +51,8 @@ public NumeralFormula.IntegerFormula applyToLower( imgr.greaterOrEquals(charCode, imgr.makeNumber(32)), imgr.lessOrEquals(charCode, imgr.makeNumber(126))); sth.addConstraint(bmgr.implication(guard, inAscii)); + // Restricting the chars to printable ASCII excludes real inputs. + sth.recordSymbolicPrecisionLoss(); } return ufmgr.callUF(toLowerUF, charCode); }