Skip to content

Commit

Permalink
Emit function to "define" global variables (i.e. allocate them) and
Browse files Browse the repository at this point in the history 
another to initialize them, except for `init()` functions and except for
initializing imported packages. Initializing imported packages requires
that `initialize'` only run once, which could use the globals map but
requires changes to the semantics of GlobalGet to permit reading an key
that hasn't been initialized as a means of checking if a package has
already been initialized.
  • Loading branch information
@upamanyus
upamanyus committed Nov 28, 2024
1 parent 42d76f7 commit a977713
Show file tree
Hide file tree
Showing 2 changed files with 113 additions and 23 deletions.
109 changes: 97 additions & 12 deletions goose.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,10 @@ type Ctx struct {
usesDefer bool

dep *depTracker

// Set of global variables in the package being translated.
globalVars map[string]glang.Type
globalVarsOrdered []string
}

func getFfi(pkg *packages.Package) string {
Expand Down Expand Up @@ -79,6 +83,7 @@ func NewPkgCtx(pkg *packages.Package, namesToTranslate map[string]bool) Ctx {
errorReporter: newErrorReporter(pkg.Fset),
dep: newDepTracker(),
namesToTranslate: namesToTranslate,
globalVars: make(map[string]glang.Type),
}
}

Expand Down Expand Up @@ -1714,7 +1719,7 @@ func (ctx *Ctx) assignFromTo(lhs ast.Expr, rhs glang.Expr, cont glang.Expr) glan
}

