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); } 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") + } +}