main.go 14.3 KB
Newer Older
1
2
3
4
5
6
7
package main

import (
	"flag"
	"fmt"
	"go/ast"
	"go/format"
8
	"go/importer"
9
10
	"go/parser"
	"go/token"
11
	"go/types"
12
	"io"
13
14
15
	"io/ioutil"
	"os"
	"path"
16
	"regexp"
17
18
	"runtime"
	"strconv"
19
	"strings"
20
21
	"text/template"

22
23
	"golang.org/x/tools/go/ast/astutil"

hmoreau's avatar
hmoreau committed
24
	"gitlab.lrde.epita.fr/spot/go2pins/channel"
Antoine Martin's avatar
Antoine Martin committed
25
	"gitlab.lrde.epita.fr/spot/go2pins/decl"
26
	"gitlab.lrde.epita.fr/spot/go2pins/goroutine"
hmoreau's avatar
hmoreau committed
27
	"gitlab.lrde.epita.fr/spot/go2pins/tools"
Antoine Martin's avatar
Antoine Martin committed
28
29
	"gitlab.lrde.epita.fr/spot/go2pins/transform"
	"gitlab.lrde.epita.fr/spot/go2pins/transform/cfg"
30
31
)

32
// Generate a list of cgo CStrings from the provided string slice.
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
func variableNamesToC(variableNames []string) []ast.Expr {
	vn := make([]ast.Expr, len(variableNames))
	for i, v := range variableNames {
		vn[i] = &ast.CallExpr{
			Fun: &ast.SelectorExpr{
				X:   ast.NewIdent("C"),
				Sel: ast.NewIdent("CString"),
			},
			Args: []ast.Expr{
				&ast.BasicLit{
					Kind:  token.STRING,
					Value: strconv.Quote(v),
				},
			},
		}
	}
	return vn
}

