Run dead code analysis with reanalyze

src/analyses/arinc.ml

@@ -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/commonPriv.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/condVars.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/fileUse.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/libraryFunctions.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/mCP.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/malloc_null.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/mutexAnalysis.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)

src/analyses/symbLocks.ml

@@ -1,8 +1,8 @@
 (** Symbolic lock-sets for use in per-element patterns. *)
 
 module LF = LibraryFunctions
-module LP = Exp.LockingPattern
-module Exp = Exp.Exp
+module LP = SymbLocksDomain.LockingPattern
+module Exp = SymbLocksDomain.Exp
 module VarEq = VarEq.Spec
 
 module PS = SetDomain.ToppedSet (LP) (struct let topname = "All" end)

src/analyses/termination.ml

@@ -4,7 +4,6 @@ open Prelude.Ana
 open Analyses
 
 module M = Messages
-let (%?) = Option.bind
 let (||?) a b = match a,b with Some x,_ | _, Some x -> Some x | _ -> None
 
 module TermDomain = struct

src/analyses/uninit.ml

@@ -78,23 +78,6 @@ struct
     | Var x, ofs -> access_offset ofs
     | Mem n, ofs -> access_one_byval a false n @ access_offset ofs
 
-  let access_byval a (rw: bool) (exps: exp list) =
-    List.concat_map (access_one_byval a rw) exps
-
-  (* TODO: unused? remove? *)
-  let access_byref ask (exps: exp list) =
-    (* Find the addresses reachable from some expression, and assume that these
-     * can all be written to. *)
-    let do_exp e =
-      match ask (Queries.ReachableFrom e) with
-      | a when not (Queries.LS.is_top a) ->
-        let to_extra (v,o) xs = (v, Base.Offs.from_offset (conv_offset o), true) :: xs  in
-        Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
-      (* Ignore soundness warnings, as invalidation proper will raise them. *)
-      | _ -> []
-    in
-    List.concat_map do_exp exps
-
   (* list accessed addresses *)
   let varoffs a (rval:exp) =
     let f vs (v,o,_) = (v,o) :: vs in

src/analyses/varEq.ml

@@ -3,7 +3,7 @@
 module Addr = ValueDomain.Addr
 module Offs = ValueDomain.Offs
 module AD = ValueDomain.AD
-module Exp = Exp.Exp
+module Exp = CilType.Exp
 module LF = LibraryFunctions
 open Prelude.Ana
 open Analyses
@@ -109,6 +109,27 @@ struct
     |	CastE (t1,e1),	CastE (t2,e2) -> typ_equal t1 t2 && exp_equal e1 e2
     | _ -> false
 
+  (* TODO: what does interesting mean? *)
+  let rec interesting x =
+    match x with
+    | SizeOf _
+    | SizeOfE _
+    | SizeOfStr _
+    | AlignOf _
+    | AlignOfE _
+    | UnOp  _
+    | BinOp _ -> false
+    | Const _ -> true
+    | AddrOf  (Var v2,_)
+    | StartOf (Var v2,_)
+    | Lval    (Var v2,_) -> true
+    | AddrOf  (Mem e,_)
+    | StartOf (Mem e,_)
+    | Lval    (Mem e,_)
+    | CastE (_,e)           -> interesting e
+    | Question _ -> failwith "Logical operations should be compiled away by CIL."
+    | _ -> failwith "Unmatched pattern."
+
   (* helper to decide equality *)
   let query_exp_equal ask e1 e2 g s =
     let e1 = constFold false (stripCasts e1) in
@@ -119,6 +140,7 @@ struct
       | _ -> false
 
   (* kill predicate for must-equality kind of analyses*)
+  (* TODO: why unused? how different from below? *)
   let may_change_t (b:exp) (a:exp) : bool =
     let rec type_may_change_t a bt =
       let rec may_change_t_offset o =
@@ -151,6 +173,7 @@ struct
     let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
     type_may_change_t a bt
 
+  (* TODO: why unused? how different from below? *)
   let may_change_pt ask (b:exp) (a:exp) : bool =
     let pt e = ask (Queries.MayPointTo e) in
     let rec lval_may_change_pt a bl : bool =
@@ -377,7 +400,7 @@ struct
     *)  let lvt = unrollType @@ Cilfacade.typeOfLval lv in
     (*     Messages.warn ~msg:(sprint 80 (d_type () lvt)) (); *)
     if is_global_var ask (Lval lv) = Some false
-    && Exp.interesting rv
+    && interesting rv
     && is_global_var ask rv = Some false
     && ((isArithmeticType lvt && match lvt with | TFloat _ -> false | _ -> true ) || isPointerType lvt)
     then D.add_eq (rv,Lval lv) (remove ask lv st)
