Skip to content

Commit cfe9550

Browse files
CatarinaGamboaCatarinaGamboa
authored
Merge pull request #33 from CatarinaGamboa/32-fields-updates-make-verification-wrong-in-state-changes
32 fields updates make verification wrong in state changes
2 parents 076d0a7 + 3c76824 commit cfe9550

File tree

6 files changed

+173
-5
lines changed

6 files changed

+173
-5
lines changed

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

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
@StateSet({"green", "amber", "red"})
7+
public class CorrectTrafficLightRGB {
8+
9+
@Refinement("r >= 0 && r <= 255") int r;
10+
11+
@Refinement("g >= 0 && g <= 255") int g;
12+
13+
@Refinement("b >= 0 && b <= 255") int b;
14+
15+
@StateRefinement(to = "green(this)")
16+
public CorrectTrafficLightRGB() {
17+
r = 255;
18+
g = 0;
19+
b = 0;
20+
}
21+
22+
@StateRefinement(from = "green(this)", to = "amber(this)")
23+
public void transitionToAmber() {
24+
r = 255;
25+
g = 120;
26+
b = 0;
27+
}
28+
29+
@StateRefinement(from = "red(this)", to = "green(this)")
30+
public void transitionToGreen() {
31+
r = 76;
32+
g = 187;
33+
b = 23;
34+
}
35+
36+
@StateRefinement(from = "amber(this)", to = "red(this)")
37+
public void transitionToRed() {
38+
r = 230;
39+
g = 0;
40+
b = 1;
41+
}
42+
43+
44+
public static void name() {
45+
CorrectTrafficLightRGB tl = new CorrectTrafficLightRGB();
46+
tl.transitionToAmber();
47+
tl.transitionToRed();
48+
}
49+
}

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

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
@StateSet({"green", "amber", "red"})
7+
public class ErrorTrafficLightRGB {
8+
9+
@Refinement("r >= 0 && r <= 255") int r;
10+
11+
@Refinement("g >= 0 && g <= 255") int g;
12+
13+
@Refinement("b >= 0 && b <= 255") int b;
14+
15+
@StateRefinement(to = "green(this)")
16+
public ErrorTrafficLightRGB() {
17+
r = 255;
18+
g = 0;
19+
b = 0;
20+
}
21+
22+
@StateRefinement(from = "green(this)", to = "amber(this)")
23+
public void transitionToAmber() {
24+
r = 255;
25+
g = 120;
26+
b = 0;
27+
}
28+
29+
@StateRefinement(from = "red(this)", to = "green(this)")
30+
public void transitionToGreen() {
31+
r = 76;
32+
g = 187;
33+
b = 23;
34+
}
35+
36+
@StateRefinement(from = "amber(this)", to = "red(this)")
37+
public void transitionToRed() {
38+
r = 230;
39+
g = 0;
40+
b = 1;
41+
}
42+
43+
44+
public static void name() {
45+
ErrorTrafficLightRGB tl = new ErrorTrafficLightRGB();
46+
tl.transitionToAmber();
47+
tl.transitionToRed();
48+
}
49+
}

‎liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ public static void main(String[] args) {
1818
// "../liquidjava/liquidjava-umbrella/liquidjava-example/src/main/java/liquidjava/test/project";
1919
String file = args.length == 0 ? allPath : args[0];
2020
ErrorEmitter ee = launch(file);
21-
System.out.println(ee.foundError()? (ee.getFullMessage()):("Correct! Passed Verification."));
21+
System.out.println(ee.foundError() ? (ee.getFullMessage()) : ("Correct! Passed Verification."));
2222

2323
}
2424

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
100100
return smtChecks(premises, et, p);
101101
}
102102

103-
private /* Predicate */ VCImplication joinPredicates(Predicate expectedType, List<RefinedVariable> mainVars,
103+
private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariable> mainVars,
104104
List<RefinedVariable> vars, HashMap<String, PlacementInCode> map) {
105105

106106
VCImplication firstSi = null;
@@ -135,7 +135,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
135135
if (firstSi != null && lastSi != null) {
136136
cSMT = firstSi.clone();
137137
lastSi.setNext(new VCImplication(expectedType));
138-
// printVCs(firstSi.toString(), cSMT.toConjunctions().toString(), expectedType);
138+
// printVCs(firstSi.toString(), cSMT.toConjunctions().toString(), expectedType); //DEBUG: UNCOMMENT
139139
}
140140

141141
return cSMT; // firstSi != null ? firstSi : new VCImplication(new Predicate());

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

Lines changed: 48 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33
import java.lang.annotation.Annotation;
44
import java.util.*;
55
import java.util.stream.Collectors;
6+
7+
import liquidjava.errors.ErrorEmitter;
68
import liquidjava.errors.ErrorHandler;
79
import liquidjava.processor.context.*;
810
import liquidjava.processor.refinement_checker.TypeChecker;
@@ -40,19 +42,44 @@ public static void handleConstructorState(CtConstructor<?> c, RefinedFunction f,
4042
return;
4143
}
4244
}
43-
setFunctionStates(f, an, tc, c); // f.setState(an, context.getGhosts(), c);
45+
setConstructorStates(f, an, tc, c); // f.setState(an, context.getGhosts(), c);
4446
} else {
4547
setDefaultState(f, tc);
4648
}
4749
}
4850

