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

[inferbo] Sem.eval do not need a location

Browse Source 
Summary:
...so I just removed it
+ renamed `loc` of type `Location.t` to `location` to differentiate from `Loc.t` values

Reviewed By: jvillard

Differential Revision: D6358413

fbshipit-source-id: 2d3eba9
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 956d6d0a1d
commit 55ff444a74
6 changed files with 159 additions and 154 deletions
Show Stats Download Patch File Download Diff File

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

@ -50,9 +50,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem
else Dom.Mem.add_heap loc arr mem
in
let loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) in
match typ.Typ.desc with
| Typ.Tarray (typ, length, stride) ->
let loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) in
declare_array pname node location loc typ ~length
?stride:(Option.map ~f:IntLit.to_int stride)
~inst_num ~dimension:(dimension + 1) mem
@ -147,7 +147,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
List.fold ~f:add_formal ~init:(mem, inst_num) (Sem.get_formals pdesc) |> fst
let instantiate_ret ret callee_pname callee_exit_mem subst_map mem ret_alias loc =
let instantiate_ret ret callee_pname callee_exit_mem subst_map mem ret_alias location =
match ret with
| Some (id, _) ->
let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
@ -155,7 +155,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let ret_var = Loc.of_var (Var.of_id id) in
let add_ret_alias l = Dom.Mem.load_alias id l mem in
let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in
Dom.Val.subst ret_val subst_map loc |> Dom.Val.add_trace_elem (Trace.Return loc)
Dom.Val.subst ret_val subst_map location |> Dom.Val.add_trace_elem (Trace.Return location)
|> Fn.flip (Dom.Mem.add_stack ret_var) mem
| None ->
mem
@ -163,7 +163,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location mem =
let formals = Sem.get_formals pdesc in
let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem location) params in
let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem) params in
let f mem formal actual =
match (snd formal).Typ.desc with
| Typ.Tptr (typ, _) -> (
@ -203,17 +203,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let instantiate_mem
: Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t option -> Typ.Procname.t
-> (Exp.t * Typ.t) list -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate =
fun tenv ret callee_pdesc callee_pname params caller_mem summary loc ->
fun tenv ret callee_pdesc callee_pname params caller_mem summary location ->
let callee_entry_mem = Dom.Summary.get_input summary in
let callee_exit_mem = Dom.Summary.get_output summary in
let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in
match callee_pdesc with
| Some pdesc ->
let subst_map, ret_alias =
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias
in
instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem ret_alias loc
|> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map loc
instantiate_ret ret callee_pname callee_exit_mem subst_map caller_mem ret_alias location
|> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map
location
| None ->
caller_mem
@ -234,8 +235,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let pname = Procdesc.get_proc_name pdesc in
let output_mem =
match instr with
| Load (id, exp, _, loc) ->
let locs = Sem.eval exp mem loc |> Dom.Val.get_all_locs in
| Load (id, exp, _, _) ->
let locs = Sem.eval exp mem |> Dom.Val.get_all_locs in
let v = Dom.Mem.find_heap_set locs mem in
if Ident.is_none id then mem
else
@ -243,9 +244,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
if PowLoc.is_singleton locs then
Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem
else mem
| Store (exp1, _, exp2, loc) ->
let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in
let v = Sem.eval exp2 mem loc |> Dom.Val.add_trace_elem (Trace.Assign loc) in
| 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 mem = Dom.Mem.update_mem locs v mem in
if PowLoc.is_singleton locs then
let loc_v = PowLoc.min_elt locs in
@ -260,23 +261,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ ->
Dom.Mem.store_simple_alias loc_v exp2 mem
else mem
| Prune (exp, loc, _, _) ->
Sem.prune exp loc mem
| Call (ret, Const Cfun callee_pname, params, loc, _)
| Prune (exp, _, _, _) ->
Sem.prune exp mem
| Call (ret, Const Cfun callee_pname, params, location, _)
-> (
let quals = Typ.Procname.get_qualifiers callee_pname in
match QualifiedCppName.Dispatch.dispatch_qualifiers Models.dispatcher quals with
| Some model ->
model callee_pname ret params node loc mem
model callee_pname ret params node location mem
| None ->
match Summary.read_summary pdesc callee_pname with
| Some summary ->
let callee = extras callee_pname in
instantiate_mem tenv ret callee callee_pname params mem summary loc
instantiate_mem tenv ret callee callee_pname params mem summary location
| None ->
L.(debug BufferOverrun Verbose)
"/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp loc ;
Models.model_by_value Dom.Val.unknown callee_pname ret params node loc mem
"/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
location ;
Models.model_by_value Dom.Val.unknown callee_pname ret params node location mem
|> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown )
| Declare_locals (locals, location) ->
(* array allocation in stack e.g., int arr[10] *)
@ -295,10 +297,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in
let mem, inst_num = List.fold ~f:(try_decl_arr location) ~init:(mem, 1) locals in
declare_symbolic_parameter pdesc tenv node location inst_num mem
| Call (_, fun_exp, _, loc, _) ->
| Call (_, fun_exp, _, location, _) ->
let () =
L.(debug BufferOverrun Verbose)
"/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp loc
"/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp location
in
mem
| Remove_temps (temps, _) ->
@ -321,28 +323,28 @@ module Report = struct
let add_condition
: Typ.Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t
-> PO.ConditionSet.t =
fun pname node exp loc mem cond_set ->
fun pname node exp location mem cond_set ->
let array_access =
match exp with
| Exp.Var _ ->
let v = Sem.eval exp mem loc in
let v = Sem.eval exp mem in
let arr = Dom.Val.get_array_blk v in
let arr_traces = Dom.Val.get_traces v in
Some (arr, arr_traces, Itv.zero, TraceSet.empty, true)
| Exp.Lindex (e1, e2) ->
let locs = Sem.eval_locs e1 mem loc |> Dom.Val.get_all_locs in
let locs = Sem.eval_locs e1 mem |> Dom.Val.get_all_locs in
let v_arr = Dom.Mem.find_set locs mem in
let arr = Dom.Val.get_array_blk v_arr in
let arr_traces = Dom.Val.get_traces v_arr in
let v_idx = Sem.eval e2 mem loc in
let v_idx = Sem.eval e2 mem in
let idx = Dom.Val.get_itv v_idx in
let idx_traces = Dom.Val.get_traces v_idx in
Some (arr, arr_traces, idx, idx_traces, true)
| Exp.BinOp ((Binop.PlusA as bop), e1, e2) | Exp.BinOp ((Binop.MinusA as bop), e1, e2) ->
let v_arr = Sem.eval e1 mem loc in
let v_arr = Sem.eval e1 mem in
let arr = Dom.Val.get_array_blk v_arr in
let arr_traces = Dom.Val.get_traces v_arr in
let v_idx = Sem.eval e2 mem loc in
let v_idx = Sem.eval e2 mem in
let idx = Dom.Val.get_itv v_idx in
let idx_traces = Dom.Val.get_traces v_idx in
let is_plus = Binop.equal bop Binop.PlusA in
@ -363,8 +365,8 @@ module Report = struct
L.(debug BufferOverrun Verbose) "@]@." ;
match (size, idx) with
| NonBottom size, NonBottom idx ->
let traces = TraceSet.merge ~traces_arr ~traces_idx loc in
PO.ConditionSet.add_bo_safety pname loc site ~size ~idx traces cond_set
let traces = TraceSet.merge ~traces_arr ~traces_idx location in
PO.ConditionSet.add_bo_safety pname location site ~size ~idx traces cond_set
| _ ->
cond_set )
| None ->
@ -374,17 +376,16 @@ module Report = struct
let instantiate_cond
: Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate
-> Summary.payload -> Location.t -> PO.ConditionSet.t =
fun tenv caller_pname callee_pdesc params caller_mem summary loc ->
fun tenv caller_pname callee_pdesc params caller_mem summary location ->
let callee_entry_mem = Dom.Summary.get_input summary in
let callee_cond = Dom.Summary.get_cond_set summary in
match callee_pdesc with
| Some pdesc ->
let subst_map, _ =
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None
loc
in
let pname = Procdesc.get_proc_name pdesc in
PO.ConditionSet.subst callee_cond subst_map caller_pname pname loc
PO.ConditionSet.subst callee_cond subst_map caller_pname pname location
| _ ->
callee_cond
@ -452,13 +453,13 @@ module Report = struct
let pname = Procdesc.get_proc_name pdesc in
let cond_set =
match instr with
| Sil.Load (_, exp, _, loc) | Sil.Store (exp, _, _, loc) ->
add_condition pname node exp loc mem cond_set
| Sil.Call (_, Const Cfun callee_pname, params, loc, _) -> (
| Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) ->
add_condition pname node exp location mem cond_set
| Sil.Call (_, Const Cfun callee_pname, params, location, _) -> (
match Summary.read_summary pdesc callee_pname with
| Some summary ->
let callee = extras callee_pname in
instantiate_cond tenv pname callee params mem summary loc
instantiate_cond tenv pname callee params mem summary location
|> PO.ConditionSet.join cond_set
| _ ->
cond_set )
@ -472,13 +473,15 @@ module Report = struct
match instr with
| Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) ->
()
| Sil.Prune (cond, loc, true_branch, _) ->
| Sil.Prune (cond, location, true_branch, _) ->
let i = match cond with Exp.Const Const.Cint i -> i | _ -> IntLit.zero in
let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
let desc =
Errdesc.explain_condition_always_true_false tenv i cond node location
in
let exn =
Exceptions.Condition_always_true_false (desc, not true_branch, __POS__)
in
Reporting.log_warning_deprecated pname ~loc exn
Reporting.log_warning_deprecated pname ~loc:location exn
(* special case for when we're at the end of a procedure *)
| Sil.Call (_, Const Cfun pname, _, _, _)
when String.equal (Typ.Procname.get_method pname) "exit"
@ -490,10 +493,10 @@ module Report = struct
&& ExitStatement.has_multiple_sibling_nodes_and_one_successor node ->
()
| _ ->
let loc = Sil.instr_get_loc instr in
let desc = Errdesc.explain_unreachable_code_after loc in
let location = Sil.instr_get_loc instr in
let desc = Errdesc.explain_unreachable_code_after location in
let exn = Exceptions.Unreachable_code_after (desc, __POS__) in
Reporting.log_error_deprecated pname ~loc exn )
Reporting.log_error_deprecated pname ~loc:location exn )
| _ ->
()
in
@ -523,18 +526,18 @@ module Report = struct
fun trace desc ->
let f elem (trace, depth) =
match elem with
| Trace.Assign loc ->
(Errlog.make_trace_element depth loc "Assignment" [] :: trace, depth)
| Trace.ArrDecl loc ->
(Errlog.make_trace_element depth loc "ArrayDeclaration" [] :: trace, depth)
| Trace.Call loc ->
(Errlog.make_trace_element depth loc "Call" [] :: trace, depth + 1)
| Trace.Return loc ->
(Errlog.make_trace_element (depth - 1) loc "Return" [] :: trace, depth - 1)
| Trace.Assign location ->
(Errlog.make_trace_element depth location "Assignment" [] :: trace, depth)
| Trace.ArrDecl location ->
(Errlog.make_trace_element depth location "ArrayDeclaration" [] :: trace, depth)
| Trace.Call location ->
(Errlog.make_trace_element depth location "Call" [] :: trace, depth + 1)
| Trace.Return location ->
(Errlog.make_trace_element (depth - 1) location "Return" [] :: trace, depth - 1)
| Trace.SymAssign _ ->
(trace, depth)
| Trace.ArrAccess loc ->
(Errlog.make_trace_element depth loc ("ArrayAccess: " ^ desc) [] :: trace, depth)
| Trace.ArrAccess location ->
(Errlog.make_trace_element depth location ("ArrayAccess: " ^ desc) [] :: trace, depth)
in
List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev
@ -548,10 +551,10 @@ module Report = struct
| None ->
()
| Some issue_type ->
let caller_pname, loc =
let caller_pname, location =
match PO.ConditionTrace.get_cond_trace trace with
| PO.ConditionTrace.Inter (caller_pname, _, loc) ->
(caller_pname, loc)
| PO.ConditionTrace.Inter (caller_pname, _, location) ->
(caller_pname, location)
| PO.ConditionTrace.Intra pname ->
(pname, PO.ConditionTrace.get_location trace)
in
@ -564,9 +567,9 @@ module Report = struct
| trace ->
make_err_trace trace description
| exception _ ->
[Errlog.make_trace_element 0 loc description []]
[Errlog.make_trace_element 0 location description []]
in
Reporting.log_error_deprecated pname ~loc ~ltr:trace exn
Reporting.log_error_deprecated pname ~loc:location ~ltr:trace exn
in
PO.ConditionSet.iter conds ~f:report1

