pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Pass integer type widths to eval for cast

Browse Source 
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
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 1486a5f105
commit c8a17b9d0e
8 changed files with 317 additions and 214 deletions
Show Stats Download Patch File Download Diff File

141
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -27,11 +27,13 @@ module Payload = SummaryPayload.Make (struct
let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun
end) end)
type extras = {symbol_table: Itv.SymbolTable.t; integer_type_widths: Typ.IntegerWidths.t}
module TransferFunctions (CFG : ProcCfg.S) = struct module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG module CFG = CFG
module Domain = Dom.Mem 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 let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace
eval_locs_sympath_partial mem location = 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) |> 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 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 = let f mem formal actual =
match (snd formal).Typ.desc with match (snd formal).Typ.desc with
| Typ.Tptr (typ, _) -> ( | Typ.Tptr (typ, _) -> (
@ -122,6 +125,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let instantiate_mem : let instantiate_mem :
Tenv.t Tenv.t
-> Typ.IntegerWidths.t
-> Ident.t * Typ.t -> Ident.t * Typ.t
-> Procdesc.t -> Procdesc.t
-> Typ.Procname.t -> Typ.Procname.t
@ -130,14 +134,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
-> BufferOverrunSummary.t -> BufferOverrunSummary.t
-> Location.t -> Location.t
-> Dom.Mem.astate = -> 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 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 rel_subst_map =
let eval_sym_trace, eval_locpath = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in 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 = let caller_mem =
instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace eval_locpath caller_mem instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace eval_locpath caller_mem
location 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 |> forget_ret_relation ret callee_pname
in in
Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem 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 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 match instr with
| Load (id, _, _, _) when Ident.is_none id -> | Load (id, _, _, _) when Ident.is_none id ->
mem mem
@ -172,14 +181,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(Pvar.pp Pp.text) pvar ; (Pvar.pp Pp.text) pvar ;
Dom.Mem.add_unknown id ~location mem ) Dom.Mem.add_unknown id ~location mem )
| Load (id, exp, _, _) -> | 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) -> | Store (exp1, _, exp2, location) ->
let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in let locs = Sem.eval integer_type_widths exp1 mem |> Dom.Val.get_all_locs in
let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in let v =
Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location)
in
let mem = let mem =
let sym_exps = let sym_exps =
Dom.Relation.SymExp.of_exps ~get_int_sym_f:(Sem.get_sym_f mem) Dom.Relation.SymExp.of_exps
~get_offset_sym_f:(Sem.get_offset_sym_f mem) ~get_size_sym_f:(Sem.get_size_sym_f mem) ~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 exp2
in in
Dom.Mem.store_relation locs sym_exps mem 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 let mem = Dom.Mem.update_latest_prune exp1 exp2 mem in
mem mem
| Prune (exp, _, _, _) -> | 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, _) -> ( | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> (
let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
match Models.Call.dispatch tenv callee_pname params with match Models.Call.dispatch tenv callee_pname params with
| Some {Models.exec} -> | Some {Models.exec} ->
let node_hash = CFG.Node.hash node in let node_hash = CFG.Node.hash node in
let model_env = 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 in
exec model_env ~ret mem exec model_env ~ret mem
| None -> ( | None -> (
@ -223,7 +237,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match Payload.of_summary callee_summary with match Payload.of_summary callee_summary with
| Some payload -> | Some payload ->
let callee_pdesc = Summary.get_proc_desc callee_summary in 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 -> | None ->
(* This may happen for procedures with a biabduction model. *) (* This may happen for procedures with a biabduction model. *)
L.d_printfln "/!\\ Call to %a has no inferbo payload" Typ.Procname.pp callee_pname ; 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.SymbolTable.t
-> Itv.SymbolPath.partial -> Itv.SymbolPath.partial
-> Tenv.t -> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int -> node_hash:int
-> Location.t -> Location.t
-> represents_multiple_values:bool -> represents_multiple_values:bool
@ -276,8 +292,8 @@ module Init = struct
-> new_sym_num:Counter.t -> new_sym_num:Counter.t
-> Dom.Mem.t -> Dom.Mem.t
-> Dom.Mem.t = -> Dom.Mem.t =
fun pname symbol_table path tenv ~node_hash location ~represents_multiple_values loc typ fun pname symbol_table path tenv integer_type_widths ~node_hash location
~inst_num ~new_sym_num mem -> ~represents_multiple_values loc typ ~inst_num ~new_sym_num mem ->
let max_depth = 2 in let max_depth = 2 in
let new_alloc_num = Counter.make 1 in let new_alloc_num = Counter.make 1 in
let rec decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth 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 -> ( | Typ.Tstruct typename -> (
match Models.TypName.dispatch tenv typename with match Models.TypName.dispatch tenv typename with
| Some {Models.declare_symbolic} -> | 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 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 ~represents_multiple_values ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem
| None -> | None ->
@ -364,6 +382,7 @@ module Init = struct
let declare_symbolic_parameters : let declare_symbolic_parameters :
Typ.Procname.t Typ.Procname.t
-> Tenv.t -> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int -> node_hash:int
-> Location.t -> Location.t
-> Itv.SymbolTable.t -> Itv.SymbolTable.t
@ -372,14 +391,14 @@ module Init = struct
-> (Pvar.t * Typ.t) list -> (Pvar.t * Typ.t) list
-> Dom.Mem.astate -> Dom.Mem.astate
-> Dom.Mem.astate = -> Dom.Mem.astate =
fun pname tenv ~node_hash location symbol_table ~represents_multiple_values ~inst_num formals fun pname tenv integer_type_widths ~node_hash location symbol_table ~represents_multiple_values
mem -> ~inst_num formals mem ->
let new_sym_num = Counter.make 0 in let new_sym_num = Counter.make 0 in
let add_formal (mem, inst_num) (pvar, typ) = let add_formal (mem, inst_num) (pvar, typ) =
let loc = Loc.of_pvar pvar in let loc = Loc.of_pvar pvar in
let path = Itv.SymbolPath.of_pvar pvar in let path = Itv.SymbolPath.of_pvar pvar in
let mem = 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 ~represents_multiple_values loc typ ~inst_num ~new_sym_num mem
in in
(mem, inst_num + 1) (mem, inst_num + 1)
@ -387,7 +406,8 @@ module Init = struct
List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst 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 node_hash = CFG.Node.hash start_node in
let location = CFG.Node.loc start_node in let location = CFG.Node.loc start_node in
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
@ -401,7 +421,9 @@ module Init = struct
| Typ.Tstruct typname -> ( | Typ.Tstruct typname -> (
match Models.TypName.dispatch tenv typname with match Models.TypName.dispatch tenv typname with
| Some {Models.declare_local} -> | 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 declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values
~dimension mem ~dimension mem
| None -> | None ->
@ -418,7 +440,7 @@ module Init = struct
let mem = Dom.Mem.init in 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 mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
let formals = Sem.get_formals 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 ~represents_multiple_values:false ~inst_num formals mem
end end
@ -475,50 +497,61 @@ module Report = struct
let check_binop_array_access : let check_binop_array_access :
is_plus:bool Typ.IntegerWidths.t
-> is_plus:bool
-> e1:Exp.t -> e1:Exp.t
-> e2:Exp.t -> e2:Exp.t
-> Location.t -> Location.t
-> Dom.Mem.astate -> Dom.Mem.astate
-> PO.ConditionSet.t -> PO.ConditionSet.t
-> PO.ConditionSet.t = -> PO.ConditionSet.t =
fun ~is_plus ~e1 ~e2 location mem cond_set -> fun integer_type_widths ~is_plus ~e1 ~e2 location mem cond_set ->
let arr = Sem.eval e1 mem in let arr = Sem.eval integer_type_widths e1 mem in
let idx = Sem.eval e2 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 mem) e2 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 let relation = Dom.Mem.get_relation mem in
BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus location cond_set BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus location cond_set
let check_binop : let check_binop :
bop:Binop.t Typ.IntegerWidths.t
-> bop:Binop.t
-> e1:Exp.t -> e1:Exp.t
-> e2:Exp.t -> e2:Exp.t
-> Location.t -> Location.t
-> Dom.Mem.astate -> Dom.Mem.astate
-> PO.ConditionSet.t -> PO.ConditionSet.t
-> 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 match bop with
| Binop.PlusPI -> | 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 -> | 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 cond_set
let check_expr_for_array_access : let check_expr_for_array_access :
Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = Typ.IntegerWidths.t
fun exp location mem cond_set -> -> 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 = let rec check_sub_expr exp cond_set =
match exp with match exp with
| Exp.Lindex (array_exp, index_exp) -> | Exp.Lindex (array_exp, index_exp) ->
cond_set |> check_sub_expr array_exp |> check_sub_expr 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) -> | Exp.BinOp (_, e1, e2) ->
cond_set |> check_sub_expr e1 |> check_sub_expr 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 check_sub_expr e cond_set
| Exp.Closure {captured_vars} -> | Exp.Closure {captured_vars} ->
List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> 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 let cond_set = check_sub_expr exp cond_set in
match exp with match exp with
| Exp.Var _ -> | 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 idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in
let relation = Dom.Mem.get_relation mem 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 BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set
| Exp.BinOp (bop, e1, e2) -> | 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 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 = let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set =
match bop with match bop with
| Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) -> | Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) ->
let lhs_v = Sem.eval lhs mem in let lhs_v = Sem.eval integer_type_widths lhs mem in
let rhs_v = Sem.eval rhs 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 BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v location
cond_set cond_set
| _ -> | _ ->
@ -576,19 +609,24 @@ module Report = struct
let instantiate_cond : let instantiate_cond :
Tenv.t Tenv.t
-> Typ.IntegerWidths.t
-> Procdesc.t -> Procdesc.t
-> (Exp.t * Typ.t) list -> (Exp.t * Typ.t) list
-> Dom.Mem.astate -> Dom.Mem.astate
-> Payload.t -> Payload.t
-> Location.t -> Location.t
-> PO.ConditionSet.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_exit_mem = BufferOverrunSummary.get_output summary in
let callee_cond = BufferOverrunSummary.get_cond_set 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 pname = Procdesc.get_proc_name callee_pdesc in
let caller_rel = Dom.Mem.get_relation caller_mem 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 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 match instr with
| Sil.Load (_, exp, _, location) -> | Sil.Load (_, exp, _, location) ->
cond_set 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 |> check_expr_for_integer_overflow integer_type_widths exp location mem
| Sil.Store (lexp, _, rexp, location) -> | Sil.Store (lexp, _, rexp, location) ->
cond_set 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 lexp location mem
|> check_expr_for_integer_overflow integer_type_widths rexp location mem |> check_expr_for_integer_overflow integer_type_widths rexp location mem
| Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> ( | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> (
@ -622,14 +660,17 @@ module Report = struct
| Some {Models.check} -> | Some {Models.check} ->
let node_hash = CFG.Node.hash node in let node_hash = CFG.Node.hash node in
let pname = Procdesc.get_proc_name pdesc 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 -> ( | None -> (
match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
| Some callee_summary -> ( | Some callee_summary -> (
match Payload.of_summary callee_summary with match Payload.of_summary callee_summary with
| Some callee_payload -> | Some callee_payload ->
let callee_pdesc = Summary.get_proc_desc callee_summary in 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 |> PO.ConditionSet.merge cond_set
| None -> | None ->
(* no inferbo payload *) cond_set ) (* 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} -> fun {proc_desc; tenv; integer_type_widths; summary} ->
Preanal.do_preanalysis proc_desc tenv ; Preanal.do_preanalysis proc_desc tenv ;
let symbol_table = Itv.SymbolTable.empty () in 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 cfg = CFG.from_pdesc proc_desc in
let initial = Init.initial_state pdata (CFG.start_node cfg) in let initial = Init.initial_state pdata (CFG.start_node cfg) in
let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in

145
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -22,10 +22,11 @@ type model_env =
; node_hash: int ; node_hash: int
; location: Location.t ; location: Location.t
; tenv: Tenv.t ; tenv: Tenv.t
; integer_type_widths: Typ.IntegerWidths.t
; symbol_table: Itv.SymbolTable.t } ; symbol_table: Itv.SymbolTable.t }
let mk_model_env 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; 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 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) (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 _, _, 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 match Dom.Val.get_itv v_length with
| Bottom -> | Bottom ->
cond_set cond_set
@ -106,25 +107,25 @@ let set_uninitialized location (typ : Typ.t) ploc mem =
let malloc size_exp = 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 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 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 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 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 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 offset, size = (Itv.zero, Dom.Val.get_itv length) in
let size_exp_opt = let size_exp_opt =
let size_exp = Option.value dyn_length ~default:length0 in 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 in
let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.set_traces traces in let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.set_traces traces in
mem mem
|> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.add_stack (Loc.of_id id) v
|> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt
|> set_uninitialized location typ (Dom.Val.get_array_locs v) |> 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) |> BoUtils.Exec.init_array_fields tenv integer_type_widths pname path ~node_hash typ
?dyn_length (Dom.Val.get_array_locs v) ?dyn_length
and check = check_alloc_size size_exp in and check = check_alloc_size size_exp in
{exec; check} {exec; check}
@ -136,35 +137,38 @@ let calloc size_exp stride_exp =
let memcpy dest_exp src_exp size_exp = let memcpy dest_exp src_exp size_exp =
let exec _ ~ret:_ mem = mem let exec _ ~ret:_ mem = mem
and check {location} mem cond_set = and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex_byte ~array_exp:dest_exp ~byte_index_exp:size_exp mem location cond_set BoUtils.Check.lindex_byte integer_type_widths ~array_exp:dest_exp ~byte_index_exp:size_exp mem
|> BoUtils.Check.lindex_byte ~array_exp:src_exp ~byte_index_exp:size_exp mem location location cond_set
|> BoUtils.Check.lindex_byte integer_type_widths ~array_exp:src_exp ~byte_index_exp:size_exp
mem location
in in
{exec; check} {exec; check}
let memset arr_exp size_exp = let memset arr_exp size_exp =
let exec _ ~ret:_ mem = mem let exec _ ~ret:_ mem = mem
and check {location} mem cond_set = and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex_byte ~array_exp:arr_exp ~byte_index_exp:size_exp mem location cond_set BoUtils.Check.lindex_byte integer_type_widths ~array_exp:arr_exp ~byte_index_exp:size_exp mem
location cond_set
in in
{exec; check} {exec; check}
let realloc src_exp size_exp = 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 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 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 traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in
let v = 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_array_size (Dom.Val.get_itv length)
|> Dom.Val.set_traces traces |> Dom.Val.set_traces traces
in in
let mem = Dom.Mem.add_stack (Loc.of_id id) v mem 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 -> 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 ) BoUtils.Exec.set_dyn_length tenv typ (Dom.Val.get_array_locs v) dyn_length mem )
and check = check_alloc_size size_exp in and check = check_alloc_size size_exp in
{exec; check} {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"] -> when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] ->
malloc size_exp malloc size_exp
| _, _ -> | _, _ ->
let exec _ ~ret:(id, _) mem = let exec {integer_type_widths} ~ret:(id, _) mem =
let src_exp = let src_exp =
if Typ.is_pointer_to_void t1 then src_exp1 if Typ.is_pointer_to_void t1 then src_exp1
else 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" ; L.d_error "Unexpected types of arguments for __placement_new" ;
src_exp1 src_exp1
in 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 Dom.Mem.add_stack (Loc.of_id id) v mem
in in
{exec; check= no_check} {exec; check= no_check}
let inferbo_min e1 e2 = let inferbo_min e1 e2 =
let exec _ ~ret:(id, _) mem = let exec {integer_type_widths} ~ret:(id, _) mem =
let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in
let i2 = Sem.eval e2 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 let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in
mem |> Dom.Mem.add_stack (Loc.of_id id) v mem |> Dom.Mem.add_stack (Loc.of_id id) v
in in
@ -208,9 +212,9 @@ let inferbo_min e1 e2 =
let inferbo_set_size e1 e2 = let inferbo_set_size e1 e2 =
let exec _model_env ~ret:_ mem = let exec {integer_type_widths} ~ret:_ mem =
let locs = Sem.eval e1 mem |> Dom.Val.get_pow_loc in let locs = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_pow_loc in
let size = Sem.eval e2 mem |> Dom.Val.get_itv 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 Dom.Mem.transform_mem ~f:(Dom.Val.set_array_size size) locs mem
and check = check_alloc_size e2 in and check = check_alloc_size e2 in
{exec; check} {exec; check}
@ -229,17 +233,18 @@ let bottom =
let infer_print e = let infer_print e =
let exec {location} ~ret:_ mem = let exec {location; integer_type_widths} ~ret:_ mem =
L.(debug BufferOverrun Medium) L.(debug BufferOverrun Medium)
"@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; "@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp
(Sem.eval integer_type_widths e mem) ;
mem mem
in in
{exec; check= no_check} {exec; check= no_check}
let get_array_length array_exp = let get_array_length array_exp =
let exec _ ~ret mem = let exec {integer_type_widths} ~ret mem =
let arr = Sem.eval_arr array_exp mem in let arr = Sem.eval_arr integer_type_widths array_exp mem in
let traces = Dom.Val.get_traces arr in let traces = Dom.Val.get_traces arr in
let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in
let result = Dom.Val.of_itv ~traces length 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 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 match array with
| Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> | 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 stride = Option.map ~f:IntLit.to_int_exn stride in
let path = Some (Symb.SymbolPath.of_pvar array_pvar) 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 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 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 traces = BufferOverrunTrace.(Set.singleton (Call location)) in
let increment_itv = if adds_at_least_one then Itv.pos else Itv.nat 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 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 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 size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in
let vector_size_locs = 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 in
Dom.Mem.transform_mem ~f:(Dom.Val.plus_a increment) vector_size_locs mem Dom.Mem.transform_mem ~f:(Dom.Val.plus_a increment) vector_size_locs mem
end end
@ -282,8 +289,8 @@ end
module Boost = struct module Boost = struct
module Split = struct module Split = struct
let std_vector vector_arg = let std_vector vector_arg =
let exec {location} ~ret:_ mem = let exec {location; integer_type_widths} ~ret:_ mem =
Split.std_vector ~adds_at_least_one:true vector_arg location mem Split.std_vector integer_type_widths ~adds_at_least_one:true vector_arg location mem
in in
{exec; check= no_check} {exec; check= no_check}
end end
@ -292,16 +299,16 @@ end
module Folly = struct module Folly = struct
module Split = struct module Split = struct
let std_vector vector_arg ignore_empty_opt = 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 = let adds_at_least_one =
match ignore_empty_opt with match ignore_empty_opt with
| Some ignore_empty_exp -> | 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 -> | None ->
(* default: ignore_empty is false *) (* default: ignore_empty is false *)
true true
in 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 in
{exec; check= no_check} {exec; check= no_check}
end end
@ -334,11 +341,11 @@ module StdArray = struct
let at _size (array_exp, _) (index_exp, _) = let at _size (array_exp, _) (index_exp, _) =
(* TODO? use size *) (* 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 ; 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 BoUtils.Exec.load_val id (Sem.eval_lindex integer_type_widths array_exp index_exp mem) mem
and check {location} mem cond_set = and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex ~array_exp ~index_exp mem location cond_set BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp mem location cond_set
in in
{exec; check} {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 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 size array_exp =
let exec _ ~ret mem = let exec {integer_type_widths} ~ret mem =
let size = get_size array_exp mem in let size = get_size integer_type_widths array_exp mem in
model_by_value size ret mem model_by_value size ret mem
in in
{exec; check= no_check} {exec; check= no_check}
let iterator alist = let iterator alist =
let exec _ ~ret mem = let exec {integer_type_widths} ~ret mem =
let itr = Sem.eval alist mem in let itr = Sem.eval integer_type_widths alist mem in
model_by_value itr ret mem model_by_value itr ret mem
in in
{exec; check= no_check} {exec; check= no_check}
let hasNext iterator = 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 (* Set the size of the iterator to be [0, size-1], so that range
will be size of the collection. *) 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 model_by_value collection_size ret mem
in in
{exec; check= no_check} {exec; check= no_check}
let addAll alist_id alist_to_add = let addAll alist_id alist_to_add =
let exec _model_env ~ret mem = let exec ({integer_type_widths} as model_env) ~ret mem =
let to_add_length = get_size alist_to_add mem in 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 change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem
in in
{exec; check= no_check} {exec; check= no_check}
let add_at_index (alist_id : Ident.t) index_exp = 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 let array_exp = Exp.Var alist_id in
BoUtils.Check.collection_access ~array_exp ~index_exp ~is_collection_add:true mem location BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp
cond_set ~is_collection_add:true mem location cond_set
in in
{exec= change_size_by ~size_f:incr_size alist_id; check} {exec= change_size_by ~size_f:incr_size alist_id; check}
let remove_at_index alist_id index_exp = 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 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 in
{exec= change_size_by ~size_f:decr_size alist_id; check} {exec= change_size_by ~size_f:decr_size alist_id; check}
let addAll_at_index alist_id index_exp alist_to_add = let addAll_at_index alist_id index_exp alist_to_add =
let exec _model_env ~ret mem = let exec ({integer_type_widths} as model_env) ~ret mem =
let to_add_length = get_size alist_to_add mem in 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 change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem
in in
let check {location} mem cond_set = let check {location; integer_type_widths} mem cond_set =
let array_exp = Exp.Var alist_id in let array_exp = Exp.Var alist_id in
BoUtils.Check.collection_access ~index_exp ~array_exp ~is_collection_add:true mem location BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp
cond_set ~is_collection_add:true mem location cond_set
in in
{exec; check} {exec; check}
let get_or_set_at_index alist_id index_exp = let get_or_set_at_index alist_id index_exp =
let exec _model_env ~ret:_ mem = mem in 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 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 in
{exec; check} {exec; check}
end end

160
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -131,8 +131,8 @@ let rec must_alias_cmp : Exp.t -> Mem.astate -> bool =
false false
let rec eval : Exp.t -> Mem.astate -> Val.t = let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t =
fun exp mem -> fun integer_type_widths exp mem ->
if must_alias_cmp exp mem then Val.of_int 0 if must_alias_cmp exp mem then Val.of_int 0
else else
match exp with match exp with
@ -142,17 +142,18 @@ let rec eval : Exp.t -> Mem.astate -> Val.t =
let ploc = Loc.of_pvar pvar in let ploc = Loc.of_pvar pvar in
if Mem.is_stack_loc ploc mem then Mem.find ploc mem else Val.of_loc ploc if Mem.is_stack_loc ploc mem then Mem.find ploc mem else Val.of_loc ploc
| Exp.UnOp (uop, e, _) -> | Exp.UnOp (uop, e, _) ->
eval_unop uop e mem eval_unop integer_type_widths uop e mem
| Exp.BinOp (bop, e1, e2) -> | Exp.BinOp (bop, e1, e2) ->
eval_binop bop e1 e2 mem eval_binop integer_type_widths bop e1 e2 mem
| Exp.Const c -> | Exp.Const c ->
eval_const c eval_const c
| Exp.Cast (_, e) -> | Exp.Cast (_, e) ->
eval e mem eval integer_type_widths e mem
| Exp.Lfield (e, fn, _) -> | 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) -> | Exp.Lindex (e1, e2) ->
eval_lindex e1 e2 mem eval_lindex integer_type_widths e1 e2 mem
| Exp.Sizeof {nbytes= Some size} -> | Exp.Sizeof {nbytes= Some size} ->
Val.of_int size Val.of_int size
| Exp.Sizeof {nbytes= None} -> | Exp.Sizeof {nbytes= None} ->
@ -161,8 +162,10 @@ let rec eval : Exp.t -> Mem.astate -> Val.t =
Val.Itv.top Val.Itv.top
and eval_lindex array_exp index_exp mem = and eval_lindex integer_type_widths array_exp index_exp mem =
let array_v, index_v = (eval array_exp mem, eval index_exp mem) in 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 if ArrayBlk.is_bot (Val.get_array_blk array_v) then
match array_exp with match array_exp with
| Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) -> | 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 Val.plus_pi array_v index_v
and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t = and eval_unop : Typ.IntegerWidths.t -> Unop.t -> Exp.t -> Mem.astate -> Val.t =
fun unop e mem -> fun integer_type_widths unop e mem ->
let v = eval e mem in let v = eval integer_type_widths e mem in
match unop with match unop with
| Unop.Neg -> | Unop.Neg ->
Val.neg v Val.neg v
@ -196,10 +199,10 @@ and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t =
Val.lnot v Val.lnot v
and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = and eval_binop : Typ.IntegerWidths.t -> Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
fun binop e1 e2 mem -> fun integer_type_widths binop e1 e2 mem ->
let v1 = eval e1 mem in let v1 = eval integer_type_widths e1 mem in
let v2 = eval e2 mem in let v2 = eval integer_type_widths e2 mem in
match binop with match binop with
| Binop.PlusA _ -> | Binop.PlusA _ ->
Val.plus_a v1 v2 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 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 the "x" is pointing to, on the other hand, (eval "x") returns the
abstract location of "x". *) abstract location of "x". *)
let rec eval_arr : Exp.t -> Mem.astate -> Val.t = let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t =
fun exp mem -> fun integer_type_widths exp mem ->
match exp with match exp with
| Exp.Var id -> ( | Exp.Var id -> (
match Mem.find_alias id mem with match Mem.find_alias id mem with
@ -259,14 +262,14 @@ let rec eval_arr : Exp.t -> Mem.astate -> Val.t =
| Exp.Lvar pvar -> | Exp.Lvar pvar ->
Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem
| Exp.BinOp (bop, e1, e2) -> | Exp.BinOp (bop, e1, e2) ->
eval_binop bop e1 e2 mem eval_binop integer_type_widths bop e1 e2 mem
| Exp.Cast (_, e) -> | Exp.Cast (_, e) ->
eval_arr e mem eval_arr integer_type_widths e mem
| Exp.Lfield (e, fn, _) -> | 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 Mem.find_set locs mem
| Exp.Lindex (e, _) -> | 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 Mem.find_set locs mem
| Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ -> | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ ->
Val.bot Val.bot
@ -334,10 +337,10 @@ let eval_sympath params sympath mem =
(ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v) (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 params =
let formals = get_formals callee_pdesc in 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 ParamBindings.make formals actuals
in in
let eval_sym s = 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) ((eval_sym, trace_of_sym), eval_locpath)
let mk_eval_sym 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 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 module Prune = struct
type astate = {prune_pairs: PrunePairs.astate; mem: Mem.astate} type astate = {prune_pairs: PrunePairs.astate; mem: Mem.astate}
@ -405,8 +410,8 @@ module Prune = struct
astate astate
let rec prune_binop_left : Exp.t -> astate -> astate = let rec prune_binop_left : Typ.IntegerWidths.t -> Exp.t -> astate -> astate =
fun e ({mem} as astate) -> fun integer_type_widths e ({mem} as astate) ->
match e with match e with
| Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e') | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e')
| Exp.BinOp ((Binop.Gt 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 match Mem.find_simple_alias x mem with
| Some lv -> | Some lv ->
let v = Mem.find lv mem in 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 update_mem_in_prune lv v' astate
| None -> | None ->
astate ) astate )
@ -423,7 +428,7 @@ module Prune = struct
match Mem.find_simple_alias x mem with match Mem.find_simple_alias x mem with
| Some lv -> | Some lv ->
let v = Mem.find lv mem in 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 update_mem_in_prune lv v' astate
| None -> | None ->
astate ) astate )
@ -431,7 +436,7 @@ module Prune = struct
match Mem.find_simple_alias x mem with match Mem.find_simple_alias x mem with
| Some lv -> | Some lv ->
let v = Mem.find lv mem in 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 update_mem_in_prune lv v' astate
| None -> | None ->
astate ) astate )
@ -443,84 +448,96 @@ module Prune = struct
Be careful when you take into account integer overflows in the abstract semantics [eval] Be careful when you take into account integer overflows in the abstract semantics [eval]
in the future. *) in the future. *)
astate astate
|> prune_binop_left (Exp.BinOp (comp, e1, Exp.BinOp (Binop.MinusA t, e3, e2))) |> prune_binop_left integer_type_widths
|> prune_binop_left (Exp.BinOp (comp, e2, Exp.BinOp (Binop.MinusA t, e3, e1))) (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 | Exp.BinOp
( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp) ( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp)
, Exp.BinOp (Binop.MinusA t, e1, e2) , Exp.BinOp (Binop.MinusA t, e1, e2)
, e3 ) -> , e3 ) ->
astate astate
|> prune_binop_left (Exp.BinOp (comp, e1, Exp.BinOp (Binop.PlusA t, e3, e2))) |> prune_binop_left integer_type_widths
|> prune_binop_left (Exp.BinOp (comp_rev comp, e2, Exp.BinOp (Binop.MinusA t, e1, e3))) (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 astate
let prune_binop_right : Exp.t -> astate -> astate = let prune_binop_right : Typ.IntegerWidths.t -> Exp.t -> astate -> astate =
fun e astate -> fun integer_type_widths e astate ->
match e with match e with
| Exp.BinOp (((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as c), e1, e2) | 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 astate
let is_unreachable_constant : Exp.t -> Mem.astate -> bool = let is_unreachable_constant : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> bool =
fun e m -> fun integer_type_widths e m ->
let v = eval e m in let v = eval integer_type_widths e m in
Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0)
&& PowLoc.is_bot (Val.get_pow_loc v) && PowLoc.is_bot (Val.get_pow_loc v)
&& ArrayBlk.is_bot (Val.get_array_blk v) && ArrayBlk.is_bot (Val.get_array_blk v)
let prune_unreachable : Exp.t -> astate -> astate = let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> astate -> astate =
fun e ({mem} as astate) -> fun integer_type_widths e ({mem} as astate) ->
if is_unreachable_constant e mem || Mem.is_relation_unsat mem then {astate with mem= Mem.bot} if is_unreachable_constant integer_type_widths e mem || Mem.is_relation_unsat mem then
{astate with mem= Mem.bot}
else astate else astate
let rec prune_helper e astate = let rec prune_helper integer_type_widths e astate =
let 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 in
match e with match e with
| Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> | 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 -> | 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, _) -> | 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) -> | 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) -> | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
astate astate
|> prune_helper (Exp.UnOp (Unop.LNot, e1, t)) |> prune_helper integer_type_widths (Exp.UnOp (Unop.LNot, e1, t))
|> prune_helper (Exp.UnOp (Unop.LNot, e2, 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.Lt as c), e1, e2), _)
| Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt 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.Le as c), e1, e2), _)
| Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge 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.Eq as c), e1, e2), _)
| Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne 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 astate
let prune : Exp.t -> Mem.astate -> Mem.astate = let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Mem.astate =
fun e mem -> fun integer_type_widths e mem ->
let mem = Mem.apply_latest_prune e mem in let mem = Mem.apply_latest_prune e mem in
let mem = 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 Mem.meet_constraints constrs mem
in 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 Mem.set_prune_pairs prune_pairs mem
end end
let get_matching_pairs : let get_matching_pairs :
Tenv.t Tenv.t
-> Typ.IntegerWidths.t
-> Val.t -> Val.t
-> Val.t -> Val.t
-> Exp.t option -> Exp.t option
@ -528,7 +545,7 @@ let get_matching_pairs :
-> Mem.astate -> Mem.astate
-> Mem.astate -> Mem.astate
-> (Relation.Var.t * Relation.SymExp.t option) list = -> (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_offset_sym v = Val.get_offset_sym v in
let get_size_sym v = Val.get_size_sym v in let get_size_sym v = Val.get_size_sym v in
let get_field_name (fn, _, _) = fn 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 -> Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var ->
let sym_exp_opt = let sym_exp_opt =
Option.first_some 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)) (Relation.SymExp.of_sym (Val.get_sym v2))
in in
(var, sym_exp_opt) :: l ) (var, sym_exp_opt) :: l )
@ -611,17 +630,26 @@ let rec list_fold2_def :
let get_subst_map : let get_subst_map :
Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> Relation.SubstMap.t = Tenv.t
fun tenv callee_pdesc params caller_mem callee_exit_mem -> -> 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 add_pair (formal, typ) (actual, actual_exp) rel_l =
let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in
let new_rel_matching = 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 in
List.rev_append new_rel_matching rel_l List.rev_append new_rel_matching rel_l
in in
let formals = get_formals callee_pdesc 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 = let rel_pairs =
list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:[] list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:[]
in in

