Merge pull request #1688 from goblint/issue_1536

Audit usages of `fold_right`

Author: michael-schwarz

src/analyses/apron/relationAnalysis.apron.ml

@@ -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 =
@@ -484,9 +482,8 @@ struct
       match reachables ask es with
       | None ->
         (* top reachable, so try to invalidate everything *)
-        RD.vars st.rel
-        |> List.filter_map RV.to_cil_varinfo
-        |> List.map Cil.var
+        let to_cil_lval x = Option.map Cil.var @@ RV.to_cil_varinfo x in
+        RD.vars st.rel |> List.filter_map to_cil_lval
       | Some ad ->
         let to_cil addr rs =
           match addr with
@@ -521,14 +518,10 @@ struct
     match desc.special args, f.vname with
     | Assert { exp; refine; _ }, _ -> assert_fn man exp refine
     | ThreadJoin { thread = id; ret_var = retvar }, _ ->
-      (
-        (* Forget value that thread return is assigned to *)
-        let st' = forget_reachable man st [retvar] in
-        let st' = Priv.thread_join ask man.global id st' in
-        match r with
-        | Some lv -> invalidate_one ask man st' lv
-        | None -> st'
-      )
+      (* Forget value that thread return is assigned to *)
+      let st' = forget_reachable man st [retvar] in
+      let st' = Priv.thread_join ask man.global id st' in
+      Option.map_default (invalidate_one ask man st') st' r
     | ThreadExit _, _ ->
       begin match ThreadId.get_current ask with
         | `Lifted tid ->
@@ -543,11 +536,10 @@ struct
       let id = List.hd args in
       Priv.thread_join ~force:true ask man.global id st
     | Rand, _ ->
-      (match r with
-       | Some lv ->
+      Option.map_default (fun lv ->
          let st = invalidate_one ask man st lv in
          assert_fn {man with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
-       | None -> st)
+        ) st r
     | _, _ ->
       let lvallist e =
         match ask.f (Queries.MayPointTo e) with
@@ -575,10 +567,7 @@ struct
       let shallow_lvals = List.concat_map lvallist shallow_addrs in
       let st' = List.fold_left (invalidate_one ask man) st' shallow_lvals in
       (* invalidate lval if present *)
-      match r with
-      | Some lv -> invalidate_one ask man st' lv
-      | None -> st'
-
+      Option.map_default (invalidate_one ask man st') st' r
 
   let query_invariant man context =
     let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in

src/analyses/base.ml

@@ -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
@@ -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
@@ -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

src/analyses/malloc_null.ml

@@ -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
@@ -103,9 +103,9 @@ struct
               | _ -> false)
           |> Queries.AD.join a
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
-        | _ -> AD.empty ()
+        | _ -> a
       in
-      List.fold_right do_exp args (AD.empty ())
+      List.fold_left do_exp (AD.empty ()) args
     in
     let vars =
       reachable
@@ -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 ->

src/analyses/region.ml

@@ -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
 

src/analyses/symbLocks.ml

@@ -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

src/analyses/uninit.ml

@@ -202,7 +202,7 @@ struct
               | _ -> false)
           |> Queries.AD.join a
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
-        | _ -> AD.empty ()
+        | _ -> a
       in
       List.fold_right do_exp args (AD.empty ())
     in

src/analyses/varEq.ml

@@ -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. *)
@@ -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  =

src/cdomain/value/cdomains/int/defExcDomain.ml

@@ -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

src/util/library/libraryFunctions.ml

@@ -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"]