From 1486b920848298ffdcf52383a90a60a9e118da07 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 26 May 2017 09:22:50 -0700 Subject: [PATCH] [inferbo] Renamed a few Itv values Reviewed By: jvillard Differential Revision: D5137445 fbshipit-source-id: f16b68e --- .../src/bufferoverrun/bufferOverrunChecker.ml | 8 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 25 +- .../bufferoverrun/bufferOverrunSemantics.ml | 340 +++++++++--------- infer/src/bufferoverrun/itv.ml | 61 ++-- 4 files changed, 217 insertions(+), 217 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 192166ead..169cb67ed 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -36,7 +36,7 @@ struct type extras = Typ.Procname.t -> Procdesc.t option let set_uninitialized (typ : Typ.t) loc mem = match typ.desc with - | Tint _ | Tfloat _ -> Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem + | Tint _ | Tfloat _ -> Dom.Mem.weak_update_heap loc Dom.Val.Itv.top mem | _ -> mem (* NOTE: heuristic *) @@ -78,13 +78,13 @@ struct let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate = fun ret mem -> match ret with - | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.nat_itv mem + | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.Itv.nat mem | _ -> mem let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate = fun ret mem -> match ret with - Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.top_itv mem + Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.Itv.top mem | None -> mem let model_infer_print @@ -236,7 +236,7 @@ struct let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in Dom.Val.subst ret_val subst_map |> Dom.Val.normalize (* normalize bottom *) - | _ -> Dom.Val.top_itv + | _ -> Dom.Val.Itv.top let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit = fun instr pre post -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index efc1062c7..b9f191aaa 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -265,17 +265,9 @@ struct let get_all_locs : t -> PowLoc.t = fun x -> PowLoc.join x.powloc (get_array_locs x) - let top_itv : t - = { bot with itv = Itv.top } + let of_itv itv = { bot with itv } - let pos_itv : t - = { bot with itv = Itv.pos } - - let nat_itv : t - = { bot with itv = Itv.nat } - - let of_int : int -> t - = fun n -> { bot with itv = Itv.of_int n } + let of_int n = of_itv (Itv.of_int n) let of_itv : Itv.t -> t = fun itv -> { bot with itv } @@ -286,9 +278,6 @@ struct let of_array_blk : ArrayBlk.astate -> t = fun a -> { bot with arrayblk = a } - let zero : t - = of_int 0 - let modify_itv : Itv.t -> t -> t = fun i x -> { x with itv = i } @@ -414,6 +403,14 @@ struct let pp_summary : F.formatter -> t -> unit = fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk + + module Itv = + struct + let nat = of_itv Itv.nat + let m1_255 = of_itv Itv.m1_255 + let pos = of_itv Itv.pos + let top = of_itv Itv.top + end end module Stack = @@ -478,7 +475,7 @@ struct let find : Loc.t -> astate -> Val.t = fun l m -> try find l m with - | Not_found -> Val.top_itv + | Not_found -> Val.Itv.top let find_set : PowLoc.t -> astate -> Val.t = fun locs mem -> diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 2a068ccd7..8d212b309 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -24,23 +24,23 @@ struct let eval_const : Const.t -> Val.t = function - | Const.Cint intlit -> (try Val.of_int (IntLit.to_int intlit) with _ -> Val.top_itv) - | Const.Cfloat f -> f |> int_of_float |> Val.of_int - | _ -> Val.top_itv (* TODO *) + | Const.Cint intlit -> (try Val.of_int (IntLit.to_int intlit) with _ -> Val.Itv.top) + | Const.Cfloat f -> f |> int_of_float |> Val.of_int + | _ -> Val.Itv.top (* TODO *) let sizeof_ikind : Typ.ikind -> int = function - | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> 1 - | Typ.IInt | Typ.IUInt -> 4 - | Typ.IShort | Typ.IUShort -> 2 - | Typ.ILong | Typ.IULong -> 4 - | Typ.ILongLong | Typ.IULongLong -> 8 - | Typ.I128 | Typ.IU128 -> 16 + | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> 1 + | Typ.IInt | Typ.IUInt -> 4 + | Typ.IShort | Typ.IUShort -> 2 + | Typ.ILong | Typ.IULong -> 4 + | Typ.ILongLong | Typ.IULongLong -> 8 + | Typ.I128 | Typ.IU128 -> 16 let sizeof_fkind : Typ.fkind -> int = function - | Typ.FFloat -> 4 - | Typ.FDouble | Typ.FLongDouble -> 8 + | Typ.FFloat -> 4 + | Typ.FDouble | Typ.FLongDouble -> 8 (* NOTE: assume 32bit machine *) let rec sizeof (typ : Typ.t) : int = @@ -58,60 +58,60 @@ struct = fun e1 e2 m -> match e1, e2 with | Exp.Var x1, Exp.Var x2 -> - (match Mem.find_alias x1 m, Mem.find_alias x2 m with - | Some x1', Some x2' -> Pvar.equal x1' x2' - | _, _ -> false) + (match Mem.find_alias x1 m, Mem.find_alias x2 m with + | Some x1', Some x2' -> Pvar.equal x1' x2' + | _, _ -> false) | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) -> - Unop.equal uop1 uop2 && must_alias e1' e2' m + Unop.equal uop1 uop2 && must_alias e1' e2' m | Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) -> - Binop.equal bop1 bop2 - && must_alias e11 e21 m - && must_alias e12 e22 m + Binop.equal bop1 bop2 + && must_alias e11 e21 m + && must_alias e12 e22 m | Exp.Exn t1, Exp.Exn t2 -> must_alias t1 t2 m | Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2 | Exp.Cast (t1, e1'), Exp.Cast (t2, e2') -> - Typ.equal t1 t2 && must_alias e1' e2' m + Typ.equal t1 t2 && must_alias e1' e2' m | Exp.Lvar x1, Exp.Lvar x2 -> - Pvar.equal x1 x2 + Pvar.equal x1 x2 | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) -> - must_alias e1 e2 m && Fieldname.equal fld1 fld2 + must_alias e1 e2 m && Fieldname.equal fld1 fld2 | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) -> - must_alias e11 e21 m && must_alias e12 e22 m + must_alias e11 e21 m && must_alias e12 e22 m | Exp.Sizeof {nbytes=Some nbytes1}, Exp.Sizeof {nbytes=Some nbytes2} -> - Int.equal nbytes1 nbytes2 + Int.equal nbytes1 nbytes2 | Exp.Sizeof {typ=t1; dynamic_length=dynlen1; subtype=subt1}, Exp.Sizeof {typ=t2; dynamic_length=dynlen2; subtype=subt2} -> - Typ.equal t1 t2 - && must_alias_opt dynlen1 dynlen2 m - && Int.equal (Subtype.compare subt1 subt2) 0 + Typ.equal t1 t2 + && must_alias_opt dynlen1 dynlen2 m + && Int.equal (Subtype.compare subt1 subt2) 0 | _, _ -> false - and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool - = fun e1_opt e2_opt m -> - match e1_opt, e2_opt with - | Some e1, Some e2 -> must_alias e1 e2 m - | None, None -> true - | _, _ -> false + and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool + = fun e1_opt e2_opt m -> + match e1_opt, e2_opt with + | Some e1, Some e2 -> must_alias e1 e2 m + | None, None -> true + | _, _ -> false let comp_rev : Binop.t -> Binop.t = function - | Binop.Lt -> Binop.Gt - | Binop.Gt -> Binop.Lt - | Binop.Le -> Binop.Ge - | Binop.Ge -> Binop.Le - | Binop.Eq -> Binop.Eq - | Binop.Ne -> Binop.Ne - | _ -> assert (false) + | Binop.Lt -> Binop.Gt + | Binop.Gt -> Binop.Lt + | Binop.Le -> Binop.Ge + | Binop.Ge -> Binop.Le + | Binop.Eq -> Binop.Eq + | Binop.Ne -> Binop.Ne + | _ -> assert (false) let comp_not : Binop.t -> Binop.t = function - | Binop.Lt -> Binop.Ge - | Binop.Gt -> Binop.Le - | Binop.Le -> Binop.Gt - | Binop.Ge -> Binop.Lt - | Binop.Eq -> Binop.Ne - | Binop.Ne -> Binop.Eq - | _ -> assert (false) + | Binop.Lt -> Binop.Ge + | Binop.Gt -> Binop.Le + | Binop.Le -> Binop.Gt + | Binop.Ge -> Binop.Lt + | Binop.Eq -> Binop.Ne + | Binop.Ne -> Binop.Eq + | _ -> assert (false) let rec must_alias_cmp : Exp.t -> Mem.astate -> bool = fun e m -> @@ -120,26 +120,26 @@ struct | Exp.BinOp (Binop.Gt, e1, e2) | Exp.BinOp (Binop.Ne, e1, e2) -> must_alias e1 e2 m | Exp.BinOp (Binop.LAnd, e1, e2) -> - must_alias_cmp e1 m || must_alias_cmp e2 m + must_alias_cmp e1 m || must_alias_cmp e2 m | Exp.BinOp (Binop.LOr, e1, e2) -> - must_alias_cmp e1 m && must_alias_cmp e2 m + must_alias_cmp e1 m && must_alias_cmp e2 m | Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) -> - must_alias_cmp e1 m + must_alias_cmp e1 m | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) -> - must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m + must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> - let e1' = Exp.UnOp (Unop.LNot, e1, t) in - let e2' = Exp.UnOp (Unop.LNot, e2, t) in - must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m + let e1' = Exp.UnOp (Unop.LNot, e1, t) in + let e2' = Exp.UnOp (Unop.LNot, e2, t) in + must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) -> - let e1' = Exp.UnOp (Unop.LNot, e1, t) in - let e2' = Exp.UnOp (Unop.LNot, e2, t) in - must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m + let e1' = Exp.UnOp (Unop.LNot, e1, t) in + let e2' = Exp.UnOp (Unop.LNot, e2, t) in + must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m | _ -> false let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t @@ -148,71 +148,71 @@ struct match exp with | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem | Exp.Lvar pvar -> - let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in - let arr = Mem.find_stack_set ploc mem in - ploc |> Val.of_pow_loc |> Val.join arr + let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in + let arr = Mem.find_stack_set ploc mem in + ploc |> Val.of_pow_loc |> Val.join arr | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc | Exp.Const c -> eval_const c | Exp.Cast (_, e) -> eval e mem loc | Exp.Lfield (e, fn, _) -> - eval e mem loc - |> Val.get_array_locs - |> Fn.flip PowLoc.append_field fn - |> Val.of_pow_loc + eval e mem loc + |> Val.get_array_locs + |> Fn.flip PowLoc.append_field fn + |> Val.of_pow_loc | Exp.Lindex (e1, _) -> - let arr = eval e1 mem loc |> Val.get_array_blk in (* must have array blk *) - (* let idx = eval e2 mem loc in *) - let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in - (* if nested array, add the array blk *) - let arr = Mem.find_heap_set ploc mem in - Val.join (Val.of_pow_loc ploc) arr + let arr = eval e1 mem loc |> Val.get_array_blk in (* must have array blk *) + (* let idx = eval e2 mem loc in *) + let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in + (* if nested array, add the array blk *) + let arr = Mem.find_heap_set ploc mem in + Val.join (Val.of_pow_loc ploc) arr | Exp.Sizeof {nbytes=Some size} -> Val.of_int size | Exp.Sizeof {typ; nbytes=None} -> Val.of_int (sizeof typ) | Exp.Exn _ - | Exp.Closure _ -> Val.top_itv + | Exp.Closure _ -> Val.Itv.top - and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t - = fun unop e mem loc -> - let v = eval e mem loc in - match unop with - | Unop.Neg -> Val.neg v - | Unop.BNot -> Val.unknown_bit v - | Unop.LNot -> Val.lnot v + and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t + = fun unop e mem loc -> + let v = eval e mem loc in + match unop with + | Unop.Neg -> Val.neg v + | Unop.BNot -> Val.unknown_bit v + | Unop.LNot -> Val.lnot v - and eval_binop - : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t - = fun binop e1 e2 mem loc -> - let v1 = eval e1 mem loc in - let v2 = eval e2 mem loc in - match binop with - | Binop.PlusA -> - Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2) - | Binop.PlusPI -> Val.plus_pi v1 v2 - | Binop.MinusA -> - Val.joins - [ Val.minus v1 v2 - ; Val.minus_pi v1 v2 - ; Val.minus_pp v1 v2 ] - | Binop.MinusPI -> Val.minus_pi v1 v2 - | Binop.MinusPP -> Val.minus_pp v1 v2 - | Binop.Mult -> Val.mult v1 v2 - | Binop.Div -> Val.div v1 v2 - | Binop.Mod -> Val.mod_sem v1 v2 - | Binop.Shiftlt -> Val.shiftlt v1 v2 - | Binop.Shiftrt -> Val.shiftrt v1 v2 - | Binop.Lt -> Val.lt_sem v1 v2 - | Binop.Gt -> Val.gt_sem v1 v2 - | Binop.Le -> Val.le_sem v1 v2 - | Binop.Ge -> Val.ge_sem v1 v2 - | Binop.Eq -> Val.eq_sem v1 v2 - | Binop.Ne -> Val.ne_sem v1 v2 - | Binop.BAnd - | Binop.BXor - | Binop.BOr -> Val.unknown_bit v1 - | Binop.LAnd -> Val.land_sem v1 v2 - | Binop.LOr -> Val.lor_sem v1 v2 - | Binop.PtrFld -> raise Not_implemented + and eval_binop + : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t + = fun binop e1 e2 mem loc -> + let v1 = eval e1 mem loc in + let v2 = eval e2 mem loc in + match binop with + | Binop.PlusA -> + Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2) + | Binop.PlusPI -> Val.plus_pi v1 v2 + | Binop.MinusA -> + Val.joins + [ Val.minus v1 v2 + ; Val.minus_pi v1 v2 + ; Val.minus_pp v1 v2 ] + | Binop.MinusPI -> Val.minus_pi v1 v2 + | Binop.MinusPP -> Val.minus_pp v1 v2 + | Binop.Mult -> Val.mult v1 v2 + | Binop.Div -> Val.div v1 v2 + | Binop.Mod -> Val.mod_sem v1 v2 + | Binop.Shiftlt -> Val.shiftlt v1 v2 + | Binop.Shiftrt -> Val.shiftrt v1 v2 + | Binop.Lt -> Val.lt_sem v1 v2 + | Binop.Gt -> Val.gt_sem v1 v2 + | Binop.Le -> Val.le_sem v1 v2 + | Binop.Ge -> Val.ge_sem v1 v2 + | Binop.Eq -> Val.eq_sem v1 v2 + | Binop.Ne -> Val.ne_sem v1 v2 + | Binop.BAnd + | Binop.BXor + | Binop.BOr -> Val.unknown_bit v1 + | Binop.LAnd -> Val.land_sem v1 v2 + | Binop.LOr -> Val.lor_sem v1 v2 + | Binop.PtrFld -> raise Not_implemented let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string = fun proc_name node inst_num dimension -> @@ -238,25 +238,25 @@ struct = fun e mem -> match e with | Exp.Var x -> - (match Mem.find_alias x mem with - | Some x' -> - let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in - let v' = Val.prune_zero v in - Mem.update_mem (PowLoc.singleton lv) v' mem - | None -> mem) + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_zero v in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> - (match Mem.find_alias x mem with - | Some x' -> - let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in - let itv_v = - if Itv.is_bot (Val.get_itv v) then Itv.bot else - Val.get_itv Val.zero - in - let v' = Val.modify_itv itv_v v in - Mem.update_mem (PowLoc.singleton lv) v' mem - | None -> mem) + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let itv_v = + if Itv.is_bot (Val.get_itv v) then Itv.bot else + Itv.false_sem + in + let v' = Val.modify_itv itv_v v in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) | _ -> mem let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate @@ -266,29 +266,29 @@ struct | Exp.BinOp (Binop.Gt as comp, Exp.Var x, e') | Exp.BinOp (Binop.Le as comp, Exp.Var x, e') | Exp.BinOp (Binop.Ge as comp, Exp.Var x, e') -> - (match Mem.find_alias x mem with - | Some x' -> - let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in - let v' = Val.prune_comp comp v (eval e' mem loc) in - Mem.update_mem (PowLoc.singleton lv) v' mem - | None -> mem) + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_comp comp v (eval e' mem loc) in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> - (match Mem.find_alias x mem with - | Some x' -> - let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in - let v' = Val.prune_eq v (eval e' mem loc) in - Mem.update_mem (PowLoc.singleton lv) v' mem - | None -> mem) + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_eq v (eval e' mem loc) in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> - (match Mem.find_alias x mem with - | Some x' -> - let lv = Loc.of_pvar x' in - let v = Mem.find_heap lv mem in - let v' = Val.prune_ne v (eval e' mem loc) in - Mem.update_mem (PowLoc.singleton lv) v' mem - | None -> mem) + (match Mem.find_alias x mem with + | Some x' -> + let lv = Loc.of_pvar x' in + let v = Mem.find_heap lv mem in + let v' = Val.prune_ne v (eval e' mem loc) in + Mem.update_mem (PowLoc.singleton lv) v' mem + | None -> mem) | _ -> mem let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate @@ -300,7 +300,7 @@ struct | Exp.BinOp (Binop.Ge as c, e', Exp.Var x) | Exp.BinOp (Binop.Eq as c, e', Exp.Var x) | Exp.BinOp (Binop.Ne as c, e', Exp.Var x) -> - prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem + prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem | _ -> mem let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool @@ -322,23 +322,23 @@ struct in match e with | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> - prune e loc mem + prune e loc mem | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> - prune (Exp.UnOp (Unop.LNot, e, None)) loc mem + prune (Exp.UnOp (Unop.LNot, e, None)) loc mem | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> prune (Exp.Var x) loc mem | Exp.BinOp (Binop.LAnd, e1, e2) -> - mem |> prune e1 loc |> prune e2 loc + mem |> prune e1 loc |> prune e2 loc | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> - mem - |> prune (Exp.UnOp (Unop.LNot, e1, t)) loc - |> prune (Exp.UnOp (Unop.LNot, e2, t)) loc + mem + |> prune (Exp.UnOp (Unop.LNot, e1, t)) loc + |> prune (Exp.UnOp (Unop.LNot, e2, t)) loc | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Gt as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ge as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq as c, e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) -> - prune (Exp.BinOp (comp_not c, e1, e2)) loc mem + prune (Exp.BinOp (comp_not c, e1, e2)) loc mem | _ -> mem let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list @@ -382,15 +382,15 @@ struct let add_pair_ptr typ v1 v2 pairs = match typ.Typ.desc with | Typ.Tptr ({desc=Tstruct typename}, _) -> - (match Tenv.lookup tenv typename with - | Some str -> - let fns = List.map ~f:get_field_name str.Typ.Struct.fields in - List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns - | _ -> pairs) + (match Tenv.lookup tenv typename with + | Some str -> + let fns = List.map ~f:get_field_name str.Typ.Struct.fields in + List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns + | _ -> pairs) | Typ.Tptr (_ ,_) -> - let v1' = deref_ptr v1 callee_mem in - let v2' = deref_ptr v2 caller_mem in - add_pair_val v1' v2' pairs + let v1' = deref_ptr v1 callee_mem in + let v2' = deref_ptr v2 caller_mem in + add_pair_val v1' v2' pairs | _ -> pairs in [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual @@ -401,10 +401,10 @@ struct let add_pair map (formal, actual) = match formal with | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 -> - let (symbol, coeff) = Itv.SymLinear.choose se1 in - if Int.equal coeff 1 - then Itv.SubstMap.add symbol actual map - else assert false + let (symbol, coeff) = Itv.SymLinear.choose se1 in + if Int.equal coeff 1 + then Itv.SubstMap.add symbol actual map + else assert false | _ -> assert false in List.fold ~f:add_pair ~init:Itv.SubstMap.empty pairs @@ -431,6 +431,6 @@ struct in let formals = get_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in - list_fold2_def ~default:Val.top_itv ~f:add_pair formals actuals ~init:[] + list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:[] |> subst_map_of_pairs end diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index dc9c34bae..fbbfb7674 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -189,7 +189,6 @@ let pp_min_max : F.formatter -> min_max_t -> unit | Min -> F.fprintf fmt "min" | Max -> F.fprintf fmt "max" - let pp : F.formatter -> t -> unit = fun fmt -> function | MInf -> F.fprintf fmt "-oo" @@ -207,6 +206,14 @@ let pp : F.formatter -> t -> unit let of_int : int -> t = fun n -> Linear (n, SymLinear.empty) +let zero = of_int 0 + +let one = of_int 1 + +let minus_one = of_int ~-1 + +let _255 = of_int 255 + let of_sym : SymLinear.t -> t = fun s -> Linear (0, s) @@ -536,8 +543,9 @@ struct let pp : F.formatter -> t -> unit = fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Bound.pp l Bound.pp u - let of_int : int -> t - = fun n -> (Bound.of_int n, Bound.of_int n) + let of_bound bound = (bound, bound) + + let of_int n = of_bound (Bound.of_int n) let get_new_sym : Typ.Procname.t -> t = fun pname -> @@ -551,29 +559,23 @@ struct let upper = Bound.of_sym (SymLinear.make pname (i+1)) in (lower, upper) - let top : t - = (Bound.MInf, Bound.PInf) + let m1_255 = (Bound.minus_one, Bound._255) - let pos : t - = (Bound.of_int 1, Bound.PInf) + let nat = (Bound.zero, Bound.PInf) - let nat : t - = (Bound.of_int 0, Bound.PInf) + let one = of_bound Bound.one - let zero : t - = of_int 0 + let pos = (Bound.one, Bound.PInf) - let one : t - = of_int 1 + let top = (Bound.MInf, Bound.PInf) - let true_sem : t - = one + let zero = of_bound Bound.zero - let false_sem : t - = zero + let true_sem = one - let unknown_bool : t - = (Bound.of_int 0, Bound.of_int 1) + let false_sem = zero + + let unknown_bool = join false_sem true_sem let is_true : t -> bool = fun (l, u) -> Bound.le (Bound.of_int 1) l || Bound.le u (Bound.of_int (-1)) @@ -869,20 +871,21 @@ let is_finite : t -> bool | NonBottom x -> ItvPure.is_finite x | Bottom -> false -let zero : t - = of_int 0 +let false_sem = NonBottom ItvPure.false_sem -let one : t - = of_int 1 +let m1_255 = NonBottom ItvPure.m1_255 + +let nat = NonBottom ItvPure.nat + +let one = NonBottom ItvPure.one + +let pos = NonBottom ItvPure.pos -let pos : t - = NonBottom ItvPure.pos +let true_sem = NonBottom ItvPure.true_sem -let nat : t - = NonBottom ItvPure.nat +let unknown_bool = NonBottom ItvPure.unknown_bool -let unknown_bool : t - = NonBottom ItvPure.unknown_bool +let zero = NonBottom ItvPure.zero let make : Bound.t -> Bound.t -> t = fun l u -> if Bound.lt u l then Bottom else NonBottom (ItvPure.make l u)