Decide precision loss by symbol kind instead of by variable name

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) {

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<Double>(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;
     }

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

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<String> inputNames = new HashSet<>();
-        for (InputElement ie : symbolicTrace.getInputs()) {
-            inputNames.add(ie.getName());
-        }
-        java.util.function.Predicate<String> 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<String> 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));
     }

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.
+ *
+ * <p>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<String, Kind> 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;
+    }
+}

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);
     }
 
     /**

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

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 <prefix>_<idx>}): an input array of the same
+     * prefix and index would otherwise share, and constrain, the allocated array's contents.
+     */
+    protected static <I extends Formula, E extends Formula> ArrayFormula<I, E> makeBaseArray(
+            ArrayFormulaManager amgr, String symbolicPrefix, FormulaType.ArrayFormulaType<I, E> 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.
      *

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();

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<NumeralFormula.IntegerFormula> 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<NumeralFormula.IntegerFormula> 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<NumeralFormula.IntegerFormula> loUF = ufmgr.declareUF("trimStart", FormulaType.IntegerType, FormulaType.StringType);
         FunctionDeclaration<NumeralFormula.IntegerFormula> 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);