main.go 19.7 KB
Newer Older
Etienne Renault's avatar
Etienne Renault committed
1
2
3
4
5
// Copyright (C) 2020 Laboratoire de Recherche et Developpement
// de l'EPITA (LRDE).
//
// This file is part of Go2Pins, a tool for Golang model-checking
//
Etienne Renault's avatar
Etienne Renault committed
6
// Go2Pins is free software; you can redistribute it and/or modify it
Etienne Renault's avatar
Etienne Renault committed
7
8
9
10
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
Etienne Renault's avatar
Etienne Renault committed
11
// Go2Pins is distributed in the hope that it will be useful, but WITHOUT
Etienne Renault's avatar
Etienne Renault committed
12
13
14
15
16
17
18
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

19
20
21
22
23
24
25
package main

import (
	"flag"
	"fmt"
	"go/ast"
	"go/format"
26
	"go/importer"
27
28
	"go/parser"
	"go/token"
29
	"go/types"
30
	"io"
31
32
	"io/ioutil"
	"os"
Etienne Renault's avatar
Etienne Renault committed
33
	"os/exec"
34
	"path"
35
	"regexp"
36
37
	"runtime"
	"strconv"
38
	"strings"
39
	"text/template"
40
	"time"
41

42
43
	"golang.org/x/tools/go/ast/astutil"

44
	"gitlab.lrde.epita.fr/spot/go2pins/cspinfo"
Antoine Martin's avatar
Antoine Martin committed
45
	"gitlab.lrde.epita.fr/spot/go2pins/decl"
hmoreau's avatar
hmoreau committed
46
	"gitlab.lrde.epita.fr/spot/go2pins/tools"
Antoine Martin's avatar
Antoine Martin committed
47
48
	"gitlab.lrde.epita.fr/spot/go2pins/transform"
	"gitlab.lrde.epita.fr/spot/go2pins/transform/cfg"
49
50
)

51
var go2pins_version = "0.1b (aka Brubeck-Take5)"
Etienne Renault's avatar
Etienne Renault committed
52

53
// Generate a list of cgo CStrings from the provided string slice.
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
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
}

73
// Compiles the input file `(path, src)` and writes it to `file`.
Hugo Moreau's avatar
Hugo Moreau committed
74
func compileTo(filepath string, src []byte, file *os.File,
Hugo Moreau's avatar
Hugo Moreau committed
75
	goroutines []*cspinfo.Goroutine, rers string, output string) (string, error, *transform.Meta) {
76
	fset := token.NewFileSet()
Hugo Moreau's avatar
Hugo Moreau committed
77
	f, err := parser.ParseFile(fset, filepath, src, 0)
78
79

	if err != nil {
Hugo Moreau's avatar
Hugo Moreau committed
80
		return "", err, nil
81
82
	}

83
	var config types.Config
84
	// FIXME: figure out if this is really needed
85
86
87
88
89
90
	config.Importer = importer.Default()
	info := &types.Info{
		Uses:       make(map[*ast.Ident]types.Object),
		Selections: make(map[*ast.SelectorExpr]*types.Selection),
	}

91
	// Ensure that our program type checks.
Hugo Moreau's avatar
Hugo Moreau committed
92
	_, err = config.Check(filepath, fset, []*ast.File{f}, info)
93

94
	// Apply all transformations.
95
	meta := transform.NewMeta(fset, info)
96

hmoreau's avatar
hmoreau committed
97
98
99
100
101
102
103
	for _, g := range goroutines {
		g.Status = meta.StateSize()
		meta.Create("Status", g.Name)
		g.LineCounter = meta.StateSize()
		meta.Create("LineCounter", g.Name)
	}

104
	localvariable := &transform.LocalVariableAssignments{Global: true}
105
	res := transform.ApplyAll(f, meta, []transform.Transform{
106
		// &transform.Debug{}, // only for debuging a special transformation
Etienne Renault's avatar
Etienne Renault committed
107
108
109
110
		&transform.Alive{},
		&transform.Channel{
			Goroutines: goroutines,
		},
Etienne Renault's avatar
Etienne Renault committed
111
		&transform.DesugarArray{},
112
		&transform.NormalizeDeclarations{},
113
		&transform.ElseFull{},
114
		&transform.ConditionnalCall{},
115
		&transform.ArithmeticCall{},
116
		&transform.InnerCall{},
117
		&transform.RegularizedAffect{},
118
		&transform.FunctionDefs{},
hmoreau's avatar
hmoreau committed
119
120
121
		&transform.RoutineAssignments{
			Functions: goroutines,
		},
Hugo Moreau's avatar
Hugo Moreau committed
122
		localvariable,
123
124
125
	})
	res = transform.ApplyAll(res, meta, []transform.Transform{
		&transform.LocalVariableAssignments{Global: false, GlobalToMain: localvariable.GlobalToMain},
Etienne Renault's avatar
Etienne Renault committed
126
		&transform.AfterChannel{},
127
		&cfg.Transform{},
hmoreau's avatar
hmoreau committed
128
129
130
		&transform.RoutineCounter{
			Functions: goroutines,
		},
131
		&transform.DoubleBrackets{},
hmoreau's avatar
hmoreau committed
132
		&transform.Format{},
133
	})
Hugo Moreau's avatar
Hugo Moreau committed
134
	globalObj = localvariable.GlobalBlackbox
Etienne Renault's avatar
Etienne Renault committed
135
	var channels = meta.GetChans()
hmoreau's avatar
hmoreau committed
136

137
	// Generate all the cases of the main switch case.
138
	cases := make([]ast.Stmt, len(meta.GetFunctions())+1)
139
140
141
142
143

	// 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.
144
145
146
147
148
149
150
151
152
153
154
	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{
155
					meta.State(),
156
157
158
159
				},
			},
		},
	}
