Maintaining Go2Pins

Last week, we discovered some errors processing some files to Go2Pins. As errors we can list this :

• Blackboxing non wanted functions, see details.
• LocalVariableAssignements transform not treating Global varialbes declared after using it, see details.
• Handling Multiple assignments on function call, see details.
• Linking function results to other packages (including Blackbox) functions, see details.

Blackboxing non wanted functions

Go2Pins used to blackbox more functions than expected, fixing that was easy, we just have to check our vector of wanted functions to be blackboxed. However, this commit fixed it.

LocalVariableAssignements transform not treating Global varialbes declared after using it

Previously, LocalVariablesAssignments transform did not work well when a global variables was declared after accessing (assignment or used) it. Example:

package main

func main() {
    a = 42 /* assignment */
}

var a int

Since meta did not store it in our vector, no transform will be applied on the assignment in the main function. Resulting to something like this:

package main

func G2P_main(G2PState structs.G2PStateType) {
    G2PState[5] = 0  // global variable a
    a = 42
}

Thus, the “simplest thing” to do was to adapt our LocalVariableAssignments to handle it separately by browsing my file first for Global variables and then for Local Variables.

Since it is two layers, we used a boolean to detect if it’s the global layer or the local layer. So that’s why our compilTo() function in main uses the main package calls twice ApplyAll().

This commit is the fix.

Handling Multiple assignments on function call

Multiple Assignments

When it comes to multiple assignments including one that contains a function call, Go2Pins failed to handle it well.
Example:

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 did not work. It ignored everything except the function call. Thus, an easy way to handle it was to make one assignment for each function call, keeping our original AssignStmt to normal:

package main

func foo() int {
    return 42
}

func main() {
    G2P_foo_1 = foo()
    a, b := G2P_foo_1, 2
    G2P_foo_2 = foo()
    a, b = 2, G2P_foo_2
    G2P_foo_3 := foo()
    G2P_foo_4 := foo()
    a, b = G2P_foo_3, G2P_foo_4
}

Inner Call to functions

Because function arguments are considered as “Assignments” as well, inner call to function was not handled well too.

package main

func foo(x, y int) int {
	return x + y
}

func bar() int {
	return 42
}

func main() {
	a := foo(bar(), -42)
	a = a
}

Fixing it

This commit fixed it. We created a new transform, InnerCall, ArithmeticCall transform’s little brother. Keeping it simple, InnerCall transform will check for two types of ast.CallExpr:

• The one contained in an ast.ExprStmt,
• The one contained in an ast.AssignStmt,

The transfrom is quite the same for this two CallExpr, it will recursively go down the function arguments and check if it’s other CallExpr, by creating some equivalent Assignments to decompose these CallExpr in multiple AssignStmt. We don’t take simply our CallExpr as it comes since we want to treat it from the root of their call, so from a Statement. Let’s take this file:

package main

import "fmt"

/* Some functions, you don't need to know more */

func main() {
    fmt.Println(foo(foo(bar(40), 2), bar(baz())), foo(1, 1))
}

Okay… it is little bit complicated here, let’s rename it for a better understanding:

fmt.Println(foo_1(foo_2(bar_1(40), 2), bar_2(baz())), foo_3(1, 1))

We have a function called CallExprRec(), as its name show, it is browsing recursively each arguments of our functions. The InnerCall will detect the first CallExpr fmt.Println and will call CallExprRec() on it. So you guessed it, CallExprRec() is called once more on the detected CallExpr arguments and creating a temporary variable that has this value, if it contains more than one argument and if one of them is a CallExpr it will treat it, otherwise, the function as it is.

Take a time and guess how many times it will be called on this example and how many temporary variables will be created ?
The answer here
It will be called 7 times including the original call:

• fmt.Println()
• foo_1()
• foo_2()
• bar_1()
• bar_2()
• baz()
• foo_3() So basically all CallExpr, because we need to check their arguments everytime.

And now for the number of variables created, it is 5, why ?

