From cc59a1391844eeaca7c4601d3b3315b37f44fb76 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 6 Sep 2021 19:45:45 -0400 Subject: [PATCH] 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()