[pulse] move to SIL proper

Summary:
[apologies for the unreviewable diff...]

Get rid of HIL expressions in pulse. This finishes the HIL -> SIL
migration. The first step made pulse start from SIL instructions but
would translate most accesses to HIL to re-use most of the existing
pulse code. This diff gets rid of the intermediate translation of SIL
expressions to HIL expressions.

Big changes:
1. `PulseOperations` mostly rewritten, driven by using `Exp.t` instead of `HilExp.AccessExpression.t` for everything.
2. Stop trying to reverse-engineer what addresses mean in terms of
   access paths from program variables. Rely on the trace pointing at
   the right places in the code to be enough. This is because it wasn't
   that useful (and could even be misleading when wrong) but could be
   prohibitively expensive in degenerate cases (eg nodes with tens of
   thousands of successive array accesses...)
3. `PulseAbductiveDomain.apply_post` now returns the computed return
   value instead of recording it itself.
4. Change of vocabulary: `materialize` -> `eval`, `crumb` -> `event`
5. Function calls arguments are now evaluated prior to doing anything
   else, which saves everything else from having to (remember to) do
   that. In particular, this changes how models look quite a bit.

Reviewed By: mbouaziz

Differential Revision: D15986373

fbshipit-source-id: 1d79935de
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent 4ac252120b
commit 7f12ced394

@ -220,50 +220,6 @@ module AccessExpression = struct
let pp = pp_access_expr let pp = pp_access_expr
let to_accesses_fold access_expr ~init ~f_array_offset =
let rec aux accum accesses = function
| Base base ->
(accum, base, accesses)
| FieldOffset (access_expr, fld) ->
aux accum (Access.FieldAccess fld :: accesses) access_expr
| ArrayOffset (access_expr, typ, index) ->
let accum, index' = f_array_offset accum index in
aux accum (Access.ArrayAccess (typ, index') :: accesses) access_expr
| AddressOf access_expr ->
aux accum (Access.TakeAddress :: accesses) access_expr
| Dereference access_expr ->
aux accum (Access.Dereference :: accesses) access_expr
in
aux init [] access_expr
let to_accesses access_expr =
let (), base, accesses =
to_accesses_fold access_expr ~init:() ~f_array_offset:(fun () index -> ((), index))
in
(base, accesses)
let add_access access access_expr =
match (access : _ Access.t) with
| FieldAccess fld ->
Some (field_offset access_expr fld)
| ArrayAccess (typ, _index) ->
Some (array_offset access_expr typ None)
| Dereference ->
Some (dereference access_expr)
| TakeAddress ->
address_of access_expr
let add_rev_accesses rev_accesses access_expr =
List.fold rev_accesses ~init:(Some access_expr) ~f:(fun access_expr_opt access ->
let open Option.Monad_infix in
access_expr_opt >>= add_access access )
let add_accesses accesses access_expr = add_rev_accesses (List.rev accesses) access_expr
(** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *) (** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *)
let rec to_access_path t = let rec to_access_path t =
let rec to_access_path_ t = let rec to_access_path_ t =
@ -366,16 +322,6 @@ module AccessExpression = struct
init init
| Sizeof (_, exp_opt) -> | Sizeof (_, exp_opt) ->
fold_vars_exp_opt exp_opt ~init ~f fold_vars_exp_opt exp_opt ~init ~f
let appears_in_source_code access_expr =
(* should probably eventually check more than just the base but yolo *)
let var, _ = get_base access_expr in
Var.appears_in_source_code var
let to_source_string access_expr =
if appears_in_source_code access_expr then Some (F.asprintf "%a" pp access_expr) else None
end end
let rec get_typ tenv = function let rec get_typ tenv = function

@ -41,7 +41,7 @@ and access_expression = private
[@@deriving compare] [@@deriving compare]
module AccessExpression : sig module AccessExpression : sig
val of_id : Ident.t -> Typ.t -> access_expression val of_id : Ident.t -> Typ.t -> access_expression [@@warning "-32"]
val base : AccessPath.base -> access_expression val base : AccessPath.base -> access_expression
@ -56,15 +56,7 @@ module AccessExpression : sig
[@@warning "-32"] [@@warning "-32"]
(** address_of doesn't always make sense, eg [address_of (Dereference t)] is [None] *) (** address_of doesn't always make sense, eg [address_of (Dereference t)] is [None] *)
val address_of_base : AccessPath.base -> access_expression val address_of_base : AccessPath.base -> access_expression [@@warning "-32"]
val to_accesses_fold :
access_expression
-> init:'accum
-> f_array_offset:('accum -> t option -> 'accum * 'array_index)
-> 'accum * AccessPath.base * 'array_index Access.t list
val to_accesses : access_expression -> AccessPath.base * t option Access.t list
val to_access_path : access_expression -> AccessPath.t val to_access_path : access_expression -> AccessPath.t
@ -92,18 +84,6 @@ module AccessExpression : sig
[@@deriving compare] [@@deriving compare]
val fold_vars : (t, Var.t, 'accum) Container.fold val fold_vars : (t, Var.t, 'accum) Container.fold
val add_access : _ Access.t -> t -> t option
val add_accesses : _ Access.t list -> t -> t option
val add_rev_accesses : _ Access.t list -> t -> t option
val appears_in_source_code : t -> bool
val to_source_string : t -> string option
(** get a string representation of the access expression in terms of symbols that appear in the
program, to show to the user *)
end end
val pp : F.formatter -> t -> unit val pp : F.formatter -> t -> unit

@ -11,7 +11,7 @@ module F = Format
(** type of a procedure call; either direct or via function pointer *) (** type of a procedure call; either direct or via function pointer *)
type call = Direct of Typ.Procname.t | Indirect of HilExp.AccessExpression.t [@@deriving compare] type call = Direct of Typ.Procname.t | Indirect of HilExp.AccessExpression.t [@@deriving compare]
val pp_call : F.formatter -> call -> unit val pp_call : F.formatter -> call -> unit [@@warning "-32"]
type t = type t =
| Assign of HilExp.AccessExpression.t * HilExp.t * Location.t | Assign of HilExp.AccessExpression.t * HilExp.t * Location.t

@ -57,7 +57,7 @@ type instr =
- [typ] is the root type of [lexp1] - [typ] is the root type of [lexp1]
- [exp2] is the expression whose value is store. *) - [exp2] is the expression whose value is stored. *)
| Prune of Exp.t * Location.t * bool * if_kind | Prune of Exp.t * Location.t * bool * if_kind
(** prune the state based on [exp=1], the boolean indicates whether true branch *) (** prune the state based on [exp=1], the boolean indicates whether true branch *)
| Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t

@ -10,6 +10,7 @@ module L = Logging
open Result.Monad_infix open Result.Monad_infix
module AbstractAddress = PulseDomain.AbstractAddress module AbstractAddress = PulseDomain.AbstractAddress
module InterprocAction = PulseDomain.InterprocAction module InterprocAction = PulseDomain.InterprocAction
module Invalidation = PulseDomain.Invalidation
module ValueHistory = PulseDomain.ValueHistory module ValueHistory = PulseDomain.ValueHistory
include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
@ -45,114 +46,87 @@ module Payload = SummaryPayload.Make (struct
let field = Payloads.Fields.pulse let field = Payloads.Fields.pulse
end) end)
let proc_name_of_call call_exp =
match (call_exp : Exp.t) with
| Const (Cfun proc_name) | Closure {name= proc_name} ->
Some proc_name
| _ ->
None
module PulseTransferFunctions = struct module PulseTransferFunctions = struct
module CFG = ProcCfg.Exceptional module CFG = ProcCfg.Exceptional
module Domain = PulseAbductiveDomain module Domain = PulseAbductiveDomain
type extras = Summary.t type extras = Summary.t
let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc let exec_unknown_call reason ret call actuals _flags call_loc astate =
astate = let event = ValueHistory.Call {f= reason; location= call_loc} in
(* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *) let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in
let crumb = match proc_name_of_call call with
ValueHistory.Assignment | Some callee_pname when Typ.Procname.is_constructor callee_pname -> (
{lhs= PulseAbductiveDomain.explain_access_expr lhs_access astate; location= loc}
in
match rhs_exp with
| AccessExpression rhs_access -> (
PulseOperations.read loc rhs_access astate
>>= fun (astate, (rhs_addr, rhs_trace)) ->
let return_addr_trace = (rhs_addr, crumb :: rhs_trace) in
PulseOperations.write loc lhs_access return_addr_trace astate
>>= fun astate ->
match lhs_access with
| Base (var, _) when Var.is_return var ->
PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr rhs_trace
astate
| _ ->
Ok astate )
| Closure (pname, captured) ->
PulseOperations.Closures.record loc lhs_access pname captured astate
| Cast (_, e) ->
exec_assign summary lhs_access e loc astate
| _ ->
PulseOperations.read_all loc (HilExp.get_access_exprs rhs_exp) astate
>>= PulseOperations.havoc [crumb] loc lhs_access
let exec_unknown_call _summary ret (call : HilInstr.call) (actuals : HilExp.t list) _flags
call_loc astate =
let read_all args astate =
PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate
in
let crumb =
ValueHistory.Call
{ f= `HilCall call
; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
; location= call_loc }
in
let havoc_ret (ret, _) astate = PulseOperations.havoc_var [crumb] ret astate in
let read_actuals_havoc_ret actuals ret astate = read_all actuals astate >>| havoc_ret ret in
match call with
| Direct callee_pname when Typ.Procname.is_constructor callee_pname -> (
L.d_printfln "constructor call detected@." ; L.d_printfln "constructor call detected@." ;
match actuals with match actuals with
| AccessExpression constructor_access :: rest -> | (object_ref, _) :: _ ->
let constructed_object = HilExp.AccessExpression.dereference constructor_access in PulseOperations.havoc_deref call_loc object_ref [event] astate >>| havoc_ret ret
PulseOperations.havoc [crumb] call_loc constructed_object astate
>>= read_actuals_havoc_ret rest ret
| _ -> | _ ->
Ok (havoc_ret ret astate) ) Ok (havoc_ret ret astate) )
| Direct (Typ.Procname.ObjC_Cpp callee_pname) | Some (Typ.Procname.ObjC_Cpp callee_pname)
when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> ( when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> (
L.d_printfln "operator= detected@." ; L.d_printfln "operator= detected@." ;
match actuals with match actuals with
(* copy assignment *) (* copy assignment *)
| [AccessExpression lhs; HilExp.AccessExpression rhs] -> | [(lhs, _); _rhs] ->
let lhs_deref = HilExp.AccessExpression.dereference lhs in PulseOperations.havoc_deref call_loc lhs [event] astate >>| havoc_ret ret
let rhs_deref = HilExp.AccessExpression.dereference rhs in
PulseOperations.havoc [crumb] call_loc lhs_deref astate
>>= fun astate ->
PulseOperations.read call_loc rhs_deref astate >>| fst >>| havoc_ret ret
| _ -> | _ ->
read_actuals_havoc_ret actuals ret astate ) Ok (havoc_ret ret astate) )
| _ -> | _ ->
L.d_printfln "skipping unknown procedure@." ; L.d_printfln "skipping unknown procedure@." ;
read_actuals_havoc_ret actuals ret astate Ok (havoc_ret ret astate)
let interprocedural_call caller_summary ret (call : HilInstr.call) (actuals : HilExp.t list) let interprocedural_call caller_summary ret call_exp actuals flags call_loc astate =
flags call_loc astate = let unknown_function reason =
let unknown_function () = exec_unknown_call reason ret call_exp actuals flags call_loc astate >>| List.return
exec_unknown_call caller_summary ret call actuals flags call_loc astate >>| List.return
in in
match call with match proc_name_of_call call_exp with
| Direct callee_pname -> ( | Some callee_pname -> (
match Payload.read_full caller_summary.Summary.proc_desc callee_pname with match Payload.read_full caller_summary.Summary.proc_desc callee_pname with
| Some (callee_proc_desc, preposts) -> | Some (callee_proc_desc, preposts) ->
let formals = let formals =
Procdesc.get_formals callee_proc_desc Procdesc.get_formals callee_proc_desc
|> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
in in
PulseOperations.Interproc.call callee_pname ~formals ~ret ~actuals flags call_loc astate (* call {!PulseAbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
preposts List.fold_result preposts ~init:[] ~f:(fun posts pre_post ->
(* apply all pre/post specs *)
PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals
astate
>>| fun (post, return_val_opt) ->
let event = ValueHistory.Call {f= `Call call_exp; location= call_loc} in
let post =
match return_val_opt with
| Some return_val ->
PulseOperations.write_id (fst ret) (return_val, [event]) post
| None ->
PulseOperations.havoc_id (fst ret) [event] post
in
post :: posts )
| None -> | None ->
(* no spec found for some reason (unknown function, ...) *) (* no spec found for some reason (unknown function, ...) *)
L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ; L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;
unknown_function () ) unknown_function (`UnknownCall call_exp) )
| Indirect access_expression -> | None ->
L.d_printfln "Indirect call %a@\n" HilExp.AccessExpression.pp access_expression ; L.d_printfln "Indirect call %a@\n" Exp.pp call_exp ;
unknown_function () unknown_function (`IndirectCall call_exp)
(** has an object just gone out of scope? *) (** has an object just gone out of scope? *)
let get_out_of_scope_object (call : HilInstr.call) (actuals : HilExp.t list) let get_out_of_scope_object call_exp actuals (flags : CallFlags.t) =
(flags : CallFlags.t) =
(* injected destructors are precisely inserted where an object goes out of scope *) (* injected destructors are precisely inserted where an object goes out of scope *)
if flags.cf_injected_destructor then if flags.cf_injected_destructor then
match (call, actuals) with match (proc_name_of_call call_exp, actuals) with
| ( Direct (Typ.Procname.ObjC_Cpp pname) | Some (Typ.Procname.ObjC_Cpp pname), [(Exp.Lvar pvar, typ)]
, [AccessExpression (AddressOf (Base (ProgramVar pvar, typ)))] )
when Pvar.is_local pvar && not (Typ.Procname.ObjC_Cpp.is_inner_destructor pname) -> when Pvar.is_local pvar && not (Typ.Procname.ObjC_Cpp.is_inner_destructor pname) ->
(* ignore inner destructors, only trigger out of scope on the final destructor call *) (* ignore inner destructors, only trigger out of scope on the final destructor call *)
Some (pvar, typ) Some (pvar, typ)
@ -163,36 +137,44 @@ module PulseTransferFunctions = struct
(** [out_of_scope_access_expr] has just gone out of scope and in now invalid *) (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *)
let exec_object_out_of_scope call_loc (pvar, typ) astate = let exec_object_out_of_scope call_loc (pvar, typ) astate =
(* invalidate both [&x] and [x]: reading either is now forbidden *) let event =
let invalidate pvar typ access astate = InterprocAction.Immediate {imm= Invalidation.GoneOutOfScope (pvar, typ); location= call_loc}
PulseOperations.invalidate
(InterprocAction.Immediate {imm= GoneOutOfScope (pvar, typ); location= call_loc})
call_loc access astate
in in
let out_of_scope_base = HilExp.AccessExpression.base (Var.of_pvar pvar, typ) in (* invalidate both [&x] and [x]: reading either is now forbidden *)
invalidate pvar typ (HilExp.AccessExpression.dereference out_of_scope_base) astate PulseOperations.eval call_loc (Exp.Lvar pvar) astate
>>= invalidate pvar typ out_of_scope_base >>= fun (astate, out_of_scope_base) ->
PulseOperations.invalidate_deref call_loc event out_of_scope_base astate
>>= PulseOperations.invalidate call_loc event out_of_scope_base
let dispatch_call summary ret (call : HilInstr.call) (actuals : HilExp.t list) flags call_loc
astate =
let dispatch_call summary ret call_exp actuals call_loc flags astate =
(* evaluate all actuals *)
List.fold_result actuals ~init:(astate, [])
~f:(fun (astate, rev_actuals_evaled) (actual_exp, actual_typ) ->
PulseOperations.eval call_loc actual_exp astate
>>| fun (astate, actual_evaled) ->
(astate, (actual_evaled, actual_typ) :: rev_actuals_evaled) )
>>= fun (astate, rev_actuals_evaled) ->
let actuals_evaled = List.rev rev_actuals_evaled in
let model = let model =
match call with match proc_name_of_call call_exp with
| Indirect _ -> | Some callee_pname ->
PulseModels.dispatch callee_pname flags
| None ->
(* function pointer, etc.: skip for now *) (* function pointer, etc.: skip for now *)
None None
| Direct callee_pname ->
PulseModels.dispatch callee_pname flags
in in
match model with match model with
| Some model -> | Some model ->
model call_loc ~ret ~actuals astate model call_loc ~ret ~actuals:actuals_evaled astate
| None -> ( | None -> (
(* do interprocedural call then destroy objects going out of scope *) (* do interprocedural call then destroy objects going out of scope *)
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
let posts = interprocedural_call summary ret call actuals flags call_loc astate in let posts =
interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate
in
PerfEvent.(log (fun logger -> log_end_event logger ())) ; PerfEvent.(log (fun logger -> log_end_event logger ())) ;
match get_out_of_scope_object call actuals flags with match get_out_of_scope_object call_exp actuals flags with
| Some pvar_typ -> | Some pvar_typ ->
L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
posts posts
@ -203,66 +185,46 @@ module PulseTransferFunctions = struct
posts ) posts )
let hil_of_sil ?(add_deref = false) exp typ =
HilExp.of_sil ~include_array_indexes:true ~f_resolve_id:(fun _ -> None) ~add_deref exp typ
let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : Sil.instr) = let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : Sil.instr) =
match instr with match instr with
| Load (lhs_id, rhs_exp, typ, loc) -> | Load (lhs_id, rhs_exp, _typ, loc) ->
let lhs_access = HilExp.AccessExpression.of_id lhs_id typ in (* [lhs_id := *rhs_exp] *)
let rhs_hexp = hil_of_sil ~add_deref:true rhs_exp typ in let result =
let post = exec_assign summary lhs_access rhs_hexp loc astate |> check_error summary in PulseOperations.eval_deref loc rhs_exp astate
[post] >>| fun (astate, (rhs_addr, rhs_history)) ->
| Store (lhs_exp, typ, rhs_exp, loc) -> PulseOperations.write_id lhs_id (rhs_addr, rhs_history) astate
let lhs_access_expr =
match
HilExp.access_expr_of_exp ~include_array_indexes:true
~f_resolve_id:(fun _ -> None)
lhs_exp typ
with
| Some access_expr ->
access_expr
| None ->
L.die InternalError "Non-assignable LHS expression %a at %a" Exp.pp lhs_exp
Location.pp_file_pos loc
in in
let rhs_hexp = hil_of_sil rhs_exp typ in [check_error summary result]
let post = | Store (lhs_exp, _typ, rhs_exp, loc) ->
exec_assign summary lhs_access_expr rhs_hexp loc astate |> check_error summary (* [*lhs_exp := rhs_exp] *)
let event = ValueHistory.Assignment {location= loc} in
let result =
PulseOperations.eval loc rhs_exp astate
>>= fun (astate, (rhs_addr, rhs_history)) ->
PulseOperations.eval loc lhs_exp astate
>>= fun (astate, lhs_addr_hist) ->
PulseOperations.write_deref loc ~ref:lhs_addr_hist
~obj:(rhs_addr, event :: rhs_history)
astate
>>= fun astate ->
match lhs_exp with
| Lvar pvar when Pvar.is_return pvar ->
PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr
rhs_history astate
| _ ->
Ok astate
in in
[post] [check_error summary result]
| Prune (condition, loc, _is_then_branch, _if_kind) -> | Prune (condition, loc, _is_then_branch, _if_kind) ->
let condition_hexp = hil_of_sil condition (Typ.mk (Tint IBool)) in (* ignored for now *)
let post = let post = PulseOperations.eval loc condition astate |> check_error summary |> fst in
PulseOperations.read_all loc (HilExp.get_access_exprs condition_hexp) astate
|> check_error summary
in
[post] [post]
| Call ((ret_id, ret_typ), call_exp, actuals, loc, call_flags) -> | Call (ret, call_exp, actuals, loc, call_flags) ->
let ret_hil = (Var.of_id ret_id, ret_typ) in dispatch_call summary ret call_exp actuals loc call_flags astate |> check_error summary
let call_hil =
match hil_of_sil call_exp (Typ.mk Tvoid) with
| Constant (Cfun procname) | Closure (procname, _) ->
HilInstr.Direct procname
| HilExp.AccessExpression access_expr ->
HilInstr.Indirect access_expr
| call_exp ->
L.(die InternalError) "Unexpected call expression %a" HilExp.pp call_exp
in
let actuals_hil = List.map ~f:(fun (exp, typ) -> hil_of_sil exp typ) actuals in
let posts =
dispatch_call summary ret_hil call_hil actuals_hil call_flags loc astate
|> check_error summary
in
posts
| Metadata (ExitScope (vars, _)) -> | Metadata (ExitScope (vars, _)) ->
let post = PulseOperations.remove_vars vars astate in [PulseOperations.remove_vars vars astate]
[post]
| Metadata (VariableLifetimeBegins (pvar, _, location)) -> | Metadata (VariableLifetimeBegins (pvar, _, location)) ->
let var = Var.of_pvar pvar in [PulseOperations.realloc_var (Var.of_pvar pvar) location astate]
let post = PulseOperations.realloc_var var location astate in
[post]
| Metadata (Abstract _ | Nullify _ | Skip) -> | Metadata (Abstract _ | Nullify _ | Skip) ->
[astate] [astate]

