Skip to content

Run dead code analysis with reanalyze #737

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
merged 17 commits into from
May 27, 2022
Merged

Run dead code analysis with reanalyze #737

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
711d37b
Run dead code analysis with reanalyze
sim642 May 16, 2022
7a0f4df
Fix SolverTest compilation after dce
sim642 May 16, 2022
948ab66
Update Gobview after dce
sim642 May 16, 2022
63c6c63
Fix reanalyze warnings about always supplied optional arguments
sim642 May 17, 2022
e3c0809
Fix wrong unused TODO in uninit access_one_byval
sim642 May 17, 2022
ca88fe4
Remove unused split from set domain
sim642 May 17, 2022
7361f9b
Remove unused Lattice.LexProd
sim642 May 17, 2022
1b2063e
Remove unused access functions in uninit analysis
sim642 May 17, 2022
bf917b5
Split up exp.ml
sim642 May 17, 2022
9c283fc
Remove unused LockDomain.Symbolic.kill_lval
sim642 May 17, 2022
cdae5fa
Move Exp.Exp.contains_var to SymbLocksDomain
sim642 May 17, 2022
25d1e66
Remove now empty exp.ml
sim642 May 17, 2022
6b43d76
Move some Lval.Fields functions to unused MusteqDomain
sim642 May 17, 2022
3bc7f42
Remove base analysis ListDomain
sim642 May 18, 2022
bb324ad
Remove Linux kernel List_empty from LibraryFunctions.lib_funs
sim642 May 18, 2022
d7088fd
Update Gobview submodule after reanalyze-dce merge
sim642 May 23, 2022
e9bd890
Merge branch 'master' into reanalyze-dce
sim642 May 27, 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 gobview
Open in desktop
Submodule gobview updated 14 files
+0 −50 src/DTreeView.re
+0 −29 src/Menu.re
+0 −20 src/bindings/dOMParser.ml
+0 −7 src/bindings/dOMParser.mli
+2 −1 src/state/gvDisplay.ml
+1 −1 src/state/gvGoblint.ml
+0 −8 src/state/gvInspect.ml
+1 −0 src/state/gvMessages.ml
+2 −2 src/state/search.ml
+0 −8 src/ui/base/form.re
+0 −37 src/ui/base/mappedInput.re
+1 −0 src/utils/httpClient.ml
+0 −59 src/utils/xml.ml
+0 −15 src/utils/xmlParser.ml
7 changes: 4 additions & 3 deletions src/analyses/arinc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
53 changes: 24 additions & 29 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,6 @@ struct

let name () = "base"
let startstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
let otherstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
let exitstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}

