Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 6 commits into from
Sep 23, 2021
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
cec9bb6
refactor handling of control effects (early return/break/continue)
RalfJung Sep 6, 2021
4629bea
support arbitrary control flow in final statement inside loop
RalfJung Sep 6, 2021
fae9aac
make stmt function more sensible and add challenging testcase
RalfJung Sep 7, 2021
ea8718c
fix 'else if' handling
RalfJung Sep 17, 2021
74c8b39
add negative testcase for break in range loop
RalfJung Sep 17, 2021
19cf6d9
this test is no longer failing
RalfJung Sep 17, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
313 changes: 173 additions & 140 deletions goose.go
View file
Open in desktop

Large diffs are not rendered by default.

12 changes: 8 additions & 4 deletions internal/examples/append_log/append_log.gold.v
View file
Open in desktop
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
Open in desktop
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
Open in desktop

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
Open in desktop
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
Open in desktop
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));;
Copy link
Collaborator Author

@RalfJung RalfJung Sep 6, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

(![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));;
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here, this diff is a bugfix.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

(![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