160
161
162

	// All other cases are simply a matter of calling the right function with the
	// program state.
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
	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(),
							},
						},
					},
				},
			},
		}
	}

183
	// Creates the main function's switch case.
184
185
186
187
188
189
190
191
	switchStmt := &ast.SwitchStmt{
		Init: nil,
		Tag:  meta.Get(meta.FunctionCounter()),
		Body: &ast.BlockStmt{
			List: cases,
		},
	}

Etienne Renault's avatar
Etienne Renault committed
192
193
	// Produce array of values for RERS
	var rers_values = []int{}
194
195
196
	var rers_position = 0
	var rers_active = 0

Hugo Moreau's avatar
Hugo Moreau committed
197
	if rers != "" {
198
199
		rers_active = 1
		var unspacify = regexp.MustCompile(` *`)
Hugo Moreau's avatar
Hugo Moreau committed
200
		s := strings.Split(unspacify.ReplaceAllString(rers, ""), ";")
201
202
203
204
205
206
207

		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
208
		}
209
210
211
212
213
		for i, e := range meta.GetVariables() {
			if strings.Contains(e, "__RERS__") {
				rers_position = i
				break
			}
Etienne Renault's avatar
Etienne Renault committed
214
215
216
		}
	}

217
218
219
	// 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.
Hugo Moreau's avatar
Hugo Moreau committed
220
221
222
223
224
225
226
	structs, err := ioutil.ReadFile(path.Join(output, "structs/structs.go"))
	if err != nil {
		fmt.Println(err)
		os.Exit(1)
	}
	fset2 := token.NewFileSet()
	node, _ := parser.ParseFile(fset2, "", structs, 0)
227
	transform.InjectDecls(
Hugo Moreau's avatar
Hugo Moreau committed
228
		node,
229
		[]ast.Decl{
Etienne Renault's avatar
Etienne Renault committed
230
			// Do we want a support for RERS?
231
			decl.Int(token.CONST, "G2PRersActive", rers_active),
Etienne Renault's avatar
Etienne Renault committed
232
233
234
			decl.Int(token.CONST, "G2PRersPos", rers_position),
			decl.IntArray("G2PRersValues", rers_values),

235
236
237
238
239
			// size of state vector
			decl.Int(token.CONST, "G2PStateSize", meta.StateSize()),

			// type declaration for state vector
			decl.Type(
Hugo Moreau's avatar
Hugo Moreau committed
240
				meta.StructStateType(),
241
242
243
				&ast.ArrayType{
					Len: ast.NewIdent("G2PStateSize"),
					Elt: ast.NewIdent("int"),
244
				},
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
			),

			// 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()),
			),
Hugo Moreau's avatar
Hugo Moreau committed
265
266
267
		},
	)
	astutil.AddImport(fset2, node, "C")
268

