Improved typechecking for if and if-in-state so that when a branch re…

…turns,

that branch's output context is not merged with the other branch's ouptut context.

resources/tests/type_checker_tests/Branching.obs

@@ -134,4 +134,50 @@ contract StatesWithFields {
             x = new StatesWithFields();
         }
     }
+}
+
+contract States {
+    state S1;
+    state S2;
+
+    States@Owned() {
+        ->S1;
+    }
+}
+
+contract ReturnBranch {
+
+    transaction t1(LinearContract@Owned >> Unowned x) {
+        if (true) {
+            disown x;
+            return;
+        }
+        // No error here despite different types of 'x' in different branches,
+        // since the only branch there returns.
+        disown x;
+    }
+
+    transaction t2(LinearContract@Owned >> Unowned x) {
+        if (true) {
+            disown x;
+            return;
+        }
+        else {
+        }
+        // No error here despite different types of 'x' in different branches,
+        // since the true branch returns.
+        disown x;
+    }
+
+    transaction t3(LinearContract@Owned >> Unowned x) {
+        States y = new States();
+
+        if (y in S1) {
+            disown x;
+            return;
+        }
+        // No error here despite different types of 'x' and 'y' in different branches,
+        // since both branches return.
+        disown x;
+    }
 }

resources/tests/type_checker_tests/Return.obs

@@ -67,3 +67,20 @@ main contract C {
         return c;
     }
 }
+
+contract HasField {
+    HasField@Owned h;
+
+    HasField@Owned() {
+        h = new HasField(); // Ignore infinite recursion for now!
+    }
+
+    transaction t() {
+        if (true) {
+            disown h;
+            return;
+        }
+        disown h;
+        h = new HasField();
+    }
+}

src/main/scala/edu/cmu/cs/obsidian/typecheck/Checker.scala

@@ -1830,11 +1830,36 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
                 val (t, contextPrime, ePrime) = inferAndCheckExpr(decl, context, eCond, NoOwnershipConsumption())
                 checkIsSubtype(contextPrime.contractTable, s, t, BoolType())
                 val (newContext, checkedStatements) = checkStatementSequence(decl, contextPrime, body)
-                val contextIfTrue = pruneContext(s,
-                    newContext,
-                    contextPrime)
-                (mergeContext(s, contextPrime, contextIfTrue), If(ePrime, checkedStatements).setLoc(s))
+                val newIf = If(ePrime, checkedStatements).setLoc(s)
+                if (hasReturnStatementDontLog(body)) {
+                    // The body definitely returns, so the body has no impact
+                    // on the context following this if. Put another way:
+
+                    /*
+                    if (e) {
+                        return;
+                    }
+                    s
+
+                    is equivalent to:
+
+                    if (e) {
+                        return;
+                    }
+                    else {
+                        // check s in the same context as the body of the if
+                        s
+                    }
 
+                    */
+                    (contextPrime, newIf)
+                }
+                else {
+                    val contextIfTrue = pruneContext(s,
+                        newContext,
+                        contextPrime)
+                    (mergeContext(s, contextPrime, contextIfTrue), newIf)
+                }
             case IfThenElse(eCond: Expression, body1: Seq[Statement], body2: Seq[Statement]) =>
                 val (t, contextPrime, ePrime) = inferAndCheckExpr(decl, context, eCond, NoOwnershipConsumption())
                 checkIsSubtype(contextPrime.contractTable, s, t, BoolType())
@@ -1848,7 +1873,27 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
                 val contextIfFalse = pruneContext(s,
                     falseContext,
                     contextPrime)
-                (mergeContext(s, contextIfTrue, contextIfFalse), IfThenElse(ePrime, checkedTrueStatements, checkedFalseStatements).setLoc(s))
+
+                val newIf = IfThenElse(ePrime, checkedTrueStatements, checkedFalseStatements).setLoc(s)
+
+                val trueBranchReturns = hasReturnStatementDontLog(body1)
+                val falseBranchReturns = hasReturnStatementDontLog(body2)
+
+                if (trueBranchReturns && falseBranchReturns) {
+                    // If they both return, then the two bodies have no impact on the context afterward.
+                    (contextPrime, newIf)
+                }
+                else if (trueBranchReturns) {
+                    // The true branch returns, so its context changes are irrelevant
+                    (contextIfFalse, newIf)
+                }
+                else if (falseBranchReturns) {
+                    // The false branch returns, so its context changes are irrelevant
+                    (contextIfTrue, newIf)
+                }
+                else {
+                    (mergeContext(s, contextIfTrue, contextIfFalse), newIf)
+                }
 
             case IfInState(e, ePerm, state, body1, body2) =>
 
@@ -2007,6 +2052,8 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
                         }
                 }
 
+                val newStatement = IfInState(ePrime, ePermPrime, state, checkedTrueStatements, checkedFalseStatements).setLoc(s)
+
                 // Throw out (prune) any variables that were local to the branches.
                 val contextIfTrue = pruneContext(s,
                     resetTrueContext,
@@ -2016,14 +2063,30 @@ class Checker(globalTable: SymbolTable, verbose: Boolean = false) {
                     resetFalseContext,
                     contextPrime)
 
-                val mergedContext = mergeContext(s, contextIfTrue, contextIfFalse)
-                val finalContext = valVariableToClear match {
-                    case None => mergedContext
-                    case Some(x) => mergedContext.updatedClearingValVariable (x)
+                val trueBranchReturns = hasReturnStatementDontLog(body1)
+                val falseBranchReturns = hasReturnStatementDontLog(body2)
+
+                if (trueBranchReturns && falseBranchReturns) {
+                    // If they both return, then the two bodies have no impact on the context afterward.
+                    (contextPrime, newStatement)
                 }
-                val newStatement = IfInState(ePrime, ePermPrime, state, checkedTrueStatements, checkedFalseStatements).setLoc(s)
+                else if (trueBranchReturns) {
+                    // The true branch returns, so its context changes are irrelevant
+                    (contextIfFalse, newStatement)
+                }
+                else if (falseBranchReturns) {
+                    // The false branch returns, so its context changes are irrelevant
+                    (contextIfTrue, newStatement)
+                }
+                else {
+                    val mergedContext = mergeContext(s, contextIfTrue, contextIfFalse)
+                    val finalContext = valVariableToClear match {
+                        case None => mergedContext
+                        case Some(x) => mergedContext.updatedClearingValVariable(x)
+                    }
 
-                (finalContext, newStatement)
+                    (finalContext, newStatement)
+                }
             case TryCatch(s1: Seq[Statement], s2: Seq[Statement]) =>
                 val (tryContext, checkedTryStatements) = checkStatementSequence(decl, context, s1)
                 val (catchContext, checkedCatchStatements) = checkStatementSequence(decl, context, s2)