Remove some special casing for imports

goose.go

@@ -330,49 +330,6 @@ func (ctx Ctx) capExpr(e *ast.CallExpr) glang.CallExpr {
 	return glang.CallExpr{}
 }
 
-func (ctx Ctx) lockMethod(f *ast.SelectorExpr) glang.CallExpr {
-	l := ctx.expr(f.X)
-	switch f.Sel.Name {
-	case "Lock":
-		return glang.NewCallExpr(glang.GallinaIdent("lock.acquire"), l)
-	case "Unlock":
-		return glang.NewCallExpr(glang.GallinaIdent("lock.release"), l)
-	default:
-		ctx.nope(f, "method %s of sync.Mutex", ctx.printGo(f))
-		return glang.CallExpr{}
-	}
-}
-
-func (ctx Ctx) condVarMethod(f *ast.SelectorExpr) glang.CallExpr {
-	l := ctx.expr(f.X)
-	switch f.Sel.Name {
-	case "Signal":
-		return glang.NewCallExpr(glang.GallinaIdent("lock.condSignal"), l)
-	case "Broadcast":
-		return glang.NewCallExpr(glang.GallinaIdent("lock.condBroadcast"), l)
-	case "Wait":
-		return glang.NewCallExpr(glang.GallinaIdent("lock.condWait"), l)
-	default:
-		ctx.unsupported(f, "method %s of sync.Cond", f.Sel.Name)
-		return glang.CallExpr{}
-	}
-}
-
-func (ctx Ctx) waitGroupMethod(f *ast.SelectorExpr, args []ast.Expr) glang.CallExpr {
-	callArgs := append([]ast.Expr{f.X}, args...)
-	switch f.Sel.Name {
-	case "Add":
-		return ctx.newCoqCall("waitgroup.Add", callArgs)
-	case "Done":
-		return ctx.newCoqCall("waitgroup.Done", callArgs)
-	case "Wait":
-		return ctx.newCoqCall("waitgroup.Wait", callArgs)
-	default:
-		ctx.unsupported(f, "method %s of sync.WaitGroup", f.Sel.Name)
-		return glang.CallExpr{}
-	}
-}
-
 func (ctx Ctx) prophIdMethod(f *ast.SelectorExpr, args []ast.Expr) glang.CallExpr {
 	callArgs := append([]ast.Expr{f.X}, args...)
 	switch f.Sel.Name {
@@ -449,12 +406,6 @@ func (ctx Ctx) packageMethod(f *ast.SelectorExpr,
 			return glang.LoggingStmt{GoCall: ctx.printGo(call)}
 		}
 	}
-	if isIdent(f.X, "sync") {
-		switch f.Sel.Name {
-		case "NewCond":
-			return ctx.newCoqCall("lock.newCond", args)
-		}
-	}
 	pkg := f.X.(*ast.Ident)
 	return ctx.newCoqCallTypeArgs(
 		glang.GallinaIdent(glang.PackageIdent{Package: pkg.Name, Ident: f.Sel.Name}.Coq(true)),
@@ -469,18 +420,6 @@ func (ctx Ctx) selectorMethod(f *ast.SelectorExpr,
 	if !ok {
 		return ctx.packageMethod(f, call)
 	}
-	if isLockRef(selectorType) {
-		return ctx.lockMethod(f)
-	}
-	if isCFMutexRef(selectorType) {
-		return ctx.lockMethod(f)
-	}
-	if isCondVar(selectorType) {
-		return ctx.condVarMethod(f)
-	}
-	if isWaitGroup(selectorType) {
-		return ctx.waitGroupMethod(f, args)
-	}
 	if isProphId(selectorType) {
 		return ctx.prophIdMethod(f, args)
 	}
@@ -654,17 +593,6 @@ func (ctx Ctx) makeExpr(args []ast.Expr) glang.CallExpr {
 
 // newExpr parses a call to new() into an appropriate allocation
 func (ctx Ctx) newExpr(s ast.Node, ty ast.Expr) glang.CallExpr {
-	if sel, ok := ty.(*ast.SelectorExpr); ok {
-		if isIdent(sel.X, "sync") && isIdent(sel.Sel, "Mutex") {
-			return glang.NewCallExpr(glang.GallinaIdent("lock.new"))
-		}
-		if isIdent(sel.X, "sync") && isIdent(sel.Sel, "WaitGroup") {
-			return glang.NewCallExpr(glang.GallinaIdent("waitgroup.New"))
-		}
-		if isIdent(sel.X, "cfmutex") && isIdent(sel.Sel, "CFMutex") {
-			return glang.NewCallExpr(glang.GallinaIdent("lock.new"))
-		}
-	}
 	if t, ok := ctx.typeOf(ty).(*types.Array); ok {
 		return glang.NewCallExpr(glang.GallinaIdent("zero_array"),
 			ctx.coqTypeOfType(ty, t.Elem()),
@@ -2028,7 +1956,6 @@ var builtinImports = map[string]bool{
 	"github.com/tchajed/goose/machine/async_disk": true,
 	"github.com/mit-pdos/gokv/time":               true,
 	"github.com/mit-pdos/vmvcc/cfmutex":           true,
-	"sync":                                        true,
 	"log":                                         true,
 	"fmt":                                         true,
 }
@@ -2055,6 +1982,7 @@ func (ctx Ctx) imports(d []ast.Spec) []glang.Decl {
 			pkgNameIndex := strings.LastIndex(importPath, "/") + 1
 			pkgName := importPath[pkgNameIndex:]
 
+			// FIXME: eliminate special case for "trusted"
 			if strings.HasPrefix(pkgName, "trusted_") {
 				decls = append(decls, glang.ImportDecl{Path: importPath, Trusted: true})
 			} else {

internal/examples/append_log/append_log.gold.v

@@ -1,6 +1,7 @@
 (* autogenerated from github.com/tchajed/goose/internal/examples/append_log *)
 From Perennial.goose_lang Require Import prelude.
-From Goose Require github_com.tchajed.marshal.
+From Goose Require github_dot_com.tchajed.marshal.
+From Goose Require sync.
 
 From Perennial.goose_lang Require Import ffi.disk_prelude.
 
@@ -67,9 +68,9 @@ Definition Log__get: val :=
 
 Definition Log__Get: val :=
   rec: "Log__Get" "log" "i" :=
-    lock.acquire (struct.loadF Log "m" "log");;
+    sync.Mutex__Lock (struct.loadF Log "m" "log");;
     let: ("v", "b") := Log__get "log" "i" in
-    lock.release (struct.loadF Log "m" "log");;
+    sync.Mutex__Unlock (struct.loadF Log "m" "log");;
     ("v", "b").
 
 Definition writeAll: val :=
@@ -91,9 +92,9 @@ Definition Log__append: val :=
 
 Definition Log__Append: val :=
   rec: "Log__Append" "log" "bks" :=
-    lock.acquire (struct.loadF Log "m" "log");;
+    sync.Mutex__Lock (struct.loadF Log "m" "log");;
     let: "b" := Log__append "log" "bks" in
-    lock.release (struct.loadF Log "m" "log");;
+    sync.Mutex__Unlock (struct.loadF Log "m" "log");;
     "b".
 
 Definition Log__reset: val :=
@@ -104,7 +105,7 @@ Definition Log__reset: val :=
 
 Definition Log__Reset: val :=
   rec: "Log__Reset" "log" :=
-    lock.acquire (struct.loadF Log "m" "log");;
+    sync.Mutex__Lock (struct.loadF Log "m" "log");;
     Log__reset "log";;
-    lock.release (struct.loadF Log "m" "log");;
+    sync.Mutex__Unlock (struct.loadF Log "m" "log");;
     #().

internal/examples/logging2/logging2.gold.v

@@ -1,5 +1,6 @@
 (* autogenerated from github.com/tchajed/goose/internal/examples/logging2 *)
 From Perennial.goose_lang Require Import prelude.
+From Goose Require sync.
 
 From Perennial.goose_lang Require Import ffi.disk_prelude.
 
@@ -62,10 +63,10 @@ Definition Log__readBlocks: val :=
 
 Definition Log__Read: val :=
   rec: "Log__Read" "log" :=
-    lock.acquire (struct.get Log "logLock" "log");;
+    sync.Mutex__Lock (struct.get Log "logLock" "log");;
     let: "disklen" := Log__readHdr "log" in
     let: "blks" := Log__readBlocks "log" "disklen" in
-    lock.release (struct.get Log "logLock" "log");;
+    sync.Mutex__Unlock (struct.get Log "logLock" "log");;
     "blks".
 
 Definition Log__memWrite: val :=
@@ -79,25 +80,25 @@ Definition Log__memWrite: val :=
 
 Definition Log__memAppend: val :=
   rec: "Log__memAppend" "log" "l" :=
-    lock.acquire (struct.get Log "memLock" "log");;
+    sync.Mutex__Lock (struct.get Log "memLock" "log");;
     (if: ((![uint64T] (struct.get Log "memLen" "log")) + (slice.len "l")) ≥ (struct.get Log "logSz" "log")
     then
-      lock.release (struct.get Log "memLock" "log");;
+      sync.Mutex__Unlock (struct.get Log "memLock" "log");;
       (#false, #0)
     else
       let: "txn" := ![uint64T] (struct.get Log "memTxnNxt" "log") in
       let: "n" := (![uint64T] (struct.get Log "memLen" "log")) + (slice.len "l") in
       (struct.get Log "memLen" "log") <-[uint64T] "n";;
       (struct.get Log "memTxnNxt" "log") <-[uint64T] ((![uint64T] (struct.get Log "memTxnNxt" "log")) + #1);;
-      lock.release (struct.get Log "memLock" "log");;
+      sync.Mutex__Unlock (struct.get Log "memLock" "log");;
       (#true, "txn")).
 
 (* XXX just an atomic read? *)
 Definition Log__readLogTxnNxt: val :=
   rec: "Log__readLogTxnNxt" "log" :=
-    lock.acquire (struct.get Log "memLock" "log");;
+    sync.Mutex__Lock (struct.get Log "memLock" "log");;
     let: "n" := ![uint64T] (struct.get Log "logTxnNxt" "log") in
-    lock.release (struct.get Log "memLock" "log");;
+    sync.Mutex__Unlock (struct.get Log "memLock" "log");;
     "n".
 
 Definition Log__diskAppendWait: val :=
@@ -130,18 +131,18 @@ Definition Log__writeBlocks: val :=
 
 Definition Log__diskAppend: val :=
   rec: "Log__diskAppend" "log" :=
-    lock.acquire (struct.get Log "logLock" "log");;
+    sync.Mutex__Lock (struct.get Log "logLock" "log");;
     let: "disklen" := Log__readHdr "log" in
-    lock.acquire (struct.get Log "memLock" "log");;
+    sync.Mutex__Lock (struct.get Log "memLock" "log");;
     let: "memlen" := ![uint64T] (struct.get Log "memLen" "log") in
     let: "allblks" := ![slice.T (slice.T byteT)] (struct.get Log "memLog" "log") in
     let: "blks" := SliceSkip (slice.T byteT) "allblks" "disklen" in
     let: "memnxt" := ![uint64T] (struct.get Log "memTxnNxt" "log") in
-    lock.release (struct.get Log "memLock" "log");;
+    sync.Mutex__Unlock (struct.get Log "memLock" "log");;
     Log__writeBlocks "log" "blks" "disklen";;
     Log__writeHdr "log" "memlen";;
     (struct.get Log "logTxnNxt" "log") <-[uint64T] "memnxt";;
-    lock.release (struct.get Log "logLock" "log");;
+    sync.Mutex__Unlock (struct.get Log "logLock" "log");;
     #().
 
 Definition Log__Logger: val :=

internal/examples/semantics/semantics.gold.v

@@ -1,5 +1,6 @@
 (* autogenerated from github.com/tchajed/goose/internal/examples/semantics *)
 From Perennial.goose_lang Require Import prelude.
+From Goose Require sync.
 
 From Perennial.goose_lang Require Import ffi.disk_prelude.
 
@@ -513,8 +514,8 @@ Definition testIfStmtInterface: val :=
 Definition testsUseLocks: val :=
   rec: "testsUseLocks" <> :=
     let: "m" := lock.new #() in
-    lock.acquire "m";;
-    lock.release "m";;
+    sync.Mutex__Lock "m";;
+    sync.Mutex__Unlock "m";;
     #true.
 
 (* loops.go *)
@@ -983,9 +984,9 @@ Definition testShiftMod: val :=
 Definition testLinearize: val :=
   rec: "testLinearize" <> :=
     let: "m" := lock.new #() in
-    lock.acquire "m";;
+    sync.Mutex__Lock "m";;
     Linearize;;
-    lock.release "m";;
+    sync.Mutex__Unlock "m";;
     #true.
 
 (* shortcircuiting.go *)
@@ -1430,12 +1431,12 @@ Definition New: val :=
 
 Definition Log__lock: val :=
   rec: "Log__lock" "l" :=
-    lock.acquire (struct.get Log "l" "l");;
+    sync.Mutex__Lock (struct.get Log "l" "l");;
     #().
 
 Definition Log__unlock: val :=
   rec: "Log__unlock" "l" :=
-    lock.release (struct.get Log "l" "l");;
+    sync.Mutex__Unlock (struct.get Log "l" "l");;
     #().
 
 (* BeginTxn allocates space for a new transaction in the log.

internal/examples/simpledb/simpledb.gold.v

@@ -1,6 +1,7 @@
 (* autogenerated from github.com/tchajed/goose/internal/examples/simpledb *)
 From Perennial.goose_lang Require Import prelude.
-From Goose Require github_com.tchajed.marshal.
+From Goose Require github_dot_com.tchajed.marshal.
+From Goose Require sync.
 
 Section code.
 Context `{ext_ty: ext_types}.
@@ -310,26 +311,26 @@ Definition NewDb: val :=
    Reflects any completed in-memory writes. *)
 Definition Read: val :=
   rec: "Read" "db" "k" :=
-    lock.acquire (struct.get Database "bufferL" "db");;
+    sync.Mutex__Lock (struct.get Database "bufferL" "db");;
     let: "buf" := ![mapT (slice.T byteT)] (struct.get Database "wbuffer" "db") in
     let: ("v", "ok") := MapGet "buf" "k" in
     (if: "ok"
     then
-      lock.release (struct.get Database "bufferL" "db");;
+      sync.Mutex__Unlock (struct.get Database "bufferL" "db");;
       ("v", #true)
     else
       let: "rbuf" := ![mapT (slice.T byteT)] (struct.get Database "rbuffer" "db") in
       let: ("v2", "ok") := MapGet "rbuf" "k" in
       (if: "ok"
       then
-        lock.release (struct.get Database "bufferL" "db");;
+        sync.Mutex__Unlock (struct.get Database "bufferL" "db");;
         ("v2", #true)
       else
-        lock.acquire (struct.get Database "tableL" "db");;
+        sync.Mutex__Lock (struct.get Database "tableL" "db");;
         let: "tbl" := struct.load Table (struct.get Database "table" "db") in
         let: ("v3", "ok") := tableRead "tbl" "k" in
-        lock.release (struct.get Database "tableL" "db");;
-        lock.release (struct.get Database "bufferL" "db");;
+        sync.Mutex__Unlock (struct.get Database "tableL" "db");;
+        sync.Mutex__Unlock (struct.get Database "bufferL" "db");;
         ("v3", "ok"))).
 
 (* Write sets a key to a new value.
@@ -340,10 +341,10 @@ Definition Read: val :=
    The new value is buffered in memory. To persist it, call db.Compact(). *)
 Definition Write: val :=
   rec: "Write" "db" "k" "v" :=
-    lock.acquire (struct.get Database "bufferL" "db");;
+    sync.Mutex__Lock (struct.get Database "bufferL" "db");;
     let: "buf" := ![mapT (slice.T byteT)] (struct.get Database "wbuffer" "db") in
     MapInsert "buf" "k" "v";;
-    lock.release (struct.get Database "bufferL" "db");;
+    sync.Mutex__Unlock (struct.get Database "bufferL" "db");;
     #().
 
 Definition freshTable: val :=
@@ -418,14 +419,14 @@ Definition constructNewTable: val :=
    writes with existing writes. *)
 Definition Compact: val :=
   rec: "Compact" "db" :=
-    lock.acquire (struct.get Database "compactionL" "db");;
-    lock.acquire (struct.get Database "bufferL" "db");;
+    sync.Mutex__Lock (struct.get Database "compactionL" "db");;
+    sync.Mutex__Lock (struct.get Database "bufferL" "db");;
     let: "buf" := ![mapT (slice.T byteT)] (struct.get Database "wbuffer" "db") in
     let: "emptyWbuffer" := NewMap uint64T (slice.T byteT) #() in
     (struct.get Database "wbuffer" "db") <-[mapT (slice.T byteT)] "emptyWbuffer";;
     (struct.get Database "rbuffer" "db") <-[mapT (slice.T byteT)] "buf";;
-    lock.release (struct.get Database "bufferL" "db");;
-    lock.acquire (struct.get Database "tableL" "db");;
+    sync.Mutex__Unlock (struct.get Database "bufferL" "db");;
+    sync.Mutex__Lock (struct.get Database "tableL" "db");;
     let: "oldTableName" := ![stringT] (struct.get Database "tableName" "db") in
     let: ("oldTable", "t") := constructNewTable "db" "buf" in
     let: "newTable" := freshTable "oldTableName" in
@@ -435,8 +436,8 @@ Definition Compact: val :=
     FS.atomicCreate #(str"db") #(str"manifest") "manifestData";;
     CloseTable "oldTable";;
     FS.delete #(str"db") "oldTableName";;
-    lock.release (struct.get Database "tableL" "db");;
-    lock.release (struct.get Database "compactionL" "db");;
+    sync.Mutex__Unlock (struct.get Database "tableL" "db");;
+    sync.Mutex__Unlock (struct.get Database "compactionL" "db");;
     #().
 
 Definition recoverManifest: val :=
@@ -505,12 +506,12 @@ Definition Recover: val :=
    cleanly closing any open files. *)
 Definition Shutdown: val :=
   rec: "Shutdown" "db" :=
-    lock.acquire (struct.get Database "bufferL" "db");;
-    lock.acquire (struct.get Database "compactionL" "db");;
+    sync.Mutex__Lock (struct.get Database "bufferL" "db");;
+    sync.Mutex__Lock (struct.get Database "compactionL" "db");;
     let: "t" := struct.load Table (struct.get Database "table" "db") in
     CloseTable "t";;
-    lock.release (struct.get Database "compactionL" "db");;
-    lock.release (struct.get Database "bufferL" "db");;
+    sync.Mutex__Unlock (struct.get Database "compactionL" "db");;
+    sync.Mutex__Unlock (struct.get Database "bufferL" "db");;
     #().
 
 (* Close closes an open database cleanly, flushing any in-memory writes.

internal/examples/trust_import/trust_import.gold.v

@@ -1,6 +1,6 @@
 (* autogenerated from github.com/tchajed/goose/internal/examples/trust_import *)
 From Perennial.goose_lang Require Import prelude.
-From Perennial.goose_lang.trusted Require Import github_com.tchajed.goose.internal.examples.trust_import.trusted_example.
+From Perennial.goose_lang.trusted Require Import github_dot_com.tchajed.goose.internal.examples.trust__import.trusted__example.
 
 Section code.
 Context `{ext_ty: ext_types}.