Fix if condition with no refinement

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;

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<String> lines();
+}

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;
+    }
+}

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<String> lines();
+}

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;
+    }
+}

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

@@ -130,6 +130,8 @@ void saveInstanceElse() {
     Optional<VariableInstance> 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();

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<Boolean> 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<Boolean> 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.
+     *
+     * <p>
+     * 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<CtStatement> 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 <T> void visitCtArrayWrite(CtArrayWrite<T> arrayWrite) {
         super.visitCtArrayWrite(arrayWrite);