@@ -387,7 +410,7 @@ struct
         | Lval rlval -> begin
             match ask (Queries.MayPointTo (mkAddrOf rlval)) with
               | rv when not (Queries.LS.is_top rv) && Queries.LS.cardinal rv = 1 ->
-                  let rv = Exp.of_clval (Queries.LS.choose rv) in
+                  let rv = Lval.CilLval.to_exp (Queries.LS.choose rv) in
                   if is_local lv && Exp.is_global_var rv = Some false
                   then D.add_eq (rv,Lval lv) st
                   else st

src/cdomains/addressDomain.ml

@@ -1,7 +1,6 @@
 open Cil
 open Pretty
 open IntOps
-let fast_addr_sets = false (* unknown addresses for fast sets == top, for slow == {?}*)
 
 module GU = Goblintutil
 module M = Messages
@@ -41,7 +40,6 @@ struct
   let unknown_ptr    = singleton Addr.UnknownPtr
   let not_null       = unknown_ptr
   let top_ptr        = of_list Addr.([UnknownPtr; NullPtr])
-  let is_unknown x   = is_element Addr.UnknownPtr x
   let may_be_unknown x = exists (fun e -> e = Addr.UnknownPtr) x
   let is_null x      = is_element Addr.NullPtr x
   let is_not_null x  = for_all (fun e -> e <> Addr.NullPtr) x
@@ -117,6 +115,7 @@ struct
       | false, false -> join x y
   *)
 
+  (* TODO: overrides is_top, but not top? *)
   let is_top a = mem Addr.UnknownPtr a
 
   let merge uop cop x y =

src/cdomains/apron/apronDomain.apron.ml

@@ -1000,11 +1000,7 @@ sig
   include SLattice with type t = Man.mt A.t
 
 
-  val exp_is_cons : exp -> bool
-  val assert_cons : t -> exp -> bool -> t
   val assert_inv : t -> exp -> bool -> t
