Skip to content

Commit 8f2142f

Browse files
rcosta358rcosta358
committed
Code Refactoring
1 parent 5bf4eab commit 8f2142f

File tree

21 files changed

+368
-409
lines changed

21 files changed

+368
-409
lines changed

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java‎

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import java.util.Formatter;
44
import java.util.HashMap;
55
import java.util.Locale;
6+
67
import liquidjava.processor.VCImplication;
78
import liquidjava.processor.context.PlacementInCode;
89
import liquidjava.rj_language.Predicate;
@@ -11,20 +12,6 @@
1112

1213
public class ErrorHandler {
1314

14-
/**
15-
* Prints the error message
16-
*
17-
* @param <T>
18-
* @param var
19-
* @param s
20-
* @param expectedType
21-
* @param cSMT
22-
*/
23-
public static <T> void printError(CtElement var, Predicate expectedType, Predicate cSMT,
24-
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
25-
printError(var, null, expectedType, cSMT, map, ee);
26-
}
27-
2815
public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
2916
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
3017
String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,12 @@
77
import liquidjava.diagnostics.warnings.LJWarning;
88
import liquidjava.processor.context.PlacementInCode;
99

10+
/**
11+
* Singleton class to store diagnostics information (errors, warnings, translation map) during the verification process
12+
*
13+
* @see LJError
14+
* @see LJWarning
15+
*/
1016
public class LJDiagnostics {
1117
private static LJDiagnostics instance;
1218

@@ -26,6 +32,24 @@ public static LJDiagnostics getInstance() {
2632
return instance;
2733
}
2834

35+
public static LJDiagnostics add(LJError error) {
36+
LJDiagnostics instance = getInstance();
37+
instance.addError(error);
38+
return instance;
39+
}
40+
41+
public static LJDiagnostics add(LJWarning warning) {
42+
LJDiagnostics instance = getInstance();
43+
instance.addWarning(warning);
44+
return instance;
45+
}
46+
47+
public static LJDiagnostics add(HashMap<String, PlacementInCode> map) {
48+
LJDiagnostics instance = getInstance();
49+
instance.setTranslationMap(map);
50+
return instance;
51+
}
52+
2953
public void addError(LJError error) {
3054
this.errors.add(error);
3155
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ public class RefinementError extends LJError {
1616
private ValDerivationNode found;
1717

1818
public RefinementError(CtElement element, Predicate expected, ValDerivationNode found) {
19-
super("Refinement Error", "Predicate refinement violation", element);
19+
super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element);
2020
this.expected = expected;
2121
this.found = found;
2222
}

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ public class StateConflictError extends LJError {
1414
private String className;
1515

1616
public StateConflictError(CtElement element, Predicate predicate, String className) {
17-
super("State Conflict Error", "Found multiple disjoint states from a StateSet in refinement", element);
17+
super("State Conflict Error", "Found multiple disjoint states in state transition", element);
1818
this.predicate = predicate;
1919
this.className = className;
2020
}

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

Lines changed: 36 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,9 @@
1313
import liquidjava.rj_language.BuiltinFunctionPredicate;
1414
import liquidjava.rj_language.Predicate;
1515
import liquidjava.rj_language.parsing.ParsingException;
16-
import liquidjava.utils.Utils;
16+
import liquidjava.utils.constants.Formats;
17+
import liquidjava.utils.constants.Keys;
18+
import liquidjava.utils.constants.Types;
1719

1820
import org.apache.commons.lang3.NotImplementedException;
1921
import spoon.reflect.code.CtArrayRead;
@@ -172,22 +174,22 @@ public <T> void visitCtNewArray(CtNewArray<T> newArray) {
172174
} catch (ParsingException e) {
173175
return; // error already in ErrorEmitter
174176
}
175-
String name = String.format(freshFormat, context.getCounter());
176-
if (c.getVariableNames().contains(WILD_VAR)) {
177-
c = c.substituteVariable(WILD_VAR, name);
177+
String name = String.format(Formats.RET, context.getCounter());
178+
if (c.getVariableNames().contains(Keys.WILDCARD)) {
179+
c = c.substituteVariable(Keys.WILDCARD, name);
178180
} else {
179181
c = Predicate.createEquals(Predicate.createVar(name), c);
180182
}
181183
context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp);
182184
Predicate ep;
183185
try {
184186
ep = Predicate.createEquals(
185-
BuiltinFunctionPredicate.builtin_length(WILD_VAR, newArray, getErrorEmitter()),
187+
BuiltinFunctionPredicate.builtin_length(Keys.WILDCARD, newArray, getErrorEmitter()),
186188
Predicate.createVar(name));
187189
} catch (ParsingException e) {
188190
return; // error already in ErrorEmitter
189191
}
190-
newArray.putMetadata(REFINE_KEY, ep);
192+
newArray.putMetadata(Keys.REFINEMENT, ep);
191193
}
192194
}
193195

@@ -201,9 +203,9 @@ public <T> void visitCtThisAccess(CtThisAccess<T> thisAccess) {
201203
CtClass<?> c = thisAccess.getParent(CtClass.class);
202204
String s = c.getSimpleName();
203205
if (thisAccess.getParent() instanceof CtReturn) {
204-
String thisName = String.format(thisFormat, s);
205-
thisAccess.putMetadata(REFINE_KEY,
206-
Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName)));
206+
String thisName = String.format(Formats.THIS, s);
207+
thisAccess.putMetadata(Keys.REFINEMENT,
208+
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
207209
}
208210
}
209211

@@ -227,7 +229,7 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) {
227229
CtFieldWrite<?> fw = ((CtFieldWrite<?>) ex);
228230
CtFieldReference<?> cr = fw.getVariable();
229231
CtField<?> f = fw.getVariable().getDeclaration();
230-
String updatedVarName = String.format(thisFormat, cr.getSimpleName());
232+
String updatedVarName = String.format(Formats.THIS, cr.getSimpleName());
231233
checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f);
232234

