Re-goose marshal without interface bug

mit-pdos · Jan 28, 2025 · 1c55501 · 1c55501
1 parent efb596e
commit 1c55501
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 6 deletions.
diff --git a/etc/update-goose.py b/etc/update-goose.py
@@ -159,11 +159,13 @@ def compile_goose():
         do_run(["go", "install", "./cmd/goose"])
         os.chdir(old_dir)
 
-    def run_goose(src_path, *pkgs):
+    def run_goose(src_path, *pkgs, extra_args=None):
         if src_path is None:
             return
         if not pkgs:
             pkgs = ["."]
+        if not extra_args:
+            extra_args = []
 
         gopath = os.getenv("GOPATH", default=None)
         if gopath is None or gopath == "":
@@ -174,6 +176,7 @@ def run_goose(src_path, *pkgs):
         output = path.join(perennial_dir, "external/Goose")
         args.extend(["-out", output])
         args.extend(["-dir", src_path])
+        args.extend(extra_args)
         args.extend(pkgs)
         do_run(args)
 
@@ -350,7 +353,7 @@ def run_goose(src_path, *pkgs):
         "./util",
     )
 
-    run_goose(marshal_dir, ".")
+    run_goose(marshal_dir, ".", extra_args=["-skip-interfaces"])
 
     run_goose(std_dir, ".")
 

diff --git a/external/Goose/github_com/tchajed/marshal.v b/external/Goose/github_com/tchajed/marshal.v
@@ -233,7 +233,7 @@ Definition WriteSlice (T:ty): val :=
   rec: "WriteSlice" "b" "xs" "writeOne" :=
     let: "b2" := ref_to (slice.T byteT) "b" in
     ForSlice T <> "x" "xs"
-      ("b2" <-[slice.T byteT] ("writeOne" "x" (![slice.T byteT] "b2")));;
+      ("b2" <-[slice.T byteT] ("writeOne" (![slice.T byteT] "b2") "x"));;
     ![slice.T byteT] "b2".
 
 Definition WriteSliceLenPrefix (T:ty): val :=

diff --git a/new/code/github_com/tchajed/marshal.v b/new/code/github_com/tchajed/marshal.v
@@ -547,8 +547,8 @@ Definition WriteSlice (T: go_type) : val :=
     do:  (let: "$range" := (![sliceT] "xs") in
     slice.for_range T "$range" (λ: <> "x",
       let: "x" := ref_ty T "x" in
-      let: "$r0" := (let: "$a0" := (![T] "x") in
-      let: "$a1" := (![sliceT] "b2") in
+      let: "$r0" := (let: "$a0" := (![sliceT] "b2") in
+      let: "$a1" := (![T] "x") in
       (![funcT] "writeOne") "$a0" "$a1") in
       do:  ("b2" <-[sliceT] "$r0")));;;
     return: (![sliceT] "b2")).

diff --git a/new/etc/update-goose-new.py b/new/etc/update-goose-new.py
@@ -98,11 +98,13 @@ def compile_goose():
         do_run(["go", "install", "./cmd/recordgen"])
         os.chdir(old_dir)
 
-    def run_goose(src_path, *pkgs):
+    def run_goose(src_path, *pkgs, extra_args=None):
         if src_path is None:
             return
         if not pkgs:
             pkgs = ["."]
+        if not extra_args:
+            extra_args = []
 
         gopath = os.getenv("GOPATH", default=None)
         if gopath is None or gopath == "":
@@ -113,6 +115,7 @@ def run_goose(src_path, *pkgs):
         output = path.join(perennial_dir, "new/code/")
         args.extend(["-out", output])
         args.extend(["-dir", src_path])
+        args.extend(extra_args)
         args.extend(pkgs)
         do_run(args)