Running on coreutils yields exception from library mechansim

[michael-schwarz]

As @reb-ddm has observed, Goblint can currently not run on its benchmark suite anymore for many programs. Consider, e.g., ./goblint ../bench/coreutils/cp_comb.c on the current master.

Fatal error: exception LibraryDsl.Pattern.Expected("Library function is called with more arguments than expected.")
Raised at LibraryDsl.Pattern.fail in file "src/util/library/libraryDsl.ml", line 14, characters 15-33
Called from Goblint_lib__AutoTune.hasFunction.relevant_static.(fun) in file "src/autoTune.ml", line 158, characters 41-60
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 29-34
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 38-48
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 38-48
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 38-48
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 38-48
Called from Stdlib__Map.Make.exists in file "map.ml", line 329, characters 38-48
Called from Goblint_lib__AutoTune.hasFunction in file "src/autoTune.ml", line 175, characters 2-77
Called from Goblint_lib__AutoSoundConfig.activateLongjmpAnalysesWhenRequired in file "src/util/autoSoundConfig.ml", line 67, characters 5-26
Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 60, characters 6-60
Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63
Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61
Called from Std_exit in file "std_exit.ml", line 18, characters 8-20

We attempted a principled fix, but that turned out to be non-trivial, so we provided a hacky workaround (https://github.com/goblint/analyzer/pull/1485/commits/8173b99f25903d3ea68d7a22a042ec3bbb5a7c94).

[sim642]

Seems like a library function declaration has incorrect arguments in Goblint. The annoying thing is that the autotuner doesn't set up our custom backtraces with program locations to easily tell where and what is the cause.

[michael-schwarz]

If you just uncomment the autotuner, an exception will be raised that comes with a backtrace, as the function seems to be actually called.

[michael-schwarz]

I'm wondering if we should not attempt to be more lenient here and emit a warning and continue analysis, rather than outright refusing to execute with a strange error message that is hard for users to grasp?

[sim642]

I want to improve the exception to replace this very internal one with an user-facing one that includes the function name etc.

Swallowing these with a warning isn't good for us because it's unlikely that we'll find out that we have some typo in a library function declaration. There's no reason Goblint should contain incorrect library function declarations. Depending on what swallowing does, we'd implicitly become unsound (if we don't invalidate the arguments) or very imprecise (if we deeply write/spawn the arguments).