Skip to content

Cleanup reporting of dead code #785

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

Merged
merged 13 commits into from
Jul 18, 2022
Merged

Cleanup reporting of dead code #785

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
36f4dc5
Include message about CIL inserted branches
michael-schwarz Jul 15, 2022
9e754a6
Make message weaker so it still applies
michael-schwarz Jul 15, 2022
924c219
Add `alldeadcode` option
michael-schwarz Jul 15, 2022
7eaf367
Bump goblint-cil
michael-schwarz Jul 18, 2022
57fcc31
Remove `alldeadcode` and enable it by default
michael-schwarz Jul 18, 2022
884c8dd
Toggle default for `removeBranchingOnConstants`, bump goblint-cil
michael-schwarz Jul 18, 2022
15186b0
Rename and simplify dead-code options
michael-schwarz Jul 18, 2022
f7154da
Fix outdated comment
michael-schwarz Jul 18, 2022
b2e38e9
push gobview
michael-schwarz Jul 18, 2022
be1b4db
Merge branch 'master' into issue_94
michael-schwarz Jul 18, 2022
4d998c4
Use DeadBranchLifter only when `ana.dead-code.branches` is enabled
michael-schwarz Jul 18, 2022
9f76a64
Bump goblint-cil
michael-schwarz Jul 18, 2022
ab670af
Remove setting of dead code options for HTML / SARIF
michael-schwarz Jul 18, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion goblint.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
# on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
# also remember to generate/adjust goblint.opam.locked!
pin-depends: [
[ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#c150579b9bcfe60c4f441a9f5ac0122c2501a88c" ]
[ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#54b0c220a9cea4213ff596eadff877a6ec9b00fb" ]
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
# quoter workaround reverted for release, so no pin needed
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.locked
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ version: "dev"
pin-depends: [
[
"goblint-cil.1.8.2"
"git+https://github.com/goblint/cil.git#c150579b9bcfe60c4f441a9f5ac0122c2501a88c"
"git+https://github.com/goblint/cil.git#54b0c220a9cea4213ff596eadff877a6ec9b00fb"
]
[
"apron.v0.9.13"
Expand Down
2 changes: 1 addition & 1 deletion goblint.opam.template
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
# also remember to generate/adjust goblint.opam.locked!
pin-depends: [
[ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#c150579b9bcfe60c4f441a9f5ac0122c2501a88c" ]
[ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#54b0c220a9cea4213ff596eadff877a6ec9b00fb" ]
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
# quoter workaround reverted for release, so no pin needed
Expand Down
2 changes: 1 addition & 1 deletion gobview
Open in desktop
Submodule gobview updated 1 files
+1 −1 public/goblint/config.json
10 changes: 5 additions & 5 deletions scripts/update_suite.rb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -367,7 +367,7 @@ def run_testset (testset, cmd, starttime)

def run
filename = File.basename(@path)
cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
starttime = Time.now
run_testset(@testset, cmd, starttime)
end
Expand Down Expand Up @@ -428,8 +428,8 @@ def create_test_set(lines)

def run
filename = File.basename(@path)
cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable dbg.print_dead_code --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
starttime = Time.now
run_testset(@testset_incr, cmd, starttime)
# apply patch
Expand Down Expand Up @@ -472,8 +472,8 @@ def create_test_set(lines)
end
def run ()
filename = File.basename(@path)
cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable dbg.print_dead_code --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
starttime = Time.now
run_testset(@testset, cmd1, starttime)
run_testset(@testset, cmd2, starttime)
Expand Down
19 changes: 10 additions & 9 deletions src/framework/control.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
|> lift (get_bool "ana.sv-comp.enabled") (module HashconsLifter)
|> lift (get_bool "ana.sv-comp.enabled") (module WitnessConstraints.PathSensitive3)
|> lift (not (get_bool "ana.sv-comp.enabled")) (module PathSensitive2)
|> lift (get_bool "dbg.print_dead_code") (module DeadBranchLifter)
|> lift (get_bool "ana.dead-code.branches") (module DeadBranchLifter)
|> lift true (module DeadCodeLifter)
|> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
|> lift (get_int "dbg.limit.widen" > 0) (module LimitLifter)
Expand Down Expand Up @@ -82,7 +82,7 @@ struct
let dead_locations : unit Deadcode.Locmap.t = Deadcode.Locmap.create 10 in
let module NH = Hashtbl.Make (Node) in
let live_nodes : unit NH.t = NH.create 10 in
let count = ref 0 in (* Is only populated if "dbg.print_dead_code" is true *)
let count = ref 0 in (* Is only populated if "ana.dead-code.lines" or "ana.dead-code.branches" is true *)
let module StringMap = BatMap.Make (String) in
let open BatPrintf in
let live_lines = ref StringMap.empty in
Expand Down Expand Up @@ -149,9 +149,9 @@ struct
M.msg_group Warning ~category:Deadcode "Function '%s' has dead code" f msgs
in
let warn_file f = StringMap.iter (warn_func f) in
if get_bool "dbg.print_dead_code" then (
if get_bool "ana.dead-code.lines" then (
if StringMap.is_empty !dead_lines
then printf "No lines with dead code found by solver (there might still be dead code removed by CIL).\n" (* TODO https://github.com/goblint/analyzer/issues/94 *)
then printf "No lines with dead code found by solver.\n"
else (
StringMap.iter warn_file !dead_lines; (* populates count by side-effect *)
let total_dead = !count + uncalled_fn_loc in
Expand All @@ -160,13 +160,14 @@ struct
printf "Total lines (logical LoC): %d\n" (live_count + !count + uncalled_fn_loc); (* We can only give total LoC if we counted dead code *)
);
let str = function true -> "then" | false -> "else" in
let cilinserted = function true -> "(possibly inserted by CIL) " | false -> "" in
let report tv (loc, dead) =
match dead, Deadcode.Locmap.find_option Deadcode.dead_branches_cond loc with
| true, Some exp -> M.warn ~loc ~category:Deadcode ~tags:[CWE (if tv then 570 else 571)] "the %s branch over expression '%a' is dead" (str tv) d_exp exp
| true, None -> M.warn ~loc ~category:Deadcode ~tags:[CWE (if tv then 570 else 571)] "an %s branch is dead" (str tv)
| true, Some exp -> M.warn ~loc ~category:Deadcode ~tags:[CWE (if tv then 570 else 571)] "the %s branch %sover expression '%a' is dead" (str tv) (cilinserted loc.synthetic) d_exp exp
| true, None -> M.warn ~loc ~category:Deadcode ~tags:[CWE (if tv then 570 else 571)] "an %s branch %sis dead" (str tv) (cilinserted loc.synthetic)
Comment on lines +166 to +167
Copy link
Member

@sim642 sim642 Jul 16, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if loc.synthetic is the appropriate thing to base this output on, because the location being synthetic doesn't necessarily correspond to an If that CIL created. In some cases it does, e.g. in a && b, when b has a constant value, then there's a dead branch in that CIL-created If and its location is synthetic because there's no program point in the original source code between the evaluation of a and b, which is why the location is synthetic.

I haven't checked with this PR, but I'm suspicious about cases like the following:

  • Again in a && b, when a has a constant value and there's a dead branch in that CIL-created If, then there is a program point (right before the whole expression) where an invariant assert (which the synthetic locations are for) about a could be inserted. So that location needn't be synthetic, it might currently be since synthetic locations are probably assigned more crudely than necessary, but if that is ever improved, then the output about a dead branch would actually become more wrong.
  • When for loops are transformed by CIL, the branching node (for which the branching expression literally exists in the original source code!) has a synthetic location, because an (assert) statement cannot be inserted between the for initializer and condition.

Maybe it's something we should address separately in the future, for example by adding synthetic fields to CIL statements (such that it's explicit which Ifs were added by CIL) and variables (such that it's explicit which temporaries, etc it came up with) instead of semi-heuristics for these.

Copy link
Member Author

@michael-schwarz michael-schwarz Jul 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that sounds like a good idea. However, I'd think that we should do this in an new issue & PR.

| _ -> ()
in
if get_bool "dbg.print_dead_code" then (
if get_bool "ana.dead-code.branches" then (
let by_fst (a,_) (b,_) = Stdlib.compare a b in
Deadcode.Locmap.to_list Deadcode.dead_branches_then |> List.sort by_fst |> List.iter (report true) ;
Deadcode.Locmap.to_list Deadcode.dead_branches_else |> List.sort by_fst |> List.iter (report false) ;
Expand Down Expand Up @@ -549,7 +550,7 @@ struct
| GFun (fn, loc) when is_bad_uncalled fn.svar loc->
let cnt = Cilfacade.countLoc fn in
uncalled_dead := !uncalled_dead + cnt;
if get_bool "dbg.uncalled" then
if get_bool "ana.dead-code.functions" then
M.warn ~loc ~category:Deadcode "Function \"%a\" will never be called: %dLoC" CilType.Fundec.pretty fn cnt
| _ -> ()
in
Expand Down Expand Up @@ -624,7 +625,7 @@ struct
let local_xml = solver2source_result lh in

let liveness =
if get_bool "dbg.print_dead_code" then
if get_bool "ana.dead-code.lines" || get_bool "ana.dead-code.branches" then
print_dead_code local_xml !uncalled_dead
else
fun _ -> true (* TODO: warn about conflicting options *)
Expand Down
2 changes: 0 additions & 2 deletions src/maingoblint.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,15 +51,13 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy (
set_string "outfile" "result";
if get_string "exp.g2html_path" = "" then
set_string "exp.g2html_path" (Fpath.to_string exe_dir);
set_bool "dbg.print_dead_code" true;
set_bool "exp.cfgdot" true;
set_bool "g2html" true;
set_string "result" "fast_xml"
in
let configure_sarif () =
if (get_string "outfile" = "") then
set_string "outfile" "goblint.sarif";
set_bool "dbg.print_dead_code" true;
set_string "result" "sarif"
in
let complete_option_value option s =
Expand Down
1 change: 1 addition & 0 deletions src/util/cilfacade.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ let isCharType = function

let init () =
initCIL ();
removeBranchingOnConstants := false;
lowerConstants := true;
Mergecil.ignore_merge_conflicts := true;
Mergecil.merge_inlines := get_bool "cil.merge.inlines";
Expand Down
37 changes: 25 additions & 12 deletions src/util/options.schema.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -881,6 +881,31 @@
}
},
"additionalProperties": false
},
"dead-code" : {
"title": "ana.dead-code",
"type": "object",
"properties": {
"lines": {
"title": "ana.dead-code.lines",
"description": "Print information about lines of dead code.",
"type": "boolean",
"default": true
},
"branches": {
"title": "ana.dead-code.branches",
"description": "Print information about dead branches.",
"type": "boolean",
"default": true
},
"functions": {
"title": "ana.dead-code.functions",
"description": "Print information about dead (uncalled) functions.",
"type": "boolean",
"default": true
}
},
"additionalProperties": false
}
},
"additionalProperties": false
Expand Down Expand Up @@ -1373,12 +1398,6 @@
},
"additionalProperties": false
},
"uncalled": {
"title": "dbg.uncalled",
"description": "Display uncalled functions.",
"type": "boolean",
"default": true
},
"dump": {
"title": "dbg.dump",
"description": "Dumps the results to the given path",
Expand Down Expand Up @@ -1433,12 +1452,6 @@
"type": "boolean",
"default": false
},
"print_dead_code": {
"title": "dbg.print_dead_code",
"description": "Print information about dead code",
"type": "boolean",
"default": false
},
Copy link
Member

@sim642 sim642 Jul 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just as a post-merge note: the renaming of dbg.print_dead_code and dbg.uncalled will probably require a bunch of renaming in the bench repo as well.

Copy link
Member Author

@michael-schwarz michael-schwarz Jul 18, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True!

"slice": {
"title": "dbg.slice",
"type": "object",
Expand Down
4 changes: 2 additions & 2 deletions tests/regression/56-witness/03-int-log-short.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
version: heads/int-log-0-g5f8473450-dirty
command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''03-int-log-short.c''
''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set''
''printstats'' ''true'' ''--enable'' ''dbg.print_dead_code'' ''--set'' ''goblint-dir''
''printstats'' ''true'' ''--set'' ''goblint-dir''
''.goblint-56-03'''
task:
input_files:
Expand Down Expand Up @@ -37,7 +37,7 @@
version: heads/int-log-0-g5f8473450-dirty
command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''03-int-log-short.c''
''--enable'' ''witness.yaml.enabled'' ''--set'' ''dbg.debug'' ''true'' ''--set''
''printstats'' ''true'' ''--enable'' ''dbg.print_dead_code'' ''--set'' ''goblint-dir''
''printstats'' ''true'' ''--set'' ''goblint-dir''
''.goblint-56-03'''
task:
input_files:
Expand Down
2 changes: 1 addition & 1 deletion tests/regression/56-witness/04-base-priv-sync-prune.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
command_line: '''/home/simmo/dev/goblint/sv-comp/goblint/goblint'' ''04-base-priv-sync-prune.c''
''--enable'' ''ana.int.interval'' ''--enable'' ''witness.yaml.enabled'' ''--set''
''witness.yaml.path'' ''04-base-priv-sync-prune.yml'' ''--set'' ''dbg.debug''
''true'' ''--set'' ''printstats'' ''true'' ''--enable'' ''dbg.print_dead_code''
''true'' ''--set'' ''printstats'' ''true''
''--set'' ''goblint-dir'' ''.goblint-56-03'''
task:
input_files:
Expand Down