51+
/**
52+
* Creates the list of states and adds them to the function
53+
*
54+
* @param f
55+
* @param anns
56+
* @param tc
57+
* @param element
58+
*
59+
* @throws ParsingException
60+
*/
61+
@SuppressWarnings({ "rawtypes" })
62+
private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<? extends Annotation>> anns,
63+
TypeChecker tc, CtElement element) throws ParsingException {
64+
List<ObjectState> l = new ArrayList<>();
65+
for (CtAnnotation<? extends Annotation> an : anns) {
66+
Map<String, CtExpression> m = an.getAllValues();
67+
String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
68+
ObjectState state = new ObjectState();
69+
if (to != null)
70+
state.setTo(new Predicate(to, element, tc.getErrorEmitter()));
71+
l.add(state);
72+
}
73+
f.setAllStates(l);
74+
}
75+
4976
public static void setDefaultState(RefinedFunction f, TypeChecker tc) {
5077
String[] path = f.getTargetClass().split("\\.");
5178
String klass = path[path.length - 1];
5279

5380
Predicate[] s = { Predicate.createVar(tc.THIS) };
5481
Predicate c = new Predicate();
55-
List<GhostFunction> sets = getDifferentSets(tc, klass);
82+
List<GhostFunction> sets = getDifferentSets(tc, klass);// ??
5683
for (GhostFunction sg : sets) {
5784
if (sg.getReturnType().toString().equals("int")) {
5885
Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s),
@@ -434,6 +461,25 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
434461
return new Predicate();
435462
}
436463

464+
/**
465+
* Method prepared to change all old vars in a predicate, however it has not been needed yet
466+
*
467+
* @param pred
468+
* @param tc
469+
*
470+
* @return
471+
*/
472+
private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) {
473+
Predicate noOld = pred;
474+
List<String> listVarsInOld = pred.getOldVariableNames();
475+
for (String varInOld : listVarsInOld) {
476+
Optional<VariableInstance> ovi = tc.getContext().getLastVariableInstance(varInOld);
477+
if (ovi.isPresent())
478+
noOld = noOld.changeOldMentions(varInOld, ovi.get().getName(), tc.getErrorEmitter());
479+
}
480+
return noOld;
481+
}
482+
437483
private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName,
438484
TypeChecker tc) {
439485
return transitionedState.changeOldMentions(instanceName, newInstanceName, tc.getErrorEmitter());

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,6 +137,30 @@ public Predicate changeOldMentions(String previousName, String newName, ErrorEmi
137137
return new Predicate(e);
138138
}
139139

140+
public List<String> getOldVariableNames() {
141+
List<String> ls = new ArrayList<>();
142+
expressionGetOldVariableNames(this.exp, ls);
143+
return ls;
144+
}
145+
146+
private void expressionGetOldVariableNames(Expression exp, List<String> ls) {
147+
if (exp instanceof FunctionInvocation) {
148+
FunctionInvocation fi = (FunctionInvocation) exp;
149+
if (fi.getName().equals(Utils.OLD)) {
150+
List<Expression> le = fi.getArgs();
151+
for (Expression e : le) {
152+
if (e instanceof Var)
153+
ls.add(((Var) e).getName());
154+
}
155+
}
156+
}
157+
if (exp.hasChildren()) {
158+
for (var ch : exp.getChildren())
159+
expressionGetOldVariableNames(ch, ls);
160+
161+
}
162+
}
163+
140164
public Predicate changeStatesToRefinements(List<GhostState> ghostState, String[] toChange, ErrorEmitter ee) {
141165
Map<String, Expression> nameRefinementMap = new HashMap<>();
142166
for (GhostState gs : ghostState)

0 commit comments

Comments
 (0)