Effect members and annotations for imported Java code

.gitignore

@@ -2,7 +2,6 @@
 .DS_STORE
 tags
 .idea
-tools/wyvern-tools.iml
 *.class
 *.pyc
 *.wyv.py

examples/ffi/callImpure.wyv

@@ -0,0 +1,10 @@
+require java
+require stdout
+
+import java:wyvern.tools.tests.examples.support.CallFromJava.singleton
+
+// singleton.impureMethod is annotated with @Effect("stdout.print")
+def doImpureThing(): {stdout.print} Unit
+  singleton.impureMethod()
+
+doImpureThing()

examples/ffi/callJava.wyv

@@ -0,0 +1,12 @@
+require java
+require stdout
+
+// We import a static object instead of a class. The type is converted to
+// a Wyvern structural type through reflection.
+import java:wyvern.tools.tests.examples.support.CallFromJava.singleton
+
+// This FFI method has no effects because it is annotated in Java with @Pure from the checker framework.
+def getString(): {} String
+  singleton.pureMethod()
+
+stdout.print(getString())

examples/ffi/callWyvernThunk.wyv

@@ -0,0 +1,6 @@
+require java
+require stdout
+
+import java:wyvern.tools.tests.examples.support.CallFromJava.singleton
+
+singleton.callWyvernThunk(() => stdout.print("called from Java!"))

examples/ffi/effectMembersInModuleDef.wyv

@@ -0,0 +1,8 @@
+module def effectMembersInModuleDef(java: Java, stdout: Stdout): {}
+
+// this demonstrates using the java and stdout capabilities from within a `module def`
+
+import java:wyvern.tools.tests.examples.support.CallFromJava.singleton
+
+def doImpureThing(): {stdout.print} Unit
+  singleton.impureMethod()

examples/ffi/objectFromJava.wyv

@@ -0,0 +1,11 @@
+require java
+require stdout
+
+import java:wyvern.tools.tests.examples.support.CallFromJava.singleton
+
+val obj = singleton.getObject()
+
+def objectPrint(): {obj.doThingEffect} Unit
+  obj.doThing()
+
+objectPrint()

stdlib/platform/java/stdout.wyv

@@ -30,7 +30,7 @@ def printFloat(f:Float): {print} Unit
 //    val s : String = str
 //    stdio.print(s)
 
-def printRational(r:Rational): Unit
+def printRational(r:Rational): {print} Unit
   stdio.printRational(r)
 
 def println(): {print} Unit

tools/.classpath

@@ -10,5 +10,6 @@
 	<classpathentry kind="lib" path="lib/hamcrest-core-1.3.jar"/>
 	<classpathentry kind="lib" path="lib/javatuples-1.2.jar"/>
 	<classpathentry kind="lib" path="lib/protobuf-java-3.5.1.jar"/>
+	<classpathentry kind="lib" path="lib/checker-qual-3.7.1.jar"/>
 	<classpathentry kind="output" path="bin"/>
 </classpath>

tools/build.xml

@@ -13,6 +13,7 @@
         <pathelement location="lib/checkstyle-8.7-all.jar" />
         <pathelement location="lib/jacocoant.jar" />
         <pathelement location="lib/protobuf-java-3.5.1.jar" />
+        <pathelement location="lib/checker-qual-3.7.1.jar" />
     </path>
 
     <taskdef name="copper" classname="edu.umn.cs.melt.copper.ant.CopperAntTask" classpath="lib/CopperCompiler.jar"/>

tools/src/wyvern/stdlib/Globals.java

