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.

[michael-schwarz]

You could locally change cilfacade.ml to the old behavior, i.e., warn and return IInt.

[sim642]

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.

https://theprofoundprogrammer.com/post/28974600028/text-it-doesnt-work-but-its-fast — the correctness of the analysis result does matter for performance, because it's easy to make things faster by breaking them.

It's good to have this regression come out though, because we'll need to fix it if there's going to be an interactive paper artifact that uses chrony.

[TimOrtel]

#define NTP_ERA_SPLIT seems to be randomly changing between different runs of Goblint. I did not have time to investigate this. However, when inspecting the incremental results you will find UTI_Int64ToTimeval and UTI_IsTimeOffsetSane and do_time_checks changed, because they reference NTP_ERA_SPLIT.

[TimOrtel]

I am getting a ton of Fixpoint not reached errors when analyzing chrony with the default analysis configuration (ana.activated not set). However the analysis works with only base and mallocWrapper set. What could be the reason for this? Logfile

[sim642]

These seem to be somehow related to anonymous structs and unions for which CIL generates fresh names containing some numbers. The errors don't look exactly like these, but it could be related to goblint/analyzer#678.

It might also be due to some difference between Goblint's master and interactive branches, because we used the latter for some evaluation and AFAIK didn't get fixpoint errors at the time.

[TimOrtel]

Which analysis do I have to disable to circumvent this error?