4
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -213,7 +213,7 @@ module Val = struct
let subst
: t -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t -> Location.t
-> t =
fun x (bound_map, trace_map) loc ->
fun x (bound_map, trace_map) location ->
let symbols = get_symbols x in
let traces_caller =
List.fold symbols
@ -221,7 +221,7 @@ module Val = struct
try TraceSet.join (Itv.SubstMap.find symbol trace_map) traces with Not_found -> traces)
~init:TraceSet.empty
in
let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces loc in
let traces = TraceSet.instantiate ~traces_caller ~traces_callee:x.traces location in
{x with itv= Itv.subst x.itv bound_map; arrayblk= ArrayBlk.subst x.arrayblk bound_map; traces}
|> normalize

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

@ -22,10 +22,10 @@ module Make (CFG : ProcCfg.S) = struct
Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node -> Location.t
-> Dom.Mem.astate -> Dom.Mem.astate
let set_uninitialized node (typ: Typ.t) loc mem =
let set_uninitialized node (typ: Typ.t) ploc mem =
match typ.desc with
| Tint _ | Tfloat _ ->
Dom.Mem.weak_update_heap loc Dom.Val.Itv.top mem
Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem
| _ ->
L.(debug BufferOverrun Verbose)
"/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp
@ -48,7 +48,7 @@ module Make (CFG : ProcCfg.S) = struct
match ret with
| Some (id, _) ->
let typ, stride, length0 = get_malloc_info (List.hd_exn params |> fst) in
let length = Sem.eval length0 mem (CFG.loc node) in
let length = Sem.eval length0 mem in
let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in
let v =
Sem.eval_array_alloc pname node typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1
@ -66,22 +66,22 @@ module Make (CFG : ProcCfg.S) = struct
model_malloc pname ret (List.tl_exn params) node location mem
let model_min _pname ret params _node location mem =
let model_min _pname ret params _node _location mem =
match (ret, params) with
| Some (id, _), [(e1, _); (e2, _)] ->
let i1 = Sem.eval e1 mem location |> Dom.Val.get_itv in
let i2 = Sem.eval e2 mem location |> Dom.Val.get_itv in
let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in
let i2 = Sem.eval 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
| _ ->
mem
let model_set_size _pname _ret params _node location mem =
let model_set_size _pname _ret params _node _location mem =
match params with
| [(e1, _); (e2, _)] ->
let locs = Sem.eval_locs e1 mem location |> Dom.Val.get_pow_loc in
let size = Sem.eval e2 mem location |> Dom.Val.get_itv in
let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in
let size = Sem.eval e2 mem |> Dom.Val.get_itv in
let arr = Dom.Mem.find_heap_set locs mem in
let arr = Dom.Val.set_array_size size arr in
Dom.Mem.strong_update_heap locs arr mem
@ -105,17 +105,16 @@ module Make (CFG : ProcCfg.S) = struct
match params with
| (e, _) :: _ ->
L.(debug BufferOverrun Medium)
"@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp
(Sem.eval e mem location) ;
"@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ;
mem
| _ ->
mem
let model_infer_set_array_length pname _ret params node location mem =
let model_infer_set_array_length pname _ret params node _location mem =
match params with
| [(Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)}); (length_exp, _)] ->
let length = Sem.eval length_exp mem location |> Dom.Val.get_itv in
let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
let stride = Option.map ~f:IntLit.to_int stride0 in
let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in
mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v

