Skip to content

Commit cd523df

Browse files
CatarinaGamboaCatarinaGamboa
authored
Fix if condition with no refinement (#210)
Before: When the guard condition had no refinement, we used the default of `true`. That, however, became a problem after joining ifs (with no else), since we assumed the condition was true. Now: We still create new fresh boolean but leave it empty, leaving the verification to the SMT solver. We also remove the branches that cannot complete normally from the If joining (`return`, `throw`, `break`, `continue`). (This can still be improved if Latte was used.) Example: ```java String loadFirstSetting(String path, String fallback) throws IOException { BufferedReader reader = new BufferedReader(new FileReader(path)); String header = reader.readLine(); // reader: open if (header.startsWith("#")) { // condition has no refinement String value = reader.readLine(); // reader: still open reader.close(); // reader: closed return value; } // Before: State Refinement Error here — the join assumed the // then-branch was taken, so reader was seen as `closed` and the // close() below failed its `!closed` precondition. // Now: the then-branch returns and contributes nothing to the join, // so reader is still `open` and the close() is accepted. reader.close(); // reader: closed return header; } ```
1 parent 65e663a commit cd523df

7 files changed

Lines changed: 272 additions & 11 deletions

File tree

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,14 @@ public void have1(int a) {
2525
int u = pos;
2626
}
2727

28+
public void haveAnd(int a, @Refinement("b > 5")int b) {
29+
@Refinement("pos > 0")
30+
int pos = 10;
31+
if (a > 0 && b > 0) {
32+
if (a > b) pos = a - b;
33+
}
34+
}
35+
2836
public static void main(String[] args) {
2937
@Refinement("_ < 10")
3038
int a = 5;

‎liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
package testSuite.classes.ts_bufferedreader_correct;
2+
import java.io.IOException;
3+
import java.io.Reader;
4+
import java.util.stream.Stream;
5+
6+
import liquidjava.specification.ExternalRefinementsFor;
7+
import liquidjava.specification.Refinement;
8+
import liquidjava.specification.RefinementAlias;
9+
import liquidjava.specification.StateRefinement;
10+
import liquidjava.specification.StateSet;
11+
12+
@RefinementAlias("NonNegative(int v) { v >= 0 }")
13+
@RefinementAlias("Positive(int v) { v > 0 }")
14+
@StateSet({"open", "marked", "closed"})
15+
@ExternalRefinementsFor("java.io.BufferedReader")
16+
public interface BufferedReaderRefinementsExpert {
17+
18+
@StateRefinement(to="open(this)")
19+
public void BufferedReader(Reader in);
20+
21+
@StateRefinement(to="open(this)")
22+
public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz);
23+
24+
@StateRefinement(from="open(this)")
25+
@StateRefinement(from="marked(this)")
26+
public int read();
27+
28+
@StateRefinement(from="open(this)")
29+
@StateRefinement(from="marked(this)")
30+
@Refinement(" _ >= -1")
31+
public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len);
32+
33+
@StateRefinement(from="open(this)")
34+
@StateRefinement(from="marked(this)")
35+
public String readLine() throws IOException;
36+
37+
@StateRefinement(from="open(this)")
38+
@StateRefinement(from="marked(this)")
39+
public boolean ready() throws IOException;
40+
41+
@StateRefinement(from="open(this)")
42+
@StateRefinement(from="marked(this)")
43+
public boolean markSupported();
44+
45+
@StateRefinement(from="open(this)", to="marked(this)")
46+
@StateRefinement(from="marked(this)")
47+
public void mark(@Refinement("NonNegative(_)") int readAheadLimit);
48+
49+
@StateRefinement(from="marked(this)", to="open(this)")
50+
public void reset();
51+
52+
@StateRefinement(from="!closed(this)", to="closed(this)")
53+
public void close();
54+
55+
@StateRefinement(from="open(this)")
56+
@StateRefinement(from="marked(this)")
57+
public Stream<String> lines();
58+
}

