From cec9bb6f4229c4b52125db58b03b52a9659d7d7d Mon Sep 17 00:00:00 2001
From: Ralf Jung <research@ralfj.de>
Date: Mon, 6 Sep 2021 18:39:04 -0400
Subject: [PATCH 1/6] refactor handling of control effects (early
 return/break/continue)

The key idea is to prepagate an ExprValUsage variable everywhere which says how
the currently generated GooseLang term will be "used", thereby also defining
which control effects are supported.
---
 goose.go                                      | 307 ++++++++++--------
 .../examples/append_log/append_log.gold.v     |  12 +-
 internal/examples/logging2/logging2.gold.v    |  26 +-
 internal/examples/semantics/semantics.gold.v  |  69 ++--
 internal/examples/simpledb/simpledb.gold.v    |  50 ++-
 internal/examples/unittest/loops.go           |  18 +-
 internal/examples/unittest/trailing_call.go   |   9 +
 internal/examples/unittest/unittest.gold.v    | 140 +++++---
 internal/examples/wal/wal.gold.v              |  29 +-
 testdata/negative-tests/badif1.go             |   2 +-
 testdata/negative-tests/badif2.go             |   4 +-
 testdata/negative-tests/badif3.go             |  13 +
 testdata/negative-tests/badloop1.go           |  12 -
 testdata/negative-tests/deadcode.go           |   4 +-
 14 files changed, 421 insertions(+), 274 deletions(-)
 create mode 100644 internal/examples/unittest/trailing_call.go
 create mode 100644 testdata/negative-tests/badif3.go
 delete mode 100644 testdata/negative-tests/badloop1.go

