Merge pull request #23 from RalfJung/nested-early-return

better handling of nested conditionals that early return

goose.go

@@ -1051,15 +1051,15 @@ func (c *cursor) Remainder() []ast.Stmt {
 	return s
 }
 
-func endsWithReturn(s ast.Stmt) bool {
+func (ctx Ctx) endsWithReturn(s ast.Stmt) bool {
 	if s == nil {
 		return false
 	}
 	switch s := s.(type) {
 	case *ast.BlockStmt:
-		return stmtsEndWithReturn(s.List)
+		return ctx.stmtsEndWithReturn(s.List)
 	default:
-		return stmtsEndWithReturn([]ast.Stmt{s})
+		return ctx.stmtsEndWithReturn([]ast.Stmt{s})
 	}
 }
 
@@ -1073,14 +1073,21 @@ func endIncludesIf(s ast.Stmt) bool {
 	return stmtsEndIncludesIf([]ast.Stmt{s})
 }
 
-func stmtsEndWithReturn(ss []ast.Stmt) bool {
+func (ctx Ctx) stmtsEndWithReturn(ss []ast.Stmt) bool {
 	if len(ss) == 0 {
 		return false
 	}
 	// TODO: should also catch implicit continue
-	switch ss[len(ss)-1].(type) {
+	switch s := ss[len(ss)-1].(type) {
 	case *ast.ReturnStmt, *ast.BranchStmt:
 		return true
+	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 false
 }
@@ -1140,7 +1147,7 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, c *cursor, loopVar *string) coq.Binding {
 	// of Else == nil should be supported, though.
 
 	remaining := c.HasNext()
-	bodyEndsWithReturn := endsWithReturn(s.Body)
+	bodyEndsWithReturn := ctx.endsWithReturn(s.Body)
 	if bodyEndsWithReturn && remaining {
 		if s.Else != nil {
 			ctx.futureWork(s.Else, "else with early return")
@@ -1159,7 +1166,7 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, c *cursor, loopVar *string) coq.Binding {
 		ife.Else = retUnit
 		return coq.NewAnon(ife)
 	}
-	elseEndsWithReturn := endsWithReturn(s.Else)
+	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
@@ -1225,7 +1232,7 @@ func (ctx Ctx) forStmt(s *ast.ForStmt) coq.ForLoopExpr {
 		post = postBlock.Expr
 	}
 
-	hasExplicitBranch := endsWithReturn(s.Body)
+	hasExplicitBranch := ctx.endsWithReturn(s.Body)
 	hasImplicitBranch := endIncludesIf(s.Body)
 
 	c := &cursor{s.Body.List}

internal/examples/simpledb/simpledb.gold.v

@@ -114,8 +114,7 @@ Definition readTableIndex: val :=
             "offset" ::= struct.get lazyFileBuf "offset" (![struct.t lazyFileBuf] "buf");
             "next" ::= "newBuf"
           ];;
-          Continue));;
-      Continue).
+          Continue))).
 
 (* RecoverTable restores a table from disk on startup. *)
 Definition RecoverTable: val :=
@@ -379,8 +378,7 @@ Definition tablePutOldTable: val :=
             "offset" ::= struct.get lazyFileBuf "offset" (![struct.t lazyFileBuf] "buf");
             "next" ::= "newBuf"
           ];;
-          Continue));;
-      Continue).
+          Continue))).
 
 (* Build a new shadow table that incorporates the current table and a
    (write) buffer wbuf.

internal/examples/unittest/loops.go

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

internal/examples/unittest/unittest.gold.v

@@ -387,6 +387,16 @@ Definition conditionalInLoop: val :=
         "i" <-[uint64T] ![uint64T] "i" + #1;;
         Continue)).
 
+Definition conditionalInLoopElse: val :=
+  rec: "conditionalInLoopElse" <> :=
+    let: "i" := ref_to uint64T #0 in
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      (if: ![uint64T] "i" > #5
+      then Break
+      else
+        "i" <-[uint64T] ![uint64T] "i" + #1;;
+        Continue)).
+
 Definition ImplicitLoopContinue: val :=
   rec: "ImplicitLoopContinue" <> :=
     let: "i" := ref_to uint64T #0 in

testdata/negative-tests/badif1.go

@@ -0,0 +1,12 @@
+package example
+
+func Skip() {}
+
+func BadIf(i uint64) {
+	if i == 0 {
+		return
+	} else { // ERROR else with early return
+		Skip()
+	}
+	Skip()
+}

testdata/negative-tests/badif2.go

@@ -0,0 +1,14 @@
+package example
+
+func Skip() {}
+
+func BadIf2(i uint64) {
+	if i == 0 {
+		if true {
+			return // ERROR nested if statement branches differ on whether they return
+		} else {
+			Skip()
+		}
+	}
+	Skip()
+}

testdata/negative-tests/badloop1.go

@@ -1,12 +1,12 @@
 package example
 
-func Skip() {}
+func Skip() bool { return false }
 
 func BadLoop(i uint64) {
-	if i == 0 {
-		return
-	} else { // ERROR else with early return
-		Skip()
+	// 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
+		}
 	}
-	Skip()
 }