Translate atomic.Pointer methods using generics

goose.go

@@ -524,10 +524,22 @@ func (ctx Ctx) selectorMethod(f *ast.SelectorExpr, call *ast.CallExpr) coq.Expr
 	namedTy := deref.(*types.Named)
 	tyName := ctx.qualifiedName(namedTy.Obj())
 	callArgs := append([]ast.Expr{f.X}, args...)
+	var typeArgs []coq.Expr
+	// TODO: this passes the struct's generic type arguments only for
+	// *atomic.Pointer[T]. We need to do this in general (including for method
+	// calls through a pointer) since structs that are generic will use the
+	// struct type arguments in the model.
+	if isPointerToAtomicPointer(selectorType) {
+		// get the type arguments to the atomic.Pointer
+		atomicPointerTy := selectorType.(*types.Pointer).Elem().(*types.Named)
+		typeArgs = append(typeArgs, ctx.typeList(call, atomicPointerTy.TypeArgs())...)
+	}
+	// append the type arguments specific to this function
+	typeArgs = append(typeArgs, ctx.typeList(call, ctx.info.Instances[f.Sel].TypeArgs)...)
 	fullName := coq.MethodName(tyName, f.Sel.Name)
 	ctx.dep.addDep(fullName)
 	coqCall := ctx.coqRecurFunc(fullName, f.Sel)
-	return ctx.newCoqCallWithExpr(coqCall, callArgs)
+	return ctx.newCoqCallTypeArgs(coqCall, typeArgs, callArgs)
 }
 
 func (ctx Ctx) newCoqCallTypeArgs(method coq.Expr, typeArgs []coq.Expr,
@@ -1031,16 +1043,6 @@ func (ctx Ctx) nilExpr(e *ast.Ident) coq.Expr {
 	}
 }
 
-func isAtomicPointerType(t types.Type) bool {
-	if t, ok := t.(*types.Named); ok {
-		obj := t.Obj()
-		if obj.Pkg().Path() == "sync/atomic" && obj.Name() == "Pointer" {
-			return true
-		}
-	}
-	return false
-}
-
 func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
 	if e.Op == token.NOT {
 		return coq.NotExpr{X: ctx.expr(e.X)}
@@ -1058,7 +1060,7 @@ func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
 			}
 		}
 		if isAtomicPointerType(ctx.typeOf(e.X)) {
-			ctx.unsupported(e, "allocate atomic.Pointer")
+			return coq.RefZeroExpr{Ty: ctx.coqTypeOfType(e, ctx.typeOf(e.X))}
 		}
 		if info, ok := ctx.getStructInfo(ctx.typeOf(e.X)); ok {
 			structLit, ok := e.X.(*ast.CompositeLit)
@@ -1565,8 +1567,7 @@ func (ctx Ctx) varSpec(s *ast.ValueSpec) coq.Binding {
 	var rhs coq.Expr
 	if len(s.Values) == 0 {
 		ty := ctx.typeOf(lhs)
-		rhs = coq.NewCallExpr(coq.GallinaIdent("ref"),
-			coq.NewCallExpr(coq.GallinaIdent("zero_val"), ctx.coqTypeOfType(s, ty)))
+		rhs = coq.RefZeroExpr{Ty: ctx.coqTypeOfType(s, ty)}
 	} else {
 		rhs = ctx.referenceTo(s.Values[0])
 	}

internal/coq/coq.go

@@ -802,6 +802,14 @@ func (e RefExpr) Coq(needs_paren bool) string {
 	return NewCallExpr(GallinaIdent("ref_to"), e.Ty, e.X).Coq(needs_paren)
 }
 
+type RefZeroExpr struct {
+	Ty Expr
+}
+
+func (e RefZeroExpr) Coq(needs_paren bool) string {
+	return NewCallExpr(GallinaIdent("ref"), NewCallExpr(GallinaIdent("zero_val"), e.Ty)).Coq(needs_paren)
+}
+
 type StoreStmt struct {
 	Dst Expr
 	Ty  Expr

internal/examples/semantics/semantics.gold.v

@@ -121,11 +121,10 @@ Definition testAtomicLoadStore64: val :=
 
 Definition testAtomicPointers: val :=
   rec: "testAtomicPointers" <> :=
-    let: "p" := struct.new atomic.Pointer [
-    ] in
+    let: "p" := ref (zero_val ptrT) in
     let: "x" := ref (zero_val uint64T) in
-    atomic.Pointer__Store "p" "x";;
-    let: "y" := atomic.Pointer__Load "p" in
+    atomic.Pointer__Store uint64T "p" "x";;
+    let: "y" := atomic.Pointer__Load uint64T "p" in
     "y" <-[uint64T] #1;;
     let: "ok" := ref_to boolT #true in
     "ok" <-[boolT] ((![boolT] "ok") && ((![uint64T] "x") = #1));;

types.go

@@ -103,6 +103,10 @@ func (ctx Ctx) coqTypeOfType(n ast.Node, t types.Type) coq.Type {
 		if t.Obj().Pkg().Name() == "disk" && t.Obj().Name() == "Disk" {
 			return coq.TypeIdent("disk.Disk")
 		}
+		// atomic.Pointer[T]
+		if t.Obj().Pkg().Name() == "atomic" && t.Obj().Name() == "Pointer" {
+			return coq.TypeIdent("ptrT")
+		}
 		if info, ok := ctx.getStructInfo(t); ok {
 			return coq.StructName(info.name)
 		}
@@ -283,6 +287,23 @@ func isDisk(t types.Type) bool {
 	return false
 }
 
+func isAtomicPointerType(t types.Type) bool {
+	if t, ok := t.(*types.Named); ok {
+		obj := t.Obj()
+		if obj.Pkg().Path() == "sync/atomic" && obj.Name() == "Pointer" {
+			return true
+		}
+	}
+	return false
+}
+
+func isPointerToAtomicPointer(t types.Type) bool {
+	if t, ok := t.(*types.Pointer); ok {
+		return isAtomicPointerType(t.Elem())
+	}
+	return false
+}
+
 type intTypeInfo struct {
 	width     int
 	isUntyped bool