Skip to content

Commit 560eb6f

Browse files
authored
Merge pull request #593 from goblint/remove-catch-all
Fix most catch-alls
2 parents f8627f1 + a5a1229 commit 560eb6f

File tree

12 files changed

+50
-43
lines changed

12 files changed

+50
-43
lines changed

src/analyses/base.ml

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -346,7 +346,7 @@ struct
346346
* which part of an array is involved. *)
347347
let rec get ?(full=false) a (gs: glob_fun) (st: store) (addrs:address) (exp:exp option): value =
348348
let at = AD.get_type addrs in
349-
let firstvar = if M.tracing then try (List.hd (AD.to_var_may addrs)).vname with _ -> "" else "" in
349+
let firstvar = if M.tracing then match AD.to_var_may addrs with [] -> "" | x :: _ -> x.vname else "" in
350350
if M.tracing then M.traceli "get" ~var:firstvar "Address: %a\nState: %a\n" AD.pretty addrs CPA.pretty st.cpa;
351351
(* Finding a single varinfo*offset pair *)
352352
let res =
@@ -929,7 +929,7 @@ struct
929929
| `Address a ->
930930
let slen = List.map String.length (AD.to_string a) in
931931
let lenOf = function
932-
| TArray (_, l, _) -> (try Some (lenOfArray l) with _ -> None)
932+
| TArray (_, l, _) -> (try Some (lenOfArray l) with LenOfArray -> None)
933933
| _ -> None
934934
in
935935
let alen = List.filter_map (fun v -> lenOf v.vtype) (AD.to_var_may a) in
@@ -1107,7 +1107,7 @@ struct
11071107
if M.tracing then M.tracel "setosek" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a\n" x.vname VD.pretty y CPA.pretty z CPA.pretty r;
11081108
r
11091109
in
1110-
let firstvar = if M.tracing then try (List.hd (AD.to_var_may lval)).vname with _ -> "" else "" in
1110+
let firstvar = if M.tracing then match AD.to_var_may lval with [] -> "" | x :: _ -> x.vname else "" in
11111111
let lval_raw = (Option.map (fun x -> Lval x) lval_raw) in
11121112
if M.tracing then M.tracel "set" ~var:firstvar "lval: %a\nvalue: %a\nstate: %a\n" AD.pretty lval VD.pretty value CPA.pretty st.cpa;
11131113
(* Updating a single varinfo*offset pair. NB! This function's type does
@@ -1512,7 +1512,9 @@ struct
15121512
* 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].
15131513
* If b is negative we have to look at the lower bound. *)
15141514
let is_divisible bound =
1515-
try ID.rem (bound a |> Option.get |> ID.of_int ikind) b |> ID.to_int = Some BI.zero with _ -> false
1515+
match bound a with
1516+
| Some ba -> ID.rem (ID.of_int ikind ba) b |> ID.to_int = Some BI.zero
1517+
| None -> false
15161518
in
15171519
let max_pos = match ID.maximal b with None -> true | Some x -> BI.compare x BI.zero >= 0 in
15181520
let min_neg = match ID.minimal b with None -> true | Some x -> BI.compare x BI.zero < 0 in

src/analyses/extract_arinc.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -278,7 +278,7 @@ struct
278278
(* evaluates an argument and returns a list of possible values for that argument. *)
279279
let eval = function
280280
| Pml.EvalSkip -> const None
281-
| Pml.EvalInt -> fun e -> Some (try eval_int e with _ -> eval_id e)
281+
| Pml.EvalInt -> fun e -> Some (try eval_int e with Failure _ -> eval_id e)
282282
| Pml.EvalString -> fun e -> Some (List.map (fun x -> "\""^x^"\"") (eval_str e))
283283
| Pml.EvalEnum f -> fun e -> Some (List.map (fun x -> Option.get (f (int_of_string x))) (eval_int e))
284284
| Pml.AssignIdOfString (res, pos) -> fun e ->

src/analyses/extract_osek.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,7 @@ struct
271271
(* evaluates an argument and returns a list of possible values for that argument. *)
272272
let eval = function
273273
| Pml.EvalSkip -> const None
274-
| Pml.EvalInt -> fun e -> Some (try eval_int e with _ -> eval_id e)
274+
| Pml.EvalInt -> fun e -> Some (try eval_int e with Failure _ -> eval_id e)
275275
| Pml.EvalString -> fun e -> Some (List.map (fun x -> "\""^x^"\"") (eval_str e))
276276
| Pml.EvalEnum f -> fun e -> Some (List.map (fun x -> Option.get (f (int_of_string x))) (eval_int e))
277277
| Pml.AssignIdOfString (res, pos) -> fun e ->

src/analyses/flag.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,7 @@ struct
122122

123123
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
124124
let _ = List.iter no_addr_of_flag arglist in
125-
match f.vname with _ -> D.top ()
125+
D.top ()
126126

127127
let startstate v = D.top ()
128128
let threadenter ctx lval f args = [D.top ()]

src/analyses/osek.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -441,11 +441,11 @@ struct
441441
if not (is_task v.vname) || flagstate = Flags.top() then begin
442442
if !GU.should_warn then begin
443443
let new_acc = ((loc,fl,rv),ust,o) in
444-
let curr : AccValSet.t = try Acc.find acc v with _ -> AccValSet.empty in
444+
let curr : AccValSet.t = Acc.find_default acc v AccValSet.empty in
445445
let neww : AccValSet.t = AccValSet.add (new_acc,flagstate) (remove_acc new_acc curr) in
446446
Acc.replace acc v neww;
447447
accKeys := AccKeySet.add v !accKeys;
448-
let curr = try Hashtbl.find off_pry_with_flag v.vname with _ -> [] in
448+
let curr = Hashtbl.find_default off_pry_with_flag v.vname [] in
449449
let pry = offpry [new_acc] in
450450
Hashtbl.replace off_pry_with_flag v.vname ((flagstate,pry)::curr)
451451
end ;
@@ -584,7 +584,7 @@ struct
584584
| Queries.Priority "" ->
585585
let pry = resourceset_to_priority (List.map names (Mutex.Lockset.ReverseAddrSet.elements ctx.local)) in
586586
Queries.ID.of_int IInt @@ IntOps.BigIntOps.of_int pry (* TODO: what ikind to use for priorities? *)
587-
| Queries.Priority vname -> begin try Queries.ID.of_int IInt @@ IntOps.BigIntOps.of_int (Hashtbl.find offensivepriorities vname) with _ -> Queries.Result.top q end (* TODO: what ikind to use for priorities? *)
587+
| Queries.Priority vname -> begin try Queries.ID.of_int IInt @@ IntOps.BigIntOps.of_int (Hashtbl.find offensivepriorities vname) with Not_found -> Queries.Result.top q end (* TODO: what ikind to use for priorities? *)
588588
| Queries.MayBePublic {global=v; _} ->
589589
let pry = resourceset_to_priority (List.map names (Mutex.Lockset.ReverseAddrSet.elements ctx.local)) in
590590
if pry = min_int then

src/cdomains/intDomain.ml

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -218,7 +218,7 @@ struct
218218
let equal_to (x: int_t) (a: t)=
219219
try
220220
Old.equal_to (BI.to_int64 x) a
221-
with e -> `Top
221+
with Z.Overflow | Failure _ -> `Top
222222

223223
let to_excl_list a = Option.map (List.map BI.of_int64) (Old.to_excl_list a)
224224
let of_excl_list ik xs =
@@ -393,7 +393,7 @@ module Size = struct (* size in bits as int, range as int64 *)
393393
let bit = function (* bits needed for representation *)
394394
| IBool -> 1
395395
| ik -> bytesSizeOfInt ik * 8
396-
let is_int64_big_int x = try let _ = int64_of_big_int x in true with _ -> false
396+
let is_int64_big_int x = Z.fits_int64 x
397397
let card ik = (* cardinality *)
398398
let b = bit ik in
399399
shift_left_big_int unit_big_int b
@@ -822,12 +822,9 @@ struct
822822
| Some (x1, x2) ->
823823
let open Invariant in
824824
let (x1', x2') = BatTuple.Tuple2.mapn (Ints_t.to_bigint) (x1, x2) in
825-
(try
826-
(* Cilfacade.typeOf will fail if c is heap allocated *)
827-
let i1 = if Ints_t.compare (min_int ik) x1 <> 0 then of_exp Cil.(BinOp (Le, kintegerCilint ik x1', c, intType)) else none in
828-
let i2 = if Ints_t.compare x2 (max_int ik) <> 0 then of_exp Cil.(BinOp (Le, c, kintegerCilint ik x2', intType)) else none in
829-
i1 && i2
830-
with e -> None)
825+
let i1 = if Ints_t.compare (min_int ik) x1 <> 0 then of_exp Cil.(BinOp (Le, kintegerCilint ik x1', c, intType)) else none in
826+
let i2 = if Ints_t.compare x2 (max_int ik) <> 0 then of_exp Cil.(BinOp (Le, c, kintegerCilint ik x2', intType)) else none in
827+
i1 && i2
831828
| None -> None
832829

833830
let arbitrary ik =
@@ -2443,11 +2440,9 @@ struct
24432440
let c = Ints_t.to_bigint c in
24442441
Invariant.of_exp Cil.(BinOp (Eq, l, Cil.kintegerCilint ik c, intType))
24452442
| Some (c, m) ->
2446-
let open Cil in
2447-
let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik @@ Ints_t.to_bigint a) (c, m) in
2448-
(try
2449-
Invariant.of_exp (BinOp (Eq, (BinOp (Mod, l, m, TInt(ik,[]))), c, intType))
2450-
with e -> None)
2443+
let open Cil in
2444+
let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik @@ Ints_t.to_bigint a) (c, m) in
2445+
Invariant.of_exp (BinOp (Eq, (BinOp (Mod, l, m, TInt(ik,[]))), c, intType))
24512446
| None -> None
24522447

24532448
let arbitrary ik =
@@ -2656,7 +2651,7 @@ module IntDomTupleImpl = struct
26562651
mapp2 { fp2 = fun (type a) (module I:S with type t = a and type int_t = int_t) -> I.to_incl_list } x |> flat merge
26572652

26582653

2659-
let pretty () = (fun xs -> text "(" ++ (try List.reduce (fun a b -> a ++ text "," ++ b) xs with _ -> nil) ++ text ")") % to_list % mapp { fp = fun (type a) (module I:S with type t = a) -> (* assert sf==I.short; *) I.pretty () } (* NOTE: the version above does something else. also, we ignore the sf-argument here. *)
2654+
let pretty () = (fun xs -> text "(" ++ (try List.reduce (fun a b -> a ++ text "," ++ b) xs with Invalid_argument _ -> nil) ++ text ")") % to_list % mapp { fp = fun (type a) (module I:S with type t = a) -> (* assert sf==I.short; *) I.pretty () } (* NOTE: the version above does something else. also, we ignore the sf-argument here. *)
26602655

26612656

26622657
let refine_functions ik : (t -> t) list =

src/cdomains/lval.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,9 @@ struct
2121
type t = (fieldinfo, Idx.t) offs
2222
include Printable.Std
2323

24-
let is_first_field x = try CilType.Fieldinfo.equal (List.hd x.fcomp.cfields) x with _ -> false
24+
let is_first_field x = match x.fcomp.cfields with
25+
| [] -> false
26+
| f :: _ -> CilType.Fieldinfo.equal f x
2527

2628
let rec cmp_zero_offset : t -> [`MustZero | `MustNonzero | `MayZero] = function
2729
| `NoOffset -> `MustZero

