Skip to content

Commit ed490d3

Browse files
CatarinaGamboaCatarinaGamboa
committed
implement derived states as part of the simplification process
1 parent a2725f3 commit ed490d3

13 files changed

Lines changed: 783 additions & 79 deletions

File tree

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

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
package testSuite.classes.imagewrite_correct;
2+
3+
import java.util.Locale;
4+
5+
import javax.imageio.ImageWriteParam;
6+
7+
import liquidjava.specification.ExternalRefinementsFor;
8+
import liquidjava.specification.Refinement;
9+
import liquidjava.specification.StateRefinement;
10+
import liquidjava.specification.StateSet;
11+
12+
/**
13+
* External typestate specification for {@code javax.imageio.ImageWriteParam}.
14+
*
15+
* <p>
16+
* The class is modelled as two independent ghost-state dimensions — tiling and compression — so a configuration error
17+
* in one dimension does not mask the other. The conditional {@code setTilingMode} / {@code setCompressionMode}
18+
* transitions only reach the {@code *Explicit} state when called with {@code MODE_EXPLICIT}; any other mode leaves the
19+
* param in its {@code start*} state, which the dimension-specific setters reject.
20+
*/
21+
@StateSet({ "startTiling", "tilingExplicit", "tilingSet" })
22+
@StateSet({ "startCompression", "compressionExplicit", "compressionSet" })
23+
@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
24+
public interface ImageWriteParamsRefinements {
25+
26+
// Constructor
27+
@StateRefinement(to = "startTiling(this) && startCompression(this)")
28+
void ImageWriteParam(Locale locale);
29+
30+
// Tiling related methods
31+
32+
@StateRefinement(to = "(mode == ImageWriteParam.MODE_EXPLICIT)? tilingExplicit(this) : startTiling(this)")
33+
void setTilingMode(int mode);
34+
35+
@StateRefinement(from = "tilingExplicit(this)", to = "tilingSet(this)")
36+
@StateRefinement(from = "tilingSet(this)", to = "tilingSet(this)")
37+
void setTiling(@Refinement("_ > 0") int tileWidth, @Refinement("_ > 0") int tileHeight, int tileGridXOffset,
38+
int tileGridYOffset);
39+
40+
@StateRefinement(from = "tilingSet(this)")
41+
int getTileGridXOffset();
42+
43+
@StateRefinement(from = "tilingSet(this)")
44+
int getTileGridYOffset();
45+
46+
@StateRefinement(from = "tilingSet(this)")
47+
int getTileHeight();
48+
49+
@StateRefinement(from = "tilingSet(this)")
50+
int getTileWidth();
51+
52+
@StateRefinement(from = "tilingExplicit(this)")
53+
@StateRefinement(from = "tilingSet(this)", to = "tilingExplicit(this)")
54+
void unsetTiling();
55+
56+
void setProgressiveMode(@Refinement("ImageWriteParam.MODE_DISABLED == mode || mode == ImageWriteParam.MODE_DEFAULT || mode == ImageWriteParam.MODE_COPY_FROM_METADATA") int mode);
57+
58+
// Compression related methods
59+
60+
@StateRefinement(to = "mode == ImageWriteParam.MODE_EXPLICIT? compressionExplicit(this) : startCompression(this)")
61+
void setCompressionMode(int mode);
62+
63+
@StateRefinement(from = "compressionExplicit(this)")
64+
@StateRefinement(from = "compressionSet(this)")
65+
void setCompressionQuality(@Refinement("_ >= 0.0 && _ <= 1.0") float quality);
66+
67+
@StateRefinement(from = "compressionExplicit(this)")
68+
@StateRefinement(from = "compressionSet(this)")
69+
String getCompressionType();
70+
71+
@StateRefinement(from = "compressionExplicit(this)", to = "compressionSet(this)")
72+
void setCompressionType(String compressionType);
73+
74+
@StateRefinement(from = "compressionExplicit(this)")
75+
@StateRefinement(from = "compressionSet(this)", to = "compressionExplicit(this)")
76+
void unsetCompression();
77+
78+
@StateRefinement(from = "compressionSet(this)")
79+
String getLocalizedCompressionTypeName();
80+
81+
@StateRefinement(from = "compressionExplicit(this)")
82+
@StateRefinement(from = "compressionSet(this)")
83+
boolean isCompressionLossless();
84+
85+
@StateRefinement(from = "compressionExplicit(this)")
86+
@StateRefinement(from = "compressionSet(this)")
87+
float getCompressionQuality();
88+
}

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

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
package testSuite.classes.imagewrite_correct;
2+
3+
import java.util.Locale;
4+
5+
import javax.imageio.ImageWriteParam;
6+
7+
/**
8+
* A JPEG export pipeline configured correctly against {@link ImageWriteParamsRefinements}.
9+
*
10+
* <p>
11+
* Both ghost-state dimensions are driven through their full transition path: each dimension's mode is set to
12+
* {@code MODE_EXPLICIT} before the dimension-specific setters run, and {@code getTileWidth} is reached only after
13+
* {@code setTiling} has moved the param into {@code tilingSet}. No state refinement is violated.
14+
*/
15+
class JpegExporter {
16+
17+
ImageWriteParam buildJpegParam() {
18+
ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
19+
param.setTilingMode(ImageWriteParam.MODE_EXPLICIT);
20+
param.setTiling(10, 30, 10, 30);
21+
param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT);
22+
param.setCompressionQuality(0.85f);
23+
return param;
24+
}
25+
26+
int firstTileWidth() {
27+
ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
28+
param.setTilingMode(ImageWriteParam.MODE_EXPLICIT);
29+
param.setTiling(8, 8, 0, 0);
30+
return param.getTileWidth();
31+
}
32+
}

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

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
package testSuite.classes.imagewrite_error;
2+
3+
import java.util.Locale;
4+
5+
import javax.imageio.ImageWriteParam;
6+
7+
import liquidjava.specification.ExternalRefinementsFor;
8+
import liquidjava.specification.Refinement;
9+
import liquidjava.specification.StateRefinement;
10+
import liquidjava.specification.StateSet;
11+
12+
/**
13+
* External typestate specification for {@code javax.imageio.ImageWriteParam}.
14+
*
15+
* <p>
16+
* The class is modelled as two independent ghost-state dimensions — tiling and compression — so a configuration error
17+
* in one dimension does not mask the other. The conditional {@code setTilingMode} / {@code setCompressionMode}
18+
* transitions only reach the {@code *Explicit} state when called with {@code MODE_EXPLICIT}; any other mode leaves the
19+
* param in its {@code start*} state, which the dimension-specific setters reject.
20+
*/
21+
@StateSet({ "startTiling", "tilingExplicit", "tilingSet" })
22+
@StateSet({ "startCompression", "compressionExplicit", "compressionSet" })
23+
@ExternalRefinementsFor("javax.imageio.ImageWriteParam")
24+
public interface ImageWriteParamsRefinements {
25+
26+
// Constructor
27+
@StateRefinement(to = "startTiling(this) && startCompression(this)")
28+
void ImageWriteParam(Locale locale);
29+
30+
// Tiling related methods
31+
32+
@StateRefinement(to = "(mode == ImageWriteParam.MODE_EXPLICIT)? tilingExplicit(this) : startTiling(this)")
33+
void setTilingMode(int mode);
34+
35+
@StateRefinement(from = "tilingExplicit(this)", to = "tilingSet(this)")
36+
@StateRefinement(from = "tilingSet(this)", to = "tilingSet(this)")
37+
void setTiling(@Refinement("_ > 0") int tileWidth, @Refinement("_ > 0") int tileHeight, int tileGridXOffset,
38+
int tileGridYOffset);
39+
40+
@StateRefinement(from = "tilingSet(this)")
41+
int getTileGridXOffset();
42+
43+
@StateRefinement(from = "tilingSet(this)")
44+
int getTileGridYOffset();
45+
46+
@StateRefinement(from = "tilingSet(this)")
47+
int getTileHeight();
48+
49+
@StateRefinement(from = "tilingSet(this)")
50+
int getTileWidth();
51+
52+
@StateRefinement(from = "tilingExplicit(this)")
53+
@StateRefinement(from = "tilingSet(this)", to = "tilingExplicit(this)")
54+
void unsetTiling();
55+
56+
void setProgressiveMode(@Refinement("ImageWriteParam.MODE_DISABLED == mode || mode == ImageWriteParam.MODE_DEFAULT || mode == ImageWriteParam.MODE_COPY_FROM_METADATA") int mode);
57+
58+
// Compression related methods
59+
60+
@StateRefinement(to = "mode == ImageWriteParam.MODE_EXPLICIT? compressionExplicit(this) : startCompression(this)")
61+
void setCompressionMode(int mode);
62+
63+
@StateRefinement(from = "compressionExplicit(this)")
64+
@StateRefinement(from = "compressionSet(this)")
65+
void setCompressionQuality(@Refinement("_ >= 0.0 && _ <= 1.0") float quality);
66+
67+
@StateRefinement(from = "compressionExplicit(this)")
68+
@StateRefinement(from = "compressionSet(this)")
69+
String getCompressionType();
70+
71+
@StateRefinement(from = "compressionExplicit(this)", to = "compressionSet(this)")
72+
void setCompressionType(String compressionType);
73+
74+
@StateRefinement(from = "compressionExplicit(this)")
75+
@StateRefinement(from = "compressionSet(this)", to = "compressionExplicit(this)")
76+
void unsetCompression();
77+
78+
@StateRefinement(from = "compressionSet(this)")
79+
String getLocalizedCompressionTypeName();
80+
81+
@StateRefinement(from = "compressionExplicit(this)")
82+
@StateRefinement(from = "compressionSet(this)")
83+
boolean isCompressionLossless();
84+
85+
@StateRefinement(from = "compressionExplicit(this)")
86+
@StateRefinement(from = "compressionSet(this)")
87+
float getCompressionQuality();
88+
}

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

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
package testSuite.classes.imagewrite_error;
2+
3+
import java.util.Locale;
4+
5+
import javax.imageio.ImageWriteParam;
6+
7+
/**
8+
* A JPEG export pipeline configured against {@link ImageWriteParamsRefinements}.
9+
*
10+
* <p>
11+
* The author did configure a tiling mode — but passed {@code MODE_DEFAULT} instead of {@code MODE_EXPLICIT}. The spec's
12+
* conditional transition leaves the param in {@code startTiling} for any non-explicit mode, so {@code setTiling}
13+
* (which requires {@code tilingExplicit} or {@code tilingSet}) violates its from-state.
14+
*
15+
* <p>
16+
* The found-state threads the same {@code param} across SSA versions joined by internal {@code stateN(x) == stateN(y)}
17+
* equalities; state derivation rewrites those into developer-facing typestate names for the diagnostic.
18+
*/
19+
class JpegExporter {
20+
21+
ImageWriteParam buildJpegParam() {
22+
ImageWriteParam param = new ImageWriteParam(Locale.getDefault());
23+
param.setTilingMode(ImageWriteParam.MODE_DEFAULT);
24+
param.setCompressionMode(ImageWriteParam.MODE_EXPLICIT);
25+
param.setCompressionQuality(0.85f);
26+
param.setTiling(10, 30, 10, 30); // State Refinement Error
27+
return param;
28+
}
29+
}

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -391,10 +391,11 @@ protected void throwStateRefinementError(SourcePosition position, Predicate foun
391391
gatherVariables(found, lrv, mainVars);
392392
TranslationTable map = new TranslationTable();
393393
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
394-
Predicate foundConjunction = new Predicate(foundState.toConjunctions().simplify(context).getValue())
395-
.addDerivedStateEqualities(context.getGhostStates());
396-
throw new StateRefinementError(position, expected.simplify(context), foundConjunction.simplify(context), map,
397-
customMessage);
394+
// simplify(context) folds the found-state predicate and, in the same pass, rewrites internal
395+
// ghost-state equalities into developer-facing state predicates (see ExpressionSimplifier /
396+
// StateDerivation). The resulting ValDerivationNode keeps the provenance of that rewrite.
397+
throw new StateRefinementError(position, expected.simplify(context),
398+
foundState.toConjunctions().simplify(context), map, customMessage);
398399
}
399400