‎liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/ConfigLoader.java‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
package testSuite.classes.ts_bufferedreader_correct;
2+
import java.io.BufferedReader;
3+
import java.io.FileReader;
4+
import java.io.IOException;
5+
6+
// Regression test for unrefined conditions: each branch reads (open/marked) before
7+
// closing. The verifier must not assume the if-condition is unconditionally true,
8+
// otherwise it would conclude the reader is always closed by line 24 and flag the
9+
// readLine() call on line 31 as a state-refinement error.
10+
11+
class ConfigLoader {
12+
13+
String loadFirstSetting(String configPath, String defaultValue) throws IOException {
14+
BufferedReader reader = new BufferedReader(new FileReader(configPath));
15+
16+
String header = reader.readLine();
17+
if (header.isEmpty()) {
18+
reader.close();
19+
return defaultValue;
20+
}
21+
22+
if (header.startsWith("#")) {
23+
String value = reader.readLine();
24+
reader.close();
25+
return value;
26+
}
27+
28+
reader.close();
29+
return header;
30+
}
31+
}

‎liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java‎

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
package testSuite.classes.ts_bufferedreader_error;
2+
import java.io.IOException;
3+
import java.io.Reader;
4+
import java.util.stream.Stream;
5+
6+
import liquidjava.specification.ExternalRefinementsFor;
7+
import liquidjava.specification.Refinement;
8+
import liquidjava.specification.RefinementAlias;
9+
import liquidjava.specification.StateRefinement;
10+
import liquidjava.specification.StateSet;
11+
12+
@RefinementAlias("NonNegative(int v) { v >= 0 }")
13+
@RefinementAlias("Positive(int v) { v > 0 }")
14+
@StateSet({"open", "marked", "closed"})
15+
@ExternalRefinementsFor("java.io.BufferedReader")
16+
public interface BufferedReaderRefinementsExpert {
17+
18+
@StateRefinement(to="open(this)")
19+
public void BufferedReader(Reader in);
20+
21+
@StateRefinement(to="open(this)")
22+
public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz);
23+
24+
@StateRefinement(from="open(this)")
25+
@StateRefinement(from="marked(this)")
26+
public int read();
27+
28+
@StateRefinement(from="open(this)")
29+
@StateRefinement(from="marked(this)")
30+
@Refinement(" _ >= -1")
31+
public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len);
32+
33+
@StateRefinement(from="open(this)")
34+
@StateRefinement(from="marked(this)")
35+
public String readLine() throws IOException;
36+
37+
@StateRefinement(from="open(this)")
38+
@StateRefinement(from="marked(this)")
39+
public boolean ready() throws IOException;
40+
41+
@StateRefinement(from="open(this)")
42+
@StateRefinement(from="marked(this)")
43+
public boolean markSupported();
44+
45+
@StateRefinement(from="open(this)", to="marked(this)")
46+
@StateRefinement(from="marked(this)")
47+
public void mark(@Refinement("NonNegative(_)") int readAheadLimit);
48+
49+
@StateRefinement(from="marked(this)", to="open(this)")
50+
public void reset();
51+
52+
@StateRefinement(from="!closed(this)", to="closed(this)")
53+
public void close();
54+
55+
@StateRefinement(from="open(this)")
56+
@StateRefinement(from="marked(this)")
57+
public Stream<String> lines();
58+
}

