Automatizing Blackbox transformation via LTL formulae
Last week, I ran two benchmarks on two RERS files, if you want to see the result, check it out here.
We can clearly see Blackbox are handling well the state space explosion problem, the number of states and transitions are drastically reduced, depending on the file.
Now we know, Blackbox is a good way to handle this problem, we want to make it easier to use, it is what I’ll be doing this week.
Combining CallGraph with variables dependencies
If we take the 2016-Problem1-ltl.go
file, we can easily draw a Call Graph, so here we go :
Taking our LTL formulae next, we can determinize what functions are needed.
So let’s take one and see how it can be interpreted:
! (false R (! ("main_final_output == 19" && (true U "main_final_output == 24")) ||
((! "main_main___RERS__ == 4" ||
(! "main_final_output == 24" U (("main_final_output == 20" &&
! "main_final_output == 24") &&
X (! "main_final_output == 24" U "main_final_output == 23"))))
U "main_final_output == 24")))
We can easily parse it and obtain the wanted variables, and with it our wanted functions. In this particular case we can see the needed function is just main
.
Parsing LTL formulae
So we previously saw what we need, the most basic implementation will be to browse our LTL formulae file line by line and seek for everything between quotes, once we have this, we can seek in the variables the function’s name.
Basically the idea is to maintain a map
with the function’s name as key and a boolean as value, to know if this function is needed in our main thread, and not to be Blackboxed. So let’s go implement a function that does this.
A little example of what it will output with the given LTL formulae :
main true
errorCheck false
calculate_output false
calculate_outputm1 false
calculate_outputm2 false
calculate_outputm3 false
calculate_outputm4 false
calculate_outputm5 false
calculate_outputm6 false
calculate_outputm7 false
calculate_outputm8 false
calculate_outputm9 false
calculate_outputm10 false
calculate_outputm11 false
calculate_outputm12 false
calculate_outputm13 false
calculate_outputm14 false
With this we can draw again our Call Graph :
Ok it seems a little bit overkill for one function, but you need to see bigger. If we need some variables in
calculate_outputm6
and calculate_outputm10
, we will obtain something like this:
Make our Call Graph interract with our list of needed functions
We now have all the necessary elements to automatize our Blackbox transform.
For this we only need to go up in our graph from all the needed functions to the root, and mark all the function we go through as needed too.
Once again, a drawing is better than all the words in the world :
Let’s take our previous graph and apply what I just explained to you.
We go down in our graph, once we encounter a function that is needed, when we go up we set the caller to needed too. So
calculate_output
become needed too (here in yellow).
Handling more complexe cases
Let’s take a simple (but not so simple) Call Graph:
Handling Blackbox with a white list of functions seems easier, since we can decide that every caller has to be in the white list too.
If we want to have
foo
, we will automatically find that bar
can’t be Blackbox.
Same for baz
function, since qux
is a caller we can’t make it a Blackbox.
Let’s suppose now we want to blackbox
foo
, there won’t be any problem, since foo
isn’t calling anyone.
Let’s suppose now it is bar
we want to blackbox, what should be the correct behaviour ?
![Snow](https://ryukizo.space/img/8.png)
![Forest](https://ryukizo.space/img/9.png)
Do we decide to ignore foo
because it is called by bar
or do we decide to say bar
can’t be Blackbox since there is a function called by it ?
So for now using a white-list rather than a black-list seems far way better, a decision should be taken deciding the correct behaviour for calling Blackbox, thus the main problem still reside in the fact that blackbox won’t be able to communicate with the main package.
Links and more
- Linear temporal logic, https://en.wikipedia.org/wiki/Linear_temporal_logic
- Clarke E.M., Klieber W., Nováček M., Zuliani P. (2012) Model Checking and the State Explosion Problem. In: Meyer B., Nordio M. (eds) Tools for Practical Software Verification. LASER 2011. Lecture Notes in Computer Science, vol 7682. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35746-6_1
- Call Graph, https://en.wikipedia.org/wiki/Call_graph
- Golang Regexp Package, https://golang.org/pkg/regexp/