Fix missing fors and restructured cross-model properties

parser.go

@@ -35,15 +35,17 @@ func ParseAst(fileSet *token.FileSet, proj_name string, commit string, ast_map m
 					if !takesCommParAsParam(decl, ast_map[pack_name]) {
 						// fmt.Println("Parsing ", decl.Name.Name)
 						// fmt.Println("Parsing ", decl.Name)
+						props := new(promela.GlobalProps)
+						props.Fileset = fileSet
 
-						var m promela.Model = promela.Model{
+						m := &promela.Model{
+							Props:                props,
 							Result_fodler:        result_folder,
 							Project_name:         proj_name,
 							Package:              pack_name,
 							Go_names:             ver.Go_names,
 							Name:                 pack_name + PACKAGE_MODEL_SEP + decl.Name.Name + fmt.Sprint(fileSet.Position(decl.Pos()).Line),
 							AstMap:               ast_map,
-							Fileset:              fileSet,
 							FuncDecls:            []*ast.FuncDecl{},
 							Proctypes:            []*promela_ast.Proctype{},
 							RecFuncs:             []promela.RecFunc{},

promela/analyse_comm_param.go

@@ -24,7 +24,6 @@ type CommPar struct {
 
 // Return the parameters that are mandatory and optional
 // Mutates len(a) => a
-
 func (m *Model) AnalyseCommParam(pack string, fun *ast.FuncDecl, ast_map map[string]*packages.Package, log bool) ([]*CommPar, error) {
 
 	params := []*CommPar{}
@@ -119,17 +118,12 @@ func (m *Model) AnalyseCommParam(pack string, fun *ast.FuncDecl, ast_map map[str
 						switch s := s.Underlying().(type) {
 						case *types.Struct:
 							for i := 0; i < s.NumFields(); i++ {
-								switch field := s.Field(i).Type().(type) {
-								case *types.Named:
-									if field.Obj() != nil {
-										if field.Obj().Pkg() != nil {
-											if field.Obj().Pkg().Name() == "sync" {
-												if field.Obj().Name() == "WaitGroup" {
-													contains_chan = true
-												}
-											}
-										}
-									}
+								if field, ok := s.Field(i).Type().(*types.Named); ok &&
+									field.Obj() != nil &&
+									field.Obj().Pkg() != nil &&
+									field.Obj().Pkg().Name() == "sync" &&
+									field.Obj().Name() == "WaitGroup" {
+									contains_chan = true
 								}
 							}
 						}
@@ -170,7 +164,7 @@ func (m *Model) AnalyseCommParam(pack string, fun *ast.FuncDecl, ast_map map[str
 						for _, param := range fun_decl.Type.Params.List {
 							switch param.Type.(type) {
 							case *ast.Ellipsis:
-								err = errors.New(ELLIPSIS + m.Fileset.Position(fun_decl.Pos()).String())
+								err = errors.New(ELLIPSIS + m.Props.Fileset.Position(fun_decl.Pos()).String())
 								return false
 							}
 						}
@@ -375,8 +369,8 @@ func (m *Model) Vid(fun *ast.FuncDecl, expr ast.Expr, mandatory bool, log bool)
 				return params
 			}
 		}
-		name := &ast.Ident{Name: TranslateIdent(expr, m.Fileset).Name}
-		params = m.Upgrade(fun, params, []*CommPar{&CommPar{Name: name, Mandatory: mandatory, Expr: expr, Alias: false}}, log)
+		name := &ast.Ident{Name: TranslateIdent(expr, m.Props.Fileset).Name}
+		params = m.Upgrade(fun, params, []*CommPar{{Name: name, Mandatory: mandatory, Expr: expr, Alias: false}}, log)
 	case *ast.BinaryExpr:
 		params = m.Upgrade(fun, params, m.Vid(fun, expr.X, mandatory, log), log)
 		params = m.Upgrade(fun, params, m.Vid(fun, expr.Y, mandatory, log), log)
@@ -424,9 +418,9 @@ func (m *Model) getIdent(expr ast.Expr) *ast.Ident {
 			Name:      "Anonymous function as ident",
 			Mandatory: "false",
 			Info:      "Unsupported",
-			Line:      m.Fileset.Position(expr.Pos()).Line,
+			Line:      m.Props.Fileset.Position(expr.Pos()).Line,
 			Commit:    m.Commit,
-			Filename:  m.Fileset.Position(expr.Pos()).Filename,
+			Filename:  m.Props.Fileset.Position(expr.Pos()).Filename,
 		})
 		return &ast.Ident{Name: "UNSUPPORTED", NamePos: expr.Pos()}
 	case *ast.FuncType:
@@ -436,9 +430,9 @@ func (m *Model) getIdent(expr ast.Expr) *ast.Ident {
 			Name:      "High order function",
 			Mandatory: "false",
 			Info:      "Unsupported",
-			Line:      m.Fileset.Position(expr.Pos()).Line,
+			Line:      m.Props.Fileset.Position(expr.Pos()).Line,
 			Commit:    m.Commit,
-			Filename:  m.Fileset.Position(expr.Pos()).Filename,
+			Filename:  m.Props.Fileset.Position(expr.Pos()).Filename,
 		})
 		return &ast.Ident{Name: "UNSUPPORTED", NamePos: expr.Pos()}
 	case *ast.KeyValueExpr:
@@ -529,9 +523,9 @@ func (m *Model) spawns(stmts *ast.BlockStmt, log bool) bool {
 			Name:      "Recursive call",
 			Mandatory: strconv.FormatBool(is_spawning),
 			Info:      "Spawning : " + strconv.FormatBool(is_spawning),
-			Line:      m.Fileset.Position(call.Pos()).Line,
+			Line:      m.Props.Fileset.Position(call.Pos()).Line,
 			Commit:    m.Commit,
-			Filename:  m.Fileset.Position(call.Pos()).Filename,
+			Filename:  m.Props.Fileset.Position(call.Pos()).Filename,
 		})
 
 	}

promela/arg.go

@@ -15,13 +15,13 @@ func (m *Model) TranslateArg(expr ast.Expr) (*promela_ast.Ident, []ast.Expr, err
 
 	exprs := []ast.Expr{}
 	if con, num := IsConst(expr, m.AstMap[m.Package]); con {
-		return &promela_ast.Ident{Name: fmt.Sprint(num), Ident: m.Fileset.Position(expr.Pos())}, exprs, nil
+		return &promela_ast.Ident{Name: fmt.Sprint(num), Ident: m.Props.Fileset.Position(expr.Pos())}, exprs, nil
 	}
 
 	switch expr := expr.(type) {
 	case *ast.Ident:
 		exprs = append(exprs, expr)
-		return &promela_ast.Ident{Name: VAR_PREFIX + expr.Name, Ident: m.Fileset.Position(expr.Pos())}, exprs, nil
+		return &promela_ast.Ident{Name: VAR_PREFIX + expr.Name, Ident: m.Props.Fileset.Position(expr.Pos())}, exprs, nil
 
 	case *ast.SelectorExpr:
 
@@ -32,7 +32,7 @@ func (m *Model) TranslateArg(expr ast.Expr) (*promela_ast.Ident, []ast.Expr, err
 		}
 		exprs = append(exprs, expr)
 		return &promela_ast.Ident{Name: x.Name + "_" + expr.Sel.Name,
-			Ident: m.Fileset.Position(expr.Pos())}, exprs, nil
+			Ident: m.Props.Fileset.Position(expr.Pos())}, exprs, nil
 
 	case *ast.BinaryExpr:
 		lhs, new_exprs1, err := m.TranslateArg(expr.X)
@@ -60,7 +60,7 @@ func (m *Model) TranslateArg(expr ast.Expr) (*promela_ast.Ident, []ast.Expr, err
 		return m.TranslateArg(expr.X)
 
 	case *ast.CallExpr:
-		call_name := TranslateIdent(expr.Fun, m.Fileset).Name
+		call_name := TranslateIdent(expr.Fun, m.Props.Fileset).Name
 		if (call_name == "len" || call_name == "int") && len(expr.Args) > 0 {
 			return m.TranslateArg(expr.Args[0]) // if its len just return the translation of the first args which is the list
 		}
@@ -74,7 +74,7 @@ func (m *Model) TranslateArg(expr ast.Expr) (*promela_ast.Ident, []ast.Expr, err
 	case *ast.ParenExpr:
 		return m.TranslateArg(expr.X)
 	default:
-		return nil, exprs, errors.New(UNPARSABLE_ARG + m.Fileset.Position(expr.Pos()).String())
+		return nil, exprs, errors.New(UNPARSABLE_ARG + m.Props.Fileset.Position(expr.Pos()).String())
 
 	}
 

promela/assign_stmt.go

@@ -2,9 +2,10 @@ package promela
 
 import (
 	"errors"
-	"github.com/nicolasdilley/gomela/promela/promela_ast"
 	"go/ast"
 	"go/token"
+
+	"github.com/nicolasdilley/gomela/promela/promela_ast"
 )
 
 func (m *Model) translateAssignStmt(s *ast.AssignStmt) (b *promela_ast.BlockStmt, err error) {
@@ -17,7 +18,7 @@ func (m *Model) translateAssignStmt(s *ast.AssignStmt) (b *promela_ast.BlockStmt
 	for i, spec := range s.Rhs {
 		switch spec := spec.(type) {
 		case *ast.FuncLit:
-			return b, errors.New(FUNC_DECLARED_AS_VAR + m.Fileset.Position(spec.Pos()).String())
+			return b, errors.New(FUNC_DECLARED_AS_VAR + m.Props.Fileset.Position(spec.Pos()).String())
 		case *ast.UnaryExpr:
 			switch spec.Op {
 

promela/block_stmt.go

@@ -12,7 +12,7 @@ func (m *Model) TranslateBlockStmt(b *ast.BlockStmt) (block_stmt *promela_ast.Bl
 	block_stmt = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}
 	defer_stmts = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}
 	if b != nil {
-		block_stmt.Block = m.Fileset.Position(b.Pos())
+		block_stmt.Block = m.Props.Fileset.Position(b.Pos())
 		for _, stmt := range b.List {
 			if stmt != nil {
 				switch stmt := stmt.(type) {

promela/branch_stmt.go

@@ -12,7 +12,7 @@ func (m *Model) translateBranchStmt(s *ast.BranchStmt) (b *promela_ast.BlockStmt
 	b = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}
 	defers = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}
 	br := &promela_ast.GotoStmt{
-		Goto: m.Fileset.Position(s.Pos()),
+		Goto: m.Props.Fileset.Position(s.Pos()),
 	}
 
 	switch s.Tok {

promela/call_expr.go

@@ -71,11 +71,11 @@ func (m *Model) TranslateCallExpr(call_expr *ast.CallExpr) (stmts *promela_ast.B
 			if decl.Name.Name == f.Name && m.Package == f.Pkg {
 				// check if positions match
 				if decl.Pos() == f.Decl.Pos() {
-					return stmts, errors.New(RECURSIVE_FUNCTION + m.Fileset.Position(decl.Pos()).String())
+					return stmts, errors.New(RECURSIVE_FUNCTION + m.Props.Fileset.Position(decl.Pos()).String())
 				}
 			}
 		}
-		func_name = decl.Name.Name + fmt.Sprint(m.Fileset.Position(decl.Pos()).Line)
+		func_name = decl.Name.Name + fmt.Sprint(m.Props.Fileset.Position(decl.Pos()).Line)
 		new_mod := m.newModel(pack_name, decl)
 		new_mod.RecFuncs = append(new_mod.RecFuncs, RecFunc{Pkg: m.Package, Name: decl.Name.Name, Decl: decl})
 
@@ -121,7 +121,7 @@ func (m *Model) TranslateCallExpr(call_expr *ast.CallExpr) (stmts *promela_ast.B
 							select_stmt := &promela_ast.SelectStmt{
 								Model:  "Notify",
 								Guards: []promela_ast.GuardStmt{guard, true_guard},
-								Select: m.Fileset.Position(name.Pos())}
+								Select: m.Props.Fileset.Position(name.Pos())}
 
 							stmts.List = append(stmts.List, select_stmt)
 						}

promela/chan_def_decl_stmt.go

@@ -9,7 +9,7 @@ import (
 
 type ChanDefDeclStmt struct {
 	Decl token.Position
-	M    *Model
+	M    *GlobalProps
 	Name *promela_ast.Ident
 	Size *promela_ast.Ident
 }
@@ -28,7 +28,21 @@ func (s *ChanDefDeclStmt) Print(num_tabs int) (stmt string) {
 		sync_monitor := &promela_ast.RunStmt{X: &promela_ast.CallExpr{Fun: &promela_ast.Ident{Name: "sync_monitor"}, Args: []promela_ast.Expr{s.Name}}}
 
 		async_guard := &promela_ast.SingleGuardStmt{
-			Cond: &promela_ast.Ident{Name: s.Name.Name + " > 0"},
+			Cond: &promela_ast.BinaryExpr{
+				Pos: s.Name.Ident,
+				Lhs: &promela_ast.SelectorExpr{
+					X: &promela_ast.Ident{
+						Name: s.Name.Name,
+					},
+					Sel: &promela_ast.Ident{
+						Name: "size",
+					},
+				},
+				Op: "<",
+				Rhs: &promela_ast.Ident{
+					Name: "0",
+				},
+			},
 			Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{
 				&promela_ast.AssignStmt{Lhs: &promela_ast.SelectorExpr{X: s.Name, Sel: &promela_ast.Ident{Name: "size"}}, Rhs: s.Size},
 				&promela_ast.RunStmt{X: &promela_ast.CallExpr{Fun: &promela_ast.Ident{Name: "async_monitor"}, Args: []promela_ast.Expr{s.Name}}},

promela/clean.go

@@ -173,7 +173,7 @@ func containsMSP(b *promela_ast.BlockStmt) bool {
 	contains := false
 	promela_ast.Inspect(b, func(s promela_ast.Stmt) bool {
 		switch s.(type) {
-		case *promela_ast.RcvStmt, *promela_ast.SendStmt, *promela_ast.RunStmt:
+		case *GenReceiver, *GenRcvStmt, *GenSendStmt, *promela_ast.RcvStmt, *promela_ast.SendStmt, *promela_ast.RunStmt:
 			contains = true
 		}
 		return !contains

promela/features.go

@@ -35,8 +35,8 @@ func CreateCSV(result_folder string) {
 func logFeature(feature Feature, m *Model) {
 
 	name := strings.Split(
-		m.Fileset.Position(m.Fun.Pos()).Filename, m.Projects_folder+"/")
-	path := []string{m.Fileset.Position(m.Fun.Pos()).Filename}
+		m.Props.Fileset.Position(m.Fun.Pos()).Filename, m.Projects_folder+"/")
+	path := []string{m.Props.Fileset.Position(m.Fun.Pos()).Filename}
 
 	splitted := []string{""}
 	if len(name) > 1 {
@@ -57,7 +57,7 @@ func logFeature(feature Feature, m *Model) {
 	}
 
 	proj_name := strings.Replace(splitted[0], AUTHOR_PROJECT_SEP, "/", -1)
-	filename := "https://github.com/" + proj_name + "/blob/" + m.Commit + "/" + file_path + "#L" + strconv.Itoa(m.Fileset.Position(m.Fun.Pos()).Line)
+	filename := "https://github.com/" + proj_name + "/blob/" + m.Commit + "/" + file_path + "#L" + strconv.Itoa(m.Props.Fileset.Position(m.Fun.Pos()).Line)
 
 	toPrint :=
 		proj_name + "," +

promela/for_stmt.go

@@ -63,7 +63,7 @@ func (m *Model) translateForStmt(s *ast.ForStmt) (b *promela_ast.BlockStmt, defe
 		err = err1
 	}
 	if len(d3.List) > 0 {
-		return b, d3, errors.New(DEFER_IN_FOR + m.Fileset.Position(s.Pos()).String())
+		return b, d3, errors.New(DEFER_IN_FOR + m.Props.Fileset.Position(s.Pos()).String())
 	}
 	spawns := m.spawns(s.Body, false)
 	if spawns || containsMSP(stmts) {
@@ -77,14 +77,14 @@ func (m *Model) translateForStmt(s *ast.ForStmt) (b *promela_ast.BlockStmt, defe
 
 			// need to change the for loop into a bounded for loop
 			b.List = append(b.List, &promela_ast.ForStmt{
-				For:  m.Fileset.Position(s.Pos()),
+				For:  m.Props.Fileset.Position(s.Pos()),
 				Lb:   lb,
 				Ub:   ub,
 				Body: stmts,
 			}, for_label)
 
 		} else if len(stmts.List) > 0 {
-			d := &promela_ast.DoStmt{Do: m.Fileset.Position(s.Pos())}
+			d := &promela_ast.DoStmt{Do: m.Props.Fileset.Position(s.Pos())}
 			d.Guards = append(
 				d.Guards,
 				&promela_ast.SingleGuardStmt{
@@ -115,7 +115,7 @@ func (m *Model) translateForStmt(s *ast.ForStmt) (b *promela_ast.BlockStmt, defe
 					Body: &promela_ast.BlockStmt{
 						List: []promela_ast.Stmt{
 							&promela_ast.ForStmt{
-								For:  m.Fileset.Position(s.Pos()),
+								For:  m.Props.Fileset.Position(s.Pos()),
 								Lb:   lb,
 								Ub:   ub,
 								Body: body2,

promela/gen_param.go

@@ -0,0 +1,46 @@
+package promela
+
+import (
+	"github.com/nicolasdilley/gomela/promela/promela_ast"
+	"github.com/nicolasdilley/gomela/promela/promela_types"
+
+	"go/token"
+)
+
+// A channel parameter is either of the form "chan c", or "Chandef c", based on M.containsClose.
+type GenChanParam struct {
+	Pos   token.Position
+	Model string
+	M     *GlobalProps // a pointer to the model to check whether it containsClose or not
+	Name  string       // the chan that we want to send on
+}
+
+func (s *GenChanParam) GoNode() token.Position {
+	return s.Pos
+}
+
+func (s *GenChanParam) Print(num_tabs int) string {
+
+	// if contains close send to monitor
+	var p *promela_ast.Param
+	if s.M.ContainsClose {
+		p = &promela_ast.Param{
+			Pos:   s.Pos,
+			Name:  s.Name,
+			Types: promela_types.Chandef,
+		}
+		return p.Print(num_tabs)
+	} else {
+		p = &promela_ast.Param{
+			Pos:   s.Pos,
+			Name:  s.Name,
+			Types: promela_types.Chan,
+		}
+	}
+	return p.Print(num_tabs)
+}
+
+func (s *GenChanParam) Clone() promela_ast.Stmt {
+	s1 := &GenChanParam{Pos: s.Pos, Name: s.Name, M: s.M, Model: s.Model}
+	return s1
+}

promela/gen_rcv_stmt.go

@@ -10,7 +10,7 @@ import (
 type GenRcvStmt struct {
 	Rcv        token.Position
 	Model      string
-	M          *Model           // a pointer to the model to check whether it containsClose or not
+	M          *GlobalProps     // a pointer to the model to check whether it containsClose or not
 	Chan       promela_ast.Expr // the chan that we want to send on
 	Sync_body  *promela_ast.BlockStmt
 	Async_body *promela_ast.BlockStmt