zstd

[michael-schwarz]

• https://github.com/facebook/zstd/ at 7543085013db1a20a848d166e5931edc49e3cc2f
  • compiledb succeeds
  • Fails as Goblint lacks support for some Intel SIMD things defined in xmmintrin.h:
    /usr/lib/gcc/x86_64-linux-gnu/7/include/xmmintrin.h:120: Unimplemented: doInit: unexpected NEXT_INIT for float __attribute__((__vector_size__(16),__may_alias__))
  • Ignore intrinsics and build with make zstd

diff --git a/programs/Makefile b/programs/Makefile
index 16763e49..8ff545b8 100644
--- a/programs/Makefile
+++ b/programs/Makefile
@@ -138,7 +138,7 @@ allVariants: zstd zstd-compress zstd-decompress zstd-small zstd-frugal zstd-nole
 zstd : CPPFLAGS += $(THREAD_CPP) $(ZLIBCPP) $(LZMACPP) $(LZ4CPP)
 zstd : LDFLAGS += $(THREAD_LD) $(DEBUGFLAGS_LD)
 zstd : LDLIBS += $(ZLIBLD) $(LZMALD) $(LZ4LD)
-zstd : CPPFLAGS += -DZSTD_LEGACY_SUPPORT=$(ZSTD_LEGACY_SUPPORT)
+zstd : CPPFLAGS += -DZSTD_LEGACY_SUPPORT=$(ZSTD_LEGACY_SUPPORT) -DZSTD_NO_INTRINSICS
 ifneq (,$(filter Windows%,$(OS)))
 zstd : $(RES_FILE)
 endif

• Need to comment the contents of includes/assert.h of Goblint for the parsing to succeed?

time ./goblint ../../bench-repos/zstd --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 --enable justcil  --disable include_stdlib --set cppflags[+] -DZSTD_NO_INTRINSICS -v &> zstd.cil.c

real    0m5,836s
user    0m5,495s
sys     0m0,308s

So parsing and everything is also non-horrible here. The program does contain threads.

With ./goblint zstd.cil.c --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 &> zstd.cil.out -v

Summary for all memory locations:
	safe:         2388
	vulnerable:     14
	unsafe:         16
	-------------------
	total:        2418

vars = 170735    evals = 432968  

Timings:
TOTAL                          224.473 s
  parse                           0.544 s
  convert to CIL                  0.694 s
  analysis                       223.237 s
    global_inits                    1.085 s
    solving                        221.102 s
      S.Dom.equal                     0.712 s
      postsolver                     52.939 s
    warn_global                     0.131 s
Timing used
Memory statistics: total=296341.32MB, max=934.02MB, minor=296304.66MB, major=2087.03MB, promoted=2050.37MB
    minor collections=141306  major collections=28 compactions=0

Found dead code on 3427 lines (including 3087 in uncalled functions)!
Total lines (logical LoC): 21415

[michael-schwarz]

Ah, and it requires goblint/analyzer#557 again

[michael-schwarz]

It works non-incrementally, but when I try to run it (on master) incrementally (without any changes to the code) I get

Fatal error: exception Invalid_argument("List.iter2")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from UpdateCil.update_ids.reset_fun in file "src/incremental/updateCil.ml", line 46, characters 4-70
Called from Stdlib__list.iter in file "list.ml", line 110, characters 12-15
Called from UpdateCil.update_ids in file "src/incremental/updateCil.ml", line 126, characters 2-43
Called from Maingoblint.diff_and_rename in file "src/maingoblint.ml", line 457, characters 22-92
Called from Maingoblint.main in file "src/maingoblint.ml", line 509, characters 110-130
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 554, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 560, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20

@stilscher said she'd take a look. May be related to goblint/analyzer#574

[sim642]

The stacktrace looks very similar to the issue I accidentally happened upon indeed: goblint/analyzer#542 (comment). Although actually it doesn't stem from there being a different number of statements, but rather locals:

List.iter2 (fun l o_l -> l.vid <- o_l.vid) f.slocals old_f.slocals;

[stilscher]

We managed to get the incremental analysis to work with the additional option --set cppflags[+] -D_FORTIFY_SOURCE=0.

The problem were multiple functions with the name realpath in the CIL file. The comparison and updating of ids for the incremental analysis assume that the functions in the CIL file have unique names. The realpath definition can be found in the /usr/include/x86_64-linux-gnu/bits/stdlib.h header. The mentioned header is only included when the fortify level is greater than 0. We have not looked into, why multiple realpath functions exist in the CIL file. It might be related to the merging errors I found in #8. However, analyzing with the above mentioned flag could be a reasonable approach for now.

But there are also duplicate global variables in the CIL file at which one needs to look.

[stilscher]

A not too rigorous configuration that worked well for an analysis (took 5-6min for the non-incremental run) is:

./goblint ../test-repos/zstd/ --disable sem.unknown_function.spawn --enable exp.earlyglobs --set ana.base.privatization none --enable incremental.save --enable dbg.print_dead_code --set cppflags[+] -DZSTD_NO_INTRINSICS --set cppflags[+] -D_FORTIFY_SOURCE=0 &> zstd.cil.out -v

Additionally adding intervals led to a steadily increasing number of contexts and I aborted after ~30min.
In the incremental run (without any changes) a big amount of time was needed for the postsolving. So it would be interesting to see how long the incremental analysis (without and with changes) takes when including the incremental postsolving from @sim642 that is currently on the interactive branch.

[michael-schwarz]

You might also want to use -DGOBLINT_NO_BSEARCH to remove some merging conflicts.

If we want to get the runtime a bit higher, we could also try:

• enabling more int domains (e.g. congruence or enums)
• enabling intervals and not them into contexts

[michael-schwarz]

Also, instead of deleting the contents of assert.h, it suffices to set -DGOBLINT_NO_ASSERT as an additional preprocessor flag.