diff --git a/parser.go b/parser.go index 7b5e2bed3..9738d5288 100755 --- a/parser.go +++ b/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{}, diff --git a/promela/analyse_comm_param.go b/promela/analyse_comm_param.go index 5e61078fa..64633ccc9 100755 --- a/promela/analyse_comm_param.go +++ b/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, }) } diff --git a/promela/arg.go b/promela/arg.go index 490fb3736..c20db44da 100755 --- a/promela/arg.go +++ b/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()) } diff --git a/promela/assign_stmt.go b/promela/assign_stmt.go index a81eda820..829a4a716 100755 --- a/promela/assign_stmt.go +++ b/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 { diff --git a/promela/block_stmt.go b/promela/block_stmt.go index cd45cf33a..1eb51b6dd 100755 --- a/promela/block_stmt.go +++ b/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) { diff --git a/promela/branch_stmt.go b/promela/branch_stmt.go index 3f9c269e2..d4ff8e94e 100755 --- a/promela/branch_stmt.go +++ b/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 { diff --git a/promela/call_expr.go b/promela/call_expr.go index 443c4e859..d78a46f5a 100755 --- a/promela/call_expr.go +++ b/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) } diff --git a/promela/chan_def_decl_stmt.go b/promela/chan_def_decl_stmt.go index 7a591a2ae..470a1b2b4 100644 --- a/promela/chan_def_decl_stmt.go +++ b/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}}}, diff --git a/promela/clean.go b/promela/clean.go index fe54bac9c..00344c433 100755 --- a/promela/clean.go +++ b/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 diff --git a/promela/features.go b/promela/features.go index 65544ed00..2b7000641 100755 --- a/promela/features.go +++ b/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 + "," + diff --git a/promela/for_stmt.go b/promela/for_stmt.go index 6bf31929b..017db5cb8 100755 --- a/promela/for_stmt.go +++ b/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, diff --git a/promela/gen_param.go b/promela/gen_param.go new file mode 100644 index 000000000..f4bb5d65c --- /dev/null +++ b/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 +} diff --git a/promela/gen_rcv_stmt.go b/promela/gen_rcv_stmt.go index 3d1b9a552..88dea2427 100644 --- a/promela/gen_rcv_stmt.go +++ b/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 diff --git a/promela/gen_receiver.go b/promela/gen_receiver.go new file mode 100644 index 000000000..3326a1c19 --- /dev/null +++ b/promela/gen_receiver.go @@ -0,0 +1,38 @@ +package promela + +import ( + "go/token" + + "github.com/nicolasdilley/gomela/promela/promela_ast" +) + +// A channel parameter is either of the form "chan c", or "Chandef c", based on M.containsClose. +type GenReceiver struct { + M *GlobalProps + Name string + Model string +} + +func (s *GenReceiver) GoNode() token.Position { + return s.M.Fileset.Position(token.NoPos) +} + +func (s *GenReceiver) Print(num_tabs int) string { + + // if contains close send to monitor + // var p *promela_ast.Param + if s.M.ContainsReceiver { + p := &promela_ast.RunStmt{ + X: &promela_ast.CallExpr{ + Fun: &promela_ast.Ident{ + Name: "receiver"}, + Args: []promela_ast.Expr{&promela_ast.Ident{Name: s.Name}}}} + return p.Print(num_tabs) + } + return "" +} + +func (s *GenReceiver) Clone() promela_ast.Stmt { + s1 := &GenReceiver{Name: s.Name, M: s.M, Model: s.Model} + return s1 +} diff --git a/promela/gen_send_stmt.go b/promela/gen_send_stmt.go index 11de575c7..11b6eba99 100644 --- a/promela/gen_send_stmt.go +++ b/promela/gen_send_stmt.go @@ -10,7 +10,7 @@ import ( type GenSendStmt struct { Send 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 @@ -23,7 +23,6 @@ func (s *GenSendStmt) GoNode() token.Position { func (s *GenSendStmt) Print(num_tabs int) string { // if contains close send to monitor - if s.M.ContainsClose { sync_send := &promela_ast.SendStmt{ @@ -32,7 +31,7 @@ func (s *GenSendStmt) Print(num_tabs int) string { Sel: &promela_ast.Ident{Name: "sync"}}, Rhs: &promela_ast.Ident{Name: "false"}, // the channel is not closed Model: s.Model, - //Send: m.Fileset.Position(s.Pos()) + Send: s.Send, } async_send := &promela_ast.RcvStmt{ Chan: &promela_ast.SelectorExpr{ @@ -40,7 +39,7 @@ func (s *GenSendStmt) Print(num_tabs int) string { Sel: &promela_ast.Ident{Name: "enq"}}, Rhs: &promela_ast.Ident{Name: "ok"}, Model: s.Model, - //Send: m.Fileset.Position(s.Pos()) + Rcv: s.Send, } assert := &promela_ast.AssertStmt{Pos: s.Send, Expr: &promela_ast.Ident{Name: "ok"}} @@ -75,7 +74,6 @@ func (s *GenSendStmt) Print(num_tabs int) string { return send_guard.Print(num_tabs) } - } func (s *GenSendStmt) Clone() promela_ast.Stmt { diff --git a/promela/go_stmt.go b/promela/go_stmt.go index 08c06abc0..4e8cee6a7 100755 --- a/promela/go_stmt.go +++ b/promela/go_stmt.go @@ -49,14 +49,14 @@ func (m *Model) TranslateGoStmt(s *ast.GoStmt, isMain bool) (b *promela_ast.Bloc for _, f := range m.RecFuncs { if decl.Name.Name == f.Name && m.Package == f.Pkg { if decl.Pos() == f.Decl.Pos() { - return b, errors.New(RECURSIVE_FUNCTION + m.Fileset.Position(decl.Pos()).String()) + return b, errors.New(RECURSIVE_FUNCTION + m.Props.Fileset.Position(decl.Pos()).String()) } } } // check if its a call on a struct that contains a chan, mutex or wgs - 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) @@ -103,15 +103,15 @@ func (m *Model) TranslateGoStmt(s *ast.GoStmt, isMain bool) (b *promela_ast.Bloc } // s can be either the go stmt or the call expr -func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.CallExpr, func_name string, decl *ast.FuncDecl, params []*promela_ast.Param, args []promela_ast.Expr, isMain bool) (*promela_ast.BlockStmt, error) { +func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.CallExpr, func_name string, decl *ast.FuncDecl, params []promela_ast.Expr, args []promela_ast.Expr, isMain bool) (*promela_ast.BlockStmt, error) { b := &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} - prom_call := &promela_ast.CallExpr{Fun: &promela_ast.Ident{Name: func_name}, Call: m.Fileset.Position(call_expr.Pos())} + prom_call := &promela_ast.CallExpr{Fun: &promela_ast.Ident{Name: func_name}, Call: m.Props.Fileset.Position(call_expr.Pos())} prom_call.Args = args proc := &promela_ast.Proctype{ Name: &promela_ast.Ident{Name: func_name}, - Pos: m.Fileset.Position(call_expr.Pos()), + Pos: m.Props.Fileset.Position(call_expr.Pos()), Active: false, Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}, Params: params, @@ -167,10 +167,10 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca } else { proc.Params = append(proc.Params, &promela_ast.Param{Name: VAR_PREFIX + commPar.Name.Name, Types: promela_types.Int}) - arg := TranslateIdent(call_expr.Args[commPar.Pos], m.Fileset) + arg := TranslateIdent(call_expr.Args[commPar.Pos], m.Props.Fileset) if found, _ := ContainsCommParam(m.CommPars, &CommPar{Name: &ast.Ident{Name: arg.Name}}); found { - prom_call.Args = append(prom_call.Args, &promela_ast.Ident{Name: VAR_PREFIX + arg.Name, Ident: m.Fileset.Position(call_expr.Pos())}) + prom_call.Args = append(prom_call.Args, &promela_ast.Ident{Name: VAR_PREFIX + arg.Name, Ident: m.Props.Fileset.Position(call_expr.Pos())}) } else { var ident *promela_ast.Ident @@ -182,7 +182,7 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca for _, expr := range exprs { // This is for accounting cases where an actual commParam args is a + b where a is known and b isnt. therefore we need to create a new def for b - if found, _ := ContainsCommParam(m.CommPars, &CommPar{Name: &ast.Ident{Name: TranslateIdent(expr, m.Fileset).Name}}); !found { + if found, _ := ContainsCommParam(m.CommPars, &CommPar{Name: &ast.Ident{Name: TranslateIdent(expr, m.Props.Fileset).Name}}); !found { // need to create a not found for it rhs := "" @@ -193,12 +193,13 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca } var buff *bytes.Buffer = bytes.NewBuffer([]byte{}) - printer.Fprint(buff, m.Fileset, commPar.Expr) - rhs += string(buff.Bytes()) + " line " + strconv.Itoa(m.Fileset.Position(commPar.Expr.Pos()).Line) - ident := &promela_ast.Ident{Name: VAR_PREFIX + TranslateIdent(expr, m.Fileset).Name} + printer.Fprint(buff, m.Props.Fileset, commPar.Expr) + rhs += buff.String() + " line " + strconv.Itoa(m.Props.Fileset.Position(commPar.Expr.Pos()).Line) + ident := &promela_ast.Ident{Name: VAR_PREFIX + TranslateIdent(expr, m.Props.Fileset).Name} m.Defines = append(m.Defines, promela_ast.DefineStmt{ Name: &promela_ast.Ident{Name: DEF_PREFIX + ident.Name}, - Rhs: &promela_ast.Ident{Name: rhs}}) + Rhs: &promela_ast.Ident{Name: rhs}, + }) b.List = append(b.List, &promela_ast.DeclStmt{ Name: ident, @@ -212,7 +213,7 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca ident = arg prom_call.Args = append(prom_call.Args, ident) } else { - ident = &promela_ast.Ident{Name: "not_found_" + strconv.Itoa(m.Fileset.Position(call_expr.Pos()).Line)} + ident = &promela_ast.Ident{Name: "not_found_" + strconv.Itoa(m.Props.Fileset.Position(call_expr.Pos()).Line)} rhs := "" if commPar.Mandatory { @@ -222,8 +223,8 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca } var buff *bytes.Buffer = bytes.NewBuffer([]byte{}) - printer.Fprint(buff, m.Fileset, commPar.Expr) - rhs += string(buff.Bytes()) + " line " + strconv.Itoa(m.Fileset.Position(commPar.Expr.Pos()).Line) + printer.Fprint(buff, m.Props.Fileset, commPar.Expr) + rhs += buff.String() + " line " + strconv.Itoa(m.Props.Fileset.Position(commPar.Expr.Pos()).Line) m.Defines = append(m.Defines, promela_ast.DefineStmt{Name: ident, Rhs: &promela_ast.Ident{Name: rhs}}) prom_call.Args = append(prom_call.Args, ident) @@ -245,8 +246,8 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca } var buff *bytes.Buffer = bytes.NewBuffer([]byte{}) - printer.Fprint(buff, m.Fileset, commPar.Expr) - rhs += string(buff.Bytes()) + " line " + strconv.Itoa(m.Fileset.Position(commPar.Expr.Pos()).Line) + printer.Fprint(buff, m.Props.Fileset, commPar.Expr) + rhs += buff.String() + " line " + strconv.Itoa(m.Props.Fileset.Position(commPar.Expr.Pos()).Line) m.Defines = append(m.Defines, promela_ast.DefineStmt{Name: ident, Rhs: &promela_ast.Ident{Name: rhs}}) prom_call.Args = append(prom_call.Args, ident) @@ -264,18 +265,14 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca Info: commPar.Name.Name, Line: 0, Commit: m.Commit, - Filename: m.Fileset.Position(m.Fun.Pos()).Filename, + Filename: m.Props.Fileset.Position(m.Fun.Pos()).Filename, }) } } - prom_call.Fun = &promela_ast.Ident{Name: func_name, Ident: m.Fileset.Position(call_expr.Pos())} + prom_call.Fun = &promela_ast.Ident{Name: func_name, Ident: m.Props.Fileset.Position(call_expr.Pos())} m.addNewProctypes(new_mod) // adding the new proctypes create in the new model - m.ContainsChan = m.ContainsChan || new_mod.ContainsChan - m.ContainsWg = m.ContainsWg || new_mod.ContainsWg - m.ContainsMutexes = m.ContainsMutexes || new_mod.ContainsMutexes - child_func_name := "child_" + func_name + strconv.Itoa(m.Counter) prom_call.Args = append(prom_call.Args, &promela_ast.Ident{Name: child_func_name}) // add child param @@ -292,12 +289,11 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca b.List = append(b.List, &promela_ast.RcvStmt{Chan: &promela_ast.Ident{Name: child_func_name}, Rhs: &promela_ast.Ident{Name: "0"}}) } else { // Add the receiver call - b.List = append(b.List, &promela_ast.RunStmt{ - X: &promela_ast.CallExpr{ - Fun: &promela_ast.Ident{ - Name: "receiver"}, - Args: []promela_ast.Expr{&promela_ast.Ident{Name: child_func_name}}}}) - m.ContainsReceiver = true + b.List = append(b.List, &GenReceiver{ + Name: child_func_name, + M: m.Props, + }) + m.Props.ContainsReceiver = true } if isMain { @@ -309,10 +305,10 @@ func (m *Model) translateCommParams(new_mod *Model, isGo bool, call_expr *ast.Ca return b, nil } -func (m *Model) translateParams(new_mod *Model, decl *ast.FuncDecl, call_expr *ast.CallExpr, isMain bool) ([]*promela_ast.Param, []promela_ast.Expr, bool, bool, error) { +func (m *Model) translateParams(new_mod *Model, decl *ast.FuncDecl, call_expr *ast.CallExpr, isMain bool) ([]promela_ast.Expr, []promela_ast.Expr, bool, bool, error) { hasChan := isMain known := true - params := []*promela_ast.Param{} + params := []promela_ast.Expr{} args := []promela_ast.Expr{} counter := 0 @@ -329,8 +325,12 @@ func (m *Model) translateParams(new_mod *Model, decl *ast.FuncDecl, call_expr *a hasChan = true if m.containsChan(call_expr.Args[counter]) { chan_name := name.Name + CHAN_NAME - params = append(params, &promela_ast.Param{Name: chan_name, Types: promela_types.Chandef}) - new_mod.Chans[name] = &ChanStruct{Name: &promela_ast.Ident{Name: chan_name}, Chan: m.Fileset.Position(name.Pos())} + params = append(params, &GenChanParam{ + Pos: m.Props.Fileset.Position(sel.Begin), + Name: chan_name, + M: m.Props, + }) + new_mod.Chans[name] = &ChanStruct{Name: &promela_ast.Ident{Name: chan_name}, Chan: m.Props.Fileset.Position(name.Pos())} ch := m.getChanStruct(call_expr.Args[counter]) @@ -345,7 +345,7 @@ func (m *Model) translateParams(new_mod *Model, decl *ast.FuncDecl, call_expr *a if sel.Sel.Name == "WaitGroup" { hasChan = true if m.containsWaitgroup(call_expr.Args[counter]) { - wg := &WaitGroupStruct{Name: &promela_ast.Ident{Name: name.Name, Ident: m.Fileset.Position(name.Pos())}, Wait: m.Fileset.Position(name.Pos())} + wg := &WaitGroupStruct{Name: &promela_ast.Ident{Name: name.Name, Ident: m.Props.Fileset.Position(name.Pos())}, Wait: m.Props.Fileset.Position(name.Pos())} params = append(params, &promela_ast.Param{Name: name.Name, Types: promela_types.Wgdef}) new_mod.WaitGroups[name] = wg arg := call_expr.Args[counter] @@ -355,7 +355,7 @@ func (m *Model) translateParams(new_mod *Model, decl *ast.FuncDecl, call_expr *a arg = unary.X } - ident := &promela_ast.Ident{Name: m.getIdent(arg).Name, Ident: m.Fileset.Position(call_expr.Pos())} + ident := &promela_ast.Ident{Name: m.getIdent(arg).Name, Ident: m.Props.Fileset.Position(call_expr.Pos())} args = append(args, ident) } else { known = false @@ -373,7 +373,7 @@ func (m *Model) translateParams(new_mod *Model, decl *ast.FuncDecl, call_expr *a arg = unary.X } - ident := &promela_ast.Ident{Name: m.getIdent(arg).Name, Ident: m.Fileset.Position(call_expr.Pos())} + ident := &promela_ast.Ident{Name: m.getIdent(arg).Name, Ident: m.Props.Fileset.Position(call_expr.Pos())} args = append(args, ident) } else { @@ -394,7 +394,7 @@ func (m *Model) translateParams(new_mod *Model, decl *ast.FuncDecl, call_expr *a // func (m *Model) GenerateParamAndArg(arg ast.Expr, t promela_types.Types) ([]*promela_ast.Param, []promela_ast.Expr) { // name := translateIdent(arg).Name -// p := &promela_ast.Param{Name: name, Pos: m.Fileset.Position(arg.Pos()), Types: t} +// p := &promela_ast.Param{Name: name, Pos: m.Props.Fileset.Position(arg.Pos()), Types: t} // e := &promela_ast.Ident{Name: name} // return p, e @@ -412,7 +412,7 @@ func (m *Model) findFunDecl(call_expr *ast.CallExpr) (*ast.FuncDecl, *ast.CallEx Params: &ast.FieldList{List: append([]*ast.Field{}, name.Type.Params.List...)}, }, } - func_name := fmt.Sprint("Anonymous", m.Fun.Name.Name, m.Fileset.Position(name.Pos()).Line) + func_name := fmt.Sprint("Anonymous", m.Fun.Name.Name, m.Props.Fileset.Position(name.Pos()).Line) ident := &ast.Ident{Name: func_name, NamePos: name.Pos()} fun_decl.Name = ident fun_decl.Body = name.Body @@ -433,7 +433,7 @@ func (m *Model) findFunDecl(call_expr *ast.CallExpr) (*ast.FuncDecl, *ast.CallEx ch_names := []*ast.Ident{} for ch, _ := range m.Chans { if !containsExpr(exprs, ch) { - ch_names = append(ch_names, &ast.Ident{Name: TranslateIdent(ch, m.Fileset).Name, NamePos: ch.Pos()}) + ch_names = append(ch_names, &ast.Ident{Name: TranslateIdent(ch, m.Props.Fileset).Name, NamePos: ch.Pos()}) new_call_expr.Args = append(new_call_expr.Args, ch) } } @@ -444,7 +444,7 @@ func (m *Model) findFunDecl(call_expr *ast.CallExpr) (*ast.FuncDecl, *ast.CallEx for wg, _ := range m.WaitGroups { if !containsExpr(exprs, wg) { - wg_names = append(wg_names, &ast.Ident{Name: TranslateIdent(wg, m.Fileset).Name, NamePos: wg.Pos()}) + wg_names = append(wg_names, &ast.Ident{Name: TranslateIdent(wg, m.Props.Fileset).Name, NamePos: wg.Pos()}) new_call_expr.Args = append(new_call_expr.Args, wg) } } @@ -460,7 +460,7 @@ func (m *Model) findFunDecl(call_expr *ast.CallExpr) (*ast.FuncDecl, *ast.CallEx for _, mu := range m.Mutexes { if !containsExpr(exprs, mu) { - mu_names = append(mu_names, &ast.Ident{Name: TranslateIdent(mu, m.Fileset).Name, NamePos: mu.Pos()}) + mu_names = append(mu_names, &ast.Ident{Name: TranslateIdent(mu, m.Props.Fileset).Name, NamePos: mu.Pos()}) new_call_expr.Args = append(new_call_expr.Args, mu) } } @@ -491,7 +491,7 @@ func (m *Model) findFunDecl(call_expr *ast.CallExpr) (*ast.FuncDecl, *ast.CallEx for _, field := range decl.Type.Params.List { switch field.Type.(type) { case *ast.Ellipsis: - return nil, nil, pack_name, errors.New(ELLIPSIS + m.Fileset.Position(call_expr.Pos()).String()) + return nil, nil, pack_name, errors.New(ELLIPSIS + m.Props.Fileset.Position(call_expr.Pos()).String()) } } new_decl, new_call_expr := m.updateDeclWithRcvAndStructs(*decl, call_expr) @@ -509,14 +509,14 @@ func (m *Model) findFunDecl(call_expr *ast.CallExpr) (*ast.FuncDecl, *ast.CallEx } } if m.isChan(expr) || m.isWaitgroup(expr) || m.isMutex(expr) { - return nil, nil, pack_name, errors.New(UNKNOWN_DECL + fmt.Sprint(m.Fileset.Position(call_expr.Fun.Pos()))) + return nil, nil, pack_name, errors.New(UNKNOWN_DECL + fmt.Sprint(m.Props.Fileset.Position(call_expr.Fun.Pos()))) } } // also check if the function is not a method on a struct that contains // a mutex, a chan or a wg ! if m.isStructWithChans(call_expr.Fun) { - return nil, nil, pack_name, errors.New(UNKNOWN_DECL + fmt.Sprint(m.Fileset.Position(call_expr.Fun.Pos()))) + return nil, nil, pack_name, errors.New(UNKNOWN_DECL + fmt.Sprint(m.Props.Fileset.Position(call_expr.Fun.Pos()))) } } diff --git a/promela/if_stmt.go b/promela/if_stmt.go index 9b361d4a8..f57b8cb17 100755 --- a/promela/if_stmt.go +++ b/promela/if_stmt.go @@ -2,16 +2,17 @@ package promela import ( "errors" - "github.com/nicolasdilley/gomela/promela/promela_ast" "go/ast" "go/token" "strconv" + + "github.com/nicolasdilley/gomela/promela/promela_ast" ) func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers *promela_ast.BlockStmt, err error) { b = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} defers = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} - i := &promela_ast.IfStmt{If: m.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} + i := &promela_ast.IfStmt{If: m.Props.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} stmts, defer_stmts, err1 := m.TranslateBlockStmt(&ast.BlockStmt{List: []ast.Stmt{s.Init}}) @@ -50,7 +51,7 @@ func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers return b, defer_stmts, err1 } if len(defer_stmts2.List) > 0 { - return b, defer_stmts, errors.New(DEFER_IN_IF + m.Fileset.Position(s.Pos()).String()) + return b, defer_stmts, errors.New(DEFER_IN_IF + m.Props.Fileset.Position(s.Pos()).String()) } contains := false @@ -65,7 +66,7 @@ func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers case *ast.BlockStmt: s1, defer_stmts3, err1 := m.TranslateBlockStmt(els) if len(defer_stmts3.List) > 0 { - return b, defer_stmts, errors.New(DEFER_IN_IF + m.Fileset.Position(s.Pos()).String()) + return b, defer_stmts, errors.New(DEFER_IN_IF + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { err = err1 @@ -74,7 +75,7 @@ func (m *Model) translateIfStmt(s *ast.IfStmt) (b *promela_ast.BlockStmt, defers default: s1, defers, err1 := m.TranslateBlockStmt(&ast.BlockStmt{List: []ast.Stmt{s.Else}}) if len(defers.List) > 0 { - return b, defer_stmts, errors.New(DEFER_IN_IF + m.Fileset.Position(s.Pos()).String()) + return b, defer_stmts, errors.New(DEFER_IN_IF + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { err = err1 @@ -132,7 +133,7 @@ func (m *Model) isIfClosed(s *ast.IfStmt) (isClosed bool, b *promela_ast.BlockSt return isClosed, b1, err1 } if len(d1.List) > 0 { - return isClosed, b1, errors.New(DEFER_IN_IF + m.Fileset.Position(s.Pos()).String()) + return isClosed, b1, errors.New(DEFER_IN_IF + m.Props.Fileset.Position(s.Pos()).String()) } then_guard := &promela_ast.SingleGuardStmt{Cond: cond, Body: b1} else_guard := &promela_ast.SingleGuardStmt{Cond: &promela_ast.Ident{Name: "else"}, Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} @@ -143,7 +144,7 @@ func (m *Model) isIfClosed(s *ast.IfStmt) (isClosed bool, b *promela_ast.BlockSt case *ast.BlockStmt: s1, defer_stmts3, err1 := m.TranslateBlockStmt(els) if len(defer_stmts3.List) > 0 { - return isClosed, b, errors.New(DEFER_IN_IF + m.Fileset.Position(s.Pos()).String()) + return isClosed, b, errors.New(DEFER_IN_IF + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { return isClosed, b, err1 @@ -152,7 +153,7 @@ func (m *Model) isIfClosed(s *ast.IfStmt) (isClosed bool, b *promela_ast.BlockSt default: s1, defers, err1 := m.TranslateBlockStmt(&ast.BlockStmt{List: []ast.Stmt{s.Else}}) if len(defers.List) > 0 { - return isClosed, b, errors.New(DEFER_IN_IF + m.Fileset.Position(s.Pos()).String()) + return isClosed, b, errors.New(DEFER_IN_IF + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { return isClosed, b, err1 diff --git a/promela/interpreter.go b/promela/interpreter.go index 5f44275c2..b2276801d 100755 --- a/promela/interpreter.go +++ b/promela/interpreter.go @@ -31,8 +31,8 @@ func Print(m *Model) { stmt += "\n" 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 { @@ -52,7 +52,7 @@ func Print(m *Model) { } } proj_name := strings.Replace(splitted[0], AUTHOR_PROJECT_SEP, "/", -1) - stmt += "// git_link=https://github.com/" + proj_name + "/blob/" + m.Commit + "/" + file_path + "#L" + strconv.Itoa(m.Fileset.Position(m.Fun.Pos()).Line) + "\n" + stmt += "// git_link=https://github.com/" + proj_name + "/blob/" + m.Commit + "/" + file_path + "#L" + strconv.Itoa(m.Props.Fileset.Position(m.Fun.Pos()).Line) + "\n" // print the bounds for _, c := range m.Defines { @@ -101,13 +101,13 @@ func Print(m *Model) { for _, c := range m.Global_vars { b.List = append(b.List, c) } - if m.ContainsChan { + if m.Props.ContainsChan { stmt += chan_struct.Print(0) } - if m.ContainsWg { + if m.Props.ContainsWg { stmt += wg_struct.Print(0) } - if m.ContainsMutexes { + if m.Props.ContainsMutexes { stmt += mutex_struct.Print(0) } @@ -125,21 +125,18 @@ func Print(m *Model) { stmt += "\n /* ================================================================================== */" stmt += "\n /* ================================================================================== */ \n" - if m.ContainsChan { - // If there is a close statement, we need the monitors - if m.ContainsClose { - stmt += GenerateAsyncMonitor() + generateSyncChanMonitor() - } + if m.Props.ContainsChan && m.Props.ContainsClose { + stmt += GenerateAsyncMonitor() + generateSyncChanMonitor() } - if m.ContainsWg { + if m.Props.ContainsWg { stmt += GenerateStructMonitor() } - if m.ContainsMutexes { + if m.Props.ContainsMutexes { stmt += GenerateMutexMonitor() } - if m.ContainsReceiver { + if m.Props.ContainsReceiver { stmt += GenerateReceiverProcess() } diff --git a/promela/label_stmt.go b/promela/label_stmt.go index b8be2dba2..3e2971a04 100755 --- a/promela/label_stmt.go +++ b/promela/label_stmt.go @@ -9,7 +9,7 @@ import ( func (m *Model) translateLabeledStmt(s *ast.LabeledStmt) (b *promela_ast.BlockStmt, defers *promela_ast.BlockStmt, err error) { b = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} defers = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} - label := &promela_ast.LabelStmt{Label: m.Fileset.Position(s.Pos()), Name: s.Label.Name} + label := &promela_ast.LabelStmt{Label: m.Props.Fileset.Position(s.Pos()), Name: s.Label.Name} stmts, d1, err1 := m.TranslateBlockStmt(&ast.BlockStmt{List: []ast.Stmt{s.Stmt}}) addBlock(defers, d1) if err1 != nil { diff --git a/promela/lookup.go b/promela/lookup.go index c7ef2ce2e..3a8c98f76 100755 --- a/promela/lookup.go +++ b/promela/lookup.go @@ -76,7 +76,7 @@ func (m *Model) lookUpFor(s *ast.ForStmt, spawns bool, pack *packages.Package) ( } if !well_formed { - ub_decl := promela_ast.DefineStmt{Name: &promela_ast.Ident{Name: fmt.Sprintf("ub_for%d_%d", m.Fileset.Position(s.Pos()).Line, m.Fileset.Position(s.Pos()).Column)}, Rhs: &promela_ast.Ident{Name: OPTIONAL_BOUND}} + ub_decl := promela_ast.DefineStmt{Name: &promela_ast.Ident{Name: fmt.Sprintf("ub_for%d_%d", m.Props.Fileset.Position(s.Pos()).Line, m.Props.Fileset.Position(s.Pos()).Column)}, Rhs: &promela_ast.Ident{Name: OPTIONAL_BOUND}} mandatory := "false" if spawns { mandatory = "true" @@ -95,7 +95,7 @@ func (m *Model) lookUpFor(s *ast.ForStmt, spawns bool, pack *packages.Package) ( Mandatory: mandatory, Line: 0, Commit: m.Commit, - Filename: m.Fileset.Position(m.Fun.Pos()).Filename, + Filename: m.Props.Fileset.Position(m.Fun.Pos()).Filename, }) lb = &promela_ast.Ident{Name: "0"} // returning the fresh vars ub = &promela_ast.Ident{Name: ub_decl.Name.Name + "-1"} @@ -108,9 +108,9 @@ func (m *Model) lookUpFor(s *ast.ForStmt, spawns bool, pack *packages.Package) ( Name: "For loop not well formed", Mandatory: "false", Info: fmt.Sprint("Init : ", s.Init, " Cond : ", s.Cond, " Post : ", s.Post), - Line: m.Fileset.Position(s.Pos()).Line, + Line: m.Props.Fileset.Position(s.Pos()).Line, Commit: m.Commit, - Filename: m.Fileset.Position(s.Pos()).Filename, + Filename: m.Props.Fileset.Position(s.Pos()).Filename, }) } } @@ -157,7 +157,7 @@ func (m *Model) lookUp(expr ast.Expr, bound_type int, spawning_for_loop bool) (* // var_name = VAR_PREFIX + var_name // } if err != nil { - ident = &promela_ast.Ident{Name: "not_found_" + strconv.Itoa(m.Fileset.Position(expr.Pos()).Line) + strconv.Itoa(m.Fileset.Position(expr.Pos()).Column)} + ident = &promela_ast.Ident{Name: "not_found_" + strconv.Itoa(m.Props.Fileset.Position(expr.Pos()).Line) + strconv.Itoa(m.Props.Fileset.Position(expr.Pos()).Column)} m.PrintFeature(Feature{ Proj_name: m.Project_name, @@ -168,7 +168,7 @@ func (m *Model) lookUp(expr ast.Expr, bound_type int, spawning_for_loop bool) (* Mandatory: mandatory, Line: 0, Commit: m.Commit, - Filename: m.Fileset.Position(m.Fun.Pos()).Filename, + Filename: m.Props.Fileset.Position(m.Fun.Pos()).Filename, }) if spawning_for_loop { @@ -184,9 +184,9 @@ func (m *Model) lookUp(expr ast.Expr, bound_type int, spawning_for_loop bool) (* Name: "Comm Param", Mandatory: mandatory, Info: ident.Name, - 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, }) m.PrintCommParFeature(expr, bound, mandatory) diff --git a/promela/mutex.go b/promela/mutex.go index 200788f49..edd53e242 100755 --- a/promela/mutex.go +++ b/promela/mutex.go @@ -16,14 +16,14 @@ func (m *Model) TranslateMutexOp(call_expr *ast.CallExpr) (b *promela_ast.BlockS case "Lock", "RLock", "Unlock", "RUnlock": chan_to_use = name.Sel.Name default: - return nil, errors.New(UNKNOWN_MUTEX_OP + m.Fileset.Position(call_expr.Pos()).String()) + return nil, errors.New(UNKNOWN_MUTEX_OP + m.Props.Fileset.Position(call_expr.Pos()).String()) } if m.containsMutex(name.X) { b.List = append(b.List, &promela_ast.RcvStmt{ - Rcv: m.Fileset.Position(name.Pos()), + Rcv: m.Props.Fileset.Position(name.Pos()), Model: chan_to_use + "()", Chan: &promela_ast.SelectorExpr{ X: &promela_ast.Ident{ @@ -32,15 +32,15 @@ func (m *Model) TranslateMutexOp(call_expr *ast.CallExpr) (b *promela_ast.BlockS Rhs: &promela_ast.Ident{Name: "ok"}, }, &promela_ast.AssertStmt{ - Pos: m.Fileset.Position(name.Pos()), + Pos: m.Props.Fileset.Position(name.Pos()), Model: chan_to_use + "()", - Expr: &promela_ast.Ident{Name: "ok"}, + Expr: &promela_ast.Ident{Name: "ok"}, }) } else { - return nil, errors.New(UNKNOWN_MUTEX + m.Fileset.Position(call_expr.Pos()).String()) + return nil, errors.New(UNKNOWN_MUTEX + m.Props.Fileset.Position(call_expr.Pos()).String()) } default: - return nil, errors.New(MUTEX_OP_ON_NON_SEL + m.Fileset.Position(call_expr.Pos()).String()) + return nil, errors.New(MUTEX_OP_ON_NON_SEL + m.Props.Fileset.Position(call_expr.Pos()).String()) } return b, nil diff --git a/promela/print-type.go b/promela/print-type.go index e1ccf6330..38f61e966 100755 --- a/promela/print-type.go +++ b/promela/print-type.go @@ -23,9 +23,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Receive as a " + bound, Mandatory: mandatory, Info: prettyPrint(expr) + " Mandatory : " + mandatory, - 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, }) } else if expr.Op == token.AND { m.PrintFeature(Feature{ @@ -35,9 +35,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Pointer as a " + bound, Mandatory: mandatory, Info: prettyPrint(expr.X), - 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, }) } @@ -50,9 +50,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Func as a " + bound, Mandatory: mandatory, Info: prettyPrint(expr), - 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, }) if m.getIdent(expr.Fun).Name == "len" { m.PrintFeature(Feature{ @@ -62,9 +62,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "len() as a " + bound, Mandatory: mandatory, Info: prettyPrint(expr), - 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, }) } @@ -78,9 +78,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Struct as a " + bound, Mandatory: mandatory, 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, }) case *ast.IndexExpr: m.PrintFeature(Feature{ @@ -90,8 +90,8 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Fun: m.Fun.Name.Name, Proj_name: m.Project_name, Model: m.Name, - Line: m.Fileset.Position(expr.Pos()).Line, - Filename: m.Fileset.Position(expr.Pos()).String(), + Line: m.Props.Fileset.Position(expr.Pos()).Line, + Filename: m.Props.Fileset.Position(expr.Pos()).String(), Commit: m.Commit, }) @@ -103,14 +103,14 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Fun: m.Fun.Name.Name, Proj_name: m.Project_name, Model: m.Name, - Line: m.Fileset.Position(expr.Pos()).Line, - Filename: m.Fileset.Position(expr.Pos()).String(), + Line: m.Props.Fileset.Position(expr.Pos()).Line, + Filename: m.Props.Fileset.Position(expr.Pos()).String(), Commit: m.Commit, }) default: Types := m.AstMap[m.Package].TypesInfo.TypeOf(expr) if Types == nil { - fmt.Println("Could not find type of expr : ", expr, " in package :", m.Package, "at pos : ", m.Fileset.Position(expr.Pos())) + fmt.Println("Could not find type of expr : ", expr, " in package :", m.Package, "at pos : ", m.Props.Fileset.Position(expr.Pos())) } else { switch Types := Types.(type) { case *types.Struct: @@ -122,9 +122,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Field of a struct as a " + bound, Mandatory: mandatory, 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, }) case *types.Basic: @@ -137,9 +137,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Integer as a " + bound, Mandatory: mandatory, Info: isConstant(expr), - 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, }) } else { m.PrintFeature(Feature{ @@ -149,9 +149,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Var as a " + bound, Mandatory: mandatory, Info: "Name :" + fmt.Sprint(expr), - 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, }) } @@ -163,9 +163,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Slice as a " + bound, Mandatory: mandatory, Info: prettyPrint(expr), - 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, }) case *types.Map: m.PrintFeature(Feature{ @@ -175,9 +175,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Map as a " + bound, Mandatory: mandatory, Info: Types.String(), - 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, }) case *types.Named: m.PrintFeature(Feature{ @@ -187,9 +187,9 @@ func (m *Model) PrintCommParFeature(expr ast.Expr, bound string, mandatory strin Name: "Var as a " + bound, Mandatory: mandatory, Info: Types.String(), - 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, }) } } diff --git a/promela/promela_ast/proctype.go b/promela/promela_ast/proctype.go index 4dd079706..e23c179fe 100755 --- a/promela/promela_ast/proctype.go +++ b/promela/promela_ast/proctype.go @@ -12,7 +12,7 @@ type Proctype struct { Pos token.Position Active bool // is it an active process ? Body *BlockStmt // the body of the process - Params []*Param + Params []Expr Decl *ast.FuncDecl } @@ -49,7 +49,7 @@ func (p *Proctype) Print(num_tabs int) (stmt string) { return } func (s *Proctype) Clone() Stmt { - s1 := &Proctype{Pos: s.Pos, Name: s.Name.Clone().(*Ident), Body: s.Body.Clone().(*BlockStmt), Active: s.Active, Params: []*Param{}} + s1 := &Proctype{Pos: s.Pos, Name: s.Name.Clone().(*Ident), Body: s.Body.Clone().(*BlockStmt), Active: s.Active, Params: []Expr{}} for _, p := range s.Params { s1.Params = append(s1.Params, p.Clone().(*Param)) diff --git a/promela/promela_translator.go b/promela/promela_translator.go index 928c77ce3..c68edaddf 100755 --- a/promela/promela_translator.go +++ b/promela/promela_translator.go @@ -32,7 +32,21 @@ var ( Features = []Feature{} ) +// GlobalProps captures traits that are relevant and must be preserved and updated across models. +type GlobalProps struct { + Fileset *token.FileSet + + // Relevant flags + ContainsWg bool + ContainsChan bool + ContainsMutexes bool + ContainsReceiver bool + ContainsClose bool // Does the partition contain a close statement ? +} + type Model struct { + Props *GlobalProps + Result_fodler string // the name of the folder where the model need to ne printed Project_name string // the full name of project (eg. "nicolasdilley/Gomela") Package string // the name of the package @@ -40,7 +54,6 @@ type Model struct { Commit string // the commit of the project RecFuncs []RecFunc SpawningFuncs []*SpawningFunc - Fileset *token.FileSet FuncDecls []*ast.FuncDecl // A list of all the funcdecl declared in the function being modelled (ie, fun := func(){ return true}) Proctypes []*promela_ast.Proctype // the processes representing the functions of the model Inlines []*promela_ast.Inline // the inlines function that represent the commpar args that are function calls @@ -48,23 +61,17 @@ type Model struct { Chans map[ast.Expr]*ChanStruct // the promela chan used in the module mapped to their go expr WaitGroups map[ast.Expr]*WaitGroupStruct // the promela chan used in the module mapped to their go expr Mutexes []ast.Expr // The promela mutex declaration - ContainsWg bool - ContainsChan bool - ContainsMutexes bool - ContainsReceiver bool - ContainsClose bool // Does the partition contain a close statement ? - Init *promela_ast.InitDef // The proctype consisting of the "main" function of the source program - Global_vars []promela_ast.Stmt // the global variable used in the ltl properties - Defines []promela_ast.DefineStmt // the channel bounds - CommPars []*CommPar // the communications paramer - Features []Feature // The features for the survey - ClosedVars map[*ChanStruct][]ast.Expr // The variable that are used to test if a channel is closed when receiving (i.e ok in r,ok := >-ch ) - process_counter int // to give unique name to Promela processes - func_counter int // to give unique name to inline func call - For_counter *ForCounter // Used to translate the for loop to break out properly out of them - Counter int // used to differentiate call expr channels - AstMap map[string]*packages.Package // the map used to find the type of the channels - Chan_closing bool + Init *promela_ast.InitDef // The proctype consisting of the "main" function of the source program + Global_vars []promela_ast.Stmt // the global variable used in the ltl properties + Defines []promela_ast.DefineStmt // the channel bounds + CommPars []*CommPar // the communications paramer + Features []Feature // The features for the survey + ClosedVars map[*ChanStruct][]ast.Expr // The variable that are used to test if a channel is closed when receiving (i.e ok in r,ok := >-ch ) + process_counter int // to give unique name to Promela processes + func_counter int // to give unique name to inline func call + For_counter *ForCounter // Used to translate the for loop to break out properly out of them + Counter int // used to differentiate call expr channels + AstMap map[string]*packages.Package // the map used to find the type of the channels Projects_folder string GenerateFeatures bool // should the model print features ? Current_return_label string @@ -105,7 +112,7 @@ func (m *Model) GoToPromela(SEP string) { }, true) m.Init = &promela_ast.InitDef{ - Def: m.Fileset.Position(m.Fun.Pos()), + Def: m.Props.Fileset.Position(m.Fun.Pos()), Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}, } @@ -138,7 +145,7 @@ func (m *Model) GoToPromela(SEP string) { Mandatory: "false", Line: 0, Commit: m.Commit, - Filename: m.Fileset.Position(m.Fun.Pos()).Filename, + Filename: m.Props.Fileset.Position(m.Fun.Pos()).Filename, }, m) } } @@ -206,13 +213,13 @@ func (m *Model) translateStruct(s ast.Stmt, lhs ast.Expr, t types.Type, seen []* if inter_pro <= MAX_STRUCTS_INTER_PRO { if t.String() == "sync.WaitGroup" { if !new_var { - return b, errors.New(WG_ALIASING + m.Fileset.Position(lhs.Pos()).String()) + return b, errors.New(WG_ALIASING + m.Props.Fileset.Position(lhs.Pos()).String()) } return m.translateWg(s, lhs) } else if t.String() == "sync.Mutex" || t.String() == "sync.RWMutex" { if !new_var { - return b, errors.New(MUTEX_ALIASING + m.Fileset.Position(lhs.Pos()).String()) + return b, errors.New(MUTEX_ALIASING + m.Props.Fileset.Position(lhs.Pos()).String()) } return m.translateMutex(s, lhs) } @@ -231,39 +238,39 @@ func (m *Model) translateStruct(s ast.Stmt, lhs ast.Expr, t types.Type, seen []* elem := GetElemIfPointer(field.Elem()) switch elem := elem.(type) { case *types.Chan: - return b, errors.New(CHAN_IN_LIST + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(CHAN_IN_LIST + m.Props.Fileset.Position(s.Pos()).String()) default: if elem.String() == "sync.WaitGroup" { - return b, errors.New(WG_IN_LIST + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(WG_IN_LIST + m.Props.Fileset.Position(s.Pos()).String()) } if elem.String() == "sync.Mutex" || elem.String() == "sync.RWMutex" { - return b, errors.New(MUTEX_IN_LIST + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(MUTEX_IN_LIST + m.Props.Fileset.Position(s.Pos()).String()) } } case *types.Slice: elem := GetElemIfPointer(field.Elem()) switch elem := elem.(type) { case *types.Chan: - return b, errors.New(CHAN_IN_LIST + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(CHAN_IN_LIST + m.Props.Fileset.Position(s.Pos()).String()) default: if elem.String() == "sync.WaitGroup" { - return b, errors.New(WG_IN_LIST + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(WG_IN_LIST + m.Props.Fileset.Position(s.Pos()).String()) } if elem.String() == "sync.Mutex" || elem.String() == "sync.RWMutex" { - return b, errors.New(MUTEX_IN_LIST + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(MUTEX_IN_LIST + m.Props.Fileset.Position(s.Pos()).String()) } } case *types.Map: elem := GetElemIfPointer(field.Elem()) switch elem := elem.(type) { case *types.Chan: - return b, errors.New(CHAN_IN_MAP + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(CHAN_IN_MAP + m.Props.Fileset.Position(s.Pos()).String()) default: if elem.String() == "sync.WaitGroup" { - return b, errors.New(WG_IN_MAP + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(WG_IN_MAP + m.Props.Fileset.Position(s.Pos()).String()) } if elem.String() == "sync.Mutex" || elem.String() == "sync.RWMutex" { - return b, errors.New(MUTEX_IN_MAP + m.Fileset.Position(s.Pos()).String()) + return b, errors.New(MUTEX_IN_MAP + m.Props.Fileset.Position(s.Pos()).String()) } } @@ -366,7 +373,7 @@ func (m *Model) lookForChans(lhs ast.Expr, rhs ast.Expr, new_var bool) (b *prome switch c.Args[0].(type) { case *ast.ChanType: if !new_var { - return b, errors.New(CHAN_ALIASING + m.Fileset.Position(lhs.Pos()).String()) + return b, errors.New(CHAN_ALIASING + m.Props.Fileset.Position(lhs.Pos()).String()) } b1, err1 := m.translateChan(lhs, c.Args) @@ -405,7 +412,7 @@ func (m *Model) lookForChans(lhs ast.Expr, rhs ast.Expr, new_var bool) (b *prome default: switch c.Type.(type) { case *ast.StructType: - panic(fmt.Sprint("A key on a struct must be an Ident at pos : ", m.Fileset.Position(c.Pos()), " with ", expr, " and key :", expr.Key)) + panic(fmt.Sprint("A key on a struct must be an Ident at pos : ", m.Props.Fileset.Position(c.Pos()), " with ", expr, " and key :", expr.Key)) } } @@ -418,7 +425,7 @@ func (m *Model) lookForChans(lhs ast.Expr, rhs ast.Expr, new_var bool) (b *prome addBlock(b, b1) // default: - // ast.Print(m.Fileset, expr) + // ast.Print(m.Props.Fileset. expr) } } @@ -434,10 +441,10 @@ func (m *Model) translateWg(s ast.Stmt, name ast.Expr) (b *promela_ast.BlockStmt prom_wg_name := translateIdent(name) if !m.containsWaitgroup(name) { - m.ContainsWg = true + m.Props.ContainsWg = true m.WaitGroups[name] = &WaitGroupStruct{ Name: &prom_wg_name, - Wait: m.Fileset.Position(name.Pos()), + Wait: m.Props.Fileset.Position(name.Pos()), Counter: 0, } @@ -448,9 +455,9 @@ func (m *Model) translateWg(s ast.Stmt, name ast.Expr) (b *promela_ast.BlockStmt Name: "new WaitGroup", Info: "Name :" + prom_wg_name.Name, Mandatory: "false", - Line: m.Fileset.Position(s.Pos()).Line, + Line: m.Props.Fileset.Position(s.Pos()).Line, Commit: m.Commit, - Filename: m.Fileset.Position(s.Pos()).Filename, + Filename: m.Props.Fileset.Position(s.Pos()).Filename, }) b.List = append(b.List, @@ -464,11 +471,11 @@ func (m *Model) translateWg(s ast.Stmt, name ast.Expr) (b *promela_ast.BlockStmt Fun: m.Fun.Name.String(), Name: "WaitGroup in for", Mandatory: "false", - Line: m.Fileset.Position(s.Pos()).Line, + Line: m.Props.Fileset.Position(s.Pos()).Line, Commit: m.Commit, - Filename: m.Fileset.Position(s.Pos()).Filename, + Filename: m.Props.Fileset.Position(s.Pos()).Filename, }) - err = errors.New(WAITGROUP_IN_FOR + m.Fileset.Position(s.Pos()).String()) + err = errors.New(WAITGROUP_IN_FOR + m.Props.Fileset.Position(s.Pos()).String()) } return b, err @@ -480,7 +487,7 @@ func (m *Model) translateMutex(s ast.Stmt, prom_mutex_name ast.Expr) (b *promela if !m.For_counter.In_for { if !m.containsMutex(prom_mutex_name) { - m.ContainsMutexes = true + m.Props.ContainsMutexes = true name := translateIdent(prom_mutex_name) m.Mutexes = append(m.Mutexes, prom_mutex_name) m.PrintFeature(Feature{ @@ -490,9 +497,9 @@ func (m *Model) translateMutex(s ast.Stmt, prom_mutex_name ast.Expr) (b *promela Name: "new Mutex", Info: "Name :" + translateIdent(prom_mutex_name).Name, Mandatory: "false", - Line: m.Fileset.Position(s.Pos()).Line, + Line: m.Props.Fileset.Position(s.Pos()).Line, Commit: m.Commit, - Filename: m.Fileset.Position(s.Pos()).Filename, + Filename: m.Props.Fileset.Position(s.Pos()).Filename, }) b.List = append(b.List, @@ -506,11 +513,11 @@ func (m *Model) translateMutex(s ast.Stmt, prom_mutex_name ast.Expr) (b *promela Fun: m.Fun.Name.String(), Name: "Mutex in for", Mandatory: "false", - Line: m.Fileset.Position(s.Pos()).Line, + Line: m.Props.Fileset.Position(s.Pos()).Line, Commit: m.Commit, - Filename: m.Fileset.Position(s.Pos()).Filename, + Filename: m.Props.Fileset.Position(s.Pos()).Filename, }) - err = errors.New(MUTEX_IN_FOR + m.Fileset.Position(s.Pos()).String()) + err = errors.New(MUTEX_IN_FOR + m.Props.Fileset.Position(s.Pos()).String()) } return b, err @@ -523,7 +530,7 @@ func (m *Model) translateChan(go_chan_name ast.Expr, args []ast.Expr) (b *promel // a new channel is found lets change its name, rename it in function and add to struct prom_chan_name := translateIdent(go_chan_name) prom_chan_name.Name += CHAN_NAME - channel := &ChanStruct{Name: &prom_chan_name, Chan: m.Fileset.Position(go_chan_name.Pos())} + channel := &ChanStruct{Name: &prom_chan_name, Chan: m.Props.Fileset.Position(go_chan_name.Pos())} var size *promela_ast.Ident @@ -536,16 +543,16 @@ func (m *Model) translateChan(go_chan_name ast.Expr, args []ast.Expr) (b *promel } chan_def := &ChanDefDeclStmt{ - Decl: m.Fileset.Position(go_chan_name.Pos()), + Decl: m.Props.Fileset.Position(go_chan_name.Pos()), Name: &prom_chan_name, Size: size, - M: m, + M: m.Props, } b.List = append(b.List, chan_def) m.Chans[go_chan_name] = channel - m.ContainsChan = true + m.Props.ContainsChan = true m.PrintFeature(Feature{ Proj_name: m.Project_name, Model: m.Name, @@ -565,11 +572,11 @@ func (m *Model) translateChan(go_chan_name ast.Expr, args []ast.Expr) (b *promel Fun: m.Fun.Name.String(), Name: "Chan in for", Mandatory: "false", - Line: m.Fileset.Position(go_chan_name.Pos()).Line, + Line: m.Props.Fileset.Position(go_chan_name.Pos()).Line, Commit: m.Commit, - Filename: m.Fileset.Position(go_chan_name.Pos()).Filename, + Filename: m.Props.Fileset.Position(go_chan_name.Pos()).Filename, }) - err = errors.New(CHAN_IN_FOR + m.Fileset.Position(go_chan_name.Pos()).String()) + err = errors.New(CHAN_IN_FOR + m.Props.Fileset.Position(go_chan_name.Pos()).String()) } return b, err } @@ -651,26 +658,25 @@ func (m *Model) TranslateExpr(expr ast.Expr) (b *promela_ast.BlockStmt, err erro switch name := expr.Fun.(type) { case *ast.Ident: if name.Name == "close" && len(expr.Args) == 1 { // closing a chan - rcv := &promela_ast.RcvStmt{Model: "Close", Rcv: m.Fileset.Position(name.Pos())} + rcv := &promela_ast.RcvStmt{Model: "Close", Rcv: m.Props.Fileset.Position(name.Pos())} if m.containsChan(expr.Args[0]) { - m.ContainsClose = true + m.Props.ContainsClose = true chan_name := m.getChanStruct(expr.Args[0]) rcv.Chan = &promela_ast.SelectorExpr{ X: chan_name.Name, Sel: &promela_ast.Ident{Name: "closing"}, - Pos: m.Fileset.Position(expr.Args[0].Pos()), + Pos: m.Props.Fileset.Position(expr.Args[0].Pos()), } rcv.Rhs = &promela_ast.Ident{Name: "closed"} - m.Chan_closing = true - assert := &promela_ast.AssertStmt{Model: "Close", Pos: m.Fileset.Position(expr.Pos()), Expr: &promela_ast.Ident{Name: "!closed"}} + assert := &promela_ast.AssertStmt{Model: "Close", Pos: m.Props.Fileset.Position(expr.Pos()), Expr: &promela_ast.Ident{Name: "!closed"}} stmts.List = append(stmts.List, rcv, assert) } else { - return stmts, errors.New(UNKNOWN_CHAN_CLOSE + m.Fileset.Position(expr.Pos()).String()) + return stmts, errors.New(UNKNOWN_CHAN_CLOSE + m.Props.Fileset.Position(expr.Pos()).String()) } } else if name.Name == "panic" && len(expr.Args) == 1 { // panic call - stmts.List = append(stmts.List, &promela_ast.CallExpr{Call: m.Fileset.Position(expr.Pos()), Model: "Panic", Fun: &promela_ast.Ident{Name: "assert"}, Args: []promela_ast.Expr{&promela_ast.Ident{Name: "20==0"}}}) + stmts.List = append(stmts.List, &promela_ast.CallExpr{Call: m.Props.Fileset.Position(expr.Pos()), Model: "Panic", Fun: &promela_ast.Ident{Name: "assert"}, Args: []promela_ast.Expr{&promela_ast.Ident{Name: "20==0"}}}) } else { call, err1 := m.TranslateCallExpr(expr) @@ -1009,7 +1015,7 @@ func isRecursive(pack string, block *ast.BlockStmt, ast_map map[string]*packages // Takes a commPar and genrate a define stmt out of the name of the commPar and the function under analysis // Returns the name of the defined variable func (m *Model) GenerateDefine(commPar *CommPar) string { - var_name := DEF_PREFIX + VAR_PREFIX + commPar.Name.Name + strconv.Itoa(m.Fileset.Position(commPar.Expr.Pos()).Line) + var_name := DEF_PREFIX + VAR_PREFIX + commPar.Name.Name + strconv.Itoa(m.Props.Fileset.Position(commPar.Expr.Pos()).Line) rhs := DEFAULT_BOUND if commPar.Mandatory { @@ -1019,8 +1025,8 @@ func (m *Model) GenerateDefine(commPar *CommPar) string { rhs += " // opt " } var buff *bytes.Buffer = bytes.NewBuffer([]byte{}) - printer.Fprint(buff, m.Fileset, commPar.Expr) - rhs += string(buff.Bytes()) + " line " + strconv.Itoa(m.Fileset.Position(commPar.Expr.Pos()).Line) + printer.Fprint(buff, m.Props.Fileset, commPar.Expr) + rhs += string(buff.Bytes()) + " line " + strconv.Itoa(m.Props.Fileset.Position(commPar.Expr.Pos()).Line) m.Defines = append(m.Defines, promela_ast.DefineStmt{Name: &promela_ast.Ident{Name: var_name}, Rhs: &promela_ast.Ident{Name: rhs}}) @@ -1169,13 +1175,10 @@ func (m *Model) newModel(pack string, fun *ast.FuncDecl) *Model { Commit: m.Commit, RecFuncs: []RecFunc{}, SpawningFuncs: m.SpawningFuncs, - Fileset: m.Fileset, Proctypes: m.Proctypes, Inlines: m.Inlines, Fun: fun, - ContainsChan: m.ContainsChan, - ContainsWg: m.ContainsWg, - ContainsReceiver: m.ContainsReceiver, + Props: m.Props, Chans: make(map[ast.Expr]*ChanStruct), WaitGroups: make(map[ast.Expr]*WaitGroupStruct), Mutexes: []ast.Expr{}, @@ -1190,7 +1193,6 @@ func (m *Model) newModel(pack string, fun *ast.FuncDecl) *Model { For_counter: m.For_counter, Counter: m.Counter, AstMap: m.AstMap, - Chan_closing: m.Chan_closing, Projects_folder: m.Projects_folder, ClosedVars: make(map[*ChanStruct][]ast.Expr), GenerateFeatures: m.GenerateFeatures, diff --git a/promela/range_stmt.go b/promela/range_stmt.go index 6d57d6c89..974d150a6 100755 --- a/promela/range_stmt.go +++ b/promela/range_stmt.go @@ -12,7 +12,7 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, b = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} defers = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} - d := &promela_ast.DoStmt{Do: m.Fileset.Position(s.Pos())} + d := &promela_ast.DoStmt{Do: m.Props.Fileset.Position(s.Pos())} had_go := m.For_counter.With_go was_in_for := m.For_counter.In_for //used to check if this is the outer loop @@ -40,8 +40,7 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, m.GenerateFeatures = true if m.containsChan(s.X) { - - m.ContainsClose = true + m.Props.ContainsClose = true m.PrintFeature(Feature{ Proj_name: m.Project_name, @@ -51,7 +50,7 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, Mandatory: "", Line: 0, Commit: m.Commit, - Filename: m.Fileset.Position(s.X.Pos()).Filename, + Filename: m.Props.Fileset.Position(s.X.Pos()).Filename, }) chan_name := m.getChanStruct(s.X) do_guard := &promela_ast.SingleGuardStmt{Cond: &promela_ast.Ident{Name: "true"}} @@ -60,7 +59,7 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, sync_rcv := &promela_ast.RcvStmt{Chan: &promela_ast.SelectorExpr{X: chan_name.Name, Sel: &promela_ast.Ident{Name: "sync"}}, Rhs: &promela_ast.Ident{Name: "state"}} - async_guard := &promela_ast.SingleGuardStmt{Cond: async_rcv, Guard: m.Fileset.Position(s.Pos()), Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} + async_guard := &promela_ast.SingleGuardStmt{Cond: async_rcv, Guard: m.Props.Fileset.Position(s.Pos()), Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} sync_guard := &promela_ast.SingleGuardStmt{ Cond: sync_rcv, @@ -74,7 +73,7 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, }}}, } rcv := &promela_ast.IfStmt{ - If: m.Fileset.Position(s.Pos()), + If: m.Props.Fileset.Position(s.Pos()), Model: "Range", Guards: []promela_ast.GuardStmt{async_guard, sync_guard}, Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} @@ -86,7 +85,7 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} if len(d1.List) > 0 { - return b, d1, errors.New(DEFER_IN_RANGE + m.Fileset.Position(s.Pos()).String()) + return b, d1, errors.New(DEFER_IN_RANGE + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { err = err1 @@ -97,7 +96,7 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, b.List = append(b.List, d, for_label) } else if isChan { - return b, b, errors.New(UNKNOWN_RANGE + m.Fileset.Position(s.Pos()).String()) + return b, b, errors.New(UNKNOWN_RANGE + m.Props.Fileset.Position(s.Pos()).String()) } else { // change into (for i:=0; i < len(x);i++) @@ -111,25 +110,25 @@ func (m *Model) translateRangeStmt(s *ast.RangeStmt) (b *promela_ast.BlockStmt, err = err1 } if len(d1.List) > 0 { - return b, d1, errors.New(DEFER_IN_RANGE + m.Fileset.Position(s.Pos()).String()) + return b, d1, errors.New(DEFER_IN_RANGE + m.Props.Fileset.Position(s.Pos()).String()) } block_stmt := s1 if m.spawns(s.Body, false) { // 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()), Lb: &promela_ast.Ident{Name: "0"}, Ub: &promela_ast.Ident{Name: ub.Name + "-1"}, Body: block_stmt}) + b.List = append(b.List, &promela_ast.ForStmt{For: m.Props.Fileset.Position(s.Pos()), Lb: &promela_ast.Ident{Name: "0"}, Ub: &promela_ast.Ident{Name: ub.Name + "-1"}, Body: block_stmt}) b.List = append(b.List, for_label) } else if containsMSP(s1) { ub.Name += "-1" // generate the optionnal loop // print the for loop with the if - if_stmt := &promela_ast.IfStmt{If: m.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} + if_stmt := &promela_ast.IfStmt{If: m.Props.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} ub_not_given := promela_ast.BinaryExpr{Lhs: ub, Rhs: &promela_ast.Ident{Name: "-3"}, Op: "!="} then := &promela_ast.SingleGuardStmt{ Cond: &ub_not_given, - Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{&promela_ast.ForStmt{For: m.Fileset.Position(s.Pos()), Lb: &promela_ast.Ident{Name: "0"}, Ub: ub, Body: block_stmt}, for_label}}, + Body: &promela_ast.BlockStmt{List: []promela_ast.Stmt{&promela_ast.ForStmt{For: m.Props.Fileset.Position(s.Pos()), Lb: &promela_ast.Ident{Name: "0"}, Ub: ub, Body: block_stmt}, for_label}}, } // else part diff --git a/promela/rcv_stmt.go b/promela/rcv_stmt.go index c31afaa99..c91168051 100755 --- a/promela/rcv_stmt.go +++ b/promela/rcv_stmt.go @@ -21,9 +21,9 @@ func (m *Model) translateRcvStmt( chan_name := m.getChanStruct(e) guard = &GenRcvStmt{ - Rcv: m.Fileset.Position(e.Pos()), + Rcv: m.Props.Fileset.Position(e.Pos()), Chan: chan_name.Name, - M: m, + M: m.Props, Sync_body: body, Async_body: body2, } @@ -36,7 +36,7 @@ func (m *Model) translateRcvStmt( Cond: &promela_ast.Ident{Name: "true"}, Body: body} } else { - err = errors.New(UNKNOWN_RCV + m.Fileset.Position(e.Pos()).String()) + err = errors.New(UNKNOWN_RCV + m.Props.Fileset.Position(e.Pos()).String()) } } diff --git a/promela/return_stmt.go b/promela/return_stmt.go index 5ee2fa8a4..95470bae1 100755 --- a/promela/return_stmt.go +++ b/promela/return_stmt.go @@ -18,22 +18,22 @@ func (m *Model) translateReturnStmt(s *ast.ReturnStmt) (b *promela_ast.BlockStmt } if m.containsChan(spec) { - return b, defers, errors.New(RETURN_CHAN + m.Fileset.Position(spec.Pos()).String()) + return b, defers, errors.New(RETURN_CHAN + m.Props.Fileset.Position(spec.Pos()).String()) } if m.containsWaitgroup(spec) { - return b, defers, errors.New(RETURN_WG + m.Fileset.Position(spec.Pos()).String()) + return b, defers, errors.New(RETURN_WG + m.Props.Fileset.Position(spec.Pos()).String()) } if m.containsMutex(spec) { - return b, defers, errors.New(RETURN_MUTEX + m.Fileset.Position(spec.Pos()).String()) + return b, defers, errors.New(RETURN_MUTEX + m.Props.Fileset.Position(spec.Pos()).String()) } if m.isStructWithChans(spec) { - return b, defers, errors.New(RETURN_STRUCT + m.Fileset.Position(spec.Pos()).String()) + return b, defers, errors.New(RETURN_STRUCT + m.Props.Fileset.Position(spec.Pos()).String()) } addBlock(b, expr) } - b.List = append(b.List, &promela_ast.GotoEndStmt{Goto: m.Fileset.Position(s.Pos()), Name: m.Current_return_label}) + b.List = append(b.List, &promela_ast.GotoEndStmt{Goto: m.Props.Fileset.Position(s.Pos()), Name: m.Current_return_label}) return b, defers, err } diff --git a/promela/select_stmt.go b/promela/select_stmt.go index 077a68dc8..e2ea54565 100755 --- a/promela/select_stmt.go +++ b/promela/select_stmt.go @@ -12,7 +12,7 @@ import ( func (m *Model) translateSelectStmt(s *ast.SelectStmt) (b *promela_ast.BlockStmt, defers *promela_ast.BlockStmt, err error) { b = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} defers = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} - i := &promela_ast.SelectStmt{Select: m.Fileset.Position(s.Pos()), Model: "Select"} + i := &promela_ast.SelectStmt{Select: m.Props.Fileset.Position(s.Pos()), Model: "Select"} was_in_for := m.For_counter.In_for //used to check if this is the outer loop had_go := m.For_counter.With_go @@ -46,7 +46,7 @@ func (m *Model) translateSelectStmt(s *ast.SelectStmt) (b *promela_ast.BlockStmt body, d1, err1 := m.TranslateBlockStmt(&ast.BlockStmt{List: comm.Body}) if len(d1.List) > 0 { - return b, d1, errors.New(DEFER_IN_SELECT + m.Fileset.Position(s.Pos()).String()) + return b, d1, errors.New(DEFER_IN_SELECT + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { return b, defers, err1 @@ -69,16 +69,16 @@ func (m *Model) translateSelectStmt(s *ast.SelectStmt) (b *promela_ast.BlockStmt chan_name := m.getChanStruct(com.Chan) gen_send := &GenSendStmt{ - Send: m.Fileset.Position(s.Pos()), + Send: m.Props.Fileset.Position(s.Pos()), Chan: chan_name.Name, - M: m, + M: m.Props, Sync_body: body, Async_body: body2, } i.Guards = append(i.Guards, gen_send) } else { - err = errors.New(UNKNOWN_SEND + m.Fileset.Position(com.Chan.Pos()).String()) + err = errors.New(UNKNOWN_SEND + m.Props.Fileset.Position(com.Chan.Pos()).String()) return b, defers, err } @@ -116,7 +116,7 @@ func (m *Model) translateSelectStmt(s *ast.SelectStmt) (b *promela_ast.BlockStmt } else { // it is default i.Has_default = true m.checkForBreak(body, goto_stmt) - i.Guards = append(i.Guards, &promela_ast.SingleGuardStmt{Cond: &promela_ast.Ident{Name: "true"}, Guard: m.Fileset.Position(comm.Pos()), Body: body}) + i.Guards = append(i.Guards, &promela_ast.SingleGuardStmt{Cond: &promela_ast.Ident{Name: "true"}, Guard: m.Props.Fileset.Position(comm.Pos()), Body: body}) } } } @@ -124,7 +124,7 @@ func (m *Model) translateSelectStmt(s *ast.SelectStmt) (b *promela_ast.BlockStmt if len(i.Guards) > 0 { b.List = append(b.List, i, goto_stmt.Label, goto_end_stmt.Label) } else { - return nil, nil, errors.New(SELECT_WITH_NO_BRANCH + m.Fileset.Position(s.Pos()).String()) + return nil, nil, errors.New(SELECT_WITH_NO_BRANCH + m.Props.Fileset.Position(s.Pos()).String()) } diff --git a/promela/send_stmt.go b/promela/send_stmt.go index 222766049..3e2b2c522 100755 --- a/promela/send_stmt.go +++ b/promela/send_stmt.go @@ -20,7 +20,7 @@ func (m *Model) translateSendStmt(s *ast.SendStmt) (b *promela_ast.BlockStmt, er }) if_stmt := &promela_ast.IfStmt{ - If: m.Fileset.Position(s.Pos()), + If: m.Props.Fileset.Position(s.Pos()), Model: "Send", Init: &promela_ast.BlockStmt{ List: []promela_ast.Stmt{}, @@ -48,15 +48,15 @@ func (m *Model) generateGenSendStmt(e ast.Expr, body *promela_ast.BlockStmt, bod chan_name := m.getChanStruct(e) g = &GenSendStmt{ - Send: m.Fileset.Position(e.Pos()), + Send: m.Props.Fileset.Position(e.Pos()), Chan: chan_name.Name, - M: m, + M: m.Props, Sync_body: body, Async_body: body2, } } else { - err = errors.New(UNKNOWN_SEND + m.Fileset.Position(e.Pos()).String()) + err = errors.New(UNKNOWN_SEND + m.Props.Fileset.Position(e.Pos()).String()) } return g, err diff --git a/promela/switch_stmt.go b/promela/switch_stmt.go index f22e1e25a..ec60cab69 100755 --- a/promela/switch_stmt.go +++ b/promela/switch_stmt.go @@ -11,7 +11,7 @@ import ( func (m *Model) translateSwitchStmt(s *ast.SwitchStmt) (b *promela_ast.BlockStmt, defers *promela_ast.BlockStmt, err error) { b = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} defers = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} - i := &promela_ast.IfStmt{If: m.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} + i := &promela_ast.IfStmt{If: m.Props.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} tag, err1 := m.TranslateExpr(s.Tag) if err1 != nil { @@ -56,7 +56,7 @@ func (m *Model) translateSwitchStmt(s *ast.SwitchStmt) (b *promela_ast.BlockStmt } if len(d2.List) > 0 { - return b, d2, errors.New(DEFER_IN_SWITCH + m.Fileset.Position(s.Pos()).String()) + return b, d2, errors.New(DEFER_IN_SWITCH + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { return b, defers, err1 diff --git a/promela/type_switch_stmt.go b/promela/type_switch_stmt.go index 83d5f9048..382972373 100755 --- a/promela/type_switch_stmt.go +++ b/promela/type_switch_stmt.go @@ -11,7 +11,7 @@ import ( func (m *Model) translateTypeSwitchStmt(s *ast.TypeSwitchStmt) (b *promela_ast.BlockStmt, defers *promela_ast.BlockStmt, err error) { b = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} defers = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} - i := &promela_ast.IfStmt{If: m.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} + i := &promela_ast.IfStmt{If: m.Props.Fileset.Position(s.Pos()), Init: &promela_ast.BlockStmt{List: []promela_ast.Stmt{}}} for _, stmt := range s.Body.List { switch c := stmt.(type) { @@ -33,7 +33,7 @@ func (m *Model) translateTypeSwitchStmt(s *ast.TypeSwitchStmt) (b *promela_ast.B } if len(d2.List) > 0 { - return b, d2, errors.New(DEFER_IN_SWITCH + m.Fileset.Position(s.Pos()).String()) + return b, d2, errors.New(DEFER_IN_SWITCH + m.Props.Fileset.Position(s.Pos()).String()) } if err1 != nil { return b, defers, err1 diff --git a/promela/wg.go b/promela/wg.go index f60293760..4de8958e9 100644 --- a/promela/wg.go +++ b/promela/wg.go @@ -2,8 +2,10 @@ package promela import ( "go/ast" + "github.com/nicolasdilley/gomela/promela/promela_ast" ) + func (m *Model) parseWgFunc(call_expr *ast.CallExpr, name *ast.SelectorExpr) (stmts *promela_ast.BlockStmt, err error) { stmts = &promela_ast.BlockStmt{List: []promela_ast.Stmt{}} if name.Sel.Name == "Add" { @@ -21,27 +23,27 @@ func (m *Model) parseWgFunc(call_expr *ast.CallExpr, name *ast.SelectorExpr) (st Fun: m.Fun.Name.String(), Name: "Add in for", Mandatory: "true", - Line: m.Fileset.Position(name.Pos()).Line, + Line: m.Props.Fileset.Position(name.Pos()).Line, Info: "", Commit: m.Commit, - Filename: m.Fileset.Position(name.Pos()).Filename, + Filename: m.Props.Fileset.Position(name.Pos()).Filename, }) } stmts.List = append(stmts.List, &promela_ast.SendStmt{ - Send: m.Fileset.Position(name.Pos()), + Send: m.Props.Fileset.Position(name.Pos()), Model: "Add(" + ub.Name + ")", Chan: &promela_ast.Ident{Name: translateIdent(name.X).Name + ".update"}, Rhs: ub}, &promela_ast.RcvStmt{ // wait to receive the ack from the monitor Chan: &promela_ast.Ident{Name: translateIdent(name.X).Name + ".update_ack"}, - Rhs: &promela_ast.Ident{Name: "ok"}}, + Rhs: &promela_ast.Ident{Name: "ok"}}, - // Check that the monitor says its ok + // Check that the monitor says its ok &promela_ast.AssertStmt{ - Pos: m.Fileset.Position(call_expr.Pos()), + Pos: m.Props.Fileset.Position(call_expr.Pos()), Model: "Add(" + ub.Name + ")", - Expr: &promela_ast.Ident{Name: "ok"}}, + Expr: &promela_ast.Ident{Name: "ok"}}, ) } else if name.Sel.Name == "Done" { @@ -52,32 +54,31 @@ func (m *Model) parseWgFunc(call_expr *ast.CallExpr, name *ast.SelectorExpr) (st Fun: m.Fun.Name.String(), Name: "Done in for", Mandatory: "false", - Line: m.Fileset.Position(name.Pos()).Line, + Line: m.Props.Fileset.Position(name.Pos()).Line, Info: "", Commit: m.Commit, - Filename: m.Fileset.Position(name.Pos()).Filename, + Filename: m.Props.Fileset.Position(name.Pos()).Filename, }) } stmts.List = append(stmts.List, &promela_ast.SendStmt{ - Send: m.Fileset.Position(name.Pos()), + Send: m.Props.Fileset.Position(name.Pos()), Model: "Done", Chan: &promela_ast.Ident{Name: translateIdent(name.X).Name + ".update"}, Rhs: &promela_ast.Ident{Name: "-1"}}, &promela_ast.RcvStmt{ // wait to receive the ack from the monitor Chan: &promela_ast.Ident{Name: translateIdent(name.X).Name + ".update_ack"}, - Rhs: &promela_ast.Ident{Name: "ok"}}, + Rhs: &promela_ast.Ident{Name: "ok"}}, - // Check that the monitor says its ok + // Check that the monitor says its ok &promela_ast.AssertStmt{ - Pos: m.Fileset.Position(call_expr.Pos()), + Pos: m.Props.Fileset.Position(call_expr.Pos()), Model: "Done()", - Expr: &promela_ast.Ident{Name: "ok"}}, - + Expr: &promela_ast.Ident{Name: "ok"}}, ) } else if name.Sel.Name == "Wait" { stmts.List = append(stmts.List, &promela_ast.RcvStmt{ - Rcv: m.Fileset.Position(name.Pos()), + Rcv: m.Props.Fileset.Position(name.Pos()), Model: "Wait()", Chan: &promela_ast.Ident{Name: translateIdent(name.X).Name + ".wait"}, Rhs: &promela_ast.Ident{Name: "0"}})