extracting field ghost update to separate method

Kirill Golubev · Kirill Golubev · commit 3127da8427c0 · 2022-10-10T04:07:38.000+03:00
diff --git a/liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -227,40 +227,16 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignement) {
             checkAssignment(name, varDecl.getType(), ex, assignement.getAssignment(), assignement, varDecl);
 
         } else if (ex instanceof CtFieldWrite) {
+            System.out.println("Got field write: " + assignement);
             CtFieldWrite<?> fw = ((CtFieldWrite<?>) ex);
             CtFieldReference<?> cr = fw.getVariable();
             CtField<?> f = fw.getVariable().getDeclaration();
             String updatedVarName = String.format(thisFormat, cr.getSimpleName());
             checkAssignment(updatedVarName, cr.getType(), ex, assignement.getAssignment(), assignement, f);
-            // corresponding ghost function update
-            CtMethod<?> transitionMethod = factory.createMethod();
-            transitionMethod.setType(factory.createCtTypeReference(void.class));
-            transitionMethod.setBody(factory.createCtBlock(factory.createCodeSnippetStatement()));
-            transitionMethod.setSimpleName("_");
-
-            transitionMethod.setParent(f.getDeclaringType());
-            CtAnnotation<?> ann = factory.createAnnotation(factory.createCtTypeReference(StateRefinement.class));
-
-            String stateChangeRefinementTo = f.getSimpleName() + "(this) == " + updatedVarName;
-            String stateChangeRefinementFrom = "true";
-            ann.addValue("to", stateChangeRefinementTo);
-            ann.addValue("from", stateChangeRefinementFrom);
-
-            transitionMethod.addAnnotation(ann);
-
-            System.out.println("Target for invocation: " + fw.getTarget());
-            CtInvocation<?> inv = factory.createInvocation(fw.getTarget(), transitionMethod.getReference(),
-                    Collections.emptyList());
-
-            RefinedFunction rf = new RefinedFunction();
-            rf.setName(transitionMethod.getSimpleName());
-            rf.setType(transitionMethod.getType());
-            rf.setRefReturn(new Predicate());
-            rf.setClass(transitionMethod.getDeclaringType().getQualifiedName());
 
+            // corresponding ghost function update
             try {
-                AuxStateHandler.handleMethodState(transitionMethod, rf, this);
-                AuxStateHandler.checkTargetChanges(this, rf, inv.getTarget(), Collections.emptyMap(), inv);
+                updateGhostField(fw);
             } catch (ParsingException e) {
                 ErrorHandler.printCostumeError(assignement, "ParsingException in `" + assignement + "` in class `"
                         + f.getDeclaringType() + "` : " + e.getMessage(), errorEmitter);
@@ -628,4 +604,42 @@ private <T> void getPutVariableMetadada(CtElement elem, String name) {
         elem.putMetadata(REFINE_KEY, cref);
     }
 
+    private void updateGhostField(CtFieldWrite<?> fw) throws ParsingException {
+        CtField<?> f = fw.getVariable().getDeclaration();
+        String updatedVarName = String.format(thisFormat, fw.getVariable().getSimpleName());
+
+        // transition method construction
+        CtMethod<?> transitionMethod = factory.createMethod();
+        transitionMethod.setType(factory.createCtTypeReference(void.class));
+        transitionMethod.setBody(factory.createCtBlock(factory.createCodeSnippetStatement()));
+        transitionMethod.setSimpleName("_");
+
+        transitionMethod.setParent(f.getDeclaringType());
+        CtAnnotation<?> ann = factory.createAnnotation(factory.createCtTypeReference(StateRefinement.class));
+
+        // state transition annatation construction
+        String stateChangeRefinementTo = f.getSimpleName() + "(this) == " + updatedVarName;
+        String stateChangeRefinementFrom = "true";
+        ann.addValue("to", stateChangeRefinementTo);
+        ann.addValue("from", stateChangeRefinementFrom);
+
+        transitionMethod.addAnnotation(ann);
+
+        // extracting target from assignment
+        System.out.println("Target for invocation: " + fw.getTarget());
+        CtInvocation<?> inv = factory.createInvocation(fw.getTarget(), transitionMethod.getReference(),
+                Collections.emptyList());
+
+        // Refined function construction for invocation facilities reuse
+        RefinedFunction rf = new RefinedFunction();
+        rf.setName(transitionMethod.getSimpleName());
+        rf.setType(transitionMethod.getType());
+        rf.setRefReturn(new Predicate());
+        rf.setClass(transitionMethod.getDeclaringType().getQualifiedName());
+
+        // applying transition:
+        AuxStateHandler.handleMethodState(transitionMethod, rf, this);
+        AuxStateHandler.checkTargetChanges(this, rf, inv.getTarget(), Collections.emptyMap(), inv);
+    }
+
 }