27
infer/src/bufferoverrun/bufferOverrunUtils.ml
Unescape View File

@ -236,7 +236,7 @@ module Exec = struct
Dom.Mem.add_heap loc size mem 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 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_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 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 = Itv.of_int_lit length in
let length = let length =
Option.value_map dyn_length ~default:length ~f:(fun dyn_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 ) Itv.plus i length )
in in
let stride = Option.map stride ~f:IntLit.to_int_exn 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 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 collection_access integer_type_widths ~array_exp ~index_exp ?(is_collection_add = false) mem
let idx = Sem.eval index_exp mem in location cond_set =
let arr = Sem.eval array_exp mem in 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 idx_traces = Dom.Val.get_traces idx in
let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in
let idx = Dom.Val.get_itv idx in let idx = Dom.Val.get_itv idx in
@ -347,10 +348,12 @@ module Check = struct
~is_collection_add location cond_set ~is_collection_add location cond_set
let lindex ~array_exp ~index_exp mem location cond_set = let lindex integer_type_widths ~array_exp ~index_exp mem location cond_set =
let idx = Sem.eval index_exp mem in let idx = Sem.eval integer_type_widths index_exp mem in
let arr = Sem.eval_arr array_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 mem) index_exp 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 let relation = Dom.Mem.get_relation mem in
array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set 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 location cond_set ~is_collection_add:true
let lindex_byte ~array_exp ~byte_index_exp mem location cond_set = let lindex_byte integer_type_widths ~array_exp ~byte_index_exp mem location cond_set =
let idx = Sem.eval byte_index_exp mem in let idx = Sem.eval integer_type_widths byte_index_exp mem in
let arr = Sem.eval_arr array_exp mem in let arr = Sem.eval_arr integer_type_widths array_exp mem in
let relation = Dom.Mem.get_relation mem in let relation = Dom.Mem.get_relation mem in
array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set

