checktype.go 3.12 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
package transform

import (
	"go/ast"
	"go/token"
Hugo Moreau's avatar
Hugo Moreau committed
24
	"strings"
25
26
27
)

/*
28
The TypeChecker triggers errors for uses of :
29
 - GoRoutines Declarations outside main function
30
 - Interface
31
 - Map
Hugo Moreau's avatar
Hugo Moreau committed
32
33
34
 - Non-integer variable
 - Panic
 - Pointer
35
 - Select
Hugo Moreau's avatar
Hugo Moreau committed
36
37
38
 - Slice
 - Struct
 - Switch
39
40
41
*/

type TypeChecker struct {
42
	currentFunction *ast.Object
43
	Blackbox        bool
44
45
46
47
48
49
50
51
52
53
54
}

// Pre traversal check if there is use of variable other than integers.
func (t *TypeChecker) Pre(meta *Meta, v *Visitor) bool {
	c := v.Cursor()
	switch node := c.Node().(type) {
	case *ast.AssignStmt:
		for i := 0; i < len(node.Rhs); i++ {
			switch rhn := node.Rhs[i].(type) {
			case *ast.BasicLit:
				if rhn.Kind != token.INT {
55
					panic("Non-integer values are not supported.")
56
				}
57
58
59
60
61
62
63
			case *ast.ArrayType:
				switch ident := rhn.Elt.(type) {
				case *ast.Ident:
					if ident.Name != "int" {
						panic("Not int arrays are not supported.")
					}
				}
64
			}
Hugo Moreau's avatar
Hugo Moreau committed
65
66
67
68
69
70
			switch lhn := node.Lhs[i].(type) {
			case *ast.Ident:
				if strings.Contains(lhn.Name, "G2P_tmp_") {
					panic("Variable name must not contain \"G2P_tmp_\"")
				}
			}
71
		}
72
73
	case *ast.FuncDecl:
		t.currentFunction = node.Name.Obj
74
75
76
77
78
79
80
	case *ast.FuncType:
		for _, elmt := range node.Params.List {
			switch elmt.Type.(type) {
			case *ast.ArrayType:
				panic("Int array as argument in functions are not supported.")
			}
		}
81
82
83
84
85
86
87
88
89
	case *ast.GoStmt:
		switch c.Parent().(type) {
		case *ast.BlockStmt:
			if t.currentFunction.Name != "main" {
				panic("GoRoutines are not supported outside of main declaration.")
			}
		default:
			panic("GoRoutines are not supported outside of main declaration.")
		}
90
91
	case *ast.Ident:
		if node.Name == "panic" {
92
			panic("Panics are not supported.")
93
		}
Hugo Moreau's avatar
Hugo Moreau committed
94
	case *ast.InterfaceType:
95
		panic("Interfaces are not supported.")
96
	case *ast.MapType:
97
		panic("Maps are not supported.")
Hugo Moreau's avatar
Hugo Moreau committed
98
	case *ast.SliceExpr:
99
		panic("Slices are not supported.")
Hugo Moreau's avatar
Hugo Moreau committed
100
	case *ast.StarExpr:
101
		panic("Pointers are not supported.")
102
	case *ast.StructType:
103
		panic("Structs are not supported.")
104
	case *ast.SwitchStmt:
105
		panic("Switch are not supported.")
106
107
108
109
110
111
112
113
114
	case *ast.ValueSpec:
		for i := 0; i < len(node.Values); i++ {
			switch value := node.Values[i].(type) {
			case *ast.BasicLit:
				if value.Kind != token.INT {
					panic("Non integer global values are not supported.")
				}
			}
		}
115
116
117
118
119
120
121
	}
	return true
}

func (TypeChecker) Post(meta *Meta, v *Visitor) bool {
	return true
}