go2pins issueshttps://gitlab.lre.epita.fr/spot/go2pins/-/issues2020-04-24T13:09:12+02:00https://gitlab.lre.epita.fr/spot/go2pins/-/issues/1Go2Pins2020-04-24T13:09:12+02:00Etienne RenaultGo2PinsThe goal of the internship is to write a translator from GO to the API in C (called PINS) developed by the ltsmin team. The PINS interface is already interfaced with Spot so the main challenge of the internship will be to proposed transl...The goal of the internship is to write a translator from GO to the API in C (called PINS) developed by the ltsmin team. The PINS interface is already interfaced with Spot so the main challenge of the internship will be to proposed translation from Go structures to C.
The following steps should help you to discover and setup the environment you will work with.
* [x] Let met know when you are registered, so that I can give you grants and setup the git repository for your internship
* [x] Download GO from https://golang.org
* [x] Take the Tour https://tour.golang.org/welcome/1
* [ ] While you are taking the tour, build the set of test. The most important is to write simple tests with only the "main" and the different control structures. Keep tests s simple as possible with only one concept per test. This will help us to detect errors and to ensure non-regressions.
* [ ] Have a look to go/ast to understand how you can extract all variable from your simple tests program
FYI there are few, but some, people that try to model check go program. You can have a look to this webpage:
https://nickng.github.io/projects/golang/
You can also have a look to http://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/ltsmin-dve.ipynb to have an idea of what we can do with Spot through the PINS interface. The input langage is DVE which is a formal langage.
----
[Updated 2 Feb. 2018]
* [x] You have to fix the subset of Go we will focus on, so that you can build a set of tests for your translater.
* [ ] Install Spot (optional)
* [x] Install divine2 following instruction in spot/tests/ltsmin/README.
* [x] You can now run` divine compile --ltsmin model.dve` this will produce 2 files: one *.cpp one *.dve2C. Have a look to the first one to understand how to convert a program from a model.
* [ ] You asked me more information about model checking. Your can have a look to my Ph.D. dissertation here `https://www.lrde.epita.fr/~renault/phd/data/renault.phd.pdf`. Chapter 1 and section 2 are probably the most relevant for understanding the global approach.
* [x] @vtourneur told us that you can have troubles compiling divine. I remember no such thing but you can (1) ask help to @vtourneur or use `https://gitlab.lrde.epita.fr/spot/divine-ltsmin-deb`2018-04-05https://gitlab.lre.epita.fr/spot/go2pins/-/issues/19Towards Go2Pins 0.22022-02-15T11:49:44+01:00Etienne RenaultTowards Go2Pins 0.2Here are the features that must be supported for next version:
- [ ] allow go-routines to support `go func () { ... }() `
- [ ] support homogeneously arrays. For instance `var someList []int = []int{-2, -5, -3, -1, 0} ` is supported as ...Here are the features that must be supported for next version:
- [ ] allow go-routines to support `go func () { ... }() `
- [ ] support homogeneously arrays. For instance `var someList []int = []int{-2, -5, -3, -1, 0} ` is supported as global variable but not as local variable
- [ ] support mutexes
- [ ] support objects
- [ ] support `len(..)` and `range(..)`
- [ ] support slices
- [ ] distribute binary (WIP merge request from @amartin )
- [ ] support alternative entry points than `main` (required to support gobench)
- [ ] handle (a large part of) gobench `https://github.com/timmyyuan/gobench`
- [ ] comparison with Gomela, BINGO, GoCatch, GoDetector
- [ ] ...
@hmoreau @amartin @akirszenberg contributions welcome ;)https://gitlab.lre.epita.fr/spot/go2pins/-/issues/18Double brackets `transform`: Handling complex nested brackets2022-05-12T12:07:50+02:00Hugo MoreauDouble brackets `transform`: Handling complex nested bracketsTaking this file [`transform/double_brackets.go`](https://gitlab.lrde.epita.fr/spot/go2pins/-/blob/master/transform/double_brackets.go), we can handle uses of array.
It will change `G2PState[4][2]` to `G2PState[4+2]`.
But taking this e...Taking this file [`transform/double_brackets.go`](https://gitlab.lrde.epita.fr/spot/go2pins/-/blob/master/transform/double_brackets.go), we can handle uses of array.
It will change `G2PState[4][2]` to `G2PState[4+2]`.
But taking this example:
```go
my_array[my_second_array[2]]
```
The transform does not handle it yet.https://gitlab.lre.epita.fr/spot/go2pins/-/issues/17LinkResults for other packages function2021-03-02T08:26:37+01:00Hugo MoreauLinkResults for other packages functionCalling an external functions with as parameters a function call defined in the current context won't link the proper result(s).
Short example:
```go
package main
import "fmt"
func foo() int {
return 42
}
func main() {
fmt.Pri...Calling an external functions with as parameters a function call defined in the current context won't link the proper result(s).
Short example:
```go
package main
import "fmt"
func foo() int {
return 42
}
func main() {
fmt.Println(foo())
}
```Hugo MoreauHugo Moreauhttps://gitlab.lre.epita.fr/spot/go2pins/-/issues/16Handling multiple assignments to function call2021-03-02T08:00:46+01:00Hugo MoreauHandling multiple assignments to function callWhen it comes to multiple assignments including one that contains a function call, **Go2Pins** fail to handle it well.
Exemple:
```go
package main
func foo() int {
return 42
}
func main() {
a, b := foo(), 2
a, b = 2, foo()
...When it comes to multiple assignments including one that contains a function call, **Go2Pins** fail to handle it well.
Exemple:
```go
package main
func foo() int {
return 42
}
func main() {
a, b := foo(), 2
a, b = 2, foo()
a, b = foo(), foo()
}
```
All of the cases in `main` function does not work. It will ignore everything except the function call.
Thus, an easy way to handle it would be to make one assignment for each function call:
```go
package main
func foo() int {
return 42
}
func main() {
a := foo()
b := 2
a = 2
b = foo()
a = foo()
b = foo()
}
```
We can take a closer look on `transform/cfg/transform.go` and `transform/cfg/linkresults.go` for a proper way to handle it,Hugo MoreauHugo Moreauhttps://gitlab.lre.epita.fr/spot/go2pins/-/issues/15LocalVariableAssignments transform: handling global variables decl before acc...2021-03-03T20:08:03+01:00Hugo MoreauLocalVariableAssignments transform: handling global variables decl before accessing itCurrently `LocalVariablesAssignments` transform does not work well when a **global variables** is declared after accessing it.
Exemple:
```go
package main
func main() {
a = 42
}
var a int
```
Since `meta` hasn't stored it yet in t...Currently `LocalVariablesAssignments` transform does not work well when a **global variables** is declared after accessing it.
Exemple:
```go
package main
func main() {
a = 42
}
var a int
```
Since `meta` hasn't stored it yet in the our vector, no transform will be applied on the `assignment` in the `main` function.
Resulting to something like this:
```go
package main
func G2P_main(G2PState structs.G2PStateType) {
G2PState[5] = 0 // global variable a
a = 42
}
```
Thus, it seems that the "simplest thing" to do is to make a transform before that will handle it.Hugo MoreauHugo Moreauhttps://gitlab.lre.epita.fr/spot/go2pins/-/issues/14Translation of BEEM benchmark2020-04-28T08:26:46+02:00Etienne RenaultTranslation of BEEM benchmarkThe BEEM benchmark is a popular benchmark for explicit model-checker.
It supports atomic transitions with multiples effects. Thus, an automatic
translation of these models is not trivial.
Indeed, we can opt for the following strateg...The BEEM benchmark is a popular benchmark for explicit model-checker.
It supports atomic transitions with multiples effects. Thus, an automatic
translation of these models is not trivial.
Indeed, we can opt for the following strategy:
- if this transition uses only local variables: no problem we can just
split that into multiple transitions
- otherwise build an extern fonction that regroup all the effect of this
transition (even thought it can be tricky with local variables) in a function
and consider this function as blackbox.
This strategy will fail since even if the model (including blackboxing) will
be correct, the go file will not be be. Indeed, the multiples effects of the
original BEEM model will now be considered as multiple ones which is really
problematic.
How can we solve that?https://gitlab.lre.epita.fr/spot/go2pins/-/issues/13Rewrite Goroutine's, Recursion's, (and Blackboxes's) transformations2020-04-24T17:56:53+02:00Etienne RenaultRewrite Goroutine's, Recursion's, (and Blackboxes's) transformationsThe aforementioned transformations differ from the other transformations
since they require a deep-copy. Since such method is not available in the
standard library we opted to write results in a new file.
Does the import of this packag...The aforementioned transformations differ from the other transformations
since they require a deep-copy. Since such method is not available in the
standard library we opted to write results in a new file.
Does the import of this package :
https://pkg.go.dev/github.com/go-toolsmith/astcopy
solve our problem?
@amartin @hmoreau what do you think?https://gitlab.lre.epita.fr/spot/go2pins/-/issues/12Invalid state space size2020-11-17T17:00:07+01:00Etienne RenaultInvalid state space size
The following code outputs a state-space of 8007 states and transitions.
```
package main
var c = 1
func compute() {
var tmp = 1
for c < 4000 {
c = c + tmp
}
}
func main() {
compute()
}
```
while this one on...
The following code outputs a state-space of 8007 states and transitions.
```
package main
var c = 1
func compute() {
var tmp = 1
for c < 4000 {
c = c + tmp
}
}
func main() {
compute()
}
```
while this one only outputs a state-space of 7 states and transitions.
```
package main
var c = 1
func compute() {
for c < 4000 {
c = c + 1
}
}
func main() {
compute()
}
```https://gitlab.lre.epita.fr/spot/go2pins/-/issues/11LTSmin does not support complex names2020-04-24T13:10:14+02:00Etienne RenaultLTSmin does not support complex namesApparently, the LTL parser of LTSmin is a quite sensitive and only do not support atomic proposition with "/" and "."Apparently, the LTL parser of LTSmin is a quite sensitive and only do not support atomic proposition with "/" and "."https://gitlab.lre.epita.fr/spot/go2pins/-/issues/10Limit to the number of variable names ?2020-01-15T13:55:18+01:00Etienne RenaultLimit to the number of variable names ?The number of variables supported seems to be limited by the current version
of our tool. The following code works perfectly well on file bench/2019-Problem17.go
(branch `er/pre-release)
```
...
},
var...The number of variables supported seems to be limited by the current version
of our tool. The following code works perfectly well on file bench/2019-Problem17.go
(branch `er/pre-release)
```
...
},
variableNamesToC(meta.GetVariables())[1:1350],
),
```
while modifying it to `1351` will produce the output directory but trying to compile this
directory will now produce
```
./main.go:28:20: undefined: G2PGoroutines
./main.go:34:24: undefined: G2PMain
./main.go:103:13: undefined: G2PVariableNames
./main.go:104:10: undefined: G2PVariableNames
./main.go:304:35: undefined: G2PVariableNames
```
i.e., the variables array etc. are not produced...https://gitlab.lre.epita.fr/spot/go2pins/-/issues/9DesugarArray: add support for slices2020-04-24T13:11:26+02:00Etienne RenaultDesugarArray: add support for slicesThe following code is not currently handled since it relies on slices
```
var a251096036 []int = []int{35, 36, 37, 38, 39, 40}
var a1577123560 []int = a251096036
```The following code is not currently handled since it relies on slices
```
var a251096036 []int = []int{35, 36, 37, 38, 39, 40}
var a1577123560 []int = a251096036
```https://gitlab.lre.epita.fr/spot/go2pins/-/issues/8Alive for variables in Loops2020-01-06T14:33:54+01:00Etienne RenaultAlive for variables in LoopsCurrently, variables declared in loops doesn't have
the `alive` associated variable. The following example
```
for i := f(...) ; i < n; i++ {
...
}
```
should be replaced by :
```
i := f(...)
for ; i < n; i++ {
...
}
```
Warni...Currently, variables declared in loops doesn't have
the `alive` associated variable. The following example
```
for i := f(...) ; i < n; i++ {
...
}
```
should be replaced by :
```
i := f(...)
for ; i < n; i++ {
...
}
```
Warning! Think to avoid name collision in this case!https://gitlab.lre.epita.fr/spot/go2pins/-/issues/7Boilerplate: fix linking on linux2019-09-23T14:08:43+02:00Hugo MoreauBoilerplate: fix linking on linux@amartin
As I began working on go2pins, I find out that there was some problem on my machine using `./ltsmin/modelcheck` on tests.
Sometimes, it just appears that it segfault. After a quick review with Etienne, we find out that you jus...@amartin
As I began working on go2pins, I find out that there was some problem on my machine using `./ltsmin/modelcheck` on tests.
Sometimes, it just appears that it segfault. After a quick review with Etienne, we find out that you just fixed it [here](https://gitlab.lrde.epita.fr/spot/go2pins/commit/750aca25058c101c16eb101e15fe3e37ab73725d).
Do you think you can merge your branch **fix-link**, or is there other things you have to see before merging it ?Hugo MoreauHugo Moreauhttps://gitlab.lre.epita.fr/spot/go2pins/-/issues/6AST transformations2020-04-24T13:09:48+02:00Etienne RenaultAST transformationsGolang has a lot of features that are not currently supported by the `go2pins` tool.
The goal of this internship is to handle more of these features.
The following steps will help you to setup your environnement:
- [x] install go co...Golang has a lot of features that are not currently supported by the `go2pins` tool.
The goal of this internship is to handle more of these features.
The following steps will help you to setup your environnement:
- [x] install go compiler `https://golang.org`
- [x] install `go2pins` (`https://gitlab.lrde.epita.fr/spot/go2pins`), create your own branch `hm/whatever` and build it
- [x] install `spot` (`https://gitlab.lrde.epita.fr/spot/spot`) and build it with these steps
```
autoreconf -vfi
./configure
make
make check
```
- [x] The directory `tests/ltsmin/` should now have a binary named `modelcheck`. Use it (as described in the readme of `go2pins`) to run the `only` test we have :(
Now that you have done that, you are ready to start your internship ! \o/
Next steps are then:
- [x] integrate the code in `tools/print_ast` into the project, i.e. I want an option such that `go2pins --print-ast` performs the same as the binary in `tools/print_ast`. This step will help you to discover the project and will be very useful for your AST processings.
- [x] write a pass that trigger errors for the use of variable other than `integer`. Have a look to `transform/normalizedeclarations.go` which is the simplest pass we have. Create tests for checking that and integrate it. **If you are familiar with Docker (or want to be) these tests will be ideally combined with spot and triggered every time a push is done**
- [x] Do the same for triggering errors when encontering: channels, panic, arrays (not supported for now, but easy to do maybe we handle that during your internship), struct, slices, pointers, interface, map, switch, and select. For each, use a dedicated pass and dedicated tests (I may missed something, but you
can test all constructs in `https://golang.org/ref/spec`). Use your `--print-ast` option to ease your comprehension.
- [x] Now, you should be able to understand very well the traversal and the structure of a go program. We can then focus to the support of recursion. First step is to build a callgraph. *Then come to me so I can explain to you how we can manage the support of recursion* :)https://gitlab.lre.epita.fr/spot/go2pins/-/issues/5Call to empty functions raise errors2020-01-06T15:28:55+01:00Etienne RenaultCall to empty functions raise errorsThe following code
```
package main
func f() {
v1 := 1
v1++
}
func main() {
f()
}
```
raise following errors:
```
panic: runtime error: index out of range
goroutine 1 [running]:
go/ast.(*AssignStmt).Pos(0xc000088ac0, 0...The following code
```
package main
func f() {
v1 := 1
v1++
}
func main() {
f()
}
```
raise following errors:
```
panic: runtime error: index out of range
goroutine 1 [running]:
go/ast.(*AssignStmt).Pos(0xc000088ac0, 0xc0000acd00)
/usr/local/go/src/go/ast/ast.go:723 +0x56
go/printer.(*printer).stmtList(0xc000107a00, 0xc000088bc0, 0x4, 0x4, 0x1, 0x1)
/usr/local/go/src/go/printer/nodes.go:1024 +0x1f7
go/printer.(*printer).block(0xc000107a00, 0xc00008da10, 0x1)
/usr/local/go/src/go/printer/nodes.go:1050 +0xf1
go/printer.(*printer).stmt(0xc000107a00, 0x1368e40, 0xc00008da10, 0x100)
/usr/local/go/src/go/printer/nodes.go:1255 +0x1dae
go/printer.(*printer).stmtList(0xc000107a00, 0xc00008dd10, 0x3, 0x3, 0x1, 0x1)
/usr/local/go/src/go/printer/nodes.go:1027 +0x17f
go/printer.(*printer).block(0xc000107a00, 0xc00008dd40, 0x1)
/usr/local/go/src/go/printer/nodes.go:1050 +0xf1
go/printer.(*printer).stmt(0xc000107a00, 0x1368e40, 0xc00008dd40, 0x100)
/usr/local/go/src/go/printer/nodes.go:1255 +0x1dae
go/printer.(*printer).stmt(0xc000107a00, 0x1369480, 0xc00010b220, 0x100)
/usr/local/go/src/go/printer/nodes.go:1195 +0x817
go/printer.(*printer).stmtList(0xc000107a00, 0xc000088c00, 0x4, 0x4, 0x1, 0x1)
/usr/local/go/src/go/printer/nodes.go:1027 +0x17f
go/printer.(*printer).block(0xc000107a00, 0xc00008df80, 0x1)
/usr/local/go/src/go/printer/nodes.go:1050 +0xf1
go/printer.(*printer).funcBody(0xc000107a00, 0x40000000, 0x4000000b, 0xc00008df80)
/usr/local/go/src/go/printer/nodes.go:1687 +0x47e
go/printer.(*printer).funcDecl(0xc000107a00, 0xc00008dfb0)
/usr/local/go/src/go/printer/nodes.go:1711 +0x189
go/printer.(*printer).decl(0xc000107a00, 0x1369180, 0xc00008dfb0)
/usr/local/go/src/go/printer/nodes.go:1721 +0x157
go/printer.(*printer).declList(0xc000107a00, 0xc0000ae2e0, 0x2, 0x2)
/usr/local/go/src/go/printer/nodes.go:1764 +0x165
go/printer.(*printer).file(0xc000107a00, 0xc0000c8080)
/usr/local/go/src/go/printer/nodes.go:1772 +0x131
go/printer.(*printer).printNode(0xc000107a00, 0x12b5b60, 0xc0000c8080, 0xc0000ac810, 0x0)
/usr/local/go/src/go/printer/printer.go:1152 +0x5f2
go/printer.(*Config).fprint(0x1531a50, 0x1363e80, 0xc000080008, 0xc0000882c0, 0x12b5b60, 0xc0000c8080, 0xc00010c030, 0x10be997, 0xc0000cc0c0)
/usr/local/go/src/go/printer/printer.go:1293 +0x172
go/printer.(*Config).Fprint(...)
/usr/local/go/src/go/printer/printer.go:1351
go/format.Node(0x1363e80, 0xc000080008, 0xc0000882c0, 0x12b5b60, 0xc0000c8080, 0x65, 0x0)
/usr/local/go/src/go/format/format.go:79 +0x114
main.compileTo(0x7ffeefbff943, 0xc, 0xc0000fa000, 0x40, 0x240, 0xc000080008, 0x0, 0xc00008e1a0, 0xd4000000012ed980, 0xc0000b9d01)
/Users/etienne/src/go2pins/main.go:182 +0x4d0
main.main()
/Users/etienne/src/go2pins/main.go:257 +0x332
```https://gitlab.lre.epita.fr/spot/go2pins/-/issues/4Handling go routines2020-04-24T13:09:31+02:00Etienne RenaultHandling go routinesThis issue aims to keep all the discussions about the internship in a single place.
The main objective is to handle goroutines `go func()`. (Note that later, the handling of channels could be a betterment) There are very few people dea...This issue aims to keep all the discussions about the internship in a single place.
The main objective is to handle goroutines `go func()`. (Note that later, the handling of channels could be a betterment) There are very few people dealing with Go for LTL model checking. To my knowledge only [these guys](https://nickng.io/projects/golang/) have done something like that. They have few papers you can read and an interesting video from `Golang UK conference 2016`.
I think that the very first steps are:
* [x] Download go2pins and make it work
* [x] Play with `https://golang.org/pkg/go/ast/` it will help you to understand the core of the project
* [x] Play with `https://tour.golang.org/concurrency/1` to have a nice comprehension of go routine
* [x] Read @akirszenberg reports
* [x] Have a pass that grab the number of `go` instruction inside of the given program.
I will add more achievement later :)Antoine Martinamartin@lrde.epita.frAntoine Martinamartin@lrde.epita.frhttps://gitlab.lre.epita.fr/spot/go2pins/-/issues/3gitlab-ci.yml2020-04-24T13:07:49+02:00Etienne Renaultgitlab-ci.ymlWe should have a simple gitlab-ci that will trigger all tests.We should have a simple gitlab-ci that will trigger all tests.https://gitlab.lre.epita.fr/spot/go2pins/-/issues/2Handling the function stack2020-04-24T13:08:36+02:00Alexandre KirszenbergHandling the function stackI'm currently implementing function calls (iterating inside of functions called from main or from other functions).
And I just realized that I might need a variable-sized function stack, even with no recursive calls.
Example:
```go
pac...I'm currently implementing function calls (iterating inside of functions called from main or from other functions).
And I just realized that I might need a variable-sized function stack, even with no recursive calls.
Example:
```go
package main
import "fmt"
func fibonacci(n int) int {
j0 := 0
j1 := 1
for ; n > 0; n-- {
j1, j0 = j1+j0, j1
}
return j0
}
func main() {
i := fibonacci(10)
j := fibonacci(20)
fmt.Println(i, j)
}
```
Here, once fibonacci at `main:0` completes, it will store its result into the state (`G2PState`). However, it also needs to indicate that on the next call to `get_successors`, it should return to `main:1`. The same goes for fibonacci at `main:1` -> `main:2`.
I see two alternatives to implementing a stack for now:
- Inlining functions.
- For each function, adding two items to the state: `PrevFunctionId` and `PrevNodeId` (in the example, that could be `main` and `0`). This is much simpler than inlining.
I'm going to go with the second option for now.
@renault WDYT?Alexandre KirszenbergAlexandre Kirszenberg