10
infer/src/bufferoverrun/bufferOverrunUtils.mli
Unescape View File

@ -118,6 +118,7 @@ module Exec : sig
val init_array_fields : val init_array_fields :
Tenv.t Tenv.t
-> Typ.IntegerWidths.t
-> Typ.Procname.t -> Typ.Procname.t
-> Itv.SymbolPath.partial option -> Itv.SymbolPath.partial option
-> node_hash:int -> node_hash:int
@ -142,7 +143,8 @@ module Check : sig
-> PO.ConditionSet.t -> PO.ConditionSet.t
val lindex : val lindex :
array_exp:Exp.t Typ.IntegerWidths.t
-> array_exp:Exp.t
-> index_exp:Exp.t -> index_exp:Exp.t
-> Dom.Mem.astate -> Dom.Mem.astate
-> Location.t -> Location.t
@ -150,7 +152,8 @@ module Check : sig
-> PO.ConditionSet.t -> PO.ConditionSet.t
val lindex_byte : val lindex_byte :
array_exp:Exp.t Typ.IntegerWidths.t
-> array_exp:Exp.t
-> byte_index_exp:Exp.t -> byte_index_exp:Exp.t
-> Dom.Mem.astate -> Dom.Mem.astate
-> Location.t -> Location.t
@ -158,7 +161,8 @@ module Check : sig
-> PO.ConditionSet.t -> PO.ConditionSet.t
val collection_access : val collection_access :
array_exp:Exp.t Typ.IntegerWidths.t
-> array_exp:Exp.t
-> index_exp:Exp.t -> index_exp:Exp.t
-> ?is_collection_add:bool -> ?is_collection_add:bool
-> Dom.Mem.astate -> Dom.Mem.astate

