diff --git a/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java b/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java index c7fa9119..9e5ed044 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectIfThen.java @@ -25,6 +25,14 @@ public void have1(int a) { int u = pos; } + public void haveAnd(int a, @Refinement("b > 5")int b) { + @Refinement("pos > 0") + int pos = 10; + if (a > 0 && b > 0) { + if (a > b) pos = a - b; + } + } + public static void main(String[] args) { @Refinement("_ < 10") int a = 5; diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java new file mode 100644 index 00000000..6a437f45 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/BufferedReaderRefinementsExpert.java @@ -0,0 +1,58 @@ +package testSuite.classes.ts_bufferedreader_correct; +import java.io.IOException; +import java.io.Reader; +import java.util.stream.Stream; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("NonNegative(int v) { v >= 0 }") +@RefinementAlias("Positive(int v) { v > 0 }") +@StateSet({"open", "marked", "closed"}) +@ExternalRefinementsFor("java.io.BufferedReader") +public interface BufferedReaderRefinementsExpert { + + @StateRefinement(to="open(this)") + public void BufferedReader(Reader in); + + @StateRefinement(to="open(this)") + public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public int read(); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + @Refinement(" _ >= -1") + public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public String readLine() throws IOException; + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public boolean ready() throws IOException; + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public boolean markSupported(); + + @StateRefinement(from="open(this)", to="marked(this)") + @StateRefinement(from="marked(this)") + public void mark(@Refinement("NonNegative(_)") int readAheadLimit); + + @StateRefinement(from="marked(this)", to="open(this)") + public void reset(); + + @StateRefinement(from="!closed(this)", to="closed(this)") + public void close(); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public Stream lines(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/ConfigLoader.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/ConfigLoader.java new file mode 100644 index 00000000..eb8e1a74 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_correct/ConfigLoader.java @@ -0,0 +1,31 @@ +package testSuite.classes.ts_bufferedreader_correct; +import java.io.BufferedReader; +import java.io.FileReader; +import java.io.IOException; + +// Regression test for unrefined conditions: each branch reads (open/marked) before +// closing. The verifier must not assume the if-condition is unconditionally true, +// otherwise it would conclude the reader is always closed by line 24 and flag the +// readLine() call on line 31 as a state-refinement error. + +class ConfigLoader { + + String loadFirstSetting(String configPath, String defaultValue) throws IOException { + BufferedReader reader = new BufferedReader(new FileReader(configPath)); + + String header = reader.readLine(); + if (header.isEmpty()) { + reader.close(); + return defaultValue; + } + + if (header.startsWith("#")) { + String value = reader.readLine(); + reader.close(); + return value; + } + + reader.close(); + return header; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java new file mode 100644 index 00000000..a6e87a44 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/BufferedReaderRefinementsExpert.java @@ -0,0 +1,58 @@ +package testSuite.classes.ts_bufferedreader_error; +import java.io.IOException; +import java.io.Reader; +import java.util.stream.Stream; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@RefinementAlias("NonNegative(int v) { v >= 0 }") +@RefinementAlias("Positive(int v) { v > 0 }") +@StateSet({"open", "marked", "closed"}) +@ExternalRefinementsFor("java.io.BufferedReader") +public interface BufferedReaderRefinementsExpert { + + @StateRefinement(to="open(this)") + public void BufferedReader(Reader in); + + @StateRefinement(to="open(this)") + public void BufferedReader(Reader in, @Refinement("Positive(_)") int sz); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public int read(); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + @Refinement(" _ >= -1") + public int read(char[] cbuf, @Refinement("NonNegative(_)") int off, @Refinement("NonNegative(_)") int len); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public String readLine() throws IOException; + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public boolean ready() throws IOException; + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public boolean markSupported(); + + @StateRefinement(from="open(this)", to="marked(this)") + @StateRefinement(from="marked(this)") + public void mark(@Refinement("NonNegative(_)") int readAheadLimit); + + @StateRefinement(from="marked(this)", to="open(this)") + public void reset(); + + @StateRefinement(from="!closed(this)", to="closed(this)") + public void close(); + + @StateRefinement(from="open(this)") + @StateRefinement(from="marked(this)") + public Stream lines(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java new file mode 100644 index 00000000..bc3f1810 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/ts_bufferedreader_error/ConfigLoader.java @@ -0,0 +1,48 @@ +package testSuite.classes.ts_bufferedreader_error; +import java.io.BufferedReader; +import java.io.FileReader; +import java.io.IOException; + +// (A) The model is co-located: BufferedReaderRefinementsExpert (de-packaged +// copy) declares states open/marked/closed on java.io.BufferedReader and +// requires open or marked for read methods. +// +// (B) The client: load the first non-comment setting from a config file. +// The author handles three branches — empty file, leading-comment header, +// plain header — and tries to close the reader as soon as it is no longer +// needed. In the leading-comment branch the close happens too early; the +// follow-up readLine runs against a closed reader. + +class ConfigLoader { + + String loadFirstSetting(String configPath, String defaultValue) throws IOException { + BufferedReader reader = new BufferedReader(new FileReader(configPath)); + + String header = reader.readLine(); + if (header.isEmpty()) { + reader.close(); + return defaultValue; + } + + if (header.startsWith("#")) { + // Header was a comment — the real value is on the next line. + reader.close(); + return reader.readLine(); // State Refinement Error + } + + reader.close(); + return header; + } + + String loadFirstSetting2(String configPath, String defaultValue) throws IOException { + BufferedReader reader = new BufferedReader(new FileReader(configPath)); + + String header = reader.readLine(); + if (header.isEmpty()) { + reader.close(); + // no return here + } + reader.close(); // State Refinement Error + return header; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java index 8ea8f67e..cfed765d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -130,6 +130,8 @@ void saveInstanceElse() { Optional getIfInstanceCombination(int counter, Predicate cond) { if (ifCombiner.isEmpty() || (!has(ifthenIndex) && !has(ifelseIndex) && !has(ifbeforeIndex))) return Optional.empty(); + if (has(ifbeforeIndex) && !has(ifthenIndex) && !has(ifelseIndex)) + return Optional.empty(); String nName = String.format("#%s_%d", super.getName(), counter); Predicate ref = new Predicate(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index c1dace74..50ba05f5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -24,7 +24,10 @@ import spoon.reflect.code.CtArrayWrite; import spoon.reflect.code.CtAssignment; import spoon.reflect.code.CtBinaryOperator; +import spoon.reflect.code.CtBlock; +import spoon.reflect.code.CtBreak; import spoon.reflect.code.CtConditional; +import spoon.reflect.code.CtContinue; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; @@ -36,7 +39,9 @@ import spoon.reflect.code.CtNewArray; import spoon.reflect.code.CtNewClass; import spoon.reflect.code.CtReturn; +import spoon.reflect.code.CtStatement; import spoon.reflect.code.CtThisAccess; +import spoon.reflect.code.CtThrow; import spoon.reflect.code.CtUnaryOperator; import spoon.reflect.code.CtVariableAccess; import spoon.reflect.code.CtVariableRead; @@ -336,18 +341,26 @@ public void visitCtIf(CtIf ifElement) { CtExpression exp = ifElement.getCondition(); Predicate expRefs = getExpressionRefinements(exp); - String freshVarName = String.format(Formats.FRESH, context.getCounter()); - expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName); - Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); - expRefs = Predicate.createConjunction(expRefs, lastExpRefs); + String pathVarName = String.format(Formats.FRESH, context.getCounter()); + RefinedVariable freshRV; + if (isUninformativeCondition(expRefs, exp)) { + // No refinement means the condition is unknown, not true: model it as a fresh + // boolean so the SMT solver may pick either truth value for each branch. + expRefs = Predicate.createVar(pathVarName); + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp); + } else { + expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName); + Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); + expRefs = Predicate.createConjunction(expRefs, lastExpRefs); + + freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp); + } // TODO Change in future if (expRefs.getVariableNames().contains("null")) { expRefs = new Predicate(); } - RefinedVariable freshRV = context.addInstanceToContext(freshVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, - exp); vcChecker.addPathVariable(freshRV); context.variablesNewIfCombination(); @@ -357,19 +370,21 @@ public void visitCtIf(CtIf ifElement) { // VISIT THEN context.enterContext(); visitCtBlock(ifElement.getThenStatement()); - context.variablesSetThenIf(); + if (canCompleteNormally(ifElement.getThenStatement())) { + context.variablesSetThenIf(); + } contextHistory.saveContext(ifElement.getThenStatement(), context); context.exitContext(); // VISIT ELSE if (ifElement.getElseStatement() != null) { - context.getVariableByName(freshVarName); - // expRefs = expRefs.negate(); - context.newRefinementToVariableInContext(freshVarName, expRefs.negate()); + context.newRefinementToVariableInContext(pathVarName, expRefs.negate()); context.enterContext(); visitCtBlock(ifElement.getElseStatement()); - context.variablesSetElseIf(); + if (canCompleteNormally(ifElement.getElseStatement())) { + context.variablesSetElseIf(); + } contextHistory.saveContext(ifElement.getElseStatement(), context); context.exitContext(); } @@ -380,6 +395,47 @@ public void visitCtIf(CtIf ifElement) { context.variablesFinishIfCombination(); } + /** + * A condition is uninformative when its refinement is the trivial {@code true} predicate yet the expression itself + * is not a boolean literal — i.e. the verifier has no symbolic information to relate the branch to. Treating such a + * condition as {@code true} would force every if-then to be taken, producing spurious state-refinement errors. + */ + private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpression condition) { + if (!conditionRefinement.isBooleanTrue()) + return false; + return !(condition instanceof CtLiteral literal && literal.getValue() instanceof Boolean); + } + + /** + * Best-effort normal-completion check (JLS §14.21): branches that always {@code return}, {@code throw}, + * {@code break} or {@code continue} cannot contribute state to code following the {@code if}, so their post-context + * must be discarded at the join. + * + *

+ * Not currently handled (treated conservatively as completing normally): {@code switch} where every case exits, + * labeled {@code break}/{@code continue} targets, {@code try}/{@code catch}/{@code finally} flow, and infinite + * loops such as {@code while (true)}. Extending this list only tightens precision. + */ + private boolean canCompleteNormally(CtStatement statement) { + if (statement == null) + return true; + if (statement instanceof CtReturn || statement instanceof CtThrow || statement instanceof CtBreak + || statement instanceof CtContinue) + return false; + if (statement instanceof CtBlock block) { + List statements = block.getStatements(); + return statements.isEmpty() || canCompleteNormally(statements.get(statements.size() - 1)); + } + if (statement instanceof CtIf nestedIf) { + CtStatement elseStatement = nestedIf.getElseStatement(); + // No else means the false path always falls through. + if (elseStatement == null) + return true; + return canCompleteNormally(nestedIf.getThenStatement()) || canCompleteNormally(elseStatement); + } + return true; + } + @Override public void visitCtArrayWrite(CtArrayWrite arrayWrite) { super.visitCtArrayWrite(arrayWrite);