Merge branch 'globals'

new/code/github_com/goose_lang/goose/testdata/examples/append_log.v

@@ -195,3 +195,18 @@ Definition Open : val :=
        "sz" ::= "$sz";
        "diskSz" ::= "$diskSz"
      }]))).
+
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/append_log".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  disk.initialize';;;
+      do:  marshal.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).

new/code/github_com/goose_lang/goose/testdata/examples/semantics.v

@@ -3108,3 +3108,18 @@ Definition disabled_testWal : val :=
     let: "$r0" := ((![boolT] "ok") && ((![uint64T] (![ptrT] (struct.field_ref Log "length" "lg"))) = #(W64 0))) in
     do:  ("ok" <-[boolT] "$r0");;;
     return: (![boolT] "ok")).
+
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/semantics".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  disk.initialize';;;
+      do:  sync.initialize';;;
+      do:  primitive.initialize';;;
+      do:  (define' #()))
+      ).

new/code/github_com/goose_lang/goose/testdata/examples/unittest.v

@@ -68,6 +68,31 @@ Definition arrayToSlice : val :=
     return: (let: "$a" := "x" in
      array.slice "$a" #(W64 0) (array.len (arrayT 2 stringT)))).
 
+Definition arrayA : Z := 0.
+
+Definition arrayB : Z := 10.
+
+(* go: array.go:44:6 *)
+Definition arrayLiteralKeyed : val :=
+  rec: "arrayLiteralKeyed" <> :=
+    exception_do (let: "x" := (ref_ty (arrayT 13 stringT) (zero_val (arrayT 13 stringT))) in
+    let: "$r0" := ((let: "$ar0" := #"A" in
+    let: "$ar1" := #"3" in
+    let: "$ar2" := (zero_val stringT) in
+    let: "$ar3" := (zero_val stringT) in
+    let: "$ar4" := (zero_val stringT) in
+    let: "$ar5" := (zero_val stringT) in
+    let: "$ar6" := (zero_val stringT) in
+    let: "$ar7" := (zero_val stringT) in
+    let: "$ar8" := (zero_val stringT) in
+    let: "$ar9" := (zero_val stringT) in
+    let: "$ar10" := #"B" in
+    let: "$ar11" := #"1" in
+    let: "$ar12" := #"2" in
+    array.literal ["$ar0"; "$ar1"; "$ar2"; "$ar3"; "$ar4"; "$ar5"; "$ar6"; "$ar7"; "$ar8"; "$ar9"; "$ar10"; "$ar11"; "$ar12"])) in
+    do:  ("x" <-[arrayT 13 stringT] "$r0");;;
+    return: (![stringT] (array.elem_ref stringT (![arrayT 13 stringT] "x") #(W64 0)))).
+
 (* go: chan.go:5:6 *)
 Definition chanBasic : val :=
   rec: "chanBasic" <> :=
@@ -891,6 +916,37 @@ Definition Dec__mset_ptr : list (string * val) := [
   ("consume", Dec__consume%V)
 ].
 
+(* go: globals.go:3:6 *)
+Definition foo : val :=
+  rec: "foo" <> :=
+    exception_do (return: (#(W64 10))).
+
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/unittest".
+
+Definition GlobalX : (string * string) := (pkg_name', "GlobalX").
+
+Definition globalY : (string * string) := (pkg_name', "globalY").
+
+Definition globalA : (string * string) := (pkg_name', "globalA").
+
+Definition globalB : (string * string) := (pkg_name', "globalB").
+
+(* go: globals.go:14:6 *)
+Definition other : val :=
+  rec: "other" <> :=
+    exception_do (let: "$r0" := #"ok" in
+    do:  ((globals.get globalY #()) <-[stringT] "$r0")).
+
+(* go: globals.go:18:6 *)
+Definition bar : val :=
+  rec: "bar" <> :=
+    exception_do (do:  (other #());;;
+    (if: ((![uint64T] (globals.get GlobalX #())) ≠ #(W64 10)) || ((![stringT] (globals.get globalY #())) ≠ #"ok")
+    then
+      do:  (let: "$a0" := (interface.make string__mset #"bad") in
+      Panic "$a0")
+    else do:  #())).
+
 (* go: higher_order.go:3:6 *)
 Definition TakesFunctionType : val :=
   rec: "TakesFunctionType" "f" :=
@@ -2408,3 +2464,37 @@ Definition testVariadicPassThrough : val :=
     let: "$sl1" := "$ret3" in
     slice.literal byteT ["$sl0"; "$sl1"])) in
     variadicFunc "$a0" "$a1" "$a2")).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  (globals.put globalB (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put globalA (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put globalY (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put GlobalX (ref_ty uint64T (zero_val uint64T)))).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  marshal.initialize';;;
+      do:  log.initialize';;;
+      do:  disk.initialize';;;
+      do:  primitive.initialize';;;
+      do:  sync.initialize';;;
+      do:  fmt.initialize';;;
+      do:  (define' #());;;
+      let: "$r0" := (foo #()) in
+      do:  ((globals.get GlobalX #()) <-[uint64T] "$r0");;;
+      let: "$r0" := #"a" in
+      do:  ((globals.get globalA #()) <-[stringT] "$r0");;;
+      let: "$r0" := #"b" in
+      do:  ((globals.get globalB #()) <-[stringT] "$r0");;;
+      let: "$r0" := (foo #()) in
+      do:  ((λ: <>,
+        exception_do (let: "$r0" := (![uint64T] (globals.get GlobalX #())) in
+        do:  ((globals.get GlobalX #()) <-[uint64T] "$r0"))
+        ) #());;;
+      do:  ((λ: <>,
+        exception_do (let: "$r0" := #"" in
+        do:  ((globals.get globalY #()) <-[stringT] "$r0"))
+        ) #()))
+      ).

new/code/github_com/goose_lang/std.v

@@ -229,4 +229,18 @@ Definition Skip : val :=
   rec: "Skip" <> :=
     exception_do (do:  #()).
 
+Definition pkg_name' : string := "github.com/goose-lang/std".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  primitive.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).
+
 End code.

new/code/github_com/mit_pdos/gokv/asyncfile.v

@@ -169,3 +169,18 @@ Definition MakeAsyncFile : val :=
     let: "$go" := (AsyncFile__flushThread (![ptrT] "s")) in
     do:  (Fork ("$go" #()));;;
     return: (![sliceT] "data", ![ptrT] "s")).
+
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/asyncfile".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  grove_ffi.initialize';;;
+      do:  std.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).

new/code/github_com/mit_pdos/gokv/bank.v

@@ -249,4 +249,20 @@ Definition MakeBankClerk : val :=
      let: "$a3" := (![sliceT] "accts") in
      MakeBankClerkSlice "$a0" "$a1" "$a2" "$a3")).
 
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/bank".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  marshal.initialize';;;
+      do:  lockservice.initialize';;;
+      do:  kv.initialize';;;
+      do:  primitive.initialize';;;
+      do:  (define' #()))
+      ).
+
 End code.

new/code/github_com/mit_pdos/gokv/cachekv.v

@@ -222,3 +222,19 @@ Definition Make : val :=
        "mu" ::= "$mu";
        "cache" ::= "$cache"
      }]))).
+
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/cachekv".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  marshal.initialize';;;
+      do:  kv.initialize';;;
+      do:  grove_ffi.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).

new/code/github_com/mit_pdos/gokv/globals_test.v

@@ -0,0 +1,70 @@
+(* autogenerated from github.com/mit-pdos/gokv/globals_test *)
+From New.golang Require Import defn.
+
+Section code.
+Context `{ffi_syntax}.
+
+(* go: globals.go:3:6 *)
+Definition foo : val :=
+  rec: "foo" <> :=
+    exception_do (return: (#(W64 10))).
+
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/globals_test".
+
+Definition GlobalX : (string * string) := (pkg_name', "GlobalX").
+
+Definition globalY : (string * string) := (pkg_name', "globalY").
+
+Definition globalA : (string * string) := (pkg_name', "globalA").
+
+Definition globalB : (string * string) := (pkg_name', "globalB").
+
+(* go: globals.go:12:6 *)
+Definition other : val :=
+  rec: "other" <> :=
+    exception_do (let: "$r0" := #"ok" in
+    do:  ((globals.get globalY #()) <-[stringT] "$r0")).
+
+(* go: globals.go:16:6 *)
+Definition bar : val :=
+  rec: "bar" <> :=
+    exception_do (do:  (other #());;;
+    (if: ((![uint64T] (globals.get GlobalX #())) ≠ #(W64 10)) || ((![stringT] (globals.get globalY #())) ≠ #"ok")
+    then
+      do:  (let: "$a0" := (interface.make string__mset #"bad") in
+      Panic "$a0")
+    else do:  #())).
+
+(* go: globals.go:31:6 *)
+Definition main : val :=
+  rec: "main" <> :=
+    exception_do (do:  (bar #())).
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  (globals.put globalB (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put globalA (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put globalY (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put GlobalX (ref_ty uint64T (zero_val uint64T)))).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  (define' #());;;
+      let: "$r0" := (foo #()) in
+      do:  ((globals.get GlobalX #()) <-[uint64T] "$r0");;;
+      let: "$r0" := #"a" in
+      do:  ((globals.get globalA #()) <-[stringT] "$r0");;;
+      let: "$r0" := #"b" in
+      do:  ((globals.get globalB #()) <-[stringT] "$r0");;;
+      do:  ((λ: <>,
+        exception_do (let: "$r0" := (![uint64T] (globals.get GlobalX #())) in
+        do:  ((globals.get GlobalX #()) <-[uint64T] "$r0"))
+        ) #());;;
+      do:  ((λ: <>,
+        exception_do (let: "$r0" := #"" in
+        do:  ((globals.get globalY #()) <-[stringT] "$r0"))
+        ) #()))
+      ).
+
+End code.

new/code/github_com/mit_pdos/gokv/kv.v

@@ -8,4 +8,16 @@ Definition Kv : go_type := interfaceT.
 
 Definition KvCput : go_type := interfaceT.
 
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/kv".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  (define' #()))
+      ).
+
 End code.

new/code/github_com/mit_pdos/gokv/lockservice.v

@@ -46,4 +46,17 @@ Definition MakeLockClerk : val :=
        "kv" ::= "$kv"
      }]))).
 
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/lockservice".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  kv.initialize';;;
+      do:  (define' #()))
+      ).
+
 End code.

new/code/github_com/mit_pdos/gokv/reconnectclient.v

@@ -108,3 +108,19 @@ Definition MakeReconnectingClient : val :=
     let: "$r0" := (![uint64T] "addr") in
     do:  ((struct.field_ref ReconnectingClient "addr" (![ptrT] "r")) <-[uint64T] "$r0");;;
     return: (![ptrT] "r")).
+
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/reconnectclient".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  urpc.initialize';;;
+      do:  grove_ffi.initialize';;;
+      do:  primitive.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).

new/code/github_com/mit_pdos/gokv/urpc.v

@@ -403,3 +403,21 @@ Definition MakeClient : val :=
     return: (![ptrT] "cl")).
 
 Definition Error : go_type := uint64T.
+
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/urpc".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  marshal.initialize';;;
+      do:  grove_ffi.initialize';;;
+      do:  std.initialize';;;
+      do:  primitive.initialize';;;
+      do:  sync.initialize';;;
+      do:  log.initialize';;;
+      do:  (define' #()))
+      ).

new/code/github_com/mit_pdos/gokv/vrsm/paxos.v

@@ -956,3 +956,23 @@ Definition StartServer : val :=
     do:  (let: "$a0" := (![uint64T] "me") in
     (urpc.Server__Serve (![ptrT] "r")) "$a0");;;
     return: (![ptrT] "s")).
+
+Definition pkg_name' : string := "github.com/mit-pdos/gokv/vrsm/paxos".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  urpc.initialize';;;
+      do:  asyncfile.initialize';;;
+      do:  std.initialize';;;
+      do:  sync.initialize';;;
+      do:  log.initialize';;;
+      do:  marshal.initialize';;;
+      do:  reconnectclient.initialize';;;
+      do:  grove_ffi.initialize';;;
+      do:  (define' #()))
+      ).