Name generated values after what they are instead of #fresh

liquidjava-example/src/main/java/testSuite/classes/generated_names_error/Door.java

@@ -0,0 +1,14 @@
+package testSuite.classes.generated_names_error;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"opened", "closed"})
+public class Door {
+
+    @StateRefinement(to = "closed(this)")
+    public Door() {}
+
+    @StateRefinement(from = "opened(this)", to = "closed(this)")
+    public void close() {}
+}

liquidjava-example/src/main/java/testSuite/classes/generated_names_error/GeneratedNames.java

@@ -0,0 +1,60 @@
+package testSuite.classes.generated_names_error;
+
+import liquidjava.specification.Refinement;
+
+// Each value the verifier introduces is named after what it is, not #fresh (#373)
+public class GeneratedNames {
+
+    static void positive(@Refinement("_ > 0") int x) {}
+
+    @Refinement("_ > 0")
+    static int negate(@Refinement("_ < 0") int x) {
+        return -x;
+    }
+
+    static boolean ready(int a) {
+        return a > 0;
+    }
+
+    static int read(int key) {
+        return key;
+    }
+
+    static void ifCondition(int a) {
+        if (ready(a))
+            positive(a); // Expect: Refinement Error
+    }
+
+    static void loopCondition(int a) {
+        while (ready(a))
+            positive(a); // Expect: Refinement Error
+    }
+
+    static int ternaryCondition(int a) {
+        return ready(a) ? negate(a) : 1; // Expect: Refinement Error
+    }
+
+    static void tryAndCatchBranches(int a) {
+        try {
+            a = read(a);
+        } catch (IllegalStateException e) {
+            a = 1;
+        } catch (RuntimeException e) {
+            positive(a); // Expect: Refinement Error
+        }
+    }
+
+    static void callResult(int key) {
+        positive(read(key) - 1); // Expect: Refinement Error
+    }
+
+    static void operationResult(String s) {
+        boolean isNull = s == null;
+        if (isNull)
+            positive(0); // Expect: Refinement Error
+    }
+
+    static void newObject() {
+        new Door().close(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -21,9 +21,9 @@
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.smt.Counterexample;
+import liquidjava.utils.GeneratedNames;
 import liquidjava.utils.Pair;
 import liquidjava.utils.Utils;
-import liquidjava.utils.constants.Formats;
 import spoon.reflect.cu.SourcePosition;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
@@ -184,7 +184,7 @@ private List<String> originalBinders() {
     private static int relevance(String term, List<String> expectedTerms, List<String> foundTerms) {
         if (expectedTerms.contains(term))
             return foundTerms.contains(term) ? 1 : 0;
-        return term.startsWith(Formats.FRESH_PREFIX) ? 3 : 2;
+        return GeneratedNames.isGenerated(term) ? 3 : 2;
     }
 
     // Variables and ghost applications of an expression, named as in the SMT model

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

@@ -21,6 +21,7 @@
 import liquidjava.rj_language.BuiltinFunctionPredicate;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Enum;
+import liquidjava.utils.GeneratedNames;
 import liquidjava.utils.StaticConstants;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
@@ -210,7 +211,7 @@ public <T> void visitCtNewArray(CtNewArray<T> newArray) {
         // TODO only working for 1 dimension
         for (CtExpression<?> exp : l) {
             Predicate c = getExpressionRefinements(exp);
-            String name = String.format(Formats.FRESH, context.getCounter());
+            String name = GeneratedNames.of(GeneratedNames.ARRAY_LENGTH, context.getCounter());
             if (c.getVariableNames().contains(Keys.WILDCARD)) {
                 c = c.substituteVariable(Keys.WILDCARD, name);
             } else {
@@ -498,7 +499,7 @@ public void visitCtIf(CtIf ifElement) {
         CtExpression<Boolean> exp = ifElement.getCondition();
         Predicate expRefs = getExpressionRefinements(exp);
 
-        String pathVarName = String.format(Formats.FRESH, context.getCounter());
+        String pathVarName = GeneratedNames.of(GeneratedNames.IF_CONDITION, context.getCounter());
         // A value refinement constrains the result of evaluating the expression; it is not
         // itself the truth value selecting the branch. Calls without a wildcard likewise
         // provide no information about their boolean result.
@@ -610,14 +611,13 @@ private void keepFreshValues(Predicate predicate) {
     }
 
     private void keepFreshValues(Predicate predicate, Set<String> visited) {
-        String freshPrefix = Formats.FRESH.substring(0, Formats.FRESH.indexOf('%'));
         for (String name : predicate.getVariableNames()) {
             if (!visited.add(name))
                 continue;
             RefinedVariable value = context.getVariableByName(name);
             if (value == null)
                 continue;
-            if (name.startsWith(freshPrefix))
+            if (GeneratedNames.isGenerated(name))
                 context.addInstanceVariable(value);
             keepFreshValues(value.getMainRefinement(), visited);
         }
@@ -821,7 +821,7 @@ private static void removeCheckMetadata(CtLoop loop) {
     private void recordExit(LoopTypestates states, CtExpression<Boolean> condition) {
         if (condition == null)
             return;
-        RefinedVariable conditionIsFalse = assumeCondition(condition, false);
+        RefinedVariable conditionIsFalse = assumeCondition(condition, false, GeneratedNames.LOOP_CONDITION);
         states.recordExit();
         if (conditionIsFalse != null)
             vcChecker.removePathVariable(conditionIsFalse);
@@ -953,22 +953,22 @@ private boolean mayChangeState(CtInvocation<?> invocation) {
      * the condition of an if, see visitCtIf). Re-assigning a variable in the body drops the conditions on it.
      */
     private void assumeLoopCondition(CtExpression<Boolean> condition) {
-        assumeCondition(condition, true);
+        assumeCondition(condition, true, GeneratedNames.LOOP_CONDITION);
     }
 
     /**
      * Adds a path condition saying that {@code condition} evaluated to {@code holds}, on the values it was evaluated
-     * on. Returns the path variable, so the caller can remove it where the condition no longer applies, or null when
-     * nothing is assumed.
+     * on, in a path variable named after {@code kind}. Returns the path variable, so the caller can remove it where the
+     * condition no longer applies, or null when nothing is assumed.
      */
-    private RefinedVariable assumeCondition(CtExpression<Boolean> condition, boolean holds) {
+    private RefinedVariable assumeCondition(CtExpression<Boolean> condition, boolean holds, String kind) {
         // conditions with side effects (e.g. (n = read()) > 0) are not encoded, so they assume nothing
         if (condition == null || !condition.getElements(new TypeFilter<>(CtVariableWrite.class)).isEmpty())
             return null;
         Predicate refs = getRefinement(condition);
         if (isUninformativeCondition(refs, condition))
             return null;
-        String pathVarName = String.format(Formats.FRESH, context.getCounter());
+        String pathVarName = GeneratedNames.of(kind, context.getCounter());
         boolean valueIsCondition = refs.getVariableNames().contains(Keys.WILDCARD);
         refs = refs.substituteVariable(Keys.WILDCARD, pathVarName);
         refs = Predicate.createConjunction(refs, substituteAllVariablesForLastInstance(refs));
@@ -1006,7 +1006,7 @@ public <T> void visitCtConditional(CtConditional<T> conditional) {
     }
 
     private void scanAssuming(CtExpression<?> branch, CtExpression<Boolean> condition, boolean holds) {
-        RefinedVariable pathVar = assumeCondition(condition, holds);
+        RefinedVariable pathVar = assumeCondition(condition, holds, GeneratedNames.TERNARY_CONDITION);
         scan(branch);
         if (pathVar != null)
             vcChecker.removePathVariable(pathVar);

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

@@ -9,6 +9,7 @@
 import liquidjava.processor.context.Variable;
 import liquidjava.processor.context.VariableInstance;
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.GeneratedNames;
 import liquidjava.utils.constants.Formats;
 import spoon.reflect.code.CtCatch;
 import spoon.reflect.code.CtExpression;
@@ -73,7 +74,8 @@ private boolean visitBranches(CtTry tryBlock, int i, Map<Variable, VariableInsta
         if (i == tryBlock.getCatchers().size())
             return visitBranch(tryBlock, i, before, inTry);
 
-        String pathVarName = String.format(Formats.FRESH, context.getCounter());
+        String branch = i == 0 ? GeneratedNames.TRY_BRANCH : GeneratedNames.CATCH_BRANCH;
+        String pathVarName = GeneratedNames.of(branch, context.getCounter());
         Predicate cond = Predicate.createVar(pathVarName);
         RefinedVariable pathVar = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE,
                 new Predicate(), tryBlock);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

@@ -10,6 +10,7 @@
 import liquidjava.processor.context.Variable;
 import liquidjava.processor.context.VariableInstance;
 import liquidjava.processor.refinement_checker.TypeChecker;
+import liquidjava.utils.GeneratedNames;
 import liquidjava.utils.StaticConstants;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
@@ -174,7 +175,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJErro
             operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), value));
             return;
         }
-        String name = Formats.FRESH;
+        String name = null;
         Predicate all;
         if (ex instanceof CtVariableWrite<T> w) {
             name = w.getVariable().getSimpleName();
@@ -211,9 +212,8 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJErro
             type = operator.getFactory().Type().booleanPrimitiveType();
         }
         Predicate metadata = rtc.getRefinement(ex);
-        String newName = !name.equals(Formats.FRESH)
-                ? String.format(Formats.INSTANCE, name, rtc.getContext().getCounter())
-                : String.format(name, rtc.getContext().getCounter());
+        String newName = name != null ? String.format(Formats.INSTANCE, name, rtc.getContext().getCounter())
+                : GeneratedNames.valueOf(ex, rtc.getContext().getCounter());
         Predicate newMeta = metadata.substituteVariable(Keys.WILDCARD, newName);
 
         Predicate unOp = getOperatorFromKind(operator.getKind(), operator);
@@ -254,7 +254,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
             CtExpression<?> element) throws LJError {
         if (element instanceof CtFieldRead<?> field) {
             if (field.getVariable().getSimpleName().equals("length")) {
-                String name = String.format(Formats.FRESH, rtc.getContext().getCounter());
+                String name = GeneratedNames.valueOf(field, rtc.getContext().getCounter());
                 rtc.getContext().addVarToContext(name, element.getType(),
                         rtc.getRefinement(element).substituteVariable(Keys.WILDCARD, name), field);
                 return Predicate.createVar(name);
@@ -327,7 +327,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!
 
             // Substitute _ by the variable that we send
-            String newName = String.format(Formats.FRESH, rtc.getContext().getCounter());
+            String newName = GeneratedNames.valueOf(inv, rtc.getContext().getCounter());
             innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName);
             rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv);
             return new Predicate(newName, inv); // Return variable that represents the invocation
@@ -341,7 +341,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
      * method without refinements
      */
     private Predicate getUnconstrainedInvocationVariable(CtInvocation<?> inv) {
-        String newName = String.format(Formats.FRESH, rtc.getContext().getCounter());
+        String newName = GeneratedNames.valueOf(inv, rtc.getContext().getCounter());
         rtc.getContext().addVarToContext(newName, inv.getType(), new Predicate(), inv);
         return new Predicate(newName, inv);
     }
@@ -365,7 +365,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
             Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!
 
             // Substitute _ by the variable that we send
-            String newName = String.format(Formats.FRESH, rtc.getContext().getCounter());
+            String newName = GeneratedNames.valueOf(inv, rtc.getContext().getCounter());
             innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName);
 
             // change this for the current instance
@@ -476,7 +476,7 @@ private Predicate createFreshValue(CtExpression<?> element, Predicate refinement
     }
 
     private Predicate createFreshValue(CtExpression<?> element, CtTypeReference<?> type, Predicate refinement) {
-        String newName = String.format(Formats.FRESH, rtc.getContext().getCounter());
+        String newName = GeneratedNames.valueOf(element, rtc.getContext().getCounter());
         Predicate freshRefinement = refinement.substituteVariable(Keys.WILDCARD, newName);
         rtc.getContext().addVarToContext(newName, type, freshRefinement, element);
         return Predicate.createVar(newName);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java

@@ -98,7 +98,7 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct
         if (functionRef.isBooleanTrue())
             function.setRefinement(superRef);
         else {
-            String name = String.format(Formats.FRESH, tc.getContext().getCounter());
+            String name = String.format(Formats.RET, tc.getContext().getCounter());
             tc.getContext().addVarToContext(name, superFunction.getType(), new Predicate(), method);
             // functionRef might be stronger than superRef
             // check (superRef <: functionRef)
@@ -138,7 +138,7 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi
                     ObjectState superState = superStates.get(i);
                     ObjectState subState = subStates.get(i);
 
-                    String thisName = String.format(Formats.FRESH, tc.getContext().getCounter());
+                    String thisName = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
                     createVariableInContext(thisName, tc, subFunction, superFunction, method);
 
                     Predicate superConst = matchVariableNames(thisName, superState.getFrom());

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -23,6 +23,7 @@
 import liquidjava.processor.state_machine.StateMachineBuilder;
 import liquidjava.processor.state_machine.StateSolver;
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.GeneratedNames;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
@@ -1090,7 +1091,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
                 && newCall.getMetadata(Keys.REFINEMENT)instanceof Predicate state) {
             // `new T(args).method()`: the receiver is a fresh object in the state the constructor gives. Must come
             // before the TARGET case: a constructor with refined parameters puts its (void) return value in TARGET
-            String name = String.format(Formats.FRESH, tc.getContext().getCounter());
+            String name = GeneratedNames.valueOf(newCall, tc.getContext().getCounter());
             RefinedVariable receiver = tc.getContext().addInstanceToContext(name, newCall.getType(),
                     state.substituteVariable(Keys.THIS, name).substituteVariable(Keys.WILDCARD, name), newCall);
             newCall.putMetadata(Keys.TARGET, receiver);
@@ -1105,7 +1106,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
                 && !isReturnValue(call)) {
             // `a.get().method()` where get() has no return refinement: the call's TARGET is its own receiver (a), not
             // the value it returns, so the receiver is a fresh value of the call's type, in a state not known here
-            String name = String.format(Formats.FRESH, tc.getContext().getCounter());
+            String name = GeneratedNames.valueOf(call, tc.getContext().getCounter());
             RefinedVariable receiver = tc.getContext().addInstanceToContext(name, call.getType(), new Predicate(),
                     call);
             call.putMetadata(Keys.RECEIVER, receiver);

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

@@ -28,7 +28,7 @@ public static String format(String name) {
         String receiver = FieldDisplayNames.writeReceiver(name);
         if (receiver != null && isField(baseName))
             return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter);
-        String prefix = isSpecialIdentifier(baseName) ? "#" : "";
+        String prefix = isReturn(baseName) ? "#" : "";
         return prefix + formatField(baseName) + toSuperscript(counter);
     }
 
@@ -80,8 +80,8 @@ private static String toSuperscript(String number) {
         return sb.toString();
     }
 
-    private static boolean isSpecialIdentifier(String id) {
-        return id.equals("fresh") || id.equals("ret");
+    private static boolean isReturn(String id) {
+        return id.equals("ret");
     }
 
     private static boolean isApplication(String name) {

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java

@@ -11,15 +11,13 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.LiteralBoolean;
 import liquidjava.rj_language.ast.Var;
-import liquidjava.utils.constants.Formats;
+import liquidjava.utils.GeneratedNames;
 
 /**
  * Simplifies VCImplication chains by removing vacuous binder implications
  */
 public class VCBinderSimplification implements VCSimplificationPass {
 
-    private static final String FRESH_PREFIX = Formats.FRESH_PREFIX;
-
     private final NeededVariables needed;
 
     public VCBinderSimplification() {
@@ -95,7 +93,7 @@ private boolean isRemovableBinder(VCImplication implication, Set<String> keptTru
      * Checks for a generated boolean path binder refined exactly by itself
      */
     private boolean isUnusedFreshPathBinder(VCImplication implication) {
-        if (!implication.hasNext() || !implication.getName().startsWith(FRESH_PREFIX)
+        if (!implication.hasNext() || !GeneratedNames.isGenerated(implication.getName())
                 || !"boolean".equals(implication.getType().getQualifiedName()))
             return false;