‎liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
package testSuite.classes.ts_bufferedreader_error;
2+
import java.io.BufferedReader;
3+
import java.io.FileReader;
4+
import java.io.IOException;
5+
6+
// (A) The model is co-located: BufferedReaderRefinementsExpert (de-packaged
7+
// copy) declares states open/marked/closed on java.io.BufferedReader and
8+
// requires open or marked for read methods.
9+
//
10+
// (B) The client: load the first non-comment setting from a config file.
11+
// The author handles three branches — empty file, leading-comment header,
12+
// plain header — and tries to close the reader as soon as it is no longer
13+
// needed. In the leading-comment branch the close happens too early; the
14+
// follow-up readLine runs against a closed reader.
15+
16+
class ConfigLoader {
17+
18+
String loadFirstSetting(String configPath, String defaultValue) throws IOException {
19+
BufferedReader reader = new BufferedReader(new FileReader(configPath));
20+
21+
String header = reader.readLine();
22+
if (header.isEmpty()) {
23+
reader.close();
24+
return defaultValue;
25+
}
26+
27+
if (header.startsWith("#")) {
28+
// Header was a comment — the real value is on the next line.
29+
reader.close();
30+
return reader.readLine(); // State Refinement Error
31+
}
32+
33+
reader.close();
34+
return header;
35+
}
36+
37+
String loadFirstSetting2(String configPath, String defaultValue) throws IOException {
38+
BufferedReader reader = new BufferedReader(new FileReader(configPath));
39+
40+
String header = reader.readLine();
41+
if (header.isEmpty()) {
42+
reader.close();
43+
// no return here
44+
}
45+
reader.close(); // State Refinement Error
46+
return header;
47+
}
48+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,8 @@ void saveInstanceElse() {
130130
Optional<VariableInstance> getIfInstanceCombination(int counter, Predicate cond) {
131131
if (ifCombiner.isEmpty() || (!has(ifthenIndex) && !has(ifelseIndex) && !has(ifbeforeIndex)))
132132
return Optional.empty();
133+
if (has(ifbeforeIndex) && !has(ifthenIndex) && !has(ifelseIndex))
134+
return Optional.empty();
133135

134136
String nName = String.format("#%s_%d", super.getName(), counter);
135137
Predicate ref = new Predicate();

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

Lines changed: 67 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,10 @@
2424
import spoon.reflect.code.CtArrayWrite;
2525
import spoon.reflect.code.CtAssignment;
2626
import spoon.reflect.code.CtBinaryOperator;
27+
import spoon.reflect.code.CtBlock;
28+
import spoon.reflect.code.CtBreak;
2729
import spoon.reflect.code.CtConditional;
30+
import spoon.reflect.code.CtContinue;
2831
import spoon.reflect.code.CtConstructorCall;
2932
import spoon.reflect.code.CtExpression;
3033
import spoon.reflect.code.CtFieldRead;
@@ -36,7 +39,9 @@
3639
import spoon.reflect.code.CtNewArray;
3740
import spoon.reflect.code.CtNewClass;
3841
import spoon.reflect.code.CtReturn;
42+
import spoon.reflect.code.CtStatement;
3943
import spoon.reflect.code.CtThisAccess;
44+
import spoon.reflect.code.CtThrow;
4045
import spoon.reflect.code.CtUnaryOperator;
4146
import spoon.reflect.code.CtVariableAccess;
4247
import spoon.reflect.code.CtVariableRead;
@@ -336,18 +341,26 @@ public void visitCtIf(CtIf ifElement) {
336341
CtExpression<Boolean> exp = ifElement.getCondition();
337342
Predicate expRefs = getExpressionRefinements(exp);
338343

339-
String freshVarName = String.format(Formats.FRESH, context.getCounter());
340-
expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName);
341-
Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
342-
expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
344+
String pathVarName = String.format(Formats.FRESH, context.getCounter());
345+
RefinedVariable freshRV;
346+
if (isUninformativeCondition(expRefs, exp)) {
347+
// No refinement means the condition is unknown, not true: model it as a fresh
348+
// boolean so the SMT solver may pick either truth value for each branch.
349+
expRefs = Predicate.createVar(pathVarName);
350+
freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp);
351+
} else {
352+
expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName);
353+
Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
354+
expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
355+
356+
freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp);
357+
}
343358

344359
// TODO Change in future
345360
if (expRefs.getVariableNames().contains("null")) {
346361
expRefs = new Predicate();
347362
}
348363

