Give an error when trying to substitute only a contract name for a ty…

…pe parameter that requires both a contract name and a permission.
mcoblenz · Jan 21, 2020 · 6d7ecd5 · 6d7ecd5
1 parent c5bbb81
commit 6d7ecd5
Show file tree

Hide file tree

Showing 5 changed files with 25 additions and 2 deletions.
diff --git a/resources/tests/type_checker_tests/GenericsStateVariables.obs b/resources/tests/type_checker_tests/GenericsStateVariables.obs
@@ -71,5 +71,10 @@ main contract C {
         // This should also fail, because peek() returns an Unowned reference
         return maybeA.peek().getX();
     }
+
+    transaction missingPermission() {
+        // Error: missing parameter s (Maybe[X@s])
+        Maybe[A] m = new Maybe[A](new A(4));
+    }
 }
 
diff --git a/src/main/scala/edu/cmu/cs/obsidian/parser/AST.scala b/src/main/scala/edu/cmu/cs/obsidian/parser/AST.scala
@@ -180,6 +180,7 @@ case class ReturnExpr(e: Expression) extends Statement {
 }
 
 // We distinguish between no update clause given and an empty update clause for a clean separation between syntax and semantics.
+// thisPermission is the permission of 'this' at the time of the transition. It is used for enforcing state locks caused by dynamic state checks.
 case class Transition(newStateName: String, updates: Option[Seq[(ReferenceIdentifier, Expression)]], thisPermission: Permission) extends Statement {
     override def substitute(genericParams: Seq[GenericType], actualParams: Seq[ObsidianType]): Transition = {
         def doSubstitute: ((ReferenceIdentifier, Expression)) => (ReferenceIdentifier, Expression) = {

diff --git a/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala b/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala
@@ -529,6 +529,15 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
             if (isSubtype(table, actualArg, substitutedParam, isThis = false).isDefined) {
                 logError(ast, GenericParameterError(param, actualArg))
             }
+
+            actualArg match {
+                case nonPrimitiveActualArg: NonPrimitiveType =>
+                    if (nonPrimitiveActualArg.permission == Inferred() && param.gVar.permissionVar.isDefined) {
+                        logError(ast, GenericParameterPermissionMissingError(param, param.gVar.permissionVar.get, nonPrimitiveActualArg))
+                    }
+                case _ =>
+                    // Nothing to do here.
+            }
         }
     }
 
@@ -2678,7 +2687,7 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
         constr.copy(body = newBody)
     }
 
-    private def checkConstructors(constructors: Seq[Constructor], contract: ObsidianContractImpl, table: ContractTable): Unit = {
+    private def checkConstructorDistinguishibility(constructors: Seq[Constructor], contract: ObsidianContractImpl, table: ContractTable): Unit = {
         if (constructors.isEmpty && table.stateLookup.nonEmpty && !contract.isInterface) {
             logError(contract, NoConstructorError(contract.name))
         }
@@ -2873,7 +2882,7 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
 
                     implementOk(table, obsContract, obsContract.bound.contractName, obsContract.declarations, boundDecls)
                     newDecls = obsContract.declarations.map(checkDeclaration(table))
-                    checkConstructors(table.constructors, obsContract, table)
+                    checkConstructorDistinguishibility(table.constructors, obsContract, table)
                 }
 
                 obsContract.copy(declarations = newDecls)

diff --git a/src/main/scala/edu/cmu/cs/obsidian/typecheck/Error.scala b/src/main/scala/edu/cmu/cs/obsidian/typecheck/Error.scala
@@ -437,6 +437,10 @@ case class GenericParameterAssetError(paramName: String, argTypeName: String) ex
         s"Argument type $argTypeName is an asset, but the type parameter $paramName is not allowed to be an asset. Add the 'asset' modifier to $paramName to allow the parameter to be an asset."
 }
 
+case class GenericParameterPermissionMissingError(param: GenericType, permVariable: String, actualArg: ObsidianType) extends Error {
+    val msg: String = s"Missing specification for a value for the permission variable $permVariable in $param in type parameter $actualArg."
+}
+
 case class PermissionCheckRedundant(actualPerm: Permission, testPermission: Permission,
                                     isSubperm: Boolean) extends Error {
     private val isSubpermStr: String =

diff --git a/src/test/scala/edu/cmu/cs/obsidian/tests/TypeCheckerTests.scala b/src/test/scala/edu/cmu/cs/obsidian/tests/TypeCheckerTests.scala
@@ -871,6 +871,10 @@ class TypeCheckerTests extends JUnitSuite {
             (ReceiverTypeIncompatibleError("getX",
                 ContractReferenceType(ContractType("A", Nil), Unowned(), NotRemoteReferenceType()),
                 StateType(ContractType("A", Nil), "S1", NotRemoteReferenceType())), 72) ::
+                (GenericParameterPermissionMissingError(GenericType(GenericVar(isAsset = false,"X",Some("s")),
+                    GenericBoundPerm(interfaceSpecified = false, permSpecified = false, ContractType.topContractType, Unowned())),
+                "s",
+                    ContractReferenceType(ContractType("A", Nil), Inferred(), NotRemoteReferenceType())), 77)::
                 Nil)
     }