Skip to content

Commit

Permalink
Merge pull request #25 from RalfJung/control-effect-refactor
Browse files Browse the repository at this point in the history 
refactor handling of control effects (early return/break/continue)
  • Loading branch information
@tchajed
tchajed authored Sep 23, 2021
2 parents 746d419 + 19cf6d9 commit 29139bd
Show file tree
Hide file tree
Showing 18 changed files with 513 additions and 286 deletions.
313 changes: 173 additions & 140 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.
29 changes: 15 additions & 14 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,16 +222,13 @@ 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
(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).
Expand Down
2 changes: 1 addition & 1 deletion internal/examples/semantics/generated_test.go
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion internal/examples/semantics/loops.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ func testBreakFromLoopNoContinue() bool {
return (i == 1)
}

func failing_testBreakFromLoopNoContinueDouble() bool {
func testBreakFromLoopNoContinueDouble() bool {
var i uint64 = 0
for i < 3 {
if i == 1 {
Expand Down
74 changes: 40 additions & 34 deletions internal/examples/semantics/semantics.gold.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -631,7 +631,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,14 +685,16 @@ 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.
Hint Resolve testBreakFromLoopNoContinue_t : types.

Definition failing_testBreakFromLoopNoContinueDouble: val :=
rec: "failing_testBreakFromLoopNoContinueDouble" <> :=
Definition testBreakFromLoopNoContinueDouble: val :=
rec: "testBreakFromLoopNoContinueDouble" <> :=
let: "i" := ref_to uint64T #0 in
Skip;;
(for: (λ: <>, ![uint64T] "i" < #3); (λ: <>, Skip) := λ: <>,
Expand All @@ -701,11 +704,12 @@ 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).
Theorem testBreakFromLoopNoContinueDouble_t: ⊢ testBreakFromLoopNoContinueDouble : (unitT -> boolT).
Proof. typecheck. Qed.
Hint Resolve failing_testBreakFromLoopNoContinueDouble_t : types.
Hint Resolve testBreakFromLoopNoContinueDouble_t : types.

Definition testBreakFromLoopForOnly: val :=
rec: "testBreakFromLoopForOnly" <> :=
Expand Down Expand Up @@ -1100,9 +1104,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 +1118,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 +1248,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 +1361,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 +1439,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 +1654,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 +1674,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 +1739,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 +1760,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 +1788,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 +1813,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 +1847,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 29139bd

Please sign in to comment.