(**************************************************************************
Expand Down Expand Up @@ -1121,7 +1120,7 @@ struct
(** [set st addr val] returns a state where [addr] is set to [val]
* it is always ok to put None for lval_raw and rval_raw, this amounts to not using/maintaining
* precise information about arrays. *)
let set (a: Q.ask) ?(ctx=None) ?(invariant=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store =
let set (a: Q.ask) ~(ctx: _ ctx) ?(invariant=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store =
let update_variable x t y z =
if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\n\n" x.vname VD.pretty y CPA.pretty z;
let r = update_variable x t y z in (* refers to defintion that is outside of set *)
Expand Down Expand Up @@ -1186,7 +1185,7 @@ struct
Priv.read_global a priv_getg st x
in
let new_value = update_offset old_value in
let r = Priv.write_global ~invariant a priv_getg (priv_sideg (Option.get ctx).sideg) st x new_value in
let r = Priv.write_global ~invariant a priv_getg (priv_sideg ctx.sideg) st x new_value in
if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a\n\n" x.vname D.pretty r;
r
end else begin
Expand Down Expand Up @@ -1230,8 +1229,6 @@ struct
VD.affect_move a v x (fun x -> None)
else
let patched_ask =
match ctx with
| Some ctx ->
(* The usual recursion trick for ctx. *)
(* Must change ctx used by ask to also use new st (not ctx.local), otherwise recursive EvalInt queries use outdated state. *)
(* Note: query is just called on base, but not any other analyses. Potentially imprecise, but seems to be sufficient for now. *)
Expand All @@ -1242,8 +1239,6 @@ struct
}
in
Analyses.ask_of_ctx ctx'
| _ ->
a
in
let moved_by = fun x -> Some 0 in (* this is ok, the information is not provided if it *)
VD.affect_move patched_ask v x moved_by (* was a set call caused e.g. by a guard *)
Expand Down Expand Up @@ -1278,7 +1273,7 @@ struct
(* if M.tracing then M.tracel "set" ~var:firstvar "set got an exception '%s'\n" x; *)
M.warn "Assignment to unknown address"; st

let set_many ?ctx a (gs:glob_fun) (st: store) lval_value_list: store =
let set_many ~ctx a (gs:glob_fun) (st: store) lval_value_list: store =
(* Maybe this can be done with a simple fold *)
let f (acc: store) ((lval:AD.t),(typ:Cil.typ),(value:value)): store =
set ~ctx a gs acc lval typ value
Expand Down Expand Up @@ -1453,7 +1448,7 @@ struct
let oldval = get a gs st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *)
let oldval = if is_some_bot oldval then (M.tracec "invariant" "%a is bot! This should not happen. Will continue with top!" d_lval lval; VD.top ()) else oldval in
let t_lval = Cilfacade.typeOfLval lval in
let state_with_excluded = set a gs st addr t_lval value ~invariant:true ~ctx:(Some ctx) in
let state_with_excluded = set a gs st addr t_lval value ~invariant:true ~ctx in
let value = get a gs state_with_excluded addr None in
let new_val = apply_invariant oldval value in
if M.tracing then M.traceu "invariant" "New value is %a\n" VD.pretty new_val;
Expand All @@ -1463,8 +1458,8 @@ struct
raise Analyses.Deadcode
)
else if VD.is_bot new_val
then set a gs st addr t_lval value ~invariant:true ~ctx:(Some ctx) (* no *_raw because this is not a real assignment *)
else set a gs st addr t_lval new_val ~invariant:true ~ctx:(Some ctx) (* no *_raw because this is not a real assignment *)
then set a gs st addr t_lval value ~invariant:true ~ctx (* no *_raw because this is not a real assignment *)
else set a gs st addr t_lval new_val ~invariant:true ~ctx (* no *_raw because this is not a real assignment *)
| None ->
if M.tracing then M.traceu "invariant" "Doing nothing.\n";
M.debug ~category:Analyzer "Invariant failed: expression \"%a\" not understood." d_plainexp exp;
Expand Down Expand Up @@ -1599,7 +1594,7 @@ struct
in
let eval e st = eval_rv a gs st e in
let eval_bool e st = match eval e st with `Int i -> ID.to_bool i | _ -> None in
let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) v ~invariant:true ~ctx:(Some ctx) in
let set' lval v st = set a gs st (eval_lv a gs st lval) (Cilfacade.typeOfLval lval) v ~invariant:true ~ctx in
let rec inv_exp c exp (st:store): store =
(* trying to improve variables in an expression so it is bottom means dead code *)
if ID.is_bot c then raise Deadcode;
Expand Down Expand Up @@ -1693,7 +1688,7 @@ struct
in
inv_exp itv exp st

let set_savetop ?ctx ?lval_raw ?rval_raw ask (gs:glob_fun) st adr lval_t v : store =
let set_savetop ~ctx ?lval_raw ?rval_raw ask (gs:glob_fun) st adr lval_t v : store =
if M.tracing then M.tracel "set" "savetop %a %a %a\n" AD.pretty adr d_type lval_t VD.pretty v;
match v with
| `Top -> set ~ctx ask gs st adr lval_t (VD.top_value (AD.get_type adr)) ?lval_raw ?rval_raw
Expand Down Expand Up @@ -1750,7 +1745,7 @@ struct
in
match is_list_init () with
| Some a when (get_bool "exp.list-type") ->
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.singleton (Addr.from_var a)) lval_t (`List (ValueDomain.Lists.bot ()))
set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.singleton (Addr.from_var a)) lval_t (`List (ValueDomain.Lists.bot ()))
| _ ->
let rval_val = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local rval in
let lval_val = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
Expand Down Expand Up @@ -1884,7 +1879,7 @@ struct
ctx.sideg (V.thread tid) (G.create_thread rv);
| _ -> ()
end;
set ~ctx:(Some ctx) ~t_override (Analyses.ask_of_ctx ctx) ctx.global nst (return_var ()) t_override rv
set ~ctx ~t_override (Analyses.ask_of_ctx ctx) ctx.global nst (return_var ()) t_override rv
(* lval_raw:None, and rval_raw:None is correct here *)

