support arbitrary control flow in final statement inside loop

also fix and extend some comments

goose.go

@@ -1065,6 +1065,7 @@ func (c *cursor) Remainder() []ast.Stmt {
 	return s
 }
 
+// If this returns true, the body truly *must* always end in an early return or loop control effect.
 func (ctx Ctx) endsWithReturn(s ast.Stmt) bool {
 	if s == nil {
 		return false
@@ -1087,10 +1088,7 @@ func (ctx Ctx) stmtsEndWithReturn(ss []ast.Stmt) bool {
 	case *ast.IfStmt:
 		left := ctx.endsWithReturn(s.Body)
 		right := ctx.endsWithReturn(s.Else)
-		if left != right {
-			ctx.unsupported(s, "nested if statement branches differ on whether they return")
-		}
-		return left // or right, doesn't matter
+		return left && right // we can only return true if we *always* end in a control effect
 	}
 	return false
 }
@@ -1156,49 +1154,47 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, remainder []ast.Stmt, usage ExprValUsage) c
 	ife := coq.IfExpr{
 		Cond: condExpr,
 	}
+	// Extract (possibly empty) list of stmts in Else
+	var Else = []ast.Stmt{}
+	if s.Else != nil {
+		Else = s.Else.(*ast.BlockStmt).List
+	}
+
+	// Supported cases are:
+	// - There is no code after the conditional -- then anything goes.
+	// - The "then" branch always returns, and there is no "else" branch.
+	// - Neither "then" nor "else" ever return.
+
+	if len(remainder) == 0 {
+		// The remainder is empty, so just propagate the usage to both branches.
+		ife.Then = ctx.blockStmt(s.Body, usage)
+		ife.Else = ctx.stmts(Else, usage)
+		return coq.NewAnon(ife)
+	}
 
+	// There is code after the conditional -- merging control flow. Let us see what we can do.
 	// Determine if we want to propagate our usage (i.e. the availability of control effects)
-	// to the conditional or not. This is not relevant for correctness (stmt generation will
-	// appropriately error when a control effect arises where it is not supported), but Crucial
-	// for supporting a reasonable subset of Go.
-	bodyEndsWithReturn := ctx.endsWithReturn(s.Body)
-
-	// If the "then" branch want to early-return, translate it accordingly, propagating the usage.
-	if bodyEndsWithReturn {
-		// stmts takes care of finalization for us
+	// to the conditional or not.
+	if ctx.endsWithReturn(s.Body) {
 		ife.Then = ctx.blockStmt(s.Body, usage)
-		if len(remainder) > 0 {
-			// If there are remaining expressions after this, put them into "else".
-			// Actual "else" must be empty.
-			if s.Else != nil {
-				ctx.futureWork(s.Else, "early return in if with an else branch")
-				return coq.Binding{}
-			}
-			// We can propagate the usage here since the return value of this part
-			// will become the return value of the entire conditional (that's why we
-			// put the remainder *inside* the conditional).
-			ife.Else = ctx.stmts(remainder, usage)
-		} else {
-			// Remainder is empty; translate "else" branch with our usage.
-			if s.Else == nil {
-				// Be careful to perform proper finalization according to our usage.
-				ife.Else = ctx.stmts([]ast.Stmt{}, usage)
-			} else {
-				ife.Else = ctx.stmts(s.Else.(*ast.BlockStmt).List, usage)
-			}
-		}
+		// Put trailing code into "else". This is correct because "then" will always return.
+		// "else" must be empty.
+		if s.Else != nil {
+			ctx.futureWork(s.Else, "early return in if with an else branch")
+			return coq.Binding{}
+		}
+		// We can propagate the usage here since the return value of this part
+		// will become the return value of the entire conditional (that's why we
+		// put the remainder *inside* the conditional).
+		ife.Else = ctx.stmts(remainder, usage)
 		return coq.NewAnon(ife)
 	}
 
 	// No early return in "then" branch; translate this as a conditional in the middle of
 	// a block (not propagating the usage). This will implicitly check that
 	// the two branches do not rely on control effects.
 	ife.Then = ctx.blockStmt(s.Body, ExprValLocal)
-	if s.Else == nil {
-		ife.Else = ctx.stmts([]ast.Stmt{}, ExprValLocal)
-	} else {
-		ife.Else = ctx.stmts(s.Else.(*ast.BlockStmt).List, ExprValLocal)
-	}
+	ife.Else = ctx.stmts(Else, ExprValLocal)
 	// And translate the remainder with our usage.
 	tailExpr := ctx.stmts(remainder, usage)
 	// Prepend the if-then-else before the tail.

internal/examples/logging2/logging2.gold.v

@@ -228,8 +228,7 @@ Definition Txn__Write: val :=
     then
       (if: ("addr" = LOGMAXBLK)
       then "ret" <-[boolT] #false
-      else MapInsert (struct.get Txn "blks" "txn") "addr" (![slice.T byteT] "blk"));;
-      #()
+      else MapInsert (struct.get Txn "blks" "txn") "addr" (![slice.T byteT] "blk"))
     else #());;
     ![boolT] "ret".
 Theorem Txn__Write_t: ⊢ Txn__Write : (struct.t Txn -> uint64T -> refT disk.blockT -> boolT).

internal/examples/semantics/semantics.gold.v

@@ -16,8 +16,7 @@ Definition findKey: val :=
       then
         "found" <-[uint64T] "k";;
         "ok" <-[boolT] #true
-      else #());;
-      #());;
+      else #()));;
     (![uint64T] "found", ![boolT] "ok").
 Theorem findKey_t: ⊢ findKey : (mapT (struct.t unit) -> (uint64T * boolT)).
 Proof. typecheck. Qed.

internal/examples/unittest/loops.go

@@ -46,6 +46,19 @@ func conditionalInLoopElse() {
 	}
 }
 
+func nestedConditionalInLoopImplicitContinue() {
+	for i := uint64(0); ; {
+		if i > 5 {
+			if i > 10 {
+				break
+			}
+		} else {
+			i = i + 1
+			continue
+		}
+	}
+}
+
 func ImplicitLoopContinue() {
 	for i := uint64(0); ; {
 		if i < 4 {

internal/examples/unittest/unittest.gold.v

@@ -407,14 +407,29 @@ Definition conditionalInLoopElse: val :=
         Continue));;
     #().
 
+Definition nestedConditionalInLoopImplicitContinue: val :=
+  rec: "nestedConditionalInLoopImplicitContinue" <> :=
+    let: "i" := ref_to uint64T #0 in
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      (if: ![uint64T] "i" > #5
+      then
+        (if: ![uint64T] "i" > #10
+        then Break
+        else Continue)
+      else
+        "i" <-[uint64T] ![uint64T] "i" + #1;;
+        Continue));;
+    #().
+
 Definition ImplicitLoopContinue: val :=
   rec: "ImplicitLoopContinue" <> :=
     let: "i" := ref_to uint64T #0 in
     (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
       (if: ![uint64T] "i" < #4
-      then "i" <-[uint64T] #0
-      else #());;
-      Continue);;
+      then
+        "i" <-[uint64T] #0;;
+        Continue
+      else Continue));;
     #().
 
 Definition ImplicitLoopContinue2: val :=

testdata/negative-tests/badif2.go

@@ -4,7 +4,7 @@ func Skip() {}
 
 func BadIf2(i uint64) {
 	if i == 0 {
-		if true { // ERROR nested if statement branches differ on whether they return
+		if true { // ERROR return in unsupported position
 			return
 		} else {
 			Skip()