33
infer/src/checkers/cost.ml
Unescape View File

@ -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. 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 match Ondemand.get_proc_desc callee_pname with
| None -> | None ->
L.(die InternalError) 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 callee_cost Typ.Procname.pp callee_pname
| Some _ -> | Some _ ->
let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in 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 ) BasicCost.subst callee_cost eval_sym )
@ -56,12 +60,15 @@ module TransferFunctionsNodesBasicCost = struct
module CFG = InstrCFG module CFG = InstrCFG
module Domain = NodesBasicCostDomain 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 cost_atomic_instruction = BasicCost.one
let exec_instr_cost inferbo_mem (astate : CostDomain.NodeInstructionToCostMap.astate) let exec_instr_cost integer_type_widths inferbo_mem
{ProcData.pdesc} (node : CFG.Node.t) instr : CostDomain.NodeInstructionToCostMap.astate = (astate : CostDomain.NodeInstructionToCostMap.astate) {ProcData.pdesc} (node : CFG.Node.t)
instr : CostDomain.NodeInstructionToCostMap.astate =
let key = CFG.Node.id node in let key = CFG.Node.id node in
let astate' = let astate' =
match instr with match instr with
@ -70,8 +77,8 @@ module TransferFunctionsNodesBasicCost = struct
match Payload.read pdesc callee_pname with match Payload.read pdesc callee_pname with
| Some {post= callee_cost} -> | Some {post= callee_cost} ->
if BasicCost.is_symbolic callee_cost then if BasicCost.is_symbolic callee_cost then
instantiate_cost ~caller_pdesc:pdesc ~inferbo_caller_mem:inferbo_mem instantiate_cost integer_type_widths ~caller_pdesc:pdesc
~callee_pname ~params ~callee_cost ~inferbo_caller_mem:inferbo_mem ~callee_pname ~params ~callee_cost
else callee_cost else callee_cost
| None -> | None ->
cost_atomic_instruction cost_atomic_instruction
@ -95,9 +102,10 @@ module TransferFunctionsNodesBasicCost = struct
astate' 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 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 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" 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 = let inferbo_invariant_map, summary =
BufferOverrunChecker.compute_invariant_map_and_check callback_args BufferOverrunChecker.compute_invariant_map_and_check callback_args
in in
@ -752,7 +760,10 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t =
in in
let instr_cfg = InstrCFG.from_pdesc proc_desc in let instr_cfg = InstrCFG.from_pdesc proc_desc in
let invariant_map_NodesBasicCost = 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 *) (*compute_WCET cfg invariant_map min_trees in *)
AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.empty AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.empty
in in