233235
// corresponding ghost function update
@@ -249,9 +251,9 @@ public <T> void visitCtArrayRead(CtArrayRead<T> arrayRead) {
249251
}
250252

251253
super.visitCtArrayRead(arrayRead);
252-
String name = String.format(instanceFormat, "arrayAccess", context.getCounter());
254+
String name = String.format(Formats.INSTANCE, "arrayAccess", context.getCounter());
253255
context.addVarToContext(name, arrayRead.getType(), new Predicate(), arrayRead);
254-
arrayRead.putMetadata(REFINE_KEY, Predicate.createVar(name));
256+
arrayRead.putMetadata(Keys.REFINEMENT, Predicate.createVar(name));
255257
// TODO predicate for now is always TRUE
256258
}
257259

@@ -261,15 +263,15 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
261263
return;
262264
}
263265

264-
List<String> types = Arrays.asList(implementedTypes);
266+
List<String> types = Arrays.asList(Types.IMPLEMENTED);
265267
String type = lit.getType().getQualifiedName();
266268
if (types.contains(type)) {
267-
lit.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR),
269+
lit.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
268270
Predicate.createLit(lit.getValue().toString(), type)));
269271

270272
} else if (lit.getType().getQualifiedName().equals("java.lang.String")) {
271273
// Only taking care of strings inside refinements
272-
} else if (type.equals(Utils.NULL_TYPE)) {
274+
} else if (type.equals(Types.NULL)) {
273275
// Skip null literals
274276
} else {
275277
throw new NotImplementedException(
@@ -293,10 +295,10 @@ public <T> void visitCtField(CtField<T> f) {
293295
// context.addVarToContext(f.getSimpleName(), f.getType(),
294296
// c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new
295297
// Predicate()) );
296-
String nname = String.format(thisFormat, f.getSimpleName());
298+
String nname = String.format(Formats.THIS, f.getSimpleName());
297299
Predicate ret = new Predicate();
298300
if (c.isPresent()) {
299-
ret = c.get().substituteVariable(WILD_VAR, nname).substituteVariable(f.getSimpleName(), nname);
301+
ret = c.get().substituteVariable(Keys.WILDCARD, nname).substituteVariable(f.getSimpleName(), nname);
300302
}
301303
RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f);
302304
if (v instanceof Variable) {
@@ -315,27 +317,27 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
315317
RefinedVariable rv = context.getVariableByName(fieldName);
316318
if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent()
317319
&& ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) {
318-
fieldRead.putMetadata(REFINE_KEY, context.getVariableRefinements(fieldName));
320+
fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName));
319321
} else {
320-
fieldRead.putMetadata(REFINE_KEY,
321-
Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(fieldName)));
322+
fieldRead.putMetadata(Keys.REFINEMENT,
323+
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName)));
322324
}
323325

