go2pins issueshttps://gitlab.lre.epita.fr/spot/go2pins/-/issues2020-11-17T17:00:07+01:00https://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/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/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/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/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 Kirszenberghttps://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/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 Moreau