33
infer/src/bufferoverrun/bufferOverrunProofObligations.ml
Unescape View File

@ -167,23 +167,23 @@ module ConditionTrace = struct
type t =
{ proc_name: Typ.Procname.t
; loc: Location.t
; location: Location.t
; id: string
; cond_trace: cond_trace
; val_traces: ValTraceSet.t }
[@@deriving compare]
let pp_location : F.formatter -> t -> unit = fun fmt ct -> Location.pp_file_pos fmt ct.loc
let pp_location : F.formatter -> t -> unit = fun fmt ct -> Location.pp_file_pos fmt ct.location
let pp : F.formatter -> t -> unit =
fun fmt ct ->
if Config.bo_debug <= 1 then F.fprintf fmt "at %a" pp_location ct
else
match ct.cond_trace with
| Inter (_, pname, loc) ->
| Inter (_, pname, location) ->
let pname = Typ.Procname.to_string pname in
F.fprintf fmt "at %a by call %s() at %a (%a)" pp_location ct pname Location.pp_file_pos
loc ValTraceSet.pp ct.val_traces
location ValTraceSet.pp ct.val_traces
| Intra _ ->
F.fprintf fmt "%a (%a)" pp_location ct ValTraceSet.pp ct.val_traces
@ -192,14 +192,14 @@ module ConditionTrace = struct
fun fmt ct ->
match ct.cond_trace with
| Inter (_, pname, _)
when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model ct.loc.Location.file) ->
when Config.bo_debug >= 1 || not (SourceFile.is_cpp_model ct.location.Location.file) ->
F.fprintf fmt " %@ %a by call %a " pp_location ct MF.pp_monospaced
(Typ.Procname.to_string pname ^ "()")
| _ ->
()
let get_location : t -> Location.t = fun ct -> ct.loc
let get_location : t -> Location.t = fun ct -> ct.location
let get_cond_trace : t -> cond_trace = fun ct -> ct.cond_trace
@ -210,12 +210,15 @@ module ConditionTrace = struct
let make : Typ.Procname.t -> Location.t -> string -> ValTraceSet.t -> t =
fun proc_name loc id val_traces -> {proc_name; loc; id; cond_trace= Intra proc_name; val_traces}
fun proc_name location id val_traces ->
{proc_name; location; id; cond_trace= Intra proc_name; val_traces}
let make_call_and_subst ~traces_caller ~caller_pname ~callee_pname loc ct =
let val_traces = ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces loc in
{ct with cond_trace= Inter (caller_pname, callee_pname, loc); val_traces}
let make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location ct =
let val_traces =
ValTraceSet.instantiate ~traces_caller ~traces_callee:ct.val_traces location
in
{ct with cond_trace= Inter (caller_pname, callee_pname, location); val_traces}
end
@ -270,17 +273,17 @@ module ConditionSet = struct
let join condset1 condset2 = List.fold_left ~f:add_one condset1 ~init:condset2
let add_bo_safety pname loc id ~idx ~size val_traces condset =
let add_bo_safety pname location id ~idx ~size val_traces condset =
match Condition.make ~idx ~size with
| None ->
condset
| Some cond ->
let trace = ConditionTrace.make pname loc id val_traces in
let trace = ConditionTrace.make pname location id val_traces in
let cwt = {cond; trace} in
join [cwt] condset
let subst condset (bound_map, trace_map) caller_pname callee_pname loc =
let subst condset (bound_map, trace_map) caller_pname callee_pname location =
let subst_add_cwt condset cwt =
match Condition.get_symbols cwt.cond with
| [] ->
@ -299,8 +302,8 @@ module ConditionSet = struct
val_traces )
in
let make_call_and_subst trace =
ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname loc
trace
ConditionTrace.make_call_and_subst ~traces_caller ~caller_pname ~callee_pname
location trace
in
let trace = make_call_and_subst cwt.trace in
add_one condset {cond; trace}

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

