diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index dfa72a912..c6f9e3e71 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -57,9 +57,9 @@ module ArrInfo = struct let diff : t -> t -> Itv.astate = fun arr1 arr2 -> Itv.minus arr1.offset arr2.offset - let subst : t -> Bound.t bottom_lifted Itv.SymbolMap.t -> t = - fun arr subst_map -> - {arr with offset= Itv.subst arr.offset subst_map; size= Itv.subst arr.size subst_map} + let subst : t -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) -> t = + fun arr eval_sym -> + {arr with offset= Itv.subst arr.offset eval_sym; size= Itv.subst arr.size eval_sym} let pp : Format.formatter -> t -> unit = @@ -138,8 +138,8 @@ let get_pow_loc : astate -> PowLoc.t = fold pow_loc_of_allocsite array PowLoc.bot -let subst : astate -> Bound.t bottom_lifted Itv.SymbolMap.t -> astate = - fun a subst_map -> map (fun info -> ArrInfo.subst info subst_map) a +let subst : astate -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> astate = + fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a let get_symbols : astate -> Itv.Symbol.t list = diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index e9db87f9e..90da2af90 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -10,8 +10,6 @@ open! AbstractDomain.Types module F = Format module L = Logging -exception Symbol_not_found of Symb.Symbol.t - exception Not_One_Symbol open Ints @@ -708,35 +706,32 @@ module Bound = struct NonBottom (f x y) - (** Substitutes ALL symbols in [x] with respect to [map]. Throws [Symbol_not_found] if a symbol in [x] can't be found in [map]. Under/over-Approximate as good as possible according to [subst_pos]. *) - let subst_exn : - subst_pos:Symb.BoundEnd.t -> t -> t bottom_lifted Symb.SymbolMap.t -> t bottom_lifted = - fun ~subst_pos x map -> - let get_exn s = - match Symb.SymbolMap.find s map with + (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *) + let subst : + subst_pos:Symb.BoundEnd.t -> t -> (Symb.Symbol.t -> t bottom_lifted) -> t bottom_lifted = + fun ~subst_pos x eval_sym -> + let get s = + match eval_sym s with | NonBottom x when Symb.Symbol.is_unsigned s -> NonBottom (ub ~default:x zero x) | x -> x in let get_mult_const s coeff = - try - if NonZeroInt.is_one coeff then get_exn s - else if NonZeroInt.is_minus_one coeff then get_exn s |> lift1 neg - else - match Symb.SymbolMap.find s map with - | Bottom -> - Bottom - | NonBottom x -> - let x = mult_const subst_pos coeff x in - if Symb.Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x - with Caml.Not_found -> ( - (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *) - match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with - | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false -> - NonBottom zero - | _ -> - raise (Symbol_not_found s) ) + if NonZeroInt.is_one coeff then get s + else if NonZeroInt.is_minus_one coeff then get s |> lift1 neg + else + match eval_sym s with + | Bottom -> ( + (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *) + match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with + | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false -> + NonBottom zero + | _ -> + Bottom ) + | NonBottom x -> + let x = mult_const subst_pos coeff x in + if Symb.Symbol.is_unsigned s then NonBottom (ub ~default:x zero x) else NonBottom x in match x with | MInf | PInf -> @@ -746,15 +741,10 @@ module Bound = struct ~init:(NonBottom (of_int c)) ~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff)) | MinMax (c, sign, min_max, d, s) -> ( - match get_exn s with + match get s with | Bottom -> - Bottom - | exception Caml.Not_found -> ( - match int_of_minmax subst_pos x with - | Some i -> - NonBottom (of_int i) - | None -> - raise (Symbol_not_found s) ) + Option.value_map (int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i -> + NonBottom (of_int i) ) | NonBottom x' -> let res = match (sign, min_max, x') with @@ -805,9 +795,9 @@ module Bound = struct NonBottom res ) - let subst_lb_exn x map = subst_exn ~subst_pos:Symb.BoundEnd.LowerBound x map + let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym - let subst_ub_exn x map = subst_exn ~subst_pos:Symb.BoundEnd.UpperBound x map + let subst_ub x eval_sym = subst ~subst_pos:Symb.BoundEnd.UpperBound x eval_sym let simplify_bound_ends_from_paths x = match x with diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index efb918137..e52320caf 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -8,8 +8,6 @@ open! IStd module F = Format -exception Symbol_not_found of Symb.Symbol.t - exception Not_One_Symbol module SymLinear : sig @@ -119,14 +117,14 @@ module Bound : sig val is_not_infty : t -> bool - val subst_lb_exn : + val subst_lb : t - -> t AbstractDomain.Types.bottom_lifted Symb.SymbolMap.t + -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted) -> t AbstractDomain.Types.bottom_lifted - val subst_ub_exn : + val subst_ub : t - -> t AbstractDomain.Types.bottom_lifted Symb.SymbolMap.t + -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted) -> t AbstractDomain.Types.bottom_lifted val simplify_bound_ends_from_paths : t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 9867601b1..879be71b2 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -34,12 +34,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = Itv.SymbolTable.t - let instantiate_ret ret callee_pname ~callee_exit_mem subst_map mem ret_alias location = + let instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace mem ret_alias location = let copy_reachable_new_locs_from locs mem = let copy loc acc = Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> let v = - Dom.Val.subst v subst_map location |> Dom.Val.add_trace_elem (Trace.Return location) + Dom.Val.subst v eval_sym_trace location + |> Dom.Val.add_trace_elem (Trace.Return location) in Dom.Mem.add_heap loc v acc ) in @@ -52,13 +53,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let ret_var = Loc.of_var (Var.of_id id) in let add_ret_alias l = Dom.Mem.load_alias id l mem in let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in - Dom.Val.subst ret_val subst_map location + Dom.Val.subst ret_val eval_sym_trace location |> Dom.Val.add_trace_elem (Trace.Return location) |> Fn.flip (Dom.Mem.add_stack ret_var) mem |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val) - let instantiate_param tenv pdesc params callee_exit_mem subst_map location mem = + let instantiate_param tenv pdesc params callee_exit_mem eval_sym_trace location mem = let formals = Sem.get_formals pdesc in let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem) params in let f mem formal actual = @@ -76,7 +77,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let formal_fields = PowLoc.append_field formal_locs ~fn in let v = Dom.Mem.find_set formal_fields callee_exit_mem in let actual_fields = PowLoc.append_field (Dom.Val.get_all_locs actual) ~fn in - Dom.Val.subst v subst_map location + Dom.Val.subst v eval_sym_trace location |> Fn.flip (Dom.Mem.strong_update actual_fields) mem in List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields @@ -89,7 +90,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let v = Dom.Mem.find_set formal_locs callee_exit_mem in let actual_locs = Dom.Val.get_all_locs actual in - Dom.Val.subst v subst_map location |> Fn.flip (Dom.Mem.strong_update actual_locs) mem ) + Dom.Val.subst v eval_sym_trace location + |> Fn.flip (Dom.Mem.strong_update actual_locs) mem ) | _ -> mem in @@ -113,15 +115,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> Location.t -> Dom.Mem.astate = fun tenv ret callee_pdesc callee_pname params caller_mem summary location -> - let callee_symbol_table = Dom.Summary.get_symbol_table summary in let callee_exit_mem = Dom.Summary.get_output summary in - let bound_subst_map, ret_alias, rel_subst_map = - Sem.get_subst_map tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem + let ret_alias, rel_subst_map = + Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in + let eval_sym_trace = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in let caller_mem = - instantiate_ret ret callee_pname ~callee_exit_mem bound_subst_map caller_mem ret_alias + instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem ret_alias location - |> instantiate_param tenv callee_pdesc params callee_exit_mem bound_subst_map location + |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location |> forget_ret_relation ret callee_pname in Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem @@ -492,15 +494,13 @@ module Report = struct -> Location.t -> PO.ConditionSet.t = fun tenv callee_pdesc params caller_mem summary location -> - let callee_symbol_table = Dom.Summary.get_symbol_table summary in let callee_exit_mem = Dom.Summary.get_output summary in let callee_cond = Dom.Summary.get_cond_set summary in - let bound_subst_map, _, rel_subst_map = - Sem.get_subst_map tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem - in + let _, rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in let pname = Procdesc.get_proc_name callee_pdesc in let caller_rel = Dom.Mem.get_relation caller_mem in - PO.ConditionSet.subst callee_cond bound_subst_map rel_subst_map caller_rel pname location + let eval_sym_trace = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in + PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel pname location let check_instr : @@ -709,7 +709,7 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_ let summary = match exit_mem with | Some exit_mem -> - let post = (Itv.SymbolTable.summary_of symbol_table, exit_mem, cond_set) in + let post = (exit_mem, cond_set) in ( if Config.bo_debug >= 1 then let proc_name = Procdesc.get_proc_name proc_desc in print_summary proc_name post ) ; diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index e63424755..2d684c089 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -276,25 +276,22 @@ module Val = struct let subst : t - -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t + -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) * (Symb.Symbol.t -> TraceSet.t) -> Location.t -> t = - fun x (bound_map, trace_map) location -> + fun x (eval_sym, trace_of_sym) location -> let symbols = get_symbols x in let traces_caller = List.fold symbols - ~f:(fun traces symbol -> - try TraceSet.join (Itv.SymbolMap.find symbol trace_map) traces with Caml.Not_found -> - traces ) + ~f:(fun traces symbol -> TraceSet.join (trace_of_sym symbol) traces) ~init:TraceSet.empty in let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in - {x with itv= Itv.subst x.itv bound_map; arrayblk= ArrayBlk.subst x.arrayblk bound_map; traces} + {x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces} + (* normalize bottom *) |> normalize - (* normalize bottom *) - let add_trace_elem : Trace.elem -> t -> t = fun elem x -> let traces = TraceSet.add_elem elem x.traces in @@ -999,16 +996,13 @@ module Mem = struct end module Summary = struct - type t = Itv.SymbolTable.summary_t * Mem.t * PO.ConditionSet.summary_t - - let get_symbol_table : t -> Itv.SymbolTable.summary_t = fst3 + type t = Mem.t * PO.ConditionSet.summary_t - let get_output : t -> Mem.t = snd3 + let get_output : t -> Mem.t = fst - let get_cond_set : t -> PO.ConditionSet.summary_t = trd3 + let get_cond_set : t -> PO.ConditionSet.summary_t = snd let pp : F.formatter -> t -> unit = - fun fmt (symbol_table, exit_mem, condition_set) -> - F.fprintf fmt "%a@;%a@;%a" Itv.SymbolTable.pp symbol_table Mem.pp exit_mem - PO.ConditionSet.pp_summary condition_set + fun fmt (exit_mem, condition_set) -> + F.fprintf fmt "%a@;%a" Mem.pp exit_mem PO.ConditionSet.pp_summary condition_set end diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 62ed2614c..fa60f400c 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -93,8 +93,8 @@ module AllocSizeCondition = struct {report_issue_type= None; propagate} ) ) - let subst bound_map length = - match ItvPure.subst length bound_map with NonBottom length -> Some length | Bottom -> None + let subst eval_sym length = + match ItvPure.subst length eval_sym with NonBottom length -> Some length | Bottom -> None end module ArrayAccessCondition = struct @@ -266,13 +266,13 @@ module ArrayAccessCondition = struct let subst : - Itv.Bound.t bottom_lifted Itv.SymbolMap.t + (Symb.Symbol.t -> Bound.t bottom_lifted) -> Relation.SubstMap.t -> Relation.astate -> t -> t option = - fun bound_map rel_map caller_relation c -> - match (ItvPure.subst c.idx bound_map, ItvPure.subst c.size bound_map) with + fun eval_sym rel_map caller_relation c -> + match (ItvPure.subst c.idx eval_sym, ItvPure.subst c.size eval_sym) with | NonBottom idx, NonBottom size -> let idx_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.idx_sym_exp in let size_sym_exp = Relation.SubstMap.symexp_subst_opt rel_map c.size_sym_exp in @@ -304,11 +304,11 @@ module Condition = struct ArrayAccessCondition.get_symbols c - let subst bound_map rel_map caller_relation = function + let subst eval_sym rel_map caller_relation = function | AllocSize c -> - AllocSizeCondition.subst bound_map c |> make_alloc_size + AllocSizeCondition.subst eval_sym c |> make_alloc_size | ArrayAccess {is_collection_add; c} -> - ArrayAccessCondition.subst bound_map rel_map caller_relation c + ArrayAccessCondition.subst eval_sym rel_map caller_relation c |> make_array_access ~is_collection_add @@ -460,24 +460,20 @@ module ConditionWithTrace = struct cmp - let subst (bound_map, trace_map) rel_map caller_relation callee_pname call_site cwt = + let subst (eval_sym, trace_of_sym) rel_map caller_relation callee_pname call_site cwt = let symbols = Condition.get_symbols cwt.cond in if List.is_empty symbols then L.(die InternalError) "Trying to substitute a non-symbolic condition %a from %a at %a. Why was it propagated in \ the first place?" pp_summary cwt Typ.Procname.pp callee_pname Location.pp call_site ; - match Condition.subst bound_map rel_map caller_relation cwt.cond with + match Condition.subst eval_sym rel_map caller_relation cwt.cond with | None -> None | Some cond -> let traces_caller = List.fold symbols ~init:ValTraceSet.empty ~f:(fun val_traces symbol -> - match Itv.SymbolMap.find symbol trace_map with - | symbol_trace -> - ValTraceSet.join symbol_trace val_traces - | exception Caml.Not_found -> - val_traces ) + ValTraceSet.join (trace_of_sym symbol) val_traces ) in let trace = ConditionTrace.make_call_and_subst ~traces_caller ~callee_pname call_site cwt.trace @@ -606,10 +602,10 @@ module ConditionSet = struct |> add_opt location val_traces condset - let subst condset bound_map_trace_map rel_subst_map caller_relation callee_pname call_site = + let subst condset eval_sym_trace rel_subst_map caller_relation callee_pname call_site = let subst_add_cwt condset cwt = match - ConditionWithTrace.subst bound_map_trace_map rel_subst_map caller_relation callee_pname + ConditionWithTrace.subst eval_sym_trace rel_subst_map caller_relation callee_pname call_site cwt with | None -> diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 56f8fcbcd..c95bd0e45 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -52,7 +52,7 @@ module ConditionSet : sig val subst : summary_t - -> Bounds.Bound.t bottom_lifted Symb.SymbolMap.t * ValTraceSet.t Symb.SymbolMap.t + -> (Symb.Symbol.t -> Bounds.Bound.t bottom_lifted) * (Symb.Symbol.t -> ValTraceSet.t) -> Relation.SubstMap.t -> Relation.astate -> Typ.Procname.t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 98813f2f5..249102d0c 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -268,6 +268,92 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t = Val.bot +let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = + fun pdesc -> + let proc_name = Procdesc.get_proc_name pdesc in + Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ)) + + +module ParamBindings = struct + include PrettyPrintable.MakePPMap (struct + include Pvar + + let pp = pp Pp.text + end) + + let make formals actuals = + let rec add_binding formals actuals acc = + match (formals, actuals) with + | (formal, _) :: formals', actual :: actuals' -> + add_binding formals' actuals' (add formal actual acc) + | _, _ -> + acc + in + add_binding formals actuals empty +end + +let rec eval_sympath_partial params p mem = + match p with + | Symb.SymbolPath.Pvar x -> + ParamBindings.find x params + | Symb.SymbolPath.Index _ | Symb.SymbolPath.Field _ -> + let locs = eval_locpath params p mem in + Mem.find_set locs mem + + +and eval_locpath params p mem = + match p with + | Symb.SymbolPath.Pvar _ -> + let v = eval_sympath_partial params p mem in + Val.get_all_locs v + | Symb.SymbolPath.Index p -> + let v = eval_sympath_partial params p mem in + Val.get_all_locs v + | Symb.SymbolPath.Field (fn, p) -> + let locs = eval_locpath params p mem in + PowLoc.append_field ~fn locs + + +let eval_sympath params sympath mem = + match sympath with + | Symb.SymbolPath.Normal p -> + let v = eval_sympath_partial params p mem in + (Val.get_itv v, Val.get_traces v) + | Symb.SymbolPath.Offset p -> + let v = eval_sympath_partial params p mem in + (ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v) + | Symb.SymbolPath.Length p -> + let v = eval_sympath_partial params p mem in + (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v) + + +let mk_eval_sym_trace callee_pdesc actual_exps caller_mem = + let formals = get_formals callee_pdesc in + let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) actual_exps in + let params = ParamBindings.make formals actuals in + let eval_sym_traced s = + let sympath = Symb.Symbol.path s in + let itv, traces = eval_sympath params sympath caller_mem in + if Itv.eq itv Itv.bot then (Bottom, TraceSet.empty) + else + let get_bound = + match Symb.Symbol.bound_end s with + | Symb.BoundEnd.LowerBound -> + Itv.lb + | Symb.BoundEnd.UpperBound -> + Itv.ub + in + (NonBottom (get_bound itv), traces) + in + let eval_sym s = fst (eval_sym_traced s) in + let trace_of_sym s = snd (eval_sym_traced s) in + (eval_sym, trace_of_sym) + + +let mk_eval_sym callee_pdesc actual_exps caller_mem = + fst (mk_eval_sym_trace callee_pdesc actual_exps caller_mem) + + let get_sym_f mem e = Val.get_sym (eval e mem) let get_offset_sym_f mem e = Val.get_offset_sym (eval e mem) @@ -416,31 +502,17 @@ module Prune = struct Mem.set_prune_pairs prune_pairs mem end -let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = - fun pdesc -> - let proc_name = Procdesc.get_proc_name pdesc in - Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ)) - - let get_matching_pairs : Tenv.t - -> Itv.SymbolPath.partial -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate - -> Itv.SymbolTable.summary_t -> Mem.astate - -> (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list - * AliasTarget.t option - * (Relation.Var.t * Relation.SymExp.t option) list = - fun tenv formal callee_v actual actual_exp_opt typ caller_mem callee_symbol_table callee_exit_mem -> - let open Itv in + -> AliasTarget.t option * (Relation.Var.t * Relation.SymExp.t option) list = + fun tenv callee_v actual actual_exp_opt typ caller_mem callee_exit_mem -> let callee_ret_alias = Mem.find_ret_alias callee_exit_mem in - let get_itv v = Val.get_itv v in - let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in - let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in let get_offset_sym v = Val.get_offset_sym v in let get_size_sym v = Val.get_size_sym v in let get_field_name (fn, _, _) = fn in @@ -462,14 +534,6 @@ let get_matching_pairs : | None -> () in - let add_pair_itv path1 itv2 traces l = - match SymbolTable.find_opt path1 callee_symbol_table with - | Some (lb1, ub1) -> - if Itv.eq itv2 bot then (lb1, Bottom, TraceSet.empty) :: (ub1, Bottom, TraceSet.empty) :: l - else (lb1, NonBottom (lb itv2), traces) :: (ub1, NonBottom (ub itv2), traces) :: l - | _ -> - l - in let add_pair_sym_main_value v1 v2 ~e2_opt l = Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var -> let sym_exp_opt = @@ -483,63 +547,40 @@ let get_matching_pairs : Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var -> (var, Relation.SymExp.of_sym s2) :: l ) in - let add_pair_val path1 v1 v2 ~e2_opt (bound_pairs, rel_pairs) = + let add_pair_val v1 v2 ~e2_opt rel_pairs = add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; - let bound_pairs = - bound_pairs - |> add_pair_itv (SymbolPath.normal path1) (get_itv v2) (Val.get_traces v2) - |> add_pair_itv (SymbolPath.offset path1) (get_offset v2) (Val.get_traces v2) - |> add_pair_itv (SymbolPath.length path1) (get_size v2) (Val.get_traces v2) - in - let rel_pairs = - rel_pairs - |> add_pair_sym_main_value v1 v2 ~e2_opt - |> add_pair_sym (get_offset_sym v1) (get_offset_sym v2) - |> add_pair_sym (get_size_sym v1) (get_size_sym v2) - in - (bound_pairs, rel_pairs) + rel_pairs + |> add_pair_sym_main_value v1 v2 ~e2_opt + |> add_pair_sym (get_offset_sym v1) (get_offset_sym v2) + |> add_pair_sym (get_size_sym v1) (get_size_sym v2) in - let add_pair_field path1 v1 v2 pairs fn = + let add_pair_field v1 v2 pairs fn = add_ret_alias (append_field v1 fn) (append_field v2 fn) ; - let path1' = SymbolPath.field (SymbolPath.index path1) fn in let v1' = deref_field v1 fn callee_exit_mem in let v2' = deref_field v2 fn caller_mem in - add_pair_val path1' v1' v2' ~e2_opt:None pairs + add_pair_val v1' v2' ~e2_opt:None pairs in - let add_pair_ptr typ path1 v1 v2 pairs = + let add_pair_ptr typ v1 v2 pairs = add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; 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 path1 v1 v2) ~init:pairs fns + List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns | _ -> pairs ) | Typ.Tptr (_, _) -> - let path1' = SymbolPath.index path1 in let v1' = deref_ptr v1 callee_exit_mem in let v2' = deref_ptr v2 caller_mem in - add_pair_val path1' v1' v2' ~e2_opt:None pairs + add_pair_val v1' v2' ~e2_opt:None pairs | _ -> pairs in - let bound_pairs, rel_pairs = - ([], []) - |> add_pair_val formal callee_v actual ~e2_opt:actual_exp_opt - |> add_pair_ptr typ formal callee_v actual - in - (bound_pairs, !ret_alias, rel_pairs) - - -let subst_map_of_bound_pairs : - (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list - -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t = - fun pairs -> - let add_pair (bound_map, trace_map) (formal, actual, traces) = - (Itv.SymbolMap.add formal actual bound_map, Itv.SymbolMap.add formal traces trace_map) + let rel_pairs = + [] |> add_pair_val callee_v actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ callee_v actual in - List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs + (!ret_alias, rel_pairs) let subst_map_of_rel_pairs : @@ -575,25 +616,19 @@ let get_subst_map : -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate - -> Itv.SymbolTable.summary_t -> Mem.astate - -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t) - * AliasTarget.t option - * Relation.SubstMap.t = - fun tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem -> - let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) = + -> AliasTarget.t option * Relation.SubstMap.t = + fun tenv callee_pdesc params caller_mem callee_exit_mem -> + let add_pair (formal, typ) (actual, actual_exp) (ret_alias, rel_l) = let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in - let new_bound_matching, ret_alias', new_rel_matching = - get_matching_pairs tenv (Itv.SymbolPath.of_pvar formal) callee_v actual actual_exp typ - caller_mem callee_symbol_table callee_exit_mem + let ret_alias', new_rel_matching = + get_matching_pairs tenv callee_v actual actual_exp typ caller_mem callee_exit_mem in - ( List.rev_append new_bound_matching bound_l - , Option.first_some ret_alias ret_alias' - , List.rev_append new_rel_matching rel_l ) + (Option.first_some ret_alias ret_alias', List.rev_append new_rel_matching rel_l) in let formals = get_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> (eval a caller_mem, Some a)) params in - let bound_pairs, ret_alias, rel_pairs = - list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:([], None, []) + let ret_alias, rel_pairs = + list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:(None, []) in - (subst_map_of_bound_pairs bound_pairs, ret_alias, subst_map_of_rel_pairs rel_pairs) + (ret_alias, subst_map_of_rel_pairs rel_pairs) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 84ad591c9..0f88ced7e 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -30,7 +30,6 @@ module Boolean = struct end open Ints -module SymbolMap = Symb.SymbolMap module Symbol = Symb.Symbol module SymbolPath = Symb.SymbolPath module SymbolTable = Symb.SymbolTable @@ -66,8 +65,8 @@ module NonNegativeBound = struct Bounds.Constant (NonNegativeInt.of_int_exn c) ) - let subst_exn b map = - match Bound.subst_ub_exn b map with + let subst b map = + match Bound.subst_ub b map with | Bottom -> Bounds.Constant NonNegativeInt.zero | NonBottom b -> @@ -81,8 +80,10 @@ module type NonNegativeSymbol = sig val int_ub : t -> NonNegativeInt.t option - val subst_exn : t -> Bound.t bottom_lifted SymbolMap.t -> (NonNegativeInt.t, t) Bounds.valclass - (** may throw Symbol_not_found *) + val subst : + t + -> (Symb.Symbol.t -> t AbstractDomain.Types.bottom_lifted) + -> (NonNegativeInt.t, t) Bounds.valclass val pp : F.formatter -> t -> unit end @@ -295,28 +296,26 @@ module MakePolynomial (S : NonNegativeSymbol) = struct let subst = let exception ReturnTop in (* avoids top-lifting everything *) - let rec subst {const; terms} map = + let rec subst {const; terms} eval_sym = M.fold (fun s p acc -> - match S.subst_exn s map with + match S.subst s eval_sym with | Constant c -> ( match PositiveInt.of_int (c :> int) with | None -> acc | Some c -> - let p = subst p map in + let p = subst p eval_sym in mult_const_positive p c |> plus acc ) | ValTop -> - let p = subst p map in + let p = subst p eval_sym in if is_zero p then acc else raise ReturnTop | Symbolic s -> - let p = subst p map in - mult_symb p s |> plus acc - | exception Bounds.Symbol_not_found _ -> - raise ReturnTop ) + let p = subst p eval_sym in + mult_symb p s |> plus acc ) terms (of_non_negative_int const) in - fun p map -> match subst p map with p -> NonTop p | exception ReturnTop -> Top + fun p eval_sym -> match subst p eval_sym with p -> NonTop p | exception ReturnTop -> Top let rec degree {terms} : int = M.fold (fun _ p acc -> max acc (degree p + 1)) terms 0 @@ -389,7 +388,9 @@ module NonNegativePolynomial = struct let widen ~prev ~next ~num_iters:_ = if ( <= ) ~lhs:next ~rhs:prev then prev else Top - let subst p map = match p with Top -> Top | NonTop p -> NonNegativeNonTopPolynomial.subst p map + let subst p eval_sym = + match p with Top -> Top | NonTop p -> NonNegativeNonTopPolynomial.subst p eval_sym + let degree p = match p with Top -> None | NonTop p -> Some (NonNegativeNonTopPolynomial.degree p) @@ -435,16 +436,13 @@ module ItvPure = struct let has_infty = function Bound.MInf, _ | _, Bound.PInf -> true | _, _ -> false - let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted = - fun (l, u) map -> - match (Bound.subst_lb_exn l map, Bound.subst_ub_exn u map) with + let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted = + fun (l, u) eval_sym -> + match (Bound.subst_lb l eval_sym, Bound.subst_ub u eval_sym) with | NonBottom l, NonBottom u -> NonBottom (l, u) | _ -> Bottom - | exception Bounds.Symbol_not_found _ -> - (* For now, let's be VERY aggressive. Under-approximate unknown symbols with Bottom. *) - Bottom let ( <= ) : lhs:t -> rhs:t -> bool = @@ -1000,8 +998,8 @@ let prune_eq : t -> t -> t = bind2 ItvPure.prune_eq let prune_ne : t -> t -> t = bind2 ItvPure.prune_ne -let subst : t -> Bound.t bottom_lifted SymbolMap.t -> t = - fun x map -> match x with NonBottom x' -> ItvPure.subst x' map | _ -> x +let subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t = + fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x let get_symbols : t -> Symbol.t list = function diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 9b6a42cce..a9202506c 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -25,7 +25,6 @@ module Boolean : sig val is_true : t -> bool end -module SymbolMap = Symb.SymbolMap module Symbol = Symb.Symbol module SymbolPath = Symb.SymbolPath module SymbolTable = Symb.SymbolTable @@ -51,7 +50,7 @@ module NonNegativePolynomial : sig val min_default_left : astate -> astate -> astate - val subst : astate -> Bound.t bottom_lifted SymbolMap.t -> astate + val subst : astate -> (Symb.Symbol.t -> Bound.t AbstractDomain.Types.bottom_lifted) -> astate val degree : astate -> int option @@ -121,7 +120,7 @@ module ItvPure : sig val get_symbols : t -> Symbol.t list - val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t bottom_lifted + val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t bottom_lifted end include module type of AbstractDomain.BottomLifted (ItvPure) @@ -224,4 +223,4 @@ val prune_eq : t -> t -> t val prune_ne : t -> t -> t -val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t +val subst : t -> (Symb.Symbol.t -> Bound.t bottom_lifted) -> t diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index bfeccdb87..64f5a31cf 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -83,18 +83,14 @@ module Symbol = struct let is_unsigned : t -> bool = fun x -> x.unsigned let path {path} = path + + let bound_end {bound_end} = bound_end end module SymbolTable = struct module M = PrettyPrintable.MakePPMap (SymbolPath) - type summary_t = (Symbol.t * Symbol.t) M.t - - let find_opt = M.find_opt - - let pp = M.pp ~pp_value:(fun fmt (lb, ub) -> F.fprintf fmt "[%a, %a]" Symbol.pp lb Symbol.pp ub) - - type t = summary_t ref + type t = (Symbol.t * Symbol.t) M.t ref let empty () = ref M.empty @@ -109,9 +105,6 @@ module SymbolTable = struct in symbol_table := M.add path s !symbol_table ; s - - - let summary_of x = !x end module SymbolMap = struct diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 96da3eb86..b25d73d79 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -16,9 +16,9 @@ module BoundEnd : sig end module SymbolPath : sig - type partial + type partial = private Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial - type t + type t = private Normal of partial | Offset of partial | Length of partial val pp : F.formatter -> t -> unit @@ -49,6 +49,8 @@ module Symbol : sig val paths_equal : t -> t -> bool val path : t -> SymbolPath.t + + val bound_end : t -> BoundEnd.t end module SymbolMap : sig @@ -60,20 +62,10 @@ module SymbolMap : sig end module SymbolTable : sig - module M : PrettyPrintable.PPMap with type key = SymbolPath.t - - type summary_t - - val pp : F.formatter -> summary_t -> unit - - val find_opt : SymbolPath.t -> summary_t -> (Symbol.t * Symbol.t) option - type t val empty : unit -> t - val summary_of : t -> summary_t - val lookup : - unsigned:bool -> Typ.Procname.t -> M.key -> t -> Counter.t -> SymbolMap.key * SymbolMap.key + unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> t -> Counter.t -> Symbol.t * Symbol.t end diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index c70bbbc67..ab6accf72 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -42,7 +42,7 @@ module TransferFunctionsNodesBasicCost = struct let cost_atomic_instruction = BasicCost.one - let instantiate_cost ~tenv ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost = + let instantiate_cost ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost = match Ondemand.get_proc_desc callee_pname with | None -> L.(die InternalError) @@ -54,20 +54,16 @@ module TransferFunctionsNodesBasicCost = struct L.(die InternalError) "Can't instantiate symbolic cost %a from call to %a (can't get summary)" BasicCost.pp callee_cost Typ.Procname.pp callee_pname - | Some inferbo_summary -> + | Some _ -> let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in - let callee_symbol_table = BufferOverrunDomain.Summary.get_symbol_table inferbo_summary in - let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in - let (subst_map, _), _, _ = - BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem - callee_symbol_table callee_exit_mem + let eval_sym = + BufferOverrunSemantics.mk_eval_sym callee_pdesc params inferbo_caller_mem in - BasicCost.subst callee_cost subst_map ) + BasicCost.subst callee_cost eval_sym ) let exec_instr_cost inferbo_mem (astate : CostDomain.NodeInstructionToCostMap.astate) - {ProcData.pdesc; tenv} (node : CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate - = + {ProcData.pdesc} (node : CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate = let key = CFG.Node.id node in let astate' = match instr with @@ -76,7 +72,7 @@ module TransferFunctionsNodesBasicCost = struct match Payload.read pdesc callee_pname with | Some {post= callee_cost} -> if BasicCost.is_symbolic callee_cost then - instantiate_cost ~tenv ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem + instantiate_cost ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem ~callee_pname ~params ~callee_cost else callee_cost | None -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c b/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c index 160a2e681..94fd79bbb 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c @@ -13,7 +13,7 @@ struct st { int get_field(t* x) { return x->field; } -void FN_call_get_field_cond_Bad() { +void call_get_field_cond_Bad() { int a[5]; t x = {0}; if (get_field_wrapper(&x)) { @@ -23,13 +23,13 @@ void FN_call_get_field_cond_Bad() { } } -void call_get_field_Good() { +void FP_call_get_field_Good() { int a[5]; t x = {0}; a[get_field_wrapper(&x)] = 0; } -void FN_call_get_field_Bad() { +void call_get_field_Bad() { int a[5]; t x = {10}; a[get_field_wrapper(&x)] = 0; diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index dc3b15e0e..637766bba 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -25,8 +25,9 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: 100 Size: 10 by call to `arr_access` ] -codetoanalyze/c/bufferoverrun/get_field.c, FN_call_get_field_cond_Bad, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] -codetoanalyze/c/bufferoverrun/get_field.c, FN_call_get_field_cond_Bad, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] +codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Call,Call,Assignment,Return,Assignment,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5] +codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]