main.go

// Copyright (C) 2020 Laboratoire de Recherche et Developpement
// de l'EPITA (LRDE).
//
// This file is part of Go2Pins, a tool for Golang model-checking
//
// Go2Pins is free software; you can redistribute it and/or modify it
// 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.
//
// Go2Pins is distributed in the hope that it will be useful, but WITHOUT
// 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/>.

package main

import (
	"flag"
	"fmt"
	"go/ast"
	"go/format"
	"go/importer"
	"go/parser"
	"go/token"
	"go/types"
	"io"
	"io/ioutil"
	"os"
	"os/exec"
	"path"
	"regexp"
	"runtime"
	"strconv"
	"strings"
	"text/template"
	"time"

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

	"gitlab.lrde.epita.fr/spot/go2pins/cspinfo"
	"gitlab.lrde.epita.fr/spot/go2pins/decl"
	"gitlab.lrde.epita.fr/spot/go2pins/tools"
	"gitlab.lrde.epita.fr/spot/go2pins/transform"
	"gitlab.lrde.epita.fr/spot/go2pins/transform/cfg"
)

var go2pins_version = "0.1b (aka Brubeck-Take5)"

// Generate a list of cgo CStrings from the provided string slice.
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
}

// Compiles the input file `(path, src)` and writes it to `file`.
func compileTo(filepath string, src []byte, file *os.File,
	goroutines []*cspinfo.Goroutine, rers string, output string) (string, error, *transform.Meta) {
	fset := token.NewFileSet()
	f, err := parser.ParseFile(fset, filepath, src, 0)

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

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

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

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

	for _, g := range goroutines {
		g.Status = meta.StateSize()
		meta.Create("Status", g.Name)
		g.LineCounter = meta.StateSize()
		meta.Create("LineCounter", g.Name)
	}

	localvariable := &transform.LocalVariableAssignments{Global: true}
	res := transform.ApplyAll(f, meta, []transform.Transform{
		// &transform.Debug{}, // only for debuging a special transformation
		&transform.Alive{},
		&transform.Channel{
			Goroutines: goroutines,
		},
		&transform.DesugarArray{},
		&transform.NormalizeDeclarations{},
		&transform.ElseFull{},
		&transform.ConditionnalCall{},
		&transform.ArithmeticCall{},
		&transform.InnerCall{},
		&transform.RegularizedAffect{},
		&transform.FunctionDefs{},
		&transform.RoutineAssignments{
			Functions: goroutines,
		},
		localvariable,
	})
	res = transform.ApplyAll(res, meta, []transform.Transform{
		&transform.LocalVariableAssignments{Global: false, GlobalToMain: localvariable.GlobalToMain},
		&transform.AfterChannel{},
		&cfg.Transform{},
		&transform.RoutineCounter{
			Functions: goroutines,
		},
		&transform.DoubleBrackets{},
		&transform.Format{},
	})
	globalObj = localvariable.GlobalBlackbox
	var channels = meta.GetChans()

	// Generate all the cases of the main switch case.
	cases := make([]ast.Stmt, len(meta.GetFunctions())+1)

	// 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.
	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{
					meta.State(),
				},
			},
		},
	}

	// All other cases are simply a matter of calling the right function with the
	// program state.
	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(),
							},
						},
					},
				},
			},
		}
	}

	// Creates the main function's switch case.
	switchStmt := &ast.SwitchStmt{
		Init: nil,
		Tag:  meta.Get(meta.FunctionCounter()),
		Body: &ast.BlockStmt{
			List: cases,
		},
	}

	// Produce array of values for RERS
	var rers_values = []int{}
	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)
		}
		for i, e := range meta.GetVariables() {
			if strings.Contains(e, "__RERS__") {
				rers_position = i
				break
			}
		}
	}

	// 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.
	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)
	transform.InjectDecls(
		node,
		[]ast.Decl{
			// Do we want a support for RERS?
			decl.Int(token.CONST, "G2PRersActive", rers_active),
			decl.Int(token.CONST, "G2PRersPos", rers_position),
			decl.IntArray("G2PRersValues", rers_values),

			// size of state vector
			decl.Int(token.CONST, "G2PStateSize", meta.StateSize()),

			// type declaration for state vector
			decl.Type(
				meta.StructStateType(),
				&ast.ArrayType{
					Len: ast.NewIdent("G2PStateSize"),
					Elt: ast.NewIdent("int"),
				},
			),

			// 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()),
			),
		},
	)
	astutil.AddImport(fset2, node, "C")

	transform.InjectDecls(
		res.(*ast.File),
		[]ast.Decl{
			decl.GoroutineArray("G2PGoroutines", goroutines),
			decl.ChannelArray("G2PChannels", channels),
			// entrypoint to get a successor from a state vector
			decl.Function(
				"G2PMain",
				[]*ast.Field{ // parameters
					&ast.Field{
						Names: []*ast.Ident{meta.State()},
						Type:  meta.StateType(),
					},
				},
				[]*ast.Field{ // return values
					&ast.Field{
						//Type: transform.ArrayOf(meta.StateType()),
						Type: meta.StateType(),
					},
				},
				[]ast.Stmt{ // function body
					switchStmt,
					&ast.ReturnStmt{
						Results: []ast.Expr{
							meta.State(),
						},
					},
				},
			),
		},
	)

	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"))
	astutil.AddImport(fset, res.(*ast.File), "C")
	return f.Name.Name, format.Node(file, fset, res), meta
}