324-
} else if (context.hasVariable(String.format(thisFormat, fieldName))) {
325-
String thisName = String.format(thisFormat, fieldName);
326-
fieldRead.putMetadata(REFINE_KEY,
327-
Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName)));
326+
} else if (context.hasVariable(String.format(Formats.THIS, fieldName))) {
327+
String thisName = String.format(Formats.THIS, fieldName);
328+
fieldRead.putMetadata(Keys.REFINEMENT,
329+
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));
328330

329331
} else if (fieldRead.getVariable().getSimpleName().equals("length")) {
330332
String targetName = fieldRead.getTarget().toString();
331333
try {
332-
fieldRead.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR),
334+
fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD),
333335
BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter())));
334336
} catch (ParsingException e) {
335337
return; // error already in ErrorEmitter
336338
}
337339
} else {
338-
fieldRead.putMetadata(REFINE_KEY, new Predicate());
340+
fieldRead.putMetadata(Keys.REFINEMENT, new Predicate());
339341
// TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE
340342
}
341343

@@ -417,8 +419,8 @@ public void visitCtIf(CtIf ifElement) {
417419
} catch (ParsingException e) {
418420
return; // error already in ErrorEmitter
419421
}
420-
String freshVarName = String.format(freshFormat, context.getCounter());
421-
expRefs = expRefs.substituteVariable(WILD_VAR, freshVarName);
422+
String freshVarName = String.format(Formats.FRESH, context.getCounter());
423+
expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName);
422424
Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs);
423425
expRefs = Predicate.createConjunction(expRefs, lastExpRefs);
424426

@@ -470,11 +472,11 @@ public <T> void visitCtArrayWrite(CtArrayWrite<T> arrayWrite) {
470472
BuiltinFunctionPredicate fp;
471473
try {
472474
fp = BuiltinFunctionPredicate.builtin_addToIndex(arrayWrite.getTarget().toString(), index.toString(),
473-
WILD_VAR, arrayWrite, getErrorEmitter());
475+
Keys.WILDCARD, arrayWrite, getErrorEmitter());
474476
} catch (ParsingException e) {
475477
return; // error already in ErrorEmitter
476478
}
477-
arrayWrite.putMetadata(REFINE_KEY, fp);
479+
arrayWrite.putMetadata(Keys.REFINEMENT, fp);
478480
}
479481

480482
@Override
@@ -487,7 +489,7 @@ public <T> void visitCtConditional(CtConditional<T> conditional) {
487489
Predicate cond = getRefinement(conditional.getCondition());
488490
Predicate c = Predicate.createITE(cond, getRefinement(conditional.getThenExpression()),
489491
getRefinement(conditional.getElseExpression()));
490-
conditional.putMetadata(REFINE_KEY, c);
492+
conditional.putMetadata(Keys.REFINEMENT, c);
491493
}
492494

493495
@Override
@@ -582,12 +584,12 @@ private Predicate substituteAllVariablesForLastInstance(Predicate c) {
582584
* Cannot be null
583585
*/
584586
private <T> void getPutVariableMetadada(CtElement elem, String name) {
585-
Predicate cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(name));
587+
Predicate cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(name));
586588
Optional<VariableInstance> ovi = context.getLastVariableInstance(name);
587589
if (ovi.isPresent()) {
588-
cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(ovi.get().getName()));
590+
cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(ovi.get().getName()));
589591
}
590592

591-
elem.putMetadata(REFINE_KEY, cref);
593+
elem.putMetadata(Keys.REFINEMENT, cref);
592594
}
593595
}

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

