dbg.timeout somtimes not respected

[michael-schwarz]

For benchmarking in my dissertation, I realized that dbg.timeout does not seem to be respected always. This was observed on the phpsys task from Concrat.

/home/goblint/michael-schwarz-dissertation/analyzer/goblint --conf /home/goblint/michael-schwarz-dissertation/analyzer/conf/traces.json --set dbg.timeout 900 --set ana.base.privatization mine-W phpspy.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump /home/goblint/michael-schwarz-dissertation/bench/bench_result/phpspy.mine-W.prec

runs for north of 5h despite a 15min timeout being set.

It still regularly dumps statistics and the number of evals goes up so it should not be a case where some inner function is stuck forever

[Info] runtime: 05:25:49.543
[Info] vars: 273065, evals: 797399

[Debug] |rho|=273065
[Debug] |stable|=266244
[Debug] |infl|=273053
[Debug] |wpoint|=17
[Debug] |sides|=12676
[Debug] |side_dep|=0
[Debug] |side_infl|=0
[Debug] |var_messages|=0
[Debug] |rho_write|=0
[Debug] |dep|=249982
[Info] |called|=45
[Debug] Found 9818 contexts for 208 functions. Top 5 functions:
[Debug] 2431	contexts for L:entry state of copy_proc_mem (7233) on phpspy.c:7826:1-7861:1
[Debug] 543	contexts for L:entry state of callgrind_sort_callees (7380) on phpspy.c:19662:1-19670:1
[Debug] 272	contexts for L:entry state of event_handler_fout_snprintf (7371) on phpspy.c:18129:1-18167:1
[Debug] 240	contexts for L:entry state of log_error (1472) on phpspy.c:8044:1-8055:1
[Debug] 235	contexts for L:entry state of event_handler_callgrind (1466) on phpspy.c:18204:1-18251:1

Memory statistics: total=46955584.81MB, max=23249.31MB, minor=46946711.20MB, major=1017657.58MB, promoted=1008783.97MB
    minor collections=22387551  major collections=423 compactions=0


[Info] runtime: 05:25:59.610
[Info] vars: 273065, evals: 797407

[Debug] |rho|=273065
[Debug] |stable|=266245
[Debug] |infl|=273053
[Debug] |wpoint|=13
[Debug] |sides|=12676
[Debug] |side_dep|=0
[Debug] |side_infl|=0
[Debug] |var_messages|=0
[Debug] |rho_write|=0
[Debug] |dep|=249982
[Info] |called|=22
[Debug] Found 9818 contexts for 208 functions. Top 5 functions:
[Debug] 2431	contexts for L:entry state of copy_proc_mem (7233) on phpspy.c:7826:1-7861:1
[Debug] 543	contexts for L:entry state of callgrind_sort_callees (7380) on phpspy.c:19662:1-19670:1
[Debug] 272	contexts for L:entry state of event_handler_fout_snprintf (7371) on phpspy.c:18129:1-18167:1
[Debug] 240	contexts for L:entry state of log_error (1472) on phpspy.c:8044:1-8055:1
[Debug] 235	contexts for L:entry state of event_handler_callgrind (1466) on phpspy.c:18204:1-18251:1

Memory statistics: total=46978496.25MB, max=23249.31MB, minor=46969556.83MB, major=1018355.54MB, promoted=1009416.12MB
    minor collections=22398445  major collections=423 compactions=0

Complete logs up to the point where I killed it: phpspy.mine-W.txt

[sim642]

This might be related to #1221.

[sim642]

My theory about OCaml signal handling poll points probably isn't the cause because dbg.solver-stats-interval does properly trigger regularly.

Since dbg.timeout is implemented using an Timeout.Timeout exception, it could be that something is eating the exception before it reaches Goblint's main. I've insisted that no new catch-all exception handlers be introduced, but there are god knows how many still around Goblint and each one could be the culprit. And it's not easy to find them all...

[sim642]

Based on #1435 (comment), I'm not completely certain that the root issue has been solved: at that point the main culprits should've been avoided already.
I suspect the robustness addition from 52f3695 might've just helped to make it look like it's working.