// Copies files over and format them according to the template data.
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)
}

func duplicateGoroutines(filepath string) (string, []*cspinfo.Goroutine) {
	fset := token.NewFileSet()

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

	tmpFile, err := ioutil.TempFile("", "*_go2pins.go")
	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([]*cspinfo.Goroutine, 0)
	gofuncs := make([]string, 0)
	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)

		chanToAdd := ""
		var fun *ast.Ident
		switch f := gostmt.Call.Fun.(type) {
		case *ast.Ident:
			fun = f
			switch decl := f.Obj.Decl.(type) {
			case *ast.FuncDecl:
				counter := 0
				for _, elmt := range decl.Type.Params.List {
					switch elmt.Type.(type) {
					case *ast.ChanType:
						for j, chanParamName := range elmt.Names {
							switch chanName := gostmt.Call.Args[counter+j].(type) {
							case *ast.Ident:
								chanToAdd += "_" + chanName.Name
							default:
								chanToAdd += "_" + chanParamName.Name
							}
						}
					}
					counter += len(elmt.Names)
				}
			}
		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")
		}

		fmt.Fprintln(tmpFile) // skip new line
		tmpName := f.Name
		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)
				}
			}
		}
		gofuncs = append(gofuncs, f.Name.Name)
		name := "_go_" + f.Name.Name + chanToAdd + "_" + strconv.Itoa(absPos.Line)
		f.Name = ast.NewIdent(name)
		format.Node(tmpFile, fset, f)
		f.Name = tmpName
		goroutines = append(goroutines, &cspinfo.Goroutine{
			Name: name,
		})

		return true
	})

	input, err := ioutil.ReadFile(tmpFile.Name())
	if err != nil {
		fmt.Println(err)
		os.Exit(1)
	}
	newInput := string(input)

	for i, gf := range gofuncs {
		newInput = strings.Replace(newInput, "go "+gf+"(", "go "+goroutines[i].Name+"(", 1)
	}

	err = ioutil.WriteFile(tmpFile.Name(), []byte(newInput), 0666)
	if err != nil {
		fmt.Println(err)
		os.Exit(1)
	}

	return tmpFile.Name(), goroutines
}

func treatGlobal(src []byte) ([]byte, bool) {
	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)
	if err != nil {
		fmt.Println(os.Stderr, err.Error())
		os.Exit(1)
	}
	meta := transform.NewMeta(fset, info)
	preglobal := &transform.PreGlobal{}
	transform.Apply(node, meta, preglobal)
	globalVar = preglobal.GlobalVar
	if len(preglobal.GlobalVar) == 0 {
		return src, false
	}

	global := &transform.Global{GlobalVar: preglobal.GlobalVar, ToIgnore: toIgnore}
	res := transform.Apply(node, meta, global)
	res = transform.Apply(node, meta, &transform.PostGlobal{GlobalBlackbox: global.GlobalBlackbox})
	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)
	}
	for _, val := range toIgnore {
		if global.GlobalBlackbox[val] {
			return src, true
		}
	}
	return src, false
}

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)
	}
	transform.ApplyAll(node, meta, []transform.Transform{
		&transform.GlobalToState{GlobalVar: globalVar, GlobalBlackbox: globalObj},
		&transform.DoubleBrackets{},
	})
	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)
	}
}