52
// Compiles the input file `(path, src)` and writes it to `file`.
Etienne Renault's avatar
Etienne Renault committed
53
func compileTo(path string, src []byte, file *os.File,
54
	goroutines []*goroutine.Goroutine, rers *string) (string, error) {
55
	fset := token.NewFileSet()
56
	f, err := parser.ParseFile(fset, path, src, 0)
57
58
59
60
61

	if err != nil {
		return "", err
	}

62
	var config types.Config
63
	// FIXME: figure out if this is really needed
64
65
66
67
68
69
	config.Importer = importer.Default()
	info := &types.Info{
		Uses:       make(map[*ast.Ident]types.Object),
		Selections: make(map[*ast.SelectorExpr]*types.Selection),
	}

70
	// Ensure that our program type checks.
71
72
	_, err = config.Check(path, fset, []*ast.File{f}, info)

73
	// Apply all transformations.
74
	meta := transform.NewMeta(fset, info)
75
	res := transform.Apply(f, meta, &transform.TypeChecker{Blackbox: (*ignorefunc != "")})
76

77
	if *ignorefunc != "" || len(goroutines) != 0 {
78
		newsrc, blackbox := tools.Isolate(flag.Args()[0], *output, toIgnore)
hmoreau's avatar
hmoreau committed
79
80
81
82
83
		src = []byte(newsrc)
		f, err = parser.ParseFile(fset, path, src, 0)
		if err != nil {
			return "", err
		}
84
85
86
87
88
		if blackbox != "" {
			if err = os.MkdirAll(*output+"/blackbox", 0777); err != nil {
				fmt.Fprintln(os.Stderr, err.Error())
				os.Exit(1)
			}
hmoreau's avatar
hmoreau committed
89

90
91
92
93
94
			err = ioutil.WriteFile(*output+"/blackbox/blackbox.go", []byte(blackbox), 0666)
			if err != nil {
				fmt.Println(err)
				os.Exit(1)
			}
hmoreau's avatar
hmoreau committed
95
96
97
		}
	}

98
99
100
101
102
103
104
105
106
107
108
	// Check if file has recursion.
	if tools.CheckRecursion(string(src), *output) {
		fmt.Println("Recursion detected : applying transformation")
		fmt.Println("maxdepth set to", *maxdepth)
		src = []byte(tools.RewriteRecursion(string(src), *output, *maxdepth, *ignorefunc != ""))
		f, err = parser.ParseFile(fset, path, src, 0)
		if err != nil {
			return "", err
		}
	}

hmoreau's avatar
hmoreau committed
109
110
111
112
113
114
115
	for _, g := range goroutines {
		g.Status = meta.StateSize()
		meta.Create("Status", g.Name)
		g.LineCounter = meta.StateSize()
		meta.Create("LineCounter", g.Name)
	}

116
	res = transform.ApplyAll(f, meta, []transform.Transform{
117
		&transform.Channel{},
118
		&transform.NormalizeDeclarations{},
hmoreau's avatar
hmoreau committed
119
		&transform.Alive{},
120
		&transform.ArrayTreat{},
121
		&transform.ElseFull{},
122
		&transform.ArithmeticCall{},
123
		&transform.RegularizedAffect{},
124
		&transform.FunctionDefs{},
hmoreau's avatar
hmoreau committed
125
126
127
		&transform.RoutineAssignments{
			Functions: goroutines,
		},
hmoreau's avatar
hmoreau committed
128
		&transform.AfterChannel{},
129
		&transform.LocalVariableAssignments{},
130
		&cfg.Transform{},
hmoreau's avatar
hmoreau committed
131
132
133
		&transform.RoutineCounter{
			Functions: goroutines,
		},
hmoreau's avatar
hmoreau committed
134
		&transform.Format{},
135
	})
136

hmoreau's avatar
hmoreau committed
137
	templ, count := "", 0
hmoreau's avatar
hmoreau committed
138
	tmpChan, tmpName, channels := channel.Channel{}, "", []channel.Channel{}
hmoreau's avatar
hmoreau committed
139
140
141
142
143
	for i, elmt := range meta.GetVariables() {
		if strings.Contains(elmt, "main.array_") {
			if strings.Contains(elmt, "_state_") {
				if templ == "" {
					templ = elmt
hmoreau's avatar
hmoreau committed
144
					tmpName = string(templ[11])
hmoreau's avatar
hmoreau committed
145
146
147
148
					for _, str := range templ[12:] {
						if string(str) == "_" {
							break
						} else {
hmoreau's avatar
hmoreau committed
149
							tmpName += string(str)
hmoreau's avatar
hmoreau committed
150
151
152
153
154
155
156
157
158
159
160
						}
					}
					tmpChan.State = i
					count++
				} else {
					count++
				}
			} else if strings.Contains(elmt, "_value_0") {
				tmpChan.Value = i
				tmpChan.Length = count
			}
hmoreau's avatar
hmoreau committed
161
		} else if elmt == "main.isalive_"+tmpName+"_value" {
hmoreau's avatar
hmoreau committed
162
163
164
165
166
			channels = append(channels, tmpChan)
			templ, count = "", 0
		}
	}

167
	// Generate all the cases of the main switch case.
168
	cases := make([]ast.Stmt, len(meta.GetFunctions())+1)
169
170
171
172
173

	// The first case it the entry point of the program, where we initialize
	// the function counter to the index of the program's main function,
	// and set its caller counter to a non-existent index, thereby ending the
	// program once it finishes executing the main function.
174
175
176
177
178
179
180
181
182
183
184
	cases[0] = &ast.CaseClause{
		List: []ast.Expr{
			transform.Int(0),
		},
		Body: []ast.Stmt{
			meta.Set(meta.FunctionCounter(), transform.Int(meta.MainFunction().Index)),
			// When the main function completes, break from the switch by jumping to a
			// non-existent case.
			meta.Set(meta.MainFunction().Caller, transform.Int(len(meta.GetFunctions())+1)),
			&ast.ReturnStmt{
				Results: []ast.Expr{
185
					meta.State(),
186
187
188
189
				},
			},
		},
	}
190
191
192

	// All other cases are simply a matter of calling the right function with the
	// program state.
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
	for _, fr := range meta.GetFunctions() {
		cases[fr.Index] = &ast.CaseClause{
			List: []ast.Expr{
				transform.Int(fr.Index),
			},
			Body: []ast.Stmt{
				&ast.ReturnStmt{
					Results: []ast.Expr{
						&ast.CallExpr{
							Fun: fr.Ident,
							Args: []ast.Expr{
								meta.State(),
							},
						},
					},
				},
			},
		}
	}

213
	// Creates the main function's switch case.
214
215
216
217
218
219
220
221
	switchStmt := &ast.SwitchStmt{
		Init: nil,
		Tag:  meta.Get(meta.FunctionCounter()),
		Body: &ast.BlockStmt{
			List: cases,
		},
	}

Etienne Renault's avatar
Etienne Renault committed
222
223
	// Produce array of values for RERS
	var rers_values = []int{}
224
225
226
227
228
229
230
231
232
233
234
235
236
237
	var rers_position = 0
	var rers_active = 0

	if *rers != "" {
		rers_active = 1
		var unspacify = regexp.MustCompile(` *`)
		s := strings.Split(unspacify.ReplaceAllString(*rers, ""), ";")

		for _, i := range s {
			j, err := strconv.Atoi(i)
			if err != nil {
				panic(err)
			}
			rers_values = append(rers_values, j)
Etienne Renault's avatar
Etienne Renault committed
238
		}
239
240
241
242
243
		for i, e := range meta.GetVariables() {
			if strings.Contains(e, "__RERS__") {
				rers_position = i
				break
			}
Etienne Renault's avatar
Etienne Renault committed
244
245
246
		}
	}

247
248
249
	// We also need to add declarations for the state size, the type of the state
	// itself, the names of the different variables of our program, and finally
	// the entry function itself.
250
251
252
	transform.InjectDecls(
		res.(*ast.File),
		[]ast.Decl{
Etienne Renault's avatar
Etienne Renault committed
253
			// Do we want a support for RERS?
254
			decl.Int(token.CONST, "G2PRersActive", rers_active),
Etienne Renault's avatar
Etienne Renault committed
255
256
257
			decl.Int(token.CONST, "G2PRersPos", rers_position),
			decl.IntArray("G2PRersValues", rers_values),

258
259
260
261
262
263
264
265
266
			// size of state vector
			decl.Int(token.CONST, "G2PStateSize", meta.StateSize()),

			// type declaration for state vector
			decl.Type(
				meta.StateType(),
				&ast.ArrayType{
					Len: ast.NewIdent("G2PStateSize"),
					Elt: ast.NewIdent("int"),
267
				},
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
			),

			// array of strings containing variable names for all variables contained
			// in the state vector
			decl.Array(
				"G2PVariableNames",
				&ast.ArrayType{
					Len: &ast.BasicLit{
						Kind:  token.INT,
						Value: strconv.Itoa(meta.StateSize()),
					},
					Elt: &ast.StarExpr{
						X: &ast.SelectorExpr{
							X:   ast.NewIdent("C"),
							Sel: ast.NewIdent("char"),
						},
					},
				},
				variableNamesToC(meta.GetVariables()),
			),

289
			decl.GoroutineArray("G2PGoroutines", goroutines),
hmoreau's avatar
hmoreau committed
290
			decl.ChannelArray("G2PChannels", channels),
291

292
293
			// entrypoint to get a successor from a state vector
			decl.Function(
294
				"G2PMain",
295
296
297
298
299
300
301
302
				[]*ast.Field{ // parameters
					&ast.Field{
						Names: []*ast.Ident{meta.State()},
						Type:  meta.StateType(),
					},
				},
				[]*ast.Field{ // return values
					&ast.Field{
303
304
						//Type: transform.ArrayOf(meta.StateType()),
						Type: meta.StateType(),
305
306
307
308
309
310
					},
				},
				[]ast.Stmt{ // function body
					switchStmt,
					&ast.ReturnStmt{
						Results: []ast.Expr{
311
							meta.State(),
312
313
314
						},
					},
				},
315
316
317
			),
		},
	)
318
	astutil.AddImport(fset, res.(*ast.File), "C")
319
320
321
	return f.Name.Name, format.Node(file, fset, res)
}

