Skip to content

Commit

Permalink
refactor handling of control effects (early return/break/continue)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@RalfJung
RalfJung committed Sep 6, 2021
1 parent 6377769 commit 04eaef0
Show file tree
Hide file tree
Showing 11 changed files with 413 additions and 269 deletions.
304 changes: 167 additions & 137 deletions goose.go
View file

Large diffs are not rendered by default.

12 changes: 8 additions & 4 deletions internal/examples/append_log/append_log.gold.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
26 changes: 14 additions & 12 deletions internal/examples/logging2/logging2.gold.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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).
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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
Expand Down
69 changes: 38 additions & 31 deletions internal/examples/semantics/semantics.gold.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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
Expand All @@ -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 #()
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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);;
Expand Down
Loading

0 comments on commit 04eaef0

Please sign in to comment.