Skip to content

Commit c151570

Browse files
CatarinaGamboarcosta358
CatarinaGamboa
and
rcosta358
authored
Refer return values in StateRefinements (#233)
## Description The previous approach to add state dependent on return values was attached to the return refinements ``` @refinement("_ --> acceptCompression(this)") boolean canWriteCompressed(); ``` However, this is not a great mental model since we should change object states only using `@StateRefinements`. Therefore, now we allow using StateRefinemets for this, and fix previous bugs with the previous logic. ``` @StateRefinement(from = "start(this)", to = "return ? acceptCompression(this) : start(this)") boolean canWriteCompressed(); ``` ## Example Now we can verify: ``` 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; } ``` where before we would get an error because `param.canWriteCompressed()` implied a state that was in conflict with the previous state assigned in the constructor. Added several tests for the feature. ## Type of change - [x] Bug fix - [x] New feature - [ ] Documentation update - [ ] Code refactoring ## Checklist - [x] Added/updated tests under `liquidjava-example/src/main/java/testSuite/` (`Correct*` / `Error*`) - [x] `mvn test` passes locally - [ ] Updated docs/README if behavior or API changed --------- Co-authored-by: Ricardo Costa <rcosta.ms358@gmail.com>
1 parent 58349fa commit c151570

7 files changed

Lines changed: 210 additions & 3 deletions

File tree

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

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.*;
4+
5+
@StateSet({"maybeEmpty", "hasNextElem", "empty"})
6+
public class CorrectIteratorReturnHasNext {
7+
8+
int index;
9+
int size;
10+
11+
@StateRefinement(to = "maybeEmpty(this) && index() == 0 && size() == size")
12+
CorrectIteratorReturnHasNext(int size) {
13+
this.size = size;
14+
this.index = 0;
15+
}
16+
17+
@StateRefinement(to = "return ? hasNextElem(this) : empty(this)")
18+
boolean hasNext() {
19+
return index < size;
20+
}
21+
22+
@StateRefinement(from = "hasNextElem(this)", to = "maybeEmpty(this) && index() == index(old(this)) + 1 && size() == size(old(this))")
23+
int next() {
24+
index += 1;
25+
return index; // return index++; does not work
26+
}
27+
28+
int main1() {
29+
CorrectIteratorReturnHasNext it = new CorrectIteratorReturnHasNext(5);
30+
int sum = 0;
31+
while (true){
32+
if(it.hasNext()){
33+
sum += it.next();
34+
} else {
35+
break;
36+
}
37+
}
38+
return sum;
39+
}
40+
}

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

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.*;
4+
5+
@StateSet({"maybeEmpty", "hasNextElem", "empty"})
6+
public class ErrorIteratorReturnHasNext {
7+
int index;
8+
int size;
9+
10+
@StateRefinement(to = "maybeEmpty(this) && index() == 0 && size() == size")
11+
ErrorIteratorReturnHasNext(int size) {
12+
this.size = size;
13+
this.index = 0;
14+
}
15+
16+
@StateRefinement(to = "return ? hasNextElem(this) : empty(this)")
17+
boolean hasNext() {
18+
return index < size;
19+
}
20+
21+
@StateRefinement(from = "hasNextElem(this)", to = "maybeEmpty(this) && index() == index(old(this)) + 1 && size() == size(old(this))")
22+
int next() {
23+
index += 1;
24+
return index; // return index++; does not work
25+
}
26+
27+
28+
void main1() {
29+
ErrorIteratorReturnHasNext it = new ErrorIteratorReturnHasNext(5);
30+
if(it.hasNext()){
31+
it.next();
32+
} else {
33+
it.next(); // State Refinement Error
34+
}
35+
}
36+
37+
void main2() {
38+
ErrorIteratorReturnHasNext it = new ErrorIteratorReturnHasNext(5);
39+
it.next(); // State Refinement Error
40+
}
41+
42+
int main3() {
43+
ErrorIteratorReturnHasNext it = new ErrorIteratorReturnHasNext(5);
44+
int sum = 0;
45+
while (true){
46+
if(!it.hasNext()){
47+
sum += it.next(); // State Refinement Error
48+
} else {
49+
break;
50+
}
51+
}
52+
return sum;
53+
}
54+
}

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

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

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

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

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

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -289,14 +289,28 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
289289
return new HashMap<>();
290290
Map<String, String> map = mapInvocation(arguments, f);
291291

292+
// Stable return-value name so `_`/`return` in @StateRefinement to= matches the post-call VariableInstance.
293+
String returnViName = null;
294+
CtTypeReference<?> retType = f.getType();
295+
if (retType != null && !"void".equals(retType.toString())) {
296+
returnViName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
297+
invocation.putMetadata(Keys.RETURN_VAR_NAME, returnViName);
298+
if (f.allRefinementsTrue())
299+
rtc.getContext().addInstanceToContext(returnViName, retType, new Predicate(), invocation);
300+
}
301+
292302
if (target != null)
293303
AuxStateHandler.prepareInvocationTarget(rtc, target, invocation);
294304

295305
if (f.allRefinementsTrue()) {
296306
if (target != null)
297307
AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
298308

299-
invocation.putMetadata(Keys.REFINEMENT, new Predicate());
309+
// Expose `_ == returnViName` so the if-condition path variable ties to this return value.
310+
Predicate returnRef = returnViName != null
311+
? Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(returnViName))
312+
: new Predicate();
313+
invocation.putMetadata(Keys.REFINEMENT, returnRef);
300314
return map;
301315
}
302316

