From 833410aa3252935aef82d8dd69f93d81c5c43c69 Mon Sep 17 00:00:00 2001 From: Upamanyu Sharma Date: Tue, 17 Dec 2024 19:49:08 -0500 Subject: [PATCH] Regoose --- .../goose/testdata/examples/unittest.v | 5 +- new/code/go_etcd_io/raft/v3.v | 68 +++++++++---------- new/code/go_etcd_io/raft/v3/tracker.v | 15 ++-- 3 files changed, 43 insertions(+), 45 deletions(-) diff --git a/new/code/github_com/goose_lang/goose/testdata/examples/unittest.v b/new/code/github_com/goose_lang/goose/testdata/examples/unittest.v index 62002b7a5..9be96835b 100644 --- a/new/code/github_com/goose_lang/goose/testdata/examples/unittest.v +++ b/new/code/github_com/goose_lang/goose/testdata/examples/unittest.v @@ -931,13 +931,13 @@ Definition globalA : (string * string) := (pkg_name', "globalA"). Definition globalB : (string * string) := (pkg_name', "globalB"). -(* go: globals.go:12:6 *) +(* 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:16:6 *) +(* go: globals.go:18:6 *) Definition bar : val := rec: "bar" <> := exception_do (do: (other #());;; @@ -2488,6 +2488,7 @@ Definition initialize' : val := 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")) diff --git a/new/code/go_etcd_io/raft/v3.v b/new/code/go_etcd_io/raft/v3.v index c0d6e0c5a..1b77d21fc 100644 --- a/new/code/go_etcd_io/raft/v3.v +++ b/new/code/go_etcd_io/raft/v3.v @@ -261,6 +261,10 @@ Definition IsEmptySnap : val := exception_do (let: "sp" := (ref_ty raftpb.Snapshot "sp") in return: ((![uint64T] (struct.field_ref raftpb.SnapshotMetadata "Index" (struct.field_ref raftpb.Snapshot "Metadata" "sp"))) = #(W64 0))). +Definition pkg_name' : string := "go.etcd.io/raft/v3". + +Definition ErrSnapshotTemporarilyUnavailable : (string * string) := (pkg_name', "ErrSnapshotTemporarilyUnavailable"). + (* go: log.go:293:19 *) Definition raftLog__snapshot : val := rec: "raftLog__snapshot" "l" <> := @@ -491,6 +495,10 @@ Definition unstable__slice : val := return: (let: "$s" := (![sliceT] (struct.field_ref unstable "entries" (![ptrT] "u"))) in slice.full_slice raftpb.Entry "$s" ((![uint64T] "lo") - (![uint64T] (struct.field_ref unstable "offset" (![ptrT] "u")))) ((![uint64T] "hi") - (![uint64T] (struct.field_ref unstable "offset" (![ptrT] "u")))) ((![uint64T] "hi") - (![uint64T] (struct.field_ref unstable "offset" (![ptrT] "u")))))). +Definition ErrUnavailable : (string * string) := (pkg_name', "ErrUnavailable"). + +Definition ErrCompacted : (string * string) := (pkg_name', "ErrCompacted"). + (* maybeLastIndex returns the last index if it has at least one unstable entry or snapshot. @@ -993,6 +1001,8 @@ Definition newReadOnly : val := "readIndexQueue" ::= zero_val sliceT }]))). +Definition globalRand : (string * string) := (pkg_name', "globalRand"). + Definition lockedRand : go_type := structT [ "mu" :: sync.Mutex ]. @@ -1080,6 +1090,8 @@ Definition raft__reset : val := newReadOnly "$a0") in do: ((struct.field_ref raft "readOnly" (![ptrT] "r")) <-[ptrT] "$r0")). +Definition stepFollowerGlobal : (string * string) := (pkg_name', "stepFollowerGlobal"). + (* go: raft.go:909:16 *) Definition raft__becomeFollower : val := rec: "raft__becomeFollower" "r" "term" "lead" := @@ -1314,6 +1326,8 @@ Definition raftLog__append : val := (unstable__truncateAndAppend (struct.field_ref raftLog "unstable" (![ptrT] "l"))) "$a0");;; return: ((raftLog__lastIndex (![ptrT] "l")) #())). +Definition emptyState : (string * string) := (pkg_name', "emptyState"). + (* Bootstrap initializes the RawNode for first use by appending configuration changes for the supplied peers. This method returns an error if the Storage is nonempty. @@ -2284,6 +2298,10 @@ Definition unstable__mset_ptr : list (string * val) := [ ("truncateAndAppend", unstable__truncateAndAppend%V) ]. +Definition raftLoggerMu : (string * string) := (pkg_name', "raftLoggerMu"). + +Definition raftLogger : (string * string) := (pkg_name', "raftLogger"). + (* go: logger.go:45:6 *) Definition SetLogger : val := rec: "SetLogger" "l" := @@ -2293,6 +2311,8 @@ Definition SetLogger : val := do: ((globals.get raftLogger #()) <-[Logger] "$r0");;; do: ((sync.Mutex__Unlock (globals.get raftLoggerMu #())) #())). +Definition defaultLogger : (string * string) := (pkg_name', "defaultLogger"). + Definition DefaultLogger : go_type := structT [ "Logger" :: ptrT; "debug" :: boolT @@ -2554,16 +2574,8 @@ Definition getLogger : val := )));;; return: (![Logger] (globals.get raftLogger #()))). -Definition pkg_name' : string := "go.etcd.io/raft/v3". - -Definition defaultLogger : (string * string) := (pkg_name', "defaultLogger"). - Definition discardLogger : (string * string) := (pkg_name', "discardLogger"). -Definition raftLoggerMu : (string * string) := (pkg_name', "raftLoggerMu"). - -Definition raftLogger : (string * string) := (pkg_name', "raftLogger"). - Definition DefaultLogger__mset : list (string * val) := [ ("Fatalln", (λ: "$recv", log.Logger__Fatalln (struct.field_get DefaultLogger "Logger" "$recv") @@ -2615,8 +2627,6 @@ Definition SnapshotFinish : expr := #(W64 1). Definition SnapshotFailure : expr := #(W64 2). -Definition emptyState : (string * string) := (pkg_name', "emptyState"). - Definition ErrStopped : (string * string) := (pkg_name', "ErrStopped"). Definition SoftState : go_type := structT [ @@ -3053,6 +3063,8 @@ Definition traceBecomeCandidate : val := Definition StateCandidate : expr := #(W64 1). +Definition stepCandidateGlobal : (string * string) := (pkg_name', "stepCandidateGlobal"). + (* go: raft.go:920:16 *) Definition raft__becomeCandidate : val := rec: "raft__becomeCandidate" "r" <> := @@ -3245,6 +3257,8 @@ Definition raft__campaign : val := }]) in (raft__send (![ptrT] "r")) "$a0")))). +Definition errBreak : (string * string) := (pkg_name', "errBreak"). + (* go: raft.go:1013:16 *) Definition raft__hasUnappliedConfChanges : val := rec: "raft__hasUnappliedConfChanges" "r" <> := @@ -4180,6 +4194,8 @@ Definition isMsgInArray : val := return: ((int_lt (![intT] "i") (let: "$a0" := (![sliceT] "arr") in slice.len "$a0")) && (![boolT] (slice.elem_ref boolT (![sliceT] "arr") (![intT] "i"))))). +Definition isLocalMsg : (string * string) := (pkg_name', "isLocalMsg"). + (* go: util.go:57:6 *) Definition IsLocalMsg : val := rec: "IsLocalMsg" "msgt" := @@ -4353,6 +4369,8 @@ Definition node__TransferLeadership : val := do: #() ))] (InjLV #()))). +Definition isResponseMsg : (string * string) := (pkg_name', "isResponseMsg"). + (* go: util.go:61:6 *) Definition IsResponseMsg : val := rec: "IsResponseMsg" "msgt" := @@ -5438,14 +5456,14 @@ Definition lockedRand__mset_ptr : list (string * val) := [ ("Intn", lockedRand__Intn%V) ]. -Definition globalRand : (string * string) := (pkg_name', "globalRand"). - Definition CampaignType__mset : list (string * val) := [ ]. Definition CampaignType__mset_ptr : list (string * val) := [ ]. +Definition stmap : (string * string) := (pkg_name', "stmap"). + (* go: raft.go:119:21 *) Definition StateType__String : val := rec: "StateType__String" "st" <> := @@ -5475,8 +5493,6 @@ Definition StateType__mset_ptr : list (string * val) := [ )%V) ]. -Definition stmap : (string * string) := (pkg_name', "stmap"). - Definition Config__mset : list (string * val) := [ ]. @@ -5718,6 +5734,8 @@ Definition traceBecomeLeader : val := exception_do (let: "" := (ref_ty ptrT "") in do: #()). +Definition stepLeaderGlobal : (string * string) := (pkg_name', "stepLeaderGlobal"). + (* go: raft.go:951:16 *) Definition raft__becomeLeader : val := rec: "raft__becomeLeader" "r" <> := @@ -6336,8 +6354,6 @@ Definition raft__mset_ptr : list (string * val) := [ ("tickHeartbeat", raft__tickHeartbeat%V) ]. -Definition errBreak : (string * string) := (pkg_name', "errBreak"). - Definition stepFunc : go_type := funcT. Definition stepFunc__mset : list (string * val) := [ @@ -6346,8 +6362,6 @@ Definition stepFunc__mset : list (string * val) := [ Definition stepFunc__mset_ptr : list (string * val) := [ ]. -Definition stepLeaderGlobal : (string * string) := (pkg_name', "stepLeaderGlobal"). - Definition readIndexStatus : go_type := structT [ "req" :: raftpb.Message; "index" :: uint64T; @@ -6990,8 +7004,6 @@ Definition stepLeader : val := else #())))));;; return: (#interface.nil)). -Definition stepCandidateGlobal : (string * string) := (pkg_name', "stepCandidateGlobal"). - (* stepCandidate is shared by StateCandidate and StatePreCandidate; the difference is whether they respond to MsgVoteResp or MsgPreVoteResp. @@ -7094,8 +7106,6 @@ Definition stepCandidate : val := else #()))))));;; return: (#interface.nil)). -Definition stepFollowerGlobal : (string * string) := (pkg_name', "stepFollowerGlobal"). - (* go: raft.go:1738:6 *) Definition stepFollower : val := rec: "stepFollower" "r" "m" := @@ -7375,6 +7385,8 @@ Definition MemoryStorage__Append : val := (interface.get "Panicf" (getLogger #())) "$a0" "$a1")));;; return: (#interface.nil)). +Definition ErrSnapOutOfDate : (string * string) := (pkg_name', "ErrSnapOutOfDate"). + (* ApplySnapshot overwrites the contents of this Storage object with those of the given snapshot. @@ -9036,14 +9048,6 @@ Definition BasicStatus__mset_ptr : list (string * val) := [ )%V) ]. -Definition ErrCompacted : (string * string) := (pkg_name', "ErrCompacted"). - -Definition ErrSnapOutOfDate : (string * string) := (pkg_name', "ErrSnapOutOfDate"). - -Definition ErrUnavailable : (string * string) := (pkg_name', "ErrUnavailable"). - -Definition ErrSnapshotTemporarilyUnavailable : (string * string) := (pkg_name', "ErrSnapshotTemporarilyUnavailable"). - Definition inMemStorageCallStats__mset : list (string * val) := [ ]. @@ -9143,10 +9147,6 @@ Definition logSlice__mset_ptr : list (string * val) := [ )%V) ]. -Definition isLocalMsg : (string * string) := (pkg_name', "isLocalMsg"). - -Definition isResponseMsg : (string * string) := (pkg_name', "isResponseMsg"). - (* go: util.go:81:6 *) Definition DescribeHardState : val := rec: "DescribeHardState" "hs" := diff --git a/new/code/go_etcd_io/raft/v3/tracker.v b/new/code/go_etcd_io/raft/v3/tracker.v index 51aba9683..d58281b38 100644 --- a/new/code/go_etcd_io/raft/v3/tracker.v +++ b/new/code/go_etcd_io/raft/v3/tracker.v @@ -427,6 +427,10 @@ Definition Progress__SentCommit : val := let: "$r0" := (![uint64T] "commit") in do: ((struct.field_ref Progress "sentCommit" (![ptrT] "pr")) <-[uint64T] "$r0")). +Definition pkg_name' : string := "go.etcd.io/raft/v3/tracker". + +Definition prstmap : (string * string) := (pkg_name', "prstmap"). + (* go: state.go:42:21 *) Definition StateType__String : val := rec: "StateType__String" "st" <> := @@ -605,10 +609,6 @@ Definition StateType__mset_ptr : list (string * val) := [ )%V) ]. -Definition pkg_name' : string := "go.etcd.io/raft/v3/tracker". - -Definition prstmap : (string * string) := (pkg_name', "prstmap"). - Definition Config : go_type := structT [ "Voters" :: quorum.JointConfig; "AutoLeave" :: boolT; @@ -1042,12 +1042,9 @@ Definition matchAckIndexer__mset_ptr : list (string * val) := [ )%V) ]. -Definition _ : (string * string) := (pkg_name', "_"). - Definition define' : val := rec: "define'" <> := - exception_do (do: (globals.put _ (ref_ty quorum.AckedIndexer (zero_val quorum.AckedIndexer)));;; - do: (globals.put prstmap (ref_ty (arrayT 3 stringT) (zero_val (arrayT 3 stringT))))). + exception_do (do: (globals.put prstmap (ref_ty (arrayT 3 stringT) (zero_val (arrayT 3 stringT))))). Definition initialize' : val := rec: "initialize'" <> := @@ -1065,7 +1062,7 @@ Definition initialize' : val := array.literal ["$ar0"; "$ar1"; "$ar2"])) in do: ((globals.get prstmap #()) <-[arrayT 3 stringT] "$r0");;; let: "$r0" := (interface.make matchAckIndexer__mset #null) in - do: ((globals.get _ #()) <-[quorum.AckedIndexer] "$r0")) + do: #()) ). End code.