@@ -298,6 +298,7 @@ public static ValueType getSystemType() {
         declTypes.add(new ValDeclType("unit", Util.unitType()));
         //declTypes.add(new EffectDeclType("ffiEffect", null, null));
         declTypes.add(new EffectDeclType("FFI", null, null));
+        declTypes.add(new EffectDeclType("FFI2", null, null));
         declTypes.add(new EffectDeclType("EffectNotInScope", null, null));
         ValueType systemType = new StructuralType(new BindingSite("this"), declTypes);
         return systemType;

tools/src/wyvern/stdlib/support/Effect.java

@@ -0,0 +1,12 @@
+package wyvern.stdlib.support;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Target({ElementType.METHOD,ElementType.TYPE})
+@Retention(RetentionPolicy.RUNTIME)
+public @interface Effect {
+    String[] value();
+}

tools/src/wyvern/stdlib/support/Pure.java

@@ -0,0 +1,11 @@
+package wyvern.stdlib.support;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Target({ElementType.METHOD,ElementType.TYPE})
+@Retention(RetentionPolicy.RUNTIME)
+public @interface Pure {
+}

tools/src/wyvern/target/corewyvernIL/expression/MethodCall.java

@@ -38,6 +38,8 @@
 import wyvern.tools.errors.FileLocation;
 import wyvern.tools.errors.HasLocation;
 import wyvern.tools.errors.ToolError;
+import wyvern.tools.interop.JObject;
+import wyvern.tools.interop.JavaValue;
 import wyvern.tools.typedAST.core.declarations.DefDeclaration;
 
 public class MethodCall extends Expression {
@@ -135,6 +137,7 @@ private ValueType getReceiverType(TypeContext ctx) {
 
     @Override
     public ValueType typeCheck(TypeContext ctx, EffectAccumulator effectAccumulator) {
+
         // If calling on a dynamic receiver, it types to Dyn (provided the args typecheck)
         if (Util.isDynamicType(getReceiverType(ctx))) {
             for (IExpr arg : args) {
@@ -429,8 +432,10 @@ public static MatchResult matches(TypeContext newCtx, ValueType receiver, DeclTy
      */
     public DefDeclType typeMethodDeclaration(TypeContext ctx, EffectAccumulator effectAccumulator) {
         boolean isTarget = false;
+
         // Typecheck receiver.
         ValueType receiver = getReceiverType(ctx);
+
         StructuralType receiverType = receiver.getStructuralType(ctx);
         // Sanity check: make sure it has declarations.
         List<DeclType> declarationTypes = receiverType.findDecls(methodName, ctx);

tools/src/wyvern/tools/errors/ErrorMessage.java

@@ -49,7 +49,7 @@ public enum ErrorMessage {
     QUALIFIED_TYPES_ONLY_FIELDS("Qualified types can only include val fields", 0),
     ILLEGAL_JUXTAPOSITION("Juxtaposed an additional argument to something that was not an application", 0),
     ILLEGAL_BINARY_JUXTAPOSITION("Cannot juxtapose an additional argument to a binary operation", 0),
-    VAL_NEEDS_TYPE("val declaration %ARG is inside a new statement and thus needs a type annotation", 1),
+    VAL_NEEDS_TYPE("val declaration %ARG is inside a \"new\" statement and thus needs a type annotation", 1),
     EFFECT_ANNOTATION_SEPARATION("Effect-annotated module depends on an effect-unannotated module", 0),
     EFFECT_ANNOTATION_DEF("Module definition has incorrect annotation", 0),
     PURE_MODULE_ANNOTATION("Pure module should always have empty effect annotation", 0),
@@ -112,8 +112,10 @@ public enum ErrorMessage {
     SCRIPT_REQUIRED_MODULE_ONLY_JAVA("A module required by a top-level script must have exactly one argument, a platform such as java", 0),
     NOT_AN_FFI("Expected an FFI object as the schema in an import URI", 0),
     SCHEME_NOT_RECOGNIZED("import scheme %ARG not recognized; did you forget to \"require java\"?", 1),
-    UNSAFE_JAVA_IMPORT("To import the %ARG object %ARG, make sure you \"require %ARG\" "
-            + "(security experts only: if this object is harmless, you can add it to the built-in whitelist (see Globals.java)", 3),
+    UNSAFE_JAVA_IMPORT("Importing java object %ARG is unsafe. Either annotate the class definition with @Pure, or use \"require java\" to include the \"java\" capability. "
+            + "(or, security experts only: if this object is harmless, you can add it to the built-in whitelist (see Globals.java)).", 1),
+    UNSAFE_JAVASCRIPT_IMPORT("To import the %ARG object %ARG, make sure you \"require %ARG\" "
+            + "(security experts only: if this object is harmless, you can add it to the built-in whitelist (see Globals.java)).", 3),
     ILLEGAL_ESCAPE_SEQUENCE("Illegal escape sequence", 0),
     UNCLOSED_STRING_LITERAL("Unclosed string literal", 0),
     NO_ABSTRACT_TYPES_IN_OBJECTS("Abstract types may not be declared in objects or modules, only in type definitions", 0),

tools/src/wyvern/tools/interop/FFI.java

@@ -1,10 +1,16 @@
 package wyvern.tools.interop;
 
+import java.lang.reflect.Method;
 import java.net.URI;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
 import java.util.HashSet;
+import java.util.List;
 import java.util.Set;
 
 import wyvern.stdlib.Globals;
+import wyvern.stdlib.support.Effect;
 import wyvern.stdlib.support.backend.BytecodeOuterClass;
 import wyvern.target.corewyvernIL.VarBinding;
 import wyvern.target.corewyvernIL.astvisitor.ASTVisitor;
@@ -13,9 +19,12 @@
 import wyvern.target.corewyvernIL.expression.Expression;
 import wyvern.target.corewyvernIL.expression.Tag;
 import wyvern.target.corewyvernIL.expression.Variable;
+import wyvern.target.corewyvernIL.modules.Module;
+import wyvern.target.corewyvernIL.modules.TypedModuleSpec;
 import wyvern.target.corewyvernIL.support.EvalContext;
 import wyvern.target.corewyvernIL.support.GenContext;
 import wyvern.target.corewyvernIL.support.InterpreterState;
+import wyvern.target.corewyvernIL.support.ModuleResolver;
 import wyvern.target.corewyvernIL.support.TypeContext;
 import wyvern.target.corewyvernIL.type.DynamicType;
 import wyvern.target.corewyvernIL.type.NominalType;
@@ -73,44 +82,68 @@ public Tag getTag(EvalContext ctx) {
         return nt.getTag(ctx);
     }
 
-    public static Pair<VarBinding, GenContext> importURI(URI uri, GenContext ctx, HasLocation errorLocation) {
+    public static Pair<Pair<VarBinding, GenContext>, List<TypedModuleSpec>> importURI(URI uri, GenContext ctx, HasLocation errorLocation) {
         final String scheme = uri.getScheme();
+        List<TypedModuleSpec> noDependencies = Collections.emptyList();
         if (scheme.equals("java")) {
             return doJavaImport(uri, ctx, errorLocation);
         } else if (scheme.equals("python")) {
-            return doPythonImport(uri, ctx);
+            return new Pair<>(doPythonImport(uri, ctx), noDependencies);
         } else if (scheme.equals("javascript")) {
-            return doJavaScriptImport(uri, ctx, errorLocation);
+            return new Pair<>(doJavaScriptImport(uri, ctx, errorLocation), noDependencies);
         } else {
             // TODO: support non-Java imports too - probably separated out into various FFI subclasses
             System.err.println("importURI called with uri=" + uri + ", ctx=" + ctx);
             throw new RuntimeException("only Java imports should get to this code path; others not implemented yet");
         }
     }
 
-    public static Pair<VarBinding, GenContext> doJavaImport(URI uri, GenContext ctx, HasLocation errorLocation) {
+    public static Pair<Pair<VarBinding, GenContext>, List<TypedModuleSpec>> doJavaImport(URI uri, GenContext ctx, HasLocation errorLocation) {
         String importName = uri.getSchemeSpecificPart();
         if (importName.contains(".")) {
             importName = importName.substring(importName.lastIndexOf(".") + 1);
         }
         String importPath = uri.getRawSchemeSpecificPart();
         FObject obj = null;
         try {
-            obj = wyvern.tools.interop.Default.importer().find(importPath, errorLocation);
+            obj = new JavaImporter(ctx).find(importPath, errorLocation);
         } catch (ReflectiveOperationException e1) {
             ToolError.reportError(ErrorMessage.IMPORT_NOT_FOUND, errorLocation, uri.toString());
         }
 
         ctx = GenUtil.ensureJavaTypesPresent(ctx);
         ctx = ImportDeclaration.extendWithImportCtx(obj, ctx);
 
+        List<TypedModuleSpec> dependencies = getJavaDependencies(obj.getJavaClass());
+
         assert (uri.toString().substring(0, 5).equals("java:"));
         boolean safe = Globals.checkSafeJavaImport(uri.toString().substring(5));
         ValueType type = GenUtil.javaClassToWyvernType(obj.getJavaClass(), ctx, safe);
 
         Expression importExp = new FFIImport(new NominalType("system", "java"), importPath, type);
         ctx = ctx.extend(importName, new Variable(importName), type);
-        return new Pair<VarBinding, GenContext>(new VarBinding(importName, type, importExp), ctx);
+        return new Pair<>(new Pair<>(new VarBinding(importName, type, importExp), ctx), dependencies);
+    }
+
+    public static List<TypedModuleSpec> getJavaDependencies(Class<?> javaClass) {
+        Set<String> modulePaths = new HashSet<>();
+        for (Method m : javaClass.getMethods()) {
+            Effect[] annotations = m.getAnnotationsByType(Effect.class);
+            for (Effect e : annotations) {
+                for (String path: e.value()) {
+                    String[] parts = path.split("\\.");
+                    String modulePath = String.join(".", Arrays.copyOf(parts, parts.length - 1));
+                    modulePaths.add(modulePath);
+                }
+            }
+        }
+
+        List<TypedModuleSpec> specs = new ArrayList<>();
+        for (String path : modulePaths) {
+            Module mod = ModuleResolver.getLocal().resolveModule(path);
+            specs.add(mod.getSpec());
+        }
+        return specs;
     }
 
     public static Pair<VarBinding, GenContext> doPythonImport(URI uri, GenContext ctx) {

tools/src/wyvern/tools/interop/FFIImport.java

@@ -69,14 +69,19 @@ public ValueType getFFIType() {
 
     @Override
     public ValueType typeCheck(TypeContext ctx, EffectAccumulator effectAccumulator) {
+        try {
+            FObject obj = new JavaImporter(ctx).find(path, this);
+        } catch (ReflectiveOperationException e1) {
+            throw new RuntimeException(e1);
+        }
         return this.getType();
     }
 
     @Override
     public Value interpret(EvalContext ctx) {
         if (this.ffiType.equals(new NominalType("system", "java"))) {
             try {
-                FObject obj = wyvern.tools.interop.Default.importer().find(path, this);
+                FObject obj = new JavaImporter(ctx).find(path, this);
                 return new JavaValue(obj, this.getType());
             } catch (ReflectiveOperationException e1) {
                 throw new RuntimeException(e1);

tools/src/wyvern/tools/interop/GenUtil.java

@@ -99,8 +99,16 @@ public static ValueType javaClassToWyvernType(Class<?> javaClass, TypeContext ct
             return Util.listType();
         }
 
+        if (javaClass.getName().equals("void")) {
+            return Util.unitType();
+        }
+
+        // otherwise, arbitrary java class
+
         StructuralTypesFromJava type = (StructuralTypesFromJava) ctx.lookupTypeOf(javaTypesObjectName);
-        return type.getJavaType(javaClass, ctx, safe);
+        ValueType newType = type.getJavaType(javaClass, ctx, safe);
+
+        return newType;
     }
 
     public static Variable getJavaTypesObject() {