322
// Copies files over and format them according to the template data.
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
func copyFile(src string, dst string, data interface{}) error {
	srcBytes, err := ioutil.ReadFile(src)
	if err != nil {
		return err
	}

	dstFile, err := os.Create(dst)
	if err != nil {
		return err
	}
	defer dstFile.Close()

	t, err := template.New("temp").Parse(string(srcBytes))
	if err != nil {
		return err
	}

	return t.Execute(dstFile, data)
}

343
func duplicateGoroutines(filepath string) (string, []*goroutine.Goroutine) {
344
345
346
347
348
349
350
351
	fset := token.NewFileSet()

	node, err := parser.ParseFile(fset, filepath, nil, 0)
	if err != nil {
		fmt.Fprintln(os.Stderr, err)
		os.Exit(1)
	}

hmoreau's avatar
hmoreau committed
352
	tmpFile, err := ioutil.TempFile("", "*_go2pins.go")
hmoreau's avatar
hmoreau committed
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
	if err != nil {
		panic("couldn't create go2pins temp file")
	}
	defer tmpFile.Close()

	srcFile, err := os.Open(filepath)
	if err != nil {
		panic("couldn't open given file")
	}
	defer srcFile.Close()

	_, err = io.Copy(tmpFile, srcFile)
	if err != nil {
		panic("couldn't copy file contents")
	}

	goroutines := make([]*goroutine.Goroutine, 0)
	gofuncs := make([]string, 0)
371
372
373
374
375
376
377
378
379
	ast.Inspect(node, func(n ast.Node) bool {
		gostmt, ok := n.(*ast.GoStmt)
		if !ok {
			return true
		}

		// get line of go call
		absPos := fset.PositionFor(gostmt.Pos(), false)

hmoreau's avatar
hmoreau committed
380
		chanToAdd := ""
381
382
383
384
		var fun *ast.Ident
		switch f := gostmt.Call.Fun.(type) {
		case *ast.Ident:
			fun = f
hmoreau's avatar
hmoreau committed
385
386
			switch decl := f.Obj.Decl.(type) {
			case *ast.FuncDecl:
387
				counter := 0
hmoreau's avatar
hmoreau committed
388
389
390
				for _, elmt := range decl.Type.Params.List {
					switch elmt.Type.(type) {
					case *ast.ChanType:
391
392
393
394
395
396
397
						for j, chanParamName := range elmt.Names {
							switch chanName := gostmt.Call.Args[counter+j].(type) {
							case *ast.Ident:
								chanToAdd += "_" + chanName.Name
							default:
								chanToAdd += "_" + chanParamName.Name
							}
hmoreau's avatar
hmoreau committed
398
399
						}
					}
400
					counter += len(elmt.Names)
hmoreau's avatar
hmoreau committed
401
402
				}
			}
403
404
405
406
407
408
409
410
411
412
413
		case *ast.SelectorExpr:
			fun = f.Sel
		default:
			panic("unsupported go call")
		}

		f, ok := fun.Obj.Decl.(*ast.FuncDecl)
		if !ok {
			panic("object should be a function")
		}

hmoreau's avatar
hmoreau committed
414
415
		fmt.Fprintln(tmpFile) // skip new line
		tmpName := f.Name
hmoreau's avatar
hmoreau committed
416
417
418
419
420
421
422
423
		if *ignorefunc != "" {
			for _, elmt := range toIgnore {
				if elmt == tmpName.Name {
					fmt.Println("WARNING: Blackbox can not be applied to goroutine call.")
					fmt.Println("\tFunc: " + elmt)
				}
			}
		}
hmoreau's avatar
hmoreau committed
424
		gofuncs = append(gofuncs, f.Name.Name)
hmoreau's avatar
hmoreau committed
425
		name := "_go_" + f.Name.Name + chanToAdd + "_" + strconv.Itoa(absPos.Line)
hmoreau's avatar
hmoreau committed
426
427
428
429
430
		f.Name = ast.NewIdent(name)
		format.Node(tmpFile, fset, f)
		f.Name = tmpName
		goroutines = append(goroutines, &goroutine.Goroutine{
			Name: name,
431
432
433
434
435
		})

		return true
	})

hmoreau's avatar
hmoreau committed
436
	input, err := ioutil.ReadFile(tmpFile.Name())
437
	if err != nil {
hmoreau's avatar
hmoreau committed
438
439
		fmt.Println(err)
		os.Exit(1)
440
	}
hmoreau's avatar
hmoreau committed
441
	newInput := string(input)
442

hmoreau's avatar
hmoreau committed
443
444
	for i, gf := range gofuncs {
		newInput = strings.Replace(newInput, "go "+gf+"(", "go "+goroutines[i].Name+"(", 1)
445
446
	}

hmoreau's avatar
hmoreau committed
447
	err = ioutil.WriteFile(tmpFile.Name(), []byte(newInput), 0666)
448
	if err != nil {
hmoreau's avatar
hmoreau committed
449
450
		fmt.Println(err)
		os.Exit(1)
451
452
	}

453
	return tmpFile.Name(), goroutines
454
455
}

