diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_stream_reader_no_constructor_correct/InputStreamReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/input_stream_reader_no_constructor_correct/InputStreamReaderRefinements.java new file mode 100644 index 00000000..fcd4eed0 --- /dev/null +++ b/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(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/input_stream_reader_no_constructor_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/input_stream_reader_no_constructor_correct/SimpleTest.java new file mode 100644 index 00000000..776e8f37 --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/jpeg_correct/CompressImage.java b/liquidjava-example/src/main/java/testSuite/classes/jpeg_correct/CompressImage.java new file mode 100644 index 00000000..ee4720b7 --- /dev/null +++ b/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 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); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/jpeg_correct/ImageWriteParamsRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/jpeg_correct/ImageWriteParamsRefinements.java new file mode 100644 index 00000000..a457547a --- /dev/null +++ b/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(); + + // ... +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 57cf8b0b..2182ec66 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/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); } 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 7204a467..c4da97d8 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 @@ -87,10 +87,16 @@ private static void setConstructorStates(RefinedFunction f, List los = new ArrayList<>(); + los.add(os); + f.setAllStates(los); + } + + public static Predicate getDefaultState(TypeChecker tc, String klass, Predicate target) { Predicate c = new Predicate(); - List sets = getDifferentSets(tc, klass); // ?? + List 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 los = new ArrayList<>(); - los.add(os); - f.setAllStates(los); + return c; } /**