Initialize Unknown States

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-example/src/main/java/testSuite/classes/jpeg_correct/CompressImage.java

@@ -0,0 +1,33 @@
+package testSuite.classes.jpeg_correct;
+
+import java.io.*;
+import java.util.*;
+import javax.imageio.*;
+import javax.imageio.stream.ImageOutputStream;
+import java.awt.image.RenderedImage;
+
+public class CompressImage {
+
+    //  Adapted from https://stackoverflow.com/questions/72024965/how-to-compress-jpg-and-png-images-in-java
+    public String compressImage(File multipartFile, RenderedImage image) throws IOException {
+        String filePath = System.getProperty("java.io.tmpdir");
+        File compressedImageFile = new File(filePath);
+        OutputStream os = new FileOutputStream(compressedImageFile.getName());
+        String extension = multipartFile.getName().substring(multipartFile.getName().lastIndexOf('.') + 1);
+        Iterator<ImageWriter> writers = ImageIO.getImageWritersByFormatName(extension);
+        ImageWriter writer = writers.next();
+        ImageOutputStream ios = ImageIO.createImageOutputStream(os);
+        writer.setOutput(ios);
+
+        ImageWriteParam param = writer.getDefaultWriteParam(); // should initialize state to start()
+        if (param.canWriteCompressed()) {
+            param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT);
+            param.setCompressionQuality(0.5f);
+        }
+        writer.write(null, new IIOImage(image, null, null), param);
+        os.close();
+        ios.close();
+        writer.dispose();
+        return String.valueOf(compressedImageFile);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/jpeg_correct/ImageWriteParamsRefinements.java

@@ -0,0 +1,39 @@
+package testSuite.classes.jpeg_correct;
+
+import liquidjava.specification.*;
+import java.util.Locale;
+import javax.imageio.ImageWriteParam;
+
+@SuppressWarnings("unused")
+@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
+@StateSet({"start", "acceptCompression", "compressionExplicit", "compressionSet"})
+@RefinementAlias("Ratio(float v) { 0 <= v && v <= 1.0 }")
+public interface ImageWriteParamsRefinements {
+
+    @StateRefinement(to="start()")
+    void ImageWriteParam(Locale locale);
+
+    void setProgressiveMode(
+        @Refinement("mode == ImageWriteParam.MODE_DISABLED || mode == ImageWriteParam.MODE_DEFAULT || mode == ImageWriteParam.MODE_COPY_FROM_METADATA")
+        int mode
+    );
+
+    @StateRefinement(
+        from="compressionExplicit() || compressionSet()", 
+        to="mode == ImageWriteParam.MODE_EXPLICIT ? compressionExplicit() : start()"
+    )
+    @StateRefinement(
+        from="acceptCompression()", 
+        to="mode == ImageWriteParam.MODE_EXPLICIT ? compressionExplicit() : acceptCompression()"
+    )
+    void setCompressionMode(int mode);
+
+    @StateRefinement(from="compressionExplicit() || compressionSet()")
+    void setCompressionQuality(@Refinement("Ratio(_)") float quality);
+
+    @StateRefinement(from="start()", to="_ ? acceptCompression(this) : start()")
+    @StateRefinement(from="!start()")
+    boolean canWriteCompressed();
+
+    // ...
+}

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

@@ -16,6 +16,7 @@
 import liquidjava.processor.context.RefinedVariable;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.processor.facade.GhostDTO;
+import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.smt.SMTEvaluator;
@@ -346,6 +347,7 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
         String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
         Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
         correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
+        correctNewRefinement = setInitialStateIfUnknown(correctNewRefinement, type, newName);
         cEt = cEt.substituteVariable(simpleName, newName);
 
         // Substitute variable in verification
@@ -358,6 +360,12 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
         context.addRefinementToVariableInContext(simpleName, type, cet, usage);
     }
 
+    private Predicate setInitialStateIfUnknown(Predicate refinement, CtTypeReference<?> type, String instanceName) {
+        if (type == null || !refinement.isBooleanTrue())
+            return refinement;
+        return AuxStateHandler.getDefaultState(this, type.getQualifiedName(), Predicate.createVar(instanceName));
+    }
+
     public void checkSMT(Predicate expectedType, CtElement element) throws LJError {
         checkSMT(expectedType, element, null);
     }

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;
     }
 
     /**