From c8a17b9d0ef3d8b613de278db491e417e05739ee Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 20 Nov 2018 23:24:49 -0800 Subject: [PATCH] [inferbo] Pass integer type widths to eval for cast Summary: In this diff, it passes the parameter of integer type widths to evaluation functions. The parameter which will be used for casting in the following diff. Reviewed By: mbouaziz Differential Revision: D12920581 fbshipit-source-id: 48bbc802b --- .../src/bufferoverrun/bufferOverrunChecker.ml | 141 +++++++++------ .../src/bufferoverrun/bufferOverrunModels.ml | 145 ++++++++-------- .../bufferoverrun/bufferOverrunSemantics.ml | 160 ++++++++++-------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 27 +-- .../src/bufferoverrun/bufferOverrunUtils.mli | 10 +- infer/src/checkers/cost.ml | 33 ++-- infer/src/checkers/cost.mli | 3 +- infer/src/checkers/hoisting.ml | 12 +- 8 files changed, 317 insertions(+), 214 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index a82816e8f..8c33862c9 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -27,11 +27,13 @@ module Payload = SummaryPayload.Make (struct let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun end) +type extras = {symbol_table: Itv.SymbolTable.t; integer_type_widths: Typ.IntegerWidths.t} + module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = Dom.Mem - type extras = Itv.SymbolTable.t + type nonrec extras = extras let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace eval_locs_sympath_partial mem location = @@ -75,9 +77,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val) - let instantiate_param tenv pdesc params callee_exit_mem eval_sym_trace location mem = + let instantiate_param tenv integer_type_widths 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 actuals = List.map ~f:(fun (a, _) -> Sem.eval integer_type_widths a mem) params in let f mem formal actual = match (snd formal).Typ.desc with | Typ.Tptr (typ, _) -> ( @@ -122,6 +125,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let instantiate_mem : Tenv.t + -> Typ.IntegerWidths.t -> Ident.t * Typ.t -> Procdesc.t -> Typ.Procname.t @@ -130,14 +134,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> BufferOverrunSummary.t -> Location.t -> Dom.Mem.astate = - fun tenv ret callee_pdesc callee_pname params caller_mem summary location -> + fun tenv integer_type_widths ret callee_pdesc callee_pname params caller_mem summary location -> let callee_exit_mem = BufferOverrunSummary.get_output summary in - let rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in - let eval_sym_trace, eval_locpath = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in + let rel_subst_map = + Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem + in + let eval_sym_trace, eval_locpath = + Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem + in let caller_mem = instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace eval_locpath caller_mem location - |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location + |> instantiate_param tenv integer_type_widths 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 @@ -145,7 +154,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate = - fun mem {pdesc; tenv; extras= symbol_table} node instr -> + fun mem {pdesc; tenv; extras= {symbol_table; integer_type_widths}} node instr -> match instr with | Load (id, _, _, _) when Ident.is_none id -> mem @@ -172,14 +181,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (Pvar.pp Pp.text) pvar ; Dom.Mem.add_unknown id ~location mem ) | Load (id, exp, _, _) -> - BoUtils.Exec.load_val id (Sem.eval exp mem) mem + BoUtils.Exec.load_val id (Sem.eval integer_type_widths exp mem) mem | Store (exp1, _, exp2, location) -> - let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in - let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in + let locs = Sem.eval integer_type_widths exp1 mem |> Dom.Val.get_all_locs in + let v = + Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) + in let mem = let sym_exps = - Dom.Relation.SymExp.of_exps ~get_int_sym_f:(Sem.get_sym_f mem) - ~get_offset_sym_f:(Sem.get_offset_sym_f mem) ~get_size_sym_f:(Sem.get_size_sym_f mem) + Dom.Relation.SymExp.of_exps + ~get_int_sym_f:(Sem.get_sym_f integer_type_widths mem) + ~get_offset_sym_f:(Sem.get_offset_sym_f integer_type_widths mem) + ~get_size_sym_f:(Sem.get_size_sym_f integer_type_widths mem) exp2 in Dom.Mem.store_relation locs sym_exps mem @@ -207,14 +220,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let mem = Dom.Mem.update_latest_prune exp1 exp2 mem in mem | Prune (exp, _, _, _) -> - Sem.Prune.prune exp mem + Sem.Prune.prune integer_type_widths exp mem | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> ( let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in match Models.Call.dispatch tenv callee_pname params with | Some {Models.exec} -> let node_hash = CFG.Node.hash node in let model_env = - Models.mk_model_env callee_pname node_hash location tenv symbol_table + Models.mk_model_env callee_pname node_hash location tenv integer_type_widths + symbol_table in exec model_env ~ret mem | None -> ( @@ -223,7 +237,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match Payload.of_summary callee_summary with | Some payload -> let callee_pdesc = Summary.get_proc_desc callee_summary in - instantiate_mem tenv ret callee_pdesc callee_pname params mem payload location + instantiate_mem tenv integer_type_widths ret callee_pdesc callee_pname params mem + payload location | None -> (* This may happen for procedures with a biabduction model. *) L.d_printfln "/!\\ Call to %a has no inferbo payload" Typ.Procname.pp callee_pname ; @@ -267,6 +282,7 @@ module Init = struct -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Tenv.t + -> Typ.IntegerWidths.t -> node_hash:int -> Location.t -> represents_multiple_values:bool @@ -276,8 +292,8 @@ module Init = struct -> new_sym_num:Counter.t -> Dom.Mem.t -> Dom.Mem.t = - fun pname symbol_table path tenv ~node_hash location ~represents_multiple_values loc typ - ~inst_num ~new_sym_num mem -> + fun pname symbol_table path tenv integer_type_widths ~node_hash location + ~represents_multiple_values loc typ ~inst_num ~new_sym_num mem -> let max_depth = 2 in let new_alloc_num = Counter.make 1 in let rec decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth @@ -334,7 +350,9 @@ module Init = struct | Typ.Tstruct typename -> ( match Models.TypName.dispatch tenv typename with | Some {Models.declare_symbolic} -> - let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in + let model_env = + Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table + in declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~represents_multiple_values ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem | None -> @@ -364,6 +382,7 @@ module Init = struct let declare_symbolic_parameters : Typ.Procname.t -> Tenv.t + -> Typ.IntegerWidths.t -> node_hash:int -> Location.t -> Itv.SymbolTable.t @@ -372,14 +391,14 @@ module Init = struct -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate = - fun pname tenv ~node_hash location symbol_table ~represents_multiple_values ~inst_num formals - mem -> + fun pname tenv integer_type_widths ~node_hash location symbol_table ~represents_multiple_values + ~inst_num formals mem -> let new_sym_num = Counter.make 0 in let add_formal (mem, inst_num) (pvar, typ) = let loc = Loc.of_pvar pvar in let path = Itv.SymbolPath.of_pvar pvar in let mem = - declare_symbolic_val pname symbol_table path tenv ~node_hash location + declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location ~represents_multiple_values loc typ ~inst_num ~new_sym_num mem in (mem, inst_num + 1) @@ -387,7 +406,8 @@ module Init = struct List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst - let initial_state {ProcData.pdesc; tenv; extras= symbol_table} start_node = + let initial_state {ProcData.pdesc; tenv; extras= {symbol_table; integer_type_widths}} start_node + = let node_hash = CFG.Node.hash start_node in let location = CFG.Node.loc start_node in let pname = Procdesc.get_proc_name pdesc in @@ -401,7 +421,9 @@ module Init = struct | Typ.Tstruct typname -> ( match Models.TypName.dispatch tenv typname with | Some {Models.declare_local} -> - let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in + let model_env = + Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table + in declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values ~dimension mem | None -> @@ -418,7 +440,7 @@ module Init = struct let mem = Dom.Mem.init in let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in let formals = Sem.get_formals pdesc in - declare_symbolic_parameters pname tenv ~node_hash location symbol_table + declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table ~represents_multiple_values:false ~inst_num formals mem end @@ -475,50 +497,61 @@ module Report = struct let check_binop_array_access : - is_plus:bool + Typ.IntegerWidths.t + -> is_plus:bool -> e1:Exp.t -> e2:Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun ~is_plus ~e1 ~e2 location mem cond_set -> - let arr = Sem.eval e1 mem in - let idx = Sem.eval e2 mem in - let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) e2 in + fun integer_type_widths ~is_plus ~e1 ~e2 location mem cond_set -> + let arr = Sem.eval integer_type_widths e1 mem in + let idx = Sem.eval integer_type_widths e2 mem in + let idx_sym_exp = + Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2 + in let relation = Dom.Mem.get_relation mem in BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus location cond_set let check_binop : - bop:Binop.t + Typ.IntegerWidths.t + -> bop:Binop.t -> e1:Exp.t -> e2:Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun ~bop ~e1 ~e2 location mem cond_set -> + fun integer_type_widths ~bop ~e1 ~e2 location mem cond_set -> match bop with | Binop.PlusPI -> - check_binop_array_access ~is_plus:true ~e1 ~e2 location mem cond_set + check_binop_array_access integer_type_widths ~is_plus:true ~e1 ~e2 location mem cond_set | Binop.MinusPI -> - check_binop_array_access ~is_plus:false ~e1 ~e2 location mem cond_set + check_binop_array_access integer_type_widths ~is_plus:false ~e1 ~e2 location mem cond_set | _ -> cond_set let check_expr_for_array_access : - Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun exp location mem cond_set -> + Typ.IntegerWidths.t + -> Exp.t + -> Location.t + -> Dom.Mem.astate + -> PO.ConditionSet.t + -> PO.ConditionSet.t = + fun integer_type_widths exp location mem cond_set -> let rec check_sub_expr exp cond_set = match exp with | Exp.Lindex (array_exp, index_exp) -> cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp - |> BoUtils.Check.lindex ~array_exp ~index_exp mem location + |> BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp mem location | Exp.BinOp (_, e1, e2) -> cond_set |> check_sub_expr e1 |> check_sub_expr e2 - | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e | Exp.Cast (_, e) -> + | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e -> + check_sub_expr e cond_set + | Exp.Cast (_, e) -> check_sub_expr e cond_set | Exp.Closure {captured_vars} -> List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> @@ -529,12 +562,12 @@ module Report = struct let cond_set = check_sub_expr exp cond_set in match exp with | Exp.Var _ -> - let arr = Sem.eval exp mem in + let arr = Sem.eval integer_type_widths exp mem in let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in let relation = Dom.Mem.get_relation mem in BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set | Exp.BinOp (bop, e1, e2) -> - check_binop ~bop ~e1 ~e2 location mem cond_set + check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set | _ -> cond_set @@ -542,8 +575,8 @@ module Report = struct let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set = match bop with | Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) -> - let lhs_v = Sem.eval lhs mem in - let rhs_v = Sem.eval rhs mem in + let lhs_v = Sem.eval integer_type_widths lhs mem in + let rhs_v = Sem.eval integer_type_widths rhs mem in BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v location cond_set | _ -> @@ -576,19 +609,24 @@ module Report = struct let instantiate_cond : Tenv.t + -> Typ.IntegerWidths.t -> Procdesc.t -> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Payload.t -> Location.t -> PO.ConditionSet.t = - fun tenv callee_pdesc params caller_mem summary location -> + fun tenv integer_type_widths callee_pdesc params caller_mem summary location -> let callee_exit_mem = BufferOverrunSummary.get_output summary in let callee_cond = BufferOverrunSummary.get_cond_set summary in - let rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in + let rel_subst_map = + Sem.get_subst_map tenv integer_type_widths 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 - let eval_sym_trace, _ = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in + let eval_sym_trace, _ = + Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem + in PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel pname location @@ -606,11 +644,11 @@ module Report = struct match instr with | Sil.Load (_, exp, _, location) -> cond_set - |> check_expr_for_array_access exp location mem + |> check_expr_for_array_access integer_type_widths exp location mem |> check_expr_for_integer_overflow integer_type_widths exp location mem | Sil.Store (lexp, _, rexp, location) -> cond_set - |> check_expr_for_array_access lexp location mem + |> check_expr_for_array_access integer_type_widths lexp location mem |> check_expr_for_integer_overflow integer_type_widths lexp location mem |> check_expr_for_integer_overflow integer_type_widths rexp location mem | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> ( @@ -622,14 +660,17 @@ module Report = struct | Some {Models.check} -> let node_hash = CFG.Node.hash node in let pname = Procdesc.get_proc_name pdesc in - check (Models.mk_model_env pname node_hash location tenv symbol_table) mem cond_set + check + (Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table) + mem cond_set | None -> ( match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with | Some callee_summary -> ( match Payload.of_summary callee_summary with | Some callee_payload -> let callee_pdesc = Summary.get_proc_desc callee_summary in - instantiate_cond tenv callee_pdesc params mem callee_payload location + instantiate_cond tenv integer_type_widths callee_pdesc params mem callee_payload + location |> PO.ConditionSet.merge cond_set | None -> (* no inferbo payload *) cond_set ) @@ -796,7 +837,7 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_ fun {proc_desc; tenv; integer_type_widths; summary} -> Preanal.do_preanalysis proc_desc tenv ; let symbol_table = Itv.SymbolTable.empty () in - let pdata = ProcData.make proc_desc tenv symbol_table in + let pdata = ProcData.make proc_desc tenv {symbol_table; integer_type_widths} in let cfg = CFG.from_pdesc proc_desc in let initial = Init.initial_state pdata (CFG.start_node cfg) in let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index e0c8685e7..7fa5dd7b6 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -22,10 +22,11 @@ type model_env = ; node_hash: int ; location: Location.t ; tenv: Tenv.t + ; integer_type_widths: Typ.IntegerWidths.t ; symbol_table: Itv.SymbolTable.t } -let mk_model_env pname node_hash location tenv symbol_table = - {pname; node_hash; location; tenv; symbol_table} +let mk_model_env pname node_hash location tenv integer_type_widths symbol_table = + {pname; node_hash; location; tenv; integer_type_widths; symbol_table} type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.astate -> Dom.Mem.astate @@ -80,9 +81,9 @@ let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = fun (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None) -let check_alloc_size size_exp {location} mem cond_set = +let check_alloc_size size_exp {location; integer_type_widths} mem cond_set = let _, _, length0, _ = get_malloc_info size_exp in - let v_length = Sem.eval length0 mem in + let v_length = Sem.eval integer_type_widths length0 mem in match Dom.Val.get_itv v_length with | Bottom -> cond_set @@ -106,25 +107,25 @@ let set_uninitialized location (typ : Typ.t) ploc mem = let malloc size_exp = - let exec {pname; node_hash; location; tenv} ~ret:(id, _) mem = + let exec {pname; node_hash; location; tenv; integer_type_widths} ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in let typ, stride, length0, dyn_length = get_malloc_info size_exp in - let length = Sem.eval length0 mem in + let length = Sem.eval integer_type_widths length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let path = Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path in let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in let offset, size = (Itv.zero, Dom.Val.get_itv length) in let size_exp_opt = let size_exp = Option.value dyn_length ~default:length0 in - Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) size_exp + Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) size_exp in let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.set_traces traces in mem |> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt |> set_uninitialized location typ (Dom.Val.get_array_locs v) - |> BoUtils.Exec.init_array_fields tenv pname path ~node_hash typ (Dom.Val.get_array_locs v) - ?dyn_length + |> BoUtils.Exec.init_array_fields tenv integer_type_widths pname path ~node_hash typ + (Dom.Val.get_array_locs v) ?dyn_length and check = check_alloc_size size_exp in {exec; check} @@ -136,35 +137,38 @@ let calloc size_exp stride_exp = let memcpy dest_exp src_exp size_exp = let exec _ ~ret:_ mem = mem - and check {location} mem cond_set = - BoUtils.Check.lindex_byte ~array_exp:dest_exp ~byte_index_exp:size_exp mem location cond_set - |> BoUtils.Check.lindex_byte ~array_exp:src_exp ~byte_index_exp:size_exp mem location + and check {location; integer_type_widths} mem cond_set = + BoUtils.Check.lindex_byte integer_type_widths ~array_exp:dest_exp ~byte_index_exp:size_exp mem + location cond_set + |> BoUtils.Check.lindex_byte integer_type_widths ~array_exp:src_exp ~byte_index_exp:size_exp + mem location in {exec; check} let memset arr_exp size_exp = let exec _ ~ret:_ mem = mem - and check {location} mem cond_set = - BoUtils.Check.lindex_byte ~array_exp:arr_exp ~byte_index_exp:size_exp mem location cond_set + and check {location; integer_type_widths} mem cond_set = + BoUtils.Check.lindex_byte integer_type_widths ~array_exp:arr_exp ~byte_index_exp:size_exp mem + location cond_set in {exec; check} let realloc src_exp size_exp = - let exec {location; tenv} ~ret:(id, _) mem = + let exec {location; tenv; integer_type_widths} ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in let typ, _, length0, dyn_length = get_malloc_info size_exp in - let length = Sem.eval length0 mem in + let length = Sem.eval integer_type_widths length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let v = - Sem.eval src_exp mem + Sem.eval integer_type_widths src_exp mem |> Dom.Val.set_array_size (Dom.Val.get_itv length) |> Dom.Val.set_traces traces in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in Option.value_map dyn_length ~default:mem ~f:(fun dyn_length -> - let dyn_length = Dom.Val.get_itv (Sem.eval dyn_length mem) in + let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in BoUtils.Exec.set_dyn_length tenv typ (Dom.Val.get_array_locs v) dyn_length mem ) and check = check_alloc_size size_exp in {exec; check} @@ -178,7 +182,7 @@ let placement_new size_exp (src_exp1, t1) src_arg2_opt = when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] -> malloc size_exp | _, _ -> - let exec _ ~ret:(id, _) mem = + let exec {integer_type_widths} ~ret:(id, _) mem = let src_exp = if Typ.is_pointer_to_void t1 then src_exp1 else @@ -191,16 +195,16 @@ let placement_new size_exp (src_exp1, t1) src_arg2_opt = L.d_error "Unexpected types of arguments for __placement_new" ; src_exp1 in - let v = Sem.eval src_exp mem in + let v = Sem.eval integer_type_widths src_exp mem in Dom.Mem.add_stack (Loc.of_id id) v mem in {exec; check= no_check} let inferbo_min e1 e2 = - let exec _ ~ret:(id, _) mem = - let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in - let i2 = Sem.eval e2 mem |> Dom.Val.get_itv in + let exec {integer_type_widths} ~ret:(id, _) mem = + let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in + let i2 = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in mem |> Dom.Mem.add_stack (Loc.of_id id) v in @@ -208,9 +212,9 @@ let inferbo_min e1 e2 = let inferbo_set_size e1 e2 = - let exec _model_env ~ret:_ mem = - let locs = Sem.eval e1 mem |> Dom.Val.get_pow_loc in - let size = Sem.eval e2 mem |> Dom.Val.get_itv in + let exec {integer_type_widths} ~ret:_ mem = + let locs = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_pow_loc in + let size = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in Dom.Mem.transform_mem ~f:(Dom.Val.set_array_size size) locs mem and check = check_alloc_size e2 in {exec; check} @@ -229,17 +233,18 @@ let bottom = let infer_print e = - let exec {location} ~ret:_ mem = + let exec {location; integer_type_widths} ~ret:_ mem = L.(debug BufferOverrun Medium) - "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; + "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp + (Sem.eval integer_type_widths e mem) ; mem in {exec; check= no_check} let get_array_length array_exp = - let exec _ ~ret mem = - let arr = Sem.eval_arr array_exp mem in + let exec {integer_type_widths} ~ret mem = + let arr = Sem.eval_arr integer_type_widths array_exp mem in let traces = Dom.Val.get_traces arr in let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in let result = Dom.Val.of_itv ~traces length in @@ -249,10 +254,10 @@ let get_array_length array_exp = let set_array_length array length_exp = - let exec {pname; node_hash; location} ~ret:_ mem = + let exec {pname; node_hash; location; integer_type_widths} ~ret:_ mem = match array with | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> - let length = Sem.eval length_exp mem |> Dom.Val.get_itv in + let length = Sem.eval integer_type_widths length_exp mem |> Dom.Val.get_itv in let stride = Option.map ~f:IntLit.to_int_exn stride in let path = Some (Symb.SymbolPath.of_pvar array_pvar) in let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in @@ -267,14 +272,16 @@ let set_array_length array length_exp = module Split = struct - let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = + let std_vector integer_type_widths ~adds_at_least_one (vector_exp, vector_typ) location mem = let traces = BufferOverrunTrace.(Set.singleton (Call location)) in let increment_itv = if adds_at_least_one then Itv.pos else Itv.nat in let increment = Dom.Val.of_itv ~traces increment_itv in let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in let vector_size_locs = - Sem.eval vector_exp mem |> Dom.Val.get_all_locs |> PowLoc.append_field ~fn:size_field + Sem.eval integer_type_widths vector_exp mem + |> Dom.Val.get_all_locs + |> PowLoc.append_field ~fn:size_field in Dom.Mem.transform_mem ~f:(Dom.Val.plus_a increment) vector_size_locs mem end @@ -282,8 +289,8 @@ end module Boost = struct module Split = struct let std_vector vector_arg = - let exec {location} ~ret:_ mem = - Split.std_vector ~adds_at_least_one:true vector_arg location mem + let exec {location; integer_type_widths} ~ret:_ mem = + Split.std_vector integer_type_widths ~adds_at_least_one:true vector_arg location mem in {exec; check= no_check} end @@ -292,16 +299,16 @@ end module Folly = struct module Split = struct let std_vector vector_arg ignore_empty_opt = - let exec {location} ~ret:_ mem = + let exec {location; integer_type_widths} ~ret:_ mem = let adds_at_least_one = match ignore_empty_opt with | Some ignore_empty_exp -> - Sem.eval ignore_empty_exp mem |> Dom.Val.get_itv |> Itv.is_false + Sem.eval integer_type_widths ignore_empty_exp mem |> Dom.Val.get_itv |> Itv.is_false | None -> (* default: ignore_empty is false *) true in - Split.std_vector ~adds_at_least_one vector_arg location mem + Split.std_vector integer_type_widths ~adds_at_least_one vector_arg location mem in {exec; check= no_check} end @@ -334,11 +341,11 @@ module StdArray = struct let at _size (array_exp, _) (index_exp, _) = (* TODO? use size *) - let exec _ ~ret:(id, _) mem = + let exec {integer_type_widths} ~ret:(id, _) mem = L.d_printfln_escaped "Using model std::array<_, %Ld>::at" _size ; - BoUtils.Exec.load_val id (Sem.eval_lindex array_exp index_exp mem) mem - and check {location} mem cond_set = - BoUtils.Check.lindex ~array_exp ~index_exp mem location cond_set + BoUtils.Exec.load_val id (Sem.eval_lindex integer_type_widths array_exp index_exp mem) mem + and check {location; integer_type_widths} mem cond_set = + BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp mem location cond_set in {exec; check} @@ -415,77 +422,83 @@ module Collection = struct let add alist_id = {exec= change_size_by ~size_f:incr_size alist_id; check= no_check} - let get_size alist mem = BoUtils.Exec.get_alist_size (Sem.eval alist mem) mem + let get_size integer_type_widths alist mem = + BoUtils.Exec.get_alist_size (Sem.eval integer_type_widths alist mem) mem + let size array_exp = - let exec _ ~ret mem = - let size = get_size array_exp mem in + let exec {integer_type_widths} ~ret mem = + let size = get_size integer_type_widths array_exp mem in model_by_value size ret mem in {exec; check= no_check} let iterator alist = - let exec _ ~ret mem = - let itr = Sem.eval alist mem in + let exec {integer_type_widths} ~ret mem = + let itr = Sem.eval integer_type_widths alist mem in model_by_value itr ret mem in {exec; check= no_check} let hasNext iterator = - let exec _ ~ret mem = + let exec {integer_type_widths} ~ret mem = (* Set the size of the iterator to be [0, size-1], so that range will be size of the collection. *) - let collection_size = get_size iterator mem |> Dom.Val.get_iterator_itv in + let collection_size = + get_size integer_type_widths iterator mem |> Dom.Val.get_iterator_itv + in model_by_value collection_size ret mem in {exec; check= no_check} let addAll alist_id alist_to_add = - let exec _model_env ~ret mem = - let to_add_length = get_size alist_to_add mem in - change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id _model_env ~ret mem + let exec ({integer_type_widths} as model_env) ~ret mem = + let to_add_length = get_size integer_type_widths alist_to_add mem in + change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem in {exec; check= no_check} let add_at_index (alist_id : Ident.t) index_exp = - let check {location} mem cond_set = + let check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access ~array_exp ~index_exp ~is_collection_add:true mem location - cond_set + BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp + ~is_collection_add:true mem location cond_set in {exec= change_size_by ~size_f:incr_size alist_id; check} let remove_at_index alist_id index_exp = - let check {location} mem cond_set = + let check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access ~array_exp ~index_exp mem location cond_set + BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp mem location + cond_set in {exec= change_size_by ~size_f:decr_size alist_id; check} let addAll_at_index alist_id index_exp alist_to_add = - let exec _model_env ~ret mem = - let to_add_length = get_size alist_to_add mem in - change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id _model_env ~ret mem + let exec ({integer_type_widths} as model_env) ~ret mem = + let to_add_length = get_size integer_type_widths alist_to_add mem in + change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem in - let check {location} mem cond_set = + let check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access ~index_exp ~array_exp ~is_collection_add:true mem location - cond_set + BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp + ~is_collection_add:true mem location cond_set in {exec; check} let get_or_set_at_index alist_id index_exp = let exec _model_env ~ret:_ mem = mem in - let check {location} mem cond_set = + let check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access ~index_exp ~array_exp mem location cond_set + BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp mem location + cond_set in {exec; check} end diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 3b2f5fbd9..0b644c72c 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -131,8 +131,8 @@ let rec must_alias_cmp : Exp.t -> Mem.astate -> bool = false -let rec eval : Exp.t -> Mem.astate -> Val.t = - fun exp mem -> +let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = + fun integer_type_widths exp mem -> if must_alias_cmp exp mem then Val.of_int 0 else match exp with @@ -142,17 +142,18 @@ let rec eval : Exp.t -> Mem.astate -> Val.t = let ploc = Loc.of_pvar pvar in if Mem.is_stack_loc ploc mem then Mem.find ploc mem else Val.of_loc ploc | Exp.UnOp (uop, e, _) -> - eval_unop uop e mem + eval_unop integer_type_widths uop e mem | Exp.BinOp (bop, e1, e2) -> - eval_binop bop e1 e2 mem + eval_binop integer_type_widths bop e1 e2 mem | Exp.Const c -> eval_const c | Exp.Cast (_, e) -> - eval e mem + eval integer_type_widths e mem | Exp.Lfield (e, fn, _) -> - eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc + eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn + |> Val.of_pow_loc | Exp.Lindex (e1, e2) -> - eval_lindex e1 e2 mem + eval_lindex integer_type_widths e1 e2 mem | Exp.Sizeof {nbytes= Some size} -> Val.of_int size | Exp.Sizeof {nbytes= None} -> @@ -161,8 +162,10 @@ let rec eval : Exp.t -> Mem.astate -> Val.t = Val.Itv.top -and eval_lindex array_exp index_exp mem = - let array_v, index_v = (eval array_exp mem, eval index_exp mem) in +and eval_lindex integer_type_widths array_exp index_exp mem = + let array_v, index_v = + (eval integer_type_widths array_exp mem, eval integer_type_widths index_exp mem) + in if ArrayBlk.is_bot (Val.get_array_blk array_v) then match array_exp with | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) -> @@ -184,9 +187,9 @@ and eval_lindex array_exp index_exp mem = Val.plus_pi array_v index_v -and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t = - fun unop e mem -> - let v = eval e mem in +and eval_unop : Typ.IntegerWidths.t -> Unop.t -> Exp.t -> Mem.astate -> Val.t = + fun integer_type_widths unop e mem -> + let v = eval integer_type_widths e mem in match unop with | Unop.Neg -> Val.neg v @@ -196,10 +199,10 @@ and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t = Val.lnot v -and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = - fun binop e1 e2 mem -> - let v1 = eval e1 mem in - let v2 = eval e2 mem in +and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = + fun integer_type_widths binop e1 e2 mem -> + let v1 = eval integer_type_widths e1 mem in + let v2 = eval integer_type_widths e2 mem in match binop with | Binop.PlusA _ -> Val.plus_a v1 v2 @@ -247,8 +250,8 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = when "x" is a program variable, (eval_arr "x") returns array blocks the "x" is pointing to, on the other hand, (eval "x") returns the abstract location of "x". *) -let rec eval_arr : Exp.t -> Mem.astate -> Val.t = - fun exp mem -> +let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = + fun integer_type_widths exp mem -> match exp with | Exp.Var id -> ( match Mem.find_alias id mem with @@ -259,14 +262,14 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t = | Exp.Lvar pvar -> Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem | Exp.BinOp (bop, e1, e2) -> - eval_binop bop e1 e2 mem + eval_binop integer_type_widths bop e1 e2 mem | Exp.Cast (_, e) -> - eval_arr e mem + eval_arr integer_type_widths e mem | Exp.Lfield (e, fn, _) -> - let locs = eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in + let locs = eval integer_type_widths e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in Mem.find_set locs mem | Exp.Lindex (e, _) -> - let locs = eval e mem |> Val.get_all_locs in + let locs = eval integer_type_widths e mem |> Val.get_all_locs in Mem.find_set locs mem | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ -> Val.bot @@ -334,10 +337,10 @@ let eval_sympath params sympath mem = (ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v) -let mk_eval_sym_trace callee_pdesc actual_exps caller_mem = +let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem = let params = let formals = get_formals callee_pdesc in - let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) actual_exps in + let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in ParamBindings.make formals actuals in let eval_sym s = @@ -354,15 +357,17 @@ let mk_eval_sym_trace callee_pdesc actual_exps caller_mem = ((eval_sym, trace_of_sym), eval_locpath) -let mk_eval_sym callee_pdesc actual_exps caller_mem = - fst (fst (mk_eval_sym_trace callee_pdesc actual_exps caller_mem)) +let mk_eval_sym integer_type_widths callee_pdesc actual_exps caller_mem = + fst (fst (mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem)) + +let get_sym_f integer_type_widths mem e = Val.get_sym (eval integer_type_widths e mem) -let get_sym_f mem e = Val.get_sym (eval e mem) +let get_offset_sym_f integer_type_widths mem e = + Val.get_offset_sym (eval integer_type_widths e mem) -let get_offset_sym_f mem e = Val.get_offset_sym (eval e mem) -let get_size_sym_f mem e = Val.get_size_sym (eval e mem) +let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_type_widths e mem) module Prune = struct type astate = {prune_pairs: PrunePairs.astate; mem: Mem.astate} @@ -405,8 +410,8 @@ module Prune = struct astate - let rec prune_binop_left : Exp.t -> astate -> astate = - fun e ({mem} as astate) -> + let rec prune_binop_left : Typ.IntegerWidths.t -> Exp.t -> astate -> astate = + fun integer_type_widths e ({mem} as astate) -> match e with | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e') | Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e') @@ -415,7 +420,7 @@ module Prune = struct match Mem.find_simple_alias x mem with | Some lv -> let v = Mem.find lv mem in - let v' = Val.prune_comp comp v (eval e' mem) in + let v' = Val.prune_comp comp v (eval integer_type_widths e' mem) in update_mem_in_prune lv v' astate | None -> astate ) @@ -423,7 +428,7 @@ module Prune = struct match Mem.find_simple_alias x mem with | Some lv -> let v = Mem.find lv mem in - let v' = Val.prune_eq v (eval e' mem) in + let v' = Val.prune_eq v (eval integer_type_widths e' mem) in update_mem_in_prune lv v' astate | None -> astate ) @@ -431,7 +436,7 @@ module Prune = struct match Mem.find_simple_alias x mem with | Some lv -> let v = Mem.find lv mem in - let v' = Val.prune_ne v (eval e' mem) in + let v' = Val.prune_ne v (eval integer_type_widths e' mem) in update_mem_in_prune lv v' astate | None -> astate ) @@ -443,84 +448,96 @@ module Prune = struct Be careful when you take into account integer overflows in the abstract semantics [eval] in the future. *) astate - |> prune_binop_left (Exp.BinOp (comp, e1, Exp.BinOp (Binop.MinusA t, e3, e2))) - |> prune_binop_left (Exp.BinOp (comp, e2, Exp.BinOp (Binop.MinusA t, e3, e1))) + |> prune_binop_left integer_type_widths + (Exp.BinOp (comp, e1, Exp.BinOp (Binop.MinusA t, e3, e2))) + |> prune_binop_left integer_type_widths + (Exp.BinOp (comp, e2, Exp.BinOp (Binop.MinusA t, e3, e1))) | Exp.BinOp ( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp) , Exp.BinOp (Binop.MinusA t, e1, e2) , e3 ) -> astate - |> prune_binop_left (Exp.BinOp (comp, e1, Exp.BinOp (Binop.PlusA t, e3, e2))) - |> prune_binop_left (Exp.BinOp (comp_rev comp, e2, Exp.BinOp (Binop.MinusA t, e1, e3))) + |> prune_binop_left integer_type_widths + (Exp.BinOp (comp, e1, Exp.BinOp (Binop.PlusA t, e3, e2))) + |> prune_binop_left integer_type_widths + (Exp.BinOp (comp_rev comp, e2, Exp.BinOp (Binop.MinusA t, e1, e3))) | _ -> astate - let prune_binop_right : Exp.t -> astate -> astate = - fun e astate -> + let prune_binop_right : Typ.IntegerWidths.t -> Exp.t -> astate -> astate = + fun integer_type_widths e astate -> match e with | Exp.BinOp (((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as c), e1, e2) -> - prune_binop_left (Exp.BinOp (comp_rev c, e2, e1)) astate + prune_binop_left integer_type_widths (Exp.BinOp (comp_rev c, e2, e1)) astate | _ -> astate - let is_unreachable_constant : Exp.t -> Mem.astate -> bool = - fun e m -> - let v = eval e m in + let is_unreachable_constant : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> bool = + fun integer_type_widths e m -> + let v = eval integer_type_widths e m in Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) && PowLoc.is_bot (Val.get_pow_loc v) && ArrayBlk.is_bot (Val.get_array_blk v) - let prune_unreachable : Exp.t -> astate -> astate = - fun e ({mem} as astate) -> - if is_unreachable_constant e mem || Mem.is_relation_unsat mem then {astate with mem= Mem.bot} + let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> astate -> astate = + fun integer_type_widths e ({mem} as astate) -> + if is_unreachable_constant integer_type_widths e mem || Mem.is_relation_unsat mem then + {astate with mem= Mem.bot} else astate - let rec prune_helper e astate = + let rec prune_helper integer_type_widths e astate = let astate = - astate |> prune_unreachable e |> prune_unop e |> prune_binop_left e |> prune_binop_right e + astate + |> prune_unreachable integer_type_widths e + |> prune_unop e + |> prune_binop_left integer_type_widths e + |> prune_binop_right integer_type_widths e in match e with | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> - prune_helper e astate + prune_helper integer_type_widths e astate | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> - prune_helper (Exp.UnOp (Unop.LNot, e, None)) astate + prune_helper integer_type_widths (Exp.UnOp (Unop.LNot, e, None)) astate | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> - prune_helper (Exp.Var x) astate + prune_helper integer_type_widths (Exp.Var x) astate | Exp.BinOp (Binop.LAnd, e1, e2) -> - astate |> prune_helper e1 |> prune_helper e2 + astate |> prune_helper integer_type_widths e1 |> prune_helper integer_type_widths e2 | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> astate - |> prune_helper (Exp.UnOp (Unop.LNot, e1, t)) - |> prune_helper (Exp.UnOp (Unop.LNot, e2, t)) + |> prune_helper integer_type_widths (Exp.UnOp (Unop.LNot, e1, t)) + |> prune_helper integer_type_widths (Exp.UnOp (Unop.LNot, e2, t)) | 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_helper (Exp.BinOp (comp_not c, e1, e2)) astate + prune_helper integer_type_widths (Exp.BinOp (comp_not c, e1, e2)) astate | _ -> astate - let prune : Exp.t -> Mem.astate -> Mem.astate = - fun e mem -> + let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Mem.astate = + fun integer_type_widths e mem -> let mem = Mem.apply_latest_prune e mem in let mem = - let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f mem) in + let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f integer_type_widths mem) in Mem.meet_constraints constrs mem in - let {mem; prune_pairs} = prune_helper e {mem; prune_pairs= PrunePairs.empty} in + let {mem; prune_pairs} = + prune_helper integer_type_widths e {mem; prune_pairs= PrunePairs.empty} + in Mem.set_prune_pairs prune_pairs mem end let get_matching_pairs : Tenv.t + -> Typ.IntegerWidths.t -> Val.t -> Val.t -> Exp.t option @@ -528,7 +545,7 @@ let get_matching_pairs : -> Mem.astate -> Mem.astate -> (Relation.Var.t * Relation.SymExp.t option) list = - fun tenv callee_v actual actual_exp_opt typ caller_mem callee_exit_mem -> + fun tenv integer_type_widths callee_v actual actual_exp_opt typ caller_mem callee_exit_mem -> 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 @@ -543,7 +560,9 @@ let get_matching_pairs : Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var -> let sym_exp_opt = Option.first_some - (Relation.SymExp.of_exp_opt ~get_sym_f:(get_sym_f caller_mem) e2_opt) + (Relation.SymExp.of_exp_opt + ~get_sym_f:(get_sym_f integer_type_widths caller_mem) + e2_opt) (Relation.SymExp.of_sym (Val.get_sym v2)) in (var, sym_exp_opt) :: l ) @@ -611,17 +630,26 @@ let rec list_fold2_def : let get_subst_map : - Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> Relation.SubstMap.t = - fun tenv callee_pdesc params caller_mem callee_exit_mem -> + Tenv.t + -> Typ.IntegerWidths.t + -> Procdesc.t + -> (Exp.t * 'a) list + -> Mem.astate + -> Mem.astate + -> Relation.SubstMap.t = + fun tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem -> let add_pair (formal, typ) (actual, actual_exp) rel_l = let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in let new_rel_matching = - get_matching_pairs tenv callee_v actual actual_exp typ caller_mem callee_exit_mem + get_matching_pairs tenv integer_type_widths callee_v actual actual_exp typ caller_mem + callee_exit_mem in 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 actuals = + List.map ~f:(fun (a, _) -> (eval integer_type_widths a caller_mem, Some a)) params + in let rel_pairs = list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:[] in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 275cdcd39..0b0ec157b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -236,7 +236,7 @@ module Exec = struct Dom.Mem.add_heap loc size mem - let init_array_fields tenv pname path ~node_hash typ locs ?dyn_length mem = + let init_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem = let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in let field_loc = PowLoc.append_field locs ~fn:field_name in @@ -246,7 +246,7 @@ module Exec = struct let length = Itv.of_int_lit length in let length = Option.value_map dyn_length ~default:length ~f:(fun dyn_length -> - let i = Dom.Val.get_itv (Sem.eval dyn_length mem) in + let i = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in Itv.plus i length ) in let stride = Option.map stride ~f:IntLit.to_int_exn in @@ -336,9 +336,10 @@ module Check = struct check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces location cond_set - let collection_access ~array_exp ~index_exp ?(is_collection_add = false) mem location cond_set = - let idx = Sem.eval index_exp mem in - let arr = Sem.eval array_exp mem in + let collection_access integer_type_widths ~array_exp ~index_exp ?(is_collection_add = false) mem + location cond_set = + let idx = Sem.eval integer_type_widths index_exp mem in + let arr = Sem.eval integer_type_widths array_exp mem in let idx_traces = Dom.Val.get_traces idx in let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in let idx = Dom.Val.get_itv idx in @@ -347,10 +348,12 @@ module Check = struct ~is_collection_add location cond_set - let lindex ~array_exp ~index_exp mem location cond_set = - let idx = Sem.eval index_exp mem in - let arr = Sem.eval_arr array_exp mem in - let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) index_exp in + let lindex integer_type_widths ~array_exp ~index_exp mem location cond_set = + let idx = Sem.eval integer_type_widths index_exp mem in + let arr = Sem.eval_arr integer_type_widths array_exp mem in + let idx_sym_exp = + Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp + in let relation = Dom.Mem.get_relation mem in array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set @@ -368,9 +371,9 @@ module Check = struct location cond_set ~is_collection_add:true - let lindex_byte ~array_exp ~byte_index_exp mem location cond_set = - let idx = Sem.eval byte_index_exp mem in - let arr = Sem.eval_arr array_exp mem in + let lindex_byte integer_type_widths ~array_exp ~byte_index_exp mem location cond_set = + let idx = Sem.eval integer_type_widths byte_index_exp mem in + let arr = Sem.eval_arr integer_type_widths array_exp mem in let relation = Dom.Mem.get_relation mem in array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index f502496fc..496cbfd11 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -118,6 +118,7 @@ module Exec : sig val init_array_fields : Tenv.t + -> Typ.IntegerWidths.t -> Typ.Procname.t -> Itv.SymbolPath.partial option -> node_hash:int @@ -142,7 +143,8 @@ module Check : sig -> PO.ConditionSet.t val lindex : - array_exp:Exp.t + Typ.IntegerWidths.t + -> array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Location.t @@ -150,7 +152,8 @@ module Check : sig -> PO.ConditionSet.t val lindex_byte : - array_exp:Exp.t + Typ.IntegerWidths.t + -> array_exp:Exp.t -> byte_index_exp:Exp.t -> Dom.Mem.astate -> Location.t @@ -158,7 +161,8 @@ module Check : sig -> PO.ConditionSet.t val collection_access : - array_exp:Exp.t + Typ.IntegerWidths.t + -> array_exp:Exp.t -> index_exp:Exp.t -> ?is_collection_add:bool -> Dom.Mem.astate diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index b28c92b97..57ac7f204 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -34,7 +34,8 @@ module Node = ProcCfg.DefaultNode The nodes in the domain of the map are those in the path reaching the current node. *) -let instantiate_cost ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~callee_cost = +let instantiate_cost integer_type_widths ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params + ~callee_cost = match Ondemand.get_proc_desc callee_pname with | None -> L.(die InternalError) @@ -48,7 +49,10 @@ let instantiate_cost ~caller_pdesc ~inferbo_caller_mem ~callee_pname ~params ~ca callee_cost Typ.Procname.pp callee_pname | Some _ -> let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in - let eval_sym = BufferOverrunSemantics.mk_eval_sym callee_pdesc params inferbo_caller_mem in + let eval_sym = + BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_pdesc params + inferbo_caller_mem + in BasicCost.subst callee_cost eval_sym ) @@ -56,12 +60,15 @@ module TransferFunctionsNodesBasicCost = struct module CFG = InstrCFG module Domain = NodesBasicCostDomain - type extras = BufferOverrunChecker.invariant_map + type extras = + { inferbo_invariant_map: BufferOverrunChecker.invariant_map + ; integer_type_widths: Typ.IntegerWidths.t } let cost_atomic_instruction = BasicCost.one - let exec_instr_cost inferbo_mem (astate : CostDomain.NodeInstructionToCostMap.astate) - {ProcData.pdesc} (node : CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate = + let exec_instr_cost integer_type_widths inferbo_mem + (astate : 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 @@ -70,8 +77,8 @@ module TransferFunctionsNodesBasicCost = struct match Payload.read pdesc callee_pname with | Some {post= callee_cost} -> if BasicCost.is_symbolic callee_cost then - instantiate_cost ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem - ~callee_pname ~params ~callee_cost + instantiate_cost integer_type_widths ~caller_pdesc:pdesc + ~inferbo_caller_mem:inferbo_mem ~callee_pname ~params ~callee_cost else callee_cost | None -> cost_atomic_instruction @@ -95,9 +102,10 @@ module TransferFunctionsNodesBasicCost = struct astate' - let exec_instr costmap ({ProcData.extras= inferbo_invariant_map} as pdata) node instr = + let exec_instr costmap ({ProcData.extras= {inferbo_invariant_map; integer_type_widths}} as pdata) + node instr = let inferbo_mem = BufferOverrunChecker.extract_pre (CFG.Node.id node) inferbo_invariant_map in - let costmap = exec_instr_cost inferbo_mem costmap pdata node instr in + let costmap = exec_instr_cost integer_type_widths inferbo_mem costmap pdata node instr in costmap @@ -732,7 +740,7 @@ let check_and_report_top_and_bottom cost proc_desc summary = else if BasicCost.is_zero cost then report IssueType.zero_execution_time_call "is zero" -let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = +let checker ({Callbacks.tenv; proc_desc; integer_type_widths} as callback_args) : Summary.t = let inferbo_invariant_map, summary = BufferOverrunChecker.compute_invariant_map_and_check callback_args in @@ -752,7 +760,10 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t = in let instr_cfg = InstrCFG.from_pdesc proc_desc in let invariant_map_NodesBasicCost = - let proc_data = ProcData.make proc_desc tenv inferbo_invariant_map in + let proc_data = + ProcData.make proc_desc tenv + TransferFunctionsNodesBasicCost.{inferbo_invariant_map; integer_type_widths} + in (*compute_WCET cfg invariant_map min_trees in *) AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.empty in diff --git a/infer/src/checkers/cost.mli b/infer/src/checkers/cost.mli index 34dfa4067..93e170649 100644 --- a/infer/src/checkers/cost.mli +++ b/infer/src/checkers/cost.mli @@ -10,7 +10,8 @@ open! IStd val checker : Callbacks.proc_callback_t val instantiate_cost : - caller_pdesc:Procdesc.t + Typ.IntegerWidths.t + -> caller_pdesc:Procdesc.t -> inferbo_caller_mem:BufferOverrunDomain.Mem.astate option -> callee_pname:Typ.Procname.t -> params:(Exp.t * 'a) list diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index 5c92793fa..96218906f 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -75,7 +75,8 @@ let do_report summary Call.({pname; loc}) loop_head_loc = Reporting.log_error summary ~loc ~ltr IssueType.invariant_call message -let should_report tenv proc_desc Call.({pname; node; params}) inferbo_invariant_map = +let should_report tenv proc_desc Call.({pname; node; params}) integer_type_widths + inferbo_invariant_map = (* If a function is modeled as variant for hoisting (like List.size or __cast ), we don't want to report it *) let is_variant_for_hoisting = @@ -95,14 +96,15 @@ let should_report tenv proc_desc Call.({pname; node; params}) inferbo_invariant_ let inferbo_invariant_map = Lazy.force inferbo_invariant_map in let inferbo_mem = BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map in (* get the cost of the function call *) - Cost.instantiate_cost ~caller_pdesc:proc_desc ~inferbo_caller_mem:inferbo_mem - ~callee_pname:pname ~params ~callee_cost:cost + Cost.instantiate_cost integer_type_widths ~caller_pdesc:proc_desc + ~inferbo_caller_mem:inferbo_mem ~callee_pname:pname ~params ~callee_cost:cost |> Itv.NonNegativePolynomial.is_symbolic | _ -> false -let checker ({Callbacks.tenv; summary; proc_desc} as callback_args) : Summary.t = +let checker ({Callbacks.tenv; summary; proc_desc; integer_type_widths} as callback_args) : + Summary.t = let cfg = InstrCFG.from_pdesc proc_desc in let proc_data = ProcData.make_default proc_desc tenv in (* computes reaching defs: node -> (var -> node set) *) @@ -129,7 +131,7 @@ let checker ({Callbacks.tenv; summary; proc_desc} as callback_args) : Summary.t let loop_head_loc = Procdesc.Node.get_loc loop_head in HoistCalls.iter (fun call -> - if should_report tenv proc_desc call inferbo_invariant_map then + if should_report tenv proc_desc call integer_type_widths inferbo_invariant_map then do_report summary call loop_head_loc ) inv_instrs ) loop_head_to_inv_instrs ;