Going deeper with our blackbox transitions

As you know, Go2Pins is now able to fully abstract functions if it is not needed in our verification process. The results are really great about it, but we want to go deeper by pushing the blackbox process further.
As we saw previously, we want now to be able to ignore not just functions, but parts of a functions. We already had a starting idea in the last articles, we need to continue seeking this way, so here we go.

The main idea

We will take an example and focus on it to describe what we want to do.

package main

var a int

func foo() {
    a = 2
    b := a + 40
    println(b)
    if b == a {
        b = 0
    }
    println(b)
}

func main() {
    foo()
}

Playground link.

If we look at this code roughly, we can see three things that we may want to keep as informations to proceed our transformation:

• global variable a
• function foo
• function main

We need to think on a way to get more informations and to detect what we need for every situations and not a single case, but identifying global variables and functions declarations are a very good starting point.

A good starting point

If we continue to look at this code as a human and not with what Go may be able to do, we can continue to treat informations and then seek a pattern in order to be applied in any situations. Let’s decompose what we have, here it will be function declarations:

• global variables:
  • a
• functions declarations:
  • foo:
    • Body containing 5 statements.
    • Manipulating 2 variables:
      • a
      • b
  • main:
    • Body containing 1 statement.

Okay… Just wow, are we really enjoying doing this ? Nah, I don’t think so, but we can clearly see where we need to go and hopefully we will stop doing this manually. The main things to see is that foo contains 5 statements and manipulate a (which is a global variable).
To sum up, we can obtain the global variables of the file and some informations about the file’s functions. So what’s the next step ? Consider we can do this with Go2pins, because we will.

The Next Step

The “main idea” is to ignore not necessary statements, we will need informations about statements then and particularly if some statements are manipulating variables, because the process will be based on wanted variables. Let’s suppose we can obtain these informations about our statements (we will), it’s better to think on a way to organize it.

The first question to ask is how do we store these informations ? A list representing our functions’ statements ? It seems like a very good idea, but let me tell you why it isn’t. We want to retrieve easily these informations and as I said before, the way we will use all of this is based on the wanted variables. See the point ? Yes, we will lose time if we are seeking twice the informations, it will then be organized based on the variables the function is manipulating.

The second question is do we need all informations ? If I simplify this question, it will be more like do we care if a variable is being written or read ? Yes, we do, but we need to identify these two different cases to treat our process in the more effective manner.

Let’s make it clear:
We need to store informations based on function’s variables and differentiate Read and Write access to these variables.

Let’s look together on our code again:

package main

var a int

func foo() {
    a = 2
    b := a + 40
    println(b)
    if b == a {
        b = 0
    }
    println(b)
}

func main() {
    foo()
}

Playground link.

Let’s try to do this briefly on the foo function, we know we have 5 statements and 2 variables:

R: READ
W: WRITE

It is really clear now to identify which statements are needed if we want to treat the variable a. It will be the first statement since we only want to see when its value change.
Are we done here ? Not really, one last thing we may want is variables dependencies.

Variables Dependencies

What if a variable is assigned the value of another ? Actually the readed variable will then become wanted as well. With our example if we dress a map, it would look like this:

Since statement 2 is b := a + 40, b is assigned the value of a.

We now have all the informations wished to perform our blackboxing in a proper way.

Blackboxing statements

Now we have all our informations, we want to see what it will look like at the end. Let’s take back all we got far from here:

package main

var a int

func foo() {
    a = 2
    b := a + 40
    println(b)
    if b == a {
        b = 0
    }
    println(b)
}

func main() {
    foo()
}

Playground link.

List of foo’s statements:

Variables Dependencies:

Let’s suppose we want to check a, the awaited result will look like this:

package main

var a int

func BB_foo() {
    b := a + 40
    println(b)
    if b == a {
        b = 0
    }
    println(b)
}

func foo() {
    a = 2
    BB_foo()
}

func main() {
    foo()
}

Playground link.

Let’s now suppose we want to check b:
Actually nothing, it will be the same as the beginning, why ? Because we only have single statement to ignore, it is then useless to ignore them.

Tricky cases

We have seen in a detached way what we need to do, but the path to success will be strewn with pitfalls.

Handling Block of Statements

As we saw, a function declarations contains a Block of Statements or a Body, call it as you want. We will need to handle statements contained in Body of statements.

For now, we will handle:

• If statement body
• Else Statement body
• For Statement body

We will then need to keep a track on the statement’s location inside the function we are treating.

Identifying Read and Write Acess to Variables

Okay we said we need to differenciate Read and Write access, then we need to know in which case a variable is written.
Since we are not treating pointers yet, there is only two cases we need to focus on:

• Assignment Statement
• Increment and Decrement Statement

Processing our informations

We seems to have all informations and all methods to obtain it, but the really hard part will be to use it. What we actually want is to put unwanted statement in a new function. It can be seen as just a cut and paste, but there are things that we need to take care about.
The function’s parameters should be the same since we will maybe access to parameters.
We can’t ignore a return statement.
We have to take care about statement order, and especially when a variable value change.

Recap

We saw today what will be our way of processing blackbox for single statement:

• Identifying Read and Write access to variables.
• Identifying variables dependencies.
• Keeping only the Write access of the needed variables.
• Repeat operations for dependencies.

This way we can achieve what we want to do, but we also there are some tricky cases we need to handle.

What was done until now

We have all our wanted informations and we are currently looking on a way to make the transform the right way.

You can find the code here:

• SHA1: 15b0fe85