diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index fc107271b..b4f0f8113 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -25,17 +25,20 @@ struct | Var of Var.t | Allocsite of Allocsite.t | Field of t * Fieldname.t - [@@deriving compare] + | Unknown + [@@deriving compare] + let unknown = Unknown let rec pp fmt = function | Var v -> - Var.pp F.str_formatter v; - let s = F.flush_str_formatter () in - if s.[0] = '&' then - F.fprintf fmt "%s" (String.sub s 1 (String.length s - 1)) - else F.fprintf fmt "%s" s + Var.pp F.str_formatter v; + let s = F.flush_str_formatter () in + if s.[0] = '&' then + F.fprintf fmt "%s" (String.sub s 1 (String.length s - 1)) + else F.fprintf fmt "%s" s | Allocsite a -> Allocsite.pp fmt a | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Fieldname.pp f + | Unknown -> F.fprintf fmt "Unknown" let is_var = function Var _ -> true | _ -> false let is_logical_var = function | Var (Var.LogicalVar _) -> true @@ -48,7 +51,7 @@ struct let is_return = function | Var (Var.ProgramVar x) -> - Mangled.equal (Pvar.get_name x) Ident.name_return + Mangled.equal (Pvar.get_name x) Ident.name_return | _ -> false end @@ -59,7 +62,10 @@ struct let bot = empty let is_bot = is_empty + let unknown = singleton Loc.unknown let of_pvar pvar = singleton (Loc.of_pvar pvar) let of_id id = singleton (Loc.of_id id) - let append_field ploc fn = fold (fun l -> add (Loc.append_field l fn)) ploc empty + let append_field ploc fn = + if is_bot ploc then singleton Loc.unknown + else fold (fun l -> add (Loc.append_field l fn)) ploc empty end diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a5a4b1bc0..65955d428 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -38,10 +38,10 @@ struct (* NOTE: heuristic *) let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t = function - | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) - | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> (typ, nbytes, length) - | Exp.Sizeof {typ; nbytes} -> (typ, nbytes, Exp.one) - | x -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x) + | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) + | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> (typ, nbytes, length) + | Exp.Sizeof {typ; nbytes} -> (typ, nbytes, Exp.one) + | x -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x) let model_malloc : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node @@ -49,19 +49,19 @@ struct = fun pname ret params node mem -> match ret with | Some (id, _) -> - let set_uninitialized typ loc mem = - match typ.Typ.desc with - | Typ.Tint _ - | Typ.Tfloat _ -> - Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem - | _ -> mem - in - let (typ, stride, length0) = get_malloc_info (List.hd_exn params |> fst) in - let length = Sem.eval length0 mem (CFG.loc node) |> Dom.Val.get_itv in - let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in - mem - |> Dom.Mem.add_stack (Loc.of_id id) v - |> set_uninitialized typ (Dom.Val.get_array_locs v) + let set_uninitialized typ loc mem = + match typ.Typ.desc with + | Typ.Tint _ + | Typ.Tfloat _ -> + Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem + | _ -> mem + in + let (typ, stride, length0) = get_malloc_info (List.hd_exn params |> fst) in + let length = Sem.eval length0 mem (CFG.loc node) |> Dom.Val.get_itv in + let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in + mem + |> Dom.Mem.add_stack (Loc.of_id id) v + |> set_uninitialized typ (Dom.Val.get_array_locs v) | _ -> mem let model_realloc @@ -70,6 +70,14 @@ struct = fun pname ret params node mem -> model_malloc pname ret (List.tl_exn params) node mem + let model_fgetc : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate + = fun ret mem -> + match ret with + | Some (id, _) -> + let itv = Itv.make (Itv.Bound.of_int (-1)) Itv.Bound.PInf in + Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_itv itv) mem + | _ -> mem + let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate = fun ret mem -> match ret with @@ -87,11 +95,11 @@ struct = fun params mem loc -> match params with | (e, _) :: _ -> - if Config.bo_debug >= 1 then - L.err "@[=== Infer Print === at %a@,%a@]%!" - Location.pp loc - Dom.Val.pp (Sem.eval e mem loc); - mem + if Config.bo_debug >= 1 then + L.err "@[=== Infer Print === at %a@,%a@]%!" + Location.pp loc + Dom.Val.pp (Sem.eval e mem loc); + mem | _ -> mem let handle_unknown_call @@ -103,8 +111,8 @@ struct | "malloc" | "__new_array" -> model_malloc pname ret params node mem | "realloc" -> model_realloc pname ret params node mem - | "strlen" - | "fgetc" -> model_natual_itv ret mem + | "strlen" -> model_natual_itv ret mem + | "fgetc" -> model_fgetc ret mem | "infer_print" -> model_infer_print params mem loc | _ -> model_unknown_itv ret mem @@ -148,32 +156,32 @@ struct in let decl_fld (mem, sym_num) (fn, typ, _) = let loc = - mem |> Dom.Mem.find_heap loc |> Dom.Val.get_all_locs |> PowLoc.choose + mem |> Dom.Mem.find_heap loc |> Dom.Val.get_array_locs |> PowLoc.choose in let field = Loc.append_field loc fn in match typ.Typ.desc with | Typ.Tint _ | Typ.Tfloat _ -> - let v = Dom.Val.make_sym pname sym_num in - (Dom.Mem.add_heap field v mem, sym_num + 2) + let v = Dom.Val.make_sym pname sym_num in + (Dom.Mem.add_heap field v mem, sym_num + 2) | Typ.Tptr (typ, _) -> - let offset = Itv.make_sym pname sym_num in - let size = Itv.make_sym pname (sym_num + 2) in - let v = - Sem.eval_array_alloc pname node typ offset size inst_num dimension - in - (Dom.Mem.add_heap field v mem, sym_num + 4) + let offset = Itv.make_sym pname sym_num in + let size = Itv.make_sym pname (sym_num + 2) in + let v = + Sem.eval_array_alloc pname node typ offset size inst_num dimension + in + (Dom.Mem.add_heap field v mem, sym_num + 4) | _ -> - if Config.bo_debug >= 3 then - L.err "decl_fld of unhandled type: %a@." (Typ.pp Pp.text) typ; - (mem, sym_num) + if Config.bo_debug >= 3 then + L.err "decl_fld of unhandled type: %a@." (Typ.pp Pp.text) typ; + (mem, sym_num) in match typ.Typ.desc with | Typ.Tstruct typename -> - (match Tenv.lookup tenv typename with - | Some str -> - List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.Typ.Struct.fields - | _ -> (mem, sym_num + 6)) + (match Tenv.lookup tenv typename with + | Some str -> + List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.Typ.Struct.fields + | _ -> (mem, sym_num + 6)) | _ -> (mem, sym_num + 6) let declare_symbolic_parameter @@ -183,19 +191,19 @@ struct let add_formal (mem, inst_num, sym_num) (pvar, typ) = match typ.Typ.desc with | Typ.Tint _ -> - let v = Dom.Val.make_sym pname sym_num in - let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in - (mem, inst_num + 1, sym_num + 2) + let v = Dom.Val.make_sym pname sym_num in + let mem = Dom.Mem.add_heap (Loc.of_pvar pvar) v mem in + (mem, inst_num + 1, sym_num + 2) | Typ.Tptr (typ, _) -> - let (mem, sym_num) = - declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ - ~inst_num ~sym_num ~dimension:1 mem - in - (mem, inst_num + 1, sym_num) + let (mem, sym_num) = + declare_symbolic_array pname tenv node (Loc.of_pvar pvar) typ + ~inst_num ~sym_num ~dimension:1 mem + in + (mem, inst_num + 1, sym_num) | _ -> - if Config.bo_debug >= 3 then - L.err "declare_symbolic_parameter of unhandled type: %a@." (Typ.pp Pp.text) typ; - (mem, inst_num, sym_num) (* TODO: add other cases if necessary *) + if Config.bo_debug >= 3 then + L.err "declare_symbolic_parameter of unhandled type: %a@." (Typ.pp Pp.text) typ; + (mem, inst_num, sym_num) (* TODO: add other cases if necessary *) in List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc) |> fst3 @@ -208,13 +216,13 @@ struct let callee_exit_mem = Dom.Summary.get_output summary in match callee_pdesc with | Some pdesc -> - let subst_map = - Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc - in - let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in - 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 *) + let subst_map = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc + in + let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in + 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 let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit @@ -248,32 +256,32 @@ struct let output_mem = match instr with | Load (id, exp, _, loc) -> - let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in - let v = Dom.Mem.find_heap_set locs mem in - Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem - |> Dom.Mem.load_alias id exp + let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in + let v = Dom.Mem.find_heap_set locs mem in + Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem + |> Dom.Mem.load_alias id exp | Store (exp1, _, exp2, loc) -> - let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in - Dom.Mem.update_mem locs (Sem.eval exp2 mem loc) mem - |> Dom.Mem.store_alias exp1 exp2 + let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in + Dom.Mem.update_mem locs (Sem.eval exp2 mem loc) mem + |> Dom.Mem.store_alias exp1 exp2 | Prune (exp, loc, _, _) -> Sem.prune exp loc mem | Call (ret, Const (Cfun callee_pname), params, loc, _) -> - (match Summary.read_summary pdesc callee_pname with - | Some summary -> - let callee = extras callee_pname in - let ret_val = - instantiate_ret tenv callee callee_pname params mem summary loc - in - (match ret with - | Some (id, _) -> - Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem - | _ -> mem) - | None -> - handle_unknown_call pname ret callee_pname params node mem loc) + (match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + let ret_val = + instantiate_ret tenv callee callee_pname params mem summary loc + in + (match ret with + | Some (id, _) -> + Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) ret_val mem + | _ -> mem) + | None -> + handle_unknown_call pname ret callee_pname params node mem loc) | Declare_locals (locals, _) -> - (* array allocation in stack e.g., int arr[10] *) - let (mem, inst_num) = List.fold ~f:try_decl_arr ~init:(mem, 1) locals in - declare_symbolic_parameter pdesc tenv node inst_num mem + (* array allocation in stack e.g., int arr[10] *) + let (mem, inst_num) = List.fold ~f:try_decl_arr ~init:(mem, 1) locals in + declare_symbolic_parameter pdesc tenv node inst_num mem | Call _ | Remove_temps _ | Abstract _ @@ -300,33 +308,33 @@ struct let array_access = match exp with | Exp.Var _ -> - let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in - Some (arr, Itv.zero, true) + let arr = Sem.eval exp mem loc |> Dom.Val.get_array_blk in + Some (arr, Itv.zero, true) | Exp.Lindex (e1, e2) | Exp.BinOp (Binop.PlusA, e1, e2) -> - let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in - let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in - Some (arr, idx, true) + let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in + let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in + Some (arr, idx, true) | Exp.BinOp (Binop.MinusA, e1, e2) -> - let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in - let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in - Some (arr, idx, false) + let arr = Sem.eval e1 mem loc |> Dom.Val.get_array_blk in + let idx = Sem.eval e2 mem loc |> Dom.Val.get_itv in + Some (arr, idx, false) | _ -> None in match array_access with | Some (arr, idx, is_plus) -> - let site = Sem.get_allocsite pname node 0 0 in - let size = ArrayBlk.sizeof arr in - let offset = ArrayBlk.offsetof arr in - let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in - (if Config.bo_debug >= 2 then - (L.err "@[Add condition :@,"; - L.err "array: %a@," ArrayBlk.pp arr; - L.err " idx: %a@," Itv.pp idx; - L.err "@]@.")); - if size <> Itv.bot && idx <> Itv.bot then - Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set - else cond_set + let site = Sem.get_allocsite pname node 0 0 in + let size = ArrayBlk.sizeof arr in + let offset = ArrayBlk.offsetof arr in + let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in + (if Config.bo_debug >= 2 then + (L.err "@[Add condition :@,"; + L.err "array: %a@," ArrayBlk.pp arr; + L.err " idx: %a@," Itv.pp idx; + L.err "@]@.")); + if size <> Itv.bot && idx <> Itv.bot then + Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set + else cond_set | None -> cond_set let instantiate_cond @@ -337,11 +345,11 @@ struct let callee_cond = Dom.Summary.get_cond_set summary in match callee_pdesc with | Some pdesc -> - let subst_map = - Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc - in - let pname = Procdesc.get_proc_name pdesc in - Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc + let subst_map = + Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem loc + in + let pname = Procdesc.get_proc_name pdesc in + Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc | _ -> callee_cond let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.ConditionSet.t -> unit @@ -363,15 +371,15 @@ struct match instr with | Sil.Load (_, exp, _, loc) | Sil.Store (exp, _, _, loc) -> - add_condition pname node exp loc mem cond_set + add_condition pname node exp loc mem cond_set | Sil.Call (_, Const (Cfun callee_pname), params, loc, _) -> - (match Summary.read_summary pdesc callee_pname with - | Some summary -> - let callee = extras callee_pname in - instantiate_cond tenv pname callee params mem summary loc - |> Dom.ConditionSet.rm_invalid - |> Dom.ConditionSet.join cond_set - | _ -> cond_set) + (match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + instantiate_cond tenv pname callee params mem summary loc + |> Dom.ConditionSet.rm_invalid + |> Dom.ConditionSet.join cond_set + | _ -> cond_set) | _ -> cond_set in let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in @@ -412,12 +420,12 @@ struct match alarm with | None -> () | Some bucket when Typ.Procname.equal pname caller_pname -> - let description = Dom.Condition.to_string cond in - let error_desc = Localise.desc_buffer_overrun bucket description in - let exn = - Exceptions.Checkers (Localise.to_issue_id Localise.buffer_overrun, error_desc) in - let trace = [Errlog.make_trace_element 0 loc description []] in - Reporting.log_error pname ~loc ~ltr:trace exn + let description = Dom.Condition.to_string cond in + let error_desc = Localise.desc_buffer_overrun bucket description in + let exn = + Exceptions.Checkers (Localise.to_issue_id Localise.buffer_overrun, error_desc) in + let trace = [Errlog.make_trace_element 0 loc description []] in + Reporting.log_error pname ~loc ~ltr:trace exn | _ -> () in Dom.ConditionSet.iter report1 conds @@ -441,7 +449,7 @@ let compute_post Report.report_error pdesc cond_set; match entry_mem, exit_mem with | Some entry_mem, Some exit_mem -> - Some (entry_mem, exit_mem, cond_set) + Some (entry_mem, exit_mem, cond_set) | _ -> None let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 52c4c6c9f..a279b9de1 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -28,134 +28,135 @@ struct loc : Location.t; trace : trace; id : string } - [@@deriving compare] -and trace = Intra of Typ.Procname.t - | Inter of Typ.Procname.t * Typ.Procname.t * Location.t -[@@deriving compare] - -and astate = t - -let set_size_pos : t -> t - = fun c -> - if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero - then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) } - else c - -let string_of_location : Location.t -> string - = fun loc -> - let fname = SourceFile.to_string loc.Location.file in - let pos = Location.to_string loc in - F.fprintf F.str_formatter "%s:%s" fname pos; - F.flush_str_formatter () - -let pp_location : F.formatter -> t -> unit - = fun fmt c -> - F.fprintf fmt "%s" (string_of_location c.loc) + [@@deriving compare] + and trace = Intra of Typ.Procname.t + | Inter of Typ.Procname.t * Typ.Procname.t * Location.t + [@@deriving compare] + + and astate = t + + let set_size_pos : t -> t + = fun c -> + if Itv.Bound.lt (Itv.lb c.size) Itv.Bound.zero + then { c with size = Itv.make Itv.Bound.zero (Itv.ub c.size) } + else c + + let string_of_location : Location.t -> string + = fun loc -> + let fname = SourceFile.to_string loc.Location.file in + let pos = Location.to_string loc in + F.fprintf F.str_formatter "%s:%s" fname pos; + F.flush_str_formatter () + + let pp_location : F.formatter -> t -> unit + = fun fmt c -> + F.fprintf fmt "%s" (string_of_location c.loc) -let pp : F.formatter -> t -> unit - = fun fmt c -> - let c = set_size_pos c in - if Config.bo_debug <= 1 then - F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c - else - match c.trace with - Inter (_, pname, loc) -> + let pp : F.formatter -> t -> unit + = fun fmt c -> + let c = set_size_pos c in + if Config.bo_debug <= 1 then + F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c + else + match c.trace with + Inter (_, pname, loc) -> let pname = Typ.Procname.to_string pname in F.fprintf fmt "%a < %a at %a by call %s() at %s" Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc) - | Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c - -let get_location : t -> Location.t - = fun c -> c.loc - -let get_trace : t -> trace - = fun c -> c.trace - -let get_proc_name : t -> Typ.Procname.t - = fun c -> c.proc_name - -let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t - = fun proc_name loc id ~idx ~size -> - { proc_name; idx; size; loc; id ; trace = Intra proc_name } - -let filter1 : t -> bool - = fun c -> - Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top - || Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf - || Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf - || (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat) - -let filter2 : t -> bool - = fun c -> - (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size)) (* basically, alarms involving infinity are filtered *) - && (* except the following cases: *) - not ((Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb < 0 *) - Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero) - || - (Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size lb *) - (Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size))) - || - (Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size ub *) - (Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size))) - || - (Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size lb *) - (Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size))) - || - (Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *) - (Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size)))) - -(* check buffer overrun and return its confidence *) -let check : t -> string option - = fun c -> - (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) - let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *) - let not_overrun = Itv.lt_sem c'.idx c'.size in - let not_underrun = Itv.le_sem Itv.zero c'.idx in - (* il >= 0 and iu < sl, definitely not an error *) - if Itv.eq not_overrun Itv.one && Itv.eq not_underrun Itv.one then - None + | Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c + + let get_location : t -> Location.t + = fun c -> c.loc + + let get_trace : t -> trace + = fun c -> c.trace + + let get_proc_name : t -> Typ.Procname.t + = fun c -> c.proc_name + + let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t + = fun proc_name loc id ~idx ~size -> + { proc_name; idx; size; loc; id ; trace = Intra proc_name } + + let filter1 : t -> bool + = fun c -> + Itv.eq c.idx Itv.top || Itv.eq c.size Itv.top + || Itv.Bound.eq (Itv.lb c.idx) Itv.Bound.MInf + || Itv.Bound.eq (Itv.lb c.size) Itv.Bound.MInf + || (Itv.eq c.idx Itv.nat && Itv.eq c.size Itv.nat) + + let filter2 : t -> bool + = fun c -> + (* basically, alarms involving infinity are filtered *) + (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size)) + && (* except the following cases *) + not ((Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb < 0 *) + Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero) + || + (Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size lb *) + (Itv.Bound.gt (Itv.lb c.idx) (Itv.lb c.size))) + || + (Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb > size ub *) + (Itv.Bound.gt (Itv.lb c.idx) (Itv.ub c.size))) + || + (Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size lb *) + (Itv.Bound.gt (Itv.ub c.idx) (Itv.lb c.size))) + || + (Itv.Bound.is_not_infty (Itv.ub c.idx) && (* idx non-infty ub > size ub *) + (Itv.Bound.gt (Itv.ub c.idx) (Itv.ub c.size)))) + + (* check buffer overrun and return its confidence *) + let check : t -> string option + = fun c -> + (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *) + let c' = set_size_pos c in (* if sl < 0, use sl' = 0 *) + let not_overrun = Itv.lt_sem c'.idx c'.size in + let not_underrun = Itv.le_sem Itv.zero c'.idx in + (* il >= 0 and iu < sl, definitely not an error *) + if Itv.eq not_overrun Itv.one && Itv.eq not_underrun Itv.one then + None (* iu < 0 or il >= su, definitely an error *) - else if Itv.eq not_overrun Itv.zero || Itv.eq not_underrun Itv.zero then - Some Localise.BucketLevel.b1 + else if Itv.eq not_overrun Itv.zero || Itv.eq not_underrun Itv.zero then + Some Localise.BucketLevel.b1 (* su <= iu < +oo, most probably an error *) - else if Itv.Bound.is_not_infty (Itv.ub c.idx) - && Itv.Bound.le (Itv.ub c.size) (Itv.ub c.idx) then - Some Localise.BucketLevel.b2 + else if Itv.Bound.is_not_infty (Itv.ub c.idx) + && Itv.Bound.le (Itv.ub c.size) (Itv.ub c.idx) then + Some Localise.BucketLevel.b2 (* symbolic il >= sl, probably an error *) - else if Itv.Bound.is_symbolic (Itv.lb c.idx) - && Itv.Bound.le (Itv.lb c'.size) (Itv.lb c.idx) then - Some Localise.BucketLevel.b3 + else if Itv.Bound.is_symbolic (Itv.lb c.idx) + && Itv.Bound.le (Itv.lb c'.size) (Itv.lb c.idx) then + Some Localise.BucketLevel.b3 (* other symbolic bounds are probably too noisy *) - else if Config.bo_debug <= 1 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size) then - None - else if filter1 c then - Some Localise.BucketLevel.b5 - else if filter2 c then - Some Localise.BucketLevel.b3 - else - Some Localise.BucketLevel.b2 - -let invalid : t -> bool - = fun x -> Itv.invalid x.idx || Itv.invalid x.size - -let to_string : t -> string - = fun c -> - let c = set_size_pos c in - "Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size - ^ " @ " ^ string_of_location c.loc - ^ (match c.trace with - Inter (_, pname, _) -> - " by call " - ^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " " - | Intra _ -> "") - -let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t - = fun c subst_map caller_pname callee_pname loc -> - if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then - { c with idx = Itv.subst c.idx subst_map; - size = Itv.subst c.size subst_map; - trace = Inter (caller_pname, callee_pname, loc) } - else c + else if Config.bo_debug <= 1 && (Itv.is_symbolic c.idx || Itv.is_symbolic c.size) then + None + else if filter1 c then + Some Localise.BucketLevel.b5 + else if filter2 c then + Some Localise.BucketLevel.b3 + else + Some Localise.BucketLevel.b2 + + let invalid : t -> bool + = fun x -> Itv.invalid x.idx || Itv.invalid x.size + + let to_string : t -> string + = fun c -> + let c = set_size_pos c in + "Offset: " ^ Itv.to_string c.idx ^ " Size: " ^ Itv.to_string c.size + ^ " @ " ^ string_of_location c.loc + ^ (match c.trace with + Inter (_, pname, _) -> + " by call " + ^ MF.monospaced_to_string (Typ.Procname.to_string pname ^ "()") ^ " " + | Intra _ -> "") + + let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t + = fun c subst_map caller_pname callee_pname loc -> + if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then + { c with idx = Itv.subst c.idx subst_map; + size = Itv.subst c.size subst_map; + trace = Inter (caller_pname, callee_pname, loc) } + else c end module ConditionSet = @@ -179,8 +180,8 @@ struct let group : t -> t Map.t = fun x -> fold (fun cond map -> - let old_set = try Map.find cond.loc map with _ -> empty in - Map.add cond.loc (add cond old_set) map) x Map.empty + let old_set = try Map.find cond.loc map with _ -> empty in + Map.add cond.loc (add cond old_set) map) x Map.empty let pp_summary : F.formatter -> t -> unit = fun fmt x -> @@ -246,9 +247,9 @@ struct let rec joins : t list -> t = function - | [] -> bot - | [a] -> a - | a :: b -> join a (joins b) + | [] -> bot + | [a] -> a + | a :: b -> join a (joins b) let get_itv : t -> Itv.t = fun x -> x.itv @@ -277,6 +278,9 @@ struct let of_int : int -> t = fun n -> { bot with itv = Itv.of_int n } + let of_itv : Itv.t -> t + = fun itv -> { bot with itv } + let of_pow_loc : PowLoc.t -> t = fun x -> { bot with powloc = x } @@ -399,7 +403,7 @@ struct let subst : t -> Itv.Bound.t Itv.SubstMap.t -> t = fun x subst_map -> { x with itv = Itv.subst x.itv subst_map; - arrayblk = ArrayBlk.subst x.arrayblk subst_map } + arrayblk = ArrayBlk.subst x.arrayblk subst_map } let get_symbols : t -> Itv.Symbol.t list = fun x -> @@ -496,7 +500,7 @@ struct let find : Loc.t -> astate -> Val.t = fun l m -> try find l m with - | Not_found -> Val.bot + | Not_found -> Val.top_itv let find_set : PowLoc.t -> astate -> Val.t = fun locs mem -> @@ -545,49 +549,49 @@ struct match M.find k rhs with | v' -> Pvar.equal v v' | exception Not_found -> false - in - M.for_all is_in_rhs lhs - - let join : t -> t -> t - = fun x y -> - let join_v _ v1_opt v2_opt = - match v1_opt, v2_opt with - | None, None -> None - | Some v, None - | None, Some v -> Some v - | Some v1, Some v2 -> if Pvar.equal v1 v2 then Some v1 else assert false - in - M.merge join_v x y +in +M.for_all is_in_rhs lhs + +let join : t -> t -> t + = fun x y -> + let join_v _ v1_opt v2_opt = + match v1_opt, v2_opt with + | None, None -> None + | Some v, None + | None, Some v -> Some v + | Some v1, Some v2 -> if Pvar.equal v1 v2 then Some v1 else assert false + in + M.merge join_v x y + +let widen : prev:t -> next:t -> num_iters:int -> t + = fun ~prev ~next ~num_iters:_ -> join prev next - let widen : prev:t -> next:t -> num_iters:int -> t - = fun ~prev ~next ~num_iters:_ -> join prev next - - let pp : F.formatter -> t -> unit - = fun fmt x -> - let pp_sep fmt () = F.fprintf fmt ", @," in - let pp1 fmt (k, v) = - F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k (Pvar.pp Pp.text) v - in - (* F.fprintf fmt "@[Logical Variables :@,"; *) - F.fprintf fmt "@[{ @,"; - F.pp_print_list ~pp_sep pp1 fmt (M.bindings x); - F.fprintf fmt " }@]"; - F.fprintf fmt "@]" - - let load : Ident.t -> Exp.t -> t -> t - = fun id exp m -> - match exp with - | Exp.Lvar x -> M.add id x m - | _ -> m - - let store : Exp.t -> Exp.t -> t -> t - = fun e _ m -> - match e with - | Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m - | _ -> m - - let find : Ident.t -> t -> Pvar.t option - = fun k m -> try Some (M.find k m) with Not_found -> None +let pp : F.formatter -> t -> unit + = fun fmt x -> + let pp_sep fmt () = F.fprintf fmt ", @," in + let pp1 fmt (k, v) = + F.fprintf fmt "%a=%a" (Ident.pp Pp.text) k (Pvar.pp Pp.text) v + in + (* F.fprintf fmt "@[Logical Variables :@,"; *) + F.fprintf fmt "@[{ @,"; + F.pp_print_list ~pp_sep pp1 fmt (M.bindings x); + F.fprintf fmt " }@]"; + F.fprintf fmt "@]" + +let load : Ident.t -> Exp.t -> t -> t + = fun id exp m -> + match exp with + | Exp.Lvar x -> M.add id x m + | _ -> m + +let store : Exp.t -> Exp.t -> t -> t + = fun e _ m -> + match e with + | Exp.Lvar x -> M.filter (fun _ y -> not (Pvar.equal x y)) m + | _ -> m + +let find : Ident.t -> t -> Pvar.t option + = fun k m -> try Some (M.find k m) with Not_found -> None end module MemReach = diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 1dbe39503..2a068ccd7 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.top_itv) + | Const.Cfloat f -> f |> int_of_float |> Val.of_int + | _ -> Val.top_itv (* 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_all_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 in (* must have array blk *) - (* let idx = eval e2 mem loc in *) - let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc 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 - 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 + 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) | _ -> 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 @@ -356,14 +356,14 @@ struct let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in let get_field_name (fn, _, _) = fn in let deref_field v fn mem = - Mem.find_heap_set (PowLoc.append_field (Val.get_all_locs v) fn) mem + Mem.find_heap_set (PowLoc.append_field (Val.get_array_locs v) fn) mem in - let deref_ptr v mem = Mem.find_heap_set (Val.get_all_locs v) mem in + let deref_ptr v mem = Mem.find_heap_set (Val.get_array_locs v) mem in let add_pair_itv itv1 itv2 l = let open Itv in - if itv1 <> bot && itv2 <> bot then + if itv1 <> bot && itv1 <> top && itv2 <> bot then (lb itv1, lb itv2) :: (ub itv1, ub itv2) :: l - else if itv1 <> bot && Itv.eq itv2 bot then + else if itv1 <> bot && itv1 <> top && Itv.eq itv2 bot then (lb itv1, Bound.Bot) :: (ub itv1, Bound.Bot) :: l else l @@ -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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/global.c b/infer/tests/codetoanalyze/c/bufferoverrun/global.c new file mode 100644 index 000000000..ab25bf70b --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/global.c @@ -0,0 +1,15 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +int global; + +void compare_global_variable_bad() { + char arr[10]; + if (global < 10) + arr[10] = 1; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 775a818cf..d2c5c8a4b 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -4,6 +4,7 @@ codetoanalyze/c/bufferoverrun/do_while.c, do_while, 3, BUFFER_OVERRUN, [Offset: codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN, [Offset: [0, 9] Size: [5, 10] @ codetoanalyze/c/bufferoverrun/for_loop.c:38:5] codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [20, 20] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:18:3 by call `arr_access()` ] codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, [Offset: [100, 100] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/function_call.c:17:3 by call `arr_access()` ] +codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/global.c:14:5] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset: [10, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 3e738fdf6..3c487eafe 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -1,3 +1,4 @@ +codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [s$6, s$7] Size: [s$6, s$7] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/cpp/bufferoverrun/trivial.cpp:15:3] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [s$14, s$15] Size: [s$14, s$15] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:91:24 by call `std::vector>_operator[]()` ]