@@ -325,7 +339,8 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
325339
varName = v.getName();
326340
}
327341

328-
String viName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
342+
String viName = returnViName != null ? returnViName
343+
: String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter());
329344
VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(),
330345
methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVIEW!!
331346
if (varName != null && f.hasStateChange() && equalsThis)

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

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -209,12 +209,22 @@ private static Predicate createStatePredicate(String value, String targetClass,
209209
throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
210210
value);
211211
}
212+
CtTypeReference<?> returnType = null;
213+
if (isTo && e instanceof CtMethod<?> method) {
214+
CtTypeReference<?> mt = method.getType();
215+
if (mt != null && !"void".equals(mt.toString())) {
216+
p = p.substituteVariable("return", Keys.WILDCARD);
217+
returnType = mt;
218+
}
219+
}
212220
CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
213221
String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
214222
String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
215223
tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e);
216224
tc.getContext().addVarToContext(name, r, new Predicate(), e);
217225
tc.getContext().addVarToContext(nameOld, r, new Predicate(), e);
226+
if (returnType != null && !tc.getContext().hasVariable(Keys.WILDCARD))
227+
tc.getContext().addVarToContext(Keys.WILDCARD, returnType, new Predicate(), e);
218228
// TODO REVIEW!!
219229
// what is it for?
220230
Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
@@ -481,7 +491,10 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
481491
found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
482492
if (found && stateChange.hasTo()) {
483493
String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
484-
Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName)
494+
// Non-void: `_` is the return value; void: legacy alias for the new instance.
495+
String returnViName = (String) invocation.getMetadata(Keys.RETURN_VAR_NAME);
496+
String wildcardTarget = returnViName != null ? returnViName : newInstanceName;
497+
Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, wildcardTarget)
485498
.substituteVariable(Keys.THIS, newInstanceName);
486499
for (String s : map.keySet()) {
487500
transitionedState = transitionedState.substituteVariable(s, map.get(s));

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ public final class Keys {
44
public static final String REFINEMENT = "refinement";
55
public static final String REFINEMENT_SAT_CHECK = "refinement_sat_check";
66
public static final String TARGET = "target";
7+
public static final String RETURN_VAR_NAME = "return_var_name";
78
public static final String THIS = "this";
89
public static final String WILDCARD = "_";
910
public static final String OLD = "old";

0 commit comments

Comments
 (0)