src/cdomains/valueDomain.ml

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -394,16 +394,17 @@ struct
394394
| _ -> log_top __POS__; AD.top_ptr
395395
)
396396
| TArray (ta, l, _) -> (* TODO, why is the length exp option? *)
397-
`Array (match v, Prelude.try_opt Cil.lenOfArray l with
398-
| `Array x, _ (* Some l' when Some l' = CArrays.length x *) -> x (* TODO handle casts between different sizes? *)
397+
(* TODO handle casts between different sizes? *)
398+
`Array (match v with
399+
| `Array x -> x
399400
| _ -> log_top __POS__; CArrays.top ()
400401
)
401402
| TComp (ci,_) -> (* struct/union *)
402403
(* rather clumsy, but our abstract values don't keep their type *)
403404
let same_struct x = (* check if both have the same parent *)
404-
(* compinfo is cyclic, so we only check the name *)
405-
try compFullName (List.hd (Structs.keys x)).fcomp = compFullName (List.hd ci.cfields).fcomp
406-
with _ -> false (* can't say if struct is empty *)
405+
match Structs.keys x, ci.cfields with
406+
| k :: _, f :: _ -> compFullName k.fcomp = compFullName f.fcomp (* compinfo is cyclic, so we only check the name *)
407+
| _, _ -> false (* can't say if struct is empty *)
407408
in
408409
(* 1. casting between structs of different type does not work
409410
* 2. dereferencing a casted pointer works, but is undefined behavior because of the strict aliasing rule (compiler assumes that pointers of different type can never point to the same location)

src/domains/access.ml

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -154,13 +154,14 @@ type var_o = varinfo option
154154
type off_o = offset option
155155

156156
let get_val_type e (vo: var_o) (oo: off_o) : acc_typ =
157-
try (* FIXME: Cilfacade.typeOf fails on our fake variables: (struct s).data *)
158-
let t = Cilfacade.typeOf e in
159-
match vo, oo with
160-
| Some v, Some o -> get_type t (AddrOf (Var v, o))
161-
| Some v, None -> get_type t (AddrOf (Var v, NoOffset))
162-
| _ -> get_type t e
163-
with _ -> get_type voidType e
157+
match Cilfacade.typeOf e with
158+
| t ->
159+
begin match vo, oo with
160+
| Some v, Some o -> get_type t (AddrOf (Var v, o))
161+
| Some v, None -> get_type t (AddrOf (Var v, NoOffset))
162+
| _ -> get_type t e
163+
end
164+
| exception (Cilfacade.TypeOfError _) -> get_type voidType e
164165

165166
let add_one side (e:exp) (w:bool) (conf:int) (ty:acc_typ) (lv:(varinfo*offs) option) a: unit =
166167
if is_ignorable lv then () else begin

src/prelude.ml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ module All = struct
55
let comp2 f g a b = f (g a) (g b)
66
let compareBy ?cmp:(cmp=compare) f = comp2 cmp f
77
let str_remove m s = String.nreplace ~str:s ~sub:m ~by:""
8-
let try_opt f a = try Some (f a) with _ -> None (* reason: match .. with _ does not include exceptions, or-patterns currently not supported for exceptions *)
98

109
(* Sys.time gives runtime in seconds as float *)
1110
let split_time () = (* gives CPU time in h,m,s,ms *)

0 commit comments

Comments
 (0)