refactor handling of control effects (early return/break/continue) #25

RalfJung · 2021-09-06T22:45:52Z

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. There are probably better names than usage ExprValUsage for this...
It is however also entirely possible that I missed something fundamental here, there are still bits of the Goose structure that I do not entirely understand. I will leave some comments in the diff.

Fixes #15. The trailing units everywhere account for the majority of the gold file diff.

I think fixes #3. Makes #2 easy to implement.

RalfJung · 2021-09-06T22:46:47Z

goose.go

+				bindings = append(bindings, binding)
+				finalized = fin
+			}
+		}


Is there a nicer way to do this entire "finalized" thing? Basically for the last statement we want to know if it "used up" its control effect or not.

RalfJung · 2021-09-06T22:47:30Z

goose.go

+				// 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)


The old code did some weird things with Unwrap here, complaining with "if statement else ends with an assignment". I have no idea what that is about, but this seems to work.

RalfJung · 2021-09-06T22:47:55Z

goose.go

+	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 })


The conversion between binding and block and so on here is somewhat annoying, I feel I am not using these types entirely as intended...

goose.go

RalfJung · 2021-09-06T22:51:18Z

internal/examples/semantics/semantics.gold.v

-      else "i" <-[uint64T] ![uint64T] "i" + #2));;
+      else
+        "i" <-[uint64T] ![uint64T] "i" + #2;;
+        Continue));;


I think the old translation was wrong here, the "else" branch was lacking a Continue.
(This test was changed in #7, but not entirely fixed I think.)

RalfJung · 2021-09-06T22:51:45Z

internal/examples/semantics/semantics.gold.v

@@ -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));;


Same here, this diff is a bugfix.

Ah this test is actually called failing_testBreakFromLoopNoContinueDouble, I guess I can rename it now? :D

RalfJung · 2021-09-06T22:59:21Z

Some of the negative examples are failing on CI

=== CONT  TestNegativeExamples/badif3.go
    examples_test.go:295: 
        	Error Trace:	examples_test.go:295
        	Error:      	%s: error message "%s" does not contain "%s"
        	Test:       	TestNegativeExamples/badif3.go
        	Messages:   	deadcode.go%!(EXTRA string=return in unsupported position, string=following return)

but go test -v passes locally. Strange.

goose.go

RalfJung · 2021-09-06T23:14:25Z

goose.go

@@ -1346,7 +1351,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),


There's an easy path to supporting control effects in slice (and map) range statements now: we translate this with ExprValLoop, and adjust coq.SliceLoopExpr generation such that the loop body should return Break or Continue to tell the iterator function what to do.

RalfJung · 2021-09-06T23:20:49Z

goose.go

-	return false
-}
-
-func stmtsEndIncludesIf(ss []ast.Stmt) bool {


I'm happy to remove these functions since I could not figure out the right contract for them anyway. ;)

goose.go

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.

also fix and extend some comments

RalfJung · 2021-09-17T03:02:33Z

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())


I am not quite sure what this file is about... it says "generated" but I hand-edited this change since CI complained about a diff here.

Are these Coq-Go-conformance tests run automatically on CI?

The comment at the top of the file is quite clear about not editing this by hand. But then how to invoke test_gen? The README says "To re-generate the Go test file you can just run go generate ./...". So I did go generate internal/examples/semantics/generated_test.go but that does not seem to do anything...

This seems to work:

go run ./cmd/test_gen -go -out ./internal/examples/semantics/generated_test.go ./internal/examples/semantics

RalfJung · 2021-09-17T17:48:26Z

I got Perennial to work again with this branch, the patch is at https://github.com/mit-pdos/perennial/tree/goose-control-flow. The only changes in the Goose'd output (besides the examples I commented on above) are from all these extra units, as far as I can see.

So I think this PR is ready.

tchajed · 2021-09-23T23:46:54Z

Okay now I think I understand this, and it passes on Perennial so I trust it.