Cleanup some option related code (#1689)

* Cleanup `option` related code

* relationAnalysis: Drastically simplify `pass_to_callee`

* Simplify some things in `relationAnalysis`

* Remove custom `default` function from `arrayDomain`

* Simplification in `addressDomain`

* Further cleanup

* Some further obvious cases

* Undo eta expansion

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

* Indentation

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

* Indentation

* Add TODO back

* Add comment back

* Indentation

---------

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

Author: michael-schwarz

src/analyses/abortUnless.ml

@@ -32,10 +32,7 @@ struct
       | [arg] when isIntegralType arg.vtype ->
         (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with
          | v when Queries.ID.is_bot v -> false
-         | v ->
-           match Queries.ID.to_bool v with
-           | Some b -> b
-           | None -> false)
+         | v -> BatOption.default false (Queries.ID.to_bool v))
       | _ ->
         (* should not happen, man.local should always be false in this case *)
         false

src/analyses/accessAnalysis.ml

@@ -79,10 +79,7 @@ struct
     man.local
 
   let return man exp fundec : D.t =
-    begin match exp with
-      | Some exp -> access_one_top man Read false exp
-      | None -> ()
-    end;
+    Option.iter (access_one_top man Read false) exp;
     man.local
 
   let body man f : D.t =
@@ -99,9 +96,7 @@ struct
       LibraryDesc.Accesses.iter desc.accs (fun {kind; deep = reach} exp ->
           access_one_top ~deref:true man kind reach exp (* access dereferenced using special accesses *)
         ) arglist;
-      (match lv with
-       | Some x -> access_one_top ~deref:true man Write false (AddrOf x)
-       | None -> ());
+      Option.iter (fun x -> access_one_top ~deref:true man Write false (AddrOf x)) lv;
       List.iter (access_one_top man Read false) arglist; (* always read all argument expressions without dereferencing *)
       man.local
 
@@ -115,19 +110,15 @@ struct
     au
 
   let combine_assign man lv fexp f args fc al f_ask =
-    begin match lv with
-      | None      -> ()
-      | Some lval -> access_one_top ~deref:true man Write false (AddrOf lval)
-    end;
+    Option.iter (fun lval -> access_one_top ~deref:true man Write false (AddrOf lval)) lv;
     man.local
 
 
   let threadspawn man  ~multiple lval f args fman =
     (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
-    begin match lval with
-      | None -> ()
-      | Some lval -> access_one_top ~force:true ~deref:true man Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
-    end;
+    Option.iter (fun lval ->
+        access_one_top ~force:true ~deref:true man Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
+      ) lval;
     man.local
 
   let query man (type a) (q: a Queries.t): a Queries.result =

src/analyses/apron/relationAnalysis.apron.ml

@@ -292,16 +292,14 @@ struct
     in
     List.fold (fun vs e -> VS.join vs (to_vs e)) (VS.empty ()) args
 
-  let pass_to_callee fundec any_local_reachable var =
-    (* TODO: currently, we pass all locals of the caller to the callee, provided one of them is reachbale to preserve relationality *)
+  let belongs_to_fundec fundec var =
+    (* TODO: currently, we pass all locals of the caller to the callee, provided one of them is reachable to preserve relationality *)
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
     let vname = GobApron.Var.show var in
-    let locals = fundec.sformals @ fundec.slocals in
-    match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
-    | None -> true
-    | Some v -> any_local_reachable
+    let equiv v = VM.var_name (Local v) = vname in (* TODO: optimize *)
+    (not @@ List.exists equiv fundec.sformals) && (not @@ List.exists equiv fundec.slocals)
 
   let make_callee_rel ~thread man f args =
     let fundec = Node.find_fundec man.node in
@@ -329,7 +327,7 @@ struct
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     RD.remove_filter_with new_rel (fun var ->
         match RV.find_metadata var with
-        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *)
+        | Some (Local _) when not (belongs_to_fundec fundec var || any_local_reachable) -> true (* remove caller locals provided they are unreachable *)
         | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
@@ -359,16 +357,14 @@ struct
     let st = man.local in
     let ask = Analyses.ask_of_man man in
     let new_rel =
-      if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then (
+      if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then
         let rel' = RD.add_vars st.rel [RV.return] in
-        match e with
-        | Some e ->
+        Option.map_default (fun e ->
           assign_from_globals_wrapper ask man.global {st with rel = rel'} e (fun rel' e' ->
               RD.assign_exp ask rel' RV.return e' (no_overflow ask e)
-            )
-        | None ->
-          rel' (* leaves V.return unconstrained *)
-      )
+              )
+          ) rel' e
+        (* default value rel' leaves V.return unconstrained *)
       else
         RD.copy st.rel
     in
@@ -426,7 +422,7 @@ struct
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
     let new_rel = RD.keep_filter st.rel (fun var ->
         match RV.find_metadata var with
-        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* keep caller locals, provided they were not passed to the function *)
+        | Some (Local _) when not (belongs_to_fundec fundec var || any_local_reachable) -> true (* keep caller locals, provided they were not passed to the function *)
         | Some (Arg _) -> true (* keep caller args *)
         | Some ((Local _ | Global _)) when not (RD.mem_var new_fun_rel var) -> false (* remove locals and globals, for which no record exists in the new_fun_apr *)
         | Some ((Local v | Global v)) when not (TaintPartialContexts.VS.mem v tainted_vars) -> true (* keep locals and globals, which have not been touched by the call *)
@@ -439,20 +435,17 @@ struct
 
   let combine_assign man r fe f args fc fun_st (f_ask : Queries.ask) =
     let unify_st = man.local in
-    if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then (
-      let unify_st' = match r with
-        | Some lv ->
+    if RD.Tracked.type_tracked (Cilfacade.fundec_return_type f) then
+      let unify_st' = Option.map_default (fun lv ->
           let ask = Analyses.ask_of_man man in
           assign_to_global_wrapper ask man.global man.sideg unify_st lv (fun st v ->
               let rel = RD.assign_var st.rel (RV.local v) RV.return in
               assert_type_bounds ask rel v (* TODO: should be done in return instead *)
             )
-        | None ->
-          unify_st
+        ) unify_st r
       in
       RD.remove_vars_with unify_st'.rel [RV.return]; (* mutates! *)
       unify_st'
-    )
     else
       unify_st
 

src/analyses/assert.ml

@@ -18,10 +18,7 @@ struct
     let check_assert e st =
       match man.ask (Queries.EvalInt e) with
       | v when Queries.ID.is_bot v -> `Bot
-      | v ->
-        match Queries.ID.to_bool v with
-        | Some b -> `Lifted b
-        | None -> `Top
+      | v -> Option.map_default (fun b -> `Lifted b) `Top (Queries.ID.to_bool v)
     in
     let expr = CilType.Exp.show e in
     let warn warn_fn ?annot msg = if check then