Skip to content

Logging element draft #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
FrogOfJuly wants to merge 10 commits into from
Closed

Logging element draft #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
c1a6d98
removed absent tests
Mar 23, 2023
362c163
no internal update as functions are opaque
Mar 23, 2023
3fb8d1b
Merge branch 'field_updates' of github.com:CatarinaGamboa/liquidjava …
alcides Nov 30, 2024
18cf222
Merge branch 'master' into field_updates
alcides Nov 30, 2024
eabd054
logging element draft
Oct 17, 2022
6e4856d
LogElement introduction
Oct 22, 2022
21c65c5
expected invocation, got LogEleemnt fixed
Oct 22, 2022
3da600c
Rebased logging
alcides Nov 30, 2024
3337774
Merge branch 'main' of github.com:CatarinaGamboa/liquidjava into logging
alcides Nov 30, 2024
d38470e
Merge branch 'main' into logging
alcides Nov 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
177 changes: 177 additions & 0 deletions liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/logging/LogElement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,177 @@
package liquidjava.logging;

import liquidjava.processor.context.PlacementInCode;
import spoon.reflect.code.CtComment;
import spoon.reflect.code.CtInvocation;
import spoon.reflect.cu.SourcePosition;
import spoon.reflect.declaration.CtAnnotation;
import spoon.reflect.declaration.CtElement;
import spoon.reflect.declaration.ParentNotInitializedException;
import spoon.reflect.path.CtPath;
import spoon.reflect.path.CtRole;
import spoon.reflect.reference.CtTypeReference;
import spoon.reflect.visitor.Filter;

import java.lang.annotation.Annotation;
import java.lang.annotation.ElementType;
import java.util.*;
import java.util.function.Function;
import java.util.stream.Collectors;

public class LogElement {
final private CtElement elem;

public LogElement(CtElement elem) {
this.elem = elem;
}

public <A extends Annotation> A getAnnotation(Class<A> var1) {
return elem.getAnnotation(var1);
}

public <A extends Annotation> boolean hasAnnotation(Class<A> var1) {
return elem.hasAnnotation(var1);
}

public List<CtAnnotation<? extends Annotation>> getAnnotations() {
return elem.getAnnotations();
}

public String getDocComment() {
return elem.getDocComment();
}

public String getShortRepresentation() {
return elem.getShortRepresentation();
}

public SourcePosition getPosition() {
return elem.getPosition();
}

public List<LogElement> getAnnotatedChildren(Class<? extends Annotation> var1) {
return elem.getAnnotatedChildren(var1).stream().map(LogElement::new).collect(Collectors.toList());
}

public boolean isImplicit() {
return elem.isImplicit();
}

public Set<CtTypeReference<?>> getReferencedTypes() {
return elem.getReferencedTypes();
}

public <E extends CtElement> List<LogElement> getElements(Filter<E> var1) {
return elem.getElements(var1).stream().map(LogElement::new).collect(Collectors.toList());
}

public LogElement getParent() throws ParentNotInitializedException {
return new LogElement(elem.getParent());
}

public <P extends CtElement> LogElement getParent(Class<P> var1) throws ParentNotInitializedException {
return new LogElement(elem.getParent(var1));
}

public <E extends CtElement> LogElement getParent(Filter<E> var1) throws ParentNotInitializedException {
return new LogElement(elem.getParent(var1));
}

public boolean isParentInitialized() {
return elem.isParentInitialized();
}

public boolean hasParent(LogElement var1) {
return elem.hasParent(var1.elem);
}

public CtRole getRoleInParent() {
return elem.getRoleInParent();
}

public Map<String, Object> getAllMetadata() {
return elem.getAllMetadata();
}

public Set<String> getMetadataKeys() {
return elem.getMetadataKeys();
}

public List<CtComment> getComments() {
return elem.getComments();
}

public <T> T getValueByRole(CtRole var1) {
return elem.getValueByRole(var1);
}

public CtPath getPath() {
return elem.getPath();
}

public Iterator<LogElement> descendantIterator() {
return new Iterator<LogElement>() {
final Iterator<CtElement> elemIt = elem.descendantIterator();

@Override
public boolean hasNext() {
return elemIt.hasNext();
}

@Override
public LogElement next() {
return new LogElement(elemIt.next());
}
};
}

public Iterable<LogElement> asIterable() {
return new Iterable<LogElement>() {
final Iterable<CtElement> elemIterable = elem.asIterable();

@Override
public Iterator<LogElement> iterator() {
return new Iterator<LogElement>() {
final Iterator<CtElement> elemIt = elemIterable.iterator();

@Override
public boolean hasNext() {
return elemIt.hasNext();
}

@Override
public LogElement next() {
return new LogElement(elemIt.next());
}
};
}
};
}

public LogElement strippedElement() {
CtElement elemCopy = elem.clone();
// cleanup annotations
if (elem.getAnnotations().size() > 0) {
for (CtAnnotation<? extends Annotation> a : elem.getAnnotations()) {
elemCopy.removeAnnotation(a);
}
}
// cleanup comments
if (elem.getComments().size() > 0) {
for (CtComment a : elem.getComments()) {
elemCopy.removeComment(a);
}
}
return new LogElement(elemCopy);
}

public String toString() {
return elem.toString();
}

public Optional<String> inspectInvocation(Function<CtInvocation<?>, String> insperctor){
return elem instanceof CtInvocation<?> ?
Optional.of(insperctor.apply((CtInvocation<?>) elem)) :
Optional.empty();
}
}
26 changes: 13 additions & 13 deletions liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,12 @@
import java.util.Formatter;
import java.util.HashMap;
import java.util.Locale;

