Skip to content

Commit b649936

Browse files
rcosta358rcosta358
committed
Initialize Unknown States
1 parent c151570 commit b649936

6 files changed

Lines changed: 120 additions & 9 deletions

File tree

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
package testSuite.classes.input_stream_reader_no_constructor_correct;
2+
3+
import liquidjava.specification.*;
4+
5+
// https://docs.oracle.com/javase/7/docs/api/java/io/InputStreamReader.html
6+
@ExternalRefinementsFor("java.io.InputStreamReader")
7+
@StateSet({"open", "closed"})
8+
public interface InputStreamReaderRefinements {
9+
10+
@StateRefinement(from="open(this)")
11+
public int read();
12+
13+
@StateRefinement(from="open(this)", to="closed(this)")
14+
public void close();
15+
}

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package testSuite.classes.input_stream_reader_no_constructor_correct;
2+
3+
import java.io.IOException;
4+
import java.io.InputStreamReader;
5+
6+
public class SimpleTest {
7+
8+
public static void main(String[] args) throws IOException {
9+
InputStreamReader isr = new InputStreamReader(System.in);
10+
isr.read();
11+
isr.close();
12+
}
13+
}

‎liquidjava-example/src/main/java/testSuite/classes/jpeg_correct/CompressImage.java‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
package testSuite.classes.jpeg_correct;
2+
3+
import java.io.*;
4+
import java.util.*;
5+
import javax.imageio.*;
6+
import javax.imageio.stream.ImageOutputStream;
7+
import java.awt.image.RenderedImage;
8+
9+
public class CompressImage {
10+
11+
// Adapted from https://stackoverflow.com/questions/72024965/how-to-compress-jpg-and-png-images-in-java
12+
public String compressImage(File multipartFile, RenderedImage image) throws IOException {
13+
String filePath = System.getProperty("java.io.tmpdir");
14+
File compressedImageFile = new File(filePath);
15+
OutputStream os = new FileOutputStream(compressedImageFile.getName());
16+
String extension = multipartFile.getName().substring(multipartFile.getName().lastIndexOf('.') + 1);
17+
Iterator<ImageWriter> writers = ImageIO.getImageWritersByFormatName(extension);
18+
ImageWriter writer = writers.next();
19+
ImageOutputStream ios = ImageIO.createImageOutputStream(os);
20+
writer.setOutput(ios);
21+
22+
ImageWriteParam param = writer.getDefaultWriteParam(); // should initialize state to start()
23+
if (param.canWriteCompressed()) {
24+
param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT);
25+
param.setCompressionQuality(0.5f);
26+
}
27+
writer.write(null, new IIOImage(image, null, null), param);
28+
os.close();
29+
ios.close();
30+
writer.dispose();
31+
return String.valueOf(compressedImageFile);
32+
}
33+
}

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

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
package testSuite.classes.jpeg_correct;
2+
3+
import liquidjava.specification.*;
4+
import java.util.Locale;
5+
import javax.imageio.ImageWriteParam;
6+
7+
@SuppressWarnings("unused")
8+
@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
9+
@StateSet({"start", "acceptCompression", "compressionExplicit", "compressionSet"})
10+
@RefinementAlias("Ratio(float v) { 0 <= v && v <= 1.0 }")
11+
public interface ImageWriteParamsRefinements {
12+
13+
@StateRefinement(to="start()")
14+
void ImageWriteParam(Locale locale);
15+
16+
void setProgressiveMode(
17+
@Refinement("mode == ImageWriteParam.MODE_DISABLED || mode == ImageWriteParam.MODE_DEFAULT || mode == ImageWriteParam.MODE_COPY_FROM_METADATA")
18+
int mode
19+
);
20+
21+
@StateRefinement(
22+
from="compressionExplicit() || compressionSet()",
23+
to="mode == ImageWriteParam.MODE_EXPLICIT ? compressionExplicit() : start()"
24+
)
25+
@StateRefinement(
26+
from="acceptCompression()",
27+
to="mode == ImageWriteParam.MODE_EXPLICIT ? compressionExplicit() : acceptCompression()"
28+
)
29+
void setCompressionMode(int mode);
30+
31+
@StateRefinement(from="compressionExplicit() || compressionSet()")
32+
void setCompressionQuality(@Refinement("Ratio(_)") float quality);
33+
34+
@StateRefinement(from="start()", to="_ ? acceptCompression(this) : start()")
35+
@StateRefinement(from="!start()")
36+
boolean canWriteCompressed();
37+
38+
// ...
39+
}

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import liquidjava.processor.context.RefinedVariable;
1717
import liquidjava.processor.facade.AliasDTO;
1818
import liquidjava.processor.facade.GhostDTO;
19+
import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
1920
import liquidjava.rj_language.Predicate;
2021
import liquidjava.rj_language.parsing.RefinementsParser;
2122
import liquidjava.smt.SMTEvaluator;
@@ -346,6 +347,7 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
346347
String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
347348
Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
348349
correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
350+
correctNewRefinement = setInitialStateIfUnknown(correctNewRefinement, type, newName);
349351
cEt = cEt.substituteVariable(simpleName, newName);
350352

351353
// Substitute variable in verification
@@ -358,6 +360,12 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
358360
context.addRefinementToVariableInContext(simpleName, type, cet, usage);
359361
}
360362

363+
private Predicate setInitialStateIfUnknown(Predicate refinement, CtTypeReference<?> type, String instanceName) {
364+
if (type == null || !refinement.isBooleanTrue())
365+
return refinement;
366+
return AuxStateHandler.getDefaultState(this, type.getQualifiedName(), Predicate.createVar(instanceName));
367+
}
368+
361369
public void checkSMT(Predicate expectedType, CtElement element) throws LJError {
362370
checkSMT(expectedType, element, null);
363371
}

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

Lines changed: 12 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -87,10 +87,16 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
8787
* @param tc
8888
*/
8989
public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
90-
String klass = f.getTargetClass();
91-
Predicate[] s = { Predicate.createVar(Keys.THIS) };
90+
ObjectState os = new ObjectState();
91+
os.setTo(getDefaultState(tc, f.getTargetClass(), Predicate.createVar(Keys.THIS)));
92+
List<ObjectState> los = new ArrayList<>();
93+
los.add(os);
94+
f.setAllStates(los);
95+
}
96+
97+
public static Predicate getDefaultState(TypeChecker tc, String klass, Predicate target) {
9298
Predicate c = new Predicate();
93-
List<GhostFunction> sets = getDifferentSets(tc, klass); // ??
99+
List<GhostFunction> sets = getDifferentSets(tc, klass);
94100
for (GhostFunction sg : sets) {
95101
String retType = sg.getReturnType().toString();
96102
Predicate typePredicate = switch (retType) {
@@ -100,14 +106,11 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
100106
case "double" -> Predicate.createLit("0.0", Types.DOUBLE);
101107
default -> throw new RuntimeException("Ghost not implemented for type " + retType);
102108
};
103-
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s), typePredicate);
109+
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), target),
110+
typePredicate);
104111
c = Predicate.createConjunction(c, p);
105112
}
106-
ObjectState os = new ObjectState();
107-
os.setTo(c);
108-
List<ObjectState> los = new ArrayList<>();
109-
los.add(os);
110-
f.setAllStates(los);
113+
return c;
111114
}
112115

113116
/**

0 commit comments

Comments
 (0)