MLCFG: Irreducible graphs fail to generate correct VCs
I was doing some investigation to see how well irreducible control flow graphs were handled by MLCFG, only to find out that they seemingly arent!
Consider the following code:
let cfg irreducible (x : bool) : ()
=
var y : int;
{ y <- 0; }
BB0 {
switch (x)
| True -> goto BB1
| False -> goto BB2
end
}
BB1 { y <- y + 1; assert { false }; goto BB2}
BB2 { y <- y - 1; assert { false }; goto BB1}
No verification conditions are generated at all! We can see the problem when we look at the translated code
module A
let irreducible (x : bool) : ()
= [@vc:divergent]
(let ref y = any int in
let rec _from_start (_ : ()) : () =
(y) <- 0 in
_from_start ())
end
The entire irreducible fragment of the graph was elided!
It seems that the transformation assumes reducibility without actually checking it!