`--compare_runs` now segfaults

[vogler]

Comparing results from --save_run with --compare_runs worked fine before, but now it leads to segmentation faults.

$  ./goblint -v --compare_runs out/coreutils/cksum_comb.c.always-side_widen out/coreutils/cksum_comb.c.cycle-side_widen coreutils/cksum_comb.c
...
Unmarshalling out/coreutils/cksum_comb.c.always-side_widen/solver.marshalled... If type of content changed, this will result in a segmentation fault!
Unmarshalling out/coreutils/cksum_comb.c.cycle-side_widen/solver.marshalled... If type of content changed, this will result in a segmentation fault!
[1]    19594 segmentation fault (core dumped)  ./goblint -v --compare_runs out/coreutils/cksum_comb.c.always-side_widen   2>

Runs have been analyzed directly before with the same binary.

$ ./goblint -v coreutils/cksum_comb.c --sets exp.solver.td3.side_widen always --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --disable exp.full-context --disable exp.widen-context --disable exp.widen-context-partial --sets exp.privatization none --disable exp.solver.td3.space_restore --sets dbg.timeout 8h --sets save_run out/coreutils/cksum_comb.c.always-side_widen
...
$ ./goblint -v coreutils/cksum_comb.c --sets exp.solver.td3.side_widen cycle --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --disable exp.full-context --disable exp.widen-context --disable exp.widen-context-partial --sets exp.privatization none --disable exp.solver.td3.space_restore --sets dbg.timeout 8h --sets save_run out/coreutils/cksum_comb.c.cycle-side_widen
...

There's not much that should be going on and the code for comparing did not change:

https://github.com/goblint/analyzer/blob/201b7d94f8269799f4f2f7dc267ec95e48368ff9/src/framework/control.ml#L403-L410

https://github.com/goblint/analyzer/blob/201b7d94f8269799f4f2f7dc267ec95e48368ff9/src/framework/constraints.ml#L1166-L1180

[vogler]

Tried the following to narrow it down:

            (* let (r1, r2) : (Spec.D.t LHT.t * Spec.G.t GHT.t) * (Spec.D.t LHT.t * Spec.G.t GHT.t) = Tuple2.mapn (fun d -> Serialize.unmarshal (d ^ Filename.dir_sep ^ solver_file)) (d1, d2) in *)
            Printf.printf "Loading runs %s and %s\n" d1 d2; flush stdout;
            let r1 : Spec.D.t LHT.t * Spec.G.t GHT.t = Marshal.input (open_in_bin (d1 ^ Filename.dir_sep ^ solver_file)) in
            Printf.printf "Loaded run %s\n" d1; flush stdout;
            let r2 : Spec.D.t LHT.t * Spec.G.t GHT.t = Marshal.input (open_in_bin (d2 ^ Filename.dir_sep ^ solver_file)) in
            Printf.printf "Loaded run %s\n" d2; flush stdout;
            Comp.compare (d1, d2) r1 r2;

and only kept compare_globals g1 g2. It then segfaults on the first call to G.leq: https://github.com/goblint/analyzer/blob/201b7d94f8269799f4f2f7dc267ec95e48368ff9/src/framework/constraints.ml#L1087-L1090

[michael-schwarz]

This is very strange. Did you try with disabling Hashconsing, there were some recent changes/fixes to relifting, maybe it is related to this?

On a different note, should we maybe add a script that tests things such as comparing runs (or incremental) to the GitHub CI? It wouldn't even have to check that these things work correctly as that is hard to check I guess, but one would at least know if it starts failing as soon as one makes a change.

[vogler]

This is very strange. Did you try with disabling Hashconsing, there were some recent changes/fixes to relifting, maybe it is related to this?

The benchmarks should run with hashconsing. I'll check if disabling helps.

On a different note, should we maybe add add script that tests things such as comparing runs (or incremental) to the GitHub CI? It wouldn't even have to check that these things work correctly as that is hard to check I guess, but one would at least know if it starts failing as soon as one makes a change.

Yes, that would probably be a good idea.

[vogler]

I ran --compare_runs without any extra config. Previously it worked since how the values compared did not depend on the set options. For compare_globals it is enough to add --sets exp.privatization none to make it not segfault, i.e., this setting changes the type of globals via some functor. So, one would think loading the config of the runs with --conf would avoid all these problems, but when doing so it still segfaults with the compare_locals(_ctx) code added back in.

$ ../analyzer/goblint --conf out-side_widen-a-c/single-thread/456.hmmer_comb.c.always-side_widen/config.json --compare_runs out-side_widen-a-c/single-thread/456.hmmer_comb.c.always-side_widen out-side_widen-a-c/single-thread/456.hmmer_comb.c.cycle-side_widen single-thread/456.hmmer_comb.c
...
[1]    924 segmentation fault (core dumped)  ../analyzer/goblint --conf  --compare_runs   single-thread/456.hmmer_comb.c

(Maybe --compare_runs should load the config automatically (left or right should not matter since they must have the same types anyway), but options after it should still be able to override, so you'd have to handle the options in phases...)

[michael-schwarz]

Is this still the case? @stilscher, you used this to benchmark things recently, right?

[stilscher]

Yes, the compare_runs worked for the zstd benchmarks. Only the configuration was different there and it was used together with the new node comparison, that compares abstract values of unknowns joined over all contexts.