Drop true binders the error does not need and write fields as in code

liquidjava-example/src/main/java/testSuite/classes/found_binders_error/ArrayListRefinements.java

@@ -0,0 +1,15 @@
+package testSuite.classes.found_binders_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@Ghost("int size")
+public interface ArrayListRefinements<E> {
+
+    public void ArrayList();
+
+    @Refinement("_ == size(this) && _ >= 0")
+    public int size();
+}

liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java

@@ -0,0 +1,58 @@
+package testSuite.classes.found_binders_error;
+
+import java.util.ArrayList;
+import java.util.Random;
+
+import liquidjava.specification.Refinement;
+
+// Found drops the true rows the error does not need and writes fields as in code (#457)
+public class Basket {
+    static int served;
+
+    @Refinement("_ >= 0")
+    int level;
+
+    private final ArrayList<String> items;
+    private final Random random = new Random();
+
+    Basket(ArrayList<String> items) {
+        this.items = items;
+    }
+
+    // the issue's reproducer: the field row only says true
+    String pick() {
+        ArrayList<String> items = this.items;
+        return items.get(random.nextInt(items.size())); // Expect: Refinement Error
+    }
+
+    // a static field
+    void serve() {
+        @Refinement("_ > 0")
+        int count = served + 1; // Expect: Refinement Error
+    }
+
+    // writes to another object's field are checked as on main, and named after that object
+    void setOther(Basket other) {
+        other.level = -1; // Expect: Refinement Error
+    }
+
+    void incrementOther(Basket other) {
+        other.level++;
+    }
+
+    void addToOther(Basket other) {
+        other.level += 1;
+    }
+
+    void decrementOther(Basket other) {
+        other.level--; // Expect: Refinement Error
+    }
+
+    void writeThroughAlias() {
+        level = 7;
+        Basket other = this;
+        other.level = 3;
+        @Refinement("_ == 7")
+        int k = level; // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/found_binders_error/RandomRefinements.java

@@ -0,0 +1,12 @@
+package testSuite.classes.found_binders_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Refinement;
+
+@ExternalRefinementsFor("java.util.Random")
+public interface RandomRefinements {
+
+    public void Random();
+
+    public int nextInt(@Refinement("bound > 0") int bound);
+}

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

@@ -9,6 +9,7 @@
 import liquidjava.diagnostics.warnings.CustomWarning;
 import liquidjava.processor.RefinementProcessor;
 import liquidjava.processor.context.ContextHistory;
+import liquidjava.rj_language.ast.formatter.FieldDisplayNames;
 import liquidjava.specification.Refinement;
 import picocli.CommandLine;
 import spoon.Launcher;
@@ -57,6 +58,7 @@ public static void launch(String... paths) {
 
         diagnostics.clear();
         contextHistory.clearHistory();
+        FieldDisplayNames.clear();
         Launcher launcher = new Launcher();
         for (String path : paths) {
             if (!new File(path).exists()) {

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -3,6 +3,7 @@
 import java.util.Objects;
 
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.opt.NeededVariables;
 import liquidjava.rj_language.opt.VCSimplification;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.utils.Utils;
@@ -79,6 +80,10 @@ public VCSimplificationResult simplify() {
         return VCSimplification.simplifyToFixedPoint(this);
     }
 
+    public VCSimplificationResult simplify(NeededVariables needed) {
+        return VCSimplification.simplifyToFixedPoint(this, needed);
+    }
+
     public Predicate toPredicate() {
         return hasBinder() || hasNext() ? toConjunctions() : refinement;
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -23,6 +23,7 @@
 import liquidjava.processor.state_machine.StateMachineBuilder;
 import liquidjava.processor.state_machine.StateSolver;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.formatter.FieldDisplayNames;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
@@ -382,6 +383,8 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
         Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName);
 
         String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
+        Utils.untrackedWriteReceiver(usage)
+                .ifPresent(receiver -> FieldDisplayNames.recordWriteReceiver(newName, receiver));
         Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
         correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
         cEt = cEt.substituteVariable(simpleName, newName);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -20,6 +20,7 @@
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.opt.NeededVariables;
 import liquidjava.smt.Counterexample;
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
@@ -83,7 +84,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         DebugLog.smtResult(result);
         if (result.isError()) {
             throw new RefinementError(element.getPosition(), declarationPosition, expectedType,
-                    implBeforeChange.simplify(), map, result.getCounterexample(), customMessage);
+                    implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map,
+                    result.getCounterexample(), customMessage);
         }
     }
 
@@ -442,17 +444,18 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl
             Predicate found, Counterexample counterexample, String customMessage) throws RefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication premises = buildPremiseChain(map, expected, found);
-        throw new RefinementError(position, declarationPosition, expected, premises.simplify(), map, counterexample,
-                customMessage);
+        throw new RefinementError(position, declarationPosition, expected,
+                premises.simplify(NeededVariables.forRefinementError(expected)), map, counterexample, customMessage);
     }
 
     protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,
             Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
             StateErrorContext context) throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
