Incremental analysis crashes when patch introduces only call to `longjmp`

[J2000A]

During the implementation for my bachelor thesis about generating test cases for the incremental analysis we encountered a problem: The incremental analysis crashes in some cases, when using longjump().

This error can be reproduced with the following example:

Initial Program inital.c (Mutated Regression Test 68/48):

#include<setjmp.h>
jmp_buf env_buffer;

int main() { return 0; /* [MUTATION][RFB] Stripped function of its body */ }

Program for incremental analysis incremental.c (Regression Test 68/48):

#include<setjmp.h>
jmp_buf env_buffer;

int main() {
  longjmp(env_buffer, 1); //WARN
}

Reproduce by calling
./goblint inital.c --enable incremental.save
./goblint incremental.c --enable incremental.load -v

Fatal error: exception Invalid_argument("List.iter2: list lengths differ") seems to be the root cause of the crash.

The full output should be:

2023-07-07 09:27:36
'./goblint' '../bench/incremental-test-generation/temp/p_0.c' '--enable' 'incremental.load' '-v'
Custom include dirs:
  1. /home/jonas/BA/Goblint-Repo/analyzer/lib/sv-comp/stub/include (exists=false)
  2. /home/jonas/BA/Goblint-Repo/analyzer/lib/goblint/stub/include (exists=false)
  3. /home/jonas/BA/Goblint-Repo/analyzer/lib/linux/stub/include (exists=true)
  4. /home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/include (exists=true)
  5. /home/jonas/BA/Goblint-Repo/analyzer/lib/sv-comp/runtime/include (exists=false)
  6. /home/jonas/BA/Goblint-Repo/analyzer/lib/goblint/runtime/include (exists=true)
  7. /home/jonas/BA/Goblint-Repo/analyzer/lib/linux/runtime/include (exists=false)
  8. /home/jonas/BA/Goblint-Repo/analyzer/lib/libc/runtime/include (exists=false)
  9. /home/jonas/BA/Goblint-Repo/analyzer/lib/sv-comp/stub/src (exists=true)
  10. /home/jonas/BA/Goblint-Repo/analyzer/lib/goblint/stub/src (exists=false)
  11. /home/jonas/BA/Goblint-Repo/analyzer/lib/linux/stub/src (exists=false)
  12. /home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/src (exists=true)
Preprocessing files.
Preprocessor cpp: is_bad=false
'cpp' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/linux/stub/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/goblint/runtime/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/sv-comp/stub/src' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/src' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/src/pthread.c' '-o' '.goblint/preprocessed/pthread.i'
'cpp' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/linux/stub/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/goblint/runtime/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/sv-comp/stub/src' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/src' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/src/stdlib.c' '-o' '.goblint/preprocessed/stdlib.i'
'cpp' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/linux/stub/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/goblint/runtime/include' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/sv-comp/stub/src' '-I' '/home/jonas/BA/Goblint-Repo/analyzer/lib/libc/stub/src' '../bench/incremental-test-generation/temp/p_0.c' '-o' '.goblint/preprocessed/p_0.i'
Parsing files.
Frontc is parsing .goblint/preprocessed/p_0.i
Converting CABS->CIL
Frontc is parsing .goblint/preprocessed/pthread.i
Converting CABS->CIL
Frontc is parsing .goblint/preprocessed/stdlib.i
Converting CABS->CIL
Pre-merging (0) .goblint/preprocessed/p_0.i
Pre-merging (1) .goblint/preprocessed/pthread.i
Pre-merging (2) .goblint/preprocessed/stdlib.i
Final merging phase (0): .goblint/preprocessed/p_0.i
Final merging phase (1): .goblint/preprocessed/pthread.i
Final merging phase (2): .goblint/preprocessed/stdlib.i
Constructors: 
Adding constructors to: main
Unmarshalling /home/jonas/BA/Goblint-Repo/analyzer/incremental_data/results/analysis.data... If type of content changed, this will result in a segmentation fault!
longjmp -> enabling longjmp analyses "activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceLongjmp, poisonVariables, expsplit, vla"
And now...  the Goblin!
Startfuns: [main]
Exitfuns: []
Otherfuns: []
Activated analyses: expRelation, base, threadid, threadflag, threadreturn, escape, mutexEvents, mutex, access, race, mallocWrapper, mhp, assert, activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceLongjmp, poisonVariables, expsplit, vla
Activated transformations: 
Generating the control flow graph.

[Error][Analyzer] About to crash!

vars = 0    evals = 0    narrow_reuses = 0

Timings:
cfgF (bindings=40 buckets=128 max_length=1 histo=88,40 load=0.312500), cfgB (bindings=40 buckets=128 max_length=2 histo=89,38,1 load=0.312500)
                                  cputime   walltime   allocated   count
