Added an error message for use of uninitialized state initializers (S…

…::x).
mcoblenz · Dec 9, 2019 · ed049b9 · ed049b9
1 parent e197dfb
commit ed049b9
Show file tree

Hide file tree

Showing 5 changed files with 33 additions and 2 deletions.
diff --git a/resources/tests/type_checker_tests/StateInitialization.obs b/resources/tests/type_checker_tests/StateInitialization.obs
@@ -65,4 +65,18 @@ contract HasField {
         S::x = 2;
         ->S;
     }
+}
+
+contract ImproperUse {
+    state S {
+        int x;
+    }
+
+    ImproperUse@S() {
+        ->S(x = 1);
+    }
+
+    transaction t(ImproperUse@S this) returns int {
+        return S::x; // Error: state initializer has not been intialized!
+    }
 }
diff --git a/src/main/scala/edu/cmu/cs/obsidian/parser/Parser.scala b/src/main/scala/edu/cmu/cs/obsidian/parser/Parser.scala
@@ -338,7 +338,8 @@ object Parser extends Parsers {
     }
 
     private def parseExpr = parseDisown
-    private def parseDisown = parseUnary(DisownT(), Disown.apply, parseAnd)
+    private def parseDisown = parseUnary(DisownT(), Disown
+        .apply, parseAnd)
     private def parseAnd = parseBinary(AndT(), Conjunction.apply, parseOr)
     private def parseOr = parseBinary(OrT(), Disjunction.apply, parseEq)
 
@@ -410,7 +411,7 @@ object Parser extends Parsers {
         val parseVar = parseId ^^ { (id: Identifier) => ReferenceIdentifier(id._1).setLoc(id) }
 
         val parseStateInitializer = parseId ~ ColonColonT() ~! parseId ^^ {
-            case stateName ~ _ ~ fieldName => StateInitializer(stateName, fieldName)
+            case stateName ~ _ ~ fieldName => StateInitializer(stateName, fieldName).setLoc(stateName)
         }
 
         val parseNumLiteral = {

diff --git a/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala b/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala
@@ -904,6 +904,14 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
                  (newTyp, finalContext, ePrime)
              case StateInitializer(stateName, fieldName) =>
                  // A state initializer expression has its field's type.
+                 if (!context.transitionFieldsDefinitelyInitialized.exists(
+                     {
+                         case (stateNameInitialized, fieldNameInitialized, _) =>
+                             (stateName._1 == stateNameInitialized && fieldName._1 == fieldNameInitialized)
+                     }))
+                     {
+                         logError(e, StateInitializerUninitialized(stateName._1, fieldName._1))
+                     }
 
                  val stateOption = context.contractTable.state(stateName._1)
                  val fieldType = stateOption match {

diff --git a/src/main/scala/edu/cmu/cs/obsidian/typecheck/Error.scala b/src/main/scala/edu/cmu/cs/obsidian/typecheck/Error.scala
@@ -468,4 +468,10 @@ case class GenericParamShadowError(param1Binder: String, param1: GenericType,
 
 case class FieldTypesIncompatibleAcrossBranches(fieldName: String, typ: ObsidianType, branch: String) extends Error {
     override val msg: String = s"Field $fieldName must have compatible types in both branches, but it was given incompatible type $typ in the $branch branch."
+}
+
+case class StateInitializerUninitialized(stateName: String, fieldName: String) extends Error {
+    override val msg: String = s"$stateName::$fieldName has not been initialized. Perhaps you are " +
+        s"trying to use a field initializer for general-purpose field access instead of only for " +
+        s"preparing for a transition."
 }
diff --git a/src/test/scala/edu/cmu/cs/obsidian/tests/TypeCheckerTests.scala b/src/test/scala/edu/cmu/cs/obsidian/tests/TypeCheckerTests.scala
@@ -509,6 +509,8 @@ class TypeCheckerTests extends JUnitSuite {
                 ::
                 (RedundantFieldInitializationError("m"), 55)
                 ::
+                (StateInitializerUninitialized("S", "x"), 80)
+                ::
                 Nil
         )
     }