Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
19 changes: 17 additions & 2 deletions latte/src/main/java/typechecking/LatteAbstractChecker.java
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,29 @@ public LatteAbstractChecker( SymbolicEnvironment symbEnv,
this.permEnv = permEnv;
this.maps = maps;
}
/**

/**
* Log info with indentation
* @param text
*/
protected void logInfo(String text) {
logger.info(" ".repeat(4*loggingSpaces) + "|- " + text);
}

/**
* Log info with indentation
* @param text
* @param ce The CtElement to which the Log relates to
*/
protected void logInfo(String text, CtElement ce) {
if(!ce.getPosition().isValidPosition())
logger.info(" ".repeat(4*loggingSpaces) + "|- " + text);
else{
String pos = ce.getPosition().getFile().getName() + ":" + ce.getPosition().getLine();
logger.info(" ".repeat(4*loggingSpaces) + "|- " + text + " (" + pos + ")");
}

}

/**
* Log error with indentation
Expand Down
12 changes: 6 additions & 6 deletions latte/src/main/java/typechecking/LatteClassFirstPass.java
Original file line number Diff line number Diff line change
Expand Up @@ -22,17 +22,17 @@ public LatteClassFirstPass(SymbolicEnvironment se, PermissionEnvironment pe,

@Override
public <T> void visitCtClass(CtClass<T> ctClass) {
logInfo("Visiting class: " + ctClass.getSimpleName());
logInfo("Visiting class: " + ctClass.getSimpleName(), ctClass);
// Add the class to the type reference and class map
CtTypeReference<?> typeRef1 = ctClass.getReference();
maps.addTypeClass(typeRef1, ctClass);
CtTypeReference<?> typeRef = ctClass.getReference();
maps.addTypeClass(typeRef, ctClass);
super.visitCtClass(ctClass);
}


@Override
public <T> void visitCtField(CtField<T> f) {
logInfo("Visiting field: " + f.getSimpleName());
logInfo("Visiting field: " + f.getSimpleName(), f);
loggingSpaces++;
CtElement k = f.getParent();
if (k instanceof CtClass){
Expand All @@ -54,14 +54,14 @@ public <T> void visitCtField(CtField<T> f) {

@Override
public <T> void visitCtMethod(CtMethod<T> m) {
logInfo("Visiting method: " + m.getSimpleName());
logInfo("Visiting method: " + m.getSimpleName(), m);
maps.addMethod((CtClass<?>) m.getParent(), m);
super.visitCtMethod(m);
}

@Override
public <T> void visitCtConstructor(CtConstructor<T> c) {
logInfo("Visiting constructor: " + c.getSimpleName());
logInfo("Visiting constructor: " + c.getSimpleName(), c);
maps.addConstructor((CtClass<?>) c.getParent(), c);
super.visitCtConstructor(c);
}
Expand Down
38 changes: 19 additions & 19 deletions latte/src/main/java/typechecking/LatteTypeChecker.java
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ public LatteTypeChecker( SymbolicEnvironment symbEnv,

@Override
public <T> void visitCtClass(CtClass<T> ctClass) {
logInfo("Visiting class: <" + ctClass.getSimpleName()+">");
logInfo("Visiting class: <" + ctClass.getSimpleName()+">", ctClass);
enterScopes();
super.visitCtClass(ctClass);
exitScopes();
Expand All @@ -57,7 +57,7 @@ public <T> void visitCtClass(CtClass<T> ctClass) {

@Override
public <T> void visitCtConstructor(CtConstructor<T> c) {
logInfo("Visiting constructor <"+ c.getSimpleName()+">");
logInfo("Visiting constructor <"+ c.getSimpleName()+">", c);
enterScopes();

// Assume 'this' is a parameter always borrowed
Expand All @@ -71,7 +71,7 @@ public <T> void visitCtConstructor(CtConstructor<T> c) {

@Override
public <T> void visitCtMethod(CtMethod<T> m) {
logInfo("Visiting method <"+ m.getSimpleName()+">");
logInfo("Visiting method <"+ m.getSimpleName()+">", m);
enterScopes();

// Assume 'this' is a parameter always borrowed
Expand All @@ -85,7 +85,7 @@ public <T> void visitCtMethod(CtMethod<T> m) {

@Override
public <T> void visitCtParameter(CtParameter<T> parameter) {
logInfo("Visiting parameter <"+ parameter.getSimpleName()+">");
logInfo("Visiting parameter <"+ parameter.getSimpleName()+">", parameter);
loggingSpaces++;
super.visitCtParameter(parameter);

Expand Down Expand Up @@ -125,7 +125,7 @@ public <T> void visitCtParameter(CtParameter<T> parameter) {
*/
@Override
public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
logInfo("Visiting local variable <"+ localVariable.getSimpleName() +">");
logInfo("Visiting local variable <"+ localVariable.getSimpleName() +">", localVariable);
loggingSpaces++;
// CheckVarDecl
// 1) Add the variable to the typing context
Expand Down Expand Up @@ -178,7 +178,7 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
*/
@Override
public <T> void visitCtInvocation(CtInvocation<T> invocation) {
logInfo("Visiting invocation <"+ invocation.toStringDebug()+">");
logInfo("Visiting invocation <"+ invocation.toStringDebug()+">", invocation);
super.visitCtInvocation(invocation);

String metName = invocation.getExecutable().getSimpleName();
Expand Down Expand Up @@ -248,7 +248,7 @@ public <T> void visitCtInvocation(CtInvocation<T> invocation) {
*/
@Override
public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
logInfo("Visiting field read <"+ fieldRead.toStringDebug()+">");
logInfo("Visiting field read <"+ fieldRead.toStringDebug()+">", fieldRead);
loggingSpaces++;

super.visitCtFieldRead(fieldRead);
Expand Down Expand Up @@ -335,7 +335,7 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
*/
@Override
public <T> void visitCtFieldWrite(CtFieldWrite<T> fieldWrite) {
logInfo("Visiting field write <"+ fieldWrite.toStringDebug()+">");
logInfo("Visiting field write <"+ fieldWrite.toStringDebug()+">", fieldWrite);
super.visitCtFieldWrite(fieldWrite);
CtExpression<?> ce = fieldWrite.getTarget();
if (ce instanceof CtVariableReadImpl){
Expand Down Expand Up @@ -374,7 +374,7 @@ public <T> void visitCtFieldWrite(CtFieldWrite<T> fieldWrite) {
*/
@Override
public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) {
logInfo("Visiting assignment <"+ assignment.toStringDebug()+">");
logInfo("Visiting assignment <"+ assignment.toStringDebug()+">", assignment);
loggingSpaces++;
super.visitCtAssignment(assignment);

Expand Down Expand Up @@ -439,7 +439,7 @@ public <T, A extends T> void visitCtAssignment(CtAssignment<T, A> assignment) {

@Override
public <T> void visitCtConstructorCall(CtConstructorCall<T> constCall) {
logInfo("Visiting constructor call <"+ constCall.toStringDebug()+">");
logInfo("Visiting constructor call <"+ constCall.toStringDebug()+">", constCall);
super.visitCtConstructorCall(constCall);

// Check if all arguments follow the restrictions
Expand Down Expand Up @@ -472,7 +472,7 @@ private void handleConstructorArgs (CtConstructorCall<?> constCall){
CtConstructor<?> c = maps.geCtConstructor(klass, paramSize);
List<SymbolicValue> paramSymbValues = new ArrayList<>();
if (klass == null || c == null){
logInfo(String.format("Cannot find the constructor for {} in the context", constCall.getType()));
logInfo(String.format("Cannot find the constructor for {} in the context", constCall.getType()), constCall);
return;
}
for (int i = 0; i < paramSize; i++){
Expand All @@ -488,7 +488,7 @@ private void handleConstructorArgs (CtConstructorCall<?> constCall){
if (!vvPerm.isGreaterEqualThan(Uniqueness.BORROWED)){
logError(String.format("Symbolic value %s:%s is not greater than BORROWED", vv, vvPerm), arg);
}
logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA));
logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA), constCall);
// Σ′ ⊢ 𝑒1, ... , 𝑒𝑛 : 𝛼1, ... , 𝛼𝑛 ⊣ Σ′′
if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA))
logError(String.format("Expected %s but got %s",
Expand All @@ -507,7 +507,7 @@ private void handleConstructorArgs (CtConstructorCall<?> constCall){

@Override
public void visitCtIf(CtIf ifElement) {
logInfo("Visiting if <"+ ifElement.toStringDebug()+">");
logInfo("Visiting if <"+ ifElement.toStringDebug()+">", ifElement);
// super.visitCtIf(ifElement);

// Evaluate the conditions
Expand Down Expand Up @@ -543,7 +543,7 @@ public void visitCtIf(CtIf ifElement) {

@Override
public <R> void visitCtReturn(CtReturn<R> returnStatement) {
logInfo("Visiting return <"+ returnStatement.toStringDebug()+">");
logInfo("Visiting return <"+ returnStatement.toStringDebug()+">", returnStatement);
super.visitCtReturn(returnStatement);

CtExpression<?> returned = returnStatement.getReturnedExpression();
Expand All @@ -567,7 +567,7 @@ public <R> void visitCtReturn(CtReturn<R> returnStatement) {
*/
@Override
public <T> void visitCtBinaryOperator(CtBinaryOperator<T> operator) {
logInfo("Visiting binary operator <"+ operator.toStringDebug()+">");
logInfo("Visiting binary operator <"+ operator.toStringDebug()+">", operator);
loggingSpaces++;
super.visitCtBinaryOperator(operator);

Expand All @@ -589,7 +589,7 @@ public <T> void visitCtBinaryOperator(CtBinaryOperator<T> operator) {
*/
@Override
public <T> void visitCtUnaryOperator(CtUnaryOperator<T> operator) {
logInfo("Visiting unary operator <"+ operator.toStringDebug()+">");
logInfo("Visiting unary operator <"+ operator.toStringDebug()+">", operator);
loggingSpaces++;
super.visitCtUnaryOperator(operator);

Expand All @@ -611,7 +611,7 @@ public <T> void visitCtUnaryOperator(CtUnaryOperator<T> operator) {
*/
@Override
public <T> void visitCtLocalVariableReference(CtLocalVariableReference<T> reference) {
logInfo("Visiting local variable reference <"+ reference.toString()+">");
logInfo("Visiting local variable reference <"+ reference.toString()+">", reference);
loggingSpaces++;
super.visitCtLocalVariableReference(reference);

Expand All @@ -634,7 +634,7 @@ public <T> void visitCtLocalVariableReference(CtLocalVariableReference<T> refere
@Override
public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
loggingSpaces++;
logInfo("Visiting variable read <"+ variableRead.toString()+">");
logInfo("Visiting variable read <"+ variableRead.toString()+">", variableRead);
super.visitCtVariableRead(variableRead);

SymbolicValue sv = symbEnv.get(variableRead.getVariable().getSimpleName());
Expand All @@ -649,7 +649,7 @@ public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
*/
@Override
public <T> void visitCtLiteral(CtLiteral<T> literal) {
logInfo("Visiting literal <"+ literal.toString()+">");
logInfo("Visiting literal <"+ literal.toString()+">", literal);

super.visitCtLiteral(literal);

Expand Down
Loading