Default                            0.070s     0.070s     20.21MB      1×
  preprocess                         0.043s     0.039s      0.01MB      1×
  FrontC                             0.009s     0.009s      4.22MB      3×
  Cabs2cil                           0.005s     0.005s      3.96MB      3×
  mergeCIL                           0.005s     0.005s      2.56MB      1×
  compareCilFiles                    0.004s     0.004s      4.40MB      1×
  analysis                           0.002s     0.002s      1.89MB      1×
    createCFG                          0.001s     0.001s      0.17MB      1×
      handle                             0.001s     0.001s      0.06MB      4×
      iter_connect                       0.001s     0.001s      0.07MB      4×
        computeSCCs                        0.001s     0.001s      0.05MB      4×

Fatal error: exception Invalid_argument("List.iter2: list lengths differ")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from Goblint_lib__Control.AnalyzeCFG.analyze in file "src/framework/control.ml", line 350, characters 4-21
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from Goblint_lib__Control.analyze_loop.(fun) in file "src/framework/control.ml", line 784, characters 4-77
Called from Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 533, characters 10-46
Re-raised at Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 546, characters 8-49
Called from Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 141, characters 10-13
Re-raised at Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 147, characters 6-13
Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 62, characters 6-35
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

The regression test 68/46 can reproduce the same crash with the equivalent mutation.

[michael-schwarz]

Thank you for reporting this issue and the detailed report: The problem seems to be that you are introducing the only usage of longjmp in this program.

Thus, the autotuner enables additional analyses which normally are disabled: (see #1019)

analyzer/src/goblint.ml

Lines 59 to 60 in 3af00a8

	(* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *)
	AutoTune.activateLongjmpAnalysesWhenRequired ();

analyzer/src/autoTune.ml

Lines 199 to 211 in 3af00a8

	(* This is run independent of the autotuner being enabled or not to be sound in the presence of setjmp/longjmp *)
	(* It is done this way around to allow enabling some of these analyses also for programs without longjmp *)
	let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceLongjmp"; "poisonVariables"; "expsplit"; "vla"]
	let activateLongjmpAnalysesWhenRequired () =
	let isLongjmp = function
	| LibraryDesc.Longjmp _ -> true
	| _ -> false
	in
	if hasFunction isLongjmp then (
	print_endline @@ "longjmp -> enabling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\"";
	enableAnalyses longjmpAnalyses;
	)

In the presence of incremental usage which may insert such idioms, it is probably required to enable these analyses manually already for the non-incremental run. Does this fix the issue?

I would suggest outputting a warning if the autotuner enables these analyses in an incremental run, but you should probably discuss this with @stilscher.

[michael-schwarz]

The other option would be to always enable the longjmp analyses when storing or reading incremental data, but I don't think that's desirable performance-wise?

CC @jerhard

[J2000A]

Thank you for reporting this issue and the detailed report: The problem seems to be that you are introducing the only usage of longjmp in this program.

Thus, the autotuner enables additional analyses which normally are disabled: (see #1019)

analyzer/src/goblint.ml

Lines 59 to 60 in 3af00a8

	(* This is run independant of the autotuner being enabled or not be sound for programs with longjmp *)
	AutoTune.activateLongjmpAnalysesWhenRequired ();

analyzer/src/autoTune.ml

Lines 199 to 211 in 3af00a8

	(* This is run independent of the autotuner being enabled or not to be sound in the presence of setjmp/longjmp *)
	(* It is done this way around to allow enabling some of these analyses also for programs without longjmp *)
	let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceLongjmp"; "poisonVariables"; "expsplit"; "vla"]
	let activateLongjmpAnalysesWhenRequired () =
	let isLongjmp = function
	| LibraryDesc.Longjmp _ -> true
	| _ -> false
	in
	if hasFunction isLongjmp then (
	print_endline @@ "longjmp -> enabling longjmp analyses \"" ^ (String.concat ", " longjmpAnalyses) ^ "\"";
	enableAnalyses longjmpAnalyses;
	)

In the presence of incremental usage which may insert such idioms, it is probably required to enable these analyses manually already for the non-incremental run. Does this fix the issue?

I would suggest outputting a warning if the autotuner enables these analyses in an incremental run, but you should probably discuss this with @stilscher.

Thanks @michael-schwarz for your explanation. You are right. Adding // PARAM: --set ana.activated ["'activeLongjmp'","'activeSetjmp'","'taintPartialContexts'","'modifiedSinceLongjmp'","'poisonVariables'","'expsplit'","'vla'"] fixes the issue. I will discuss this with @stilscher.

[J2000A]

Idea for writing out a warning (discussed with @stilscher):

• Store which analysis were activated when marshalling (Relevant code lines: control.ml:515,518,541,765, serialize.ml data_querry)
• When using the incremental analysis load the previously activated analysis and compare them to the currently activated analyses. When they do not match print a prominent warning. One might also want to print a warning when the longjump analysis was activated, that the user is required to activate the longjump analysis also in the non-incremental run. However, it was not clear yet, where in the code this could be implemented. (Relevant code lines: control.ml:343, maingoblint.ml:529)