Skip to content

Commit

Permalink
Prove closed globals_test using new globals/funcs/methods
Browse files Browse the repository at this point in the history
  • Loading branch information
@upamanyus
upamanyus committed Jan 17, 2025
1 parent f956ce8 commit 89ed8ab
Show file tree
Hide file tree
Showing 40 changed files with 1,281 additions and 2,849 deletions.
36 changes: 18 additions & 18 deletions new/code/github_com/goose_lang/goose/testdata/examples/append_log.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,10 @@ Definition Log__mkHdr : val :=
(func_call #marshal.pkg_name' #"NewEnc"%go) "$a0") in
do: ("enc" <-[marshal.Enc] "$r0");;;
do: (let: "$a0" := (![uint64T] (struct.field_ref Log "sz" (![ptrT] "log"))) in
(method_call #marshal.pkg_name' #"Enc" #"PutInt" "PutInt" #() (![marshal.Enc] "enc")) "$a0");;;
(method_call #marshal.pkg_name' #"Enc" #"PutInt" (![marshal.Enc] "enc")) "$a0");;;
do: (let: "$a0" := (![uint64T] (struct.field_ref Log "diskSz" (![ptrT] "log"))) in
(method_call #marshal.pkg_name' #"Enc" #"PutInt" "PutInt" #() (![marshal.Enc] "enc")) "$a0");;;
return: ((method_call #marshal.pkg_name' #"Enc" #"Finish" "Finish" #() (![marshal.Enc] "enc")) #())).
(method_call #marshal.pkg_name' #"Enc" #"PutInt" (![marshal.Enc] "enc")) "$a0");;;
return: ((method_call #marshal.pkg_name' #"Enc" #"Finish" (![marshal.Enc] "enc")) #())).

Definition pkg_name' : go_string := "github.com/goose-lang/goose/testdata/examples/append_log".

Expand All @@ -33,7 +33,7 @@ Definition Log__writeHdr : val :=
rec: "Log__writeHdr" "log" <> :=
exception_do (let: "log" := (ref_ty ptrT "log") in
do: (let: "$a0" := #(W64 0) in
let: "$a1" := ((method_call #pkg_name' #"Log'ptr" #"mkHdr" #() (![ptrT] "log")) #()) in
let: "$a1" := ((method_call #pkg_name' #"Log'ptr" #"mkHdr" (![ptrT] "log")) #()) in
(func_call #disk.pkg_name' #"Write"%go) "$a0" "$a1")).

(* go: append_log.go:33:6 *)
Expand Down Expand Up @@ -61,7 +61,7 @@ Definition Init : val :=
"diskSz" ::= "$diskSz"
}])) in
do: ("log" <-[ptrT] "$r0");;;
do: ((method_call #pkg_name' #"Log'ptr" #"writeHdr" #() (![ptrT] "log")) #());;;
do: ((method_call #pkg_name' #"Log'ptr" #"writeHdr" (![ptrT] "log")) #());;;
return: (![ptrT] "log", #true)).

(* go: append_log.go:42:6 *)
Expand All @@ -76,10 +76,10 @@ Definition Open : val :=
(func_call #marshal.pkg_name' #"NewDec"%go) "$a0") in
do: ("dec" <-[marshal.Dec] "$r0");;;
let: "sz" := (ref_ty uint64T (zero_val uint64T)) in
let: "$r0" := ((method_call #marshal.pkg_name' #"Dec" #"GetInt" "GetInt" #() (![marshal.Dec] "dec")) #()) in
let: "$r0" := ((method_call #marshal.pkg_name' #"Dec" #"GetInt" (![marshal.Dec] "dec")) #()) in
do: ("sz" <-[uint64T] "$r0");;;
let: "diskSz" := (ref_ty uint64T (zero_val uint64T)) in
let: "$r0" := ((method_call #marshal.pkg_name' #"Dec" #"GetInt" "GetInt" #() (![marshal.Dec] "dec")) #()) in
let: "$r0" := ((method_call #marshal.pkg_name' #"Dec" #"GetInt" (![marshal.Dec] "dec")) #()) in
do: ("diskSz" <-[uint64T] "$r0");;;
return: (ref_ty Log (let: "$m" := (ref_ty sync.Mutex (zero_val sync.Mutex)) in
let: "$sz" := (![uint64T] "sz") in
Expand Down Expand Up @@ -110,16 +110,16 @@ Definition Log__Get : val :=
rec: "Log__Get" "log" "i" :=
exception_do (let: "log" := (ref_ty ptrT "log") in
let: "i" := (ref_ty uint64T "i") in
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" #() (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
let: "b" := (ref_ty boolT (zero_val boolT)) in
let: "v" := (ref_ty sliceT (zero_val sliceT)) in
let: ("$ret0", "$ret1") := (let: "$a0" := (![uint64T] "i") in
(method_call #pkg_name' #"Log'ptr" #"get" #() (![ptrT] "log")) "$a0") in
(method_call #pkg_name' #"Log'ptr" #"get" (![ptrT] "log")) "$a0") in
let: "$r0" := "$ret0" in
let: "$r1" := "$ret1" in
do: ("v" <-[sliceT] "$r0");;;
do: ("b" <-[boolT] "$r1");;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" #() (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
return: (![sliceT] "v", ![boolT] "b")).

(* go: append_log.go:65:6 *)
Expand Down Expand Up @@ -152,20 +152,20 @@ Definition Log__append : val :=
(func_call #pkg_name' #"writeAll"%go) "$a0" "$a1");;;
do: ((struct.field_ref Log "sz" (![ptrT] "log")) <-[uint64T] ((![uint64T] (struct.field_ref Log "sz" (![ptrT] "log"))) + (let: "$a0" := (![sliceT] "bks") in
slice.len "$a0")));;;
do: ((method_call #pkg_name' #"Log'ptr" #"writeHdr" #() (![ptrT] "log")) #());;;
do: ((method_call #pkg_name' #"Log'ptr" #"writeHdr" (![ptrT] "log")) #());;;
return: (#true)).

(* go: append_log.go:82:17 *)
Definition Log__Append : val :=
rec: "Log__Append" "log" "bks" :=
exception_do (let: "log" := (ref_ty ptrT "log") in
let: "bks" := (ref_ty sliceT "bks") in
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" #() (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
let: "b" := (ref_ty boolT (zero_val boolT)) in
let: "$r0" := (let: "$a0" := (![sliceT] "bks") in
(method_call #pkg_name' #"Log'ptr" #"append" #() (![ptrT] "log")) "$a0") in
(method_call #pkg_name' #"Log'ptr" #"append" (![ptrT] "log")) "$a0") in
do: ("b" <-[boolT] "$r0");;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" #() (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
return: (![boolT] "b")).

(* go: append_log.go:89:17 *)
Expand All @@ -174,15 +174,15 @@ Definition Log__reset : val :=
exception_do (let: "log" := (ref_ty ptrT "log") in
let: "$r0" := #(W64 0) in
do: ((struct.field_ref Log "sz" (![ptrT] "log")) <-[uint64T] "$r0");;;
do: ((method_call #pkg_name' #"Log'ptr" #"writeHdr" #() (![ptrT] "log")) #())).
do: ((method_call #pkg_name' #"Log'ptr" #"writeHdr" (![ptrT] "log")) #())).

(* go: append_log.go:94:17 *)
Definition Log__Reset : val :=
rec: "Log__Reset" "log" <> :=
exception_do (let: "log" := (ref_ty ptrT "log") in
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" #() (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
do: ((method_call #pkg_name' #"Log'ptr" #"reset" #() (![ptrT] "log")) #());;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" #() (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #())).
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #());;;
do: ((method_call #pkg_name' #"Log'ptr" #"reset" (![ptrT] "log")) #());;;
do: ((method_call #sync.pkg_name' #"Mutex'ptr" #"Unlock" (![ptrT] (struct.field_ref Log "m" (![ptrT] "log")))) #())).

Definition vars' : list (go_string * go_type) := [].

Expand Down
Loading

0 comments on commit 89ed8ab

Please sign in to comment.