Qualify field context keys by declaring type

Author: rcosta358

liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java

@@ -0,0 +1,16 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectDistinctClassFields {
+    @Refinement("_ < 0") int port = -1;
+    private final Job job = new Job();
+
+    public void send() {
+        job.port = 5;
+    }
+
+    static class Job {
+        @Refinement("_ >= 0") int port;
+    }
+}

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

@@ -15,6 +15,7 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Enum;
 import liquidjava.utils.StaticConstants;
+import liquidjava.utils.FieldNames;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Types;
@@ -220,7 +221,7 @@ private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) thr
         } else if (ex instanceof CtFieldWrite<?> fw) {
             CtFieldReference<?> cr = fw.getVariable();
             CtField<?> f = fw.getVariable().getDeclaration();
-            String updatedVarName = String.format(Formats.THIS, cr.getSimpleName());
+            String updatedVarName = FieldNames.of(cr);
             checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f);
 
             // corresponding ghost function update
@@ -261,7 +262,7 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
     public <T> void visitCtField(CtField<T> f) {
         super.visitCtField(f);
         Optional<Predicate> c = getRefinementFromAnnotation(f);
-        String name = String.format(Formats.THIS, f.getSimpleName());
+        String name = FieldNames.of(f.getReference());
         Predicate ret = new Predicate();
         if (c.isPresent()) {
             ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name);
@@ -291,8 +292,8 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
                         Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName)));
             }
 
-        } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) {
-            String thisName = String.format(Formats.THIS, fieldName);
+        } else if (context.hasVariable(FieldNames.of(fieldRead.getVariable()))) {
+            String thisName = FieldNames.of(fieldRead.getVariable());
             fieldRead.putMetadata(Keys.REFINEMENT,
                     Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
 

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.FieldNames;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Ops;
@@ -125,8 +126,8 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJErro
         Predicate all;
         if (ex instanceof CtVariableWrite<T> w) {
             name = w.getVariable().getSimpleName();
-            if (w instanceof CtFieldWrite<?>)
-                name = String.format(Formats.THIS, name);
+            if (w instanceof CtFieldWrite<?> fieldWrite)
+                name = FieldNames.of(fieldWrite.getVariable());
             all = getRefinementUnaryVariableWrite(ex, operator, w, name);
             rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration());
             return;
@@ -203,8 +204,8 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
 
         if (element instanceof CtVariableRead<?> elemVar) {
             String elemName = elemVar.getVariable().getSimpleName();
-            if (elemVar instanceof CtFieldRead)
-                elemName = String.format(Formats.THIS, elemName);
+            if (elemVar instanceof CtFieldRead<?> fieldRead)
+                elemName = FieldNames.of(fieldRead.getVariable());
             Predicate elemRef = rtc.getContext().getVariableRefinements(elemName);
 
             String returnName = elemName;
@@ -336,8 +337,8 @@ private Predicate getCurrentVariableValue(String name) {
     private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throws LJError {
         if (element instanceof CtVariableRead<?> variableRead) {
             String name = variableRead.getVariable().getSimpleName();
-            if (variableRead instanceof CtFieldRead<?>)
-                name = String.format(Formats.THIS, name);
+            if (variableRead instanceof CtFieldRead<?> fieldRead)
+                name = FieldNames.of(fieldRead.getVariable());
             return getCurrentVariableValue(name);
         } else if (element instanceof CtBinaryOperator<?> binaryOperator) {
             Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand());

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

@@ -11,6 +11,7 @@
 import liquidjava.processor.refinement_checker.TypeChecker;
 import liquidjava.processor.refinement_checker.TypeCheckingUtils;
 import liquidjava.rj_language.Predicate;
+import liquidjava.utils.FieldNames;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
@@ -392,7 +393,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre
      */
     public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws LJError {
         CtField<?> field = fw.getVariable().getDeclaration();
-        String updatedVarName = String.format(Formats.THIS, fw.getVariable().getSimpleName());
+        String updatedVarName = FieldNames.of(fw.getVariable());
         String targetClass = field.getDeclaringType().getQualifiedName();
 
         // state transition annotation construction
@@ -604,7 +605,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             // means invocation is in a form of `t.method(args)`
             String name = v.getVariable().getSimpleName();
             if (target2 instanceof CtFieldRead<?> fieldRead && fieldRead.getTarget() instanceof CtThisAccess<?>) {
-                String fieldName = String.format(Formats.THIS, name);
+                String fieldName = FieldNames.of(fieldRead.getVariable());
                 if (tc.getContext().hasVariable(fieldName))
                     name = fieldName;
             }

liquidjava-verifier/src/main/java/liquidjava/utils/FieldNames.java

@@ -0,0 +1,19 @@
+package liquidjava.utils;
+
+import spoon.reflect.reference.CtFieldReference;
+
+public final class FieldNames {
+    private FieldNames() {
+    }
+
+    public static String of(CtFieldReference<?> field) {
+        StringBuilder name = new StringBuilder("this#");
+        field.getDeclaringType().getQualifiedName().codePoints().forEach(c -> {
+            if (c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z' || c >= '0' && c <= '9' || c == '_')
+                name.appendCodePoint(c);
+            else
+                name.append('#').append(Integer.toHexString(c)).append('#');
+        });
+        return name.append('#').append(field.getSimpleName()).toString();
+    }
+}