Merge pull request #785 from goblint/issue_94

Cleanup reporting of dead code

Author: michael-schwarz

goblint.opam

@@ -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#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

goblint.opam.locked

@@ -121,7 +121,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"

goblint.opam.template

@@ -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

gobview

@@ -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
@@ -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
@@ -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)

scripts/update_suite.rb

@@ -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)
@@ -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
@@ -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
@@ -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)
       | _ -> ()
     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) ;
@@ -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
@@ -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 *)

src/framework/control.ml

@@ -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 =

src/maingoblint.ml

@@ -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";

src/util/cilfacade.ml

@@ -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
@@ -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",
@@ -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
-        },
         "slice": {
           "title": "dbg.slice",
           "type": "object",

src/util/options.schema.json

@@ -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:
@@ -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: