Refined External Libraries support

latte/pom.xml

@@ -96,6 +96,12 @@
       <version>${version.spoon}</version>
     </dependency>
 
+    <dependency>
+      <groupId>org.apache.commons</groupId>
+      <artifactId>commons-lang3</artifactId>
+      <version>3.12.0</version>
+    </dependency>
+
   </dependencies>
 
   <build>
@@ -139,5 +145,15 @@
         </plugin>
       </plugins>
     </pluginManagement>
+      <plugins>
+          <plugin>
+              <groupId>org.apache.maven.plugins</groupId>
+              <artifactId>maven-compiler-plugin</artifactId>
+              <configuration>
+                  <source>11</source>
+                  <target>11</target>
+              </configuration>
+          </plugin>
+      </plugins>
   </build>
 </project>

latte/src/main/java/context/ClassLevelMaps.java

@@ -7,19 +7,20 @@
 
 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<CtTypeReference<?>, CtClass<?>> typeClassMap;
     Map<CtClass<?>, Map<String, CtField<?>>> classFields;
     Map<CtClass<?>, Map<Integer, CtConstructor<?>>> classConstructors;
     Map<CtClass<?>, Map<Pair<String, Integer>, CtMethod<?>>> classMethods;
+
+    Map<CtTypeReference<?>, Map<Pair<String, Integer>, CtMethod<?>>> externalMethods;
+    Map<CtTypeReference<?>, Map<Pair<String, Integer>, List<UniquenessAnnotation>>> externalMethodParamPermissions;
 
 
 
@@ -28,6 +29,9 @@ public ClassLevelMaps() {
         classFields = new HashMap<CtClass<?>, Map<String, CtField<?>>>();
         classConstructors = new HashMap<>();
         classMethods = new HashMap<>();
+
+        externalMethods = new HashMap<>();
+        externalMethodParamPermissions = new HashMap<>();
     }
 
     public CtClass<?> getClassFrom(CtTypeReference<?> type) {
@@ -241,6 +245,62 @@ public static void joinElim(
         }
 	}
 
+    public void addExternalMethod(CtTypeReference<?> klass, CtMethod<?> method) {
+        Pair<String, Integer> mPair = Pair.of(method.getSimpleName(), method.getParameters().size());
+        if (externalMethods.containsKey(klass)){
+            Map<Pair<String, Integer>, CtMethod<?>> m = externalMethods.get(klass);
+            m.put(mPair, method);
+        } else {
+            Map<Pair<String, Integer>, CtMethod<?>> m = new HashMap<Pair<String, Integer>, CtMethod<?>>();
+            m.put(mPair, method);
+            externalMethods.put(klass, m);
+        }
+    }
+
+    public void addExternalMethodParamPermissions(
+            CtTypeReference<?> typeRef,
+            String methodName,
+            int numParams,
+            List<UniquenessAnnotation> paramAnnotations
+    ) {
+        if (externalMethodParamPermissions == null)
+            externalMethodParamPermissions = new HashMap<>();
+
+        Pair<String, Integer> methodSig = Pair.of(methodName, numParams);
+        externalMethodParamPermissions
+                .computeIfAbsent(typeRef, k -> new HashMap<>())
+                .put(methodSig, paramAnnotations);
+    }
+
+    public List<UniquenessAnnotation> getExternalMethodParamPermissions(
+            CtTypeReference<?> clazz, String methodName, int arity) {
+        Map<Pair<String, Integer>, List<UniquenessAnnotation>> methodMap = externalMethodParamPermissions.get(clazz);
+        if (methodMap == null) return null;
+        return methodMap.get(Pair.of(methodName, arity));
+    }
 
+    public boolean hasExternalMethodParamPermissions(
+            CtTypeReference<?> clazz, String methodName, int arity) {
 
+        Map<Pair<String, Integer>, List<UniquenessAnnotation>> methodMap =
+                externalMethodParamPermissions.get(clazz);
+
+        if (methodMap == null) return false;
+
+        return methodMap.containsKey(Pair.of(methodName, arity));
+    }
+    public CtMethod<?> getExternalCtMethod(CtTypeReference<?> klass, String methodName, int numParams) {
+        Pair<String, Integer> mPair = Pair.of(methodName, numParams);
+        if (externalMethods.containsKey(klass)){
+            Map<Pair<String, Integer>, CtMethod<?>> m = externalMethods.get(klass);
+            if (m.containsKey(mPair)){
+                return m.get(mPair);
+            }
+        }
+        return null;
+    }
+
+    public Object getExternaRefinementsMap() {
+        return externalMethodParamPermissions;
+    }
 }

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();
+}