-        throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map,
-                customMessage, hints, category, context);
+        throw new StateRefinementError(position, declarationPosition, expected,
+                foundState.simplify(NeededVariables.forStateError(expected)), map, customMessage, hints, category,
+                context);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java

@@ -22,6 +22,9 @@ public static ExpressionNameResolver forExpression(Expression expression) {
 
     public String resolveVariable(String name) {
         String formatted = VariableFormatter.format(name);
+        // a field is always written as in code, as its binder and the counterexample write it
+        if (VariableFormatter.isField(name))
+            return formatted;
         return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted
                 : Utils.getSimpleName(formatted);
     }

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/FieldDisplayNames.java

@@ -0,0 +1,51 @@
+package liquidjava.rj_language.ast.formatter;
+
+import java.util.Map;
+import java.util.Set;
+import java.util.concurrent.ConcurrentHashMap;
+
+/**
+ * What a verification learns about field names that their internal form does not say, so that {@link VariableFormatter}
+ * can write them as in code: which fields are static, and which field instances were created by a write through another
+ * object. Filled during a verification and cleared when the next one starts
+ */
+public final class FieldDisplayNames {
+    private static final Set<String> STATIC_FIELDS = ConcurrentHashMap.newKeySet();
+    private static final Map<String, String> WRITE_RECEIVERS = new ConcurrentHashMap<>();
+
+    private FieldDisplayNames() {
+    }
+
+    /**
+     * Records that a field name ({@code this#<declaring type>.<field>}) belongs to a static field, written
+     * {@code Class.field}
+     */
+    public static void recordStaticField(String name) {
+        STATIC_FIELDS.add(name);
+    }
+
+    /**
+     * Records that a field instance ({@code #this#<declaring type>.<field>_<n>}) was created by a write through
+     * {@code receiver} ({@code receiver.field = v}), written {@code receiver.field}; an empty receiver writes the bare
+     * field name. Only the display changes
+     */
+    public static void recordWriteReceiver(String instanceName, String receiver) {
+        WRITE_RECEIVERS.put(instanceName, receiver);
+    }
+
+    /**
+     * Forgets what the previous verification recorded
+     */
+    public static void clear() {
+        STATIC_FIELDS.clear();
+        WRITE_RECEIVERS.clear();
+    }
+
+    static boolean isStaticField(String name) {
+        return STATIC_FIELDS.contains(name);
+    }
+
+    static String writeReceiver(String instanceName) {
+        return WRITE_RECEIVERS.get(instanceName);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java

@@ -8,6 +8,8 @@
  */
 public final class VariableFormatter {
     private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$");
+    // this#<declaring type>.<field>
+    private static final Pattern FIELD_PATTERN = Pattern.compile("^this#([\\w.$]+)\\.([\\w$]+)$");
     private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' };
 
     public static String format(String name) {
@@ -19,19 +21,54 @@ public static String format(String name) {
 
         Matcher matcher = INSTACE_VAR_PATTERN.matcher(name);
         if (!matcher.matches())
-            return name;
+            return formatField(name);
 
         String baseName = matcher.group(1);
         String counter = matcher.group(2);
+        String receiver = FieldDisplayNames.writeReceiver(name);
+        if (receiver != null && isField(baseName))
+            return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter);
         String prefix = isSpecialIdentifier(baseName) ? "#" : "";
-        return prefix + baseName + toSuperscript(counter);
+        return prefix + formatField(baseName) + toSuperscript(counter);
     }
 
     public static String withoutInstance(String name) {
         Matcher matcher = INSTACE_VAR_PATTERN.matcher(name);
         return matcher.matches() ? matcher.group(1) : name;
     }
 
+    /**
+     * Whether a name is that of a field, {@code this#<declaring type>.<field>}, possibly with an instance counter
+     */
+    public static boolean isField(String name) {
+        return FIELD_PATTERN.matcher(withoutInstance(name)).matches();
+    }
+
+    /**
+     * Writes a field name as it is written in code: {@code this.field} for an instance field and {@code Class.field}
+     * for a static one, leaving any other name unchanged; the internal name keeps the declaring type to tell fields of
+     * different classes apart
+     */
+    private static String formatField(String name) {
+        Matcher matcher = FIELD_PATTERN.matcher(name);
+        if (!matcher.matches())
+            return name;
+
+        if (FieldDisplayNames.isStaticField(name))
+            return simpleTypeName(matcher.group(1)) + "." + matcher.group(2);
+        return "this." + matcher.group(2);
+    }
+
+    private static String fieldOf(String name) {
+        Matcher matcher = FIELD_PATTERN.matcher(name);
+        return matcher.matches() ? matcher.group(2) : name;
+    }
+
+    private static String simpleTypeName(String qualifiedName) {
+        int start = Math.max(qualifiedName.lastIndexOf('.'), qualifiedName.lastIndexOf('$'));
+        return qualifiedName.substring(start + 1);
+    }
+
     private static String toSuperscript(String number) {
         StringBuilder sb = new StringBuilder(number.length());
         for (char c : number.toCharArray()) {