@ -186,8 +186,8 @@ module Make (CFG : ProcCfg.S) = struct
false
let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t =
fun exp mem loc ->
let rec eval : Exp.t -> Mem.astate -> Val.t =
fun exp mem ->
if must_alias_cmp exp mem then Val.of_int 0
else
match exp with
@ -198,20 +198,19 @@ module Make (CFG : ProcCfg.S) = struct
let arr = Mem.find_stack_set ploc mem in
ploc |> Val.of_pow_loc |> Val.join arr
| Exp.UnOp (uop, e, _) ->
eval_unop uop e mem loc
eval_unop uop e mem
| Exp.BinOp (bop, e1, e2) ->
eval_binop bop e1 e2 mem loc
eval_binop bop e1 e2 mem
| Exp.Const c ->
eval_const c
| Exp.Cast (_, e) ->
eval e mem loc
eval e mem
| Exp.Lfield (e, fn, _) ->
eval e mem loc |> Val.get_array_locs |> Fn.flip PowLoc.append_field fn
|> Val.of_pow_loc
eval e mem |> Val.get_array_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc
| Exp.Lindex (e1, _) ->
let arr = eval e1 mem loc |> Val.get_array_blk in
let arr = eval e1 mem |> Val.get_array_blk in
(* must have array blk *)
(* let idx = eval e2 mem loc in *)
(* let idx = eval e2 mem in *)
let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in
(* if nested array, add the array blk *)
let arr = Mem.find_heap_set ploc mem in
@ -224,9 +223,9 @@ module Make (CFG : ProcCfg.S) = struct
Val.Itv.top
and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t =
fun unop e mem loc ->
let v = eval e mem loc in
and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t =
fun unop e mem ->
let v = eval e mem in
match unop with
| Unop.Neg ->
Val.neg v
@ -236,10 +235,10 @@ module Make (CFG : ProcCfg.S) = struct
Val.lnot v
and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t =
fun binop e1 e2 mem loc ->
let v1 = eval e1 mem loc in
let v2 = eval e2 mem loc in
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
match binop with
| Binop.PlusA ->
Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2)
@ -281,8 +280,8 @@ module Make (CFG : ProcCfg.S) = struct
Val.lor_sem v1 v2
let rec eval_locs : Exp.t -> Mem.astate -> Location.t -> Val.t =
fun exp mem loc ->
let rec eval_locs : Exp.t -> Mem.astate -> Val.t =
fun exp mem ->
match exp with
| Exp.Var id -> (
match Mem.find_alias id mem with
@ -293,14 +292,14 @@ module Make (CFG : ProcCfg.S) = struct
| Exp.Lvar pvar ->
pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc
| Exp.BinOp (bop, e1, e2) ->
eval_binop bop e1 e2 mem loc
eval_binop bop e1 e2 mem
| Exp.Cast (_, e) ->
eval_locs e mem loc
eval_locs e mem
| Exp.Lfield (e, fn, _) ->
eval e mem loc |> Val.get_all_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc
eval e mem |> Val.get_all_locs |> Fn.flip PowLoc.append_field fn |> Val.of_pow_loc
| Exp.Lindex (e1, e2) ->
let arr = eval e1 mem loc in
let idx = eval e2 mem loc in
let arr = eval e1 mem in
let idx = eval e2 mem in
Val.plus_pi arr idx
| Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ ->
Val.bot
@ -358,8 +357,8 @@ module Make (CFG : ProcCfg.S) = struct
mem
let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
fun e loc mem ->
let prune_binop_left : Exp.t -> Mem.astate -> Mem.astate =
fun e mem ->
match e with
| Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e')
| Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e')
@ -368,7 +367,7 @@ module Make (CFG : ProcCfg.S) = struct
match Mem.find_simple_alias x mem with
| Some lv ->
let v = Mem.find_heap lv mem in
let v' = Val.prune_comp comp v (eval e' mem loc) in
let v' = Val.prune_comp comp v (eval e' mem) in
Mem.update_mem (PowLoc.singleton lv) v' mem
| None ->
mem )
@ -376,7 +375,7 @@ module Make (CFG : ProcCfg.S) = struct
match Mem.find_simple_alias x mem with
| Some lv ->
let v = Mem.find_heap lv mem in
let v' = Val.prune_eq v (eval e' mem loc) in
let v' = Val.prune_eq v (eval e' mem) in
Mem.update_mem (PowLoc.singleton lv) v' mem
| None ->
mem )
@ -384,7 +383,7 @@ module Make (CFG : ProcCfg.S) = struct
match Mem.find_simple_alias x mem with
| Some lv ->
let v = Mem.find_heap lv mem in
let v' = Val.prune_ne v (eval e' mem loc) in
let v' = Val.prune_ne v (eval e' mem) in
Mem.update_mem (PowLoc.singleton lv) v' mem
| None ->
mem )
@ -392,8 +391,8 @@ module Make (CFG : ProcCfg.S) = struct
mem
let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
fun e loc mem ->
let prune_binop_right : Exp.t -> Mem.astate -> Mem.astate =
fun e mem ->
match e with
| Exp.BinOp ((Binop.Lt as c), e', Exp.Var x)
| Exp.BinOp ((Binop.Gt as c), e', Exp.Var x)
@ -401,43 +400,42 @@ module Make (CFG : ProcCfg.S) = struct
| Exp.BinOp ((Binop.Ge as c), e', Exp.Var x)
| Exp.BinOp ((Binop.Eq as c), e', Exp.Var x)
| Exp.BinOp ((Binop.Ne as c), e', Exp.Var x) ->
prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem
prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem
| _ ->
mem
let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool =
fun e loc m -> Val.( <= ) ~lhs:(eval e m loc) ~rhs:(Val.of_int 0)
let is_unreachable_constant : Exp.t -> Mem.astate -> bool =
fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0)
let prune_unreachable : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
fun e loc mem -> if is_unreachable_constant e loc mem then Mem.bot else mem
let prune_unreachable : Exp.t -> Mem.astate -> Mem.astate =
fun e mem -> if is_unreachable_constant e mem then Mem.bot else mem
let rec prune : Exp.t -> Location.t -> Mem.astate -> Mem.astate =
fun e loc mem ->
let rec prune : Exp.t -> Mem.astate -> Mem.astate =
fun e mem ->
let mem =
mem |> prune_unreachable e loc |> prune_unop e |> prune_binop_left e loc
|> prune_binop_right e loc
mem |> prune_unreachable e |> prune_unop e |> prune_binop_left e |> prune_binop_right e
in
match e with
| Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
prune e loc mem
prune e mem
| Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i ->
prune (Exp.UnOp (Unop.LNot, e, None)) loc mem
prune (Exp.UnOp (Unop.LNot, e, None)) mem
| Exp.UnOp (Unop.Neg, Exp.Var x, _) ->
prune (Exp.Var x) loc mem
prune (Exp.Var x) mem
| Exp.BinOp (Binop.LAnd, e1, e2) ->
mem |> prune e1 loc |> prune e2 loc
mem |> prune e1 |> prune e2
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
mem |> prune (Exp.UnOp (Unop.LNot, e1, t)) loc |> prune (Exp.UnOp (Unop.LNot, e2, t)) loc
mem |> prune (Exp.UnOp (Unop.LNot, e1, t)) |> prune (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 (Exp.BinOp (comp_not c, e1, e2)) loc mem
prune (Exp.BinOp (comp_not c, e1, e2)) mem
| _ ->
mem
@ -553,10 +551,10 @@ module Make (CFG : ProcCfg.S) = struct
let get_subst_map
: Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate
-> callee_ret_alias:AliasTarget.t option -> Location.t
-> callee_ret_alias:AliasTarget.t option
-> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t)
* AliasTarget.t option =
fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias loc ->
fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias ->
let add_pair (formal, typ) actual (l, ret_alias) =
let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in
let new_matching, ret_alias' =
@ -565,7 +563,7 @@ module Make (CFG : ProcCfg.S) = struct
(List.rev_append new_matching l, Option.first_some ret_alias ret_alias')
in
let formals = get_formals callee_pdesc in
let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in
let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in
let pairs, ret_alias =
list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None)
in

38
infer/src/bufferoverrun/bufferOverrunTrace.ml
Unescape View File

@ -35,18 +35,18 @@ module BoTrace = struct
let pp_elem : F.formatter -> elem -> unit =
fun fmt elem ->
match elem with
| Assign loc ->
F.fprintf fmt "Assign (%a)" Location.pp_file_pos loc
| ArrDecl loc ->
F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos loc
| Call loc ->
F.fprintf fmt "Call (%a)" Location.pp_file_pos loc
| Return loc ->
F.fprintf fmt "Return (%a)" Location.pp_file_pos loc
| SymAssign loc ->
F.fprintf fmt "SymAssign (%a)" Location.pp_file_pos loc
| ArrAccess loc ->
F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos loc
| Assign location ->
F.fprintf fmt "Assign (%a)" Location.pp_file_pos location
| ArrDecl location ->
F.fprintf fmt "ArrDecl (%a)" Location.pp_file_pos location
| Call location ->
F.fprintf fmt "Call (%a)" Location.pp_file_pos location
| Return location ->
F.fprintf fmt "Return (%a)" Location.pp_file_pos location
| SymAssign location ->
F.fprintf fmt "SymAssign (%a)" Location.pp_file_pos location
| ArrAccess location ->
F.fprintf fmt "ArrAccess (%a)" Location.pp_file_pos location
let pp : F.formatter -> t -> unit =
@ -78,30 +78,32 @@ module Set = struct
if is_empty t then singleton (BoTrace.singleton elem) else map (BoTrace.add_elem_last elem) t
let instantiate ~traces_caller ~traces_callee loc =
let instantiate ~traces_caller ~traces_callee location =
if is_empty traces_caller then
map (fun trace_callee -> BoTrace.add_elem_last (BoTrace.Call loc) trace_callee) traces_callee
map
(fun trace_callee -> BoTrace.add_elem_last (BoTrace.Call location) trace_callee)
traces_callee
else
fold
(fun trace_callee traces ->
fold
(fun trace_caller traces ->
let new_trace_caller = BoTrace.add_elem (BoTrace.Call loc) trace_caller in
let new_trace_caller = BoTrace.add_elem (BoTrace.Call location) trace_caller in
let new_trace = BoTrace.append trace_callee new_trace_caller in
add new_trace traces)
traces_caller traces)
traces_callee empty
let merge ~traces_arr ~traces_idx loc =
let merge ~traces_arr ~traces_idx location =
if is_empty traces_idx then
map (fun trace_arr -> BoTrace.add_elem (BoTrace.ArrAccess loc) trace_arr) traces_arr
map (fun trace_arr -> BoTrace.add_elem (BoTrace.ArrAccess location) trace_arr) traces_arr
else
fold
(fun trace_idx traces ->
fold
(fun trace_arr traces ->
let new_trace_idx = BoTrace.add_elem (BoTrace.ArrAccess loc) trace_idx in
let new_trace_idx = BoTrace.add_elem (BoTrace.ArrAccess location) trace_idx in
let new_trace = BoTrace.append new_trace_idx trace_arr in
add new_trace traces)
traces_arr traces)

Write Preview
Loading…
Cancel
Save