type packageTemplate struct {
	PackagePath string
	PackageName string
	Output      string
}

var toIgnore []string
var globalObj map[string]*ast.Object
var globalVar []string

var (
	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")
	ignorefunc     = flag.String("blackbox-fn", "", "Function will be considered as non-existent\n./go2pins -blackbox-fn \"func1;func2;func3\" <file>")
	formulae       = flag.String("formulae", "", "Formulae file")
	maxdepth       = flag.Int("maxdepth", 10, "fix the maximum depth of recursion for a recursive file")
	output         = flag.String("o", "output", "output `directory`")
	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\"")
	version        = flag.Bool("version", false, "The current version of Go2Pins")
)

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

func main() {
	flag.Parse()
	start := time.Now()

	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)
	}

	if len(flag.Args()) < 1 {
		flag.Usage()
		os.Exit(1)
	}

	if *astprint {
		tools.PrintAst(flag.Args()[0])
	}

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

	rersinput := ""
	if *rers {
		rersinput = tools.RersInput(flag.Args()[0])
	}

	relPackagePath := flag.Args()[0]
	basePackagePath := path.Base(relPackagePath)

	// Check whether the output/ directory already exists.
	*output = path.Clean(*output)
	if _, err := os.Stat(*output); err == nil {
		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)
			os.Exit(1)
		}
	}

	// Create the output directory.
	if err := os.MkdirAll(*output, 0777); err != nil {
		fmt.Fprintln(os.Stderr, err.Error())
		os.Exit(1)
	}
	// 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)

	// 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()

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

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

			*ignorefunc = tools.Formuala(flag.Args()[0], flag.Args()[1])
		}
		var unspacify = regexp.MustCompile(` *`)
		s := unspacify.ReplaceAllString(*ignorefunc, "")
		toIgnore = strings.Split(s, ";")
		fmt.Println("Will ignore :", len(toIgnore), "functions", toIgnore)
	}

	tmpFilePath, goroutines := duplicateGoroutines(relPackagePath)
	// FIXME: do we want this ?
	// defer os.Remove(tmpFilePath)
	flag.Args()[0] = tmpFilePath

	src, err := ioutil.ReadFile(tmpFilePath)
	if err != nil {
		fmt.Println(err)
		os.Exit(1)
	}

	// 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 != "")})

	var global bool = false
	if len(toIgnore) != 0 {
		src, global = treatGlobal(src)
		a, bb := tools.RewriteBlackbox(string(src), toIgnore, *output)

		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)
		err = ioutil.WriteFile(path.Join(*output, basePackagePath), []byte(src), 0666)
		if err != nil {
			fmt.Println(err)
			os.Exit(1)
		}
	}

	// 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)
	}

	// Compile and write the package to the output file.
	packageName, err, meta := compileTo(basePackagePath, src, f, goroutines, rersinput, *output)
	if err != nil {
		fmt.Fprintln(os.Stderr, err.Error())
		os.Exit(1)
	}
	if global {
		insertGlobalInBlackbox(meta, path.Join(*output, "blackbox/blackbox.go"))
	}

	tools.FormatArray(path.Join(*output, "structs/structs.go"), "var G2PVariableNames =")

	boilerplateFiles := []string{
		"Makefile",
		"go2pins.c",
		"go2pins.h",
		"main.go",
	}
	data := packageTemplate{basePackagePath, packageName, *output}
	for _, filename := range boilerplateFiles {
		from := path.Join(go2pinsDir, "boilerplate/"+filename)
		to := path.Join(*output, filename)
		copyFile(from, to, data)
	}

	transpile_time := time.Since(start)
	start = time.Now()

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

	// Ease users life, do not force them to make by themself
	cmd := exec.Command("make", "-C", *output)
	_, err = cmd.Output()

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

	if err != nil {
		fmt.Println(err.Error())
		os.Exit(2)
	}
	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")
	}
}