import liquidjava.logging.LogElement;
import liquidjava.processor.VCImplication;
import liquidjava.processor.context.PlacementInCode;
import liquidjava.rj_language.Predicate;
import spoon.reflect.code.CtLiteral;
import spoon.reflect.declaration.CtElement;

public class ErrorHandler {

Expand All @@ -16,16 +17,15 @@ public class ErrorHandler {
*
* @param <T>
* @param var
* @param s
* @param expectedType
* @param cSMT
*/
public static <T> void printError(CtElement var, Predicate expectedType, Predicate cSMT,
public static <T> void printError(LogElement var, Predicate expectedType, Predicate cSMT,
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
printError(var, null, expectedType, cSMT, map, ee);
}

public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
public static <T> void printError(LogElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
// cSMT.toString();
Expand All @@ -49,7 +49,7 @@ public static <T> void printError(CtElement var, String moreInfo, Predicate expe
errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
}

public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
public static void printStateMismatch(LogElement element, String method, VCImplication constraintForErrorMsg,
String states, HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {

String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + ";
Expand Down Expand Up @@ -78,7 +78,7 @@ public static void printStateMismatch(CtElement element, String method, VCImplic
errorl.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
}

public static <T> void printErrorUnknownVariable(CtElement var, String et, String correctRefinement,
public static <T> void printErrorUnknownVariable(LogElement var, String et, String correctRefinement,
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {

String resumeMessage = "Encountered unknown variable";
Expand All @@ -97,7 +97,7 @@ public static <T> void printErrorUnknownVariable(CtElement var, String et, Strin
errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
}

public static <T> void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg,
public static <T> void printNotFound(LogElement var, Predicate constraint, Predicate constraint2, String msg,
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {

StringBuilder sb = new StringBuilder();
Expand All @@ -114,7 +114,7 @@ public static <T> void printNotFound(CtElement var, Predicate constraint, Predic
errorl.addError(msg, sb.toString(), var.getPosition(), 2, map);
}

public static <T> void printErrorArgs(CtElement var, Predicate expectedType, String msg,
public static <T> void printErrorArgs(LogElement var, Predicate expectedType, String msg,
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
StringBuilder sb = new StringBuilder();
sb.append("______________________________________________________\n");
Expand All @@ -128,7 +128,7 @@ public static <T> void printErrorArgs(CtElement var, Predicate expectedType, Str
errorl.addError(title, sb.toString(), var.getPosition(), 2, map);
}

public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message,
public static void printErrorTypeMismatch(LogElement element, Predicate expectedType, String message,
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
StringBuilder sb = new StringBuilder();
sb.append("______________________________________________________\n");
Expand All @@ -141,7 +141,7 @@ public static void printErrorTypeMismatch(CtElement element, Predicate expectedT
errorl.addError(message, sb.toString(), element.getPosition(), 2, map);
}

public static void printSameStateSetError(CtElement element, Predicate p, String name,
public static void printSameStateSetError(LogElement element, Predicate p, String name,
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
String resume = "Error found multiple disjoint states from a State Set in a refinement";

Expand All @@ -160,7 +160,7 @@ public static void printSameStateSetError(CtElement element, Predicate p, String
errorl.addError(resume, sb.toString(), element.getPosition(), 1, map);
}

public static void printErrorConstructorFromState(CtElement element, CtLiteral<String> from, ErrorEmitter errorl) {
public static void printErrorConstructorFromState(LogElement element, CtLiteral<String> from, ErrorEmitter errorl) {
StringBuilder sb = new StringBuilder();
sb.append("______________________________________________________\n");
String s = " Error found constructor with FROM state (Constructor's should only have a TO state)\n\n";
Expand All @@ -173,7 +173,7 @@ public static void printErrorConstructorFromState(CtElement element, CtLiteral<S
errorl.addError(s, sb.toString(), element.getPosition(), 1);
}

public static void printCostumeError(CtElement element, String msg, ErrorEmitter errorl) {
public static void printCostumeError(LogElement element, String msg, ErrorEmitter errorl) {
StringBuilder sb = new StringBuilder();
sb.append("______________________________________________________\n");
String s = "Found Error: " + msg;
Expand All @@ -186,7 +186,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter
errorl.addError(s, sb.toString(), element.getPosition(), 1);
}

public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter errorl) {
public static void printSyntaxError(String msg, String ref, LogElement element, ErrorEmitter errorl) {
StringBuilder sb = new StringBuilder();
sb.append("______________________________________________________\n");
StringBuilder sbtitle = new StringBuilder();
Expand Down
Loading
Loading