Skip to content

Commit 371c005

Browse files
CatarinaGamboaCatarinaGamboa
committed
Check current receiver typestate across loops
1 parent dcfc4eb commit 371c005

5 files changed

Lines changed: 226 additions & 7 deletions

File tree

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

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
@StateSet({"open", "marked"})
7+
public class CorrectLoopPostState {
8+
@StateRefinement(to = "open(this)")
9+
CorrectLoopPostState() {}
10+
11+
@StateRefinement(to = "marked(this)")
12+
void mark() {}
13+
14+
@StateRefinement(from = "marked(this)", to = "open(this)")
15+
void reset() {}
16+
17+
@StateRefinement(from = "open(this)")
18+
void use() {}
19+
20+
// A state-preserving call leaves the entry state available after the loop.
21+
static void unchangedState(int n) {
22+
CorrectLoopPostState b = new CorrectLoopPostState();
23+
while (n > 0) {
24+
b.use();
25+
n--;
26+
}
27+
b.use();
28+
}
29+
30+
// An unconditional transition after the loop establishes the required state.
31+
static void establishStateAfterLoop(int n) {
32+
CorrectLoopPostState b = new CorrectLoopPostState();
33+
while (n > 0) {
34+
b.mark();
35+
n--;
36+
}
37+
b.mark();
38+
b.reset();
39+
}
40+
41+
@StateRefinement(from = "open(this)")
42+
void unchangedThisState(int n) {
43+
while (n > 0) {
44+
this.use();
45+
n--;
46+
}
47+
use();
48+
}
49+
50+
@StateRefinement(from = "open(this)")
51+
void establishThisStateAfterLoop(int n) {
52+
while (n > 0) {
53+
mark();
54+
n--;
55+
}
56+
this.mark();
57+
reset();
58+
}
59+
60+
@StateRefinement(from = "open(this)")
61+
void directValidTransitions() {
62+
this.use();
63+
mark();
64+
this.reset();
65+
use();
66+
}
67+
68+
@StateRefinement(from = "open(this)")
69+
@StateRefinement(from = "marked(this)")
70+
void acceptEitherState() {}
71+
72+
// Neither alternative is known individually; the call accepts their union and preserves it.
73+
@StateRefinement(from = "open(this)")
74+
@StateRefinement(from = "marked(this)")
75+
void wrapEitherState() {
76+
acceptEitherState();
77+
this.acceptEitherState();
78+
}
79+
}

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

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
@StateSet({"open", "marked"})
7+
public class ErrorLoopPostState {
8+
@StateRefinement(to = "open(this)")
9+
ErrorLoopPostState() {}
10+
11+
@StateRefinement(to = "marked(this)")
12+
void mark() {}
13+
14+
@StateRefinement(from = "marked(this)", to = "open(this)")
15+
void reset() {}
16+
17+
@StateRefinement(from = "open(this)")
18+
void use() {}
19+
20+
// Issue #338: the loop may run zero times, leaving b open.
21+
static void whileMayBeEmpty(int n) {
22+
ErrorLoopPostState b = new ErrorLoopPostState();
23+
int k = 0;
24+
while (k < n) {
25+
b.mark();
26+
k++;
27+
}
28+
b.reset(); // Expect: State Refinement Error
29+
}
30+
31+
static void forMayBeEmpty(int n) {
32+
ErrorLoopPostState b = new ErrorLoopPostState();
33+
for (int k = 0; k < n; k++) {
34+
b.mark();
35+
}
36+
b.reset(); // Expect: State Refinement Error
37+
}
38+
39+
static void forEachMayBeEmpty(int[] values) {
40+
ErrorLoopPostState b = new ErrorLoopPostState();
41+
for (int value : values) {
42+
b.mark();
43+
}
44+
b.reset(); // Expect: State Refinement Error
45+
}
46+
47+
@StateRefinement(from = "open(this)")
48+
void explicitThisMayBeEmpty(int n) {
49+
while (n > 0) {
50+
this.mark();
51+
n--;
52+
}
53+
this.reset(); // Expect: State Refinement Error
54+
}
55+
56+
@StateRefinement(from = "open(this)")
57+
void implicitThisMayBeEmpty(int n) {
58+
while (n > 0) {
59+
mark();
60+
n--;
61+
}
62+
reset(); // Expect: State Refinement Error
63+
}
64+
65+
@StateRefinement(from = "open(this)")
66+
void laterIteration(int n) {
67+
while (n > 0) {
68+
use(); // Expect: State Refinement Error
69+
mark();
70+
n--;
71+
}
72+
}
73+
74+
@StateRefinement(from = "open(this)")
75+
void directInvalidCall() {
76+
this.reset(); // Expect: State Refinement Error
77+
}
78+
79+
@StateRefinement(from = "open(this)")
80+
void directInvalidSequence() {
81+
mark();
82+
use(); // Expect: State Refinement Error
83+
}
84+
85+
@StateRefinement(from = "open(this)")
86+
@StateRefinement(from = "marked(this)")
87+
void unionDoesNotImplyOneState() {
88+
use(); // Expect: State Refinement Error
89+
}
90+
}

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

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -604,13 +604,17 @@ private void havocChangedIn(CtLoop loop) {
604604
loop.getElements(new TypeFilter<CtVariableWrite<?>>(CtVariableWrite.class)));
605605
List<CtAbstractInvocation<?>> calls = loop
606606
.getElements(new TypeFilter<CtAbstractInvocation<?>>(CtAbstractInvocation.class));
607+
Set<String> names = new LinkedHashSet<>();
607608
for (CtAbstractInvocation<?> call : calls) {
608-
if (call instanceof CtInvocation<?> inv && inv.getTarget()instanceof CtVariableAccess<?> target
609+
if (call instanceof CtInvocation<?> inv
609610
&& context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size())
610-
.stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo)))
611-
changed.add(target);
611+
.stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) {
612+
if (inv.getTarget()instanceof CtVariableAccess<?> target)
613+
changed.add(target);
614+
else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTarget()))
615+
names.add(Keys.THIS);
616+
}
612617
}
613-
Set<String> names = new LinkedHashSet<>();
614618
for (CtVariableAccess<?> access : changed) {
615619
CtVariable<?> declaration = access.getVariable().getDeclaration();
616620
if (declaration != null && declaration.hasParent(loop.getBody()))

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
import liquidjava.utils.Utils;
2020
import liquidjava.utils.constants.Formats;
2121
import liquidjava.utils.constants.Keys;
22+
import liquidjava.utils.constants.Types;
2223
import spoon.reflect.code.CtConstructorCall;
2324
import spoon.reflect.code.CtExpression;
2425
import spoon.reflect.code.CtFieldRead;
@@ -446,6 +447,19 @@ public void loadFunctionInfo(CtExecutable<?> method) {
446447
for (Variable v : lv)
447448
rtc.getContext().addVarToContext(v);
448449
}
450+
if (method instanceof CtMethod<?> instanceMethod && !instanceMethod.isStatic()) {
451+
// The contract describes the entry state, not an invariant of every intermediate receiver state.
452+
Predicate entry = fi == null || fi.getAllStates().isEmpty() ? new Predicate() : fi.getFromStates()
453+
.stream().reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction);
454+
CtTypeReference<?> receiverType = rtc.getFactory().Type().createReference(className);
455+
RefinedVariable receiver = rtc.getContext().addVarToContext(Keys.THIS, receiverType, new Predicate(),
456+
method);
457+
receiver.addSuperTypes(receiverType.getSuperclass(), receiverType.getSuperInterfaces());
458+
String instanceName = String.format(Formats.INSTANCE, Keys.THIS, rtc.getContext().getCounter());
459+
rtc.getContext().addInstanceToContext(instanceName, receiverType,
460+
entry.substituteVariable(Keys.THIS, instanceName), method);
461+
rtc.getContext().addRefinementInstanceToVariable(Keys.THIS, instanceName);
462+
}
449463
}
450464
}
451465
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 35 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -564,8 +564,28 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
564564
.substituteVariable(name, instanceName);
565565