latte/src/main/java/typechecking/ExternalRefinementFirstPass.java

@@ -0,0 +1,101 @@
+package typechecking;
+
+import context.ClassLevelMaps;
+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;
+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 {
+
+    private CtTypeReference<?> currentExtRefTarget = null;
+
+    public ExternalRefinementFirstPass(SymbolicEnvironment symbEnv,
+                                       PermissionEnvironment permEnv,
+                                       ClassLevelMaps maps) {
+        super(symbEnv, permEnv, maps);
+        logInfo("[ External Refinements Pass started ]");
+        enterScopes();
+    }
+
+    @Override
+    public <T> void visitCtInterface(CtInterface<T> ctInterface) {
+        logInfo("Visiting interface: " + ctInterface.getSimpleName(), ctInterface);
+        // @ExternalRefinementsFor annotation check
+        CtAnnotation<?> ann = ctInterface.getAnnotation(ctInterface.getFactory().Type().createReference("specification.ExternalRefinementsFor"));
+
+        if (ann == null) {
+            return;
+        }
+
+        CtExpression<?> expr = ann.getValues().get("value");
+
+        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 (currentExtRefTarget == null) {
+            logWarning("No target class specified in @ExternalRefinementsFor");
+            return;
+        }
+
+        if (ctInterface.isPublic()) {
+            logInfo("Processing external interface: " + ctInterface.getQualifiedName(), ctInterface);
+            scan(ctInterface.getMethods());
+        }
+        super.visitCtInterface(ctInterface);
+
+        currentExtRefTarget = null;
+    }
+
+    @Override
+    public <T> void visitCtMethod(CtMethod<T> method) {
+        logInfo("Visiting method: " + method.getSimpleName(), method);
+
+        if (currentExtRefTarget == null) {
+            return;
+        }
+
+        CtBlock<?> body = method.getBody();
+        if (body != null && !body.isImplicit()) return;
+
+        List<CtParameter<?>> parameters = method.getParameters();
+        List<UniquenessAnnotation> paramAnnotations = new ArrayList<>();
+
+        for (CtParameter<?> param : parameters) {
+            UniquenessAnnotation ua = new UniquenessAnnotation(param);
+            paramAnnotations.add(ua);
+        }
+
+        Pair<String, Integer> 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
+        );
+        super.visitCtMethod(method);
+
+        logInfo("Collected annotations for method: " + methodSig + " => " + paramAnnotations, method);
+        super.visitCtMethod(method);
+    }
+
+}

latte/src/main/java/typechecking/LatteClassFirstPass.java

@@ -4,11 +4,9 @@
 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.code.CtExpression;
+import spoon.reflect.code.CtLiteral;
+import spoon.reflect.declaration.*;
 import spoon.reflect.reference.CtTypeReference;
 
 public class LatteClassFirstPass extends LatteAbstractChecker{
@@ -54,6 +52,24 @@ public <T> void visitCtField(CtField<T> f) {
 
 	@Override
 	public <T> void visitCtMethod(CtMethod<T> m) {
+		CtTypeReference<?> type = ((CtType<?>) m.getParent()).getTypeErasure();
+		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);
 		super.visitCtMethod(m);

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));
         }

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;
@@ -198,30 +199,54 @@ public <T> void visitCtInvocation(CtInvocation<T> invocation) {
 		CtMethod<?> m = maps.getCtMethod(klass, metName, 
 			invocation.getArguments().size());
 
-		if (m == null){
-			logInfo("Cannot find method {" + metName + "} for {} in the context");
-			return;
-		}
 		List<SymbolicValue> 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);
+		if (m == null){
+			CtExecutableReference<?> execRef = invocation.getExecutable();
 
-			paramSymbValues.add(vv);
+			if (maps.hasExternalMethodParamPermissions(e, execRef.getSimpleName(), invocation.getArguments().size())) {
+				List<UniquenessAnnotation> externalParams = maps.getExternalMethodParamPermissions(
+						e, 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);
+
+					paramSymbValues.add(vv);
+				}
+				m = maps.getExternalCtMethod(e, metName, invocation.getArguments().size());
+			} 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);
+			}
 		}
-
 		// distinct(Δ′, {𝜈𝑖 : borrowed ≤ 𝛼𝑖 })
 		// distinct(Δ, 𝑆) ⇐⇒ ∀𝜈, 𝜈′ ∈ 𝑆 : Δ ⊢ 𝜈 ⇝ 𝜈′ =⇒ 𝜈 = 𝜈′
 		List<SymbolicValue> check_distinct = new ArrayList<>();