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.

Author: RalfJung

goose.go

@@ -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.

internal/examples/append_log/append_log.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

internal/examples/logging2/logging2.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,17 +1740,16 @@ 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
     disk.Write "nextAddr" "aBlock";;
     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,15 +1789,17 @@ 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.
 
 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);;