3
infer/src/checkers/cost.mli
Unescape View File

@ -10,7 +10,8 @@ open! IStd
val checker : Callbacks.proc_callback_t val checker : Callbacks.proc_callback_t
val instantiate_cost : val instantiate_cost :
caller_pdesc:Procdesc.t Typ.IntegerWidths.t
-> caller_pdesc:Procdesc.t
-> inferbo_caller_mem:BufferOverrunDomain.Mem.astate option -> inferbo_caller_mem:BufferOverrunDomain.Mem.astate option
-> callee_pname:Typ.Procname.t -> callee_pname:Typ.Procname.t
-> params:(Exp.t * 'a) list -> params:(Exp.t * 'a) list

12
infer/src/checkers/hoisting.ml
Unescape View File

@ -75,7 +75,8 @@ let do_report summary Call.({pname; loc}) loop_head_loc =
Reporting.log_error summary ~loc ~ltr IssueType.invariant_call message 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 (* If a function is modeled as variant for hoisting (like
List.size or __cast ), we don't want to report it *) List.size or __cast ), we don't want to report it *)
let is_variant_for_hoisting = 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_invariant_map = Lazy.force inferbo_invariant_map in
let inferbo_mem = BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map in let inferbo_mem = BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map in
(* get the cost of the function call *) (* get the cost of the function call *)
Cost.instantiate_cost ~caller_pdesc:proc_desc ~inferbo_caller_mem:inferbo_mem Cost.instantiate_cost integer_type_widths ~caller_pdesc:proc_desc
~callee_pname:pname ~params ~callee_cost:cost ~inferbo_caller_mem:inferbo_mem ~callee_pname:pname ~params ~callee_cost:cost
|> Itv.NonNegativePolynomial.is_symbolic |> Itv.NonNegativePolynomial.is_symbolic
| _ -> | _ ->
false 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 cfg = InstrCFG.from_pdesc proc_desc in
let proc_data = ProcData.make_default proc_desc tenv in let proc_data = ProcData.make_default proc_desc tenv in
(* computes reaching defs: node -> (var -> node set) *) (* 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 let loop_head_loc = Procdesc.Node.get_loc loop_head in
HoistCalls.iter HoistCalls.iter
(fun call -> (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 ) do_report summary call loop_head_loc )
inv_instrs ) inv_instrs )
loop_head_to_inv_instrs ; loop_head_to_inv_instrs ;

Write Preview
Loading…
Cancel
Save