Storing our formulae in a configuration file

As we saw before, we are always “playing” with some formulae and it can be boring to lug around with it everytime. Especially when we have more than one formula. Therefore, I decided to create a configuration file to keep a track on what we need to use, for now it only contains a list of formula, but later we can consider to add more informations (Model checking backend to use, Number of thread to use…).

Which file format are we going to use ?

There are a few file format we can use, YAML1, JSON2, XML3, CSV4, Protobuf5 and many more I guess. My choice went to JSON, why ? Because golang provide directly a package, encoding/json.

What’s new in go2pins-mc ?

All formulae are now automatically saved in a config.json located at the root of the generated directory.
Using the -formulae flag with go2pins or just giving a single formula will be detected and then placed accordingly in the configuration file. Example:

{
    "formulae": [
        "EMPTY !<> ((\"main___VERIFIER_error_n == 0\") && \"main___VERIFIER_error__callerLabel != 0\")",
        ...
    ]
}

Thus, we have our configuration file and we want to interract with it, let me introduce two new flags:

  • -formulae displays all the saved formulae with their index.
  • -formula index computes the desired formula from the configuration file based on its index.

A concrete example would be to use it like that, let’s suppose a formulae.txt file containing 42 formulae:

❯ go2pins -formulae formulae.txt file.go
❯ ./output/go2pins-mc -formula 27

This will compute the 28th formula of :formulae.txt.

Want to have a look on this ? Here it is:

Going deeper with our Blackbox transitions

As we saw during the previous weeks, we are now able to ignore “any” desired functions to focus on one or more global variables with our blackbox. We want now to focus on a more complex problem, what if we want to ignore part of a function ?

Ignoring Statements ?

We need to put an image on what we are going to do so let’s focus on an example and I will try to explain what we need to do with it.

package main

var a int

func foo() {
        // Modifying global variable a
        a = 2
}

func main() {
        println(a)
        foo()
        println(a)
}

Playground link.

Okay nothing too complicated here, if we want to keep everything modifying our variable a, we will keep every functions, here foo.

Let’s see a simple case where we can ignore some statements.

package main

var a int

func foo() {
	// Creating a new variable, b
	b := 20
	b += 20
	// Modifying global variable a
	a = 2
}

func main() {
	println(a)
	foo()
	println(a)
}

Playground link.

You’re beginning to see where I want to go, here the variable b is not useful for us, so we can simply put it away by “ignoring” and put it in a blackbox block.

I continue with something a little bit more tricky.

package main

var a int

func foo() {
	// Creating a new variable, b
	b := 20
	b += 20
	// Modifying global variable a
	a = 2
	// Assigning to b with global variable a
	b += a
}

func main() {
	println(a)
	foo()
	println(a)
}

Playground link.

We can see our output is always the same. Since the global variable a is only accessed and not modified, do we now need to keep our b variable with us or can we just ignore this new new statement too ? It can’t be really obvious at the beginning, but since we need to access to our global variable a, we can’t put these new statement away unless we create an error: Not defined variable: a.

So here we can see our guideline, whenever the wanted variable is accessed or modified, we will need to keep the current statement.

Variable dependencies

Let’s continue to escalate thing with trickier and trickier cases.

package main

var a int

func foo() {
	// Creating a new variable, d
	d := 10
	// Creating a new variable, c
	c := 10 + d
	// Creating a new variable, b
	b := 20
	b += c
	// Modifying global variable a
	a = 2
	// Assigning to b with global variable a
	b += a
}

func main() {
	println(a)
	foo()
	println(a)
}

Playground link.

There are not much codes and it’s already really messy to figure out what we need to do… Okay so we want to keep our global variable a, but since b is accessing a, we also want to keep b and same for c and d.

What’s the point to show allof that ? It’s really important to figure now how we are going to process to ignore undesired statements. And this case allow me to think that we will need a map of all variable inter-dependencies. Let me picture it:

a: []
b: [c, a]
c: [d]
d: []

First, if a had some dependencies we would be sure that we can’t ignore them. Secondly, we can easily draw a graph of our dependencies (representing in green our wanted variables):

We now know we will have to explore our Abstract syntax tree to get this informations, before making any decisions. We also know c and d can be computed in a blackbox function since a is not directly interacting with it.

Function calls

Okay, now let’s see about function call, obviously same as our variable dependencies, any function accessing or modifying our wanted variable won’t be ignored. But what if a function takes as parameter one of our wanted variable ? Same as before, if our variable is not used in the function, using it as a parameter won’t do anything, thus the function call will remain the same and the function ignored.

package main

var a int

func foo(x int) {
	// Creating a new variable, b
	b := x
	b += 2
}

func main() {
	println(a)
	foo(a)
	println(a)
}

Playground link.

We clearly see with this example that a is used as parameter in foo function, since in foo, it’s not a anymore but x, this function will be ignored anyway.

Let’s suppose already have a blackboxed function but there are statements to ignore.

package main

var a int

func bar() {
	// Creating a new variable, b
	b := 40
	b += 2
}

func foo() {
	// Calling a function, bar
	bar()
	// Modifying global variable a
	a = 2
	// Calling a function, bar
	bar()
	// Calling a function, bar
	bar()
}

func main() {
	println(a)
	foo()
	println(a)
}

Playground link.

The first call to bar will already be a call to a blackbox function, but after there are two calls to bar, do we regroup this into one statement ?

Variable shadowing

Let’s focus on a case that may occurs and seems tricky, variable shadowing.

package main

var a int

func foo() {
	// Creating a new variable, b
	b := 40
	// Modifying global variable a
	a = 2
	// Creating a new variable, a (variable shadowing)
	a := 60
	b += a
}

func main() {
	println(a)
	foo()
	println(a)
}

Playground link.

We clearly see we don’t need anything excepting the statement that modifies our global variable a. The problem is that we have a new variable with the same name. How to resolve this conflict ? Let’s take a look at ast.Ident. We can identify a variable with its Name, but with its Obj too. So we can now deduce two new things:

  • We will need a map for each function.
  • We will not store variable Name, but variable Obj.

Scoping

Next question to ask is how are we gonna handle the scoping ? If we take our previous example:

package main

var a int

func foo() {
        // TO IGNORE
	// Creating a new variable, b
	b := 40
	// Modifying global variable a
	a = 2
        // TO IGNORE
	// Creating a new variable, a (variable shadowing)
	a := 60
        // TO IGNORE
	b += a
}

func main() {
	println(a)
	foo()
	println(a)
}

We need to ignore three statements, but between them we have a statement we can’t ignore. Do we make two new scopes to ignore or one big scope in which we put the three statements ? Since a does not need them, they can be regrouped.

Recap

We have now an idea what we are going to deal with and what need to be ignored. The guideline is to explore our abstract syntax tree to determine which statements need to be kept. And especially when it’s a matter of variable.

Links and more

References

  1. https://en.wikipedia.org/wiki/YAML ↩︎

  2. https://en.wikipedia.org/wiki/JSON ↩︎

  3. https://en.wikipedia.org/wiki/XML ↩︎

  4. https://en.wikipedia.org/wiki/Comma-separated_values ↩︎

  5. https://en.wikipedia.org/wiki/Protocol_Buffers ↩︎