Skip to content

Commit 0604e65

Browse files
michael-schwarzmichael-schwarz
committed
Cleanup option related code
1 parent 746d436 commit 0604e65

File tree

11 files changed

+146
-232
lines changed

11 files changed

+146
-232
lines changed

‎src/analyses/abortUnless.ml‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -32,10 +32,7 @@ struct
3232
| [arg] when isIntegralType arg.vtype ->
3333
(match man.ask (EvalInt (Lval (Var arg, NoOffset))) with
3434
| v when Queries.ID.is_bot v -> false
35-
| v ->
36-
match Queries.ID.to_bool v with
37-
| Some b -> b
38-
| None -> false)
35+
| v -> BatOption.default false (Queries.ID.to_bool v))
3936
| _ ->
4037
(* should not happen, man.local should always be false in this case *)
4138
false

‎src/analyses/accessAnalysis.ml‎

Lines changed: 6 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -79,10 +79,7 @@ struct
7979
man.local
8080

8181
let return man exp fundec : D.t =
82-
begin match exp with
83-
| Some exp -> access_one_top man Read false exp
84-
| None -> ()
85-
end;
82+
Option.iter (access_one_top man Read false) exp;
8683
man.local
8784

8885
let body man f : D.t =
@@ -99,9 +96,7 @@ struct
9996
LibraryDesc.Accesses.iter desc.accs (fun {kind; deep = reach} exp ->
10097
access_one_top ~deref:true man kind reach exp (* access dereferenced using special accesses *)
10198
) arglist;
102-
(match lv with
103-
| Some x -> access_one_top ~deref:true man Write false (AddrOf x)
104-
| None -> ());
99+
Option.iter (fun x -> access_one_top ~deref:true man Write false (AddrOf x)) lv;
105100
List.iter (access_one_top man Read false) arglist; (* always read all argument expressions without dereferencing *)
106101
man.local
107102

@@ -115,19 +110,15 @@ struct
115110
au
116111

117112
let combine_assign man lv fexp f args fc al f_ask =
118-
begin match lv with
119-
| None -> ()
120-
| Some lval -> access_one_top ~deref:true man Write false (AddrOf lval)
121-
end;
113+
Option.iter (fun lval -> access_one_top ~deref:true man Write false (AddrOf lval)) lv;
122114
man.local
123115

124116

