README.md 3.73 KB
Newer Older
Etienne Renault's avatar
Etienne Renault committed
1
# Go2Pins: Bridging the Gap between Model Checking and Software Verification
Alexandre Kirszenberg's avatar
Alexandre Kirszenberg committed
2

Etienne Renault's avatar
Etienne Renault committed
3
4
Go2Pins is a Golang-to-Golang transpiler. Its main objective is to
bring verification techniques into the Golang realm. 
Alexandre Kirszenberg's avatar
Alexandre Kirszenberg committed
5

6
## Usage
Alexandre Kirszenberg's avatar
Alexandre Kirszenberg committed
7

Etienne Renault's avatar
Etienne Renault committed
8
Go2Pins is itself a Go program. As such, you will need to have installed a
9
distribution of Go on your computer in order to build it.
Alexandre Kirszenberg's avatar
Alexandre Kirszenberg committed
10

Hugo Moreau's avatar
Hugo Moreau committed
11
The minimum recommended Go version is 1.12.
Alexandre Kirszenberg's avatar
Alexandre Kirszenberg committed
12

13
Once you have cloned the repository:
Alexandre Kirszenberg's avatar
Alexandre Kirszenberg committed
14

15
```
Antoine Martin's avatar
Antoine Martin committed
16
17
cd go2pins

Etienne Renault's avatar
Etienne Renault committed
18
19
20
# Build go2pins and run tests
make 
make check
21
22

# Then, you can feed your program to go2pins
Etienne Renault's avatar
Etienne Renault committed
23
24
./go2pins -o output tests/concurrent_fibonacci.go

25
# The output directory will contain all the files necessary to compile the
Etienne Renault's avatar
Etienne Renault committed
26
# shared library respecting the PINS interface
27
28
29
cd output
make

Etienne Renault's avatar
Etienne Renault committed
30
31
32
# Then, you can  generate the state tree of your program.
# Note that this is only aivalable if you have Spot's modelcheck
# utility in your PATH (in <spot>/tests/ltsmin/modelcheck)
Etienne Renault's avatar
Etienne Renault committed
33
34
35
./go2pins-mc -display

# You can also perform LTL model checking by running either 
Etienne Renault's avatar
Etienne Renault committed
36
./go2pins-mc  '<some_ltl_formula>' -backend spot
Etienne Renault's avatar
Etienne Renault committed
37
38

# or if you have LTSmin backend installed
Etienne Renault's avatar
Etienne Renault committed
39
./go2pins-mc  '<some_ltl_formula>' -backend ltsmin
Etienne Renault's avatar
Etienne Renault committed
40
41

# Note that the LTL syntax may differ according to the various backend.
Etienne Renault's avatar
Etienne Renault committed
42
43
44
45
46
47
48
49
50
51
52
# Spot requires escaping while ltsmin refuses uppercase atomic propositions
# and requires spaces
#   - Spot syntax:      '[] "main_fibonacci_n==1"'
#   - LTsmin syntax:    '[] main_fibonacci_n == 1' 

# The list of available commands is accessible through
./go2pins-mc -help
```

## Performances

53
You can run the benchmark associated to this tool by running
Etienne Renault's avatar
Etienne Renault committed
54
55
56
57
```
make benchmark
```

58
59
60
61
62
63
64
Nonetheless, even with 8 threads and 200Go of RAM this benchmakr
will take at least multiple day. Consequently You can run the benchmark
on small problems  by running
```
make demo
```

Etienne Renault's avatar
Etienne Renault committed
65
66
67
68
69
70
Note that some part of this benchmark requires a lot of memory and can
then fail on your machine. 

## LTLrec

A tool named `ltlrec` is provided when running `make`. This tool
71
implements the LTLrec sugaring useful for handling recursion. For now,
Etienne Renault's avatar
Etienne Renault committed
72
this tool is external so that it can easily be used by other tools.
73
We plan to integrate this tool directly to Go2Pins.
Etienne Renault's avatar
Etienne Renault committed
74
75
76
77
78
79

As a consequence, the equivalences must be specified by hand though
a JSON file. For instance:

```
./ltlrec 'F all("a") || all("b")' '{"a": ["a1", "a2"], "b": ["b1", "b2", "b3"]}'
80
```
Alexandre Kirszenberg's avatar
Alexandre Kirszenberg committed
81

Etienne Renault's avatar
Etienne Renault committed
82
83
84
85
86
87
88
will output
```
F ("a1" && "a2") || ("b1" && "b2" && "b3")
```

Our goal is to integrate this tool directly inside of the `output` directory.

89
90
91
## Limitations

* Only 32-bit integer value types are currently supported.
Etienne Renault's avatar
Etienne Renault committed
92
93
* 32-bit integer array are supported, but raw initialisation is
  not fully supported, especially for local arrays
Etienne Renault's avatar
Etienne Renault committed
94
* Complex for loop statements are not yet handled
Etienne Renault's avatar
Etienne Renault committed
95
96
97
98
99
100
101
102
* Function calls are authorized for goroutines, nonetheless they will
  be automatically considered as blackbox
* Unbounded channels are supported. But channels can only be declared
  as global variables

Ensuring that the input file respect all these limitation is very painful.
We try to reject it correctly, but, a lot of corner cases are not covered.
Please be indulgent, and bug report. 
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117


## Architecture of the project

* `main.go` is the entry point of the program. It takes care of argument
  parsing, file parsing and any kind of top-level transformation and templating
  logic.
* `src/decl/` is a utility library to quickly generate the AST representation of
  Go types and values.
* `src/transform/` contains the logic of all other transformations.
* `tests/` contains example programs that can be fed into go2pins.
* `tools/` contains utility tools to inspect the AST of Go programs. They should
  be built separately.
* `boilerplate/` contains all the boilerplate necessary to create a PINS shared
  library with cgo.
Etienne Renault's avatar
Etienne Renault committed
118
119
* `cspinfo` information about concurrency
* `benchs` the benchmark of the paper