Hugo Moreau's avatar
Hugo Moreau committed
269
270
271
	transform.InjectDecls(
		res.(*ast.File),
		[]ast.Decl{
272
			decl.GoroutineArray("G2PGoroutines", goroutines),
hmoreau's avatar
hmoreau committed
273
			decl.ChannelArray("G2PChannels", channels),
274
275
			// entrypoint to get a successor from a state vector
			decl.Function(
276
				"G2PMain",
277
278
279
280
281
282
283
284
				[]*ast.Field{ // parameters
					&ast.Field{
						Names: []*ast.Ident{meta.State()},
						Type:  meta.StateType(),
					},
				},
				[]*ast.Field{ // return values
					&ast.Field{
285
286
						//Type: transform.ArrayOf(meta.StateType()),
						Type: meta.StateType(),
287
288
289
290
291
292
					},
				},
				[]ast.Stmt{ // function body
					switchStmt,
					&ast.ReturnStmt{
						Results: []ast.Expr{
293
							meta.State(),
294
295
296
						},
					},
				},
297
298
299
			),
		},
	)
Hugo Moreau's avatar
Hugo Moreau committed
300
301
302
303
304
305
306
307
308
309
310
311
312
313

	structFile, err := os.OpenFile(path.Join(output, "structs/structs.go"), os.O_CREATE|os.O_WRONLY|os.O_TRUNC, 0644)
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(2)
	}
	defer structFile.Close()
	err = format.Node(structFile, fset2, node)
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(2)
	}

	astutil.AddImport(fset, res.(*ast.File), path.Join(output, "structs"))
314
	astutil.AddImport(fset, res.(*ast.File), "C")
Hugo Moreau's avatar
Hugo Moreau committed
315
	return f.Name.Name, format.Node(file, fset, res), meta
316
317
}

318
// Copies files over and format them according to the template data.
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
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)
}

339
func duplicateGoroutines(filepath string) (string, []*cspinfo.Goroutine) {
340
341
342
343
344
345
346
347
	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
348
	tmpFile, err := ioutil.TempFile("", "*_go2pins.go")
hmoreau's avatar
hmoreau committed
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
	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")
	}

365
	goroutines := make([]*cspinfo.Goroutine, 0)
hmoreau's avatar
hmoreau committed
366
	gofuncs := make([]string, 0)
367
368
369
370
371
372
373
374
375
	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
376
		chanToAdd := ""
377
378
379
380
		var fun *ast.Ident
		switch f := gostmt.Call.Fun.(type) {
		case *ast.Ident:
			fun = f
hmoreau's avatar
hmoreau committed
381
382
			switch decl := f.Obj.Decl.(type) {
			case *ast.FuncDecl:
383
				counter := 0
hmoreau's avatar
hmoreau committed
384
385
386
				for _, elmt := range decl.Type.Params.List {
					switch elmt.Type.(type) {
					case *ast.ChanType:
387
388
389
390
391
392
393
						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
394
395
						}
					}
396
					counter += len(elmt.Names)
hmoreau's avatar
hmoreau committed
397
398
				}
			}
399
400
401
402
403
404
405
406
407
408
409
		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
410
411
		fmt.Fprintln(tmpFile) // skip new line
		tmpName := f.Name
hmoreau's avatar
hmoreau committed
412
413
414
415
416
417
418
419
		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
420
		gofuncs = append(gofuncs, f.Name.Name)
hmoreau's avatar
hmoreau committed
421
		name := "_go_" + f.Name.Name + chanToAdd + "_" + strconv.Itoa(absPos.Line)
hmoreau's avatar
hmoreau committed
422
423
424
		f.Name = ast.NewIdent(name)
		format.Node(tmpFile, fset, f)
		f.Name = tmpName
425
		goroutines = append(goroutines, &cspinfo.Goroutine{
hmoreau's avatar
hmoreau committed
426
			Name: name,
427
428
429
430
431
		})

		return true
	})

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

hmoreau's avatar
hmoreau committed
439
440
	for i, gf := range gofuncs {
		newInput = strings.Replace(newInput, "go "+gf+"(", "go "+goroutines[i].Name+"(", 1)
441
442
	}

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

449
	return tmpFile.Name(), goroutines
450
451
}

452
func treatGlobal(src []byte) ([]byte, bool) {
Hugo Moreau's avatar
Hugo Moreau committed
453
454
455
456
457
458
459
	info := &types.Info{
		Uses:       make(map[*ast.Ident]types.Object),
		Selections: make(map[*ast.SelectorExpr]*types.Selection),
	}

	fset := token.NewFileSet()
	node, err := parser.ParseFile(fset, "", src, 0)
Hugo Moreau's avatar
Hugo Moreau committed
460
461
462
463
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(1)
	}
