Run dead code analysis with reanalyze #737

sim642 · 2022-05-16T08:35:38Z

This is the result of me trying out reanalyze on our codebase. Instead of a local unused check based on signatures (which we rarely have) that the OCaml compiler has, this attempts to perform a global dead code analysis.

I manually went through all of its warnings and did one of the following for each one:

Removed the dead code.
Added a TODO for potentially significant code, which should maybe be used. Feel free to voice your opinions.
Ignored the warning for false positives, significant code to keep or ARINC/spec analysis (which I didn't want to unnecessarily touch).

TODO

Merge Run dead code analysis with reanalyze gobview#13.
Update git submodule after Run dead code analysis with reanalyze gobview#13 merge.

sim642 · 2022-05-16T08:41:47Z

Looks like I'll have to open a PR for Gobview as well. Will do that in a moment.

src/analyses/condVars.ml

src/analyses/base.ml

src/analyses/mCP.ml

src/cdomains/listDomain.ml

src/analyses/uninit.ml

michael-schwarz · 2022-05-17T07:24:05Z

src/analyses/varEq.ml

@@ -119,6 +119,7 @@ struct
      | _ -> false

  (* kill predicate for must-equality kind of analyses*)
+  (* TODO: why unused? how different from below? *)


They seem to be virtually identical, except the one below being a fair bit more chaotic.

I guess it might have been copied there, but without completely rewriting this all, I'd rather not touch this analysis more than necessary.

michael-schwarz · 2022-05-17T07:28:50Z

src/analyses/varEq.ml

@@ -151,6 +152,7 @@ struct
    let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
    type_may_change_t a bt

+  (* TODO: why unused? how different from below? *)


They are very similar, but the code below handles more cases, but is also considerably more weird.

michael-schwarz · 2022-05-17T07:33:13Z

src/cdomains/addressDomain.ml

@@ -117,6 +115,7 @@ struct
      | false, false -> join x y
  *)

+  (* TODO: overrides is_top, but not top? *)


Yes, that is some kind of hack to avoid the creation of top addresses as this will fail from HoarePO. What is a bit strange is that is_top answers true as soon as the Addr.UnknownPtr is in the set, but top_ptr is defined as

let top_ptr = of_list Addr.([UnknownPtr; NullPtr])

I suppose it's weird because there isn't just a single value that this is_top returns true for. Probably good to have a comment about it to avoid surprises until we somehow design a more consistent domain where this inconsistency isn't necessary.

src/util/server.ml

michael-schwarz · 2022-05-17T07:39:20Z

src/util/intOps.ml

+  val lower_bound : t option (* TODO: unused *)
+  val upper_bound : t option (* TODO: unused *)


Those seem a bit strange here. IIRC, IntOpsBase is the module type we use for single values, not modules, ....
Maybe @jerhard knows what they are intended for?

I suppose at some point (maybe pre-bigints) it was necessary to know the min_int and max_int for these different types.

michael-schwarz · 2022-05-17T07:39:52Z

src/util/intOps.ml

@@ -42,7 +42,7 @@ sig
  val compare : t -> t -> int
  val equal : t -> t -> bool
  val hash : t -> int
-  val top_range : t -> t -> bool
+  val top_range : t -> t -> bool (* TODO: unused *)


Same here, I am not so sure what the intended semantics is here

Looking at the implementations, it seems to be for checking if the two arguments are min_int and max_int respectively. Again I guess we might've used that pre-bigints to do some special treatment, but that seems specific to intervals anyway.

michael-schwarz · 2022-05-17T07:40:14Z

src/util/intOps.ml

@@ -51,7 +51,7 @@ sig
  val to_int : t -> int
  val of_int64 : int64 -> t
  val to_int64 : t -> int64
-  val of_string : string -> t
+  val of_string : string -> t (* TODO: unused *)


I think we can keep the of_string, it may be handy sometimes.

Possibly yes. I guess this was used when we still parsed the strings from CIL constants for big values.

