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..3319d9e0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectLoopCondition.java @@ -0,0 +1,145 @@ +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; + } + + 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); + } + } + + // 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 new file mode 100644 index 00000000..a94e938b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopCondition.java @@ -0,0 +1,163 @@ +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; + } + + 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; + } + } + + // 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; + while (c) { + if (n <= 0) { + break; + } + } + 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 bf6dcc99..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,9 +1,12 @@ 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; import java.util.Optional; +import java.util.Set; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; @@ -21,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; @@ -28,14 +32,19 @@ 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.CtFieldAccess; 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 +55,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 +510,118 @@ 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()); + 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()); + }); + } + + @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: 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(); + havocChangedIn(loop); + iteration.run(); + vcChecker.restorePathVariables(pathVariables); + havocChangedIn(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 (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 = 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; + 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); + 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)) + 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); 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);