From f6746fff2caba50e2fbf0210a1ba03fa284cd308 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Fri, 13 Jun 2025 19:31:26 +0100 Subject: [PATCH 01/12] Added map for external methods annotations and new file for first pass --- latte/src/main/java/context/ClassLevelMaps.java | 17 ++++++++++++++++- .../ExternalRefinementFirstPass.java | 4 ++++ 2 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 latte/src/main/java/typechecking/ExternalRefinementFirstPass.java diff --git a/latte/src/main/java/context/ClassLevelMaps.java b/latte/src/main/java/context/ClassLevelMaps.java index f3029cc..c2bba21 100644 --- a/latte/src/main/java/context/ClassLevelMaps.java +++ b/latte/src/main/java/context/ClassLevelMaps.java @@ -20,6 +20,7 @@ public class ClassLevelMaps { Map, Map>> classFields; Map, Map>> classConstructors; Map, Map, CtMethod>> classMethods; + Map, Map, List>> externalMethodParamPermissions; @@ -28,6 +29,7 @@ public ClassLevelMaps() { classFields = new HashMap, Map>>(); classConstructors = new HashMap<>(); classMethods = new HashMap<>(); + externalMethodParamPermissions = new HashMap<>(); } public CtClass getClassFrom(CtTypeReference type) { @@ -241,6 +243,19 @@ public static void joinElim( } } - + public void addExternalMethodPermissions( + CtTypeReference typeRef, + String methodName, + int numParams, + List paramAnnotations + ) { + if (externalMethodParamPermissions == null) + externalMethodParamPermissions = new HashMap<>(); + + Pair methodSig = Pair.of(methodName, numParams); + externalMethodParamPermissions + .computeIfAbsent(typeRef, k -> new HashMap<>()) + .put(methodSig, paramAnnotations); + } } diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java new file mode 100644 index 0000000..8054c03 --- /dev/null +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -0,0 +1,4 @@ +package typechecking; + +public class ExternalRefinementFirstPass { +} From 32dc45e578f290cd20b84656d0301581ff464685 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Fri, 13 Jun 2025 21:50:05 +0100 Subject: [PATCH 02/12] external refinements pass implementation and related addition to CLM.java --- latte/pom.xml | 6 ++ .../src/main/java/context/ClassLevelMaps.java | 9 ++- .../ExternalRefinementFirstPass.java | 80 ++++++++++++++++++- 3 files changed, 92 insertions(+), 3 deletions(-) diff --git a/latte/pom.xml b/latte/pom.xml index 6b77334..fc9479d 100644 --- a/latte/pom.xml +++ b/latte/pom.xml @@ -96,6 +96,12 @@ ${version.spoon} + + org.apache.commons + commons-lang3 + 3.12.0 + + diff --git a/latte/src/main/java/context/ClassLevelMaps.java b/latte/src/main/java/context/ClassLevelMaps.java index c2bba21..9da0eae 100644 --- a/latte/src/main/java/context/ClassLevelMaps.java +++ b/latte/src/main/java/context/ClassLevelMaps.java @@ -243,7 +243,7 @@ public static void joinElim( } } - public void addExternalMethodPermissions( + public void addExternalMethodParamPermissions( CtTypeReference typeRef, String methodName, int numParams, @@ -258,4 +258,11 @@ public void addExternalMethodPermissions( .put(methodSig, paramAnnotations); } + public List getExternalMethodParamPermissions( + CtTypeReference clazz, String methodName, int arity) { + Map, List> methodMap = externalMethodParamPermissions.get(clazz); + if (methodMap == null) return null; + return methodMap.get(Pair.of(methodName, arity)); + } + } diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java index 8054c03..e7f218b 100644 --- a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -1,4 +1,80 @@ package typechecking; -public class ExternalRefinementFirstPass { -} +import context.ClassLevelMaps; +import context.PermissionEnvironment; +import context.SymbolicEnvironment; +import context.UniquenessAnnotation; +import spoon.reflect.code.CtBlock; +import spoon.reflect.declaration.*; +import spoon.reflect.reference.CtTypeReference; +import spoon.reflect.visitor.filter.TypeFilter; +import org.apache.commons.lang3.tuple.Pair; + +import java.lang.annotation.Annotation; +import java.util.*; + +/** + * First pass that collects permission annotations (@unique, @shared, etc.) + * for external method parameters and stores them in ClassLevelMaps. + */ +public class ExternalRefinementFirstPass extends LatteAbstractChecker { + + public ExternalRefinementFirstPass(SymbolicEnvironment symbEnv, + PermissionEnvironment permEnv, + ClassLevelMaps maps) { + super(symbEnv, permEnv, maps); + } + + @Override + public void visitCtInterface(CtInterface ctInterface) { + // @ExternalRefinementsFor annotation check + boolean hasAnnotation = ctInterface.getAnnotations().stream().anyMatch(ann -> + ann.getAnnotationType().getQualifiedName().equals("specification.ExternalRefinementsFor") + ); + + if (!hasAnnotation) { + return; + } + + CtTypeReference targetRef = null; + for (CtAnnotation annotation : ctInterface.getAnnotations()) { + if (annotation.getAnnotationType().getQualifiedName().equals("specification.ExternalRefinementsFor")) { + targetRef = (CtTypeReference) annotation.getValues().values().iterator().next(); + break; + } + } + + if (targetRef == null) { + logWarning("No target class specified in @ExternalRefinementsFor"); + return; + } + + if (ctInterface.isPublic()) { + logInfo("Processing external interface: " + ctInterface.getQualifiedName(), ctInterface); + scan(ctInterface.getMethods()); + } + } + + @Override + public void visitCtMethod(CtMethod method) { + CtTypeReference declaringClass = method.getDeclaringType().getReference(); + + // Skip if it has a body — it's not external + CtBlock body = method.getBody(); + if (body != null && !body.isImplicit()) return; + + List> parameters = method.getParameters(); + List paramAnnotations = new ArrayList<>(); + + for (CtParameter param : parameters) { + UniquenessAnnotation ua = new UniquenessAnnotation(param); + paramAnnotations.add(ua); + } + + Pair methodSig = Pair.of(method.getSimpleName(), parameters.size()); + + maps.addExternalMethodParamPermissions(declaringClass, methodSig.getLeft(), methodSig.getRight(), paramAnnotations); + + logInfo("Collected annotations for method: " + methodSig + " => " + paramAnnotations, method); + } +} \ No newline at end of file From 026cbd5b1c5e0aa7af0dfaa07427f4fb2fb1a127 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Fri, 13 Jun 2025 21:50:50 +0100 Subject: [PATCH 03/12] added external refinement to processor pipeline --- latte/src/main/java/typechecking/LatteProcessor.java | 1 + 1 file changed, 1 insertion(+) diff --git a/latte/src/main/java/typechecking/LatteProcessor.java b/latte/src/main/java/typechecking/LatteProcessor.java index 2ab807f..358e9e4 100644 --- a/latte/src/main/java/typechecking/LatteProcessor.java +++ b/latte/src/main/java/typechecking/LatteProcessor.java @@ -27,6 +27,7 @@ public void process(CtPackage pkg) { if (!visitedPackages.contains(pkg)) { visitedPackages.add(pkg); + pkg.accept(new ExternalRefinementFirstPass( se, pe, mtc)); pkg.accept(new LatteClassFirstPass( se, pe, mtc)); pkg.accept(new LatteTypeChecker( se, pe, mtc)); } From f1d6b6934d394d87402fca279c690d6b34197d46 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Sat, 14 Jun 2025 17:21:35 +0100 Subject: [PATCH 04/12] Annotation, Fixes to correctly register the annotated methods, type checking changes based on those annotations --- latte/pom.xml | 10 +++++++ .../src/main/java/context/ClassLevelMaps.java | 10 +++++++ .../specification/ExternalRefinementsFor.java | 21 +++++++++++++++ .../ExternalRefinementFirstPass.java | 13 ++++++++- .../java/typechecking/LatteTypeChecker.java | 27 +++++++++++++++++-- 5 files changed, 78 insertions(+), 3 deletions(-) create mode 100644 latte/src/main/java/specification/ExternalRefinementsFor.java diff --git a/latte/pom.xml b/latte/pom.xml index fc9479d..ee63bd3 100644 --- a/latte/pom.xml +++ b/latte/pom.xml @@ -145,5 +145,15 @@ + + + org.apache.maven.plugins + maven-compiler-plugin + + 11 + 11 + + + diff --git a/latte/src/main/java/context/ClassLevelMaps.java b/latte/src/main/java/context/ClassLevelMaps.java index 9da0eae..f1c4b6e 100644 --- a/latte/src/main/java/context/ClassLevelMaps.java +++ b/latte/src/main/java/context/ClassLevelMaps.java @@ -265,4 +265,14 @@ public List getExternalMethodParamPermissions( return methodMap.get(Pair.of(methodName, arity)); } + public boolean hasExternalMethodParamPermissions( + CtTypeReference clazz, String methodName, int arity) { + + Map, List> methodMap = + externalMethodParamPermissions.get(clazz); + + if (methodMap == null) return false; + + return methodMap.containsKey(Pair.of(methodName, arity)); + } } diff --git a/latte/src/main/java/specification/ExternalRefinementsFor.java b/latte/src/main/java/specification/ExternalRefinementsFor.java new file mode 100644 index 0000000..4178530 --- /dev/null +++ b/latte/src/main/java/specification/ExternalRefinementsFor.java @@ -0,0 +1,21 @@ +package specification; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Annotation to create refinements for an external library. The annotation receives the path of the + * library e.g. @ExternalRefinementsFor("java.lang.Math") + */ +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE}) +public @interface ExternalRefinementsFor { + /** + * The prefix of the external method + * + * @return + */ + public String value(); +} \ No newline at end of file diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java index e7f218b..127e755 100644 --- a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -4,7 +4,10 @@ import context.PermissionEnvironment; import context.SymbolicEnvironment; import context.UniquenessAnnotation; +import specification.ExternalRefinementsFor; import spoon.reflect.code.CtBlock; +import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtLiteral; import spoon.reflect.declaration.*; import spoon.reflect.reference.CtTypeReference; import spoon.reflect.visitor.filter.TypeFilter; @@ -39,7 +42,15 @@ public void visitCtInterface(CtInterface ctInterface) { CtTypeReference targetRef = null; for (CtAnnotation annotation : ctInterface.getAnnotations()) { if (annotation.getAnnotationType().getQualifiedName().equals("specification.ExternalRefinementsFor")) { - targetRef = (CtTypeReference) annotation.getValues().values().iterator().next(); + CtExpression expr = annotation.getValues().get("value"); + + if (expr instanceof CtLiteral && ((CtLiteral) expr).getValue() instanceof String) { + targetRef = ctInterface.getFactory().Type().createReference((String) ((CtLiteral) expr).getValue()); + } else { + logWarning("Expected a string literal in @ExternalRefinementsFor"); + return; + } + break; } } diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 63d07c6..5865a85 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -27,6 +27,7 @@ import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtParameter; +import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtFieldReference; import spoon.reflect.reference.CtLocalVariableReference; import spoon.reflect.reference.CtTypeReference; @@ -199,8 +200,30 @@ public void visitCtInvocation(CtInvocation invocation) { invocation.getArguments().size()); if (m == null){ - logInfo("Cannot find method {" + metName + "} for {} in the context"); - return; + CtExecutableReference execRef = invocation.getExecutable(); + CtTypeReference declaringType = execRef.getDeclaringType(); + + if (maps.hasExternalMethodParamPermissions(declaringType, execRef.getSimpleName(), invocation.getArguments().size())) { + List externalParams = maps.getExternalMethodParamPermissions( + declaringType, execRef.getSimpleName(), invocation.getArguments().size()); + + for (int i = 0; i < invocation.getArguments().size(); i++) { + CtExpression arg = invocation.getArguments().get(i); + + UniquenessAnnotation expectedUA = externalParams.get(i); + + SymbolicValue vv = (SymbolicValue) arg.getMetadata(EVAL_KEY); + if (vv == null) logError("Symbolic value for constructor argument not found", invocation); + + UniquenessAnnotation vvPerm = permEnv.get(vv); + + if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA)) + logError(String.format("Expected %s but got %s in the external refinement", expectedUA, vvPerm), arg); + } + } else { + logInfo("Cannot find method {" + metName + "} for {} in the context"); + return; + } } List paramSymbValues = new ArrayList<>(); From 5df33093a0f80034d988727aee32bea4ea90afdc Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Sat, 14 Jun 2025 18:01:36 +0100 Subject: [PATCH 05/12] Added simple logging for external refinements pass --- .../main/java/typechecking/ExternalRefinementFirstPass.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java index 127e755..f1378aa 100644 --- a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -26,10 +26,13 @@ public ExternalRefinementFirstPass(SymbolicEnvironment symbEnv, PermissionEnvironment permEnv, ClassLevelMaps maps) { super(symbEnv, permEnv, maps); + logInfo("[ External Refinements Pass started ]"); + enterScopes(); } @Override public void visitCtInterface(CtInterface ctInterface) { + logInfo("Visiting interface: " + ctInterface.getSimpleName(), ctInterface); // @ExternalRefinementsFor annotation check boolean hasAnnotation = ctInterface.getAnnotations().stream().anyMatch(ann -> ann.getAnnotationType().getQualifiedName().equals("specification.ExternalRefinementsFor") @@ -68,6 +71,7 @@ public void visitCtInterface(CtInterface ctInterface) { @Override public void visitCtMethod(CtMethod method) { + logInfo("Visiting method: " + method.getSimpleName(), method); CtTypeReference declaringClass = method.getDeclaringType().getReference(); // Skip if it has a body — it's not external From 5fd2584025a3cb2b045530880d8a41dac99bd672 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Sat, 14 Jun 2025 18:12:38 +0100 Subject: [PATCH 06/12] get external refine map in CLM; correction in ERFP (missing super.visit...()) --- latte/src/main/java/context/ClassLevelMaps.java | 4 ++++ .../main/java/typechecking/ExternalRefinementFirstPass.java | 3 +++ 2 files changed, 7 insertions(+) diff --git a/latte/src/main/java/context/ClassLevelMaps.java b/latte/src/main/java/context/ClassLevelMaps.java index f1c4b6e..f74e7b3 100644 --- a/latte/src/main/java/context/ClassLevelMaps.java +++ b/latte/src/main/java/context/ClassLevelMaps.java @@ -275,4 +275,8 @@ public boolean hasExternalMethodParamPermissions( return methodMap.containsKey(Pair.of(methodName, arity)); } + + public Object getExternaRefinementsMap() { + return externalMethodParamPermissions; + } } diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java index f1378aa..05b388c 100644 --- a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -67,6 +67,7 @@ public void visitCtInterface(CtInterface ctInterface) { logInfo("Processing external interface: " + ctInterface.getQualifiedName(), ctInterface); scan(ctInterface.getMethods()); } + super.visitCtInterface(ctInterface); } @Override @@ -91,5 +92,7 @@ public void visitCtMethod(CtMethod method) { maps.addExternalMethodParamPermissions(declaringClass, methodSig.getLeft(), methodSig.getRight(), paramAnnotations); logInfo("Collected annotations for method: " + methodSig + " => " + paramAnnotations, method); + super.visitCtMethod(method); } + } \ No newline at end of file From 0f87b4a597f0826cd366266b3c2b7a4574e8e4c5 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Tue, 17 Jun 2025 23:39:50 +0100 Subject: [PATCH 07/12] First Pass Check for External Libraries --- .../main/java/typechecking/LatteClassFirstPass.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/latte/src/main/java/typechecking/LatteClassFirstPass.java b/latte/src/main/java/typechecking/LatteClassFirstPass.java index 1678823..10edd3f 100644 --- a/latte/src/main/java/typechecking/LatteClassFirstPass.java +++ b/latte/src/main/java/typechecking/LatteClassFirstPass.java @@ -4,11 +4,7 @@ import context.PermissionEnvironment; import context.SymbolicEnvironment; import context.UniquenessAnnotation; -import spoon.reflect.declaration.CtClass; -import spoon.reflect.declaration.CtConstructor; -import spoon.reflect.declaration.CtElement; -import spoon.reflect.declaration.CtField; -import spoon.reflect.declaration.CtMethod; +import spoon.reflect.declaration.*; import spoon.reflect.reference.CtTypeReference; public class LatteClassFirstPass extends LatteAbstractChecker{ @@ -54,6 +50,10 @@ public void visitCtField(CtField f) { @Override public void visitCtMethod(CtMethod m) { + CtTypeReference type = ((CtType) m.getParent()).getTypeErasure(); + if(maps.hasExternalMethodParamPermissions(type, m.getSimpleName(), m.getParameters().size())) { + return; + } logInfo("Visiting method: " + m.getSimpleName(), m); maps.addMethod((CtClass) m.getParent(), m); super.visitCtMethod(m); From 8676845a3285fa71b3908384fee48ed661ca4618 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Wed, 18 Jun 2025 10:09:51 +0100 Subject: [PATCH 08/12] some changes, needing correct integration with perm and symb environments --- .../ExternalRefinementFirstPass.java | 46 +++++++++-------- .../typechecking/LatteClassFirstPass.java | 20 +++++++- .../java/typechecking/LatteTypeChecker.java | 49 ++++++++++--------- 3 files changed, 69 insertions(+), 46 deletions(-) diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java index 05b388c..c85f978 100644 --- a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -22,6 +22,8 @@ */ public class ExternalRefinementFirstPass extends LatteAbstractChecker { + private CtTypeReference currentExtRefTarget = null; + public ExternalRefinementFirstPass(SymbolicEnvironment symbEnv, PermissionEnvironment permEnv, ClassLevelMaps maps) { @@ -34,31 +36,22 @@ public ExternalRefinementFirstPass(SymbolicEnvironment symbEnv, public void visitCtInterface(CtInterface ctInterface) { logInfo("Visiting interface: " + ctInterface.getSimpleName(), ctInterface); // @ExternalRefinementsFor annotation check - boolean hasAnnotation = ctInterface.getAnnotations().stream().anyMatch(ann -> - ann.getAnnotationType().getQualifiedName().equals("specification.ExternalRefinementsFor") - ); + CtAnnotation ann = ctInterface.getAnnotation(ctInterface.getFactory().Type().createReference("specification.ExternalRefinementsFor")); - if (!hasAnnotation) { + if (ann == null) { return; } - CtTypeReference targetRef = null; - for (CtAnnotation annotation : ctInterface.getAnnotations()) { - if (annotation.getAnnotationType().getQualifiedName().equals("specification.ExternalRefinementsFor")) { - CtExpression expr = annotation.getValues().get("value"); - - if (expr instanceof CtLiteral && ((CtLiteral) expr).getValue() instanceof String) { - targetRef = ctInterface.getFactory().Type().createReference((String) ((CtLiteral) expr).getValue()); - } else { - logWarning("Expected a string literal in @ExternalRefinementsFor"); - return; - } + CtExpression expr = ann.getValues().get("value"); - break; - } + if (expr instanceof CtLiteral && ((CtLiteral) expr).getValue() instanceof String) { + currentExtRefTarget = ctInterface.getFactory().Type().createReference((String) ((CtLiteral) expr).getValue()); + } else { + logWarning("Expected a string literal in @ExternalRefinementsFor"); + return; } - if (targetRef == null) { + if (currentExtRefTarget == null) { logWarning("No target class specified in @ExternalRefinementsFor"); return; } @@ -68,14 +61,19 @@ public void visitCtInterface(CtInterface ctInterface) { scan(ctInterface.getMethods()); } super.visitCtInterface(ctInterface); + + currentExtRefTarget = null; } @Override public void visitCtMethod(CtMethod method) { logInfo("Visiting method: " + method.getSimpleName(), method); - CtTypeReference declaringClass = method.getDeclaringType().getReference(); - // Skip if it has a body — it's not external + if (currentExtRefTarget == null) { + logInfo("?????????????????????????"); + return; + } + CtBlock body = method.getBody(); if (body != null && !body.isImplicit()) return; @@ -89,7 +87,13 @@ public void visitCtMethod(CtMethod method) { Pair methodSig = Pair.of(method.getSimpleName(), parameters.size()); - maps.addExternalMethodParamPermissions(declaringClass, methodSig.getLeft(), methodSig.getRight(), paramAnnotations); + logInfo("Registering external refinements for: " + currentExtRefTarget, method); + maps.addExternalMethodParamPermissions( + currentExtRefTarget, methodSig.getLeft(), methodSig.getRight(), paramAnnotations + ); + super.visitCtMethod(method); + + logInfo("SSSSSSSSSSSS + " + currentExtRefTarget); logInfo("Collected annotations for method: " + methodSig + " => " + paramAnnotations, method); super.visitCtMethod(method); diff --git a/latte/src/main/java/typechecking/LatteClassFirstPass.java b/latte/src/main/java/typechecking/LatteClassFirstPass.java index 10edd3f..9d068e4 100644 --- a/latte/src/main/java/typechecking/LatteClassFirstPass.java +++ b/latte/src/main/java/typechecking/LatteClassFirstPass.java @@ -4,6 +4,8 @@ import context.PermissionEnvironment; import context.SymbolicEnvironment; import context.UniquenessAnnotation; +import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtLiteral; import spoon.reflect.declaration.*; import spoon.reflect.reference.CtTypeReference; @@ -51,8 +53,22 @@ public void visitCtField(CtField f) { @Override public void visitCtMethod(CtMethod m) { CtTypeReference type = ((CtType) m.getParent()).getTypeErasure(); - if(maps.hasExternalMethodParamPermissions(type, m.getSimpleName(), m.getParameters().size())) { - return; + CtType parentType = (CtType) m.getParent(); + if(parentType instanceof CtInterface){ + CtAnnotation ann = parentType.getAnnotation( + parentType.getFactory().Type().createReference("specification.ExternalRefinementsFor") + ); + if (ann != null) { + CtExpression expr = ann.getValues().get("value"); + + if (expr instanceof CtLiteral && ((CtLiteral) expr).getValue() instanceof String) { + String refinedClassName = (String) ((CtLiteral) expr).getValue(); + CtTypeReference refinedTypeRef = parentType.getFactory().Type().createReference(refinedClassName); + if(maps.hasExternalMethodParamPermissions(refinedTypeRef, m.getSimpleName(), m.getParameters().size())) + logInfo("External refinement match found for: " + m.getSimpleName() + " in refined class: " + refinedClassName); + return; + } + } } logInfo("Visiting method: " + m.getSimpleName(), m); maps.addMethod((CtClass) m.getParent(), m); diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 5865a85..3134dd4 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -199,13 +199,16 @@ public void visitCtInvocation(CtInvocation invocation) { CtMethod m = maps.getCtMethod(klass, metName, invocation.getArguments().size()); + List paramSymbValues = new ArrayList<>(); + if (m == null){ CtExecutableReference execRef = invocation.getExecutable(); - CtTypeReference declaringType = execRef.getDeclaringType(); - if (maps.hasExternalMethodParamPermissions(declaringType, execRef.getSimpleName(), invocation.getArguments().size())) { + logInfo("BBBBBBBB + " + e + " + " + execRef.getSimpleName() + " + " + invocation.getArguments().size()); + + if (maps.hasExternalMethodParamPermissions(e, execRef.getSimpleName(), invocation.getArguments().size())) { List externalParams = maps.getExternalMethodParamPermissions( - declaringType, execRef.getSimpleName(), invocation.getArguments().size()); + e, execRef.getSimpleName(), invocation.getArguments().size()); for (int i = 0; i < invocation.getArguments().size(); i++) { CtExpression arg = invocation.getArguments().get(i); @@ -219,32 +222,32 @@ public void visitCtInvocation(CtInvocation invocation) { if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA)) logError(String.format("Expected %s but got %s in the external refinement", expectedUA, vvPerm), arg); + + paramSymbValues.add(vv); } } else { logInfo("Cannot find method {" + metName + "} for {} in the context"); return; } + } else { + for (int i = 0; i < paramSize; i++){ + CtExpression arg = invocation.getArguments().get(i); + // Γ; Δ; Σ ⊢ 𝑒1, ... , 𝑒𝑛 ⇓ 𝜈1, ... , 𝜈𝑛 ⊣ Γ′; Δ′; Σ′ + SymbolicValue vv = (SymbolicValue) arg.getMetadata(EVAL_KEY); + if (vv == null) logError("Symbolic value for constructor argument not found", invocation); + + CtParameter p = m.getParameters().get(i); + UniquenessAnnotation expectedUA = new UniquenessAnnotation(p); + UniquenessAnnotation vvPerm = permEnv.get(vv); + + logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA)); + // Σ′ ⊢ 𝑒1, ... , 𝑒𝑛 : 𝛼1, ... , 𝛼𝑛 ⊣ Σ′′ + if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA)) + logError(String.format("Expected %s but got %s", expectedUA, vvPerm), arg); + + paramSymbValues.add(vv); + } } - List paramSymbValues = new ArrayList<>(); - - for (int i = 0; i < paramSize; i++){ - CtExpression arg = invocation.getArguments().get(i); - // Γ; Δ; Σ ⊢ 𝑒1, ... , 𝑒𝑛 ⇓ 𝜈1, ... , 𝜈𝑛 ⊣ Γ′; Δ′; Σ′ - SymbolicValue vv = (SymbolicValue) arg.getMetadata(EVAL_KEY); - if (vv == null) logError("Symbolic value for constructor argument not found", invocation); - - CtParameter p = m.getParameters().get(i); - UniquenessAnnotation expectedUA = new UniquenessAnnotation(p); - UniquenessAnnotation vvPerm = permEnv.get(vv); - - logInfo(String.format("Checking constructor argument %s:%s, %s <= %s", p.getSimpleName(), vv, vvPerm, expectedUA)); - // Σ′ ⊢ 𝑒1, ... , 𝑒𝑛 : 𝛼1, ... , 𝛼𝑛 ⊣ Σ′′ - if (!permEnv.usePermissionAs(vv, vvPerm, expectedUA)) - logError(String.format("Expected %s but got %s", expectedUA, vvPerm), arg); - - paramSymbValues.add(vv); - } - // distinct(Δ′, {𝜈𝑖 : borrowed ≤ 𝛼𝑖 }) // distinct(Δ, 𝑆) ⇐⇒ ∀𝜈, 𝜈′ ∈ 𝑆 : Δ ⊢ 𝜈 ⇝ 𝜈′ =⇒ 𝜈 = 𝜈′ List check_distinct = new ArrayList<>(); From 309cad3ee71c7db5f82954396c9ce85e9c667a18 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Mon, 23 Jun 2025 14:14:54 +0100 Subject: [PATCH 09/12] added some fixes, it now works properly --- .../src/main/java/context/ClassLevelMaps.java | 34 ++++++++++++++++--- .../ExternalRefinementFirstPass.java | 2 ++ .../java/typechecking/LatteTypeChecker.java | 5 +++ 3 files changed, 36 insertions(+), 5 deletions(-) diff --git a/latte/src/main/java/context/ClassLevelMaps.java b/latte/src/main/java/context/ClassLevelMaps.java index f74e7b3..4d00efa 100644 --- a/latte/src/main/java/context/ClassLevelMaps.java +++ b/latte/src/main/java/context/ClassLevelMaps.java @@ -7,19 +7,19 @@ import org.apache.commons.lang3.tuple.Pair; -import spoon.reflect.declaration.CtClass; -import spoon.reflect.declaration.CtConstructor; -import spoon.reflect.declaration.CtField; -import spoon.reflect.declaration.CtMethod; +import spoon.reflect.declaration.*; import spoon.reflect.reference.CtTypeReference; -public class ClassLevelMaps { +public class +ClassLevelMaps { static ClassLevelMaps instance; Map, CtClass> typeClassMap; Map, Map>> classFields; Map, Map>> classConstructors; Map, Map, CtMethod>> classMethods; + + Map, Map, CtMethod>> externalMethods; Map, Map, List>> externalMethodParamPermissions; @@ -29,6 +29,8 @@ public ClassLevelMaps() { classFields = new HashMap, Map>>(); classConstructors = new HashMap<>(); classMethods = new HashMap<>(); + + externalMethods = new HashMap<>(); externalMethodParamPermissions = new HashMap<>(); } @@ -243,6 +245,18 @@ public static void joinElim( } } + public void addExternalMethod(CtTypeReference klass, CtMethod method) { + Pair mPair = Pair.of(method.getSimpleName(), method.getParameters().size()); + if (externalMethods.containsKey(klass)){ + Map, CtMethod> m = externalMethods.get(klass); + m.put(mPair, method); + } else { + Map, CtMethod> m = new HashMap, CtMethod>(); + m.put(mPair, method); + externalMethods.put(klass, m); + } + } + public void addExternalMethodParamPermissions( CtTypeReference typeRef, String methodName, @@ -275,6 +289,16 @@ public boolean hasExternalMethodParamPermissions( return methodMap.containsKey(Pair.of(methodName, arity)); } + public CtMethod getExternalCtMethod(CtTypeReference klass, String methodName, int numParams) { + Pair mPair = Pair.of(methodName, numParams); + if (externalMethods.containsKey(klass)){ + Map, CtMethod> m = externalMethods.get(klass); + if (m.containsKey(mPair)){ + return m.get(mPair); + } + } + return null; + } public Object getExternaRefinementsMap() { return externalMethodParamPermissions; diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java index c85f978..53bfd5b 100644 --- a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -88,6 +88,8 @@ public void visitCtMethod(CtMethod method) { Pair methodSig = Pair.of(method.getSimpleName(), parameters.size()); logInfo("Registering external refinements for: " + currentExtRefTarget, method); + + maps.addExternalMethod(currentExtRefTarget, method); maps.addExternalMethodParamPermissions( currentExtRefTarget, methodSig.getLeft(), methodSig.getRight(), paramAnnotations ); diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 3134dd4..9b6812a 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -201,6 +201,8 @@ public void visitCtInvocation(CtInvocation invocation) { List paramSymbValues = new ArrayList<>(); + logInfo("CCCCCCCC000000000 : " + m); + if (m == null){ CtExecutableReference execRef = invocation.getExecutable(); @@ -225,6 +227,8 @@ public void visitCtInvocation(CtInvocation invocation) { paramSymbValues.add(vv); } + m = maps.getExternalCtMethod(e, metName, invocation.getArguments().size()); + logInfo("CCCCCC222222 : " + m); } else { logInfo("Cannot find method {" + metName + "} for {} in the context"); return; @@ -248,6 +252,7 @@ public void visitCtInvocation(CtInvocation invocation) { paramSymbValues.add(vv); } } + logInfo("CCCCCCCC111111 : " + m); // distinct(Δ′, {𝜈𝑖 : borrowed ≤ 𝛼𝑖 }) // distinct(Δ, 𝑆) ⇐⇒ ∀𝜈, 𝜈′ ∈ 𝑆 : Δ ⊢ 𝜈 ⇝ 𝜈′ =⇒ 𝜈 = 𝜈′ List check_distinct = new ArrayList<>(); From 60c6bebf4be91372f5e259856d8c1c5a6beae6b5 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Mon, 23 Jun 2025 15:11:53 +0100 Subject: [PATCH 10/12] Removed debugging logs --- .../main/java/typechecking/ExternalRefinementFirstPass.java | 3 --- latte/src/main/java/typechecking/LatteTypeChecker.java | 6 ------ 2 files changed, 9 deletions(-) diff --git a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java index 53bfd5b..7c20389 100644 --- a/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java +++ b/latte/src/main/java/typechecking/ExternalRefinementFirstPass.java @@ -70,7 +70,6 @@ public void visitCtMethod(CtMethod method) { logInfo("Visiting method: " + method.getSimpleName(), method); if (currentExtRefTarget == null) { - logInfo("?????????????????????????"); return; } @@ -95,8 +94,6 @@ public void visitCtMethod(CtMethod method) { ); super.visitCtMethod(method); - logInfo("SSSSSSSSSSSS + " + currentExtRefTarget); - logInfo("Collected annotations for method: " + methodSig + " => " + paramAnnotations, method); super.visitCtMethod(method); } diff --git a/latte/src/main/java/typechecking/LatteTypeChecker.java b/latte/src/main/java/typechecking/LatteTypeChecker.java index 9b6812a..dd2da2d 100644 --- a/latte/src/main/java/typechecking/LatteTypeChecker.java +++ b/latte/src/main/java/typechecking/LatteTypeChecker.java @@ -201,13 +201,9 @@ public void visitCtInvocation(CtInvocation invocation) { List paramSymbValues = new ArrayList<>(); - logInfo("CCCCCCCC000000000 : " + m); - if (m == null){ CtExecutableReference execRef = invocation.getExecutable(); - logInfo("BBBBBBBB + " + e + " + " + execRef.getSimpleName() + " + " + invocation.getArguments().size()); - if (maps.hasExternalMethodParamPermissions(e, execRef.getSimpleName(), invocation.getArguments().size())) { List externalParams = maps.getExternalMethodParamPermissions( e, execRef.getSimpleName(), invocation.getArguments().size()); @@ -228,7 +224,6 @@ public void visitCtInvocation(CtInvocation invocation) { paramSymbValues.add(vv); } m = maps.getExternalCtMethod(e, metName, invocation.getArguments().size()); - logInfo("CCCCCC222222 : " + m); } else { logInfo("Cannot find method {" + metName + "} for {} in the context"); return; @@ -252,7 +247,6 @@ public void visitCtInvocation(CtInvocation invocation) { paramSymbValues.add(vv); } } - logInfo("CCCCCCCC111111 : " + m); // distinct(Δ′, {𝜈𝑖 : borrowed ≤ 𝛼𝑖 }) // distinct(Δ, 𝑆) ⇐⇒ ∀𝜈, 𝜈′ ∈ 𝑆 : Δ ⊢ 𝜈 ⇝ 𝜈′ =⇒ 𝜈 = 𝜈′ List check_distinct = new ArrayList<>(); From 6ddeb9abdae4eac009df5d66b1e3a52aefc44d7d Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Tue, 24 Jun 2025 15:50:55 +0100 Subject: [PATCH 11/12] small bug fix --- latte/src/main/java/typechecking/LatteClassFirstPass.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/latte/src/main/java/typechecking/LatteClassFirstPass.java b/latte/src/main/java/typechecking/LatteClassFirstPass.java index 9d068e4..6683c73 100644 --- a/latte/src/main/java/typechecking/LatteClassFirstPass.java +++ b/latte/src/main/java/typechecking/LatteClassFirstPass.java @@ -66,9 +66,9 @@ public void visitCtMethod(CtMethod m) { CtTypeReference refinedTypeRef = parentType.getFactory().Type().createReference(refinedClassName); if(maps.hasExternalMethodParamPermissions(refinedTypeRef, m.getSimpleName(), m.getParameters().size())) logInfo("External refinement match found for: " + m.getSimpleName() + " in refined class: " + refinedClassName); - return; } } + return; } logInfo("Visiting method: " + m.getSimpleName(), m); maps.addMethod((CtClass) m.getParent(), m); From 611660a9076197a33805e9c546e0d0d905c31041 Mon Sep 17 00:00:00 2001 From: Antonio Almeida Date: Tue, 24 Jun 2025 15:54:36 +0100 Subject: [PATCH 12/12] Added tests, one failing and one correct --- .../test/examples/LinkedListRefinement.java | 27 +++++++++++++++++++ .../LinkedListRefinementIncorrect.java | 24 +++++++++++++++++ latte/src/test/java/AppTest.java | 6 +++-- 3 files changed, 55 insertions(+), 2 deletions(-) create mode 100644 latte/src/test/examples/LinkedListRefinement.java create mode 100644 latte/src/test/examples/LinkedListRefinementIncorrect.java diff --git a/latte/src/test/examples/LinkedListRefinement.java b/latte/src/test/examples/LinkedListRefinement.java new file mode 100644 index 0000000..052265a --- /dev/null +++ b/latte/src/test/examples/LinkedListRefinement.java @@ -0,0 +1,27 @@ +import specification.*; +import java.util.LinkedList; + +public class LinkedListRefinement { + @Unique Object o1; + + public Object test(Object obj, Object obj2, @Free Object temp) { + LinkedList list = new LinkedList<>(); + + list.add(obj); + list.add(obj); + list.add(1, obj2); + + list.remove(temp); + } +} + +@ExternalRefinementsFor("java.util.LinkedList") +interface LinkedListRefinements2 { + + public void add(@Shared T t); + + public void add(int n, @Shared T t); + + public void remove(@Free T t); + +} \ No newline at end of file diff --git a/latte/src/test/examples/LinkedListRefinementIncorrect.java b/latte/src/test/examples/LinkedListRefinementIncorrect.java new file mode 100644 index 0000000..164a731 --- /dev/null +++ b/latte/src/test/examples/LinkedListRefinementIncorrect.java @@ -0,0 +1,24 @@ +import specification.*; +import java.util.LinkedList; + +public class LinkedListRefinementIncorrect { + @Unique Object o1; + + public Object test(@Free Object obj) { + Object o2 = o1; + LinkedList list = new LinkedList<>(); + + list.add(obj); + list.add(o2); + } +} + +@ExternalRefinementsFor("java.util.LinkedList") +interface LinkedListRefinements { + + public void add(@Free T t); + + public void add(int n, T t); + + public void remove(@Free T t); +} \ No newline at end of file diff --git a/latte/src/test/java/AppTest.java b/latte/src/test/java/AppTest.java index 8bd0f59..b692f00 100644 --- a/latte/src/test/java/AppTest.java +++ b/latte/src/test/java/AppTest.java @@ -40,7 +40,8 @@ private static Stream provideCorrectTestCases() { Arguments.of("src/test/examples/searching_state_space/TimerTaskCannotReschedule.java"), Arguments.of("src/test/examples/searching_state_space/ResultSetNoNext.java"), Arguments.of("src/test/examples/searching_state_space/ResultSetForwardOnly.java"), - Arguments.of("src/test/examples/stack_overflow/MediaRecord.java") + Arguments.of("src/test/examples/stack_overflow/MediaRecord.java"), + Arguments.of("src/test/examples/LinkedListRefinement.java") ); } @@ -60,7 +61,8 @@ private static Stream provideIncorrectTestCases() { Arguments.of("src/test/examples/SmallestIncorrectExample.java", "UNIQUE but got BORROWED"), Arguments.of("src/test/examples/MyStackFieldAssignMethod.java", "UNIQUE but got SHARED"), Arguments.of("src/test/examples/FieldAccessNoThis.java", "UNIQUE but got SHARED"), - Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE") + Arguments.of("src/test/examples/FieldAccessRightNoThis.java", "FREE but got UNIQUE"), + Arguments.of("src/test/examples/LinkedListRefinementIncorrect.java", "FREE but got UNIQUE") ); }