Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Incremental goblint crashes with Goblint_lib.Lattice.BotValue on some commits of chrony and zstd #955

Closed
jerhard opened this issue Dec 21, 2022 · 1 comment · Fixed by #957
Closed

Incremental goblint crashes with Goblint_lib.Lattice.BotValue on some commits of chrony and zstd #955

jerhard opened this issue Dec 21, 2022 · 1 comment · Fixed by #957
Labels
bug
Milestone
v2.2.0

Comments

@jerhard
Copy link
Member

jerhard commented Dec 21, 2022 •
edited
Loading

Goblint (branch interactive_benchmarking, 29d9c21), crashes on some incremental runs with Goblint_lib.Lattice.BotValue.

Goblint is observed to crash on chrony on one parent-child sequence of the efficiency runs with this exception.

Parent commit:
35220aac9dee4b7101dbd415dda34750e4998f7d
Command line:

./goblint --conf conf/custom/figlet.json -v --enable incremental.load --disable incremental.save ../chrony

Child commit:
e66f1df89d56983de0f7d1a70aa6e3ae0fe62730

./goblint --conf conf/custom/figlet.json -v --enable incremental.load --disable incremental.save ../chrony

The incremental analysis on the child fails with the following stack trace:

Exception backtrace 
Fatal error: exception Goblint_lib.Lattice.BotValue
Marked with transfer function at /home/goblint/sqlite-benchmarks/analyzer/lib/libc/stub/src/stdlib.c:11:7-11:43
Marked with transfer function at chrony/samplefilt.c:237:3-237:52
Marked with transfer function at chrony/samplefilt.c:410:3-410:29
Marked with transfer function at chrony/refclock.c:787:9-787:53
Marked with transfer function at chrony/sched.c:528:6-528:19
Marked with transfer function at chrony/sched.c:775:5-775:28
Marked with transfer function at chrony/main.c:683:3-683:17
Raised at Goblint_lib__Lattice.NoBotTop.bot in file "src/domains/lattice.ml", line 86, characters 15-29
Called from Goblint_lib__MapDomain.MapBot.pretty_diff.p in file "src/domains/mapDomain.ml", line 383, characters 31-44
Called from Goblint_lib__MapDomain.MapBot.pretty_diff.diff_key in file "src/domains/mapDomain.ml", line 390, characters 20-25
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 26-41
Called from Goblint_lib__MapDomain.MapBot.pretty_diff in file "src/domains/mapDomain.ml", line 394, characters 10-31
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from Goblint_lib__MapDomain.MapBot.pretty_diff.diff_key in file "src/domains/mapDomain.ml", line 390, characters 34-58
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Goblint_lib__MapDomain.MapBot.pretty_diff in file "src/domains/mapDomain.ml", line 394, characters 10-31
Called from Goblint_lib__MCPRegistry.DomListLattice.pretty_diff.f.(fun) in file "src/analyses/mCPRegistry.ml", line 307, characters 16-47
Called from Goblint_lib__GobList.fold_left3 in file "src/util/gobList.ml", line 15, characters 49-65
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from Goblint_lib__DisjointDomain.PairwiseSet.pretty_diff.(fun) in file "src/domains/disjointDomain.ml", line 309, characters 12-88
Called from BatSet.Concrete.fold in file "src/batSet.mlv", line 316, characters 35-56
Called from BatSet.Make.fold in file "src/batSet.mlv" (inlined), line 873, characters 21-54
Called from Goblint_lib__DisjointDomain.PairwiseSet.pretty_diff in file "src/domains/disjointDomain.ml", line 307, characters 6-260
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from Goblint_lib__PostSolver.Verify.complain_constraint in file "src/solvers/postSolver.ml", line 83, characters 13-208
Called from Goblint_lib__PostSolver.MakeIncr.post.one_constraint.get in file "src/solvers/postSolver.ml", line 204, characters 8-17
Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 7-17
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 742, characters 15-25
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 BatList.map.loop in file "src/batList.mlv", line 242, characters 28-33
Called from BatList.map in file "src/batList.mlv", line 245, characters 4-12
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 789, characters 19-44
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 4-105
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__PostSolver.MakeIncr.post.one_constraint in file "src/solvers/postSolver.ml", line 213, characters 16-25
Called from Goblint_lib__PostSolver.MakeIncr.post.one_constraint.get in file "src/solvers/postSolver.ml", line 204, characters 8-17
Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 7-17
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 742, characters 15-25
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 BatList.map in file "src/batList.mlv", line 244, characters 23-28
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 789, characters 19-44
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 4-105
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__PostSolver.MakeIncr.post.one_constraint in file "src/solvers/postSolver.ml", line 213, characters 16-25
Called from Goblint_lib__PostSolver.MakeIncr.post.one_constraint.get in file "src/solvers/postSolver.ml", line 204, characters 8-17
Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 7-17
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 742, characters 15-25
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 BatList.map in file "src/batList.mlv", line 244, characters 23-28
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 789, characters 19-44
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 4-105
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__PostSolver.MakeIncr.post.one_constraint in file "src/solvers/postSolver.ml", line 213, characters 16-25

(abbreviated stack trace)

There is also a warning about a not reached fix-point in the incremental run (see message below). However, there are some commits on zstd where the reluctant incremental analysis fails with this exception, but there is no fixpoint issue mentioned in the printout.

