Optimize CFG representation

[sim642]

Split CFG hashtables per function throughout, not just for the duration of connectedness checking (like in #603). This should speed up analogous lookups during transfer functions as well (which use Cfg.prev). The problem is that now looking up the predecessors of a Statement node requires first looking up the fundec of the statement in another mapping just to know which function's CFG hashtable to consult for the predecessors. This might not be too bad (or if it is, then fundec could also be added to Statement or Node.t itself, although changing that requires broader changes). The problem right now has to do with reluctant destabilization, see below.

TODO

• Fix reluctant destabilization. When reluctant destabilization is being applied, there's some limbo between the old CFG and the new CFG. The reluctant solve somehow ends up solving a function with its old ID (because that's what's in the unmarshaled hashtable), but the CFG and the constraint system only know about the function with its new ID. I'm not yet sure whether and how this can be fixed.

• Figure out why a lot of GC is happening in innocent (non-allocating) functions like Hashtbl.mem and Hashtbl.find.

  find shouldn't, but mem does. To be fixed in OCaml standard library: Manually unbox closure in Hashtbl.mem ocaml/ocaml#11500.

• Move fundec into Node.Statement to avoid extra Node.find_fundec lookups?

[sim642]

I think I will cherry-pick some (working) changes from this PR to a new PR that could be safely merged. Then we could already benefit from some optimizations while the full representation change isn't yet in working order.

[sim642]

I've been debugging the reluctant destabilization problem and decided to do some tracing on master to see how it works with the one big CFG hashtable there, but I have become increasingly confused.

Tracing the incremental run of 03-precision-annotation/01-change_precision on master (with an added trace for Cfg.prev, see below), the reluctant solve of the return node of foo outputs the following:

  %%% sol2: solve call of foo on 01-change_precision.c:7:1-12:1, called: false, stable: false
  %%% sol2: init call of foo on 01-change_precision.c:7:1-12:1
  %%% sol: New call of foo on 01-change_precision.c:7:1-12:1
  %%% sol2: eq call of foo on 01-change_precision.c:7:1-12:1
  %%% cfg: call of foo: 
  %%% sol: Var: call of foo on 01-change_precision.c:7:1-12:1
  %%% sol: Contrib:Dead code
  %%% sol: Old value:bot
  %%% sol: New Value:Dead code
  %%% sol2: destabilize call of foo on 01-change_precision.c:7:1-12:1
  %%% sol2: solve call of foo on 01-change_precision.c:7:1-12:1, called: false, stable: true
  %%% sol2: init call of foo on 01-change_precision.c:7:1-12:1

Importantly the cfg: call of foo: line means Cfg.prev for call of foo returns an empty list and thus it concludes that it's completely dead. So it seems to me that the exact same problem of the fundec variable ID changing already exists prior to this PR. The only difference is that instead of blowing up with a Not_found exception, it has always silently caused unsound bottoms.

Therefore, I am now extremely suspicious of reluctant destabilization and have my doubts about the correctness of its implementation. Maybe it's so fast because it just computes trivial bottoms... @stilscher

---

The extra tracing is by:

diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index b7bcd0781..e04509cab 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -598,7 +598,12 @@ let getCFG (file: file) : cfg * cfg =
       (cfgF, cfgB)
   in
   if get_bool "justcfg" then fprint_hash_dot cfgB;
-  H.find_all cfgF, H.find_all cfgB
+  let find_cfg f n =
+    let ns = f n in
+    if Messages.tracing then Messages.trace "cfg" "%a: %a\n" Node.pretty n (d_list ", " Node.pretty) (List.map snd ns);
+    ns
+  in
+  find_cfg (H.find_all cfgF), find_cfg (H.find_all cfgB)
 
 
 (* TODO: unused *)

[stilscher]

So I reconstructed what you described above. The reluctant destabilization works fine on a minimized example without the precision annotation. In the run on 03-precision-annotation/01-change_precision, the problem arises because the new CIL file contains an added global, a GVarDecl for foo which contains the same varinfo as the global GFun for foo that appears in the old and new CIL file but has changed.
The id of this shared varinfo is updated twice in update_ids. First it is adapted to match the corresponding id from the old CIL file as part of updating the ids of changed globals. And then it is updated again, this time with a newly generated id, when the ids for added globals are generated. Due to this, the changed function foo then has a new id that can not be found in the marshaled results of the previous run.
This can also occur when one makes a change inside a function and adds a new change a file and insert a declaration of a function before its actual definition. I created a test case where this leads to the function foo being dead after the incremental run (which is not the case in 03-precision-annotation/01-change_precision because the added precision annotation leads to main also being a changed function).
One could try to fix this by not doing reluctant destabilization for nodes whose id is also in added, that is simply excluding all ids from obsolete_ret that are also in changes.added.

[sim642]

I created a test case where this leads to the function foo being dead after the incremental run (which is not the case in 03-precision-annotation/01-change_precision because the added precision annotation leads to main also being a changed function).

Thanks for looking into it and constructing a test where the unsoundness actually shows. I wasn't 100% sure whether it actually ever would.

One could try to fix this by not doing reluctant destabilization for nodes whose id is also in added, that is simply excluding all ids from obsolete_ret that are also in changes.added.

This feels like a quick hack than a proper fix, because really the problem is with the incremental comparison and updating, if it gets confused by a GVarDecl. Large and real-world programs heavily use function declarations, which get included into lots of files, so I think we should aim to fix the underlying issue since it's more likely to happen on real programs than our small tests that usually don't forward-declare any functions.

[stilscher]

This feels like a quick hack than a proper fix, because really the problem is with the incremental comparison and updating, if it gets confused by a GVarDecl

Actually I also have some doubts about whether the reluctant destabilization in the solver is the right place to handle this. But I think the comparison and updating of ids is actually quite consistent. The varinfo receives a new id because the declaration was newly added. I'm not so sure whether the distinguishing between changes in GFun and GVarDecl in the comparison algorithm should be removed even if they share the same varinfo object. At least they represent different Cil data structures and I think it is cleaner to categorize them separately instead of letting changes in one of them influence how the other is categorized.

Large and real-world programs heavily use function declarations, which get included into lots of files

That is probably true. However, a change that adds a function declaration for a function that already exists and is changed at the same time is probably rather rare. And as far as I know, this should be the only case were the problem occurs.

Maybe one can do a quick fix, to make sure that our benchmarks are correct and open an issue to think about improving it later?

[sim642]

The varinfo receives a new id because the declaration was newly added. I'm not so sure whether the distinguishing between changes in GFun and GVarDecl in the comparison algorithm should be removed even if they share the same varinfo object. At least they represent different Cil data structures and I think it is cleaner to categorize them separately instead of letting changes in one of them influence how the other is categorized.

I think the comparison and updating should still ensure that the invariant holds that they share the same varinfo, otherwise we really risk breaking an assumption that's made all over the place, including inside CIL itself. But I guess the updating needs to be smarter about it when both are present.

Maybe one can do a quick fix, to make sure that our benchmarks are correct and open an issue to think about improving it later?

That makes sense, we don't have to make the more sophisticated general fix immediately and in this PR.

[sim642]

Just to make it very clear, this is blocked by #627.

[sim642]

I now brought this up to date and the previously failing incremental test at least passes now.
But somehow this is breaking incremental tests with CFG comparison.

EDIT: I managed to fix the major issue, but one failure still remains.

EDIT 2: I managed to also fix the last issue for now.

[sim642]

@michael-schwarz Was it the plan for some students to benchmark this? If so, then this should be in a suitable state for doing so.

It's still suboptimal due to extra Node.find_fundec lookups. That could be optimized if need be.

EDIT: Apparently not. My last fix broke the added test again, so there might be more to this with CFG comparison.

[michael-schwarz]

The thought was that the students working on improving Goblint performance might want to consider this. However, if it is currently broken in a way we do not 100% understand ourselves, it may be better to not include it in the scope of their work.

[sim642]

It does work non-incrementally, so it would still be possible to benchmark this. If there's no benefit, then there's no reason to try to fix it for CFG comparison either. So it could still be tried if there's interest/resources, but it's not a top priority.

[sim642]

I merged master into this and two CFG comparison tests still fail: one crashes in some List.iter2 and the other is unsound.

[jerhard]

As discussed at Gobcon today, one may try to evaluate this with ffmpeg, as this was the reason for this PR (see #603).
In case there is no speed up on ffmpeg, this PR can be closed without merging.

If this turns out to be useful but still breaks the CFG comparison, one may remove the CFG comparison.