let vdecl ctx (v:varinfo) =
Expand All @@ -1894,7 +1889,7 @@ struct
let lval = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Var v, NoOffset) in
let current_value = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local (Lval (Var v, NoOffset)) in
let new_value = VD.update_array_lengths (eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local) current_value v.vtype in
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval v.vtype new_value
set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval v.vtype new_value

(**************************************************************************
* Function calls
Expand All @@ -1908,7 +1903,7 @@ struct
in
List.concat_map do_exp exps

let invalidate ?ctx ask (gs:glob_fun) (st:store) (exps: exp list): store =
let invalidate ~ctx ask (gs:glob_fun) (st:store) (exps: exp list): store =
if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]\n" (d_list ", " d_plainexp) exps;
if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_plainexp) exps;
(* To invalidate a single address, we create a pair with its corresponding
Expand All @@ -1935,7 +1930,7 @@ struct
let vs = List.map (Tuple3.third) invalids' in
M.tracel "invalidate" "Setting addresses [%a] to values [%a]\n" (d_list ", " AD.pretty) addrs (d_list ", " VD.pretty) vs
);
set_many ?ctx ask gs st invalids'
set_many ~ctx ask gs st invalids'


let make_entry ?(thread=false) (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) fundec args: D.t =
Expand Down Expand Up @@ -2146,7 +2141,7 @@ struct
| _ ->
VD.top_value dest_typ
in
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
| _, _ -> failwith "strange memset arguments"
end
| `Unknown (("bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk") as name) ->
Expand All @@ -2160,7 +2155,7 @@ struct
(* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *)
let value = VD.zero_init_value dest_typ in
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
| _, _ -> failwith "strange bzero arguments"
end
| `Unknown "F59" (* strcpy *)
Expand Down Expand Up @@ -2205,10 +2200,10 @@ struct
let eadr = AD.singleton (Addr.from_var elm) in
let eitemadr = AD.singleton (Addr.from_var_offset (elm, convert_offset (Analyses.ask_of_ctx ctx) ctx.global ctx.local next)) in
let new_list = `List (ValueDomain.Lists.add eadr ld) in
let s1 = set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local ladr lst.vtype new_list in
let s2 = set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global s1 eitemadr (AD.get_type eitemadr) (`Address (AD.singleton (Addr.from_var lst))) in
let s1 = set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local ladr lst.vtype new_list in
let s2 = set ~ctx (Analyses.ask_of_ctx ctx) ctx.global s1 eitemadr (AD.get_type eitemadr) (`Address (AD.singleton (Addr.from_var lst))) in
s2
| _ -> set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local ladr lst.vtype `Top
| _ -> set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local ladr lst.vtype `Top
end
| _ -> failwith "List function arguments are strange/complicated."
end
Expand All @@ -2220,13 +2215,13 @@ struct
let lptr = AD.singleton (Addr.from_var_offset (elm, convert_offset (Analyses.ask_of_ctx ctx) ctx.global ctx.local next)) in
let lprt_val = get (Analyses.ask_of_ctx ctx) ctx.global ctx.local lptr None in
let lst_poison = `Address (AD.singleton (Addr.from_var ListDomain.list_poison)) in
let s1 = set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local lptr (AD.get_type lptr) (VD.join lprt_val lst_poison) in
let s1 = set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local lptr (AD.get_type lptr) (VD.join lprt_val lst_poison) in
match get (Analyses.ask_of_ctx ctx) ctx.global ctx.local lptr None with
| `Address ladr -> begin
match get (Analyses.ask_of_ctx ctx) ctx.global ctx.local ladr None with
| `List ld ->
let del_ls = ValueDomain.Lists.del eadr ld in
let s2 = set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global s1 ladr (AD.get_type ladr) (`List del_ls) in
let s2 = set ~ctx (Analyses.ask_of_ctx ctx) ctx.global s1 ladr (AD.get_type ladr) (`List del_ls) in
s2
| _ -> s1
end
Expand Down Expand Up @@ -2281,7 +2276,7 @@ struct
| `Thread a ->
let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in
(* TODO: is this type right? *)
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v
set ~ctx (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v
| _ -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
end
| _ -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var]
Expand Down Expand Up @@ -2348,7 +2343,7 @@ struct
| `Unknown "__goblint_unknown" ->
begin match args with
| [Lval lv] | [CastE (_,AddrOf lv)] ->
let st = set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lv) (Cilfacade.typeOfLval lv) `Top in
let st = set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lv) (Cilfacade.typeOfLval lv) `Top in
st
| _ ->
failwith "Function __goblint_unknown expected one address-of argument."
Expand Down Expand Up @@ -2378,7 +2373,7 @@ struct
LF.effects_for f.vname args
|> List.map (fun sets ->
List.fold_left (fun acc (lv, x) ->
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global acc (eval_lv (Analyses.ask_of_ctx ctx) ctx.global acc lv) (Cilfacade.typeOfLval lv) x
set ~ctx (Analyses.ask_of_ctx ctx) ctx.global acc (eval_lv (Analyses.ask_of_ctx ctx) ctx.global acc lv) (Cilfacade.typeOfLval lv) x
) st sets
)
|> BatList.fold_left D.meet st
Expand Down Expand Up @@ -2476,7 +2471,7 @@ struct
Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
| Events.AssignSpawnedThread (lval, tid) ->
(* TODO: is this type right? *)
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid))
set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid))
| _ ->
ctx.local
end
Expand Down
3 changes: 0 additions & 3 deletions src/analyses/commonPriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
1 change: 1 addition & 0 deletions src/analyses/condVars.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
(** Must equality between variables and logical expressions. *)
(* TODO: unused, what is this analysis? *)

