analyzer
analyzer copied to clipboard
Published
20 hours ago •
goblint
goblint
EvalAssert transformation crashes on some programs
When activating the EvalAssert transformation, goblint crashes on some programs when the transformation is performed.
In particular, this happens on all of the bench/coreutil programs. Example command-line:
./goblint --trans.activated '["assert"]' -v ../bench/coreutils/cksum_comb.c
Goblint will crash with the following stack trace (on master, b4c0057e1d82d9649b627af96f5237b2e4a8e1e0):
Stack trace
Fatal error: exception Not_found
Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 393, characters 21-36
Called from Goblint_lib__Control.AnalyzeCFG.analyze.solve_and_postprocess.ask.(fun) in file "src/framework/control.ml", line 582, characters 50-83
Called from Goblint_lib__Constraints.DeadBranchLifter.conv.(fun) in file "src/framework/constraints.ml", line 1095, characters 29-49
Called from Goblint_lib__MCP.MCP2.inner_ctx.(fun) in file "src/analyses/mCP.ml", line 341, characters 30-51
Called from Goblint_lib__Base.MainFunctor.priv_getg in file "src/analyses/base.ml", line 70, characters 32-49
Called from Goblint_lib__BasePriv.TracingPriv.read_global.getg in file "src/analyses/basePriv.ml", line 1654, characters 14-20
Called from Goblint_lib__BasePriv.PrecisionDumpPriv.read_global in file "src/analyses/basePriv.ml", line 1625, characters 12-42
Called from Goblint_lib__BasePriv.TracingPriv.read_global in file "src/analyses/basePriv.ml", line 1658, characters 12-42
Called from Goblint_lib__ValueDomain.ValueInvariant.deref_invariant in file "src/cdomains/valueDomain.ml", line 1295, characters 12-19
Called from Goblint_lib__ValueDomain.ValueInvariant.ad_invariant.(fun) in file "src/cdomains/valueDomain.ml", line 1249, characters 28-85
Called from Stdlib__Map.Make.fold in file "map.ml", line 321, characters 19-42
Called from Goblint_lib__ValueDomain.ValueInvariant.ad_invariant in file "src/cdomains/valueDomain.ml", line 1225, characters 16-1023
Called from Goblint_lib__Base.MainFunctor.query_invariant.(fun) in file "src/analyses/base.ml", line 1166, characters 32-47
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__Base.MainFunctor.query_invariant in file "src/analyses/base.ml", line 1164, characters 10-195
Called from Goblint_lib__MCP.MCP2.query'.f in file "src/analyses/mCP.ml", line 262, characters 29-43
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Goblint_lib__MCP.MCP2.query' in file "src/analyses/mCP.ml", line 287, characters 20-75
Called from Goblint_lib__Constraints.PathSensitive2.query.(fun) in file "src/framework/constraints.ml", line 1027, characters 60-65
Called from Goblint_lib__Constraints.PathSensitive2.fold'.k in file "src/framework/constraints.ml", line 1000, characters 10-37
Called from BatSet.Concrete.fold in file "src/batSet.ml", line 310, characters 35-56
Called from Goblint_lib__Constraints.DeadCodeLifter.lift_fun in file "src/framework/constraints.ml", line 410, characters 13-29
Called from Goblint_lib__EvalAssert.EvalAssert.visitor#vstmt.make_assert in file "src/transform/evalAssert.ml", line 58, characters 14-53
Called from Goblint_lib__EvalAssert.EvalAssert.visitor#vstmt.instrument_instructions.instrument_instructions in file "src/transform/evalAssert.ml", line 94, characters 17-35
Called from Goblint_lib__EvalAssert.EvalAssert.visitor#vstmt.instrument_instructions in file "src/transform/evalAssert.ml", line 101, characters 8-34
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5371, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5347, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5371, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5347, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenStmt.(fun).fBlock in file "src/cil.ml" (inlined), line 5334, characters 17-36
Called from GoblintCil__Cil.childrenStmt.(fun) in file "src/cil.ml", line 5371, characters 17-25
Called from GoblintCil__Cil.doVisit in file "src/cil.ml", line 5113, characters 40-60
Called from GoblintCil__Cil.visitCilStmt in file "src/cil.ml", line 5318, characters 12-64
Called from GoblintCil__Cil.mapNoCopy.aux in file "src/cil.ml", line 5121, characters 15-18
Called from GoblintCil__Cil.childrenBlock in file "src/cil.ml", line 5398, characters 15-39
Called from GoblintCil__Cil.childrenFunction in file "src/cil.ml", line 5561, characters 13-38
Called from GoblintCil__Cil.visitCilFunction in file "src/cil.ml", line 5541, characters 10-54
Called from GoblintCil__Cil.childrenGlobal in file "src/cil.ml", line 5577, characters 15-37
Called from GoblintCil__Cil.doVisitList in file "src/cil.ml", line 5145, characters 19-36
Called from GoblintCil__Cil.visitCilGlobal in file "src/cil.ml", line 5571, characters 12-58
Called from GoblintCil__Cil.visitCilFile.fGlob in file "src/cil.ml", line 5702, characters 16-36
Called from GoblintCil__Cil.visitCilFile in file "src/cil.ml", line 5709, characters 2-19
Called from Goblint_lib__EvalAssert.EvalAssert.transform in file "src/transform/evalAssert.ml", line 142, characters 4-39
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Goblint_lib__Control.AnalyzeCFG.analyze.solve_and_postprocess in file "src/framework/control.ml", line 592, characters 8-82
Called from Goblint_lib__Timeout.Unix.timeout in file "src/util/timeout.ml", line 6, characters 14-19
Called from Goblint_lib__Control.AnalyzeCFG.analyze in file "src/framework/control.ml", line 610, characters 17-100
Called from Goblint_lib__Control.analyze_loop.(fun) in file "src/framework/control.ml", line 686, characters 4-21
Called from Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 442, characters 10-46
Re-raised at Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 451, characters 8-49
Called from Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 140, characters 10-13
Re-raised at Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 146, 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
I guess this line https://github.com/goblint/analyzer/blob/b4c0057e1d82d9649b627af96f5237b2e4a8e1e0/src/framework/control.ml#L582 might require a fallback to bot. At least YAML witnesses have this for unknown reason: https://github.com/goblint/analyzer/blob/b4c0057e1d82d9649b627af96f5237b2e4a8e1e0/src/witness/yamlWitness.ml#L140
This indeed fixes the crash on at least cksum_comb.c and cp_comb.c (did not try the others yet). The question is, whether a fallback to bot is the right thing to do here, or whether one should go to top?
Since the local states that the transformations operate on are joined over all contexts, it seems possible that this leads to different globals to be queried than during the analysis -- so one may not have computed sound values for these.
That's a valid concern which is related to a GobCon topic from a year ago:
Join over all contexts/paths during postprocessing is unsound!
- For example, joining a singlethreaded and a multithreaded local state yields a multithreaded one, but in base CPA all the unpublished values remain
- Would need to call sync on the result, which removes unprotected from local state (a la branched thread creation)
- Sync has side-effects so cannot be called during postprocessing
I think we don't have a solution to this and we do such joins all over the place.
Might be worth just temporarily printing out the constraint variable names that it happens with to see if it could be a problem.
Might be worth just temporarily printing out the constraint variable names that it happens with to see if it could be a problem.
This produces a long, but mostly repeating list of globals. As far as I checked, those globals that cannot be found are functions that are passed as parameters to other functions (triple_compare etc.).
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_compare not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:dev_info_compare not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:src_to_dest_compare not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:free not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_free not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:src_to_dest_free not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_hash not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_hash_no_name not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:dev_info_hash not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:src_to_dest_hash not found during transformation, proceeding with bot. (copy.c:2557:7-2557:66)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_compare not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:dev_info_compare not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:src_to_dest_compare not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:free not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_free not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:src_to_dest_free not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_hash not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:triple_hash_no_name not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:dev_info_hash not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
[Warning][Unsound] Global either either unprotected or protected or FlagConfiguredTID: prefix * set:src_to_dest_hash not found during transformation, proceeding with bot. (copy.c:2549:5-2549:41)
I also looked at the variables with require a bottom default in YamlWitness and there the first ones are just the result of #819. Performing a MayAccessed query on a node, which didn't have any accesses, left it missing in the solution, which is expected.
So accessing such globals isn't necessarily due to the joined local state, but simply that invariant generation invokes some queries to write-only globals that weren't (and couldn't be) used during the analysis itself. Unless there's a specific case of unsoundness from this fallback, I'd assume it's harmless.