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
michael-schwarz merged 13 commits into from
Jul 18, 2022
Merged

Cleanup reporting of dead code #785

Show file tree
Hide file tree
Changes from 3 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 @@ -68,7 +68,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#53c6fa8beaf69619e86d83ff05eb4521aacd356b" ]
# 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 @@ -124,7 +124,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#53c6fa8beaf69619e86d83ff05eb4521aacd356b"
]
[
"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#53c6fa8beaf69619e86d83ff05eb4521aacd356b" ]
# 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
10 changes: 6 additions & 4 deletions src/framework/control.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,19 +151,21 @@ struct
let warn_file f = StringMap.iter (warn_func f) in
if get_bool "dbg.print_dead_code" 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%s.\n" (if GobConfig.get_bool "alldeadcode" then "" else "(there might still be dead code removed by CIL, try running with --enable alldeadcode to see all) ") (* TODO https://github.com/goblint/analyzer/issues/94 *)
else (
StringMap.iter warn_file !dead_lines; (* populates count by side-effect *)
let total_dead = !count + uncalled_fn_loc in
printf "Found dead code on %d line%s%s!\n" total_dead (if total_dead>1 then "s" else "") (if uncalled_fn_loc > 0 then Printf.sprintf " (including %d in uncalled functions)" uncalled_fn_loc else "")
printf "Found dead code on %d line%s%s!\n" total_dead (if total_dead>1 then "s" else "") (if uncalled_fn_loc > 0 then Printf.sprintf " (including %d in uncalled functions)" uncalled_fn_loc else "");
(if not @@ GobConfig.get_bool "alldeadcode" then printf "There might still be more dead code removed by CIL, try running with --enable alldeadcode to see all.\n")
);
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 (
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 := not (GobConfig.get_bool "alldeadcode");
lowerConstants := true;
Mergecil.ignore_merge_conflicts := true;
Mergecil.merge_inlines := get_bool "cil.merge.inlines";
Expand Down
7 changes: 7 additions & 0 deletions src/util/options.schema.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,13 @@
"type": "integer",
"default": 1
},
"alldeadcode": {
"title": "alldeadcode",
"description":
"Report on all dead code, disables removing of dead branches over constants in CIL",
"type": "boolean",
"default": false
},
"goblint-dir": {
"title": "goblint-dir",
"description": "Directory used for intermediate data.",
Expand Down