goblint / goblint/analyzer

`--compare_runs` now segfaults

Open
#240 6 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
OCaml
Stars
252
Forks
90
Avg merge
4d 1m
Merged PRs (30d)
19

Description

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

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Reproduce the crash with the shown --save_run and --compare_runs commands, then inspect src/framework/control.ml lines 403-410 and src/framework/constraints.ml lines 1166-1180. Compare the unmarshalling and comparison paths for runs produced by the same binary. Done means comparing the two saved runs completes without a segmentation fault.

Written by the indexing model from the issue text.

Assessment

Tech stack
c, ocaml
Domain
devtools
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.