Hugo Moreau's avatar
Hugo Moreau committed
464
	meta := transform.NewMeta(fset, info)
465
466
	preglobal := &transform.PreGlobal{}
	transform.Apply(node, meta, preglobal)
Hugo Moreau's avatar
Hugo Moreau committed
467
	globalVar = preglobal.GlobalVar
468
469
470
471
	if len(preglobal.GlobalVar) == 0 {
		return src, false
	}

Hugo Moreau's avatar
Hugo Moreau committed
472
473
474
	global := &transform.Global{GlobalVar: preglobal.GlobalVar, ToIgnore: toIgnore}
	res := transform.Apply(node, meta, global)
	res = transform.Apply(node, meta, &transform.PostGlobal{GlobalBlackbox: global.GlobalBlackbox})
Hugo Moreau's avatar
Hugo Moreau committed
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
	tmpFile, err := ioutil.TempFile("", "*_go2pins.go")
	if err != nil {
		panic("couldn't create go2pins temp file")
	}
	defer tmpFile.Close()
	err = format.Node(tmpFile, fset, res)
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(2)
	}
	src, err = ioutil.ReadFile(tmpFile.Name())
	if err != nil {
		fmt.Println(err)
		os.Exit(1)
	}
490
491
492
493
494
495
	for _, val := range toIgnore {
		if global.GlobalBlackbox[val] {
			return src, true
		}
	}
	return src, false
Hugo Moreau's avatar
Hugo Moreau committed
496
497
}

Hugo Moreau's avatar
Hugo Moreau committed
498
499
500
501
502
503
504
505
506
507
508
509
func insertGlobalInBlackbox(meta *transform.Meta, filename string) {
	src, err := ioutil.ReadFile(filename)
	if err != nil {
		fmt.Println(err)
		os.Exit(1)
	}
	fset := token.NewFileSet()
	node, err := parser.ParseFile(fset, "", src, 0)
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(1)
	}
Hugo Moreau's avatar
Hugo Moreau committed
510
511
512
513
	transform.ApplyAll(node, meta, []transform.Transform{
		&transform.GlobalToState{GlobalVar: globalVar, GlobalBlackbox: globalObj},
		&transform.DoubleBrackets{},
	})
Hugo Moreau's avatar
Hugo Moreau committed
514
515
516
517
518
519
520
521
522
523
524
525
526
	file, err := os.OpenFile(filename, os.O_CREATE|os.O_WRONLY|os.O_TRUNC, 0644)
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(2)
	}
	defer file.Close()
	err = format.Node(file, fset, node)
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(2)
	}
}

527
528
529
type packageTemplate struct {
	PackagePath string
	PackageName string
530
	Output      string
531
532
}

hmoreau's avatar
hmoreau committed
533
var toIgnore []string
Hugo Moreau's avatar
Hugo Moreau committed
534
535
var globalObj map[string]*ast.Object
var globalVar []string
hmoreau's avatar
hmoreau committed
536

hmoreau's avatar
hmoreau committed
537
var (
Antoine Martin's avatar
Antoine Martin committed
538
539
540
	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")
541
	ignorefunc     = flag.String("blackbox-fn", "", "Function will be considered as non-existent\n./go2pins -blackbox-fn \"func1;func2;func3\" <file>")
542
	formulae       = flag.String("formulae", "", "Formulae file")
Antoine Martin's avatar
Antoine Martin committed
543
544
	maxdepth       = flag.Int("maxdepth", 10, "fix the maximum depth of recursion for a recursive file")
	output         = flag.String("o", "output", "output `directory`")
Hugo Moreau's avatar
Hugo Moreau committed
545
	rers           = flag.Bool("rers", false, "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\"")
Etienne Renault's avatar
Etienne Renault committed
546
	version        = flag.Bool("version", false, "The current version of Go2Pins")
hmoreau's avatar
hmoreau committed
547
)
Antoine Martin's avatar
Antoine Martin committed
548
549
550

func init() {
	flag.Usage = func() {
551
		fmt.Fprintln(os.Stderr, "Usage: "+os.Args[0]+" [options] <file> [formula]\n")
Antoine Martin's avatar
Antoine Martin committed
552
553
554
555
		flag.PrintDefaults()
	}
}

