Fix Field Access

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufTest.java

@@ -9,14 +9,13 @@ public class ByteBufTest {
 
     public static final int TEST_BUFFER_SIZE = 128;
 
-    // private ByteBuffer mDirectBuffer;
+    private ByteBuffer mDirectBuffer;
 
     public ByteBufTest() {
         // FIX (from accepted answer): mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]);
         // or guard with: if (mDirectBuffer.hasArray()) { ... }
-        ByteBuffer mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]);
-        // VIOLATION: a direct buffer is not array-backed -> array() throws
-        // UnsupportedOperationException.
+        mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]);
+        // wrap returns an array-backed buffer, so the field retains the state required by array()
         byte[] buf = mDirectBuffer.array();
         buf[1] = 100;
     }

liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufTest.java

@@ -9,12 +9,12 @@ public class ByteBufTest {
 
     public static final int TEST_BUFFER_SIZE = 128;
 
-    // private ByteBuffer mDirectBuffer;
+    private ByteBuffer mDirectBuffer;
 
     public ByteBufTest() {
         // FIX (from accepted answer): mDirectBuffer = ByteBuffer.wrap(new byte[TEST_BUFFER_SIZE]);
         // or guard with: if (mDirectBuffer.hasArray()) { ... }
-        ByteBuffer mDirectBuffer = ByteBuffer.allocateDirect(TEST_BUFFER_SIZE);
+        mDirectBuffer = ByteBuffer.allocateDirect(TEST_BUFFER_SIZE);
         // VIOLATION: a direct buffer is not array-backed -> array() throws
         // UnsupportedOperationException.
         byte[] buf = mDirectBuffer.array(); // State Refinement Error

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

@@ -594,11 +594,19 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2,
             // v--------- field read
             // 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);
+                if (tc.getContext().hasVariable(fieldName))
+                    name = fieldName;
+            }
             Optional<VariableInstance> invocationCallee = tc.getContext().getLastVariableInstance(name);
             if (invocationCallee.isPresent()) {
                 invocation.putMetadata(Keys.TARGET, invocationCallee.get());
             } else if (target2.getMetadata(Keys.TARGET) == null) {
                 RefinedVariable var = tc.getContext().getVariableByName(name);
+                if (var == null)
+                    return name;
+
                 String nName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
                 RefinedVariable rv = tc.getContext().addInstanceToContext(nName, var.getType(),
                         var.getRefinement().substituteVariable(name, nName), target2);