`Unimplemented: joinLoc` `Errormsg.Error while parsing` on `bench`

[vogler]

bench/coreutils but also others now fail with an exception while parsing:

./goblint -v coreutils/cksum_comb.c --enable exp.solver.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --disable ana.context.widen --sets exp.privatization none --disable exp.solver.td3.space_restore --sets dbg.timeout 6h --sets save_run out/coreutils/cksum_comb.c.enable-term
Custom include dirs:
  1. /home/voglerr/bench/includes (exists=true)
Preprocessing files.
Preprocessor cpp: is_bad=false
cpp --undef __BLOCKS__ '-I' '/home/voglerr/bench/includes' "/home/voglerr/bench/includes/stdlib.c" -o "/home/voglerr/bench/goblint_temp_68b1cf/stdlib.c"
cpp --undef __BLOCKS__ '-I' '/home/voglerr/bench/includes' "coreutils/cksum_comb.c" -o "/home/voglerr/bench/goblint_temp_68b1cf/cksum_comb.c"
Parsing files.
Frontc is parsing /home/voglerr/bench/goblint_temp_68b1cf/stdlib.c
Converting CABS->CIL
Frontc is parsing /home/voglerr/bench/goblint_temp_68b1cf/cksum_comb.c
Unimplemented: joinLoc parse-datetime.c:1765:3--1:-1 parse-datetime.y:325:38--1:-1
Caught Errormsg.Error while parsing
Fatal error: exception Errormsg.Error
Raised at Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 210, characters 6-13
Called from Frontc.parse_to_cabs in file "src/frontc/frontc.ml", line 121, characters 13-38
Called from Frontc.parse_helper in file "src/frontc/frontc.ml", line 256, characters 13-32
Called from Frontc.parse in file "src/frontc/frontc.ml" (inlined), line 264, characters 32-55
Called from Cilfacade.parse in file "src/util/cilfacade.ml", line 48, characters 2-26
Called from Stdlib__list.rev_map.rmap_f in file "list.ml", line 103, characters 22-25
Called from Maingoblint.merge_preprocessed in file "src/maingoblint.ml", line 292, characters 18-62
Called from Maingoblint.main in file "src/maingoblint.ml", line 505, characters 15-56
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
Command exited with non-zero status 2
	Command being timed: "./goblint -v coreutils/cksum_comb.c --enable exp.solver.td3.term --enable exp.earlyglobs --enable ana.int.interval --disable ana.int.enums --disable ana.int.def_exc --disable ana.context.widen --sets exp.privatization none --disable exp.solver.td3.space_restore --sets dbg.timeout 6h --sets save_run out/coreutils/cksum_comb.c.enable-term"
	User time (seconds): 0.18
	System time (seconds): 0.04
	Percent of CPU this job got: 98%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.23
	Average shared text size (kbytes): 0
	Average unshared data size (kbytes): 0
	Average stack size (kbytes): 0
	Average total size (kbytes): 0
	Maximum resident set size (kbytes): 33896
	Average resident set size (kbytes): 0
	Major (requiring I/O) page faults: 0
	Minor (reclaiming a frame) page faults: 7728
	Voluntary context switches: 20
	Involuntary context switches: 1
	Swaps: 0
	File system inputs: 0
	File system outputs: 3768
	Socket messages sent: 0
	Socket messages received: 0
	Signals delivered: 0
	Page size (bytes): 4096
	Exit status: 2

[sim642]

Great, I thought it was just the deprecated LLVM C++ -> C converter that produced code where the function definition header and function definition end were in different files, but apparently there's more... I wonder what nonsense this benchmark contains then.

[vogler]

Is it a problem of #51 not being extensive enough or were files preprocessed in a wrong way?

If it's the latter we could update those *_comb.c files.
At the end of the file it says char const *Version = "8.13.14-081e2-dirty";
Latest https://github.com/coreutils/coreutils tag is v9.0.

[michael-schwarz]

joinLoc parse-datetime.c:1765:3--1:-1 parse-datetime.y:325:38--1:-1
The y file extension seems to point at a parser that is generated by YACC/BISON, so I guess recombining will still yield the same issue.

[vogler]

I checked out a commit before #51 and adjusted goblint, but for #53 there'd be a lot more places to undo in goblint.
It's a bit disappointing that there's no easy way to revert a PR for testing (without also undoing other changes).

[sim642]

I found the problematic part in the benchmark:

#line 1509 "parse-datetime.c"
int yyparse(parser_control *pc ) 
// omitted
#line 1764
  switch (yyn) {
  case 4: 
#line 325 "parse-datetime.y"
  pc->seconds = (yyvsp + 0)->timespec;
#line 326
  pc->timespec_seen = (_Bool)1;
#line 328
  break;

The problem is that the case statement starts with case 4 in the .c file on line 1765, but then switches and ends in the .y file.

There's no way to represent a range of code which starts in one file and ends in another. Goblint itself doesn't care too much, but none of the exposed outputs like SARIF or Gobpie have such general notion of ranges, because it's insane.
It's hard to blame anyone specifically for this because both the #line declarations are too loose and allow this and code-generation tools may not bother to super strictly inject additional change back to the outer file location just to allow downstream tools to represent such ranges.
(Although even then, truly representing the range is difficult, because it switches files twice...)

So I don't think there's much we can do about it, making joinLoc return just the start location (and leaving the end fields unknown, as is) is probably the best we can do in this case. Maybe worth just printing some kind of warning from CIL, that there was a range we couldn't join.