@ -85,12 +85,6 @@ let ( <= ) ~lhs ~rhs =
~rhs:(rhs.post :> PulseDomain.t) ~rhs:(rhs.post :> PulseDomain.t)
let explain_access_expr access_expr {post} =
PulseDomain.explain_access_expr access_expr (post :> base_domain)
let explain_hil_exp hil_exp {post} = PulseDomain.explain_hil_exp hil_exp (post :> base_domain)
module Stack = struct module Stack = struct
let is_abducible astate var = let is_abducible astate var =
(* HACK: formals are pre-registered in the initial state *) (* HACK: formals are pre-registered in the initial state *)
@ -103,25 +97,25 @@ module Stack = struct
if phys_equal new_post astate.post then astate else {astate with post= new_post} if phys_equal new_post astate.post then astate else {astate with post= new_post}
let materialize var astate = let eval var astate =
match BaseStack.find_opt var (astate.post :> base_domain).stack with match BaseStack.find_opt var (astate.post :> base_domain).stack with
| Some addr_loc_opt -> | Some addr_hist ->
(astate, addr_loc_opt) (astate, addr_hist)
| None -> | None ->
let addr_loc_opt' = (AbstractAddress.mk_fresh (), None) in let addr_hist = (AbstractAddress.mk_fresh (), []) in
let post_stack = BaseStack.add var addr_loc_opt' (astate.post :> base_domain).stack in let post_stack = BaseStack.add var addr_hist (astate.post :> base_domain).stack in
let pre = let pre =
(* do not overwrite values of variables already in the pre *) (* do not overwrite values of variables already in the pre *)
if (not (BaseStack.mem var (astate.pre :> base_domain).stack)) && is_abducible astate var if (not (BaseStack.mem var (astate.pre :> base_domain).stack)) && is_abducible astate var
then then
let foot_stack = BaseStack.add var addr_loc_opt' (astate.pre :> base_domain).stack in let foot_stack = BaseStack.add var addr_hist (astate.pre :> base_domain).stack in
let foot_heap = let foot_heap =
BaseMemory.register_address (fst addr_loc_opt') (astate.pre :> base_domain).heap BaseMemory.register_address (fst addr_hist) (astate.pre :> base_domain).heap
in in
InvertedDomain.make foot_stack foot_heap InvertedDomain.make foot_stack foot_heap
else astate.pre else astate.pre
in in
({post= Domain.update astate.post ~stack:post_stack; pre}, addr_loc_opt') ({post= Domain.update astate.post ~stack:post_stack; pre}, addr_hist)
let add var addr_loc_opt astate = let add var addr_loc_opt astate =
@ -140,6 +134,8 @@ module Stack = struct
let fold f astate accum = BaseStack.fold f (astate.post :> base_domain).stack accum let fold f astate accum = BaseStack.fold f (astate.post :> base_domain).stack accum
let find_opt var astate = BaseStack.find_opt var (astate.post :> base_domain).stack let find_opt var astate = BaseStack.find_opt var (astate.post :> base_domain).stack
let mem var astate = BaseStack.mem var (astate.post :> base_domain).stack
end end
module Memory = struct module Memory = struct
@ -174,7 +170,7 @@ module Memory = struct
map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap) map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap)
let materialize_edge addr access astate = let eval_edge addr access astate =
match BaseMemory.find_edge_opt addr access (astate.post :> base_domain).heap with match BaseMemory.find_edge_opt addr access (astate.post :> base_domain).heap with
| Some addr_trace' -> | Some addr_trace' ->
(astate, addr_trace') (astate, addr_trace')
@ -224,11 +220,13 @@ let mk_initial proc_desc =
correspond to formals *) correspond to formals *)
let formals = let formals =
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
let location = Some (Procdesc.get_loc proc_desc) in let location = Procdesc.get_loc proc_desc in
Procdesc.get_formals proc_desc Procdesc.get_formals proc_desc
|> List.map ~f:(fun (mangled, _) -> |> List.map ~f:(fun (mangled, _) ->
let var = Var.of_pvar (Pvar.mk mangled proc_name) in let var = Var.of_pvar (Pvar.mk mangled proc_name) in
(var, (AbstractAddress.mk_fresh (), location)) ) ( var
, (AbstractAddress.mk_fresh (), [PulseDomain.ValueHistory.VariableDeclaration location])
) )
in in
let initial_stack = let initial_stack =
List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack
@ -323,14 +321,16 @@ module PrePost = struct
let fold_globals_of_stack stack call_state ~f = let fold_globals_of_stack stack call_state ~f =
Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:BaseStack.fold) Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:BaseStack.fold)
stack ~init:call_state ~f:(fun call_state (var, stack_value) -> stack ~init:call_state ~f:(fun call_state (var, stack_value) ->
if Var.is_global var then match var with
let call_state, (addr_caller, _) = | Var.ProgramVar pvar when Pvar.is_global pvar ->
let astate, var_value = Stack.materialize var call_state.astate in let call_state, (addr_caller, _) =
if phys_equal astate call_state.astate then (call_state, var_value) let astate, var_value = Stack.eval var call_state.astate in
else ({call_state with astate}, var_value) if phys_equal astate call_state.astate then (call_state, var_value)
in else ({call_state with astate}, var_value)
f var ~stack_value ~addr_caller call_state in
else Ok call_state ) f pvar ~stack_value ~addr_caller call_state
| _ ->
Ok call_state )
let visit call_state ~addr_callee ~addr_caller = let visit call_state ~addr_callee ~addr_caller =
@ -361,8 +361,8 @@ module PrePost = struct
(** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in
[call_state.astate] starting from address [addr_caller]. Report an error if some invalid [call_state.astate] starting from address [addr_caller]. Report an error if some invalid
addresses are traversed in the process. *) addresses are traversed in the process. *)
let rec materialize_pre_from_address callee_proc_name call_location access_expr ~pre ~addr_pre let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_caller
~addr_caller history call_state = history call_state =
let mk_action action = let mk_action action =
PulseDomain.InterprocAction.ViaCall PulseDomain.InterprocAction.ViaCall
{action; proc_name= callee_proc_name; location= call_location} {action; proc_name= callee_proc_name; location= call_location}
@ -381,25 +381,17 @@ module PrePost = struct
| Error invalidated_by -> | Error invalidated_by ->
Error Error
(PulseDiagnostic.AccessToInvalidAddress (PulseDiagnostic.AccessToInvalidAddress
{ access= explain_access_expr access_expr call_state.astate {invalidated_by; accessed_by= {action; history}})
; invalidated_by
; accessed_by= {action; history} })
| Ok astate -> | Ok astate ->
let call_state = {call_state with astate} in let call_state = {call_state with astate} in
Container.fold_result Container.fold_result
~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold)
~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) ->
let astate, (addr_caller_dest, _) = let astate, (addr_caller_dest, _) =
Memory.materialize_edge addr_caller access call_state.astate Memory.eval_edge addr_caller access call_state.astate
in in
let call_state = {call_state with astate} in let call_state = {call_state with astate} in
let access_expr = materialize_pre_from_address callee_proc_name call_location ~pre
(* if the new access expression doesn't make sense then keep the old one; should
be fine since this is used only for reporting *)
HilExp.AccessExpression.add_access access access_expr
|> Option.value ~default:access_expr
in
materialize_pre_from_address callee_proc_name call_location access_expr ~pre
~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest history call_state )) ~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest history call_state ))
|> function Some result -> result | None -> Ok call_state ) |> function Some result -> result | None -> Ok call_state )
@ -408,22 +400,16 @@ module PrePost = struct
has been instantiated with the corresponding [actual] into the current state has been instantiated with the corresponding [actual] into the current state
[call_state.astate] *) [call_state.astate] *)
let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state = let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state =
L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal (Pp.option AbstractAddress.pp) let addr_caller, trace = actual in
(Option.map ~f:fst3 actual) ; L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp addr_caller ;
match actual with (let open Option.Monad_infix in
| None -> PulseDomain.Stack.find_opt formal pre.PulseDomain.stack
(* the expression representing the actual couldn't be evaluated down to an abstract address >>= fun (addr_formal_pre, _) ->
*) PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap
Ok call_state >>| fun (formal_pre, _) ->
| Some (addr_caller, access_expr, trace) -> ( materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre
(let open Option.Monad_infix in ~addr_caller trace call_state)
PulseDomain.Stack.find_opt formal pre.PulseDomain.stack |> function Some result -> result | None -> Ok call_state
>>= fun (addr_formal_pre, _) ->
PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap
>>| fun (formal_pre, _) ->
materialize_pre_from_address callee_proc_name call_location access_expr ~pre
~addr_pre:formal_pre ~addr_caller trace call_state)
|> function Some result -> result | None -> Ok call_state )
let is_cell_read_only ~cell_pre_opt ~cell_post:(edges_post, attrs_post) = let is_cell_read_only ~cell_pre_opt ~cell_post:(edges_post, attrs_post) =
@ -448,7 +434,7 @@ module PrePost = struct
call [materialize_pre_from] on them. Give up if calling the function introduces aliasing. call [materialize_pre_from] on them. Give up if calling the function introduces aliasing.
*) *)
match match
IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal actual -> IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) ->
materialize_pre_from_actual callee_proc_name call_location materialize_pre_from_actual callee_proc_name call_location
~pre:(pre_post.pre :> PulseDomain.t) ~pre:(pre_post.pre :> PulseDomain.t)
~formal ~actual call_state ) ~formal ~actual call_state )
@ -463,15 +449,10 @@ module PrePost = struct
let materialize_pre_for_globals callee_proc_name call_location pre_post call_state = let materialize_pre_for_globals callee_proc_name call_location pre_post call_state =
fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state
~f:(fun var ~stack_value:(addr_pre, loc_opt) ~addr_caller call_state -> ~f:(fun _var ~stack_value:(addr_pre, history) ~addr_caller call_state ->
let trace = materialize_pre_from_address callee_proc_name call_location
Option.map loc_opt ~f:(fun loc -> PulseDomain.ValueHistory.VariableDeclaration loc)
|> Option.to_list
in
let access_expr = HilExp.AccessExpression.base (var, Typ.void) in
materialize_pre_from_address callee_proc_name call_location access_expr
~pre:(pre_post.pre :> PulseDomain.t) ~pre:(pre_post.pre :> PulseDomain.t)
~addr_pre ~addr_caller trace call_state ) ~addr_pre ~addr_caller history call_state )
let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state =
@ -591,7 +572,7 @@ module PrePost = struct
( subst ( subst
, ( addr_curr , ( addr_curr
, PulseDomain.ValueHistory.Call , PulseDomain.ValueHistory.Call
{f= `HilCall (Direct callee_proc_name); actuals= [ (* TODO *) ]; location= call_loc} {f= `Call (Const (Cfun callee_proc_name)); location= call_loc}
:: trace_post ) ) ) :: trace_post ) ) )
in in
let caller_post = let caller_post =
@ -608,36 +589,50 @@ module PrePost = struct
let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state = let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state =
L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal let addr_caller, _ = actual in
(Pp.option AbstractAddress.pp) (Option.map ~f:fst3 actual) ; L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractAddress.pp
match actual with addr_caller ;
match
let open Option.Monad_infix in
PulseDomain.Stack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack
>>= fun (addr_formal_pre, _) ->
PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference
(pre_post.pre :> PulseDomain.t).PulseDomain.heap
>>| fun (formal_pre, _) ->
record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre
~addr_caller call_state
with
| Some call_state ->
call_state
| None -> | None ->
call_state call_state
| Some (addr_caller, _access_expr, _trace) -> (
let open Option.Monad_infix in
match
PulseDomain.Stack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack
>>= fun (addr_formal_pre, _) ->
PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference
(pre_post.pre :> PulseDomain.t).PulseDomain.heap
>>| fun (formal_pre, _) ->
record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre
~addr_caller call_state
with
| Some call_state ->
call_state
| None ->
call_state )
let record_post_for_return callee_proc_name call_loc pre_post ~ret call_state = let record_post_for_return callee_proc_name call_loc pre_post call_state =
let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in
match PulseDomain.Stack.find_opt return_var (pre_post.post :> PulseDomain.t).stack with match PulseDomain.Stack.find_opt return_var (pre_post.post :> PulseDomain.t).stack with
| Some (addr_return, _) ->
record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_return
~addr_caller:(fst ret) call_state
| None -> | None ->
call_state (call_state, None)
| Some (addr_return, _) -> (
match
PulseDomain.Memory.find_edge_opt addr_return Dereference
(pre_post.post :> PulseDomain.t).PulseDomain.heap
with
| None ->
(call_state, None)
| Some (return_callee, _) ->
let return_caller =
match AddressMap.find_opt return_callee call_state.subst with
| Some return_caller ->
return_caller
| None ->
AbstractAddress.mk_fresh ()
in
let call_state =
record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee
~addr_caller:return_caller call_state
in
(call_state, Some return_caller) )
let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
@ -648,7 +643,7 @@ module PrePost = struct
between pre and post since it's unreliable, eg replace value read in pre with same value in between pre and post since it's unreliable, eg replace value read in pre with same value in
post but nuke other fields in the meantime? is that possible?). *) post but nuke other fields in the meantime? is that possible?). *)
match match
List.fold2 formals actuals ~init:call_state ~f:(fun call_state formal actual -> List.fold2 formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) ->
record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state
) )
with with
@ -673,15 +668,15 @@ module PrePost = struct
call_state call_state
let apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state = let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state =
PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ;
let r = let r =
apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals
call_state call_state
|> Option.map ~f:(fun call_state -> |> Option.map ~f:(fun call_state ->
apply_post_for_globals callee_proc_name call_location pre_post call_state apply_post_for_globals callee_proc_name call_location pre_post call_state
|> record_post_for_return callee_proc_name call_location pre_post ~ret |> record_post_for_return callee_proc_name call_location pre_post
|> fun {astate; _} -> astate ) |> fun ({astate; _}, return_caller) -> (astate, return_caller) )
in in
PerfEvent.(log (fun logger -> log_end_event logger ())) ; PerfEvent.(log (fun logger -> log_end_event logger ())) ;
r r
@ -701,7 +696,7 @@ module PrePost = struct
the noise that this will introduce since we don't care about values. For instance, if the pre the noise that this will introduce since we don't care about values. For instance, if the pre
is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is
to bake in some value analysis. *) to bake in some value analysis. *)
let apply callee_proc_name call_location pre_post ~formals ~ret ~actuals astate = let apply callee_proc_name call_location pre_post ~formals ~actuals astate =
L.d_printfln "Applying pre/post for %a(%a):@\n%a" Typ.Procname.pp callee_proc_name L.d_printfln "Applying pre/post for %a(%a):@\n%a" Typ.Procname.pp callee_proc_name
(Pp.seq ~sep:"," Var.pp) formals pp pre_post ; (Pp.seq ~sep:"," Var.pp) formals pp pre_post ;
let empty_call_state = let empty_call_state =
@ -714,11 +709,11 @@ module PrePost = struct
| exception Aliasing -> | exception Aliasing ->
(* can't make sense of the pre-condition in the current context: give up on that particular (* can't make sense of the pre-condition in the current context: give up on that particular
pre/post pair *) pre/post pair *)
Ok astate Ok (astate, None)
| None -> | None ->
(* couldn't apply the pre for some technical reason (as in: not by the fault of the (* couldn't apply the pre for some technical reason (as in: not by the fault of the
programmer as far as we know) *) programmer as far as we know) *)
Ok astate Ok (astate, None)
| Some (Error _ as error) -> | Some (Error _ as error) ->
(* error: the function call requires to read some state known to be invalid *) (* error: the function call requires to read some state known to be invalid *)
error error
@ -726,18 +721,13 @@ module PrePost = struct
(* reset [visited] *) (* reset [visited] *)
let call_state = {call_state with visited= AddressSet.empty} in let call_state = {call_state with visited= AddressSet.empty} in
(* apply the postcondition *) (* apply the postcondition *)
match match apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state with
apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state
with
| exception Aliasing -> | exception Aliasing ->
Ok astate Ok (astate, None)
| None -> | None ->
(* same as when trying to apply the pre: give up for that pre/post pair and return the (* same as when trying to apply the pre: give up for that pre/post pair and return the
original state *) original state *)
Ok astate Ok (astate, None)
| Some astate_post -> | Some astate_post ->
Ok astate_post ) Ok astate_post )
end end
let explain_access_expr access_expr {post} =
PulseDomain.explain_access_expr access_expr (post :> base_domain)

