diff --git a/liquidjava-example/src/main/java/testSuite/CorrectIteratorReturnHasNext.java b/liquidjava-example/src/main/java/testSuite/CorrectIteratorReturnHasNext.java new file mode 100644 index 00000000..6e7b1b6a --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIteratorReturnHasNext.java b/liquidjava-example/src/main/java/testSuite/ErrorIteratorReturnHasNext.java new file mode 100644 index 00000000..ea2196f2 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/ImageWriteParamsRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/ImageWriteParamsRefinements.java new file mode 100644 index 00000000..033b189c --- /dev/null +++ b/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(); +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/JpegExporter.java b/liquidjava-example/src/main/java/testSuite/classes/image_params_so_error/JpegExporter.java new file mode 100644 index 00000000..a78e510b --- /dev/null +++ b/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 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); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index d9d6b2b5..a41280a3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -289,6 +289,16 @@ private Map checkInvocationRefinements(CtElement invocation, Lis return new HashMap<>(); Map 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); @@ -296,7 +306,11 @@ private Map checkInvocationRefinements(CtElement invocation, Lis 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 returnRef = returnViName != null + ? Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(returnViName)) + : new Predicate(); + invocation.putMetadata(Keys.REFINEMENT, returnRef); return map; } @@ -325,7 +339,8 @@ private Map 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) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index d8402d48..7204a467 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/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