349-
RefinedVariable freshRV = context.addInstanceToContext(freshVarName, factory.Type().INTEGER_PRIMITIVE, expRefs,
350-
exp);
351364
vcChecker.addPathVariable(freshRV);
352365

353366
context.variablesNewIfCombination();
@@ -357,19 +370,21 @@ public void visitCtIf(CtIf ifElement) {
357370
// VISIT THEN
358371
context.enterContext();
359372
visitCtBlock(ifElement.getThenStatement());
360-
context.variablesSetThenIf();
373+
if (canCompleteNormally(ifElement.getThenStatement())) {
374+
context.variablesSetThenIf();
375+
}
361376
contextHistory.saveContext(ifElement.getThenStatement(), context);
362377
context.exitContext();
363378

364379
// VISIT ELSE
365380
if (ifElement.getElseStatement() != null) {
366-
context.getVariableByName(freshVarName);
367-
// expRefs = expRefs.negate();
368-
context.newRefinementToVariableInContext(freshVarName, expRefs.negate());
381+
context.newRefinementToVariableInContext(pathVarName, expRefs.negate());
369382

370383
context.enterContext();
371384
visitCtBlock(ifElement.getElseStatement());
372-
context.variablesSetElseIf();
385+
if (canCompleteNormally(ifElement.getElseStatement())) {
386+
context.variablesSetElseIf();
387+
}
373388
contextHistory.saveContext(ifElement.getElseStatement(), context);
374389
context.exitContext();
375390
}
@@ -380,6 +395,47 @@ public void visitCtIf(CtIf ifElement) {
380395
context.variablesFinishIfCombination();
381396
}
382397

398+
/**
399+
* A condition is uninformative when its refinement is the trivial {@code true} predicate yet the expression itself
400+
* is not a boolean literal — i.e. the verifier has no symbolic information to relate the branch to. Treating such a
401+
* condition as {@code true} would force every if-then to be taken, producing spurious state-refinement errors.
402+
*/
403+
private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpression<Boolean> condition) {
404+
if (!conditionRefinement.isBooleanTrue())
405+
return false;
406+
return !(condition instanceof CtLiteral<?> literal && literal.getValue() instanceof Boolean);
407+
}
408+
409+
/**
410+
* Best-effort normal-completion check (JLS §14.21): branches that always {@code return}, {@code throw},
411+
* {@code break} or {@code continue} cannot contribute state to code following the {@code if}, so their post-context
412+
* must be discarded at the join.
413+
*
414+
* <p>
415+
* Not currently handled (treated conservatively as completing normally): {@code switch} where every case exits,
416+
* labeled {@code break}/{@code continue} targets, {@code try}/{@code catch}/{@code finally} flow, and infinite
417+
* loops such as {@code while (true)}. Extending this list only tightens precision.
418+
*/
419+
private boolean canCompleteNormally(CtStatement statement) {
420+
if (statement == null)
421+
return true;
422+
if (statement instanceof CtReturn<?> || statement instanceof CtThrow || statement instanceof CtBreak
423+
|| statement instanceof CtContinue)
424+
return false;
425+
if (statement instanceof CtBlock<?> block) {
426+
List<CtStatement> statements = block.getStatements();
427+
return statements.isEmpty() || canCompleteNormally(statements.get(statements.size() - 1));
428+
}
429+
if (statement instanceof CtIf nestedIf) {
430+
CtStatement elseStatement = nestedIf.getElseStatement();
431+
// No else means the false path always falls through.
432+
if (elseStatement == null)
433+
return true;
434+
return canCompleteNormally(nestedIf.getThenStatement()) || canCompleteNormally(elseStatement);
435+
}
436+
return true;
437+
}
438+
383439
@Override
384440
public <T> void visitCtArrayWrite(CtArrayWrite<T> arrayWrite) {
385441
super.visitCtArrayWrite(arrayWrite);

0 commit comments

Comments
 (0)