456
457
458
459
460
type packageTemplate struct {
	PackagePath string
	PackageName string
}

hmoreau's avatar
hmoreau committed
461
462
var toIgnore []string

hmoreau's avatar
hmoreau committed
463
var (
Antoine Martin's avatar
Antoine Martin committed
464
465
466
	astprint       = flag.Bool("print-ast", false, "Print AST of <file>")
	callgraph      = flag.Bool("callgraph", false, "Display callgraph of <file>")
	forceOverwrite = flag.Bool("f", false, "overwrite output file if it exists")
Etienne Renault's avatar
Etienne Renault committed
467
	ignorefunc     = flag.String("ignore-fn", "", "Function will be considered as non-existent\n./go2pins -ignore-fn \"func1;func2;func3\" <file>")
Antoine Martin's avatar
Antoine Martin committed
468
469
	maxdepth       = flag.Int("maxdepth", 10, "fix the maximum depth of recursion for a recursive file")
	output         = flag.String("o", "output", "output `directory`")
Etienne Renault's avatar
Etienne Renault committed
470
	rers           = flag.String("rers", "", "support for RERS challenge: instruction \"__RERS += __RERS__ + 1\" will be\nreplaced to simulate environment, i.e. this instruction will produce as many\nsuccessors as values in parameters.\n./go2pins -rers \"val1;val2;val3\"")
hmoreau's avatar
hmoreau committed
471
)
Antoine Martin's avatar
Antoine Martin committed
472
473
474
475
476
477
478
479