556
func main() {
Antoine Martin's avatar
Antoine Martin committed
557
	flag.Parse()
558
	start := time.Now()
Etienne Renault's avatar
Etienne Renault committed
559
560
561
562
563
564
565
566
567
568

	if *version { // Version preempt all
		fmt.Println("Go2Pins, version go2pins" + go2pins_version + "\n")
		fmt.Println("Copyright (C) 2020  Laboratoire de Recherche et Développement de l'Epita.")
		fmt.Println("License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>.")
		fmt.Println("This is free software: you are free to change and redistribute it.")
		fmt.Println("There is NO WARRANTY, to the extent permitted by law.")
		os.Exit(0)
	}

569
	if len(flag.Args()) < 1 {
Antoine Martin's avatar
Antoine Martin committed
570
		flag.Usage()
571
572
573
		os.Exit(1)
	}

hmoreau's avatar
hmoreau committed
574
575
	if *astprint {
		tools.PrintAst(flag.Args()[0])
576
577
578
	}

	if *callgraph {
579
580
		src, _ := ioutil.ReadFile(flag.Args()[0])
		tools.Callgraph(string(src))
581
	}
582

Hugo Moreau's avatar
Hugo Moreau committed
583
584
585
586
587
	rersinput := ""
	if *rers {
		rersinput = tools.RersInput(flag.Args()[0])
	}

588
589
590
591
	relPackagePath := flag.Args()[0]
	basePackagePath := path.Base(relPackagePath)

	// Check whether the output/ directory already exists.
592
	*output = path.Clean(*output)
593
594
595
	if _, err := os.Stat(*output); err == nil {
		if !*forceOverwrite {
			fmt.Fprintln(os.Stderr, *output+" already exists")
hmoreau's avatar
hmoreau committed
596
597
			os.Exit(1)
		}
598
		err = os.RemoveAll(*output)
hmoreau's avatar
hmoreau committed
599
		if err != nil {
600
			fmt.Fprintln(os.Stderr, "couldn't delete "+*output)
hmoreau's avatar
hmoreau committed
601
602
			os.Exit(1)
		}
603
	}
604

605
606
607
608
609
	// Create the output directory.
	if err := os.MkdirAll(*output, 0777); err != nil {
		fmt.Fprintln(os.Stderr, err.Error())
		os.Exit(1)
	}
Hugo Moreau's avatar
Hugo Moreau committed
610
611
612
613
614
615
616
617
618
619
620
621
622
623
	// Create the structs package
	if err := os.MkdirAll(path.Join(*output, "structs"), 0777); err != nil {
		fmt.Fprintln(os.Stderr, err.Error())
		os.Exit(1)
	}
	// 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)
	copyFile(path.Join(go2pinsDir, "boilerplate/structs/structs.go"), path.Join(*output, "structs/structs.go"), nil)
hmoreau's avatar
hmoreau committed
624

625
626
627
628
629
630
631
	// 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()
632

633
634
635
636
	if *formulae != "" {
		*ignorefunc = tools.Formulae(flag.Args()[0], *formulae)
	}

637
	if *ignorefunc != "" {
638
		if *formulae == "" && len(flag.Args()) >= 2 && *ignorefunc == "auto" {
639

640
641
			*ignorefunc = tools.Formuala(flag.Args()[0], flag.Args()[1])
		}
642
643
644
		var unspacify = regexp.MustCompile(` *`)
		s := unspacify.ReplaceAllString(*ignorefunc, "")
		toIgnore = strings.Split(s, ";")
Etienne Renault's avatar
Etienne Renault committed
645
		fmt.Println("Will ignore :", len(toIgnore), "functions", toIgnore)
646
	}
647

648
649
650
651
	tmpFilePath, goroutines := duplicateGoroutines(relPackagePath)
	// FIXME: do we want this ?
	// defer os.Remove(tmpFilePath)
	flag.Args()[0] = tmpFilePath
hmoreau's avatar
hmoreau committed
652

653
654
655
656
657
	src, err := ioutil.ReadFile(tmpFilePath)
	if err != nil {
		fmt.Println(err)
		os.Exit(1)
	}
658

659
660
661
662
663
664
665
666
667
668
	// Check if all constraints are respected
	info := &types.Info{
		Uses:       make(map[*ast.Ident]types.Object),
		Selections: make(map[*ast.SelectorExpr]*types.Selection),
	}
	fset := token.NewFileSet()
	node, err := parser.ParseFile(fset, "", src, 0)
	meta := transform.NewMeta(fset, info)
	transform.Apply(node, meta, &transform.TypeChecker{Blackbox: (*ignorefunc != "")})

Hugo Moreau's avatar
Hugo Moreau committed
669
	var global bool = false
670
	if len(toIgnore) != 0 {
Hugo Moreau's avatar
Hugo Moreau committed
671
		src, global = treatGlobal(src)
672
		a, bb := tools.RewriteBlackbox(string(src), toIgnore, *output)
673
674
675
676
677
678
679
680
681
682
683
684

		if err = os.MkdirAll(*output+"/blackbox", 0777); err != nil {
			fmt.Fprintln(os.Stderr, err.Error())
			os.Exit(1)
		}
		err = ioutil.WriteFile(*output+"/blackbox/blackbox.go", []byte(bb), 0666)

		if err != nil {
			fmt.Println(err)
			os.Exit(1)
		}
		src = []byte(a)
Hugo Moreau's avatar
Hugo Moreau committed
685
686
687
688
689
		err = ioutil.WriteFile(path.Join(*output, basePackagePath), []byte(src), 0666)
		if err != nil {
			fmt.Println(err)
			os.Exit(1)
		}
690
	}
691
692
693
694
695
696
697
698

	// Unroll recursion if needed
	tmp, ok := tools.RewriteRecursion(string(src), *maxdepth)
	src = []byte(tmp)
	if ok {
		fmt.Println("RECURSION DETECTED: unroll recursive functions up to depth", *maxdepth)
	}

699
	// Compile and write the package to the output file.
Hugo Moreau's avatar
Hugo Moreau committed
700
	packageName, err, meta := compileTo(basePackagePath, src, f, goroutines, rersinput, *output)
701
702
703
704
	if err != nil {
		fmt.Fprintln(os.Stderr, err.Error())
		os.Exit(1)
	}
Hugo Moreau's avatar
Hugo Moreau committed
705
706
707
	if global {
		insertGlobalInBlackbox(meta, path.Join(*output, "blackbox/blackbox.go"))
	}
Etienne Renault's avatar
Etienne Renault committed
708

Hugo Moreau's avatar
Hugo Moreau committed
709
	tools.FormatArray(path.Join(*output, "structs/structs.go"), "var G2PVariableNames =")
Etienne Renault's avatar
Etienne Renault committed
710

711
712
713
714
715
716
	boilerplateFiles := []string{
		"Makefile",
		"go2pins.c",
		"go2pins.h",
		"main.go",
	}
717
	data := packageTemplate{basePackagePath, packageName, *output}
718
719
720
721
	for _, filename := range boilerplateFiles {
		from := path.Join(go2pinsDir, "boilerplate/"+filename)
		to := path.Join(*output, filename)
		copyFile(from, to, data)
hmoreau's avatar
hmoreau committed
722
	}
723

724
725
726
727
728
	transpile_time := time.Since(start)
	start = time.Now()

	fmt.Println("transpilation time: ", transpile_time.Milliseconds(), "ms")

Etienne Renault's avatar
Etienne Renault committed
729
730
731
	// Ease users life, do not force them to make by themself
	cmd := exec.Command("make", "-C", *output)
	_, err = cmd.Output()
732
733
734
735

	compilation_time := time.Since(start)
	fmt.Println("compilation time: ", compilation_time.Milliseconds(), "ms")

Etienne Renault's avatar
Etienne Renault committed
736
737
	if err != nil {
		fmt.Println(err.Error())
738
		os.Exit(2)
Etienne Renault's avatar
Etienne Renault committed
739
	}
740
741
742
743
744
745
746
747
748
749
750
751
752
753
	if len(flag.Args()) > 1 {
		formulaCmd := exec.Cmd{
			Path:   "./" + *output + "/go2pins-mc",
			Args:   []string{"./" + *output + "/go2pins-mc", "-ltl", flag.Args()[1]},
			Stdout: os.Stdout,
			Stderr: os.Stdout,
		}
		formulaCmd.Start()
		formulaCmd.Wait()
	} else {
		fmt.Println("Preprocessing done.\n")
		fmt.Println("Display all available options (including LTL verification) by running:")
		fmt.Println("      ./" + *output + "/go2pins-mc -help\n")
	}
754
}