Skip to content

Commit

Permalink
Audit usages of fold_right
Browse files Browse the repository at this point in the history
  • Loading branch information
michael-schwarz committed Feb 18, 2025
1 parent 746d436 commit c13bcc3
Show file tree
Hide file tree
Showing 8 changed files with 33 additions and 31 deletions.
10 changes: 4 additions & 6 deletions src/analyses/apron/relationAnalysis.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -465,17 +465,15 @@ struct

(* Give the set of reachables from argument. *)
let reachables (ask: Queries.ask) es =
let reachable e st =
match st with
| None -> None
| Some st ->
let reachable acc e =
Option.bind acc (fun st ->
let ad = ask.f (Queries.ReachableFrom e) in
if Queries.AD.is_top ad then
None
else
Some (Queries.AD.join ad st)
Some (Queries.AD.join ad st))
in
List.fold_right reachable es (Some (Queries.AD.empty ()))
List.fold_left reachable (Some (Queries.AD.empty ())) es


let forget_reachable man st es =
Expand Down
6 changes: 3 additions & 3 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -518,7 +518,7 @@ struct
(* From a list of values, presumably arguments to a function, simply extract
* the pointer arguments. *)
let get_ptrs (vals: value list): address list =
let f (x:value) acc = match x with
let f acc (x:value) = match x with
| Address adrs when AD.is_top adrs ->
M.info ~category:Unsound "Unknown address given as function argument"; acc
| Address adrs when AD.to_var_may adrs = [] -> acc
Expand All @@ -528,7 +528,7 @@ struct
| Top -> M.info ~category:Unsound "Unknown value type given as function argument"; acc
| _ -> acc
in
List.fold_right f vals []
List.fold_left f [] vals

let rec reachable_from_value ask (value: value) (t: typ) (description: string) =
let empty = AD.empty () in
Expand Down Expand Up @@ -572,7 +572,7 @@ struct
if M.tracing then M.traceli "reachability" "Checking reachable arguments from [%a]!" (d_list ", " AD.pretty) args;
let empty = AD.empty () in
(* We begin looking at the parameters: *)
let argset = List.fold_right (AD.join) args empty in
let argset = List.fold_left (AD.join) empty args in
let workset = ref argset in
(* And we keep a set of already visited variables *)
let visited = ref empty in
Expand Down
8 changes: 4 additions & 4 deletions src/analyses/malloc_null.ml
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ struct
(* Remove null values from state that are unreachable from exp.*)
let remove_unreachable (ask: Queries.ask) (args: exp list) (st: D.t) : D.t =
let reachable =
let do_exp e a =
let do_exp a e =
match ask.f (Queries.ReachableFrom e) with
| ad when not (Queries.AD.is_top ad) ->
ad
Expand All @@ -103,9 +103,9 @@ struct
| _ -> false)
|> Queries.AD.join a
(* Ignore soundness warnings, as invalidation proper will raise them. *)
| _ -> AD.empty ()
| _ -> AD.empty () (* TODO: correct?! *)
in
List.fold_right do_exp args (AD.empty ())
List.fold_left do_exp (AD.empty ()) args
in
let vars =
reachable
Expand Down Expand Up @@ -164,7 +164,7 @@ struct
let return_addr () = !return_addr_

let return man (exp:exp option) (f:fundec) : D.t =
let remove_var x v = List.fold_right D.remove (to_addrs v) x in
let remove_var x v = List.fold_left (Fun.flip @@ D.remove) x (to_addrs v) in
let nst = List.fold_left remove_var man.local (f.slocals @ f.sformals) in
match exp with
| Some ret ->
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/region.ml
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ struct
| Queries.Regions e ->
let regpart = man.global () in
if is_bullet e regpart man.local then Queries.Result.bot q (* TODO: remove bot *) else
let ls = List.fold_right Queries.LS.add (regions e regpart man.local) (Queries.LS.empty ()) in
let ls = List.fold_left (Fun.flip @@ Queries.LS.add) (Queries.LS.empty ()) (regions e regpart man.local) in
ls
| _ -> Queries.Result.top q