125117
let threadspawn man ~multiple lval f args fman =
126118
(* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
127-
begin match lval with
128-
| None -> ()
129-
| Some lval -> access_one_top ~force:true ~deref:true man Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
130-
end;
119+
Option.iter (fun lval ->
120+
access_one_top ~force:true ~deref:true man Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
121+
) lval;
131122
man.local
132123

133124
let query man (type a) (q: a Queries.t): a Queries.result =

‎src/analyses/assert.ml‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,7 @@ struct
1818
let check_assert e st =
1919
match man.ask (Queries.EvalInt e) with
2020
| v when Queries.ID.is_bot v -> `Bot
21-
| v ->
22-
match Queries.ID.to_bool v with
23-
| Some b -> `Lifted b
24-
| None -> `Top
21+
| v -> Option.map_default (fun b -> `Lifted b) `Top (Queries.ID.to_bool v)
2522
in
2623
let expr = CilType.Exp.show e in
2724
let warn warn_fn ?annot msg = if check then

‎src/analyses/base.ml‎

Lines changed: 108 additions & 160 deletions
Large diffs are not rendered by default.

‎src/analyses/baseInvariant.ml‎

Lines changed: 16 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -305,9 +305,7 @@ struct
305305
* If the upper bound of a is divisible by b, we can also meet with the result of a/b*b - c to get the precise [3,3].
306306
* If b is negative we have to look at the lower bound. *)
307307
let is_divisible bound =
308-
match bound a with
309-
| Some ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some Z.zero
310-
| None -> false
308+
GobOption.exists (fun ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some Z.zero) (bound a)
311309
in
312310
let max_pos = match ID.maximal b with None -> true | Some x -> Z.compare x Z.zero >= 0 in
313311
let min_neg = match ID.minimal b with None -> true | Some x -> Z.compare x Z.zero < 0 in
@@ -735,6 +733,7 @@ struct
735733
| _ -> Int c
736734
in
737735
(* handle special calls *)
736+
let default () = update_lval c x c' ID.pretty in
738737
begin match x, t with
739738
| (Var v, offs), TInt (ik, _) ->
740739
let tmpSpecial = man.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in
@@ -744,24 +743,21 @@ struct
744743
let c' = ID.cast_to ik c in (* different ik! *)
745744
inv_exp (Int (ID.join c' (ID.neg c'))) xInt st
746745
| tmpSpecial ->
747-
begin match ID.to_bool c with
748-
| Some tv ->
749-
begin match tmpSpecial with
750-
| `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
751-
| `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
752-
(* should be correct according to C99 standard*)
753-
(* The following do to_bool and of_bool to convert Not{0} into 1 for downstream float inversions *)
754-
| `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
755-
| `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
756-
| `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
757-
| `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
758-
| `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
759-
| _ -> update_lval c x c' ID.pretty
760-
end
761-
| None -> update_lval c x c' ID.pretty
762-
end
746+
BatOption.map_default_delayed (fun tv ->
747+
match tmpSpecial with
748+
| `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st
749+
| `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st
750+
(* should be correct according to C99 standard*)
751+
(* The following do to_bool and of_bool to convert Not{0} into 1 for downstream float inversions *)
752+
| `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st
753+
| `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st
754+
| `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
755+
| `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
756+
| `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
757+
| _ -> default ()
758+
) default (ID.to_bool c)
763759
end
764-
| _, _ -> update_lval c x c' ID.pretty
760+
| _, _ -> default ()
765761
end
766762
| Float c ->
767763
let c' = match t with

‎src/analyses/extractPthread.ml‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -643,11 +643,7 @@ module Codegen = struct
643643
let end_label = res_id ^ "_end" in
644644
let goto = goto_str % label in
645645
let goto_start_node =
646-
match List.find is_start_node nodes with
647-
| Some node ->
648-
goto node
649-
| None ->
650-
""
646+
Option.map_default goto "" (List.find is_start_node nodes)
651647
in
652648
let called_funs = ref [] in
653649
let str_edge (a, action, b) =

‎src/analyses/loopTermination.ml‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -75,9 +75,7 @@ struct
7575
| Queries.MustTermLoop loop_statement ->
7676
let multithreaded = man.ask Queries.IsEverMultiThreaded in
7777
(not multithreaded)
78-
&& (match G.find_opt (`Lifted loop_statement) (man.global ()) with
79-
Some b -> b
80-
| None -> false)
78+
&& (BatOption.default false (G.find_opt (`Lifted loop_statement) (man.global ())))
8179
| Queries.MustTermAllLoops ->
8280
let multithreaded = man.ask Queries.IsEverMultiThreaded in
8381
if multithreaded then (

‎src/analyses/malloc_null.ml‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -166,14 +166,13 @@ struct
166166
let return man (exp:exp option) (f:fundec) : D.t =
167167
let remove_var x v = List.fold_right D.remove (to_addrs v) x in
168168
let nst = List.fold_left remove_var man.local (f.slocals @ f.sformals) in
169-
match exp with
170-
| Some ret ->
169+
BatOption.map_default (fun ret ->
171170
warn_deref_exp (Analyses.ask_of_man man) man.local ret;
172-
begin match get_concrete_exp ret man.global man.local with
173-
| Some ev when might_be_null (Analyses.ask_of_man man) ev man.global man.local ->
174-
D.add (return_addr ()) nst
175-
| _ -> nst end
176-
| None -> nst
171+
match get_concrete_exp ret man.global man.local with
172+
| Some ev when might_be_null (Analyses.ask_of_man man) ev man.global man.local ->
173+
D.add (return_addr ()) nst
174+
| _ -> nst
175+
) nst exp
177176

178177
(* Function calls *)
179178

‎src/autoTune.ml‎

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -97,15 +97,10 @@ let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> Functi
9797
let findMallocWrappers () =
9898
let isMalloc f =
9999
Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
100-
if LibraryFunctions.is_special f then (
100+
if LibraryFunctions.is_special f then
101101
let desc = LibraryFunctions.find f in
102-
match functionArgs f with
103-
| None -> false
104-
| Some args ->
105-
match desc.special args with
106-
| Malloc _ -> true
107-
| _ -> false
108-
)
102+
let args = functionArgs f in
103+
GobOption.exists (fun args -> match desc.special args with Malloc _ -> true | _ -> false) args
109104
else
110105
false
111106
in

‎src/maingoblint.ml‎

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -214,12 +214,7 @@ let parse_arguments () =
214214
let anon_arg = set_string "files[+]" in
215215
let arg_speclist = Arg_complete.arg_speclist (Lazy.force option_spec_list) in
216216
Arg.parse arg_speclist anon_arg "Look up options using 'goblint --help'.";
217-
begin match !writeconffile with
218-
| Some writeconffile ->
219-
GobConfig.write_file writeconffile;
220-
raise Stdlib.Exit
221-
| None -> ()
222-
end;
217+
GobOption.iter (fun writeconffile -> GobConfig.write_file writeconffile; raise Stdlib.Exit) !writeconffile;
223218
handle_options ();
224219
if not (get_bool "server.enabled") && get_string_list "files" = [] then (
225220
Logs.error "No files for Goblint?";

0 commit comments

Comments
 (0)