// This handles conversions arising from the notion of "assignability" in the Go spec.
func (ctx *Ctx) handleImplicitConversion(n ast.Node, from, to types.Type, e glang.Expr) glang.Expr {
func (ctx *Ctx) handleImplicitConversion(n locatable, from, to types.Type, e glang.Expr) glang.Expr {
if to == nil {
// This happens when the LHS is `_`
return e
Expand Down Expand Up @@ -1818,6 +1823,11 @@ func (ctx *Ctx) assignStmt(s *ast.AssignStmt, cont glang.Expr) glang.Expr {
return e
}

// Execute assignments left-to-right
for i := len(s.Lhs); i > 0; i-- {
e = ctx.assignFromTo(s.Lhs[i-1], glang.IdentExpr(fmt.Sprintf("$r%d", i-1)), e)
}

// Determine RHS types, specially handling multiple returns from a function call.
var rhsTypes []types.Type
for i := 0; i < len(s.Rhs); i++ {
Expand Down Expand Up @@ -1845,11 +1855,6 @@ func (ctx *Ctx) assignStmt(s *ast.AssignStmt, cont glang.Expr) glang.Expr {
}
}

// Execute assignments left-to-right
for i := len(s.Lhs); i > 0; i-- {
e = ctx.assignFromTo(s.Lhs[i-1], glang.IdentExpr(fmt.Sprintf("$r%d", i-1)), e)
}

// Let bindings for RHSs including conversions
for i := len(s.Lhs); i > 0; i-- {
e = glang.LetExpr{
Expand Down Expand Up @@ -2320,6 +2325,10 @@ func (ctx *Ctx) globalVarDecl(d *ast.GenDecl) []glang.Decl {
for _, spec := range d.Specs {
s := spec.(*ast.ValueSpec)
for _, name := range s.Names {
if _, ok := ctx.globalVars[name.Name]; !ok {
ctx.globalVars[name.Name] = ctx.glangType(name, ctx.info.TypeOf(name))
ctx.globalVarsOrdered = append(ctx.globalVarsOrdered, name.Name)
}
decls = append(decls, glang.VarDecl{
DeclName: name.Name,
VarUniqueId: ctx.pkgPath + "." + name.Name,
Expand Down Expand Up @@ -2395,21 +2404,97 @@ func (ctx *Ctx) maybeDecls(d ast.Decl) []glang.Decl {
return nil
}

func (ctx *Ctx) initFunction() glang.Decl {
func (ctx *Ctx) initFunctions() []glang.Decl {
// TODO: some constraints for the init translation:
// - Variables are initialized before `init()` runs
// - `init()` can be defined multiple times, and are run in source order.
// - Need to fully initialize lower level packages (e.g. call `init()`s) before
// initializing vars of the current package.
// - should only `init` a package once, even if imported multiple times.

fd := glang.FuncDecl{Name: "initialize'"}

fd.Body = glang.Tt
defineFunc := glang.FuncDecl{Name: "define'"}
ctx.dep.setCurrentName("define'")
var e glang.Expr
if len(ctx.globalVarsOrdered) == 0 {
e = glang.DoExpr{Expr: glang.Tt}
} else {
for _, varName := range ctx.globalVarsOrdered {
s := glang.NewCallExpr(glang.GallinaIdent("globals.put"),
glang.GallinaIdent(varName),
glang.RefExpr{
X: glang.NewCallExpr(glang.GallinaIdent("zero_val"), ctx.globalVars[varName]),
Ty: ctx.globalVars[varName],
})
e = glang.SeqExpr{Expr: s, Cont: e}
}
}
defineFunc.Body = e
ctx.dep.unsetCurrentName()

ctx.dep.setCurrentName("initialize'")
initFunc := glang.FuncDecl{Name: "initialize'"}
ctx.dep.addDep("define'")
e = nil
for _, init := range ctx.info.InitOrder {
ctx.unsupported(init.Rhs, "initializer")
// Execute assignments left-to-right
for i := len(init.Lhs); i > 0; i-- {
e = glang.NewDoSeq(
glang.StoreStmt{
Dst: glang.NewCallExpr(glang.GallinaIdent("globals.get"),
glang.GallinaIdent(init.Lhs[i-1].Name())),
X: glang.IdentExpr(fmt.Sprintf("$r%d", i-1)),
Ty: ctx.glangType(init.Lhs[i-1], init.Lhs[i-1].Type()),
}, e)
}

// Determine RHS types, specially handling multiple returns from a function call.
var rhsTypes []types.Type
t := ctx.typeOf(init.Rhs)
if tuple, ok := t.(*types.Tuple); ok {
for i := range tuple.Len() {
rhsTypes = append(rhsTypes, tuple.At(i).Type())
}
} else {
rhsTypes = append(rhsTypes, t)
}

// collect the RHS expressions
var rhsExprs []glang.Expr
if 1 == len(init.Lhs) {
rhsExprs = append(rhsExprs, ctx.expr(init.Rhs))
} else {
// RHS is a function call returning multiple things. Will introduce
// extra let bindings to destructure those multiple returns.
for i := range init.Lhs {
rhsExprs = append(rhsExprs, glang.IdentExpr(fmt.Sprintf("$ret%d", i)))
}
}

// Let bindings for RHSs including conversions
for i := len(init.Lhs); i > 0; i-- {
e = glang.LetExpr{
Names: []string{fmt.Sprintf("$r%d", i-1)},
ValExpr: ctx.handleImplicitConversion(init.Lhs[i-1], rhsTypes[i-1],
init.Lhs[i-1].Type(), rhsExprs[i-1]),
Cont: e,
}
}

// Extra let bindings in case RHS is a multiple-returning function
if 1 != len(init.Lhs) {
var n []string
for i := range init.Lhs {
n = append(n, fmt.Sprintf("$ret%d", i))
}
e = glang.LetExpr{
Names: n,
ValExpr: ctx.exprSpecial(init.Rhs, true),
Cont: e,
}
}
}
e = glang.NewDoSeq(glang.NewCallExpr(glang.GallinaIdent("define'"), glang.Tt), e)
initFunc.Body = e

return fd
return []glang.Decl{defineFunc, initFunc}
}
27 changes: 16 additions & 11 deletions interface.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ import (

// declsOrError translates one top-level declaration,
// catching Goose translation errors and returning them as a regular Go error
func (ctx Ctx) declsOrError(stmt ast.Decl) (decls []glang.Decl, err error) {
func (ctx *Ctx) declsOrError(stmt ast.Decl) (decls []glang.Decl, err error) {
defer func() {
if r := recover(); r != nil {
if gooseErr, ok := r.(gooseError); ok {
Expand All @@ -31,7 +31,7 @@ func (ctx Ctx) declsOrError(stmt ast.Decl) (decls []glang.Decl, err error) {
}

// catching Goose translation errors and returning them as a regular Go error
func (ctx Ctx) initsOrError() (decls glang.Decl, err error) {
func (ctx *Ctx) initOrError() (decls []glang.Decl, err error) {
defer func() {
if r := recover(); r != nil {
if gooseErr, ok := r.(gooseError); ok {
Expand All @@ -42,7 +42,7 @@ func (ctx Ctx) initsOrError() (decls glang.Decl, err error) {
}
}
}()
return ctx.initFunction(), nil
return ctx.initFunctions(), nil
}

func filterImports(decls []glang.Decl) (nonImports []glang.Decl, imports glang.ImportDecls) {
Expand All @@ -62,7 +62,7 @@ type declId struct {
declIdx int
}

func (ctx Ctx) filterDecls(decls []glang.Decl) (newDecls []glang.Decl) {
func (ctx *Ctx) filterDecls(decls []glang.Decl) (newDecls []glang.Decl) {
if ctx.namesToTranslate == nil {
return decls
}
Expand All @@ -76,7 +76,7 @@ func (ctx Ctx) filterDecls(decls []glang.Decl) (newDecls []glang.Decl) {
}

// Decls converts an entire package (possibly multiple files) to a list of decls
func (ctx Ctx) decls(fs []*ast.File) (imports glang.ImportDecls, sortedDecls []glang.Decl, errs []error) {
func (ctx *Ctx) decls(fs []*ast.File) (imports glang.ImportDecls, sortedDecls []glang.Decl, errs []error) {
decls := make(map[string]glang.Decl)
var declNames []string
declNameToId := make(map[string]declId)
Expand Down Expand Up @@ -106,14 +106,19 @@ func (ctx Ctx) decls(fs []*ast.File) (imports glang.ImportDecls, sortedDecls []g
}
}

newDecl, err := ctx.initsOrError()
newDecls, err := ctx.initOrError()
if err != nil {
errs = append(errs, err)
} else {
_, name := newDecl.DefName()
declNames = append(declNames, name)
// declNameToId[newDecl.DefName()] =
decls[name] = newDecl
for _, newDecl := range newDecls {
named, name := newDecl.DefName()
if !named {
panic("Unnamed decl")
}
declNames = append(declNames, name)
// declNameToId[newDecl.DefName()] =
decls[name] = newDecl
}
}

// Sort Glang decls based on dependencies
Expand Down Expand Up @@ -232,7 +237,7 @@ func translatePackage(pkg *packages.Package, namesToTranslate map[string]bool) (
return coqFile, nil
}

func (ctx Ctx) ffiHeaderFooter(pkg *packages.Package) (header string, footer string) {
func (ctx *Ctx) ffiHeaderFooter(pkg *packages.Package) (header string, footer string) {
if ctx.namesToTranslate != nil {
header += fmt.Sprintf("From New.code_axioms Require Export %s.\n\n", pkg.Name)
}
Expand Down

0 comments on commit a977713

Please sign in to comment.