open Prelude.Ana
open Analyses
Expand Down
8 changes: 0 additions & 8 deletions src/analyses/fileUse.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
4 changes: 0 additions & 4 deletions src/analyses/mCP.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))
Expand Down
4 changes: 0 additions & 4 deletions src/analyses/malloc_null.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
15 changes: 4 additions & 11 deletions src/analyses/mutexAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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)
Expand Down
1 change: 0 additions & 1 deletion src/analyses/termination.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/analyses/uninit.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,7 @@ struct
| Var x, ofs -> access_offset ofs
| Mem n, ofs -> access_one_byval a false n @ access_offset ofs

(* TODO: unused? remove? *)
let access_byval a (rw: bool) (exps: exp list) =
List.concat_map (access_one_byval a rw) exps

Expand Down
2 changes: 2 additions & 0 deletions src/analyses/varEq.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ struct
| _ -> false

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

@michael-schwarz michael-schwarz May 17, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

@sim642 sim642 May 17, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

let may_change_t (b:exp) (a:exp) : bool =
let rec type_may_change_t a bt =
let rec may_change_t_offset o =
Expand Down Expand Up @@ -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? *)
Copy link
Member

@michael-schwarz michael-schwarz May 17, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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 =
Expand Down
3 changes: 1 addition & 2 deletions src/cdomains/addressDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -117,6 +115,7 @@ struct
| false, false -> join x y
*)

(* TODO: overrides is_top, but not top? *)
Copy link
Member

@michael-schwarz michael-schwarz May 17, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

@sim642 sim642 May 17, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

let is_top a = mem Addr.UnknownPtr a

let merge uop cop x y =
Expand Down
Loading