@ -29,7 +29,10 @@ module Stack : sig
val find_opt : Var.t -> t -> PulseDomain.Stack.value option val find_opt : Var.t -> t -> PulseDomain.Stack.value option
val materialize : Var.t -> t -> t * PulseDomain.Stack.value val eval : Var.t -> t -> t * PulseDomain.AddrTracePair.t
(** return the value of the variable in the stack or create a fresh one if needed *)
val mem : Var.t -> t -> bool
end end
(** stack operations like {!PulseDomain.Heap} but that also take care of propagating facts to the (** stack operations like {!PulseDomain.Heap} but that also take care of propagating facts to the
@ -43,7 +46,7 @@ module Memory : sig
val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
val check_valid : val check_valid :
HilExp.AccessExpression.t PulseDomain.explained PulseDomain.InterprocAction.t unit PulseDomain.InterprocAction.t
-> AbstractAddress.t -> AbstractAddress.t
-> t -> t
-> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result -> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result
@ -62,7 +65,9 @@ module Memory : sig
val std_vector_reserve : AbstractAddress.t -> t -> t val std_vector_reserve : AbstractAddress.t -> t -> t
val materialize_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t val eval_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
(** [eval_edge addr access astate] follows the edge [addr --access--> .] in memory and returns
what it points to or creates a fresh value if that edge didn't exist. *)
end end
module PrePost : sig module PrePost : sig
@ -79,18 +84,12 @@ module PrePost : sig
-> Location.t -> Location.t
-> t -> t
-> formals:Var.t list -> formals:Var.t list
-> ret:AbstractAddress.t * PulseDomain.ValueHistory.t -> actuals:((AbstractAddress.t * PulseDomain.ValueHistory.t) * Typ.t) list
-> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseDomain.ValueHistory.t) option
list
-> domain_t -> domain_t
-> (domain_t, PulseDiagnostic.t) result -> (domain_t * AbstractAddress.t option, PulseDiagnostic.t) result
(** return the abstract state after the call along with an optional return value *)
end end
val discard_unreachable : t -> t val discard_unreachable : t -> t
(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
keep its size down *) keep its size down *)
val explain_access_expr :
HilExp.AccessExpression.t -> t -> HilExp.AccessExpression.t PulseDomain.explained
val explain_hil_exp : HilExp.t -> t -> HilExp.t PulseDomain.explained

@ -10,9 +10,8 @@ module F = Format
type t = type t =
| AccessToInvalidAddress of | AccessToInvalidAddress of
{ access: HilExp.AccessExpression.t PulseDomain.explained { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t ; accessed_by: unit PulseDomain.Trace.t }
; accessed_by: HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t }
| StackVariableAddressEscape of | StackVariableAddressEscape of
{ variable: Var.t { variable: Var.t
; history: PulseDomain.ValueHistory.t ; history: PulseDomain.ValueHistory.t
@ -26,7 +25,7 @@ let get_location = function
let get_message = function let get_message = function
| AccessToInvalidAddress {access; accessed_by; invalidated_by; _} -> | AccessToInvalidAddress {accessed_by; invalidated_by; _} ->
(* The goal is to get one of the following messages depending on the scenario: (* The goal is to get one of the following messages depending on the scenario:
42: delete x; return x->f 42: delete x; return x->f
@ -44,47 +43,13 @@ let get_message = function
Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then
"`x->f` accesses `x`, which was invalidated at line 42 by `delete`" "`x->f` accesses `x`, which was invalidated at line 42 by `delete`"
*) *)
let pp_access_trace invalidated f let pp_access_trace f (trace : _ PulseDomain.Trace.t) =
(trace : HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t) =
match trace.action with match trace.action with
| Immediate {imm= access; _} -> ( | Immediate {imm= _; _} ->
match HilExp.AccessExpression.to_source_string (access :> HilExp.AccessExpression.t) with F.fprintf f "accessing memory that "
| Some access_s | ViaCall {proc_name; _} ->
when HilExp.AccessExpression.equal (access :> HilExp.AccessExpression.t) invalidated -> F.fprintf f "call to `%a` eventually accesses memory that " Typ.Procname.describe
F.fprintf f "`%s` " access_s proc_name
| Some access_s -> (
match HilExp.AccessExpression.to_source_string invalidated with
| Some invalidated_s ->
F.fprintf f "`%s` accesses `%s`, which " access_s invalidated_s
| None ->
F.fprintf f "access to `%s`, which " access_s )
| None -> (
match HilExp.AccessExpression.to_source_string invalidated with
| Some invalidated_s ->
F.fprintf f "`%s` " invalidated_s
| None ->
F.fprintf f "accessing memory that " ) )
| ViaCall {action; proc_name; _} -> (
let access_and_invalidated_s =
match
( HilExp.AccessExpression.to_source_string
(PulseDomain.InterprocAction.get_immediate action :> HilExp.AccessExpression.t)
, HilExp.AccessExpression.to_source_string invalidated )
with
| Some access_s, Some invalidated_s ->
Some (access_s, invalidated_s)
| Some s, None | None, Some s ->
Some (s, s)
| None, None ->
None
in
match access_and_invalidated_s with
| Some (access_s, invalidated_s) ->
F.fprintf f "call to `%a` eventually accesses `%s` but `%s` " Typ.Procname.describe
proc_name access_s invalidated_s
| None ->
F.fprintf f "call to `%a` eventually accesses `%a`, which " Typ.Procname.describe
proc_name HilExp.AccessExpression.pp invalidated )
in in
let pp_invalidation_trace line f trace = let pp_invalidation_trace line f trace =
match trace.PulseDomain.Trace.action with match trace.PulseDomain.Trace.action with
@ -103,9 +68,7 @@ let get_message = function
line line
in in
let invalidation_line = line_of_trace invalidated_by in let invalidation_line = line_of_trace invalidated_by in
F.asprintf "%a%a" F.asprintf "%a%a" pp_access_trace accessed_by
(pp_access_trace (access :> HilExp.AccessExpression.t))
accessed_by
(pp_invalidation_trace invalidation_line) (pp_invalidation_trace invalidation_line)
invalidated_by invalidated_by
| StackVariableAddressEscape {variable; _} -> | StackVariableAddressEscape {variable; _} ->
@ -123,9 +86,7 @@ let get_trace = function
F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation ) F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation )
invalidated_by invalidated_by
@@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here" @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here"
(fun f (access : HilExp.AccessExpression.t PulseDomain.explained) -> (fun f () -> F.pp_print_string f "invalid access occurs here")
F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp
(access :> HilExp.AccessExpression.t) )
accessed_by accessed_by
@@ [] @@ []
| StackVariableAddressEscape {history; location; _} -> | StackVariableAddressEscape {history; location; _} ->

@ -10,9 +10,8 @@ open! IStd
(** an error to report to the user *) (** an error to report to the user *)
type t = type t =
| AccessToInvalidAddress of | AccessToInvalidAddress of
{ access: HilExp.AccessExpression.t PulseDomain.explained { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t ; accessed_by: unit PulseDomain.Trace.t }
; accessed_by: HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t }
| StackVariableAddressEscape of | StackVariableAddressEscape of
{ variable: Var.t { variable: Var.t
; history: PulseDomain.ValueHistory.t ; history: PulseDomain.ValueHistory.t

@ -10,8 +10,6 @@ module L = Logging
(* {2 Abstract domain description } *) (* {2 Abstract domain description } *)
type 'a explained = 'a [@@deriving compare]
module Invalidation = struct module Invalidation = struct
type std_vector_function = type std_vector_function =
| Assign | Assign
@ -44,17 +42,17 @@ module Invalidation = struct
type t = type t =
| CFree of HilExp.AccessExpression.t explained | CFree
| CppDelete of HilExp.AccessExpression.t explained | CppDelete
| GoneOutOfScope of Pvar.t * Typ.t | GoneOutOfScope of Pvar.t * Typ.t
| Nullptr | Nullptr
| StdVector of std_vector_function * HilExp.AccessExpression.t explained | StdVector of std_vector_function
[@@deriving compare] [@@deriving compare]
let issue_type_of_cause = function let issue_type_of_cause = function
| CFree _ -> | CFree ->
IssueType.use_after_free IssueType.use_after_free
| CppDelete _ -> | CppDelete ->
IssueType.use_after_delete IssueType.use_after_delete
| GoneOutOfScope _ -> | GoneOutOfScope _ ->
IssueType.use_after_lifetime IssueType.use_after_lifetime
@ -64,12 +62,12 @@ module Invalidation = struct
IssueType.vector_invalidation IssueType.vector_invalidation
let describe f = function let describe f cause =
| CFree access_expr -> match cause with
F.fprintf f "was invalidated by call to `free()` on `%a`" HilExp.AccessExpression.pp | CFree ->
access_expr F.pp_print_string f "was invalidated by call to `free()`"
| CppDelete access_expr -> | CppDelete ->
F.fprintf f "was invalidated by `delete` on `%a`" HilExp.AccessExpression.pp access_expr F.pp_print_string f "was invalidated by `delete`"
| GoneOutOfScope (pvar, typ) -> | GoneOutOfScope (pvar, typ) ->
let pp_var f pvar = let pp_var f pvar =
if Pvar.is_cpp_temporary pvar then if Pvar.is_cpp_temporary pvar then
@ -78,17 +76,16 @@ module Invalidation = struct
in in
F.fprintf f "%a whose lifetime has ended" pp_var pvar F.fprintf f "%a whose lifetime has ended" pp_var pvar
| Nullptr -> | Nullptr ->
F.fprintf f "is the null pointer" F.pp_print_string f "is the null pointer"
| StdVector (std_vector_f, access_expr) -> | StdVector std_vector_f ->
F.fprintf f "was potentially invalidated by `%a()` on `%a`" pp_std_vector_function F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f
std_vector_f HilExp.AccessExpression.pp access_expr
let pp f invalidation = let pp f invalidation =
match invalidation with match invalidation with
| CFree _ -> | CFree ->
F.fprintf f "CFree(%a)" describe invalidation F.fprintf f "CFree(%a)" describe invalidation
| CppDelete _ -> | CppDelete ->
F.fprintf f "CppDelete(%a)" describe invalidation F.fprintf f "CppDelete(%a)" describe invalidation
| GoneOutOfScope _ -> | GoneOutOfScope _ ->
describe f invalidation describe f invalidation
@ -102,14 +99,10 @@ module ValueHistory = struct
type event = type event =
| VariableDeclaration of Location.t | VariableDeclaration of Location.t
| CppTemporaryCreated of Location.t | CppTemporaryCreated of Location.t
| Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t} | Assignment of {location: Location.t}
| Capture of | Capture of {captured_as: Pvar.t; location: Location.t}
{ captured_as: AccessPath.base
; captured: HilExp.AccessExpression.t explained
; location: Location.t }
| Call of | Call of
{ f: [`HilCall of HilInstr.call | `Model of string] { f: [`Call of Exp.t | `UnknownCall of Exp.t | `IndirectCall of Exp.t | `Model of string]
; actuals: HilExp.t explained list
; location: Location.t } ; location: Location.t }
[@@deriving compare] [@@deriving compare]
@ -118,20 +111,22 @@ module ValueHistory = struct
F.pp_print_string fmt "variable declared" F.pp_print_string fmt "variable declared"
| CppTemporaryCreated _ -> | CppTemporaryCreated _ ->
F.pp_print_string fmt "C++ temporary created" F.pp_print_string fmt "C++ temporary created"
| Capture {captured_as; captured; location= _} -> | Capture {captured_as; location= _} ->
F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured F.fprintf fmt "value captured as `%a`" (Pvar.pp Pp.text) captured_as
AccessPath.pp_base captured_as | Assignment _ ->
| Assignment {lhs; location= _} -> F.pp_print_string fmt "assigned"
if HilExp.AccessExpression.appears_in_source_code lhs then | Call {f; location= _} ->
F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs
| Call {f; actuals; location= _} ->
let pp_f fmt = function let pp_f fmt = function
| `HilCall call -> | `Call call_exp ->
F.fprintf fmt "%a" HilInstr.pp_call call F.fprintf fmt "`%a()`" Exp.pp call_exp
| `UnknownCall call_exp ->
F.fprintf fmt "unknown function `%a`" Exp.pp call_exp
| `IndirectCall call_exp ->
F.fprintf fmt "unresolved expression `%a`" Exp.pp call_exp
| `Model model -> | `Model model ->
F.pp_print_string fmt model F.fprintf fmt "`%s()` (pulse model)" model
in in
F.fprintf fmt "returned from call to `%a(%a)`" pp_f f (Pp.seq ~sep:"," HilExp.pp) actuals F.fprintf fmt "returned from call to %a" pp_f f
let location_of_event = function let location_of_event = function
@ -239,8 +234,8 @@ end
module Attribute = struct module Attribute = struct
type t = type t =
| Invalid of Invalidation.t Trace.t | Invalid of Invalidation.t Trace.t
| MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t | MustBeValid of unit InterprocAction.t
| AddressOfCppTemporary of Var.t * Location.t option | AddressOfCppTemporary of Var.t * ValueHistory.t
| Closure of Typ.Procname.t | Closure of Typ.Procname.t
| StdVectorReserve | StdVectorReserve
[@@deriving compare, variants] [@@deriving compare, variants]
@ -256,13 +251,7 @@ module Attribute = struct
let must_be_valid_rank = let must_be_valid_rank =
Variants.to_rank Variants.to_rank (MustBeValid (Immediate {imm= (); location= Location.dummy}))
(MustBeValid
(Immediate
{ imm=
HilExp.AccessExpression.base
(AccessPath.base_of_pvar (Pvar.mk_global Mangled.self) Typ.void)
; location= Location.dummy }))
let std_vector_reserve_rank = Variants.to_rank StdVectorReserve let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
@ -272,11 +261,11 @@ module Attribute = struct
(Trace.pp Invalidation.pp) f invalidation (Trace.pp Invalidation.pp) f invalidation
| MustBeValid action -> | MustBeValid action ->
F.fprintf f "MustBeValid (read by %a @ %a)" F.fprintf f "MustBeValid (read by %a @ %a)"
(InterprocAction.pp HilExp.AccessExpression.pp) (InterprocAction.pp (fun _ () -> ()))
action Location.pp action Location.pp
(InterprocAction.to_outer_location action) (InterprocAction.to_outer_location action)
| AddressOfCppTemporary (var, location_opt) -> | AddressOfCppTemporary (var, history) ->
F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt F.fprintf f "&%a (%a)" Var.pp var ValueHistory.pp history
| Closure pname -> | Closure pname ->
Typ.Procname.pp f pname Typ.Procname.pp f pname
| StdVectorReserve -> | StdVectorReserve ->
@ -532,22 +521,16 @@ module Stack = struct
F.fprintf f "%a%a" pp_ampersand var Var.pp var F.fprintf f "%a%a" pp_ampersand var Var.pp var
end end
module VarValue = struct include PrettyPrintable.MakePPMonoMap (VarAddress) (AddrTracePair)
type t = AbstractAddress.t * Location.t option [@@deriving compare]
let pp = Pp.pair ~fst:AbstractAddress.pp ~snd:(Pp.option Location.pp)
end
include PrettyPrintable.MakePPMonoMap (VarAddress) (VarValue)
let pp fmt m = let pp fmt m =
let pp_item fmt (var_address, v) = let pp_item fmt (var_address, v) =
F.fprintf fmt "%a=%a" VarAddress.pp var_address VarValue.pp v F.fprintf fmt "%a=%a" VarAddress.pp var_address AddrTracePair.pp v
in in
PrettyPrintable.pp_collection ~pp_item fmt (bindings m) PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
let compare = compare VarValue.compare let compare = compare AddrTracePair.compare
end end
type t = {heap: Memory.t; stack: Stack.t} type t = {heap: Memory.t; stack: Stack.t}
@ -787,77 +770,3 @@ let reachable_addresses astate =
~init:() ~finish:Fn.id ~init:() ~finish:Fn.id
~f:(fun () _ _ _ -> Continue ()) ~f:(fun () _ _ _ -> Continue ())
|> fst |> fst
let rec evaluate_accesses address accesses astate =
match accesses with
| [] ->
Some address
| access :: next_accesses ->
let open Option.Monad_infix in
Memory.find_edge_opt address access astate.heap
>>= fun (addr, _) -> evaluate_accesses addr next_accesses astate
let evaluate_access_path var should_deref astate =
let open Option.Monad_infix in
Stack.find_opt var astate.stack
>>= fun (addr_var, _) ->
if should_deref then evaluate_accesses addr_var [HilExp.Access.Dereference] astate
else Some addr_var
let explain_address address astate =
GraphVisit.fold astate ~init:() ~var_filter:Var.appears_in_source_code
~finish:(fun _ -> None)
~f:(fun () address' var accesses ->
if AbstractAddress.equal address address' then Stop (Some (var, accesses)) else Continue ()
)
|> snd
|> Option.bind ~f:(fun (var, rev_accesses) ->
let base = HilExp.AccessExpression.address_of_base (var, Typ.void) in
HilExp.AccessExpression.add_rev_accesses rev_accesses base )
let explain_access_expr access_expr astate =
if HilExp.AccessExpression.appears_in_source_code access_expr then access_expr
else
let (base_var, _), accesses = HilExp.AccessExpression.to_accesses access_expr in
let should_deref, accesses_left =
match accesses with [HilExp.Access.TakeAddress] -> (false, []) | _ -> (true, accesses)
in
match
let open Option.Monad_infix in
evaluate_access_path base_var should_deref astate
>>= fun base_address ->
explain_address base_address astate >>= HilExp.AccessExpression.add_accesses accesses_left
with
| Some explained ->
explained
| None ->
L.d_printfln "Can't explain how to reach address %a from state %a"
HilExp.AccessExpression.pp access_expr pp astate ;
access_expr
let rec explain_hil_exp (e : HilExp.t) astate =
match e with
| AccessExpression access_expr ->
HilExp.AccessExpression (explain_access_expr access_expr astate)
| UnaryOperator (op, e', t) ->
HilExp.UnaryOperator (op, explain_hil_exp e' astate, t)
| BinaryOperator (op, e1, e2) ->
HilExp.BinaryOperator (op, explain_hil_exp e1 astate, explain_hil_exp e2 astate)
| Exception e' ->
HilExp.Exception (explain_hil_exp e' astate)
| Closure (proc_name, captured) ->
HilExp.Closure
(proc_name, List.map captured ~f:(fun (base, e') -> (base, explain_hil_exp e' astate)))
| Constant _ ->
e
| Cast (t, e') ->
HilExp.Cast (t, explain_hil_exp e' astate)
| Sizeof (t, Some e') ->
HilExp.Sizeof (t, Some (explain_hil_exp e' astate))
| Sizeof (_, None) ->
e

@ -8,8 +8,6 @@
open! IStd open! IStd
module F = Format module F = Format
type 'a explained = private 'a
module Invalidation : sig module Invalidation : sig
type std_vector_function = type std_vector_function =
| Assign | Assign
@ -25,11 +23,11 @@ module Invalidation : sig
val pp_std_vector_function : Format.formatter -> std_vector_function -> unit val pp_std_vector_function : Format.formatter -> std_vector_function -> unit
type t = type t =
| CFree of HilExp.AccessExpression.t explained | CFree
| CppDelete of HilExp.AccessExpression.t explained | CppDelete
| GoneOutOfScope of Pvar.t * Typ.t | GoneOutOfScope of Pvar.t * Typ.t
| Nullptr | Nullptr
| StdVector of std_vector_function * HilExp.AccessExpression.t explained | StdVector of std_vector_function
[@@deriving compare] [@@deriving compare]
val issue_type_of_cause : t -> IssueType.t val issue_type_of_cause : t -> IssueType.t
@ -41,14 +39,10 @@ module ValueHistory : sig
type event = type event =
| VariableDeclaration of Location.t | VariableDeclaration of Location.t
| CppTemporaryCreated of Location.t | CppTemporaryCreated of Location.t
| Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t} | Assignment of {location: Location.t}
| Capture of | Capture of {captured_as: Pvar.t; location: Location.t}
{ captured_as: AccessPath.base
; captured: HilExp.AccessExpression.t explained
; location: Location.t }
| Call of | Call of
{ f: [`HilCall of HilInstr.call | `Model of string] { f: [`Call of Exp.t | `UnknownCall of Exp.t | `IndirectCall of Exp.t | `Model of string]
; actuals: HilExp.t explained list
; location: Location.t } ; location: Location.t }
type t = event list [@@deriving compare] type t = event list [@@deriving compare]
@ -82,8 +76,8 @@ end
module Attribute : sig module Attribute : sig
type t = type t =
| Invalid of Invalidation.t Trace.t | Invalid of Invalidation.t Trace.t
| MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t | MustBeValid of unit InterprocAction.t
| AddressOfCppTemporary of Var.t * Location.t option | AddressOfCppTemporary of Var.t * ValueHistory.t
| Closure of Typ.Procname.t | Closure of Typ.Procname.t
| StdVectorReserve | StdVectorReserve
[@@deriving compare] [@@deriving compare]
@ -92,7 +86,7 @@ end
module Attributes : sig module Attributes : sig
include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t
val get_must_be_valid : t -> HilExp.AccessExpression.t explained InterprocAction.t option val get_must_be_valid : t -> unit InterprocAction.t option
end end
module AbstractAddress : sig module AbstractAddress : sig
@ -117,21 +111,18 @@ module AbstractAddressSet : PrettyPrintable.PPSet with type elt = AbstractAddres
module AbstractAddressMap : PrettyPrintable.PPMap with type key = AbstractAddress.t module AbstractAddressMap : PrettyPrintable.PPMap with type key = AbstractAddress.t
module AddrTracePair : sig
type t = AbstractAddress.t * ValueHistory.t [@@deriving compare]
end
module Stack : sig module Stack : sig
include include PrettyPrintable.MonoMap with type key = Var.t and type value = AddrTracePair.t
PrettyPrintable.MonoMap
with type key = Var.t
and type value = AbstractAddress.t * Location.t option
(* need to shadow the declaration in [MonoMap] even though it is unused since [MapS.compare] has a (* need to shadow the declaration in [MonoMap] even though it is unused since [MapS.compare] has a
different type *) different type *)
val compare : t -> t -> int [@@warning "-32"] val compare : t -> t -> int [@@warning "-32"]
end end
module AddrTracePair : sig
type t = AbstractAddress.t * ValueHistory.t [@@deriving compare]
end
module Memory : sig module Memory : sig
module Access : module Access :
PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t
@ -194,7 +185,3 @@ type isograph_relation =
val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation
val is_isograph : lhs:t -> rhs:t -> mapping -> bool val is_isograph : lhs:t -> rhs:t -> mapping -> bool
val explain_access_expr : HilExp.AccessExpression.t -> t -> HilExp.AccessExpression.t explained
val explain_hil_exp : HilExp.t -> t -> HilExp.t explained

@ -9,8 +9,8 @@ open Result.Monad_infix
type exec_fun = type exec_fun =
Location.t Location.t
-> ret:Var.t * Typ.t -> ret:Ident.t * Typ.t
-> actuals:HilExp.t list -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list
-> PulseAbductiveDomain.t -> PulseAbductiveDomain.t
-> PulseAbductiveDomain.t list PulseOperations.access_result -> PulseAbductiveDomain.t list PulseOperations.access_result
@ -24,14 +24,10 @@ module C = struct
let free : model = let free : model =
fun location ~ret:_ ~actuals astate -> fun location ~ret:_ ~actuals astate ->
match actuals with match actuals with
| [AccessExpression deleted_access] -> | [(deleted_access, _)] ->
PulseOperations.invalidate PulseOperations.invalidate location
(PulseDomain.InterprocAction.Immediate (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CFree; location})
{ imm= deleted_access astate
PulseDomain.Invalidation.CFree
(PulseAbductiveDomain.explain_access_expr deleted_access astate)
; location })
location deleted_access astate
>>| List.return >>| List.return
| _ -> | _ ->
Ok [astate] Ok [astate]
@ -40,63 +36,38 @@ end
module Cplusplus = struct module Cplusplus = struct
let delete : model = let delete : model =
fun location ~ret:_ ~actuals astate -> fun location ~ret:_ ~actuals astate ->
PulseOperations.read_all location (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
>>= fun astate ->
match actuals with match actuals with
| [AccessExpression deleted_access] -> | [(deleted_access, _)] ->
PulseOperations.invalidate PulseOperations.invalidate location
(PulseDomain.InterprocAction.Immediate (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CppDelete; location})
{ imm= deleted_access astate
PulseDomain.Invalidation.CppDelete
(PulseAbductiveDomain.explain_access_expr deleted_access astate)
; location })
location deleted_access astate
>>| List.return >>| List.return
| _ -> | _ ->
Ok [astate] Ok [astate]
let operator_call : model = let operator_call : model =
fun location ~ret:(ret_var, _) ~actuals astate -> fun location ~ret:(ret_id, _) ~actuals astate ->
PulseOperations.read_all location (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
>>= fun astate ->
( match actuals with ( match actuals with
| AccessExpression lambda :: _ -> | (lambda, _) :: _ ->
PulseOperations.read location HilExp.AccessExpression.(dereference lambda) astate PulseOperations.Closures.check_captured_addresses
>>= fun (astate, address) -> (PulseDomain.InterprocAction.Immediate {imm= (); location})
PulseOperations.Closures.check_captured_addresses location lambda (fst address) astate (fst lambda) astate
| _ -> | _ ->
Ok astate ) Ok astate )
>>| fun astate -> >>| fun astate ->
[ PulseOperations.havoc_var let event = PulseDomain.ValueHistory.Call {f= `Model "<lambda>"; location} in
[ PulseDomain.ValueHistory.Call [PulseOperations.havoc_id ret_id [event] astate]
{ f= `Model "<lambda>"
; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
; location } ]
ret_var astate ]
let placement_new : model = let placement_new : model =
fun location ~ret:(ret_var, _) ~actuals astate -> fun location ~ret:(ret_id, _) ~actuals astate ->
let read_all args astate = let event = PulseDomain.ValueHistory.Call {f= `Model "<placement new>"; location} in
PulseOperations.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate
in
let crumb =
PulseDomain.ValueHistory.Call
{ f= `Model "<placement new>"
; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
; location }
in
match List.rev actuals with match List.rev actuals with
| HilExp.AccessExpression expr :: other_actuals -> | ((address, _), _) :: _ ->
PulseOperations.read location expr astate Ok [PulseOperations.write_id ret_id (address, [event]) astate]
>>= fun (astate, (address, trace)) -> | _ ->
PulseOperations.write_var ret_var (address, crumb :: trace) astate Ok [PulseOperations.havoc_id ret_id [event] astate]
|> read_all other_actuals >>| List.return
| _ :: other_actuals ->
read_all other_actuals astate >>| PulseOperations.havoc_var [crumb] ret_var >>| List.return
| [] ->
Ok [PulseOperations.havoc_var [crumb] ret_var astate]
end end
module StdVector = struct module StdVector = struct
@ -106,41 +77,39 @@ module StdVector = struct
"__internal_array" "__internal_array"
let to_internal_array vector = HilExp.AccessExpression.field_offset vector internal_array let to_internal_array location vector astate =
PulseOperations.eval_access location vector (FieldAccess internal_array) astate
let deref_internal_array vector =
HilExp.AccessExpression.(dereference (to_internal_array vector))
let element_of_internal_array vector index = let element_of_internal_array location vector index astate =
HilExp.AccessExpression.array_offset (deref_internal_array vector) Typ.void index to_internal_array location vector astate
>>= fun (astate, vector_internal_array) ->
PulseOperations.eval_access location vector_internal_array
(ArrayAccess (Typ.void, index))
astate
let reallocate_internal_array trace vector vector_f location astate = let reallocate_internal_array trace vector vector_f location astate =
let array_address = to_internal_array vector in to_internal_array location vector astate
let array = deref_internal_array vector in >>= fun (astate, array_address) ->
let invalidation = let invalidation =
PulseDomain.InterprocAction.Immediate PulseDomain.InterprocAction.Immediate
{ imm= {imm= PulseDomain.Invalidation.StdVector vector_f; location}
PulseDomain.Invalidation.StdVector
(vector_f, PulseAbductiveDomain.explain_access_expr vector astate)
; location }
in in
PulseOperations.invalidate_array_elements invalidation location array astate PulseOperations.invalidate_array_elements location invalidation array_address astate
>>= PulseOperations.invalidate invalidation location array >>= PulseOperations.invalidate_deref location invalidation array_address
>>= PulseOperations.havoc trace location array_address >>= PulseOperations.havoc_field location vector internal_array trace
let invalidate_references vector_f : model = let invalidate_references vector_f : model =
fun location ~ret:_ ~actuals astate -> fun location ~ret:_ ~actuals astate ->
match actuals with match actuals with
| AccessExpression vector :: _ -> | (vector, _) :: _ ->
let crumb = let crumb =
PulseDomain.ValueHistory.Call PulseDomain.ValueHistory.Call
{ f= { f=
`Model `Model
(Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f) (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f)
; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
; location } ; location }
in in
reallocate_internal_array [crumb] vector vector_f location astate >>| List.return reallocate_internal_array [crumb] vector vector_f location astate >>| List.return
@ -150,39 +119,22 @@ module StdVector = struct
let at : model = let at : model =
fun location ~ret ~actuals astate -> fun location ~ret ~actuals astate ->
let crumb = let event = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; location} in
PulseDomain.ValueHistory.Call
{ f= `Model "std::vector::at"
; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
; location }
in
match actuals with match actuals with
| [AccessExpression vector_access_expr; index_exp] -> | [(vector, _); (index, _)] ->
PulseOperations.read location element_of_internal_array location vector (fst index) astate
(element_of_internal_array vector_access_expr (Some index_exp)) >>| fun (astate, (addr, _)) -> [PulseOperations.write_id (fst ret) (addr, [event]) astate]
astate
>>= fun (astate, (addr, trace)) ->
PulseOperations.write location
(HilExp.AccessExpression.base ret)
(addr, crumb :: trace)
astate
>>| List.return
| _ -> | _ ->
Ok [PulseOperations.havoc_var [crumb] (fst ret) astate] Ok [PulseOperations.havoc_id (fst ret) [event] astate]
let reserve : model = let reserve : model =
fun location ~ret:_ ~actuals astate -> fun location ~ret:_ ~actuals astate ->
match actuals with match actuals with
| [AccessExpression vector; _value] -> | [(vector, _); _value] ->
let crumb = let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; location} in
PulseDomain.ValueHistory.Call
{ f= `Model "std::vector::reserve"
; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
; location }
in
reallocate_internal_array [crumb] vector Reserve location astate reallocate_internal_array [crumb] vector Reserve location astate
>>= PulseOperations.StdVector.mark_reserved location vector >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector)
>>| List.return >>| List.return
| _ -> | _ ->
Ok [astate] Ok [astate]
@ -191,16 +143,9 @@ module StdVector = struct
let push_back : model = let push_back : model =
fun location ~ret:_ ~actuals astate -> fun location ~ret:_ ~actuals astate ->
match actuals with match actuals with
| [AccessExpression vector; _value] -> | [(vector, _); _value] ->
let crumb = let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; location} in
PulseDomain.ValueHistory.Call if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then
{ f= `Model "std::vector::push_back"
; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate)
; location }
in
PulseOperations.StdVector.is_reserved location vector astate
>>= fun (astate, is_reserved) ->
if is_reserved then
(* assume that any call to [push_back] is ok after one called [reserve] on the same vector (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
(a perfect analysis would also make sure we don't exceed the reserved size) *) (a perfect analysis would also make sure we don't exceed the reserved size) *)
Ok [astate] Ok [astate]

@ -8,8 +8,8 @@ open! IStd
type exec_fun = type exec_fun =
Location.t Location.t
-> ret:Var.t * Typ.t -> ret:Ident.t * Typ.t
-> actuals:HilExp.t list -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list
-> PulseAbductiveDomain.t -> PulseAbductiveDomain.t
-> PulseAbductiveDomain.t list PulseOperations.access_result -> PulseAbductiveDomain.t list PulseOperations.access_result

@ -27,194 +27,179 @@ type t = PulseAbductiveDomain.t
type 'a access_result = ('a, PulseDiagnostic.t) result type 'a access_result = ('a, PulseDiagnostic.t) result
(** Check that the address is not known to be invalid *) (** Check that the [address] is not known to be invalid *)
let check_addr_access access action (address, history) astate = let check_addr_access action (address, history) astate =
Memory.check_valid action address astate Memory.check_valid action address astate
|> Result.map_error ~f:(fun invalidated_by -> |> Result.map_error ~f:(fun invalidated_by ->
let access = PulseAbductiveDomain.explain_access_expr access astate in PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= {action; history}} )
PulseDiagnostic.AccessToInvalidAddress
{access; invalidated_by; accessed_by= {action; history}} )
module Closures = struct
open Result.Monad_infix
(** Walk the heap starting from [addr] and following [path]. Stop either at the element before last module Memory = PulseAbductiveDomain.Memory
and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it
is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each let fake_capture_field_prefix = "__capture_"
address reached is valid. *)
let rec walk ~dereference_to_ignore access_expr action ~on_last addr_trace path astate = let mk_fake_field ~id =
let check_addr_access_optional action addr_trace astate = Typ.Fieldname.Clang.from_class_name
match dereference_to_ignore with (Typ.CStruct (QualifiedCppName.of_list ["std"; "function"]))
| Some 0 -> (Printf.sprintf "%s%d" fake_capture_field_prefix id)
Ok astate
let is_captured_fake_access (access : _ HilExp.Access.t) =
match access with
| FieldAccess fieldname
when String.is_prefix ~prefix:fake_capture_field_prefix (Typ.Fieldname.to_string fieldname)
->
true
| _ -> | _ ->
check_addr_access access_expr action addr_trace astate false
in
match (path, on_last) with
| [], `Access -> let mk_capture_edges captured =
Ok (astate, addr_trace) let fake_fields =
| [], `Overwrite _ -> List.rev_mapi captured ~f:(fun id captured_addr_trace ->
L.die InternalError "Cannot overwrite last address in empty path" (HilExp.Access.FieldAccess (mk_fake_field ~id), captured_addr_trace) )
| [a], `Overwrite new_addr_trace -> in
check_addr_access_optional action addr_trace astate Memory.Edges.of_seq (Caml.List.to_seq fake_fields)
>>| fun astate ->
let astate = Memory.add_edge (fst addr_trace) a new_addr_trace astate in
(astate, new_addr_trace) let check_captured_addresses action lambda_addr astate =
| a :: path, _ -> match Memory.find_opt lambda_addr astate with
check_addr_access_optional action addr_trace astate | None ->
>>= fun astate -> Ok astate
let dereference_to_ignore = | Some (edges, attributes) ->
Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function
in | Attribute.Closure _ ->
let astate, addr_trace' = Memory.materialize_edge (fst addr_trace) a astate in IContainer.iter_result
let access_expr = ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges
HilExp.AccessExpression.add_access a access_expr |> Option.value ~default:access_expr ~f:(fun (access, addr_trace) ->
in if is_captured_fake_access access then
walk access_expr ~dereference_to_ignore action ~on_last addr_trace' path astate check_addr_access action addr_trace astate >>| fun _ -> ()
else Ok () )
| _ ->
let write_var var new_addr_trace astate = Ok () )
let astate, (var_address_of, _) = Stack.materialize var astate in >>| fun () -> astate
(* Update heap with var_address_of -*-> new_addr *)
Memory.add_edge var_address_of HilExp.Access.Dereference new_addr_trace astate
let record location pname captured astate =
let captured_addresses =
let ends_with_addressof = function HilExp.AccessExpression.AddressOf _ -> true | _ -> false List.rev_map captured ~f:(fun (captured_as, (address_captured, trace_captured)) ->
let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in
let last_dereference access_list = (address_captured, new_trace) )
let rec last_dereference_inner access_list index result = in
match access_list with let closure_addr = AbstractAddress.mk_fresh () in
| [] -> let fake_capture_edges = mk_capture_edges captured_addresses in
result let astate =
| HilExp.Access.Dereference :: rest -> Memory.set_cell closure_addr
last_dereference_inner rest (index + 1) (Some index) (fake_capture_edges, Attributes.singleton (Closure pname))
| _ :: rest -> astate
last_dereference_inner rest (index + 1) result in
in (astate, (closure_addr, (* TODO: trace *) []))
last_dereference_inner access_list 0 None end
let eval_var var astate = Stack.eval var astate
let rec to_accesses location access_expr astate =
let exception Failed_fold of PulseDiagnostic.t in let eval_access location addr_trace access astate =
try let addr = fst addr_trace in
HilExp.AccessExpression.to_accesses_fold access_expr ~init:astate let action = InterprocAction.Immediate {imm= (); location} in
~f_array_offset:(fun astate hil_exp_opt -> check_addr_access action addr_trace astate >>| fun astate -> Memory.eval_edge addr access astate
match hil_exp_opt with
| None ->
(astate, AbstractAddress.mk_fresh ()) let eval location exp0 astate =
| Some hil_exp -> ( let action = InterprocAction.Immediate {imm= (); location} in
match eval_hil_exp location hil_exp astate with let rec eval exp astate =
| Ok result -> match (exp : Exp.t) with
result | Var id ->
| Error diag -> Ok (eval_var (Var.of_id id) astate)
raise (Failed_fold diag) ) ) | Lvar pvar ->
|> Result.return Ok (eval_var (Var.of_pvar pvar) astate)
with Failed_fold diag -> Error diag | Lfield (exp', field, _) ->
eval exp' astate
>>= fun (astate, addr_trace) ->
(** add addresses to the state to give an address to the destination of the given access path *) check_addr_access action addr_trace astate
and walk_access_expr ~on_last astate access_expr location = >>| fun astate -> Memory.eval_edge (fst addr_trace) (FieldAccess field) astate
to_accesses location access_expr astate | Lindex (exp', exp_index) ->
>>= fun (astate, base, access_list) -> eval exp_index astate
let dereference_to_ignore = >>= fun (astate, addr_trace_index) ->
if ends_with_addressof access_expr then last_dereference access_list else None check_addr_access action addr_trace_index astate
>>= fun astate ->
eval exp' astate
>>= fun (astate, addr_trace) ->
check_addr_access action addr_trace astate
>>| fun astate ->
Memory.eval_edge (fst addr_trace) (ArrayAccess (Typ.void, fst addr_trace_index)) astate
| Closure {name; captured_vars} ->
List.fold_result captured_vars ~init:(astate, [])
~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) ->
eval capt_exp astate
>>| fun (astate, addr_trace) -> (astate, (captured_as, addr_trace) :: rev_captured) )
>>| fun (astate, rev_captured) ->
Closures.record location name (List.rev rev_captured) astate
| Cast (_, exp') ->
eval exp' astate
| Sizeof _ | UnOp _ | BinOp _ | Exn _ | Const _ ->
Ok (astate, (AbstractAddress.mk_fresh (), (* TODO history *) []))
in in
let access_var, _ = base in eval exp0 astate
if Config.write_html then
L.d_printfln "Accessing %a -> [%a]" Var.pp access_var
(Pp.seq ~sep:"," Memory.Access.pp) let eval_deref location exp astate =
access_list ; eval location exp astate
match (on_last, access_list) with >>= fun (astate, addr_trace) ->
| `Overwrite new_addr_trace, [] -> let action = InterprocAction.Immediate {imm= (); location} in
Ok (write_var access_var new_addr_trace astate, new_addr_trace) check_addr_access action addr_trace astate
| `Access, _ | `Overwrite _, _ :: _ -> ( >>| fun astate -> Memory.eval_edge (fst addr_trace) Dereference astate
let astate, base_addr_trace =
let astate, (addr, init_loc_opt) = Stack.materialize access_var astate in
let trace =
Option.map init_loc_opt ~f:(fun init_loc ->
if Var.is_cpp_temporary access_var then ValueHistory.CppTemporaryCreated init_loc
else ValueHistory.VariableDeclaration init_loc )
|> Option.to_list
in
(astate, (addr, trace))
in
match access_list with
| [HilExp.Access.TakeAddress] ->
Ok (astate, base_addr_trace)
| _ ->
let action =
InterprocAction.Immediate
{imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location}
in
walk
(HilExp.AccessExpression.base base)
~dereference_to_ignore action ~on_last base_addr_trace
(HilExp.Access.Dereference :: access_list)
astate )
(** Use the stack and heap to walk the access path represented by the given expression down to an
abstract address representing what the expression points to.
Return an error state if it traverses some known invalid address or if the end destination is
known to be invalid. *)
and materialize_address astate access_expr = walk_access_expr ~on_last:`Access astate access_expr
and read location access_expr astate = materialize_address astate access_expr location
and read_all location access_exprs astate =
List.fold_result access_exprs ~init:astate ~f:(fun astate access_expr ->
read location access_expr astate >>| fst )
and eval_hil_exp location (hil_exp : HilExp.t) astate =
match hil_exp with
| AccessExpression access_expr ->
read location access_expr astate >>| fun (astate, (addr, _)) -> (astate, addr)
| _ ->
read_all location (HilExp.get_access_exprs hil_exp) astate
>>| fun astate -> (astate, AbstractAddress.mk_fresh ())
(** Use the stack and heap to walk the access path represented by the given expression down to an
abstract address representing what the expression points to, and replace that with the given
address.
Return an error state if it traverses some known invalid address. *)
let overwrite_address astate access_expr new_addr_trace =
walk_access_expr ~on_last:(`Overwrite new_addr_trace) astate access_expr
(** Add the given address to the set of know invalid addresses. *)
let mark_invalid action address astate = Memory.invalidate address action astate
let realloc_var var location astate = let realloc_var var location astate =
Stack.add var (AbstractAddress.mk_fresh (), Some location) astate Stack.add var (AbstractAddress.mk_fresh (), [ValueHistory.VariableDeclaration location]) astate
let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate
let havoc trace location (access_expr : HilExp.AccessExpression.t) astate = let havoc_id id loc_opt astate =
overwrite_address astate access_expr (AbstractAddress.mk_fresh (), trace) location >>| fst if Stack.mem (Var.of_id id) astate then write_id id (AbstractAddress.mk_fresh (), loc_opt) astate
else astate
let write location access_expr addr astate = let action_of_address location = InterprocAction.Immediate {imm= (); location}
overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate
let write_access location addr_trace_ref access addr_trace_obj astate =
let action = action_of_address location in
check_addr_access action addr_trace_ref astate
>>| Memory.add_edge (fst addr_trace_ref) access addr_trace_obj
let invalidate cause location access_expr astate =
materialize_address astate access_expr location
>>= fun (astate, addr_trace) ->
check_addr_access access_expr
(Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location})
addr_trace astate
>>| mark_invalid cause addr_trace
let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
write_access location addr_trace_ref Dereference addr_trace_obj astate
let invalidate_array_elements cause location access_expr astate =
materialize_address astate access_expr location let write_field location addr_trace_ref field addr_trace_obj astate =
>>= fun (astate, addr_trace) -> write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate
check_addr_access access_expr
(Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location})
addr_trace astate let havoc_deref location addr_trace trace_obj astate =
write_deref location ~ref:addr_trace ~obj:(AbstractAddress.mk_fresh (), trace_obj) astate
let havoc_field location addr_trace field trace_obj astate =
write_field location addr_trace field (AbstractAddress.mk_fresh (), trace_obj) astate
let invalidate location cause addr_trace astate =
let action = action_of_address location in
check_addr_access action addr_trace astate >>| Memory.invalidate addr_trace cause
let invalidate_deref location cause (addr_ref, history) astate =
let astate, (addr_obj, _) = Memory.eval_edge addr_ref Dereference astate in
invalidate location cause (addr_obj, history) astate
let invalidate_array_elements location cause addr_trace astate =
let action = action_of_address location in
check_addr_access action addr_trace astate
>>| fun astate -> >>| fun astate ->
match Memory.find_opt (fst addr_trace) astate with match Memory.find_opt (fst addr_trace) astate with
| None -> | None ->
@ -224,7 +209,7 @@ let invalidate_array_elements cause location access_expr astate =
(fun access dest_addr_trace astate -> (fun access dest_addr_trace astate ->
match (access : Memory.Access.t) with match (access : Memory.Access.t) with
| ArrayAccess _ -> | ArrayAccess _ ->
mark_invalid cause dest_addr_trace astate Memory.invalidate dest_addr_trace cause astate
| _ -> | _ ->
astate ) astate )
edges astate edges astate
@ -263,9 +248,9 @@ let check_address_escape escape_location proc_desc address history astate =
check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate
let mark_address_of_cpp_temporary location variable address astate = let mark_address_of_cpp_temporary history variable address astate =
Memory.add_attributes address Memory.add_attributes address
(Attributes.singleton (AddressOfCppTemporary (variable, location))) (Attributes.singleton (AddressOfCppTemporary (variable, history)))
astate astate
@ -273,136 +258,10 @@ let remove_vars vars astate =
let astate = let astate =
List.fold vars ~init:astate ~f:(fun heap var -> List.fold vars ~init:astate ~f:(fun heap var ->
match Stack.find_opt var astate with match Stack.find_opt var astate with
| Some (address, location) when Var.is_cpp_temporary var -> | Some (address, history) when Var.is_cpp_temporary var ->
mark_address_of_cpp_temporary location var address astate mark_address_of_cpp_temporary history var address astate
| _ -> | _ ->
heap ) heap )
in in
let astate' = Stack.remove_vars vars astate in let astate' = Stack.remove_vars vars astate in
if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate' if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate'
module Closures = struct
open Result.Monad_infix
module Memory = PulseAbductiveDomain.Memory
let fake_capture_field_prefix = "__capture_"
let mk_fake_field ~id =
Typ.Fieldname.Clang.from_class_name
(Typ.CStruct (QualifiedCppName.of_list ["std"; "function"]))
(Printf.sprintf "%s%d" fake_capture_field_prefix id)
let is_captured_fake_access (access : _ HilExp.Access.t) =
match access with
| FieldAccess fieldname
when String.is_prefix ~prefix:fake_capture_field_prefix (Typ.Fieldname.to_string fieldname)
->
true
| _ ->
false
let mk_capture_edges captured =
let fake_fields =
List.rev_mapi captured ~f:(fun id captured_addr_trace ->
(HilExp.Access.FieldAccess (mk_fake_field ~id), captured_addr_trace) )
in
Memory.Edges.of_seq (Caml.List.to_seq fake_fields)
let check_captured_addresses location lambda addr astate =
match Memory.find_opt addr astate with
| None ->
Ok astate
| Some (edges, attributes) ->
IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function
| Attribute.Closure _ ->
IContainer.iter_result
~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges
~f:(fun (access, addr_trace) ->
if is_captured_fake_access access then
check_addr_access lambda
(Immediate
{imm= PulseAbductiveDomain.explain_access_expr lambda astate; location})
addr_trace astate
>>| fun _ -> ()
else Ok () )
| _ ->
Ok () )
>>| fun () -> astate
let write location access_expr pname captured astate =
let closure_addr = AbstractAddress.mk_fresh () in
write location access_expr
( closure_addr
, [ ValueHistory.Assignment
{lhs= PulseAbductiveDomain.explain_access_expr access_expr astate; location} ] )
astate
>>| fun astate ->
let fake_capture_edges = mk_capture_edges captured in
Memory.set_cell closure_addr (fake_capture_edges, Attributes.singleton (Closure pname)) astate
let record location access_expr pname captured astate =
List.fold_result captured ~init:(astate, [])
~f:(fun ((astate, captured) as result) (captured_as, captured_exp) ->
match captured_exp with
| HilExp.AccessExpression (AddressOf access_expr as captured_access_expr) ->
read location access_expr astate
>>= fun (astate, (address, trace)) ->
let new_trace =
ValueHistory.Capture
{ captured_as
; captured= PulseAbductiveDomain.explain_access_expr captured_access_expr astate
; location }
:: trace
in
Ok (astate, (address, new_trace) :: captured)
| _ ->
Ok result )
>>= fun (astate, captured_addresses) ->
write location access_expr pname captured_addresses astate
end
module StdVector = struct
open Result.Monad_infix
module Memory = PulseAbductiveDomain.Memory
let is_reserved location vector_access_expr astate =
read location vector_access_expr astate
>>| fun (astate, (addr, _)) -> (astate, Memory.is_std_vector_reserved addr astate)
let mark_reserved location vector_access_expr astate =
read location vector_access_expr astate
>>| fun (astate, (addr, _)) -> Memory.std_vector_reserve addr astate
end
module Interproc = struct
open Result.Monad_infix
(* compute addresses for actuals and then call {!PulseAbductiveDomain.PrePost.apply} on each
pre/post pair in the summary. *)
let call callee_pname ~formals ~ret ~actuals _flags call_loc astate pre_posts =
L.d_printfln "PulseOperations.call" ;
List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_actual_addresses) actual ->
match actual with
| HilExp.AccessExpression access_expr ->
read call_loc access_expr astate
>>| fun (astate, (addr, trace)) ->
(astate, Some (addr, access_expr, trace) :: rev_actual_addresses)
| _ ->
Ok (astate, None :: rev_actual_addresses) )
>>= fun (astate, rev_actual_addresses) ->
let actuals = List.rev rev_actual_addresses in
read call_loc HilExp.AccessExpression.(address_of_base ret) astate
>>= fun (astate, ret) ->
List.fold_result pre_posts ~init:[] ~f:(fun posts pre_post ->
(* apply all pre/post specs *)
PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~ret ~actuals
astate
>>| fun post -> post :: posts )
end

@ -14,66 +14,77 @@ type 'a access_result = ('a, PulseDiagnostic.t) result
module Closures : sig module Closures : sig
val check_captured_addresses : val check_captured_addresses :
Location.t unit PulseDomain.InterprocAction.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result
-> HilExp.AccessExpression.t
-> PulseDomain.AbstractAddress.t
-> t
-> t access_result
(** assert the validity of the addresses captured by the lambda *) (** assert the validity of the addresses captured by the lambda *)
val record :
Location.t
-> HilExp.AccessExpression.t
-> Typ.Procname.t
-> (AccessPath.base * HilExp.t) list
-> t
-> t access_result
(** record that the access expression points to a lambda with its captured addresses *)
end end
module StdVector : sig val eval : Location.t -> Exp.t -> t -> (t * PulseDomain.AddrTracePair.t) access_result
val is_reserved : Location.t -> HilExp.AccessExpression.t -> t -> (t * bool) access_result (** Use the stack and heap to evaluate the given expression down to an abstract address representing
its value.
val mark_reserved : Location.t -> HilExp.AccessExpression.t -> t -> t access_result Return an error state if it traverses some known invalid address or if the end destination is
end known to be invalid. *)
val read : val eval_deref : Location.t -> Exp.t -> t -> (t * PulseDomain.AddrTracePair.t) access_result
(** Like [eval] but evaluates [*exp]. *)
val eval_access :
Location.t Location.t
-> HilExp.AccessExpression.t -> PulseDomain.AddrTracePair.t
-> PulseDomain.Memory.Access.t
-> t -> t
-> (t * (AbstractAddress.t * PulseDomain.ValueHistory.t)) access_result -> (t * PulseDomain.AddrTracePair.t) access_result
(** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if
so dereferences it according to the access. *)
val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result val havoc_id : Ident.t -> PulseDomain.ValueHistory.t -> t -> t
val havoc_var : PulseDomain.ValueHistory.t -> Var.t -> t -> t val havoc_deref :
Location.t -> PulseDomain.AddrTracePair.t -> PulseDomain.ValueHistory.t -> t -> t access_result
val havoc : val havoc_field :
PulseDomain.ValueHistory.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result Location.t
-> PulseDomain.AddrTracePair.t
-> Typ.Fieldname.t
-> PulseDomain.ValueHistory.t
-> t
-> t access_result
val realloc_var : Var.t -> Location.t -> t -> t val realloc_var : Var.t -> Location.t -> t -> t
val write_var : Var.t -> AbstractAddress.t * PulseDomain.ValueHistory.t -> t -> t val write_id : Ident.t -> PulseDomain.Stack.value -> t -> t
val write : val write_deref :
Location.t Location.t
-> HilExp.AccessExpression.t -> ref:PulseDomain.AddrTracePair.t
-> AbstractAddress.t * PulseDomain.ValueHistory.t -> obj:PulseDomain.AddrTracePair.t
-> t -> t
-> t access_result -> t access_result
(** write the edge [ref --*--> obj] *)
val invalidate : val invalidate :
PulseDomain.Invalidation.t PulseDomain.InterprocAction.t Location.t
-> Location.t -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-> HilExp.AccessExpression.t -> PulseDomain.AddrTracePair.t
-> t -> t
-> t access_result -> t access_result
(** record that the address is invalid *)
val invalidate_deref :
Location.t
-> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-> PulseDomain.AddrTracePair.t
-> t
-> t access_result
(** record that what the address points to is invalid *)
val invalidate_array_elements : val invalidate_array_elements :
PulseDomain.Invalidation.t PulseDomain.InterprocAction.t Location.t
-> Location.t -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-> HilExp.AccessExpression.t -> PulseDomain.AddrTracePair.t
-> t -> t
-> t access_result -> t access_result
(** record that all the array elements that address points to is invalid *)
val remove_vars : Var.t list -> t -> t val remove_vars : Var.t list -> t -> t
@ -84,16 +95,3 @@ val check_address_escape :
-> PulseDomain.ValueHistory.t -> PulseDomain.ValueHistory.t
-> t -> t
-> t access_result -> t access_result
module Interproc : sig
val call :
Typ.Procname.t
-> formals:Var.t list
-> ret:AccessPath.base
-> actuals:HilExp.t list
-> CallFlags.t
-> Location.t
-> t
-> PulseSummary.t
-> PulseAbductiveDomain.t list access_result
end

@ -1,50 +1,51 @@
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `*ptr` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here]
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `ptr` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here]
codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `*(a.f)` here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int*>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `*(a.f)` here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int>::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `*(a.f)` here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `*(a.f)` here] codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `this` here,use-after-lifetime part of the trace starts here,invalid access to `this` here] codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `y`,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,assigned to `z`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,when calling `call_store()` here,when calling `store()` here,invalid access to `*(y.p)` here] codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `_fun_may_return_invalid_ptr_ok()`,assigned,when calling `call_store()` here,when calling `store()` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `result`,memory was invalidated by `delete` on `result` here,use-after-lifetime part of the trace starts here,assigned to `result`,invalid access to `*result` here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` on `*(*(&this.b))` here,use-after-lifetime part of the trace starts here,assigned to `*(this.b)`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access to `*(&rw.b->f)` here] codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access occurs here here]
codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,returned from call to `getwrapperStack()`,invalid access to `*(&rw.b->f)` here] codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_ReferenceWrapperStack::ReferenceWrapperStack()`,invalid access occurs here here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,returned here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `y`,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,assigned,returned here]
codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~UniquePtr` here,when calling `__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` on `*(*(&this.x_))` here,use-after-lifetime part of the trace starts here,assigned to `return`,returned from call to `temporaries::UniquePtr<temporaries::A>::get()`,assigned to `a`,invalid access to `*(a.s_)` here] codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~UniquePtr` here,when calling `__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `_fun_temporaries::UniquePtr<temporaries::A>::get()`,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,when calling `Simple` here,invalid access to `*(__param_0.f)` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,when calling `Simple` here,invalid access to `*(__param_0.f)` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,invalid access to `*(s.f)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `<placement new>()` (pulse model),assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,memory was invalidated by `delete` on `alias` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalid access to `*(alias.f)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `<placement new>()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `alias`,invalid access to `*(alias.f)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,assigned to `*(this.f)`,returned from call to `use_after_destructor::S::operator=()`,invalid access to `*(*(&s.f))` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_use_after_destructor::S::operator=()`,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(int))`,assigned to `*(this.f)`,returned from call to `use_after_destructor::S::S()`,invalid access to `*(*(&s.f))` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_use_after_destructor::S::S()`,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,invalid access to `*(pc.f)` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` on `global_pointer` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access to `global_pointer` here] codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `x` here] codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here here]
codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `*x` here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,invalid access to `*y` here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace_back()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::insert()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::insert()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::reserve()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::shrink_to_fit()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::reserve()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]
codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::shrink_to_fit()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]

Loading…
Cancel
Save