chrony

[stilscher]

I tried to run Goblint on this repository that is also in frama-c's case study benchmarks (#4).

chrony: https://chrony.tuxfamily.org/ at a2d1569455aa10a273e41eba5f79ca6210934d68
goblint: at goblint/analyzer@5ecb6c5 with goblint/analyzer#585
bear: 3.0.8 (compiledb throws errors about not being able to create the already existing directory .deps and not being able to regenerate the Makefile. A workaround for this seems to be the removal of the .deps... and Makefile targets from the Makefile before running compiledb make)

run in chrony:
./configure && bear -- make chronyd (alternatively one can also choose to use chronyc)
or when using compiledb:

git clean -fdx
./configure
make -j 1 chronyd | tee build.log
compiledb --parse build.log

then run the analysis with:

./goblint ../path/to/chrony --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --enable dbg.print_dead_code &> chrony.cil.out -v

output for the analysis of chronyd:

Summary for all memory locations:
	safe:         1257
	vulnerable:      0
	unsafe:          3
	-------------------
	total:        1260

vars = 37055    evals = 76212  

Timings:
TOTAL                          22.663 s
  parse                           1.449 s
  convert to CIL                  1.706 s
  analysis                       19.509 s
    global_inits                    0.056 s
    solving                        19.193 s
      S.Dom.equal                     0.043 s
      postsolver                      4.360 s
    warn_global                     0.008 s
      access                          0.005 s
Timing used
Memory statistics: total=65494.81MB, max=706.25MB, minor=65436.07MB, major=977.57MB, promoted=918.84MB
    minor collections=31220  major collections=20 compactions=0

Found dead code on 4769 lines (including 4683 in uncalled functions)!
Total lines (logical LoC): 11364

[sim642]

bear: 3.0.8 (compiledb throws errors about not being able to create the already existing directory .deps and not being able to regenerate the Makefile. A workaround for this seems to be the removal of the .deps... and Makefile targets from the Makefile before running compiledb make)

This sounds like the project itself wants to use -MD to generate additional Makefiles on the go, but the current include dependency gathering mechanism in Goblint also tries to use the same mechanism, which can break both Goblint and the project's build process. I think it's inevitable that we need to gather the includes via CIL.

[michael-schwarz]

I think it's inevitable that we need to gather the includes via CIL.

I've been planning on getting started with that, but spent today almost only teaching. I'll hopefully get around to it tomorrow 😄

[sim642]

Well, this is fabulous, Goblint's analysis of chrony is also unsound. @vesalvojdani

There's also a function end_resolving, which accesses the same inst struct and its fields, but none of those accesses show with allglobs because the entire function is simply dead.

EDIT: Based on a quick look, this again seems to because the project uses malloc wrappers (memory.c), but Goblint conf doesn't declare them, so all allocated data is joined together into a supertop.
Just adding malloc wrappers isn't enough to fix the issue though, because chrony uses its own dynamic array implementation in array.c, which itself requires Goblint to properly handle realloc (goblint/analyzer#701) and memcpy such that the array contents don't immediately get invalidated to oblivion.

[sim642]

That unsoundness looks fixed by goblint/analyzer#712. Then 8 races are reported, all of which seem to be exclude-able using goblint/analyzer#695 and goblint/analyzer#707.

[sim642]

There would still be unsoundness due to goblint/analyzer#716.

[TimOrtel]

I cannot get this to run on the current Goblint Master Branch. This is my setup. To reproduce simple cherry pick this commit onto the master branch.

The analysis fails with Fatal error: exception Invalid_argument("Cilfacade.get_ikind: non-integer type double ") for me.

[michael-schwarz]

Probably due to goblint/analyzer@2bfadcd. Might be good to identify where the call comes from, one suspect is e.g. comparisons of floats.

[TimOrtel]

I am not really interested in the analysis result but rather in the performance. Can I somehow deactivate this exception without breaking everything? It doesn't matter if the analysis result is wrong afterwards.