Refer return values in StateRefinements

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

@@ -0,0 +1,40 @@
+package testSuite;
+
+import liquidjava.specification.*;
+
+@StateSet({"maybeEmpty", "hasNextElem", "empty"})
+public class CorrectIteratorReturnHasNext {
+
+    int index;
+    int size;
+
+    @StateRefinement(to = "maybeEmpty(this) && index() == 0 && size() == size")
+    CorrectIteratorReturnHasNext(int size) {
+        this.size = size;
+        this.index = 0;
+    }
+
+    @StateRefinement(to = "return ? hasNextElem(this) : empty(this)")
+    boolean hasNext() {
+        return index < size;
+    }
+
+    @StateRefinement(from = "hasNextElem(this)", to = "maybeEmpty(this) && index() == index(old(this)) + 1 && size() == size(old(this))")
+    int next() {
+        index += 1;
+        return index; // return index++; does not work
+    }
+
+    int main1() {
+        CorrectIteratorReturnHasNext it = new CorrectIteratorReturnHasNext(5);
+        int sum = 0;
+        while (true){
+            if(it.hasNext()){
+                sum += it.next();
+            } else {
+                break;
+            }
+        }
+        return sum;
+    }
+}

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

@@ -0,0 +1,54 @@
+package testSuite;
+
+import liquidjava.specification.*;
+
+@StateSet({"maybeEmpty", "hasNextElem", "empty"})
+public class ErrorIteratorReturnHasNext {
+    int index;
+    int size;
+
+    @StateRefinement(to = "maybeEmpty(this) && index() == 0 && size() == size")
+    ErrorIteratorReturnHasNext(int size) {
+        this.size = size;
+        this.index = 0;
+    }
+
+    @StateRefinement(to = "return ? hasNextElem(this) : empty(this)")
+    boolean hasNext() {
+        return index < size;
+    }
+
+    @StateRefinement(from = "hasNextElem(this)", to = "maybeEmpty(this) && index() == index(old(this)) + 1 && size() == size(old(this))")
+    int next() {
+        index += 1;
+        return index; // return index++; does not work
+    }
+
+
+    void main1() {
+        ErrorIteratorReturnHasNext it = new ErrorIteratorReturnHasNext(5);
+        if(it.hasNext()){
+            it.next();
+        } else {
+            it.next(); // State Refinement Error
+        }
+    }
+
+    void main2() {
+        ErrorIteratorReturnHasNext it = new ErrorIteratorReturnHasNext(5);
+        it.next(); // State Refinement Error
+    }
+
+    int main3() {
+        ErrorIteratorReturnHasNext it = new ErrorIteratorReturnHasNext(5);
+        int sum = 0;
+        while (true){
+            if(!it.hasNext()){
+                sum += it.next(); // State Refinement Error
+            } else {
+                break;
+            }
+        }
+        return sum;
+    }
+}

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

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

liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/JpegExporter.java

@@ -0,0 +1,49 @@
+package testSuite.classes.image_params_so_error;
+import java.awt.image.RenderedImage;
+import java.io.File;
+import java.io.FileOutputStream;
+import java.io.IOException;
+import java.io.OutputStream;
+import java.util.Locale;
+
+import javax.imageio.IIOImage;
+import javax.imageio.ImageIO;
+import javax.imageio.ImageWriteParam;
+import javax.imageio.ImageWriter;
+import javax.imageio.stream.ImageOutputStream;
+import java.util.Iterator;
+
+class JpegExporter {
+
+    // Adapted from https://stackoverflow.com/questions/72024965/how-to-compress-jpg-and-png-images-in-java
+    ImageWriteParam setCompressionPreferences() {
+        ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
+        if (param.canWriteCompressed()) {
+            param.setCompressionMode(ImageWriteParam.MODE_DEFAULT);
+            param.setCompressionQuality(0.85f); // State Refinement Error
+        }
+        return param;
+    }
+
+    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();
+        param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT); // State Refinement Error
+        param.setCompressionQuality(0.5f);
+
+        writer.write(null, new IIOImage(image, null, null), param);
+        os.close();
+        ios.close();
+        writer.dispose();
+        return String.valueOf(compressedImageFile);
+    }
+}

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

@@ -289,14 +289,28 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
             return new HashMap<>();
         Map<String, String> map = mapInvocation(arguments, f);
 
+        // Stable return-value name so `_`/`return` in @StateRefinement to= matches the post-call VariableInstance.
+        String returnViName = null;
+        CtTypeReference<?> retType = f.getType();
+        if (retType != null && !"void".equals(retType.toString())) {
+            returnViName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
+            invocation.putMetadata(Keys.RETURN_VAR_NAME, returnViName);
+            if (f.allRefinementsTrue())
+                rtc.getContext().addInstanceToContext(returnViName, retType, new Predicate(), invocation);
+        }
+
         if (target != null)
             AuxStateHandler.prepareInvocationTarget(rtc, target, invocation);
 
         if (f.allRefinementsTrue()) {
             if (target != null)
                 AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
 
-            invocation.putMetadata(Keys.REFINEMENT, new Predicate());
+            // Expose `_ == returnViName` so the if-condition path variable ties to this return value.
+            Predicate emptyRef = returnViName != null
+                    ? Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(returnViName))
+                    : new Predicate();
+            invocation.putMetadata(Keys.REFINEMENT, emptyRef);
             return map;
         }
 
@@ -325,7 +339,8 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
                     varName = v.getName();
             }
 
-            String viName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
+            String viName = returnViName != null ? returnViName
+                    : String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
             VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(),
                     methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVIEW!!
             if (varName != null && f.hasStateChange() && equalsThis)

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

@@ -209,12 +209,22 @@ private static Predicate createStatePredicate(String value, String targetClass,
             throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
                     value);
         }
+        CtTypeReference<?> returnType = null;
+        if (isTo && e instanceof CtMethod<?> method) {
+            CtTypeReference<?> mt = method.getType();
+            if (mt != null && !"void".equals(mt.toString())) {
+                p = p.substituteVariable("return", Keys.WILDCARD);
+                returnType = mt;
+            }
+        }
         CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
         String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
         String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
         tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e);
         tc.getContext().addVarToContext(name, r, new Predicate(), e);
         tc.getContext().addVarToContext(nameOld, r, new Predicate(), e);
+        if (returnType != null && !tc.getContext().hasVariable(Keys.WILDCARD))
+            tc.getContext().addVarToContext(Keys.WILDCARD, returnType, new Predicate(), e);
         // TODO REVIEW!!
         // what is it for?
         Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
@@ -481,7 +491,10 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
             found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
             if (found && stateChange.hasTo()) {
                 String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
-                Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName)
+                // Non-void: `_` is the return value; void: legacy alias for the new instance.
+                String returnViName = (String) invocation.getMetadata(Keys.RETURN_VAR_NAME);
+                String wildcardTarget = returnViName != null ? returnViName : newInstanceName;
+                Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, wildcardTarget)
                         .substituteVariable(Keys.THIS, newInstanceName);
                 for (String s : map.keySet()) {
                     transitionedState = transitionedState.substituteVariable(s, map.get(s));

liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java

@@ -4,6 +4,7 @@ public final class Keys {
     public static final String REFINEMENT = "refinement";
     public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check";
     public static final String TARGET = "target";
+    public static final String RETURN_VAR_NAME = "return_var_name";
     public static final String THIS = "this";
     public static final String WILDCARD = "_";
     public static final String OLD = "old";