Fixed a dynamic state test bug: only reset the tested variable's type…

… if it is still in scope.
mcoblenz · Nov 27, 2019 · 1a09352 · 1a09352
1 parent 6025ed6
commit 1a09352
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 4 deletions.
diff --git a/resources/tests/type_checker_tests/InState.obs b/resources/tests/type_checker_tests/InState.obs
@@ -106,4 +106,23 @@ contract TestFieldShared {
              ->S1(next = temp);
          }
      }
- }
+ }
+
+ contract TestTransition {
+    state S1;
+    state S2 {
+        TestTransition@Shared x;
+    }
+
+    TestTransition@S1() {
+        ->S1;
+    }
+
+    transaction t1(TestTransition@Shared this) {
+        if (this in S2) {
+            if (x in S2) {
+                ->S1;
+            }
+        }
+    }
+}
diff --git a/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala b/src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala
@@ -1008,7 +1008,7 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
         }
     }
 
-    // Removes any field types from thisFieldTypes that are already consisten with their declarations.
+    // Removes any field types from thisFieldTypes that are already consistent with their declarations.
     private def packFieldTypes(context: Context): Context = {
         var resultContext = context
         for ((field, typ) <- context.thisFieldTypes) {
@@ -1986,8 +1986,18 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
                     case None => (packedTrueContext, packedFalseContext)
                     case Some((x, oldType)) =>
                         if (exprIsField) {
-                            (packedTrueContext.updatedThisFieldType(x, oldType),
-                            packedFalseContext.updatedThisFieldType(x, oldType))
+                            // Only reset the tested field in the context if it is still in scope (since the type of this may have changed)
+                            val revisedTrueContext = if (packedTrueContext.lookupDeclaredFieldTypeInThis(x).isDefined) {
+                                packedTrueContext.updatedThisFieldType(x, oldType)
+                            } else {
+                                packedTrueContext
+                            }
+                            val revisedFalseContext = if (packedFalseContext.lookupDeclaredFieldTypeInThis(x).isDefined) {
+                                packedFalseContext.updatedThisFieldType(x, oldType)
+                            } else {
+                                packedFalseContext
+                            }
+                            (revisedTrueContext, revisedFalseContext)
                         }
                         else {
                             (packedTrueContext.updated(x, oldType), packedFalseContext.updated(x, oldType))