-  val check_assert : t -> exp -> [> `False | `Top | `True ]
-  val eval_interval_expr : t -> exp -> Z.t option * Z.t option
   val eval_int : t -> exp -> Queries.ID.t
 end
 
@@ -1020,7 +1016,6 @@ module ApronComponents (D2: S2) (PrivD: Lattice.S):
 sig
   module AD: S2 with type Man.mt = D2.Man.mt
   include Lattice.S with type t = (D2.t, PrivD.t) aproncomponents_t
-  val op_scheme: (D2.t -> D2.t -> D2.t) -> (PrivD.t -> PrivD.t -> PrivD.t) -> t -> t -> t
 end =
 struct
   module AD = D2

src/cdomains/arrayDomain.ml

@@ -25,7 +25,6 @@ sig
   val get_vars_in_e: t -> Cil.varinfo list
   val map: (value -> value) -> t -> t
   val fold_left: ('a -> value -> 'a) -> 'a -> t -> 'a
-  val fold_left2: ('a -> value -> value -> 'a) -> 'a -> t -> t -> 'a
   val smart_join: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t
   val smart_widen: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> t
   val smart_leq: (exp -> BI.t option) -> (exp -> BI.t option) -> t -> t -> bool
@@ -60,7 +59,6 @@ struct
   let get_vars_in_e _ = []
   let map f x = f x
   let fold_left f a x = f a x
-  let fold_left2 f a x y = f a x y
 
   let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>Any</key>\n%a\n</map>\n</value>\n" Val.printXml x
   let smart_join _ _ = join
@@ -145,7 +143,6 @@ struct
   let get_vars_in_e _ = []
   let map f (xl, xr) = ((List.map f xl), f xr)
   let fold_left f a x = f a (join_of_all_parts x)
-  let fold_left2 f a x y = f a (join_of_all_parts x) (join_of_all_parts y)
   let printXml f (xl,xr) = BatPrintf.fprintf f "<value>\n<map>\n
   <key>unrolled array</key>\n
   <key>xl</key>\n%a\n\n
@@ -309,9 +306,6 @@ struct
   let fold_left f a (_, ((xl:value), (xm:value), (xr:value))) =
     f (f (f a xl) xm) xr
 
-  let fold_left2 f a (_, ((xl:value), (xm:value), (xr:value))) (_, ((yl:value), (ym:value), (yr:value))) =
-    f (f (f a xl yl) xm ym) xr yr
-
   let move_if_affected_with_length ?(replace_with_const=false) length (ask:Q.ask) ((e, (xl,xm, xr)) as x) (v:varinfo) movement_for_exp =
     normalize @@
     let move (i:int option) =
@@ -381,7 +375,7 @@ struct
           end
     | _ -> x (* If the array is not partitioned, nothing to do *)
 
-  let move_if_affected ?(replace_with_const=false) = move_if_affected_with_length ~replace_with_const:replace_with_const None
+  let move_if_affected ?replace_with_const = move_if_affected_with_length ?replace_with_const None
 
   let set_with_length length (ask:Q.ask) ((e, (xl, xm, xr)) as x) (i,_) a =
     if M.tracing then M.trace "update_offset" "part array set_with_length %a %a %a\n" pretty x LiftExp.pretty i Val.pretty a;
@@ -707,7 +701,6 @@ struct
   let move_if_affected ?(replace_with_const=false) _ x _ _ = x
   let map f (x, l):t = (Base.map f x, l)
   let fold_left f a (x, l) = Base.fold_left f a x
-  let fold_left2 f a (x, l) (y, l) = Base.fold_left2 f a x y
   let get_vars_in_e _ = []
 
   let smart_join _ _ = join
@@ -743,12 +736,11 @@ struct
   let make l x = Base.make l x, l
   let length (_,l) = Some l
 
-  let move_if_affected ?(replace_with_const=false) ask (x,l) v i =
-    (Base.move_if_affected_with_length ~replace_with_const:replace_with_const (Some l) ask x v i), l
+  let move_if_affected ?replace_with_const ask (x,l) v i =
+    (Base.move_if_affected_with_length ?replace_with_const (Some l) ask x v i), l
 
   let map f (x, l):t = (Base.map f x, l)
   let fold_left f a (x, l) = Base.fold_left f a x
-  let fold_left2 f a (x, l) (y, l) = Base.fold_left2 f a x y
   let get_vars_in_e (x, _) = Base.get_vars_in_e x
 
   let smart_join x_eval_int y_eval_int (x,xl) (y,yl) =
@@ -794,7 +786,6 @@ struct
   let move_if_affected ?(replace_with_const=false) _ x _ _ = x
   let map f (x, l):t = (Base.map f x, l)
   let fold_left f a (x, l) = Base.fold_left f a x
-  let fold_left2 f a (x, l) (y, l) = Base.fold_left2 f a x y
   let get_vars_in_e _ = []
 
   let smart_join _ _ = join
@@ -855,7 +846,6 @@ struct
   let length = unop' P.length T.length U.length
   let map f = unop_to_t' (P.map f) (T.map f) (U.map f)
   let fold_left f s = unop' (P.fold_left f s) (T.fold_left f s) (U.fold_left f s)
-  let fold_left2 f s = binop' (P.fold_left2 f s) (T.fold_left2 f s) (U.fold_left2 f s)
 
   let move_if_affected ?(replace_with_const=false) (ask:Q.ask) x v f = unop_to_t' (fun x -> P.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> T.move_if_affected ~replace_with_const:replace_with_const ask x v f) (fun x -> U.move_if_affected ~replace_with_const:replace_with_const ask x v f) x
   let get_vars_in_e = unop' P.get_vars_in_e T.get_vars_in_e U.get_vars_in_e

src/cdomains/arrayDomain.mli

@@ -38,9 +38,6 @@ sig
   val fold_left: ('a -> value -> 'a) -> 'a -> t -> 'a
   (** Left fold (like List.fold_left) over the arrays elements *)
 
-  val fold_left2: ('a -> value -> value -> 'a) -> 'a -> t -> t -> 'a
-  (** Left fold over the elements of two arrays (like List.fold_left2 *)
-
   val smart_join: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t  -> t
   val smart_widen: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t -> t
   val smart_leq: (Cil.exp -> BigIntOps.t option) -> (Cil.exp -> BigIntOps.t option) -> t -> t  -> bool

src/cdomains/basetype.ml

@@ -29,8 +29,6 @@ struct
       "(" ^ x.vname ^ ", " ^ description ^ ")"
     else x.vname
   let pretty () x = Pretty.text (show x)
-  let pretty_trace () x = Pretty.dprintf "%s on %a" x.vname CilType.Location.pretty x.vdecl
-  let get_location x = x.vdecl
   type group = Global | Local | Parameter | Temp [@@deriving show { with_path = false }]
   let (%) = Batteries.(%)
   let to_group = Option.some % function
@@ -40,8 +38,6 @@ struct
     | _ -> Local
   let name () = "variables"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
-  let var_id _ = "globals"
-  let node _ = MyCFG.Function Cil.dummyFunDec
 
   let arbitrary () = MyCheck.Arbitrary.varinfo
 end