Merge pull request #57 from goose-lang/tchajed/atomic-pointer

Add support for atomic.Pointer

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,
@@ -1047,6 +1059,9 @@ func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
 					ctx.expr(x.X), ctx.expr(x.Index))
 			}
 		}
+		if isAtomicPointerType(ctx.typeOf(e.X)) {
+			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)
 			if ok {
@@ -1552,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/atomic.go

@@ -13,3 +13,14 @@ func testAtomicLoadStore64() bool {
 	ok = ok && z == 1
 	return ok
 }
+
+func testAtomicPointers() bool {
+	p := &atomic.Pointer[uint64]{}
+	var x uint64
+	p.Store(&x)
+	y := p.Load()
+	*y = 1
+	var ok = true
+	ok = ok && x == 1
+	return ok
+}

internal/examples/semantics/semantics.gold.v

@@ -119,6 +119,17 @@ Definition testAtomicLoadStore64: val :=
     "ok" <-[boolT] ((![boolT] "ok") && ("z" = #1));;
     ![boolT] "ok".
 
+Definition testAtomicPointers: val :=
+  rec: "testAtomicPointers" <> :=
+    let: "p" := ref (zero_val ptrT) in
+    let: "x" := ref (zero_val uint64T) 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));;
+    ![boolT] "ok".
+
 (* closures.go *)
 
 Notation AdderType := (uint64T -> uint64T)%ht (only parsing).

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