Merge pull request #737 from goblint/reanalyze-dce

Run dead code analysis with reanalyze

Author: sim642

gobview

@@ -625,11 +625,12 @@ struct
       | _ -> d
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
-    let d = ctx.local in
+    (* let d = ctx.local in *)
     match q with
-    | Queries.Priority _ ->
+    (* had this query but nobody asked for it *)
+    (* | Queries.Priority _ ->
       if Pri.is_int d.pri then Queries.ID.of_int IInt @@ BI.of_int64 @@ Option.get @@ Pri.to_int d.pri (* TODO: what ikind to use for priorities? *)
-      else if Pri.is_top d.pri then Queries.Result.top q else Queries.Result.bot q (* TODO: remove bot *)
+      else if Pri.is_top d.pri then Queries.Result.top q else Queries.Result.bot q (* TODO: remove bot *) *)
     (* | Queries.MayBePublic _ -> *)
     (*   `Bool ((PrE.to_int d.pre = Some 0L || PrE.to_int d.pre = None) && (not (mode_is_init d.pmo))) *)
     | _ -> Queries.Result.top q

src/analyses/arinc.ml

@@ -61,9 +61,6 @@ struct
     let r = is_protected_by ask m x in
     if r then ProtectionLogging.record m x;
     r
-
-  let is_atomic ask: bool =
-    ask Q.MustBeAtomic
 end
 
 module MutexGlobals =

src/analyses/base.ml

@@ -1,4 +1,5 @@
 (** Must equality between variables and logical expressions. *)
+(* TODO: unused, what is this analysis? *)
 
 open Prelude.Ana
 open Analyses

src/analyses/commonPriv.ml

@@ -39,14 +39,6 @@ struct
     | [(v,_)] -> Some v
     | _ -> None
 
-  let query_eq (ask: Queries.ask) exp =
-    match ask.f (Queries.EqualSet exp) with
-    | l when not (Queries.ES.is_top l) ->
-      Queries.ES.elements l
-    | _ -> []
-  let print_query_eq ?msg:(msg="") ask exp =
-    let xs = query_eq ask exp in (* EqualSet -> ExpSet *)
-    Messages.debug "%s EqualSet %a = [%a]" msg d_exp exp (Pretty.d_list ", " d_exp) xs
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =

src/analyses/condVars.ml

@@ -563,7 +563,7 @@ let get_threadsafe_inv_ac name =
 
 
 
-let lib_funs = ref (Set.String.of_list ["list_empty"; "__raw_read_unlock"; "__raw_write_unlock"; "spin_trylock"])
+let lib_funs = ref (Set.String.of_list ["__raw_read_unlock"; "__raw_write_unlock"; "spin_trylock"])
 let add_lib_funs funs = lib_funs := List.fold_right Set.String.add funs !lib_funs
 let use_special fn_name = Set.String.mem fn_name !lib_funs
 

src/analyses/fileUse.ml

@@ -268,9 +268,6 @@ struct
           Result.meet a @@ S.query ctx' q
         in
         match q with
-        | Queries.PrintFullState ->
-          ignore (Pretty.printf "Current State:\n%a\n\n" D.pretty ctx.local);
-          ()
         | Queries.WarnGlobal g ->
           (* WarnGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *)
           let (n, g): V.t = Obj.obj g in
@@ -331,7 +328,6 @@ struct
     { ctx with
       local  = obj d
     ; context = (fun () -> ctx.context () |> assoc n |> obj)
-    ; postsub= assoc_sub post_all
     ; global = (fun v      -> ctx.global (v_of n v) |> g_to n |> obj)
     ; split
     ; sideg  = (fun v g    -> ctx.sideg (v_of n v) (g_of n g))

src/analyses/libraryFunctions.ml

@@ -183,10 +183,6 @@ struct
 
   (* Function calls *)
 
-  let eval_funvar ctx (fv:exp) : varinfo list =
-    warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local fv;
-    []
-
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     let nst = remove_unreachable (Analyses.ask_of_ctx ctx) args ctx.local in
     may (fun x -> warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local (Lval x)) lval;

src/analyses/mCP.ml

@@ -143,13 +143,6 @@ struct
       event ctx e octx (* delegate to must lockset analysis *)
 end
 
-module MyParam =
-struct
-  module G = LockDomain.Simple
-  let effect_fun ?write:(w=false) ls = Lockset.export_locks ls
-  let check_fun = effect_fun
-end
-
 module WriteBased =
 struct
   module GReadWrite =
@@ -163,12 +156,12 @@ struct
     let name () = "write"
   end
   module G = Lattice.Prod (GReadWrite) (GWrite)
-  let effect_fun ?write:(w=false) ls =
+  let effect_fun ?(write=false) ls =
     let locks = Lockset.export_locks ls in
-    (locks, if w then locks else Mutexes.top ())
-  let check_fun ?write:(w=false) ls =
+    (locks, if write then locks else Mutexes.top ())
+  let check_fun ?(write=false) ls =
     let locks = Lockset.export_locks ls in
-    if w then (Mutexes.bot (), locks) else (locks, Mutexes.bot ())
+    if write then (Mutexes.bot (), locks) else (locks, Mutexes.bot ())
 end
 
 module Spec = MakeSpec (WriteBased)