From 7f023ee6ce70227fc08524b1c6f3ee2c2f029bae Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Fri, 2 Oct 2026 13:56:48 +0100 Subject: [PATCH 1/3] Assume loop conditions in loop bodies, soundly (#306) The condition of a while/for loop is now assumed in its body as a path condition, like the condition of an if, so `while (n > 0) use(n)` verifies. Loops were previously checked as if the body ran exactly once with the pre-loop values, and the for update was visited before the body. To keep the new assumption sound, a loop is now checked for one arbitrary iteration: - variables written in the loop are havocked (keep only their declared refinement, which every write re-checks) before the loop and after it; - for loops visit init, condition, body, then update; - do-while does not assume the condition in the body; - path conditions added inside a loop (its condition, `if (..) break;`) are dropped after it; - conditions that write variables (e.g. `(n = read()) > 0`) assume nothing. Also drop path conditions on a variable when it is incremented or decremented (`i++`), as already done for assignments: before, `if (i < 10) { i++; use(i); }` wrongly assumed `i < 10` for the new value. Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectLoopCondition.java | 76 +++++++++++++ .../java/testSuite/ErrorLoopCondition.java | 80 ++++++++++++++ .../RefinementTypeChecker.java | 104 +++++++++++++++++- .../refinement_checker/TypeChecker.java | 10 ++ .../refinement_checker/VCChecker.java | 9 ++ .../general_checkers/OperationsChecker.java | 1 + 6 files changed, 275 insertions(+), 5 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java new file mode 100644 index 00000000..2043e467 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java @@ -0,0 +1,76 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class CorrectLoopCondition { + + @Refinement("_ >= -1") + static int read() { + return -1; + } + + static void write(@Refinement("_ > 0") int n) {} + + static void open(@Refinement("_ >= 0 && _ <= 65535") int port) {} + + static void lessThanTen(@Refinement("_ < 10") int n) {} + + // the condition holds in the body, and again after each re-assignment once it is re-checked + static void readLoop() { + int n = read(); + while (n > 0) { + write(n); + n = read(); + } + } + + // the loop variable keeps its declared refinement across iterations; the condition gives the upper bound + static void scanFrom(int start) { + if (start <= 0) { + return; + } + for (@Refinement("_ > 0") int i = start; i < 65535; i++) { + open(i); + } + } + + // the update runs after the body: the body sees i < 10, not i + 1 + static void updateAfterBody() { + for (@Refinement("_ >= 0") int i = 0; i < 10; i++) { + lessThanTen(i); + } + } + + // the condition is assumed on a variable the body does not modify + static void unmodifiedVariable(int limit) { + int count = 0; + while (limit > 0 && count < 10) { + write(limit); + count = count + 1; + } + } + + // conditions of nested loops hold together in the inner body + static void nestedLoops(int a, int b) { + while (a > 0) { + while (b > 0) { + write(a); + write(b); + b = read(); + } + a = read(); + } + } + + // an if (...) break inside the body is a path condition for the rest of the body + static void breakInBody() { + while (true) { + int n = read(); + if (n <= 0) { + break; + } + write(n); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java new file mode 100644 index 00000000..8a52143d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java @@ -0,0 +1,80 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorLoopCondition { + + @Refinement("_ >= -1") + static int read() { + return -1; + } + + static void write(@Refinement("_ > 0") int n) {} + + static void lessThanTen(@Refinement("_ < 10") int n) {} + + // the condition was checked on the old value of n, not on the re-assigned one + static void useAfterReassignment() { + int n = read(); + while (n > 0) { + n = read(); + write(n); // Expect: Refinement Error + } + } + + // the condition does not imply the requirement + static void weakerCondition() { + int n = read(); + while (n >= 0) { + write(n); // Expect: Refinement Error + n = read(); + } + } + + // the body must see i, not the incremented value i + 1 (which would be > 0) + static void updateNotBeforeBody() { + for (@Refinement("_ >= 0") int i = 0; i < 10; i++) { + write(i); // Expect: Refinement Error + } + } + + // a do-while body runs once before the condition is checked + static void doWhileFirstIteration() { + int n = read(); + do { + write(n); // Expect: Refinement Error + n = read(); + } while (n > 0); + } + + // i++ in the body invalidates the condition on i + static void incrementInBody() { + int i = 0; + while (i < 10) { + i++; + lessThanTen(i); // Expect: Refinement Error + } + } + + // later iterations: k is decremented while the condition only re-checks m + static void laterIteration() { + int k = read(); + int m = k; + while (m > 0) { + write(k); // Expect: Refinement Error + k = k - 1; + } + } + + // the loop may run zero times or exit through the break: facts from its body do not hold after it + static void factsAfterLoop(int p, boolean c) { + int n = p; + while (c) { + if (n <= 0) { + break; + } + } + write(n); // Expect: Refinement Error + } +} 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 bf6dcc99..91e6c4aa 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 @@ -2,8 +2,10 @@ import java.lang.annotation.Annotation; import java.util.Arrays; +import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; +import java.util.Set; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; @@ -28,14 +30,18 @@ import spoon.reflect.code.CtBreak; import spoon.reflect.code.CtConditional; import spoon.reflect.code.CtContinue; +import spoon.reflect.code.CtDo; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; import spoon.reflect.code.CtFieldWrite; +import spoon.reflect.code.CtFor; +import spoon.reflect.code.CtForEach; import spoon.reflect.code.CtIf; import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLiteral; import spoon.reflect.code.CtLocalVariable; +import spoon.reflect.code.CtLoop; import spoon.reflect.code.CtNewArray; import spoon.reflect.code.CtNewClass; import spoon.reflect.code.CtOperatorAssignment; @@ -46,11 +52,14 @@ import spoon.reflect.code.CtUnaryOperator; import spoon.reflect.code.CtVariableAccess; import spoon.reflect.code.CtVariableRead; +import spoon.reflect.code.CtVariableWrite; +import spoon.reflect.code.CtWhile; import spoon.reflect.declaration.*; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtFieldReference; import spoon.reflect.reference.CtTypeReference; import spoon.reflect.reference.CtVariableReference; +import spoon.reflect.visitor.filter.TypeFilter; import spoon.support.reflect.code.CtVariableWriteImpl; public class RefinementTypeChecker extends TypeChecker { @@ -498,6 +507,95 @@ private boolean canCompleteNormally(CtStatement statement) { return true; } + @Override + public void visitCtWhile(CtWhile whileLoop) { + visitLoop(whileLoop, () -> { + scan(whileLoop.getLoopingExpression()); + assumeLoopCondition(whileLoop.getLoopingExpression()); + scan(whileLoop.getBody()); + }); + } + + @Override + public void visitCtFor(CtFor forLoop) { + scan(forLoop.getForInit()); + visitLoop(forLoop, () -> { + scan(forLoop.getExpression()); + assumeLoopCondition(forLoop.getExpression()); + scan(forLoop.getBody()); + // the update runs after the body, so the body sees the values the condition was checked on + scan(forLoop.getForUpdate()); + }); + } + + @Override + public void visitCtDo(CtDo doLoop) { + // the condition is not checked before the first iteration, so it is not assumed in the body + visitLoop(doLoop, () -> super.visitCtDo(doLoop)); + } + + @Override + public void visitCtForEach(CtForEach forEach) { + visitLoop(forEach, () -> super.visitCtForEach(forEach)); + } + + /** + * Checks one arbitrary iteration of a loop: the variables the loop writes are havocked (keep only their declared + * refinements, which every assignment re-checks) before it and again after it, since the loop may run any number of + * times. Path conditions added inside the loop (e.g. the loop condition, or an {@code if (...) break;}) are dropped + * after it. + */ + private void visitLoop(CtLoop loop, Runnable iteration) { + List pathVariables = vcChecker.getPathVariables(); + havocVariablesWrittenIn(loop); + iteration.run(); + vcChecker.restorePathVariables(pathVariables); + havocVariablesWrittenIn(loop); + } + + private void havocVariablesWrittenIn(CtLoop loop) { + Set names = new LinkedHashSet<>(); + for (CtVariableWrite write : loop.getElements(new TypeFilter>(CtVariableWrite.class))) { + CtVariable declaration = write.getVariable().getDeclaration(); + if (declaration != null && declaration.hasParent(loop.getBody())) + continue; // declared in the body: a new variable on each iteration + String name = write.getVariable().getSimpleName(); + names.add(write instanceof CtFieldWrite ? String.format(Formats.THIS, name) : name); + } + for (String name : names) { + if (!(context.getVariableByName(name)instanceof Variable variable)) + continue; + removePathConditionsOn(name); + String instanceName = String.format(Formats.INSTANCE, name, context.getCounter()); + Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName); + context.addInstanceToContext(instanceName, variable.getType(), declared, loop); + context.addRefinementInstanceToVariable(name, instanceName); + } + } + + /** + * Assumes the loop condition in the body, as a path condition on the values it was evaluated on (same encoding as + * the condition of an if, see visitCtIf). Re-assigning a variable in the body drops the conditions on it. + */ + private void assumeLoopCondition(CtExpression condition) { + // conditions with side effects (e.g. (n = read()) > 0) are not encoded, so they assume nothing + if (condition == null || !condition.getElements(new TypeFilter<>(CtVariableWrite.class)).isEmpty()) + return; + Predicate refs = getRefinement(condition); + if (isUninformativeCondition(refs, condition) || refs.getVariableNames().contains("null")) + return; + String pathVarName = String.format(Formats.FRESH, context.getCounter()); + boolean valueIsCondition = refs.getVariableNames().contains(Keys.WILDCARD); + refs = refs.substituteVariable(Keys.WILDCARD, pathVarName); + refs = Predicate.createConjunction(refs, substituteAllVariablesForLastInstance(refs)); + if (valueIsCondition) { + refs = Predicate.createConjunction(refs, Predicate.createEquals(Predicate.createVar(pathVarName), + Predicate.createLit("true", Types.BOOLEAN))); + } + vcChecker.addPathVariable( + context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, refs, condition)); + } + @Override public void visitCtArrayWrite(CtArrayWrite arrayWrite) { super.visitCtArrayWrite(arrayWrite); @@ -541,11 +639,7 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression< refinementFound = new Predicate(); } } - Optional r = context.getLastVariableInstance(name); - // AQUI!! - r.ifPresent(variableInstance -> vcChecker.removePathVariableThatIncludes(variableInstance.getName())); - - vcChecker.removePathVariableThatIncludes(name); // AQUI!! + removePathConditionsOn(name); checkVariableRefinements(refinementFound, name, type, parentElem, varDecl); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 752e69e8..e05ddcb2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -371,6 +371,16 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam context.addRefinementToVariableInContext(simpleName, type, cet, usage); } + /** + * Drops the path conditions that mention {@code name}, which is about to be re-assigned, so facts about its old + * value do not apply to the new one + */ + public void removePathConditionsOn(String name) { + context.getLastVariableInstance(name) + .ifPresent(instance -> vcChecker.removePathVariableThatIncludes(instance.getName())); + vcChecker.removePathVariableThatIncludes(name); + } + public void checkSMT(Predicate expectedType, CtElement element, SourcePosition declarationPosition, String customMessage) throws LJError { vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, declarationPosition, diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index b51d1c3e..8e0a9295 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -352,6 +352,15 @@ void clearPathVariables() { pathVariables.clear(); } + List getPathVariables() { + return new ArrayList<>(pathVariables); + } + + /** Drops the path variables added since {@code saved} was taken, keeping any removed meanwhile removed */ + void restorePathVariables(List saved) { + pathVariables.retainAll(saved); + } + void removePathVariableThatIncludes(String otherVar) { pathVariables.stream().filter(rv -> rv.getRefinement().getVariableNames().contains(otherVar)).toList() .forEach(pathVariables::remove); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 550d6781..4f111326 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -127,6 +127,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro name = w.getVariable().getSimpleName(); if (w instanceof CtFieldWrite) name = String.format(Formats.THIS, name); + rtc.removePathConditionsOn(name); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; From c9551907cbdcb54c5d94c90e0ab4ece43d9a9611 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Fri, 2 Oct 2026 14:24:30 +0100 Subject: [PATCH 2/3] Havoc fields and object state in loops, fix continue before for update Review fixes for the loop-condition change (#306): - a continue reaches the for update without the rest of the body, so when the body has one, the update no longer sees the body's path conditions or assignments (`for (..; ..; use(n)) { if (n <= 0) continue; ... }` was accepted) - a loop also changes fields (through any call) and the state of objects it calls state-changing methods on; these are now havocked too, since the assumed condition could otherwise combine with their stale values (accepted programs that main rejected) - drop the null check on the condition, dead since null literals carry no information (#311) - move the i++ path-condition fix out (it is not needed for loops and is a separate pre-existing bug in if branches) Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectLoopCondition.java | 69 ++++++++++++++++++ .../java/testSuite/ErrorLoopCondition.java | 73 +++++++++++++++++++ .../RefinementTypeChecker.java | 54 +++++++++++--- .../refinement_checker/TypeChecker.java | 10 --- .../general_checkers/OperationsChecker.java | 1 - 5 files changed, 184 insertions(+), 23 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java index 2043e467..3319d9e0 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java @@ -1,10 +1,33 @@ package testSuite; import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; @SuppressWarnings("unused") +@StateSet({"open", "closed"}) public class CorrectLoopCondition { + int field; + + @StateRefinement(to = "open(this)") + CorrectLoopCondition() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + void close() {} + + @StateRefinement(from = "open(this)") + void use() {} + + @StateRefinement(to = "return ? open(this) : closed(this)") + boolean isOpen() { + return true; + } + + void setFieldNegative() { + field = -1; + } + @Refinement("_ >= -1") static int read() { return -1; @@ -73,4 +96,50 @@ static void breakInBody() { write(n); } } + + // the declared refinement of a variable assigned in the loop holds after it + static void valueAfterLoop(boolean c) { + @Refinement("_ > 0") int n = 1; + while (c) { + n = 2; + } + write(n); + } + + // a continue in the body, with an update that needs no fact from the body + static void continueInFor(int p) { + int n = p; + for (int i = 0; i < 10; i++) { + if (n <= 0) { + continue; + } + write(n); + } + } + + // the condition on a field holds in the body + void fieldCondition() { + while (field > 0) { + write(field); + field = field - 1; + } + } + + // methods that keep the state of r can be called in the loop + static void stateKeptInLoop(int k) { + CorrectLoopCondition r = new CorrectLoopCondition(); + while (k > 0) { + r.use(); + k = k - 1; + } + r.close(); + } + + // the condition checks the state of r on every iteration + static void stateCheckedByCondition(CorrectLoopCondition r) { + while (r.isOpen()) { + r.use(); + r.close(); + } + } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java index 8a52143d..11e7ba43 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java @@ -1,10 +1,33 @@ package testSuite; import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; @SuppressWarnings("unused") +@StateSet({"open", "closed"}) public class ErrorLoopCondition { + int field; + + @StateRefinement(to = "open(this)") + ErrorLoopCondition() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + void close() {} + + @StateRefinement(from = "open(this)") + void use() {} + + @StateRefinement(to = "return ? open(this) : closed(this)") + boolean isOpen() { + return true; + } + + void setFieldNegative() { + field = -1; + } + @Refinement("_ >= -1") static int read() { return -1; @@ -77,4 +100,54 @@ static void factsAfterLoop(int p, boolean c) { } write(n); // Expect: Refinement Error } + + // the loop may run zero times: a value assigned in it is not the value after it + static void valueAfterLoop(boolean c) { + int n = -1; + while (c) { + n = 1; + } + write(n); // Expect: Refinement Error + } + + // a continue skips the rest of the body, so the update cannot rely on its facts + static void continueBeforeUpdate(int p) { + int n = p; + for (int i = 0; i < 10; write(n)) { // Expect: Refinement Error + if (n <= 0) { + continue; + } + i++; + } + } + + // a call in the body writes the field, which later iterations use + void fieldWrittenByCall(int p) { + field = p; + int k = p; + while (k > 0) { + write(field); // Expect: Refinement Error + setFieldNegative(); + } + } + + // the loop changes the state of r: the second iteration uses it closed + static void stateChangedInLoop(ErrorLoopCondition r) { + boolean open = r.isOpen(); + while (open) { + r.use(); // Expect: State Refinement Error + r.close(); + } + } + + // the inner loop also runs in later iterations of the do-while, after n = 5 + static void innerLoopInDoWhile(boolean c) { + int n = 0; + do { + while (n > 0) { + write(n - 10); // Expect: Refinement Error + } + n = 5; + } while (c); + } } 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 91e6c4aa..547f98ba 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 @@ -1,6 +1,7 @@ package liquidjava.processor.refinement_checker; import java.lang.annotation.Annotation; +import java.util.ArrayList; import java.util.Arrays; import java.util.LinkedHashSet; import java.util.List; @@ -23,6 +24,7 @@ import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.CtArrayRead; +import spoon.reflect.code.CtAbstractInvocation; import spoon.reflect.code.CtArrayWrite; import spoon.reflect.code.CtAssignment; import spoon.reflect.code.CtBinaryOperator; @@ -33,6 +35,7 @@ import spoon.reflect.code.CtDo; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtFieldAccess; import spoon.reflect.code.CtFieldRead; import spoon.reflect.code.CtFieldWrite; import spoon.reflect.code.CtFor; @@ -522,7 +525,13 @@ public void visitCtFor(CtFor forLoop) { visitLoop(forLoop, () -> { scan(forLoop.getExpression()); assumeLoopCondition(forLoop.getExpression()); + List pathVariables = vcChecker.getPathVariables(); scan(forLoop.getBody()); + if (!forLoop.getBody().getElements(new TypeFilter<>(CtContinue.class)).isEmpty()) { + // a continue reaches the update from any point of the body, skipping its facts and assignments + vcChecker.restorePathVariables(pathVariables); + havocChangedIn(forLoop); + } // the update runs after the body, so the body sees the values the condition was checked on scan(forLoop.getForUpdate()); }); @@ -540,32 +549,49 @@ public void visitCtForEach(CtForEach forEach) { } /** - * Checks one arbitrary iteration of a loop: the variables the loop writes are havocked (keep only their declared - * refinements, which every assignment re-checks) before it and again after it, since the loop may run any number of + * Checks one arbitrary iteration of a loop: what the loop may change is havocked (keeps only its declared + * refinement, which every assignment re-checks) before it and again after it, since the loop may run any number of * times. Path conditions added inside the loop (e.g. the loop condition, or an {@code if (...) break;}) are dropped * after it. */ private void visitLoop(CtLoop loop, Runnable iteration) { List pathVariables = vcChecker.getPathVariables(); - havocVariablesWrittenIn(loop); + havocChangedIn(loop); iteration.run(); vcChecker.restorePathVariables(pathVariables); - havocVariablesWrittenIn(loop); + havocChangedIn(loop); } - private void havocVariablesWrittenIn(CtLoop loop) { + /** + * Havocs what the loop may change: the variables it writes, the objects it calls state-changing methods on, and the + * fields if it calls any method or constructor (which may write them) + */ + private void havocChangedIn(CtLoop loop) { + List> changed = new ArrayList<>( + loop.getElements(new TypeFilter>(CtVariableWrite.class))); + List> calls = loop + .getElements(new TypeFilter>(CtAbstractInvocation.class)); + for (CtAbstractInvocation call : calls) { + if (call instanceof CtInvocation inv && inv.getTarget()instanceof CtVariableAccess target + && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size()) + .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) + changed.add(target); + } Set names = new LinkedHashSet<>(); - for (CtVariableWrite write : loop.getElements(new TypeFilter>(CtVariableWrite.class))) { - CtVariable declaration = write.getVariable().getDeclaration(); + for (CtVariableAccess access : changed) { + CtVariable declaration = access.getVariable().getDeclaration(); if (declaration != null && declaration.hasParent(loop.getBody())) continue; // declared in the body: a new variable on each iteration - String name = write.getVariable().getSimpleName(); - names.add(write instanceof CtFieldWrite ? String.format(Formats.THIS, name) : name); + String name = access.getVariable().getSimpleName(); + names.add(access instanceof CtFieldAccess ? String.format(Formats.THIS, name) : name); } + if (!calls.isEmpty()) + context.getCtxVars().stream().map(RefinedVariable::getName) + .filter(n -> n.startsWith(String.format(Formats.THIS, ""))).forEach(names::add); for (String name : names) { if (!(context.getVariableByName(name)instanceof Variable variable)) continue; - removePathConditionsOn(name); + vcChecker.removePathVariableThatIncludes(name); String instanceName = String.format(Formats.INSTANCE, name, context.getCounter()); Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName); context.addInstanceToContext(instanceName, variable.getType(), declared, loop); @@ -582,7 +608,7 @@ private void assumeLoopCondition(CtExpression condition) { if (condition == null || !condition.getElements(new TypeFilter<>(CtVariableWrite.class)).isEmpty()) return; Predicate refs = getRefinement(condition); - if (isUninformativeCondition(refs, condition) || refs.getVariableNames().contains("null")) + if (isUninformativeCondition(refs, condition)) return; String pathVarName = String.format(Formats.FRESH, context.getCounter()); boolean valueIsCondition = refs.getVariableNames().contains(Keys.WILDCARD); @@ -639,7 +665,11 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression< refinementFound = new Predicate(); } } - removePathConditionsOn(name); + Optional r = context.getLastVariableInstance(name); + // AQUI!! + r.ifPresent(variableInstance -> vcChecker.removePathVariableThatIncludes(variableInstance.getName())); + + vcChecker.removePathVariableThatIncludes(name); // AQUI!! checkVariableRefinements(refinementFound, name, type, parentElem, varDecl); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index e05ddcb2..752e69e8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -371,16 +371,6 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam context.addRefinementToVariableInContext(simpleName, type, cet, usage); } - /** - * Drops the path conditions that mention {@code name}, which is about to be re-assigned, so facts about its old - * value do not apply to the new one - */ - public void removePathConditionsOn(String name) { - context.getLastVariableInstance(name) - .ifPresent(instance -> vcChecker.removePathVariableThatIncludes(instance.getName())); - vcChecker.removePathVariableThatIncludes(name); - } - public void checkSMT(Predicate expectedType, CtElement element, SourcePosition declarationPosition, String customMessage) throws LJError { vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, declarationPosition, diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 4f111326..550d6781 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -127,7 +127,6 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro name = w.getVariable().getSimpleName(); if (w instanceof CtFieldWrite) name = String.format(Formats.THIS, name); - rtc.removePathConditionsOn(name); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; From 3edab8376a55b07646f664d8bc19f2579728818f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Fri, 2 Oct 2026 18:48:42 +0100 Subject: [PATCH 3/3] Test loop violation reached after a known first iteration --- .../src/main/java/testSuite/ErrorLoopCondition.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java index 11e7ba43..a94e938b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java @@ -90,6 +90,16 @@ static void laterIteration() { } } + // x starts at 3, but on its third iteration x is 1 and y becomes 0. + // Checking only the first iteration accepts the false refinement on y. + static void laterIterationFromKnownStart() { + int x = 3; + while (x > 0) { + @Refinement("_ > 0") int y = x - 1; // Expect: Refinement Error + x--; + } + } + // the loop may run zero times or exit through the break: facts from its body do not hold after it static void factsAfterLoop(int p, boolean c) { int n = p;