Expand Down
3 changes: 2 additions & 1 deletion src/analyses/symbLocks.ml
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,8 @@ struct
let assign man lval rval = invalidate_lval (Analyses.ask_of_man man) lval man.local

let return man exp fundec =
List.fold_right D.remove_var (fundec.sformals@fundec.slocals) man.local
let rm list acc = List.fold_left (Fun.flip @@ D.remove_var) acc list in
rm fundec.slocals (rm fundec.sformals man.local)

let enter man lval f args = [(man.local,man.local)]
let combine_env man lval fexp f args fc au f_ask = au
Expand Down
10 changes: 5 additions & 5 deletions src/analyses/varEq.ml
Original file line number Diff line number Diff line change
Expand Up @@ -386,12 +386,12 @@ struct
*)
(* Give the set of reachables from argument. *)
let reachables ~deep (ask: Queries.ask) es =
let reachable e st =
let reachable acc e =
let q = if deep then Queries.ReachableFrom e else Queries.MayPointTo e in
let ad = ask.f q in
Queries.AD.join ad st
Queries.AD.join ad acc
in
List.fold_right reachable es (Queries.AD.empty ())
List.fold_left reachable (Queries.AD.empty ()) es


(* Probably ok as is. *)
Expand All @@ -402,8 +402,8 @@ struct

(* Just remove things that go out of scope. *)
let return man exp fundec =
let rm v = remove (Analyses.ask_of_man man) (Var v,NoOffset) in
List.fold_right rm (fundec.sformals@fundec.slocals) man.local
let rm acc v = remove (Analyses.ask_of_man man) (Var v, NoOffset) acc in
List.fold_left rm man.local (fundec.sformals@fundec.slocals)

(* removes all equalities with lval and then tries to make a new one: lval=rval *)
let assign man (lval:lval) (rval:exp) : D.t =
Expand Down
23 changes: 13 additions & 10 deletions src/cdomain/value/cdomains/int/defExcDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -299,15 +299,15 @@ struct
let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in
norm ik @@ (`Excluded (ex, r))

let to_bitfield ik x =
match x with
| `Definite c -> (Z.lognot c, c)
| _ when Cil.isSigned ik ->
let one_mask = Z.lognot Z.zero in
let to_bitfield ik x =
match x with
| `Definite c -> (Z.lognot c, c)
| _ when Cil.isSigned ik ->
let one_mask = Z.lognot Z.zero in
(one_mask, one_mask)
| _ ->
let one_mask = Z.lognot Z.zero in
let ik_mask = snd (Size.range ik) in
| _ ->
let one_mask = Z.lognot Z.zero in
let ik_mask = snd (Size.range ik) in
(one_mask, ik_mask)

let starting ?(suppress_ovwarn=false) ikind x =
Expand All @@ -321,6 +321,9 @@ struct
let of_excl_list t l =
let r = size t in (* elements in l are excluded from the full range of t! *)
`Excluded (List.fold_right S.add l (S.empty ()), r)
(* TODO: Change after #1686 has landed *)
(* `Excluded (S.of_list l, r) *)

let is_excl_list l = match l with `Excluded _ -> true | _ -> false
let to_excl_list (x:t) = match x with
| `Definite _ -> None
Expand Down Expand Up @@ -542,8 +545,8 @@ struct

let refine_with_congruence ik a b = a

let refine_with_bitfield ik x (z,o) =
match BitfieldDomain.Bitfield.to_int (z,o) with
let refine_with_bitfield ik x (z,o) =
match BitfieldDomain.Bitfield.to_int (z,o) with
| Some y ->
meet ik x (`Definite y)
| _ ->
Expand Down
2 changes: 1 addition & 1 deletion src/util/library/libraryFunctions.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1288,7 +1288,7 @@ let reset_lazy () =
ResettableLazy.reset activated_library_descs

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 add_lib_funs funs = lib_funs := List.fold_left (Fun.flip @@ Set.String.add) !lib_funs funs
let use_special fn_name = Set.String.mem fn_name !lib_funs

let kernel_safe_uncalled = Set.String.of_list ["__inittest"; "init_module"; "__exittest"; "cleanup_module"]
Expand Down

0 comments on commit c13bcc3

Please sign in to comment.