func init() {
	flag.Usage = func() {
		fmt.Fprintln(os.Stderr, "Usage: "+os.Args[0]+" [options] <file>\n")
		flag.PrintDefaults()
	}
}

480
func main() {
Antoine Martin's avatar
Antoine Martin committed
481
482
483
	flag.Parse()
	if len(flag.Args()) != 1 {
		flag.Usage()
484
485
486
		os.Exit(1)
	}

hmoreau's avatar
hmoreau committed
487
488
489
	if *astprint {
		tools.PrintAst(flag.Args()[0])
	} else if *callgraph {
hmoreau's avatar
hmoreau committed
490
		tools.PrintCG(tools.CallGraph(flag.Args()[0]))
hmoreau's avatar
hmoreau committed
491
	} else {
hmoreau's avatar
hmoreau committed
492
493
		relPackagePath := flag.Args()[0]
		basePackagePath := path.Base(relPackagePath)
494

hmoreau's avatar
hmoreau committed
495
496
		// Check whether the output/ directory already exists.
		if _, err := os.Stat(*output); err == nil {
Antoine Martin's avatar
Antoine Martin committed
497
498
499
500
501
502
503
			if !*forceOverwrite {
				fmt.Fprintln(os.Stderr, *output+" already exists")
				os.Exit(1)
			}
			err = os.RemoveAll(*output)
			if err != nil {
				fmt.Fprintln(os.Stderr, "couldn't delete "+*output)
504
505
				os.Exit(1)
			}
hmoreau's avatar
hmoreau committed
506
		}
507

hmoreau's avatar
hmoreau committed
508
509
510
511
512
		// Create the output directory.
		if err := os.MkdirAll(*output, 0777); err != nil {
			fmt.Fprintln(os.Stderr, err.Error())
			os.Exit(1)
		}
513

hmoreau's avatar
hmoreau committed
514
515
516
517
518
519
520
		// Create a file in output/ with the same name as the input package.
		f, err := os.Create(path.Join(*output, basePackagePath))
		if err != nil {
			fmt.Fprintln(os.Stderr, err.Error())
			os.Exit(1)
		}
		defer f.Close()
521

522
		if *ignorefunc != "" {
523
524
525
			var unspacify = regexp.MustCompile(` *`)
			s := unspacify.ReplaceAllString(*ignorefunc, "")
			toIgnore = strings.Split(s, ";")
526
		}
hmoreau's avatar
hmoreau committed
527

528
		tmpFilePath, goroutines := duplicateGoroutines(relPackagePath)
529
530
		// FIXME: do we want this ?
		// defer os.Remove(tmpFilePath)
hmoreau's avatar
hmoreau committed
531
		flag.Args()[0] = tmpFilePath
532

533
		src, err := ioutil.ReadFile(tmpFilePath)
534
535
536
537
538
		if err != nil {
			fmt.Println(err)
			os.Exit(1)
		}

hmoreau's avatar
hmoreau committed
539
		// Compile and write the package to the output file.
540
		packageName, err := compileTo(basePackagePath, src, f, goroutines, rers)
hmoreau's avatar
hmoreau committed
541
542
543
544
		if err != nil {
			fmt.Fprintln(os.Stderr, err.Error())
			os.Exit(1)
		}
hmoreau's avatar
hmoreau committed
545

hmoreau's avatar
hmoreau committed
546
		tools.FormatArray(*output+"/"+basePackagePath, "var G2PVariableNames =")
547

hmoreau's avatar
hmoreau committed
548
549
550
551
552
553
554
		// Get project root directory to locate boilerplate/ dir
		_, currentPath, _, ok := runtime.Caller(0)
		if !ok {
			fmt.Fprintln(os.Stderr, "can't get path of current file")
			os.Exit(1)
		}
		go2pinsDir := path.Dir(currentPath)
Etienne Renault's avatar
Etienne Renault committed
555

hmoreau's avatar
hmoreau committed
556
557
558
559
560
561
562
563
564
565
566
567
		boilerplateFiles := []string{
			"Makefile",
			"go2pins.c",
			"go2pins.h",
			"main.go",
		}
		data := packageTemplate{basePackagePath, packageName}
		for _, filename := range boilerplateFiles {
			from := path.Join(go2pinsDir, "boilerplate/"+filename)
			to := path.Join(*output, filename)
			copyFile(from, to, data)
		}
568

hmoreau's avatar
hmoreau committed
569
570
571
572
573
		fmt.Println("Preprocessing done.\n\nTo display the state space of you program, follows the instructions below")
		fmt.Println("      cd", *output)
		fmt.Println("      make")
		fmt.Println("      <path_to_spot>/ltsmin/modelcheck -gm main.dve2C 'true'")
	}
574
}