566566
boolean found = false;
567+
boolean preservesState = stateChanges.stream().noneMatch(ObjectState::hasTo);
568+
if (preservesState) {
569+
// A state-preserving call accepts any of its entry states, including a disjunction of them.
570+
Predicate expected = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom)
571+
.reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction)
572+
.substituteVariable(Keys.THIS, instanceName);
573+
Predicate previous = prevState;
574+
for (String parameter : map.keySet()) {
575+
previous = previous.substituteVariable(parameter, map.get(parameter));
576+
expected = expected.substituteVariable(parameter, map.get(parameter));
577+
}
578+
expected = expected.changeOldMentions(vi.getName(), instanceName);
579+
try {
580+
found = tc.checkStateSMT(previous, expected, invocation.getPosition());
581+
} catch (SMTUnknownError error) {
582+
error.setDeclarationPosition(stateChanges.stream().map(ObjectState::getFromPosition)
583+
.filter(Objects::nonNull).findFirst().orElse(function.getPlacementInCode().getPosition()));
584+
throw error;
585+
}
586+
}
567587
for (ObjectState stateChange : stateChanges) { // TODO: only working for 1 state annotation
568-
if (found)
588+
if (found || preservesState)
569589
break;
570590
if (!stateChange.hasFrom())
571591
continue;
@@ -679,6 +699,18 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
679699
invocation.putMetadata(Keys.TARGET, vi2);
680700
}
681701

702+
/** Whether the access denotes the receiver of the enclosing type, including unqualified super. */
703+
public static boolean isCurrentReceiver(CtElement target) {
704+
CtType<?> owner = target.getParent(CtType.class);
705+
if (owner == null)
706+
return false;
707+
if (target instanceof CtThisAccess<?> self)
708+
return self.getType() != null && self.getType().getQualifiedName().equals(owner.getQualifiedName());
709+
if (target instanceof CtSuperAccess<?> parent)
710+
return parent.getTarget() == null || parent.getTarget().isImplicit();
711+
return false;
712+
}
713+
682714
/**
683715
* Gets the name of the parent target and adds the closest target to the elem TARGET metadata
684716
*
@@ -687,10 +719,10 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
687719
* @return the name of the parent target
688720
*/
689721
public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, CtElement invocation) {
690-
if (target2 instanceof CtVariableRead<?> v) {
722+
if (target2 instanceof CtVariableRead<?> || isCurrentReceiver(target2)) {
691723
// v--------- field read
692724
// means invocation is in a form of `t.method(args)`
693-
String name = v.getVariable().getSimpleName();
725+
String name = target2 instanceof CtVariableRead<?> v ? v.getVariable().getSimpleName() : Keys.THIS;
694726
if (target2 instanceof CtFieldRead<?> fieldRead && fieldRead.getTarget() instanceof CtThisAccess<?>) {
695727
String fieldName = Utils.qualifyFieldName(fieldRead.getVariable());
696728
if (tc.getContext().hasVariable(fieldName))

0 commit comments

Comments
 (0)