Skip to content

Commit 206bed3

Browse files
committed
Collapse base collect_invalidate result into single address set
There's no point keeping them separate. And it would just benefit from not having the same duplicate address in multiple sets in the list.
1 parent 461485c commit 206bed3

File tree

1 file changed

+11
-11
lines changed

1 file changed

+11
-11
lines changed

src/analyses/base.ml

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2100,21 +2100,21 @@ struct
21002100
(** From a list of expressions, collect a list of addresses that they might point to, or contain pointers to. *)
21012101
let collect_funargs ~man ?(warn=false) (st:store) (exps: exp list) =
21022102
let ask = Analyses.ask_of_man man in
2103-
let do_exp e =
2103+
let do_exp acc e =
21042104
let immediately_reachable = reachable_from_value ask (eval_rv ~man st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in
2105-
reachable_vars ~man st immediately_reachable
2105+
AD.join acc (reachable_vars ~man st immediately_reachable)
21062106
in
2107-
List.map do_exp exps
2107+
List.fold_left do_exp (AD.empty ()) exps
21082108

21092109
let collect_invalidate ~deep ~man ?(warn=false) (st:store) (exps: exp list) =
21102110
if deep then
21112111
collect_funargs ~man ~warn st exps
21122112
else (
2113-
let mpt e = match eval_rv_address ~man st e with
2114-
| Address a -> AD.remove NullPtr a
2115-
| _ -> AD.empty ()
2113+
let mpt acc e = match eval_rv_address ~man st e with
2114+
| Address a -> AD.join acc (AD.remove NullPtr a)
2115+
| _ -> acc
21162116
in
2117-
List.map mpt exps
2117+
List.fold_left mpt (AD.empty ()) exps
21182118
)
21192119

21202120
let invalidate ~(must: bool) ?(deep=true) ~man (st:store) (exps: exp list): store =
@@ -2129,8 +2129,8 @@ struct
21292129
(a, t, nv)
21302130
in
21312131
let invalids =
2132-
let args = collect_invalidate ~deep ~man ~warn:true st exps in (* NB! the returned list isn't necessarily as long as exps *)
2133-
let args = List.concat_map AD.elements args in (* split all address sets up because each address of different type (and with different current value) should get a different invalidated value *)
2132+
let args = collect_invalidate ~deep ~man ~warn:true st exps in
2133+
let args = AD.elements args in (* split all address sets up because each address of different type (and with different current value) should get a different invalidated value *)
21342134
List.map invalidate_addr args
21352135
in
21362136
let is_fav_addr x =
@@ -2236,8 +2236,8 @@ struct
22362236
let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in
22372237
let shallow_flist = collect_invalidate ~deep:false ~man man.local shallow_args in
22382238
let deep_flist = collect_invalidate ~deep:true ~man man.local deep_args in
2239-
let flist = shallow_flist @ deep_flist in
2240-
let addrs = List.concat_map AD.to_var_may flist in
2239+
let flist = AD.join shallow_flist deep_flist in
2240+
let addrs = AD.to_var_may flist in
22412241
if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs;
22422242
List.filter_map (create_thread ~multiple:true None None) addrs
22432243

0 commit comments

Comments
 (0)