diff --git a/goose.go b/goose.go
index aa668f76..c5355b62 100644
--- a/goose.go
+++ b/goose.go
@@ -40,6 +40,20 @@ type Ctx struct {
 // Implement flag.Value for a "set" of strings; used by Config
 type StringSet map[string]bool
 
+// Says how the result of the currently generated expression will be used
+type ExprValUsage int
+
+const (
+	// The result of this expression will only be used locally, or entirelz discarded
+	ExprValLocal ExprValUsage = iota
+	// The result of this expression will be returned from the current function
+	// (i.e., the "early return" control effect is available here)
+	ExprValReturned
+	// The result of this expression will control the current loop
+	// (i.e., the "break/continue" control effect is available here)
+	ExprValLoop
+)
+
 func (s *StringSet) String() string {
 	r := ""
 	for k := range *s {
@@ -983,7 +997,7 @@ func (ctx Ctx) funcLit(e *ast.FuncLit) coq.FuncLit {
 
 	fl.Args = ctx.paramList(e.Type.Params)
 	// fl.ReturnType = ctx.returnType(d.Type.Results)
-	fl.Body = ctx.blockStmt(e.Body, nil)
+	fl.Body = ctx.blockStmt(e.Body, ExprValReturned)
 	return fl
 }
 
@@ -1024,8 +1038,8 @@ func (ctx Ctx) exprSpecial(e ast.Expr, isSpecial bool) coq.Expr {
 	return nil
 }
 
-func (ctx Ctx) blockStmt(s *ast.BlockStmt, loopVar *string) coq.BlockExpr {
-	return ctx.stmts(s.List, loopVar)
+func (ctx Ctx) blockStmt(s *ast.BlockStmt, usage ExprValUsage) coq.BlockExpr {
+	return ctx.stmts(s.List, usage)
 }
 
 type cursor struct {
@@ -1063,21 +1077,10 @@ func (ctx Ctx) endsWithReturn(s ast.Stmt) bool {
 	}
 }
 
-func endIncludesIf(s ast.Stmt) bool {
-	if s == nil {
-		return false
-	}
-	if s, ok := s.(*ast.BlockStmt); ok {
-		return stmtsEndIncludesIf(s.List)
-	}
-	return stmtsEndIncludesIf([]ast.Stmt{s})
-}
-
 func (ctx Ctx) stmtsEndWithReturn(ss []ast.Stmt) bool {
 	if len(ss) == 0 {
 		return false
 	}
-	// TODO: should also catch implicit continue
 	switch s := ss[len(ss)-1].(type) {
 	case *ast.ReturnStmt, *ast.BranchStmt:
 		return true
@@ -1092,35 +1095,56 @@ func (ctx Ctx) stmtsEndWithReturn(ss []ast.Stmt) bool {
 	return false
 }
 
-func stmtsEndIncludesIf(ss []ast.Stmt) bool {
-	if len(ss) <= 1 {
-		return false
-	}
-	if _, ok := ss[len(ss)-1].(*ast.IfStmt); ok {
-		return false
-	}
-	for _, item := range ss {
-		if _, ok := item.(*ast.IfStmt); ok {
-			return true
-		}
-	}
-	return false
-}
-
-func (ctx Ctx) stmts(ss []ast.Stmt, loopVar *string) coq.BlockExpr {
+func (ctx Ctx) stmts(ss []ast.Stmt, usage ExprValUsage) coq.BlockExpr {
 	c := &cursor{ss}
 	var bindings []coq.Binding
+	var finalized bool
 	for c.HasNext() {
-		bindings = append(bindings, ctx.stmt(c.Next(), c, loopVar))
+		s := c.Next()
+		// ifStmt is special, it gets a chance to "wrap" the entire remainder
+		// to better support early returns.
+		switch s := s.(type) {
+		case *ast.IfStmt:
+			bindings = append(bindings, ctx.ifStmt(s, c.Remainder(), usage))
+			finalized = true
+			break // This would happen anyway since we consumed the iterator via "Remainder"
+		default:
+			if c.HasNext() {
+				// "finalized" will always be true.
+				binding, _ := ctx.stmtInBlock(s, ExprValLocal)
+				bindings = append(bindings, binding)
+			} else {
+				// The last statement is special: we propagate the usage and store "finalized"
+				binding, fin := ctx.stmtInBlock(s, usage)
+				bindings = append(bindings, binding)
+				finalized = fin
+			}
+		}
 	}
-	if len(bindings) == 0 {
-		retExpr := coq.ReturnExpr{coq.Tt}
-		return coq.BlockExpr{[]coq.Binding{coq.NewAnon(retExpr)}}
+	// Crucially, we also arrive in this branch if the list if statements is empty.
+	if !finalized {
+		switch usage {
+		case ExprValReturned:
+			bindings = append(bindings, coq.NewAnon(coq.ReturnExpr{coq.Tt}))
+		case ExprValLoop:
+			bindings = append(bindings, coq.NewAnon(coq.LoopContinue))
+		case ExprValLocal:
+			// Make sure the list of bindings is not empty -- translate empty blocks to unit
+			if len(bindings) == 0 {
+				bindings = append(bindings, coq.NewAnon(coq.ReturnExpr{coq.Tt}))
+			}
+		default:
+			panic("bad ExprValUsage")
+		}
 	}
 	return coq.BlockExpr{bindings}
 }
 
-func (ctx Ctx) ifStmt(s *ast.IfStmt, c *cursor, loopVar *string) coq.Binding {
+// ifStmt has special support for an early-return "then" branch; to achieve that
+// it is responsible for generating the if *together with* all the statements that
+// follow it in the same block.
+// It is also responsible for "finalizing" the expression according to the usage.
+func (ctx Ctx) ifStmt(s *ast.IfStmt, remainder []ast.Stmt, usage ExprValUsage) coq.Binding {
 	// TODO: be more careful about nested if statements; if the then branch has
 	//  an if statement with early return, this is probably not handled correctly.
 	//  We should conservatively disallow such returns until they're properly analyzed.
@@ -1128,66 +1152,58 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, c *cursor, loopVar *string) coq.Binding {
 		ctx.unsupported(s.Init, "if statement initializations")
 		return coq.Binding{}
 	}
-	thenExpr, ok := ctx.stmt(s.Body, &cursor{nil}, loopVar).Unwrap()
-	if !ok {
-		ctx.nope(s.Body, "if statement body ends with an assignment")
-		return coq.Binding{}
-	}
+	condExpr := ctx.expr(s.Cond)
 	ife := coq.IfExpr{
-		Cond: ctx.expr(s.Cond),
-		Then: thenExpr,
+		Cond: condExpr,
 	}
 
-	// supported use cases
-	// (1) early return, no else branch; remainder of function is lifted to else
-	// (2) both branches and no remainder
-	//
-	// If the else branch also doesn't return it's not a problem to handle subsequent code,
-	// but that's annoying and we can leave it for later. Maybe the special case
-	// of Else == nil should be supported, though.
-
-	remaining := c.HasNext()
+	// 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 bodyEndsWithReturn && remaining {
-		if s.Else != nil {
-			ctx.futureWork(s.Else, "else with early return")
-			return coq.Binding{}
+
+	// If the "then" branch want to early-return, translate it accordingly, propagating the usage.
+	if bodyEndsWithReturn {
+		// stmts takes care of finalization for us
+		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)
+			}
 		}
-		ife.Else = ctx.stmts(c.Remainder(), loopVar)
 		return coq.NewAnon(ife)
 	}
-	if !bodyEndsWithReturn && remaining && s.Else == nil {
-		// conditional statement in the middle of a block
-		retUnit := coq.ReturnExpr{coq.Tt}
-		ife.Then = coq.BlockExpr{[]coq.Binding{
-			coq.NewAnon(ife.Then),
-			coq.NewAnon(retUnit),
-		}}
-		ife.Else = retUnit
-		return coq.NewAnon(ife)
-	}
-	elseEndsWithReturn := ctx.endsWithReturn(s.Else)
-	// the if expression is last in the surrounding block,
-	// so returns in it become returns from the overall function
-	// OR
-	// neither branch terminates the outer function,
-	// the if expression is just a conditional in the middle
-	if !remaining || (!bodyEndsWithReturn && !elseEndsWithReturn) {
-		if s.Else == nil {
-			ife.Else = coq.ReturnExpr{coq.Tt}
-			return coq.NewAnon(ife)
-		}
-		elseExpr, ok := ctx.stmt(s.Else, c, loopVar).Unwrap()
-		if !ok {
-			ctx.nope(s.Else, "if statement else ends with an assignment")
-			return coq.Binding{}
-		}
-		ife.Else = elseExpr
-		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)
 	}
-	// there are some other cases that can be handled but it's a bit tricky
-	ctx.futureWork(s, "non-terminal if expressions are only partially supported")
-	return coq.Binding{}
+	// And translate the remainder with our usage.
+	tailExpr := ctx.stmts(remainder, usage)
+	// Prepend the if-then-else before the tail.
+	bindings := append([]coq.Binding{coq.NewAnon(ife)}, tailExpr.Bindings...)
+	return coq.NewAnon(coq.BlockExpr{Bindings: bindings})
 }
 
 func (ctx Ctx) loopVar(s ast.Stmt) (ident *ast.Ident, init coq.Expr) {
@@ -1210,14 +1226,12 @@ func (ctx Ctx) loopVar(s ast.Stmt) (ident *ast.Ident, init coq.Expr) {
 func (ctx Ctx) forStmt(s *ast.ForStmt) coq.ForLoopExpr {
 	var init = coq.NewAnon(coq.Skip)
 	var ident *ast.Ident
-	loopVar := new(string)
 	if s.Init != nil {
 		ident, _ = ctx.loopVar(s.Init)
 		ctx.addDef(ident, identInfo{
 			IsPtrWrapped: true,
 		})
-		init = ctx.stmt(s.Init, &cursor{nil}, nil)
-		loopVar = &ident.Name
+		init = ctx.stmt(s.Init, ExprValLocal)
 	}
 	var cond coq.Expr = coq.True
 	if s.Cond != nil {
@@ -1225,25 +1239,14 @@ func (ctx Ctx) forStmt(s *ast.ForStmt) coq.ForLoopExpr {
 	}
 	var post coq.Expr = coq.Skip
 	if s.Post != nil {
-		postBlock := ctx.stmt(s.Post, &cursor{nil}, loopVar)
+		postBlock := ctx.stmt(s.Post, ExprValLocal)
 		if len(postBlock.Names) > 0 {
 			ctx.unsupported(s.Post, "post cannot bind names")
 		}
 		post = postBlock.Expr
 	}
 
-	hasExplicitBranch := ctx.endsWithReturn(s.Body)
-	hasImplicitBranch := endIncludesIf(s.Body)
-
-	c := &cursor{s.Body.List}
-	var bindings []coq.Binding
-	for c.HasNext() {
-		bindings = append(bindings, ctx.stmt(c.Next(), c, loopVar))
-	}
-	if !hasExplicitBranch && !hasImplicitBranch {
-		bindings = append(bindings, coq.NewAnon(coq.LoopContinue))
-	}
-	body := coq.BlockExpr{bindings}
+	body := ctx.blockStmt(s.Body, ExprValLoop)
 	return coq.ForLoopExpr{
 		Init: init,
 		Cond: cond,
@@ -1312,7 +1315,7 @@ func (ctx Ctx) mapRangeStmt(s *ast.RangeStmt) coq.Expr {
 		KeyIdent:   key,
 		ValueIdent: val,
 		Map:        ctx.expr(s.X),
-		Body:       ctx.blockStmt(s.Body, nil),
+		Body:       ctx.blockStmt(s.Body, ExprValLocal),
 	}
 }
 
@@ -1332,7 +1335,6 @@ func (ctx Ctx) identBinder(id *ast.Ident) coq.Binder {
 }
 
 func (ctx Ctx) sliceRangeStmt(s *ast.RangeStmt) coq.Expr {
-	var loopVar *string
 	key := getIdentOrNil(s.Key)
 	val := getIdentOrNil(s.Value)
 	if key != nil {
@@ -1340,7 +1342,6 @@ func (ctx Ctx) sliceRangeStmt(s *ast.RangeStmt) coq.Expr {
 			IsPtrWrapped: false,
 			IsMacro:      false,
 		})
-		loopVar = &key.Name
 	}
 	if val != nil {
 		ctx.addDef(val, identInfo{
@@ -1353,7 +1354,7 @@ func (ctx Ctx) sliceRangeStmt(s *ast.RangeStmt) coq.Expr {
 		Val:   ctx.identBinder(val),
 		Slice: ctx.expr(s.X),
 		Ty:    ctx.coqTypeOfType(s.X, sliceElem(ctx.typeOf(s.X))),
-		Body:  ctx.blockStmt(s.Body, loopVar),
+		Body:  ctx.blockStmt(s.Body, ExprValLocal),
 	}
 }
 
@@ -1585,7 +1586,7 @@ func (ctx Ctx) assignFromTo(s ast.Node,
 	return coq.Binding{}
 }
 
-func (ctx Ctx) assignStmt(s *ast.AssignStmt, c *cursor, loopVar *string) coq.Binding {
+func (ctx Ctx) assignStmt(s *ast.AssignStmt) coq.Binding {
 	if s.Tok == token.DEFINE {
 		return ctx.defineStmt(s)
 	}
@@ -1610,7 +1611,7 @@ func (ctx Ctx) assignStmt(s *ast.AssignStmt, c *cursor, loopVar *string) coq.Bin
 	return ctx.assignFromTo(s, lhs, rhs)
 }
 
-func (ctx Ctx) incDecStmt(stmt *ast.IncDecStmt, loopVar *string) coq.Binding {
+func (ctx Ctx) incDecStmt(stmt *ast.IncDecStmt) coq.Binding {
 	ident := getIdentOrNil(stmt.X)
 	if ident == nil {
 		ctx.todo(stmt, "cannot inc/dec non-var")
@@ -1638,7 +1639,7 @@ func (ctx Ctx) spawnExpr(thread ast.Expr) coq.SpawnExpr {
 			"only function literal spawns are supported")
 		return coq.SpawnExpr{}
 	}
-	return coq.SpawnExpr{Body: ctx.blockStmt(f.Body, nil)}
+	return coq.SpawnExpr{Body: ctx.blockStmt(f.Body, ExprValLocal)}
 }
 
 func (ctx Ctx) branchStmt(s *ast.BranchStmt) coq.Expr {
@@ -1660,43 +1661,55 @@ func (ctx Ctx) goStmt(e *ast.GoStmt) coq.Expr {
 	return ctx.spawnExpr(e.Call.Fun)
 }
 
-func (ctx Ctx) stmt(s ast.Stmt, c *cursor, loopVar *string) coq.Binding {
-	switch s := s.(type) {
-	case *ast.ReturnStmt:
-		if c.HasNext() {
-			ctx.unsupported(c.Next(), "statement following return")
-			return coq.Binding{}
+// This function also returns wether the expression has been "finalized",
+// which means the usage has been taken care of. If it is not finalized,
+// the caller is responsible for adding a trailing "return unit"/"continue".
+func (ctx Ctx) stmtInBlock(s ast.Stmt, usage ExprValUsage) (coq.Binding, bool) {
+	// First the case where the statement matches the usage, i.e. the necessary
+	// control effect is actually available.
+	switch usage {
+	case ExprValReturned:
+		s, ok := s.(*ast.ReturnStmt)
+		if ok {
+			return coq.NewAnon(ctx.returnExpr(s.Results)), true
 		}
-		if loopVar != nil {
-			ctx.futureWork(s, "return in loop (use break)")
-			return coq.Binding{}
+	case ExprValLoop:
+		s, ok := s.(*ast.BranchStmt)
+		if ok {
+			return coq.NewAnon(ctx.branchStmt(s)), true
 		}
-		return coq.NewAnon(ctx.returnExpr(s.Results))
+	}
+	// Some statements can handle the usage themselves, and they make sure to finalize it, too
+	switch s := s.(type) {
+	case *ast.IfStmt:
+		return ctx.ifStmt(s, []ast.Stmt{}, usage), true
+	case *ast.BlockStmt:
+		return coq.NewAnon(ctx.blockStmt(s, usage)), true
+	}
+	// For everything else, we generate the statement and possibly tell the caller
+	// that this is not yet finalized.
+	var binding coq.Binding = coq.Binding{}
+	switch s := s.(type) {
+	case *ast.ReturnStmt:
+		ctx.futureWork(s, "return in unsupported position")
 	case *ast.BranchStmt:
-		if loopVar == nil {
-			ctx.unsupported(s, "branching outside of a loop")
-		}
-		return coq.NewAnon(ctx.branchStmt(s))
+		ctx.futureWork(s, "break/continue in unsupported position")
 	case *ast.GoStmt:
-		return coq.NewAnon(ctx.goStmt(s))
+		binding = coq.NewAnon(ctx.goStmt(s))
 	case *ast.ExprStmt:
-		return coq.NewAnon(ctx.expr(s.X))
+		binding = coq.NewAnon(ctx.expr(s.X))
 	case *ast.AssignStmt:
-		return ctx.assignStmt(s, c, loopVar)
+		binding = ctx.assignStmt(s)
 	case *ast.DeclStmt:
-		return ctx.varDeclStmt(s)
+		binding = ctx.varDeclStmt(s)
 	case *ast.IncDecStmt:
-		return ctx.incDecStmt(s, loopVar)
-	case *ast.BlockStmt:
-		return coq.NewAnon(ctx.blockStmt(s, loopVar))
-	case *ast.IfStmt:
-		return ctx.ifStmt(s, c, loopVar)
+		binding = ctx.incDecStmt(s)
 	case *ast.ForStmt:
 		// note that this might be a nested loop,
 		// in which case the loop var gets replaced by the inner loop.
-		return coq.NewAnon(ctx.forStmt(s))
+		binding = coq.NewAnon(ctx.forStmt(s))
 	case *ast.RangeStmt:
-		return coq.NewAnon(ctx.rangeStmt(s))
+		binding = coq.NewAnon(ctx.rangeStmt(s))
 	case *ast.SwitchStmt:
 		ctx.todo(s, "check for switch statement")
 	case *ast.TypeSwitchStmt:
@@ -1704,7 +1717,27 @@ func (ctx Ctx) stmt(s ast.Stmt, c *cursor, loopVar *string) coq.Binding {
 	default:
 		ctx.unsupported(s, "statement")
 	}
-	return coq.Binding{}
+	switch usage {
+	case ExprValLocal:
+		// Nothing to finalize.
+		return binding, true
+	default:
+		// Finalization required
+		return binding, false
+	}
+}
+
+// Translate a single statement and finalize it if needed
+func (ctx Ctx) stmt(s ast.Stmt, usage ExprValUsage) coq.Binding {
+	// stmts takes care of finalization...
+	block := ctx.stmts([]ast.Stmt{s}, usage)
+	// ...but let's prettify the result while converting to a Binding.
+	// FIXME(RJ): not "prettifying" (always using NewAnon) actually breaks translation. Hu?
+	if len(block.Bindings) == 1 {
+		return block.Bindings[0]
+	} else {
+		return coq.NewAnon(block)
+	}
 }
 
 func (ctx Ctx) returnExpr(es []ast.Expr) coq.Expr {
@@ -1766,7 +1799,7 @@ func (ctx Ctx) funcDecl(d *ast.FuncDecl) coq.FuncDecl {
 	}
 	fd.Args = append(fd.Args, ctx.paramList(d.Type.Params)...)
 	fd.ReturnType = ctx.returnType(d.Type.Results)
-	fd.Body = ctx.blockStmt(d.Body, nil)
+	fd.Body = ctx.blockStmt(d.Body, ExprValReturned)
 	return fd
 }
 
diff --git a/internal/examples/append_log/append_log.gold.v b/internal/examples/append_log/append_log.gold.v
index f2ad2085..496a8d10 100644
--- a/internal/examples/append_log/append_log.gold.v
+++ b/internal/examples/append_log/append_log.gold.v
@@ -28,7 +28,8 @@ Hint Resolve Log__mkHdr_t : types.
 
 Definition Log__writeHdr: val :=
   rec: "Log__writeHdr" "log" :=
-    disk.Write #0 (Log__mkHdr "log").
+    disk.Write #0 (Log__mkHdr "log");;
+    #().
 Theorem Log__writeHdr_t: ⊢ Log__writeHdr : (struct.ptrT Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__writeHdr_t : types.
@@ -92,7 +93,8 @@ Hint Resolve Log__Get_t : types.
 Definition writeAll: val :=
   rec: "writeAll" "bks" "off" :=
     ForSlice (slice.T byteT) "i" "bk" "bks"
-      (disk.Write ("off" + "i") "bk").
+      (disk.Write ("off" + "i") "bk");;
+    #().
 Theorem writeAll_t: ⊢ writeAll : (slice.T disk.blockT -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve writeAll_t : types.
@@ -124,7 +126,8 @@ Hint Resolve Log__Append_t : types.
 Definition Log__reset: val :=
   rec: "Log__reset" "log" :=
     struct.storeF Log "sz" "log" #0;;
-    Log__writeHdr "log".
+    Log__writeHdr "log";;
+    #().
 Theorem Log__reset_t: ⊢ Log__reset : (struct.ptrT Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__reset_t : types.
@@ -133,7 +136,8 @@ Definition Log__Reset: val :=
   rec: "Log__Reset" "log" :=
     lock.acquire (struct.loadF Log "m" "log");;
     Log__reset "log";;
-    lock.release (struct.loadF Log "m" "log").
+    lock.release (struct.loadF Log "m" "log");;
+    #().
 Theorem Log__Reset_t: ⊢ Log__Reset : (struct.ptrT Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Reset_t : types.
diff --git a/internal/examples/logging2/logging2.gold.v b/internal/examples/logging2/logging2.gold.v
index b8c8239b..2c3f3fb6 100644
--- a/internal/examples/logging2/logging2.gold.v
+++ b/internal/examples/logging2/logging2.gold.v
@@ -34,7 +34,8 @@ Definition Log__writeHdr: val :=
   rec: "Log__writeHdr" "log" "len" :=
     let: "hdr" := NewSlice byteT #4096 in
     UInt64Put "hdr" "len";;
-    disk.Write LOGCOMMIT "hdr".
+    disk.Write LOGCOMMIT "hdr";;
+    #().
 Theorem Log__writeHdr_t: ⊢ Log__writeHdr : (struct.t Log -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__writeHdr_t : types.
@@ -95,7 +96,8 @@ Definition Log__memWrite: val :=
     let: "i" := ref_to uint64T #0 in
     (for: (λ: <>, ![uint64T] "i" < "n"); (λ: <>, "i" <-[uint64T] ![uint64T] "i" + #1) := λ: <>,
       struct.get Log "memLog" "log" <-[slice.T (slice.T byteT)] SliceAppend (slice.T byteT) (![slice.T (slice.T byteT)] (struct.get Log "memLog" "log")) (SliceGet (slice.T byteT) "l" (![uint64T] "i"));;
-      Continue).
+      Continue);;
+    #().
 Theorem Log__memWrite_t: ⊢ Log__memWrite : (struct.t Log -> slice.T disk.blockT -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__memWrite_t : types.
@@ -136,7 +138,8 @@ Definition Log__diskAppendWait: val :=
       let: "logtxn" := Log__readLogTxnNxt "log" in
       (if: "txn" < "logtxn"
       then Break
-      else Continue)).
+      else Continue));;
+    #().
 Theorem Log__diskAppendWait_t: ⊢ Log__diskAppendWait : (struct.t Log -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__diskAppendWait_t : types.
@@ -145,9 +148,7 @@ Definition Log__Append: val :=
   rec: "Log__Append" "log" "l" :=
     let: ("ok", "txn") := Log__memAppend "log" "l" in
     (if: "ok"
-    then
-      Log__diskAppendWait "log" "txn";;
-      #()
+    then Log__diskAppendWait "log" "txn"
     else #());;
     "ok".
 Theorem Log__Append_t: ⊢ Log__Append : (struct.t Log -> slice.T disk.blockT -> boolT).
@@ -161,7 +162,8 @@ Definition Log__writeBlocks: val :=
     (for: (λ: <>, ![uint64T] "i" < "n"); (λ: <>, "i" <-[uint64T] ![uint64T] "i" + #1) := λ: <>,
       let: "bk" := SliceGet (slice.T byteT) "l" (![uint64T] "i") in
       disk.Write ("pos" + ![uint64T] "i") "bk";;
-      Continue).
+      Continue);;
+    #().
 Theorem Log__writeBlocks_t: ⊢ Log__writeBlocks : (struct.t Log -> slice.T disk.blockT -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__writeBlocks_t : types.
@@ -179,7 +181,8 @@ Definition Log__diskAppend: val :=
     Log__writeBlocks "log" "blks" "disklen";;
     Log__writeHdr "log" "memlen";;
     struct.get Log "logTxnNxt" "log" <-[uint64T] "memnxt";;
-    lock.release (struct.get Log "logLock" "log").
+    lock.release (struct.get Log "logLock" "log");;
+    #().
 Theorem Log__diskAppend_t: ⊢ Log__diskAppend : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__diskAppend_t : types.
@@ -189,7 +192,8 @@ Definition Log__Logger: val :=
     Skip;;
     (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
       Log__diskAppend "log";;
-      Continue).
+      Continue);;
+    #().
 Theorem Log__Logger_t: ⊢ Log__Logger : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Logger_t : types.
@@ -218,9 +222,7 @@ Definition Txn__Write: val :=
     let: "ret" := ref_to boolT #true in
     let: (<>, "ok") := MapGet (struct.get Txn "blks" "txn") "addr" in
     (if: "ok"
-    then
-      MapInsert (struct.get Txn "blks" "txn") "addr" (![slice.T byteT] "blk");;
-      #()
+    then MapInsert (struct.get Txn "blks" "txn") "addr" (![slice.T byteT] "blk")
     else #());;
     (if: ~ "ok"
     then
diff --git a/internal/examples/semantics/semantics.gold.v b/internal/examples/semantics/semantics.gold.v
index 82b849f2..93ab9a70 100644
--- a/internal/examples/semantics/semantics.gold.v
+++ b/internal/examples/semantics/semantics.gold.v
@@ -16,7 +16,8 @@ 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.
@@ -631,7 +632,8 @@ Definition LoopStruct__forLoopWait: val :=
       then Break
       else
         struct.get LoopStruct "loopNext" "ls" <-[uint64T] ![uint64T] (struct.get LoopStruct "loopNext" "ls") + #1;;
-        Continue)).
+        Continue));;
+    #().
 Theorem LoopStruct__forLoopWait_t: ⊢ LoopStruct__forLoopWait : (struct.t LoopStruct -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve LoopStruct__forLoopWait_t : types.
@@ -684,7 +686,9 @@ Definition testBreakFromLoopNoContinue: val :=
       then
         "i" <-[uint64T] ![uint64T] "i" + #1;;
         Break
-      else "i" <-[uint64T] ![uint64T] "i" + #2));;
+      else
+        "i" <-[uint64T] ![uint64T] "i" + #2;;
+        Continue));;
     (![uint64T] "i" = #1).
 Theorem testBreakFromLoopNoContinue_t: ⊢ testBreakFromLoopNoContinue : (unitT -> boolT).
 Proof. typecheck. Qed.
@@ -701,7 +705,8 @@ Definition failing_testBreakFromLoopNoContinueDouble: val :=
         Break
       else
         "i" <-[uint64T] ![uint64T] "i" + #2;;
-        "i" <-[uint64T] ![uint64T] "i" + #2));;
+        "i" <-[uint64T] ![uint64T] "i" + #2;;
+        Continue));;
     (![uint64T] "i" = #4).
 Theorem failing_testBreakFromLoopNoContinueDouble_t: ⊢ failing_testBreakFromLoopNoContinueDouble : (unitT -> boolT).
 Proof. typecheck. Qed.
@@ -1100,9 +1105,7 @@ Definition testOrCompare: val :=
   rec: "testOrCompare" <> :=
     let: "ok" := ref_to boolT #true in
     (if: ~ (#3 > #4) || (#4 > #3)
-    then
-      "ok" <-[boolT] #false;;
-      #()
+    then "ok" <-[boolT] #false
     else #());;
     (if: (#4 < #3) || (#2 > #3)
     then "ok" <-[boolT] #false
@@ -1116,9 +1119,7 @@ Definition testAndCompare: val :=
   rec: "testAndCompare" <> :=
     let: "ok" := ref_to boolT #true in
     (if: (#3 > #4) && (#4 > #3)
-    then
-      "ok" <-[boolT] #false;;
-      #()
+    then "ok" <-[boolT] #false
     else #());;
     (if: (#4 > #3) || (#2 < #3)
     then #()
@@ -1248,7 +1249,8 @@ Definition ArrayEditor__Advance: val :=
     SliceSet uint64T "arr" #0 (SliceGet uint64T "arr" #0 + #1);;
     SliceSet uint64T (struct.loadF ArrayEditor "s" "ae") #0 (struct.loadF ArrayEditor "next_val" "ae");;
     struct.storeF ArrayEditor "next_val" "ae" "next";;
-    struct.storeF ArrayEditor "s" "ae" (SliceSkip uint64T (struct.loadF ArrayEditor "s" "ae") #1).
+    struct.storeF ArrayEditor "s" "ae" (SliceSkip uint64T (struct.loadF ArrayEditor "s" "ae") #1);;
+    #().
 Theorem ArrayEditor__Advance_t: ⊢ ArrayEditor__Advance : (struct.ptrT ArrayEditor -> slice.T uint64T -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve ArrayEditor__Advance_t : types.
@@ -1360,14 +1362,16 @@ Definition Foo := struct.decl [
 Definition Bar__mutate: val :=
   rec: "Bar__mutate" "bar" :=
     struct.storeF Bar "a" "bar" #2;;
-    struct.storeF Bar "b" "bar" #3.
+    struct.storeF Bar "b" "bar" #3;;
+    #().
 Theorem Bar__mutate_t: ⊢ Bar__mutate : (struct.ptrT Bar -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Bar__mutate_t : types.
 
 Definition Foo__mutateBar: val :=
   rec: "Foo__mutateBar" "foo" :=
-    Bar__mutate (struct.loadF Foo "bar" "foo").
+    Bar__mutate (struct.loadF Foo "bar" "foo");;
+    #().
 Theorem Foo__mutateBar_t: ⊢ Foo__mutateBar : (struct.ptrT Foo -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Foo__mutateBar_t : types.
@@ -1436,14 +1440,16 @@ Hint Resolve S__readBVal_t : types.
 
 Definition S__updateBValX: val :=
   rec: "S__updateBValX" "s" "i" :=
-    struct.storeF TwoInts "x" (struct.fieldRef S "b" "s") "i".
+    struct.storeF TwoInts "x" (struct.fieldRef S "b" "s") "i";;
+    #().
 Theorem S__updateBValX_t: ⊢ S__updateBValX : (struct.ptrT S -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve S__updateBValX_t : types.
 
 Definition S__negateC: val :=
   rec: "S__negateC" "s" :=
-    struct.storeF S "c" "s" (~ (struct.loadF S "c" "s")).
+    struct.storeF S "c" "s" (~ (struct.loadF S "c" "s"));;
+    #().
 Theorem S__negateC_t: ⊢ S__negateC : (struct.ptrT S -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve S__negateC_t : types.
@@ -1649,9 +1655,7 @@ Definition New: val :=
     let: "d" := disk.Get #() in
     let: "diskSize" := disk.Size #() in
     (if: "diskSize" ≤ logLength
-    then
-      Panic ("disk is too small to host log");;
-      #()
+    then Panic ("disk is too small to host log")
     else #());;
     let: "cache" := NewMap disk.blockT in
     let: "header" := intToBlock #0 in
@@ -1671,14 +1675,16 @@ Hint Resolve New_t : types.
 
 Definition Log__lock: val :=
   rec: "Log__lock" "l" :=
-    lock.acquire (struct.get Log "l" "l").
+    lock.acquire (struct.get Log "l" "l");;
+    #().
 Theorem Log__lock_t: ⊢ Log__lock : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__lock_t : types.
 
 Definition Log__unlock: val :=
   rec: "Log__unlock" "l" :=
-    lock.release (struct.get Log "l" "l").
+    lock.release (struct.get Log "l" "l");;
+    #().
 Theorem Log__unlock_t: ⊢ Log__unlock : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__unlock_t : types.
@@ -1734,9 +1740,7 @@ Definition Log__Write: val :=
     Log__lock "l";;
     let: "length" := ![uint64T] (struct.get Log "length" "l") in
     (if: "length" ≥ MaxTxnWrites
-    then
-      Panic ("transaction is at capacity");;
-      #()
+    then Panic ("transaction is at capacity")
     else #());;
     let: "aBlock" := intToBlock "a" in
     let: "nextAddr" := #1 + #2 * "length" in
@@ -1744,7 +1748,8 @@ Definition Log__Write: val :=
     disk.Write ("nextAddr" + #1) "v";;
     MapInsert (struct.get Log "cache" "l") "a" "v";;
     struct.get Log "length" "l" <-[uint64T] "length" + #1;;
-    Log__unlock "l".
+    Log__unlock "l";;
+    #().
 Theorem Log__Write_t: ⊢ Log__Write : (struct.t Log -> uint64T -> disk.blockT -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Write_t : types.
@@ -1756,7 +1761,8 @@ Definition Log__Commit: val :=
     let: "length" := ![uint64T] (struct.get Log "length" "l") in
     Log__unlock "l";;
     let: "header" := intToBlock "length" in
-    disk.Write #0 "header".
+    disk.Write #0 "header";;
+    #().
 Theorem Log__Commit_t: ⊢ Log__Commit : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Commit_t : types.
@@ -1783,7 +1789,8 @@ Definition applyLog: val :=
         disk.Write (logLength + "a") "v";;
         "i" <-[uint64T] ![uint64T] "i" + #1;;
         Continue
-      else Break)).
+      else Break));;
+    #().
 Theorem applyLog_t: ⊢ applyLog : (disk.Disk -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve applyLog_t : types.
@@ -1791,7 +1798,8 @@ Hint Resolve applyLog_t : types.
 Definition clearLog: val :=
   rec: "clearLog" "d" :=
     let: "header" := intToBlock #0 in
-    disk.Write #0 "header".
+    disk.Write #0 "header";;
+    #().
 Theorem clearLog_t: ⊢ clearLog : (disk.Disk -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve clearLog_t : types.
@@ -1806,7 +1814,8 @@ Definition Log__Apply: val :=
     applyLog (struct.get Log "d" "l") "length";;
     clearLog (struct.get Log "d" "l");;
     struct.get Log "length" "l" <-[uint64T] #0;;
-    Log__unlock "l".
+    Log__unlock "l";;
+    #().
 Theorem Log__Apply_t: ⊢ Log__Apply : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Apply_t : types.
@@ -1839,9 +1848,7 @@ Definition disabled_testWal: val :=
     let: "ok" := ref_to boolT #true in
     let: "lg" := New #() in
     (if: Log__BeginTxn "lg"
-    then
-      Log__Write "lg" #2 (intToBlock #11);;
-      #()
+    then Log__Write "lg" #2 (intToBlock #11)
     else #());;
     "ok" <-[boolT] (![boolT] "ok") && (blockToInt (Log__Read "lg" #2) = #11);;
     "ok" <-[boolT] (![boolT] "ok") && (blockToInt (disk.Read #0) = #0);;
diff --git a/internal/examples/simpledb/simpledb.gold.v b/internal/examples/simpledb/simpledb.gold.v
index cac95eb6..eb6a65e3 100644
--- a/internal/examples/simpledb/simpledb.gold.v
+++ b/internal/examples/simpledb/simpledb.gold.v
@@ -114,7 +114,8 @@ Definition readTableIndex: val :=
             "offset" ::= struct.get lazyFileBuf "offset" (![struct.t lazyFileBuf] "buf");
             "next" ::= "newBuf"
           ];;
-          Continue))).
+          Continue)));;
+    #().
 
 (* RecoverTable restores a table from disk on startup. *)
 Definition RecoverTable: val :=
@@ -130,7 +131,8 @@ Definition RecoverTable: val :=
 (* CloseTable frees up the fd held by a table. *)
 Definition CloseTable: val :=
   rec: "CloseTable" "t" :=
-    FS.close (struct.get Table "File" "t").
+    FS.close (struct.get Table "File" "t");;
+    #().
 
 Definition readValue: val :=
   rec: "readValue" "f" "off" :=
@@ -174,18 +176,21 @@ Definition bufFlush: val :=
     then #()
     else
       FS.append (struct.get bufFile "file" "f") "buf";;
-      struct.get bufFile "buf" "f" <-[slice.T byteT] slice.nil).
+      struct.get bufFile "buf" "f" <-[slice.T byteT] slice.nil;;
+      #()).
 
 Definition bufAppend: val :=
   rec: "bufAppend" "f" "p" :=
     let: "buf" := ![slice.T byteT] (struct.get bufFile "buf" "f") in
     let: "buf2" := SliceAppendSlice byteT "buf" "p" in
-    struct.get bufFile "buf" "f" <-[slice.T byteT] "buf2".
+    struct.get bufFile "buf" "f" <-[slice.T byteT] "buf2";;
+    #().
 
 Definition bufClose: val :=
   rec: "bufClose" "f" :=
     bufFlush "f";;
-    FS.close (struct.get bufFile "file" "f").
+    FS.close (struct.get bufFile "file" "f");;
+    #().
 
 Definition tableWriter := struct.decl [
   "index" :: mapT uint64T;
@@ -211,7 +216,8 @@ Definition tableWriterAppend: val :=
   rec: "tableWriterAppend" "w" "p" :=
     bufAppend (struct.get tableWriter "file" "w") "p";;
     let: "off" := ![uint64T] (struct.get tableWriter "offset" "w") in
-    struct.get tableWriter "offset" "w" <-[uint64T] "off" + slice.len "p".
+    struct.get tableWriter "offset" "w" <-[uint64T] "off" + slice.len "p";;
+    #().
 
 Definition tableWriterClose: val :=
   rec: "tableWriterClose" "w" :=
@@ -244,7 +250,8 @@ Definition tablePut: val :=
     let: "tmp3" := EncodeSlice "v" "tmp2" in
     let: "off" := ![uint64T] (struct.get tableWriter "offset" "w") in
     MapInsert (struct.get tableWriter "index" "w") "k" ("off" + slice.len "tmp2");;
-    tableWriterAppend "w" "tmp3".
+    tableWriterAppend "w" "tmp3";;
+    #().
 
 (* Database is a handle to an open database. *)
 Definition Database := struct.decl [
@@ -329,7 +336,8 @@ Definition Write: val :=
     lock.acquire (struct.get Database "bufferL" "db");;
     let: "buf" := ![mapT (slice.T byteT)] (struct.get Database "wbuffer" "db") in
     MapInsert "buf" "k" "v";;
-    lock.release (struct.get Database "bufferL" "db").
+    lock.release (struct.get Database "bufferL" "db");;
+    #().
 
 Definition freshTable: val :=
   rec: "freshTable" "p" :=
@@ -343,7 +351,8 @@ Definition freshTable: val :=
 Definition tablePutBuffer: val :=
   rec: "tablePutBuffer" "w" "buf" :=
     MapIter "buf" (λ: "k" "v",
-      tablePut "w" "k" "v").
+      tablePut "w" "k" "v");;
+    #().
 
 (* add all of table t to the table w being created; skip any keys in the (read)
    buffer b since those writes overwrite old ones *)
@@ -359,9 +368,7 @@ Definition tablePutOldTable: val :=
       then
         let: (<>, "ok") := MapGet "b" (struct.get Entry "Key" "e") in
         (if: ~ "ok"
-        then
-          tablePut "w" (struct.get Entry "Key" "e") (struct.get Entry "Value" "e");;
-          #()
+        then tablePut "w" (struct.get Entry "Key" "e") (struct.get Entry "Value" "e")
         else #());;
         "buf" <-[struct.t lazyFileBuf] struct.mk lazyFileBuf [
           "offset" ::= struct.get lazyFileBuf "offset" (![struct.t lazyFileBuf] "buf") + "l";
@@ -378,7 +385,8 @@ Definition tablePutOldTable: val :=
             "offset" ::= struct.get lazyFileBuf "offset" (![struct.t lazyFileBuf] "buf");
             "next" ::= "newBuf"
           ];;
-          Continue))).
+          Continue)));;
+    #().
 
 (* Build a new shadow table that incorporates the current table and a
    (write) buffer wbuf.
@@ -421,7 +429,8 @@ Definition Compact: val :=
     CloseTable "oldTable";;
     FS.delete #(str"db") "oldTableName";;
     lock.release (struct.get Database "tableL" "db");;
-    lock.release (struct.get Database "compactionL" "db").
+    lock.release (struct.get Database "compactionL" "db");;
+    #().
 
 Definition recoverManifest: val :=
   rec: "recoverManifest" <> :=
@@ -439,7 +448,9 @@ Definition deleteOtherFile: val :=
     else
       (if: ("name" = #(str"manifest"))
       then #()
-      else FS.delete #(str"db") "name")).
+      else
+        FS.delete #(str"db") "name";;
+        #())).
 
 Definition deleteOtherFiles: val :=
   rec: "deleteOtherFiles" "tableName" :=
@@ -453,7 +464,8 @@ Definition deleteOtherFiles: val :=
         let: "name" := SliceGet stringT "files" (![uint64T] "i") in
         deleteOtherFile "name" "tableName";;
         "i" <-[uint64T] ![uint64T] "i" + #1;;
-        Continue)).
+        Continue));;
+    #().
 
 (* Recover restores a previously created database after a crash or shutdown. *)
 Definition Recover: val :=
@@ -491,7 +503,8 @@ Definition Shutdown: val :=
     let: "t" := struct.load Table (struct.get Database "table" "db") in
     CloseTable "t";;
     lock.release (struct.get Database "compactionL" "db");;
-    lock.release (struct.get Database "bufferL" "db").
+    lock.release (struct.get Database "bufferL" "db");;
+    #().
 
 (* Close closes an open database cleanly, flushing any in-memory writes.
 
@@ -499,6 +512,7 @@ Definition Shutdown: val :=
 Definition Close: val :=
   rec: "Close" "db" :=
     Compact "db";;
-    Shutdown "db".
+    Shutdown "db";;
+    #().
 
 End code.
diff --git a/internal/examples/unittest/loops.go b/internal/examples/unittest/loops.go
index 88348042..1b354723 100644
--- a/internal/examples/unittest/loops.go
+++ b/internal/examples/unittest/loops.go
@@ -50,7 +50,23 @@ func ImplicitLoopContinue() {
 	for i := uint64(0); ; {
 		if i < 4 {
 			i = 0
-			// note that continue here is not correctly supported
+		}
+	}
+}
+
+func ImplicitLoopContinue2() {
+	for i := uint64(0); ; {
+		if i < 4 {
+			i = 0
+			continue
+		}
+	}
+}
+
+func ImplicitLoopContinueAfterIfBreak(i uint64) {
+	for {
+		if i > 0 {
+			break
 		}
 	}
 }
diff --git a/internal/examples/unittest/trailing_call.go b/internal/examples/unittest/trailing_call.go
new file mode 100644
index 00000000..93f3f91a
--- /dev/null
+++ b/internal/examples/unittest/trailing_call.go
@@ -0,0 +1,9 @@
+package unittest
+
+func mkInt() uint64 {
+	return 42
+}
+
+func mkNothing() {
+	mkInt()
+}
diff --git a/internal/examples/unittest/unittest.gold.v b/internal/examples/unittest/unittest.gold.v
index 33967101..ad4bcf28 100644
--- a/internal/examples/unittest/unittest.gold.v
+++ b/internal/examples/unittest/unittest.gold.v
@@ -39,7 +39,8 @@ Definition condvarWrapping: val :=
     "mu" <-[lockRefT] lock.new #();;
     let: "cond1" := lock.newCond (![lockRefT] "mu") in
     "mu" <-[lockRefT] lock.new #();;
-    lock.condWait "cond1".
+    lock.condWait "cond1";;
+    #().
 
 (* const.go *)
 
@@ -155,7 +156,8 @@ Definition useSlice: val :=
   rec: "useSlice" <> :=
     let: "s" := NewSlice byteT #1 in
     let: "s1" := SliceAppendSlice byteT "s" "s" in
-    atomicCreateStub #(str"dir") #(str"file") "s1".
+    atomicCreateStub #(str"dir") #(str"file") "s1";;
+    #().
 
 Definition useSliceIndexing: val :=
   rec: "useSliceIndexing" <> :=
@@ -171,14 +173,17 @@ Definition useMap: val :=
     let: ("x", "ok") := MapGet "m" #2 in
     (if: "ok"
     then #()
-    else MapInsert "m" #3 "x").
+    else
+      MapInsert "m" #3 "x";;
+      #()).
 
 Definition usePtr: val :=
   rec: "usePtr" <> :=
     let: "p" := ref (zero_val uint64T) in
     "p" <-[uint64T] #1;;
     let: "x" := ![uint64T] "p" in
-    "p" <-[uint64T] "x".
+    "p" <-[uint64T] "x";;
+    #().
 
 Definition iterMapKeysAndValues: val :=
   rec: "iterMapKeysAndValues" "m" :=
@@ -215,7 +220,8 @@ Definition diskWrapper := struct.decl [
 Definition diskArgument: val :=
   rec: "diskArgument" "d" :=
     let: "b" := disk.Read #0 in
-    disk.Write #1 "b".
+    disk.Write #1 "b";;
+    #().
 
 (* empty_functions.go *)
 
@@ -241,11 +247,13 @@ Definition Enc__consume: val :=
 
 Definition Enc__UInt64: val :=
   rec: "Enc__UInt64" "e" "x" :=
-    UInt64Put (Enc__consume "e" #8) "x".
+    UInt64Put (Enc__consume "e" #8) "x";;
+    #().
 
 Definition Enc__UInt32: val :=
   rec: "Enc__UInt32" "e" "x" :=
-    UInt32Put (Enc__consume "e" #4) "x".
+    UInt32Put (Enc__consume "e" #4) "x";;
+    #().
 
 Definition Dec := struct.decl [
   "p" :: slice.T byteT
@@ -320,7 +328,8 @@ Definition useLocks: val :=
   rec: "useLocks" <> :=
     let: "m" := lock.new #() in
     lock.acquire "m";;
-    lock.release "m".
+    lock.release "m";;
+    #().
 
 Definition useCondVar: val :=
   rec: "useCondVar" <> :=
@@ -329,7 +338,8 @@ Definition useCondVar: val :=
     lock.acquire "m";;
     lock.condSignal "c";;
     lock.condWait "c";;
-    lock.release "m".
+    lock.release "m";;
+    #().
 
 Definition hasCondVar := struct.decl [
   "cond" :: condvarRefT
@@ -377,15 +387,14 @@ Definition conditionalInLoop: val :=
     let: "i" := ref_to uint64T #0 in
     (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
       (if: ![uint64T] "i" < #3
-      then
-        DoSomething (#(str"i is small"));;
-        #()
+      then DoSomething (#(str"i is small"))
       else #());;
       (if: ![uint64T] "i" > #5
       then Break
       else
         "i" <-[uint64T] ![uint64T] "i" + #1;;
-        Continue)).
+        Continue));;
+    #().
 
 Definition conditionalInLoopElse: val :=
   rec: "conditionalInLoopElse" <> :=
@@ -395,7 +404,8 @@ Definition conditionalInLoopElse: val :=
       then Break
       else
         "i" <-[uint64T] ![uint64T] "i" + #1;;
-        Continue)).
+        Continue));;
+    #().
 
 Definition ImplicitLoopContinue: val :=
   rec: "ImplicitLoopContinue" <> :=
@@ -404,7 +414,28 @@ Definition ImplicitLoopContinue: val :=
       (if: ![uint64T] "i" < #4
       then "i" <-[uint64T] #0
       else #());;
-      Continue).
+      Continue);;
+    #().
+
+Definition ImplicitLoopContinue2: val :=
+  rec: "ImplicitLoopContinue2" <> :=
+    let: "i" := ref_to uint64T #0 in
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      (if: ![uint64T] "i" < #4
+      then
+        "i" <-[uint64T] #0;;
+        Continue
+      else Continue));;
+    #().
+
+Definition ImplicitLoopContinueAfterIfBreak: val :=
+  rec: "ImplicitLoopContinueAfterIfBreak" "i" :=
+    Skip;;
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      (if: "i" > #0
+      then Break
+      else Continue));;
+    #().
 
 Definition nestedLoops: val :=
   rec: "nestedLoops" <> :=
@@ -418,7 +449,8 @@ Definition nestedLoops: val :=
           "j" <-[uint64T] ![uint64T] "j" + #1;;
           Continue));;
       "i" <-[uint64T] ![uint64T] "i" + #1;;
-      Continue).
+      Continue);;
+    #().
 
 Definition nestedGoStyleLoops: val :=
   rec: "nestedGoStyleLoops" <> :=
@@ -429,7 +461,8 @@ Definition nestedGoStyleLoops: val :=
         (if: #true
         then Break
         else Continue));;
-      Continue).
+      Continue);;
+    #().
 
 Definition sumSlice: val :=
   rec: "sumSlice" "xs" :=
@@ -444,19 +477,22 @@ Definition breakFromLoop: val :=
     (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
       (if: #true
       then Break
-      else Continue)).
+      else Continue));;
+    #().
 
 (* maps.go *)
 
 Definition clearMap: val :=
   rec: "clearMap" "m" :=
-    MapClear "m".
+    MapClear "m";;
+    #().
 
 Definition IterateMapKeys: val :=
   rec: "IterateMapKeys" "m" "sum" :=
     MapIter "m" (λ: "k" <>,
       let: "oldSum" := ![uint64T] "sum" in
-      "sum" <-[uint64T] "oldSum" + "k").
+      "sum" <-[uint64T] "oldSum" + "k");;
+    #().
 
 Definition MapSize: val :=
   rec: "MapSize" "m" :=
@@ -468,7 +504,8 @@ Definition MapWrapper: ty := mapT boolT.
 
 Definition MapTypeAliases: val :=
   rec: "MapTypeAliases" "m1" "m2" :=
-    MapInsert "m1" #4 (Fst (MapGet "m2" #0)).
+    MapInsert "m1" #4 (Fst (MapGet "m2" #0));;
+    #().
 
 (* multiple.go *)
 
@@ -490,12 +527,14 @@ Definition multipleVar: val :=
 Definition AssignNilSlice: val :=
   rec: "AssignNilSlice" <> :=
     let: "s" := NewSlice (slice.T byteT) #4 in
-    SliceSet (slice.T byteT) "s" #2 slice.nil.
+    SliceSet (slice.T byteT) "s" #2 slice.nil;;
+    #().
 
 Definition AssignNilPointer: val :=
   rec: "AssignNilPointer" <> :=
     let: "s" := NewSlice (refT uint64T) #4 in
-    SliceSet (refT uint64T) "s" #2 slice.nil.
+    SliceSet (refT uint64T) "s" #2 slice.nil;;
+    #().
 
 Definition CompareSliceToNil: val :=
   rec: "CompareSliceToNil" <> :=
@@ -549,7 +588,8 @@ Definition AssignOps: val :=
     "x" <-[uint64T] ![uint64T] "x" + #3;;
     "x" <-[uint64T] ![uint64T] "x" - #3;;
     "x" <-[uint64T] ![uint64T] "x" + #1;;
-    "x" <-[uint64T] ![uint64T] "x" - #1.
+    "x" <-[uint64T] ![uint64T] "x" - #1;;
+    #().
 
 (* package.go *)
 
@@ -562,13 +602,15 @@ Definition wrapExternalStruct := struct.decl [
 
 Definition wrapExternalStruct__moveUint64: val :=
   rec: "wrapExternalStruct__moveUint64" "w" :=
-    marshal.Enc__PutInt (struct.get wrapExternalStruct "e" "w") (marshal.Dec__GetInt (struct.get wrapExternalStruct "d" "w")).
+    marshal.Enc__PutInt (struct.get wrapExternalStruct "e" "w") (marshal.Dec__GetInt (struct.get wrapExternalStruct "d" "w"));;
+    #().
 
 (* panic.go *)
 
 Definition PanicAtTheDisco: val :=
   rec: "PanicAtTheDisco" <> :=
-    Panic "disco".
+    Panic "disco";;
+    #().
 
 (* reassign.go *)
 
@@ -590,7 +632,8 @@ Definition ReassignVars: val :=
       "a" ::= "y";
       "b" ::= ![uint64T] "x"
     ];;
-    "x" <-[uint64T] struct.get composite "a" (![struct.t composite] "z").
+    "x" <-[uint64T] struct.get composite "a" (![struct.t composite] "z");;
+    #().
 
 (* replicated_disk.go *)
 
@@ -646,7 +689,8 @@ Definition ReplicatedDiskWrite: val :=
     TwoDiskLock "a";;
     TwoDiskWrite Disk1 "a" "v";;
     TwoDiskWrite Disk2 "a" "v";;
-    TwoDiskUnlock "a".
+    TwoDiskUnlock "a";;
+    #().
 
 Definition ReplicatedDiskRecover: val :=
   rec: "ReplicatedDiskRecover" <> :=
@@ -657,12 +701,11 @@ Definition ReplicatedDiskRecover: val :=
       else
         let: ("v", "ok") := TwoDiskRead Disk1 (![uint64T] "a") in
         (if: "ok"
-        then
-          TwoDiskWrite Disk2 (![uint64T] "a") "v";;
-          #()
+        then TwoDiskWrite Disk2 (![uint64T] "a") "v"
         else #());;
         "a" <-[uint64T] ![uint64T] "a" + #1;;
-        Continue)).
+        Continue));;
+    #().
 
 (* slices.go *)
 
@@ -711,14 +754,13 @@ Definition simpleSpawn: val :=
     Fork (lock.acquire "l";;
           let: "x" := ![uint64T] "v" in
           (if: "x" > #0
-          then
-            Skip #();;
-            #()
+          then Skip #()
           else #());;
           lock.release "l");;
     lock.acquire "l";;
     "v" <-[uint64T] #1;;
-    lock.release "l".
+    lock.release "l";;
+    #().
 
 Definition threadCode: val :=
   rec: "threadCode" "tid" :=
@@ -734,7 +776,8 @@ Definition loopSpawn: val :=
     let: "dummy" := ref_to boolT #true in
     (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
       "dummy" <-[boolT] ~ (![boolT] "dummy");;
-      Continue).
+      Continue);;
+    #().
 
 (* strings.go *)
 
@@ -818,11 +861,13 @@ Definition S__readBVal: val :=
 
 Definition S__writeB: val :=
   rec: "S__writeB" "s" "two" :=
-    struct.storeF S "b" "s" "two".
+    struct.storeF S "b" "s" "two";;
+    #().
 
 Definition S__negateC: val :=
   rec: "S__negateC" "s" :=
-    struct.storeF S "c" "s" (~ (struct.loadF S "c" "s")).
+    struct.storeF S "c" "s" (~ (struct.loadF S "c" "s"));;
+    #().
 
 Definition S__refC: val :=
   rec: "S__refC" "s" :=
@@ -846,12 +891,25 @@ Definition setField: val :=
 Definition DoSomeLocking: val :=
   rec: "DoSomeLocking" "l" :=
     lock.acquire "l";;
-    lock.release "l".
+    lock.release "l";;
+    #().
 
 Definition makeLock: val :=
   rec: "makeLock" <> :=
     let: "l" := lock.new #() in
-    DoSomeLocking "l".
+    DoSomeLocking "l";;
+    #().
+
+(* trailing_call.go *)
+
+Definition mkInt: val :=
+  rec: "mkInt" <> :=
+    #42.
+
+Definition mkNothing: val :=
+  rec: "mkNothing" <> :=
+    mkInt #();;
+    #().
 
 (* type_alias.go *)
 
diff --git a/internal/examples/wal/wal.gold.v b/internal/examples/wal/wal.gold.v
index ee91906a..97a67307 100644
--- a/internal/examples/wal/wal.gold.v
+++ b/internal/examples/wal/wal.gold.v
@@ -41,9 +41,7 @@ Definition New: val :=
     let: "d" := disk.Get #() in
     let: "diskSize" := disk.Size #() in
     (if: "diskSize" ≤ logLength
-    then
-      Panic ("disk is too small to host log");;
-      #()
+    then Panic ("disk is too small to host log")
     else #());;
     let: "cache" := NewMap disk.blockT in
     let: "header" := intToBlock #0 in
@@ -63,14 +61,16 @@ Hint Resolve New_t : types.
 
 Definition Log__lock: val :=
   rec: "Log__lock" "l" :=
-    lock.acquire (struct.get Log "l" "l").
+    lock.acquire (struct.get Log "l" "l");;
+    #().
 Theorem Log__lock_t: ⊢ Log__lock : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__lock_t : types.
 
 Definition Log__unlock: val :=
   rec: "Log__unlock" "l" :=
-    lock.release (struct.get Log "l" "l").
+    lock.release (struct.get Log "l" "l");;
+    #().
 Theorem Log__unlock_t: ⊢ Log__unlock : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__unlock_t : types.
@@ -126,9 +126,7 @@ Definition Log__Write: val :=
     Log__lock "l";;
     let: "length" := ![uint64T] (struct.get Log "length" "l") in
     (if: "length" ≥ MaxTxnWrites
-    then
-      Panic ("transaction is at capacity");;
-      #()
+    then Panic ("transaction is at capacity")
     else #());;
     let: "aBlock" := intToBlock "a" in
     let: "nextAddr" := #1 + #2 * "length" in
@@ -136,7 +134,8 @@ Definition Log__Write: val :=
     disk.Write ("nextAddr" + #1) "v";;
     MapInsert (struct.get Log "cache" "l") "a" "v";;
     struct.get Log "length" "l" <-[uint64T] "length" + #1;;
-    Log__unlock "l".
+    Log__unlock "l";;
+    #().
 Theorem Log__Write_t: ⊢ Log__Write : (struct.t Log -> uint64T -> disk.blockT -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Write_t : types.
@@ -148,7 +147,8 @@ Definition Log__Commit: val :=
     let: "length" := ![uint64T] (struct.get Log "length" "l") in
     Log__unlock "l";;
     let: "header" := intToBlock "length" in
-    disk.Write #0 "header".
+    disk.Write #0 "header";;
+    #().
 Theorem Log__Commit_t: ⊢ Log__Commit : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Commit_t : types.
@@ -175,7 +175,8 @@ Definition applyLog: val :=
         disk.Write (logLength + "a") "v";;
         "i" <-[uint64T] ![uint64T] "i" + #1;;
         Continue
-      else Break)).
+      else Break));;
+    #().
 Theorem applyLog_t: ⊢ applyLog : (disk.Disk -> uint64T -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve applyLog_t : types.
@@ -183,7 +184,8 @@ Hint Resolve applyLog_t : types.
 Definition clearLog: val :=
   rec: "clearLog" "d" :=
     let: "header" := intToBlock #0 in
-    disk.Write #0 "header".
+    disk.Write #0 "header";;
+    #().
 Theorem clearLog_t: ⊢ clearLog : (disk.Disk -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve clearLog_t : types.
@@ -198,7 +200,8 @@ Definition Log__Apply: val :=
     applyLog (struct.get Log "d" "l") "length";;
     clearLog (struct.get Log "d" "l");;
     struct.get Log "length" "l" <-[uint64T] #0;;
-    Log__unlock "l".
+    Log__unlock "l";;
+    #().
 Theorem Log__Apply_t: ⊢ Log__Apply : (struct.t Log -> unitT).
 Proof. typecheck. Qed.
 Hint Resolve Log__Apply_t : types.
diff --git a/testdata/negative-tests/badif1.go b/testdata/negative-tests/badif1.go
index 67599d91..fa7a4047 100644
--- a/testdata/negative-tests/badif1.go
+++ b/testdata/negative-tests/badif1.go
@@ -5,7 +5,7 @@ func Skip() {}
 func BadIf(i uint64) {
 	if i == 0 {
 		return
-	} else { // ERROR else with early return
+	} else { // ERROR early return in if with an else branch
 		Skip()
 	}
 	Skip()
diff --git a/testdata/negative-tests/badif2.go b/testdata/negative-tests/badif2.go
index 1e4d1869..a000d6cd 100644
--- a/testdata/negative-tests/badif2.go
+++ b/testdata/negative-tests/badif2.go
@@ -4,8 +4,8 @@ func Skip() {}
 
 func BadIf2(i uint64) {
 	if i == 0 {
-		if true {
-			return // ERROR nested if statement branches differ on whether they return
+		if true { // ERROR nested if statement branches differ on whether they return
+			return
 		} else {
 			Skip()
 		}
diff --git a/testdata/negative-tests/badif3.go b/testdata/negative-tests/badif3.go
new file mode 100644
index 00000000..fd006585
--- /dev/null
+++ b/testdata/negative-tests/badif3.go
@@ -0,0 +1,13 @@
+package example
+
+func Skip() {}
+
+func BadIf2(i uint64) {
+	if i == 0 {
+		if true {
+			return // ERROR return in unsupported position
+		}
+		Skip()
+	}
+	Skip()
+}
diff --git a/testdata/negative-tests/badloop1.go b/testdata/negative-tests/badloop1.go
deleted file mode 100644
index fe173dc5..00000000
--- a/testdata/negative-tests/badloop1.go
+++ /dev/null
@@ -1,12 +0,0 @@
-package example
-
-func Skip() bool { return false }
-
-func BadLoop(i uint64) {
-	// This used to translate incorrectly, into a loop that always `Continue`s.
-	for {
-		if !Skip() { // ERROR nested if statement branches differ on whether they return
-			break
-		}
-	}
-}
diff --git a/testdata/negative-tests/deadcode.go b/testdata/negative-tests/deadcode.go
index 7681b323..29e72318 100644
--- a/testdata/negative-tests/deadcode.go
+++ b/testdata/negative-tests/deadcode.go
@@ -1,7 +1,7 @@
 package example
 
 func codeAfterReturn(m map[uint64]uint64) uint64 {
-	return 0
-	m[1] = 1 // ERROR following return
+	return 0 // ERROR return in unsupported position
+	m[1] = 1
 	return 1
 }

From 4629beabd516ffa64926a2da1c805e9a30ebf372 Mon Sep 17 00:00:00 2001
From: Ralf Jung <research@ralfj.de>
Date: Mon, 6 Sep 2021 19:45:45 -0400
Subject: [PATCH 2/6] support arbitrary control flow in final statement inside
 loop

also fix and extend some comments
---
 goose.go                                     | 70 +++++++++-----------
 internal/examples/logging2/logging2.gold.v   |  3 +-
 internal/examples/semantics/semantics.gold.v |  3 +-
 internal/examples/unittest/loops.go          | 13 ++++
 internal/examples/unittest/unittest.gold.v   | 21 +++++-
 testdata/negative-tests/badif2.go            |  2 +-
 6 files changed, 67 insertions(+), 45 deletions(-)

diff --git a/goose.go b/goose.go
index c5355b62..3b8c9e07 100644
--- a/goose.go
+++ b/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,37 +1154,39 @@ 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)
 	}
 
@@ -1194,11 +1194,7 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, remainder []ast.Stmt, usage ExprValUsage) c
 	// 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.
diff --git a/internal/examples/logging2/logging2.gold.v b/internal/examples/logging2/logging2.gold.v
index 2c3f3fb6..0dc16d69 100644
--- a/internal/examples/logging2/logging2.gold.v
+++ b/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).
diff --git a/internal/examples/semantics/semantics.gold.v b/internal/examples/semantics/semantics.gold.v
index 93ab9a70..46f77472 100644
--- a/internal/examples/semantics/semantics.gold.v
+++ b/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.
diff --git a/internal/examples/unittest/loops.go b/internal/examples/unittest/loops.go
index 1b354723..1a3598d7 100644
--- a/internal/examples/unittest/loops.go
+++ b/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 {
diff --git a/internal/examples/unittest/unittest.gold.v b/internal/examples/unittest/unittest.gold.v
index ad4bcf28..7484ff4e 100644
--- a/internal/examples/unittest/unittest.gold.v
+++ b/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 :=
diff --git a/testdata/negative-tests/badif2.go b/testdata/negative-tests/badif2.go
index a000d6cd..42e327a7 100644
--- a/testdata/negative-tests/badif2.go
+++ b/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()

From fae9aace94a442a21684beb568dc8002721f18d4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <research@ralfj.de>
Date: Tue, 7 Sep 2021 09:18:45 -0400
Subject: [PATCH 3/6] make stmt function more sensible and add challenging
 testcase

---
 goose.go                                   | 38 ++++++++++------------
 internal/examples/unittest/control_flow.go | 14 ++++++++
 internal/examples/unittest/unittest.gold.v | 11 +++++++
 3 files changed, 42 insertions(+), 21 deletions(-)

diff --git a/goose.go b/goose.go
index 3b8c9e07..c0139fde 100644
--- a/goose.go
+++ b/goose.go
@@ -1107,10 +1107,9 @@ func (ctx Ctx) stmts(ss []ast.Stmt, usage ExprValUsage) coq.BlockExpr {
 			finalized = true
 			break // This would happen anyway since we consumed the iterator via "Remainder"
 		default:
+			// All other statements are translated one-by-one
 			if c.HasNext() {
-				// "finalized" will always be true.
-				binding, _ := ctx.stmtInBlock(s, ExprValLocal)
-				bindings = append(bindings, binding)
+				bindings = append(bindings, ctx.stmt(s))
 			} else {
 				// The last statement is special: we propagate the usage and store "finalized"
 				binding, fin := ctx.stmtInBlock(s, usage)
@@ -1119,7 +1118,7 @@ func (ctx Ctx) stmts(ss []ast.Stmt, usage ExprValUsage) coq.BlockExpr {
 			}
 		}
 	}
-	// Crucially, we also arrive in this branch if the list if statements is empty.
+	// Crucially, we also arrive in this branch if the list of statements is empty.
 	if !finalized {
 		switch usage {
 		case ExprValReturned:
@@ -1154,10 +1153,10 @@ 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{}
+	// Extract (possibly empty) block in Else
+	var Else = &ast.BlockStmt{List: []ast.Stmt{}}
 	if s.Else != nil {
-		Else = s.Else.(*ast.BlockStmt).List
+		Else = s.Else.(*ast.BlockStmt)
 	}
 
 	// Supported cases are:
@@ -1168,7 +1167,7 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, remainder []ast.Stmt, usage ExprValUsage) c
 	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)
+		ife.Else = ctx.blockStmt(Else, usage)
 		return coq.NewAnon(ife)
 	}
 
@@ -1179,7 +1178,7 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, remainder []ast.Stmt, usage ExprValUsage) c
 		ife.Then = ctx.blockStmt(s.Body, usage)
 		// Put trailing code into "else". This is correct because "then" will always return.
 		// "else" must be empty.
-		if s.Else != nil {
+		if len(Else.List) > 0 {
 			ctx.futureWork(s.Else, "early return in if with an else branch")
 			return coq.Binding{}
 		}
@@ -1194,7 +1193,7 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, remainder []ast.Stmt, usage ExprValUsage) c
 	// 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)
-	ife.Else = ctx.stmts(Else, ExprValLocal)
+	ife.Else = ctx.blockStmt(Else, ExprValLocal)
 	// And translate the remainder with our usage.
 	tailExpr := ctx.stmts(remainder, usage)
 	// Prepend the if-then-else before the tail.
@@ -1227,7 +1226,7 @@ func (ctx Ctx) forStmt(s *ast.ForStmt) coq.ForLoopExpr {
 		ctx.addDef(ident, identInfo{
 			IsPtrWrapped: true,
 		})
-		init = ctx.stmt(s.Init, ExprValLocal)
+		init = ctx.stmt(s.Init)
 	}
 	var cond coq.Expr = coq.True
 	if s.Cond != nil {
@@ -1235,7 +1234,7 @@ func (ctx Ctx) forStmt(s *ast.ForStmt) coq.ForLoopExpr {
 	}
 	var post coq.Expr = coq.Skip
 	if s.Post != nil {
-		postBlock := ctx.stmt(s.Post, ExprValLocal)
+		postBlock := ctx.stmt(s.Post)
 		if len(postBlock.Names) > 0 {
 			ctx.unsupported(s.Post, "post cannot bind names")
 		}
@@ -1723,17 +1722,14 @@ func (ctx Ctx) stmtInBlock(s ast.Stmt, usage ExprValUsage) (coq.Binding, bool) {
 	}
 }
 
-// Translate a single statement and finalize it if needed
-func (ctx Ctx) stmt(s ast.Stmt, usage ExprValUsage) coq.Binding {
+// Translate a single statement without usage (i.e., no control effects available)
+func (ctx Ctx) stmt(s ast.Stmt) coq.Binding {
 	// stmts takes care of finalization...
-	block := ctx.stmts([]ast.Stmt{s}, usage)
-	// ...but let's prettify the result while converting to a Binding.
-	// FIXME(RJ): not "prettifying" (always using NewAnon) actually breaks translation. Hu?
-	if len(block.Bindings) == 1 {
-		return block.Bindings[0]
-	} else {
-		return coq.NewAnon(block)
+	binding, finalized := ctx.stmtInBlock(s, ExprValLocal)
+	if !finalized {
+		panic("ExprValLocal usage should always be finalized")
 	}
+	return binding
 }
 
 func (ctx Ctx) returnExpr(es []ast.Expr) coq.Expr {
diff --git a/internal/examples/unittest/control_flow.go b/internal/examples/unittest/control_flow.go
index a8163538..af4a6e64 100644
--- a/internal/examples/unittest/control_flow.go
+++ b/internal/examples/unittest/control_flow.go
@@ -15,6 +15,20 @@ func alwaysReturn(x bool) uint64 {
 	}
 }
 
+func alwaysReturnInNestedBranches(x bool) uint64 {
+	if !x {
+		if x {
+			return 0
+		} else {
+			return 1
+		}
+	} else {
+		// we can even have an empty else block
+	}
+	y := uint64(14)
+	return y
+}
+
 func earlyReturn(x bool) {
 	if x {
 		return
diff --git a/internal/examples/unittest/unittest.gold.v b/internal/examples/unittest/unittest.gold.v
index 7484ff4e..2a0dbefb 100644
--- a/internal/examples/unittest/unittest.gold.v
+++ b/internal/examples/unittest/unittest.gold.v
@@ -77,6 +77,17 @@ Definition alwaysReturn: val :=
     then #0
     else #1).
 
+Definition alwaysReturnInNestedBranches: val :=
+  rec: "alwaysReturnInNestedBranches" "x" :=
+    (if: ~ "x"
+    then
+      (if: "x"
+      then #0
+      else #1)
+    else
+      let: "y" := #14 in
+      "y").
+
 Definition earlyReturn: val :=
   rec: "earlyReturn" "x" :=
     (if: "x"

From ea8718c45ebfa13b59a3dfd5fb8f2aafc5e7f688 Mon Sep 17 00:00:00 2001
From: Ralf Jung <research@ralfj.de>
Date: Thu, 16 Sep 2021 22:37:21 -0400
Subject: [PATCH 4/6] fix 'else if' handling

---
 goose.go                                   | 10 +++++++++-
 internal/examples/unittest/control_flow.go | 10 ++++++++++
 internal/examples/unittest/unittest.gold.v |  9 +++++++++
 3 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/goose.go b/goose.go
index c0139fde..d0891536 100644
--- a/goose.go
+++ b/goose.go
@@ -1156,7 +1156,15 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, remainder []ast.Stmt, usage ExprValUsage) c
 	// Extract (possibly empty) block in Else
 	var Else = &ast.BlockStmt{List: []ast.Stmt{}}
 	if s.Else != nil {
-		Else = s.Else.(*ast.BlockStmt)
+		switch s := s.Else.(type) {
+		case *ast.BlockStmt:
+			Else = s
+		case *ast.IfStmt:
+			// This is an "else if"
+			Else.List = []ast.Stmt{s}
+		default:
+			panic("if statement with unexpected kind of else branch")
+		}
 	}
 
 	// Supported cases are:
diff --git a/internal/examples/unittest/control_flow.go b/internal/examples/unittest/control_flow.go
index af4a6e64..26f0c6ff 100644
--- a/internal/examples/unittest/control_flow.go
+++ b/internal/examples/unittest/control_flow.go
@@ -45,3 +45,13 @@ func conditionalAssign(x bool) uint64 {
 	y += 1
 	return y
 }
+
+func elseIf(x, y bool) uint64 {
+	if x {
+		return 0
+	} else if y {
+		return 1
+	} else {
+		return 2
+	}
+}
diff --git a/internal/examples/unittest/unittest.gold.v b/internal/examples/unittest/unittest.gold.v
index 2a0dbefb..2aff09a2 100644
--- a/internal/examples/unittest/unittest.gold.v
+++ b/internal/examples/unittest/unittest.gold.v
@@ -103,6 +103,15 @@ Definition conditionalAssign: val :=
     "y" <-[uint64T] ![uint64T] "y" + #1;;
     ![uint64T] "y".
 
+Definition elseIf: val :=
+  rec: "elseIf" "x" "y" :=
+    (if: "x"
+    then #0
+    else
+      (if: "y"
+      then #1
+      else #2)).
+
 (* conversions.go *)
 
 Definition stringWrapper: ty := stringT.

From 74c8b39155261b6559204a0c5fdf9a635eab9b8d Mon Sep 17 00:00:00 2001
From: Ralf Jung <research@ralfj.de>
Date: Thu, 16 Sep 2021 22:50:21 -0400
Subject: [PATCH 5/6] add negative testcase for break in range loop

---
 testdata/negative-tests/badbreak.go | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 testdata/negative-tests/badbreak.go

diff --git a/testdata/negative-tests/badbreak.go b/testdata/negative-tests/badbreak.go
new file mode 100644
index 00000000..850d13ef
--- /dev/null
+++ b/testdata/negative-tests/badbreak.go
@@ -0,0 +1,10 @@
+package example
+
+func sumSlice(xs []uint64) uint64 {
+	var sum uint64
+	for _, x := range xs {
+		sum += x
+		break // ERROR break/continue in unsupported position
+	}
+	return sum
+}

From 19cf6d94814f057c7d3e6731af8501f4386a6043 Mon Sep 17 00:00:00 2001
From: Ralf Jung <research@ralfj.de>
Date: Thu, 16 Sep 2021 22:57:07 -0400
Subject: [PATCH 6/6] this test is no longer failing

---
 internal/examples/semantics/generated_test.go | 2 +-
 internal/examples/semantics/loops.go          | 2 +-
 internal/examples/semantics/semantics.gold.v  | 8 ++++----
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/internal/examples/semantics/generated_test.go b/internal/examples/semantics/generated_test.go
index 15dffc72..c2481417 100644
--- a/internal/examples/semantics/generated_test.go
+++ b/internal/examples/semantics/generated_test.go
@@ -194,7 +194,7 @@ func (suite *GoTestSuite) TestBreakFromLoopNoContinue() {
 func (suite *GoTestSuite) TestBreakFromLoopNoContinueDouble() {
 	d := disk.NewMemDisk(30)
 	disk.Init(d)
-	suite.Equal(true, failing_testBreakFromLoopNoContinueDouble())
+	suite.Equal(true, testBreakFromLoopNoContinueDouble())
 }
 
 func (suite *GoTestSuite) TestBreakFromLoopForOnly() {
diff --git a/internal/examples/semantics/loops.go b/internal/examples/semantics/loops.go
index b251569e..3d556077 100644
--- a/internal/examples/semantics/loops.go
+++ b/internal/examples/semantics/loops.go
@@ -80,7 +80,7 @@ func testBreakFromLoopNoContinue() bool {
 	return (i == 1)
 }
 
-func failing_testBreakFromLoopNoContinueDouble() bool {
+func testBreakFromLoopNoContinueDouble() bool {
 	var i uint64 = 0
 	for i < 3 {
 		if i == 1 {
diff --git a/internal/examples/semantics/semantics.gold.v b/internal/examples/semantics/semantics.gold.v
index 46f77472..71cfc4f0 100644
--- a/internal/examples/semantics/semantics.gold.v
+++ b/internal/examples/semantics/semantics.gold.v
@@ -693,8 +693,8 @@ Theorem testBreakFromLoopNoContinue_t: ⊢ testBreakFromLoopNoContinue : (unitT
 Proof. typecheck. Qed.
 Hint Resolve testBreakFromLoopNoContinue_t : types.
 
-Definition failing_testBreakFromLoopNoContinueDouble: val :=
-  rec: "failing_testBreakFromLoopNoContinueDouble" <> :=
+Definition testBreakFromLoopNoContinueDouble: val :=
+  rec: "testBreakFromLoopNoContinueDouble" <> :=
     let: "i" := ref_to uint64T #0 in
     Skip;;
     (for: (λ: <>, ![uint64T] "i" < #3); (λ: <>, Skip) := λ: <>,
@@ -707,9 +707,9 @@ Definition failing_testBreakFromLoopNoContinueDouble: val :=
         "i" <-[uint64T] ![uint64T] "i" + #2;;
         Continue));;
     (![uint64T] "i" = #4).
-Theorem failing_testBreakFromLoopNoContinueDouble_t: ⊢ failing_testBreakFromLoopNoContinueDouble : (unitT -> boolT).
+Theorem testBreakFromLoopNoContinueDouble_t: ⊢ testBreakFromLoopNoContinueDouble : (unitT -> boolT).
 Proof. typecheck. Qed.
-Hint Resolve failing_testBreakFromLoopNoContinueDouble_t : types.
+Hint Resolve testBreakFromLoopNoContinueDouble_t : types.
 
 Definition testBreakFromLoopForOnly: val :=
   rec: "testBreakFromLoopForOnly" <> :=