Lines changed: 17 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,9 @@
1717
import liquidjava.rj_language.Predicate;
1818
import liquidjava.rj_language.parsing.ParsingException;
1919
import liquidjava.rj_language.parsing.RefinementsParser;
20-
import liquidjava.utils.Utils;
20+
import liquidjava.utils.constants.Formats;
21+
import liquidjava.utils.constants.Keys;
22+
import liquidjava.utils.constants.Types;
2123
import spoon.reflect.code.CtExpression;
2224
import spoon.reflect.code.CtLiteral;
2325
import spoon.reflect.code.CtNewArray;
@@ -31,16 +33,6 @@
3133
import spoon.reflect.visitor.CtScanner;
3234

3335
public abstract class TypeChecker extends CtScanner {
34-
public final String REFINE_KEY = "refinement";
35-
public final String TARGET_KEY = "target";
36-
// public final String STATE_KEY = "state";
37-
public final String THIS = "this";
38-
public final String WILD_VAR = "_";
39-
public final String freshFormat = "#fresh_%d";
40-
public final String instanceFormat = "#%s_%d";
41-
public final String thisFormat = "this#%s";
42-
public String[] implementedTypes = { "boolean", "int", "short", "long", "float", "double" }; // TODO add
43-
// types e.g., "int[]"
4436

4537
Context context;
4638
Factory factory;
@@ -63,7 +55,7 @@ public Factory getFactory() {
6355
}
6456

6557
public Predicate getRefinement(CtElement elem) {
66-
Predicate c = (Predicate) elem.getMetadata(REFINE_KEY);
58+
Predicate c = (Predicate) elem.getMetadata(Keys.REFINEMENT);
6759
return c == null ? new Predicate() : c;
6860
}
6961

@@ -142,7 +134,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
142134
context.addGhostClass(g.getParentClassName());
143135

144136
List<CtExpression<?>> ls = e.getElements();
145-
Predicate ip = Predicate.createInvocation(g.getName(), Predicate.createVar(THIS));
137+
Predicate ip = Predicate.createInvocation(g.getName(), Predicate.createVar(Keys.WILDCARD));
146138
int order = 0;
147139
for (CtExpression<?> ce : ls) {
148140
if (ce instanceof CtLiteral<?>) {
@@ -154,7 +146,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
154146
gs.setGhostParent(g);
155147
gs.setRefinement(
156148
/* new OperationPredicate(new InvocationPredicate(f, THIS), "<-->", */
157-
Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Utils.INT))); // open(THIS)
149+
Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS)
158150
// ->
159151
// state1(THIS)
160152
// == 1
@@ -258,7 +250,7 @@ protected void handleAlias(String value, CtElement element) {
258250
errorEmitter);
259251
return;
260252
}
261-
AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path);
253+
AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path);
262254
context.addAlias(aw);
263255
}
264256
} catch (ParsingException e) {
@@ -295,12 +287,12 @@ else if (expectedType.isPresent())
295287
else
296288
cEt = new Predicate();
297289

298-
cEt = cEt.substituteVariable(WILD_VAR, simpleName);
299-
Predicate cet = cEt.substituteVariable(WILD_VAR, simpleName);
290+
cEt = cEt.substituteVariable(Keys.WILDCARD, simpleName);
291+
Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName);
300292

301-
String newName = String.format(instanceFormat, simpleName, context.getCounter());
302-
Predicate correctNewRefinement = refinementFound.substituteVariable(WILD_VAR, newName);
303-
correctNewRefinement = correctNewRefinement.substituteVariable(THIS, newName);
293+
String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter());
294+
Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName);
295+
correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName);
304296
cEt = cEt.substituteVariable(simpleName, newName);
305297

306298
// Substitute variable in verification
@@ -314,18 +306,16 @@ else if (expectedType.isPresent())
314306
}
315307

316308
public void checkSMT(Predicate expectedType, CtElement element) {
317-
vcChecker.processSubtyping(expectedType, context.getGhostState(), WILD_VAR, THIS, element, factory);
318-
element.putMetadata(REFINE_KEY, expectedType);
309+
vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory);
310+
element.putMetadata(Keys.REFINEMENT, expectedType);
319311
}
320312

321-
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String string) {
322-
vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, target, string,
323-
factory);
313+
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) {
314+
vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, moreInfo, factory);
324315
}
325316

326317
public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) {
327-
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, p,
328-
factory);
318+
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
329319
}
330320

331321
public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customeMessage) {

0 commit comments

Comments
 (0)