400401
protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 3 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -221,70 +221,6 @@ public Predicate changeStatesToRefinements(List<GhostState> ghostState, String[]
221221
return new Predicate(e);
222222
}
223223

224-
public Predicate addDerivedStateEqualities(List<GhostState> ghostStates) {
225-
List<Expression> conjuncts = exp.getConjuncts();
226-
Map<String, String> stateToInternalState = new HashMap<>();
227-
for (GhostState gs : ghostStates) {
228-
if (gs.getRefinement() == null)
229-
continue;
230-
Expression ref = gs.getRefinement().getExpression();
231-
if (ref instanceof GroupExpression ge)
232-
ref = ge.getExpression();
233-
if (ref instanceof BinaryExpression be && Ops.EQ.equals(be.getOperator())) {
234-
FunctionInvocation state = functionInvocation(be.getFirstOperand());
235-
if (state == null)
236-
state = functionInvocation(be.getSecondOperand());
237-
if (state != null)
238-
stateToInternalState.put(gs.getName(), state.getName());
239-
}
240-
}
241-
242-
Predicate result = new Predicate();
243-
List<Predicate> derivedStates = new ArrayList<>();
244-
for (Expression conjunct : conjuncts) {
245-
boolean replaced = false;
246-
if (conjunct instanceof BinaryExpression be && Ops.EQ.equals(be.getOperator())) {
247-
FunctionInvocation left = functionInvocation(be.getFirstOperand());
248-
FunctionInvocation right = functionInvocation(be.getSecondOperand());
249-
if (left != null && right != null && left.getArgs().size() == 1 && right.getArgs().size() == 1
250-
&& sameName(left.getName(), right.getName())) {
251-
for (Expression stateConjunct : conjuncts) {
252-
FunctionInvocation state = functionInvocation(stateConjunct);
253-
if (state == null || state.getArgs().size() != 1)
254-
continue;
255-
for (Map.Entry<String, String> stateName : stateToInternalState.entrySet()) {
256-
if (!sameName(stateName.getKey(), state.getName())
257-
|| !sameName(stateName.getValue(), left.getName()))
258-
continue;
259-
260-
Expression known = state.getArgs().get(0);
261-
Expression target = known.equals(left.getArgs().get(0)) ? right.getArgs().get(0)
262-
: known.equals(right.getArgs().get(0)) ? left.getArgs().get(0) : null;
263-
if (target != null) {
264-
derivedStates.add(createInvocation(state.getName(), new Predicate(target)));
265-
replaced = true;
266-
}
267-
}
268-
}
269-
}
270-
}
271-
if (!replaced)
272-
result = createConjunction(result, new Predicate(conjunct));
273-
}
274-
for (Predicate derivedState : derivedStates)
275-
result = createConjunction(result, derivedState);
276-
return result;
277-
}
278-
279-
private static FunctionInvocation functionInvocation(Expression exp) {
280-
return exp instanceof GroupExpression ge ? functionInvocation(ge.getExpression())
281-
: exp instanceof FunctionInvocation fi ? fi : null;
282-
}
283-
284-
private static boolean sameName(String first, String second) {
285-
return first.equals(second) || Utils.getSimpleName(first).equals(Utils.getSimpleName(second));
286-
}
287-
288224
public boolean isBooleanTrue() {
289225
return exp.isBooleanTrue();
290226
}
@@ -321,8 +257,9 @@ public ValDerivationNode simplify(Context context) {
321257
for (AliasWrapper aw : context.getAliases()) {
322258
aliases.put(aw.getName(), aw.createAliasDTO());
323259
}
324-
// simplify expression
325-
ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases);
260+
// simplify expression — ghost states let the simplifier rewrite internal state equalities into
261+
// developer-facing state predicates for error messages
262+
ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases, context.getGhostStates());
326263
DebugLog.simplification(this.getExpression(), result.getValue());
327264
return result;
328265
}

0 commit comments

Comments
 (0)