Skip to content

Commit 3da600c

Browse files
alcidesalcides
committed
Rebased logging
1 parent 21c65c5 commit 3da600c

File tree

6 files changed

+242
-78
lines changed

6 files changed

+242
-78
lines changed

‎liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java‎

Lines changed: 174 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,174 @@
1+
package liquidjava.logging;
2+
3+
import spoon.reflect.code.CtComment;
4+
import spoon.reflect.code.CtInvocation;
5+
import spoon.reflect.cu.SourcePosition;
6+
import spoon.reflect.declaration.CtAnnotation;
7+
import spoon.reflect.declaration.CtElement;
8+
import spoon.reflect.declaration.ParentNotInitializedException;
9+
import spoon.reflect.path.CtPath;
10+
import spoon.reflect.path.CtRole;
11+
import spoon.reflect.reference.CtTypeReference;
12+
import spoon.reflect.visitor.Filter;
13+
14+
import java.lang.annotation.Annotation;
15+
import java.util.*;
16+
import java.util.function.Function;
17+
import java.util.stream.Collectors;
18+
19+
public class LogElement {
20+
final private CtElement elem;
21+
22+
public LogElement(CtElement elem) {
23+
this.elem = elem;
24+
}
25+
26+
public <A extends Annotation> A getAnnotation(Class<A> var1) {
27+
return elem.getAnnotation(var1);
28+
}
29+
30+
public <A extends Annotation> boolean hasAnnotation(Class<A> var1) {
31+
return elem.hasAnnotation(var1);
32+
}
33+
34+
public List<CtAnnotation<? extends Annotation>> getAnnotations() {
35+
return elem.getAnnotations();
36+
}
37+
38+
public String getDocComment() {
39+
return elem.getDocComment();
40+
}
41+
42+
public String getShortRepresentation() {
43+
return elem.getShortRepresentation();
44+
}
45+
46+
public SourcePosition getPosition() {
47+
return elem.getPosition();
48+
}
49+
50+
public List<LogElement> getAnnotatedChildren(Class<? extends Annotation> var1) {
51+
return elem.getAnnotatedChildren(var1).stream().map(LogElement::new).collect(Collectors.toList());
52+
}
53+
54+
public boolean isImplicit() {
55+
return elem.isImplicit();
56+
}
57+
58+
public Set<CtTypeReference<?>> getReferencedTypes() {
59+
return elem.getReferencedTypes();
60+
}
61+
62+
public <E extends CtElement> List<LogElement> getElements(Filter<E> var1) {
63+
return elem.getElements(var1).stream().map(LogElement::new).collect(Collectors.toList());
64+
}
65+
66+
public LogElement getParent() throws ParentNotInitializedException {
67+
return new LogElement(elem.getParent());
68+
}
69+
70+
public <P extends CtElement> LogElement getParent(Class<P> var1) throws ParentNotInitializedException {
71+
return new LogElement(elem.getParent(var1));
72+
}
73+
74+
public <E extends CtElement> LogElement getParent(Filter<E> var1) throws ParentNotInitializedException {
75+
return new LogElement(elem.getParent(var1));
76+
}
77+
78+
public boolean isParentInitialized() {
79+
return elem.isParentInitialized();
80+
}
81+
82+
public boolean hasParent(LogElement var1) {
83+
return elem.hasParent(var1.elem);
84+
}
85+
86+
public CtRole getRoleInParent() {
87+
return elem.getRoleInParent();
88+
}
89+
90+
public Map<String, Object> getAllMetadata() {
91+
return elem.getAllMetadata();
92+
}
93+
94+
public Set<String> getMetadataKeys() {
95+
return elem.getMetadataKeys();
96+
}
97+
98+
public List<CtComment> getComments() {
99+
return elem.getComments();
100+
}
101+
102+
public <T> T getValueByRole(CtRole var1) {
103+
return elem.getValueByRole(var1);
104+
}
105+
106+
public CtPath getPath() {
107+
return elem.getPath();
108+
}
109+
110+
public Iterator<LogElement> descendantIterator() {
111+
return new Iterator<LogElement>() {
112+
final Iterator<CtElement> elemIt = elem.descendantIterator();
113+
114+
@Override
115+
public boolean hasNext() {
116+
return elemIt.hasNext();
117+
}
118+
119+
@Override
120+
public LogElement next() {
121+
return new LogElement(elemIt.next());
122+
}
123+
};
124+
}
125+
126+
public Iterable<LogElement> asIterable() {
127+
return new Iterable<LogElement>() {
128+
final Iterable<CtElement> elemIterable = elem.asIterable();
129+
130+
@Override
131+
public Iterator<LogElement> iterator() {
132+
return new Iterator<LogElement>() {
133+
final Iterator<CtElement> elemIt = elemIterable.iterator();
134+
135+
@Override
136+
public boolean hasNext() {
137+
return elemIt.hasNext();
138+
}
139+
140+
@Override
141+
public LogElement next() {
142+
return new LogElement(elemIt.next());
143+
}
144+
};
145+
}
146+
};
147+
}
148+
149+
public LogElement strippedElement() {
150+
CtElement elemCopy = elem.clone();
151+
// cleanup annotations
152+
if (elem.getAnnotations().size() > 0) {
153+
for (CtAnnotation<? extends Annotation> a : elem.getAnnotations()) {
154+
elemCopy.removeAnnotation(a);
155+
}
156+
}
157+
// cleanup comments
158+
if (elem.getComments().size() > 0) {
159+
for (CtComment a : elem.getComments()) {
160+
elemCopy.removeComment(a);
161+
}
162+
}
163+
return new LogElement(elemCopy);
164+
}
165+
166+
public String toString() {
167+
return elem.toString();
168+
}
169+
170+
public Optional<String> inspectInvocation(Function<CtInvocation<?>, String> insperctor) {
171+
return elem instanceof CtInvocation<?> ? Optional.of(insperctor.apply((CtInvocation<?>) elem))
172+
: Optional.empty();
173+
}
174+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -78,8 +78,7 @@ public Predicate getAllRefinements() {
7878
}
7979

8080
/**
81-
* Gives the Predicate for a certain parameter index and regards all the
82-
* previous parameters' Predicates
81+
* Gives the Predicate for a certain parameter index and regards all the previous parameters' Predicates
8382
*
8483
* @param index
8584
*

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,8 @@
88
import org.apache.commons.lang3.NotImplementedException;
99

1010
import liquidjava.errors.ErrorEmitter;
11-
<<<<<<< HEAD:liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
12-
=======
1311
import liquidjava.errors.ErrorHandler;
1412
import liquidjava.logging.LogElement;
15-
>>>>>>> efcaaf1d (LogElement introduction):liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
1613
import liquidjava.processor.context.*;
1714
import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
1815
import liquidjava.processor.refinement_checker.general_checkers.OperationsChecker;

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -220,8 +220,7 @@ public boolean smtChecks(Predicate cSMT, Predicate expectedType, LogElement p) {
220220
}
221221

222222
/**
223-
* Checks the expectedType against the cSMT constraint. If the types do not
224-
* check and error is sent and the program
223+
* Checks the expectedType against the cSMT constraint. If the types do not check and error is sent and the program
225224
* ends
226225
*
227226
* @param cSMT

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

Lines changed: 61 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -158,8 +158,7 @@ public <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws Parsin
158158
}
159159

160160
/**
161-
* Retrieves all the refinements for the Operation including the refinements of
162-
* all operands for expressions without
161+
* Retrieves all the refinements for the Operation including the refinements of all operands for expressions without
163162
* a variable as parent
164163
*
165164
* @param operator
@@ -261,11 +260,12 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
261260
String newName = String.format(rtc.freshFormat, rtc.getContext().getCounter());
262261

263262
innerRefs = innerRefs.substituteVariable(rtc.WILD_VAR, newName);
264-
rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv);
265-
return new Predicate(newName, inv, rtc.getErrorEmitter()); // Return variable that represents the invocation
263+
rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, elementForLogging);
264+
return new Predicate(newName, elementForLogging, rtc.getErrorEmitter());// Return variable that represents
266265
}
267266
return rtc.getRefinement(element);
268267
// TODO Maybe add cases
268+
}
269269

270270
private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv, CtBinaryOperator<?> operator)
271271
throws ParsingException {
@@ -343,69 +343,69 @@ private <T> Predicate getRefinementUnaryVariableWrite(LogElement ex, CtUnaryOper
343343
*/
344344
private String getOperatorFromKind(BinaryOperatorKind kind) {
345345
switch (kind) {
346-
case PLUS:
347-
return Utils.PLUS;
348-
case MINUS:
349-
return Utils.MINUS;
350-
case MUL:
351-
return Utils.MUL;
352-
case DIV:
353-
return Utils.DIV;
354-
case MOD:
355-
return Utils.MOD;
356-
357-
case AND:
358-
return Utils.AND;
359-
case OR:
360-
return Utils.OR;
361-
362-
case EQ:
363-
return Utils.EQ;
364-
case NE:
365-
return Utils.NEQ;
366-
case GE:
367-
return Utils.GE;
368-
case GT:
369-
return Utils.GT;
370-
case LE:
371-
return Utils.LE;
372-
case LT:
373-
return Utils.LT;
374-
default:
375-
return null;
376-
// TODO COMPLETE WITH MORE OPERANDS
346+
case PLUS:
347+
return Utils.PLUS;
348+
case MINUS:
349+
return Utils.MINUS;
350+
case MUL:
351+
return Utils.MUL;
352+
case DIV:
353+
return Utils.DIV;
354+
case MOD:
355+
return Utils.MOD;
356+
357+
case AND:
358+
return Utils.AND;
359+
case OR:
360+
return Utils.OR;
361+
362+
case EQ:
363+
return Utils.EQ;
364+
case NE:
365+
return Utils.NEQ;
366+
case GE:
367+
return Utils.GE;
368+
case GT:
369+
return Utils.GT;
370+
case LE:
371+
return Utils.LE;
372+
case LT:
373+
return Utils.LT;
374+
default:
375+
return null;
376+
// TODO COMPLETE WITH MORE OPERANDS
377377
}
378378
}
379379

380380
private Predicate getOperatorFromKind(UnaryOperatorKind kind, LogElement elem) throws ParsingException {
381381
String ret = null;
382382
switch (kind) {
383-
case POSTINC:
384-
ret = rtc.WILD_VAR + " + 1";
385-
break;
386-
case POSTDEC:
387-
ret = rtc.WILD_VAR + " - 1";
388-
break;
389-
case PREINC:
390-
ret = rtc.WILD_VAR + " + 1";
391-
break;
392-
case PREDEC:
393-
ret = rtc.WILD_VAR + " - 1";
394-
break;
395-
case COMPL:
396-
ret = "(32 & " + rtc.WILD_VAR + ")";
397-
break;
398-
case NOT:
399-
ret = "!" + rtc.WILD_VAR;
400-
break;
401-
case POS:
402-
ret = "0 + " + rtc.WILD_VAR;
403-
break;
404-
case NEG:
405-
ret = "-" + rtc.WILD_VAR;
406-
break;
407-
default:
408-
throw new ParsingException(kind + "operation not supported");
383+
case POSTINC:
384+
ret = rtc.WILD_VAR + " + 1";
385+
break;
386+
case POSTDEC:
387+
ret = rtc.WILD_VAR + " - 1";
388+
break;
389+
case PREINC:
390+
ret = rtc.WILD_VAR + " + 1";
391+
break;
392+
case PREDEC:
393+
ret = rtc.WILD_VAR + " - 1";
394+
break;
395+
case COMPL:
396+
ret = "(32 & " + rtc.WILD_VAR + ")";
397+
break;
398+
case NOT:
399+
ret = "!" + rtc.WILD_VAR;
400+
break;
401+
case POS:
402+
ret = "0 + " + rtc.WILD_VAR;
403+
break;
404+
case NEG:
405+
ret = "-" + rtc.WILD_VAR;
406+
break;
407+
default:
408+
throw new ParsingException(kind + "operation not supported");
409409
}
410410
return new Predicate(ret, elem, rtc.getErrorEmitter());
411411
}

0 commit comments

Comments
 (0)