michael-schwarz · 2022-05-17T07:43:34Z

src/framework/analyses.ml

  changes: CompareCIL.change_info
 }

-let empty_increment_data ?(server=false) file = {
+let empty_increment_data ?(server=false) () = {
  server;
  old_data = None;


It's interesting that the file need not be saved here...

The file isn't saved in the incremental data, but with a separate variant into a separate file using Serialize, so this field was never read from. Actually #357 would probably change this and put the file (along with everything else) into a single record and not have separate files. Depending on the choices taken for #357, it need not be this increment data record that everything goes into, but maybe some outer wrapping record.

src/domains/setDomain.ml

michael-schwarz · 2022-05-17T07:57:21Z

src/domains/partitionDomain.ml

@@ -132,6 +132,7 @@ struct
      in
      fold f xs (empty ())

+  (* TODO: unused *)


I think we might want to keep this

michael-schwarz · 2022-05-17T07:58:05Z

src/domains/mapDomain.ml

@@ -31,7 +31,7 @@ sig
  val for_all: (key -> value -> bool) -> t -> bool
  val map2: (value -> value -> value) -> t -> t -> t
  val long_map2: (value -> value -> value) -> t -> t -> t
-  val merge : (key -> value option -> value option -> value option) -> t -> t -> t
+  val merge : (key -> value option -> value option -> value option) -> t -> t -> t (* TODO: unused, remove? *)


I think merge may also be worth keeping

src/domains/lattice.ml

michael-schwarz · 2022-05-17T07:59:20Z

src/domains/hoareDomain.ml

@@ -105,7 +104,7 @@ struct
    (* Map.map (List.map f) m *)
    (* since hashes might change we need to rebuild: *)
    apply_list (List.map f) m
-  let filter f m = apply_list (List.filter f) m (* TODO do something better? *)
+  let filter f m = apply_list (List.filter f) m (* TODO do something better? unused *)


I think it's worth keeping

michael-schwarz · 2022-05-17T07:59:33Z

src/domains/hoareDomain.ml

@@ -48,6 +48,7 @@ struct
  let elements m = Map.values m |> List.of_enum |> List.flatten

  (* merge elements in x and y by f *)
+  (* TODO: unused, remove? *)
  let merge op f x y =


also worth keeping in my opinion

src/cdomains/lval.ml

src/analyses/uninit.ml

src/cdomains/exp.ml

sim642 · 2022-05-22T13:34:56Z

Since goblint/gobview#13 is now merged into Gobview, which now depends on changes from this PR, it would be good to now delay this too much since it blocks any other PRs to Gobview as they would only work on this branch of Goblint.

Regarding all the "worth keeping" comments, I'd suggest not removing those things now, but leaving the comments so it's immediately apparent if some weird code is used for anything or not.

michael-schwarz · 2022-05-22T13:46:49Z

I'd suggest not removing those things now, but leaving the comments so it's immediately apparent if some weird code is used for anything or not.

Ok, sounds good to me!

Run dead code analysis with reanalyze

711d37b

sim642 added the cleanup Refactoring, clean-up label May 16, 2022

sim642 added this to the v2.0.0 milestone May 16, 2022

michael-schwarz requested review from jerhard, michael-schwarz and vogler May 16, 2022 08:36

Fix SolverTest compilation after dce

7a0f4df

michael-schwarz requested a review from vesalvojdani May 16, 2022 08:58

sim642 mentioned this pull request May 16, 2022

Run dead code analysis with reanalyze goblint/gobview#13

Merged

Update Gobview after dce

948ab66

michael-schwarz reviewed May 16, 2022

View reviewed changes

src/analyses/condVars.ml Show resolved Hide resolved

michael-schwarz reviewed May 16, 2022

View reviewed changes

src/analyses/base.ml Show resolved Hide resolved

michael-schwarz reviewed May 16, 2022

View reviewed changes

src/analyses/mCP.ml Show resolved Hide resolved