Fixpoint not reached 
Fixpoint not reached at node 10369496025 "return;" on /usr/include/x86_64-linux-gnu/bits/byteswap.h:44:1-48:1
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 16658 "tmp = __builtin_bswap32((int )__bsx);" on /usr/include/x86_64-linux-gnu/bits/byteswap.h:47:3-47:35
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 16659 "return ((unsigned int )tmp);" on /usr/include/x86_64-linux-gnu/bits/byteswap.h:47:3-47:35
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 16275 "filter->index = -1;" on chrony/samplefilt.c:176:3-176:21
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 16276 "filter->used = 0;" on chrony/samplefilt.c:177:3-177:19
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
Fixpoint not reached at node 16277 "! keep_last" on chrony/samplefilt.c:178:7-178:17
 Solver computed:
 bot
 Right-Hand-Side:
 Dead code
 Difference: Dead code instead of bot
@jerhard
Copy link
Member Author

jerhard commented Dec 21, 2022 •
edited
Loading

One pair of commits where this issue appears on zstd, without that a fixpoint issue is reported in the output (note, that the postsolver crashed, so it may also just not have been reported yet), is the following:

parent commit:
e7b0ae385e8ed68171b0c8024cf5649d6cfca7ef

parent command:
./goblint --conf conf/custom/zstd-race.json -v --disable incremental.load --enable incremental.save ../zstd

child commit:
9985e10fdaec1d3d49cb20ee78ee8a746467acb8

child command:
./goblint --conf conf/custom/zstd-race-incrpostsolver.json -v --enable incremental.load --disable incremental.save --enable incremental.reluctant.enabled ../zstd

Before running goblint, the compile db has to be created in the zstd repository with running this script.

Stack trace 
Fatal error: exception Goblint_lib.Lattice.BotValue
Marked with transfer function at zstd/lib/decompress/zstd_decompress.c:324:9-324:29
Marked with transfer function at zstd/lib/decompress/zstd_decompress.c:1571:5-1571:30
Marked with transfer function at zstd/programs/fileio.c:2046:19-2046:52
Raised at Goblint_lib__Lattice.NoBotTop.bot in file "src/domains/lattice.ml", line 86, characters 15-29
Called from Goblint_lib__MapDomain.MapBot.pretty_diff.p in file "src/domains/mapDomain.ml", line 383, characters 31-44
Called from Goblint_lib__MapDomain.MapBot.pretty_diff.diff_key in file "src/domains/mapDomain.ml", line 390, characters 20-25
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 26-41
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 26-41
Called from Goblint_lib__MapDomain.MapBot.pretty_diff in file "src/domains/mapDomain.ml", line 394, characters 10-31
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from Goblint_lib__MapDomain.MapTop.pretty_diff.diff_key in file "src/domains/mapDomain.ml", line 454, characters 34-58
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 26-41
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 26-41
Called from Goblint_lib__MapDomain.MapTop.pretty_diff in file "src/domains/mapDomain.ml", line 458, characters 10-31
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from Goblint_lib__MapDomain.MapBot.pretty_diff.diff_key in file "src/domains/mapDomain.ml", line 390, characters 34-58
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Goblint_lib__MapDomain.MapBot.pretty_diff in file "src/domains/mapDomain.ml", line 394, characters 10-31
Called from Goblint_lib__MCPRegistry.DomListLattice.pretty_diff.f.(fun) in file "src/analyses/mCPRegistry.ml", line 307, characters 16-47
Called from Goblint_lib__GobList.fold_left3 in file "src/util/gobList.ml", line 15, characters 49-65
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from Goblint_lib__DisjointDomain.PairwiseSet.pretty_diff.(fun) in file "src/domains/disjointDomain.ml", line 309, characters 12-88
Called from BatSet.Concrete.fold in file "src/batSet.mlv", line 316, characters 35-56
Called from BatSet.Make.fold in file "src/batSet.mlv" (inlined), line 873, characters 21-54
Called from Goblint_lib__DisjointDomain.PairwiseSet.pretty_diff in file "src/domains/disjointDomain.ml", line 307, characters 6-260
Called from GoblintCil__Pretty.gprintf.collect.(fun) in file "src/ocamlutil/pretty.ml", line 742, characters 35-52
Called from Goblint_lib__PostSolver.Verify.complain_constraint in file "src/solvers/postSolver.ml", line 83, characters 13-208
Called from Goblint_lib__PostSolver.MakeIncr.post.one_constraint.get in file "src/solvers/postSolver.ml", line 204, characters 8-17
Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 7-17
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 742, characters 15-25
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 BatList.map in file "src/batList.mlv", line 244, characters 23-28
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 778, characters 27-47
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 4-105
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__PostSolver.MakeIncr.post.one_constraint in file "src/solvers/postSolver.ml", line 213, characters 16-25
Called from Goblint_lib__PostSolver.MakeIncr.post.one_constraint.get in file "src/solvers/postSolver.ml", line 204, characters 8-17
Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv" (inlined), line 77, characters 20-25
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 7-17
Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 742, characters 15-25
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 BatList.map in file "src/batList.mlv", line 244, characters 23-28
Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 778, characters 27-47
Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 1012, characters 4-105
Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15

@jerhard jerhard added the bug label Dec 21, 2022
@stilscher stilscher mentioned this issue Dec 21, 2022
Merged
@sim642 sim642 added this to the v2.2.0 milestone Apr 5, 2023
@sim642 sim642 mentioned this issue Sep 13, 2023
Closed
sim642 added a commit to sim642/opam-repository that referenced this issue Sep 13, 2023
@sim642
[new release] goblint (2.2.0)
eb80bce 
CHANGES:

* Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019).
* Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016).
* Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082).
* Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073).
* Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048).
* Add affine equalities analysis (goblint/analyzer#592).
* Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114).
* Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979).
* Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952).
* Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124).
* Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777).
* Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031).
* Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078).
* Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091).
* Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027).
* Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053).
* Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138).
* Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
v2.2.0
Development

Successfully merging a pull request may close this issue.

Fix: not found global should be added not removed goblint/analyzer
2 participants
@sim642 @jerhard