diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 0d5b7d36f..b8106ff00 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -52,7 +52,7 @@ module ArrInfo = struct , C {offset= offset2; size= size2; stride= stride2} ) -> let offset = let thresholds = - if Itv.eq size1 size2 then Option.to_list (Itv.is_const size1) else [] + if Itv.eq size1 size2 then Option.to_list (Itv.get_const size1) else [] in Itv.widen_thresholds ~thresholds ~prev:offset1 ~next:offset2 ~num_iters in @@ -224,7 +224,7 @@ module ArrInfo = struct fun new_stride arr -> match arr with | C {offset; size; stride} -> - Option.value_map (Itv.is_const stride) ~default:arr ~f:(fun stride -> + Option.value_map (Itv.get_const stride) ~default:arr ~f:(fun stride -> assert ((not Z.(equal stride zero)) && not Z.(equal new_stride zero)) ; if Z.equal new_stride stride then arr else diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 97a50cea4..303a36276 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -200,7 +200,7 @@ module SymLinear = struct plus x to_add - let is_same_symbol x1 x2 = + let get_same_one_symbol x1 x2 = match (get_one_symbol_opt x1, get_one_symbol_opt x2) with | Some s1, Some s2 when Symb.Symbol.paths_equal s1 s2 -> Some (Symb.Symbol.path s1) @@ -856,7 +856,7 @@ module Bound = struct let widen_u : t -> t -> t = fun x y -> widen_u_thresholds ~thresholds:[] x y - let is_const : t -> Z.t option = + let get_const : t -> Z.t option = fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None @@ -1157,10 +1157,10 @@ module Bound = struct if phys_equal a a' && phys_equal b b' then x else mk_MinMaxB (m, a', b') - let is_same_symbol b1 b2 = + let get_same_one_symbol b1 b2 = match (b1, b2) with | Linear (n1, se1), Linear (n2, se2) when Z.(equal n1 zero) && Z.(equal n2 zero) -> - SymLinear.is_same_symbol se1 se2 + SymLinear.get_same_one_symbol se1 se2 | _ -> None @@ -1282,7 +1282,7 @@ module NonNegativeBound = struct | Bound.MInf -> assert false | b -> ( - match Bound.is_const b with + match Bound.get_const b with | None -> Symbolic (b, trace) | Some c -> diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 62446edb6..a4820df4d 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -90,7 +90,7 @@ module Bound : sig val widen_u_thresholds : thresholds:Z.t list -> t -> t -> t - val is_const : t -> Z.t option + val get_const : t -> Z.t option val plus_l : weak:bool -> t -> t -> t @@ -120,7 +120,7 @@ module Bound : sig val simplify_min_one : t -> t - val is_same_symbol : t -> t -> Symb.SymbolPath.t option + val get_same_one_symbol : t -> t -> Symb.SymbolPath.t option val exists_str : f:(string -> bool) -> t -> bool end diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index bb33054e2..89c57d3a7 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -259,7 +259,7 @@ module TransferFunctions = struct let length = Sem.eval_array_locs_length (Sem.eval_locs arr_exp mem) mem |> Dom.Val.get_itv in - Option.map (Itv.is_const length) + Option.map (Itv.get_const length) ~f:(Dom.ModeledRange.of_big_int ~trace:(Bounds.BoundTrace.of_loop location)) | _ -> None diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index db5b84df4..7f426d992 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -394,7 +394,7 @@ module Val = struct else pruned_itv in let itv_thresholds = - Option.value_map (Itv.is_const y.itv) ~default:x.itv_thresholds ~f:(fun z -> + Option.value_map (Itv.get_const y.itv) ~default:x.itv_thresholds ~f:(fun z -> x.itv_thresholds |> ItvThresholds.add Z.(z - one) |> ItvThresholds.add z diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml index 3e3bd2c87..2cd85be49 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml @@ -858,12 +858,12 @@ module Make (Manager : Manager_S) = struct let lb, ub = (Itv.ItvPure.lb itv_pure, Itv.ItvPure.ub itv_pure) in Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp -> let tcons_lb = - Option.map (Itv.Bound.is_const lb) ~f:(fun lb -> + Option.map (Itv.Bound.get_const lb) ~f:(fun lb -> let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_big_int lb) in Tcons1.make sym_minus_lb Tcons1.SUPEQ ) in let tcons_ub = - Option.map (Itv.Bound.is_const ub) ~f:(fun ub -> + Option.map (Itv.Bound.get_const ub) ~f:(fun ub -> let ub_minus_sym = SymExp.minus (SymExp.of_big_int ub) sym_exp in Tcons1.make ub_minus_sym Tcons1.SUPEQ ) in diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 8beaa3937..c5909a288 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -44,7 +44,7 @@ module ItvPure = struct let is_finite : t -> bool = fun (l, u) -> - match (Bound.is_const l, Bound.is_const u) with Some _, Some _ -> true | _, _ -> false + match (Bound.get_const l, Bound.get_const u) with Some _, Some _ -> true | _, _ -> false let have_similar_bounds (l1, u1) (l2, u2) = Bound.are_similar l1 l2 && Bound.are_similar u1 u2 @@ -104,7 +104,7 @@ module ItvPure = struct fun ~markup fmt (l, u) -> if Bound.equal l u then Bound.pp_mark ~markup fmt l else - match Bound.is_same_symbol l u with + match Bound.get_same_one_symbol l u with | Some symbol when Config.bo_debug < 3 -> Symb.SymbolPath.pp_mark ~markup fmt symbol | _ -> @@ -153,9 +153,9 @@ module ItvPure = struct let is_nat : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_pinf u - let is_const : t -> Z.t option = + let get_const : t -> Z.t option = fun (l, u) -> - match (Bound.is_const l, Bound.is_const u) with + match (Bound.get_const l, Bound.get_const u) with | (Some n as z), Some m when Z.equal n m -> z | _, _ -> @@ -257,7 +257,7 @@ module ItvPure = struct let mult : t -> t -> t = fun x y -> - match (is_const x, is_const y) with + match (get_const x, get_const y) with | _, Some n -> mult_const n x | Some n, _ -> @@ -266,17 +266,17 @@ module ItvPure = struct top - let div : t -> t -> t = fun x y -> match is_const y with None -> top | Some n -> div_const x n + let div : t -> t -> t = fun x y -> match get_const y with None -> top | Some n -> div_const x n let mod_sem : t -> t -> t = fun x y -> - match is_const y with + match get_const y with | None -> top | Some n when Z.(equal n zero) -> x (* x % [0,0] does nothing. *) | Some m -> ( - match is_const x with + match get_const x with | Some n -> of_big_int Z.(n mod m) | None -> @@ -291,7 +291,7 @@ module ItvPure = struct (* x << [-1,-1] does nothing. *) let shiftlt : t -> t -> t = fun x y -> - Option.value_map (is_const y) ~default:top ~f:(fun n -> + Option.value_map (get_const y) ~default:top ~f:(fun n -> match Z.to_int n with | n -> if n < 0 then x else mult_const Z.(one lsl n) x @@ -304,7 +304,7 @@ module ItvPure = struct fun x y -> if is_zero x then x else - match is_const y with + match get_const y with | Some n when Z.(leq n zero) -> x | Some n when Z.(n >= of_int 64) -> @@ -317,7 +317,7 @@ module ItvPure = struct let band_sem : t -> t -> t = fun x y -> - match (is_const x, is_const y) with + match (get_const x, get_const y) with | Some x', Some y' -> if Z.(equal x' y') then x else of_big_int Z.(x' land y') | _, _ -> @@ -637,7 +637,7 @@ let set_lb_zero = lift1 ItvPure.set_lb_zero let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv -let is_const : t -> Z.t option = bind1zo ItvPure.is_const +let get_const : t -> Z.t option = bind1zo ItvPure.get_const let is_zero = bind1bool ItvPure.is_zero diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 8ce91543a..6b1fb9c66 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -145,7 +145,7 @@ val of_big_int : Z.t -> t val of_int_lit : IntLit.t -> t -val is_const : t -> Z.t option +val get_const : t -> Z.t option val is_zero : t -> bool