Implicit Constructor Refinements (#236)

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/input_stream_reader_no_constructor_correct/InputStreamReaderRefinements.java

@@ -0,0 +1,15 @@
+package testSuite.classes.input_stream_reader_no_constructor_correct;
+
+import liquidjava.specification.*;
+
+// https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html
+@ExternalRefinementsFor("java.io.InputStreamReader")
+@StateSet({"open", "closed"})
+public interface InputStreamReaderRefinements {
+
+    @StateRefinement(from="open(this)")
+    public int read();
+
+    @StateRefinement(from="open(this)", to="closed(this)")
+    public void close();
+}

liquidjava-example/src/main/java/testSuite/classes/input_stream_reader_no_constructor_correct/SimpleTest.java

@@ -0,0 +1,13 @@
+package testSuite.classes.input_stream_reader_no_constructor_correct;
+
+import java.io.IOException;
+import java.io.InputStreamReader;
+
+public class SimpleTest {
+
+    public static void main(String[] args) throws IOException {
+        InputStreamReader isr = new InputStreamReader(System.in);
+        isr.read();
+        isr.close();
+    }
+}

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

@@ -66,10 +66,18 @@ public void getConstructorInvocationRefinements(CtConstructorCall<?> ctConstruct
             RefinedFunction f = rtc.getContext().getFunction(exe.getSimpleName(),
                     exe.getDeclaringType().getQualifiedName(), paramTypes);
             if (f != null) {
+                // explicit constructor refinements
                 Map<String, String> map = checkInvocationRefinements(ctConstructorCall,
                         ctConstructorCall.getArguments(), ctConstructorCall.getTarget(), f.getName(),
                         f.getTargetClass(), paramTypes);
                 AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall);
+            } else {
+                // default constructor refinements
+                CtTypeReference<?> type = exe.getDeclaringType() != null ? exe.getDeclaringType()
+                        : ctConstructorCall.getType();
+                if (type != null)
+                    ctConstructorCall.putMetadata(Keys.REFINEMENT, AuxStateHandler.getDefaultState(rtc,
+                            type.getQualifiedName(), Predicate.createVar(Keys.THIS)));
             }
         }
     }

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

@@ -87,10 +87,16 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
      * @param tc
      */
     public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
-        String klass = f.getTargetClass();
-        Predicate[] s = { Predicate.createVar(Keys.THIS) };
+        ObjectState os = new ObjectState();
+        os.setTo(getDefaultState(tc, f.getTargetClass(), Predicate.createVar(Keys.THIS)));
+        List<ObjectState> los = new ArrayList<>();
+        los.add(os);
+        f.setAllStates(los);
+    }
+
+    public static Predicate getDefaultState(TypeChecker tc, String klass, Predicate target) {
         Predicate c = new Predicate();
-        List<GhostFunction> sets = getDifferentSets(tc, klass); // ??
+        List<GhostFunction> sets = getDifferentSets(tc, klass);
         for (GhostFunction sg : sets) {
             String retType = sg.getReturnType().toString();
             Predicate typePredicate = switch (retType) {
@@ -100,14 +106,11 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
             case "double" -> Predicate.createLit("0.0", Types.DOUBLE);
             default -> throw new RuntimeException("Ghost not implemented for type " + retType);
             };
-            Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s), typePredicate);
+            Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), target),
+                    typePredicate);
             c = Predicate.createConjunction(c, p);
         }
-        ObjectState os = new ObjectState();
-        os.setTo(c);
-        List<ObjectState> los = new ArrayList<>();
-        los.add(os);
-        f.setAllStates(los);
+        return c;
     }
 
     /**