go2pins issueshttps://gitlab.lre.epita.fr/spot/go2pins/-/issues2022-02-15T11:49:44+01:00https://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/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/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
```