• foo_1() is an argument of fmt.Println() and fmt.Println() has 3 arguments.
• foo_3() as foo_1() and foo_3().
• foo_2() is an argment of foo_1() that has 2 arguments.
• bar_2() as foo_2().
• bar_1() is an argument of foo_2() that has 2 arguments. As said previously, everytime there is a function call and more than one arguments, there is a new variable. With a given file:

package main

import (
	"fmt"
)

func foo(x int) int {
	return x
}

func bar(x, y int) int {
	return x + y
}

func main() {
	a, b := bar(foo(4), foo(20)), foo(54)
	fmt.Println(a, b)
	fmt.Println(foo(2011920))
	fmt.Println(bar(foo(42), foo(3)), foo(55), bar(400, 4))
}

InnerCall transform will give this:

package main

import (
	"fmt"
)

func foo(x int) int {
	return x
}
func bar(x, y int) int {
	return x + y
}
func main() {
	G2P_foo_1 := foo(4)
	G2P_foo_2 := foo(20)
	G2P_bar_1 := bar(G2P_foo_1, G2P_foo_2)
	G2P_foo_3 := foo(54)
	a, b := G2P_bar_1, G2P_foo_3
	G2P_is_alive_a := 1
	G2P_is_alive_b := 1
	fmt.Println(a, b)
	fmt.Println(foo(2011920))
	G2P_foo_4 := foo(42)
	G2P_foo_5 := foo(3)
	G2P_bar_2 := bar(G2P_foo_4, G2P_foo_5)
	G2P_foo_6 := foo(55)
	G2P_bar_3 := bar(400, 4)
	fmt.Println(G2P_bar_2, G2P_foo_6, G2P_bar_3)
}

In a continuous integration context, SelectorExpr (other packages functions) are not decomposed. Let’s assume we call Go2Pins on the same file but with blackbox on foo and bar, nothing is changed, avoiding state explosion:

package main

import (
	"fmt"
	"output/blackbox"
)

func main() {
	a, b := blackbox.Bar(blackbox.Foo(4), blackbox.Foo(20)), blackbox.Foo(54)
	G2P_is_alive_a := 1
	G2P_is_alive_b := 1
	fmt.Println(a, b)
	fmt.Println(blackbox.Foo(2011920))
	fmt.Println(blackbox.Bar(blackbox.Foo(42), blackbox.Foo(3)), blackbox.Foo(55), blackbox.Bar(400, 4))
}

With blackboxed functions, we have 9 states and 9 transitions against 48 states and 48 transitions with these new transform.

Linking function results to other packages (including Blackbox) functions

Calling an external functions with as parameters a function call defined in the current context didn’t link the proper result(s). Short example:

package main

import "fmt"

func foo() int {
    return 42
}

func main() {
    fmt.Println(foo())
}

It appeared it was just a typo in our code. This commit fixed it, a typo slipped into our code.
Misunderstanding the size of the results between two nested CallExpr.

Grip on RERS files

The RERS Challenge provides a wealth of problems of increasing complexity, the more involved of which will probably be beyond any individual state-of-the-art method or tool. In order to encourage cooperation and the consideration of alternative solutions, the RERS Challenges follow a clear free-style philosophy: Apply whatever approach you consider to be valuable, be it one that is already available or one that you are willing to specifically conceive/implement.

I won’t describe a lot what is RERS challenge, if you want more infos, check it here. We use files coming from the RERS which have been translated into Go in order to evaluate the scalability of Go2Pins.

RERS as it come

I tested 2 RERS files, and we can see two different things:

2016-Problem1-ltl.go

As you can see, our Blackbox approach seems to work well on this file, the number of states and transitions goes down slowly, going from (26141,35145) to (4830,7786), dividing by 6 the number of states and by 5 the number of transitions.

2016-Problem10-Reach.go

Here you can see that our state space decrease really fast, and then stay at 10000 states and transitions.

Links and more

• RERS Challenge, http://www.rers-challenge.org/