[pulse] add traces to the domain

Summary:
Record per-location traces. Actually, that doesn't quite make sense as a
location can be accessed in many ways, so associate a trace to each
*edge* in the memory graph. For instance, when doing `x->f = *y`, we
want to take the history of the `<val of y> --*--> ..` edge, add "assigned
at location blah" to it and store this extended history to the edge
`<val of x> --f--> ..`.

Use this machinery to print nicer traces in `infer explore` and better
error messages too (include the last assignment, like biabduction
messages).

Reviewed By: da319

Differential Revision: D13518668

fbshipit-source-id: 0a62fb55f
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent d9978bb897
commit 4c1ee2a485

@ -11,6 +11,8 @@ module F = Format
(** 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]
val pp_call : F.formatter -> call -> unit
type t =
| Assign of HilExp.AccessExpression.t * HilExp.t * Location.t
(** LHS access expression, RHS expression *)

@ -108,7 +108,7 @@ let get_simplified_name pv =
let s = Mangled.to_string pv.pv_name in
match String.rsplit2 s ~on:'.' with
| Some (s1, s2) -> (
match String.rsplit2 s1 ~on:'.' with Some (_, s4) -> s4 ^ "." ^ s2 | _ -> s )
match String.rsplit2 s1 ~on:'.' with Some (_, s4) -> Printf.sprintf "%s.%s" s4 s2 | _ -> s )
| _ ->
s

@ -20,9 +20,11 @@ let none file = {line= -1; col= -1; file}
let dummy = none (SourceFile.invalid __FILE__)
let pp_line f loc = F.fprintf f "line %d" loc.line
(** Pretty print a location *)
let pp f (loc : t) =
F.fprintf f "line %d" loc.line ;
pp_line f loc ;
if loc.col <> -1 then F.fprintf f ", column %d" loc.col

@ -25,6 +25,9 @@ val dummy : t
val pp : Format.formatter -> t -> unit
(** Pretty print a location. *)
val pp_line : Format.formatter -> t -> unit
(** print just the line information *)
val to_string : t -> string
(** String representation of a location. *)

@ -44,15 +44,17 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc
astate =
(* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *)
let crumb = PulseTrace.Assignment {lhs= lhs_access; location= loc} in
match rhs_exp with
| AccessExpression rhs_access -> (
PulseDomain.read loc rhs_access astate
>>= fun (astate, rhs_value) ->
PulseDomain.write loc lhs_access rhs_value astate
>>= fun (astate, (rhs_addr, rhs_trace)) ->
let return_addr_trace = (rhs_addr, crumb :: rhs_trace) in
PulseDomain.write loc lhs_access return_addr_trace astate
>>= fun astate ->
match lhs_access with
| Base (var, _) when Var.is_return var ->
PulseDomain.check_address_of_local_variable summary.Summary.proc_desc rhs_value astate
PulseDomain.check_address_of_local_variable summary.Summary.proc_desc rhs_addr astate
| _ ->
Ok astate )
| Closure (pname, captured) ->
@ -61,7 +63,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
exec_assign summary lhs_access e loc astate
| _ ->
PulseDomain.read_all loc (HilExp.get_access_exprs rhs_exp) astate
>>= PulseDomain.havoc loc lhs_access
>>= PulseDomain.havoc [crumb] loc lhs_access
let exec_call summary _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc
@ -69,6 +71,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
let read_all args astate =
PulseDomain.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate
in
let crumb = PulseTrace.Call {f= `HilCall call; actuals; location= call_loc} in
match call with
| Direct callee_pname when is_destructor callee_pname -> (
match actuals with
@ -86,7 +89,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
match actuals with
| AccessExpression constructor_access :: rest ->
let constructed_object = HilExp.AccessExpression.dereference constructor_access in
PulseDomain.havoc call_loc constructed_object astate >>= read_all rest
PulseDomain.havoc [crumb] call_loc constructed_object astate >>= read_all rest
| _ ->
Ok astate )
| Direct (Typ.Procname.ObjC_Cpp callee_pname)
@ -101,7 +104,7 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
| [AccessExpression lhs; HilExp.AccessExpression rhs] ->
let lhs_deref = HilExp.AccessExpression.dereference lhs in
let rhs_deref = HilExp.AccessExpression.dereference rhs in
PulseDomain.havoc call_loc lhs_deref astate
PulseDomain.havoc [crumb] call_loc lhs_deref astate
>>= fun astate -> PulseDomain.read call_loc rhs_deref astate >>| fst
| _ ->
read_all actuals astate )
@ -122,7 +125,9 @@ module PulseTransferFunctions (CFG : ProcCfg.S) = struct
match model with
| None ->
exec_call summary ret call actuals flags call_loc astate
>>| PulseDomain.havoc_var (fst ret)
>>| PulseDomain.havoc_var
[PulseTrace.Call {f= `HilCall call; actuals; location= call_loc}]
(fst ret)
| Some model ->
model call_loc ~ret ~actuals astate

@ -41,6 +41,15 @@ end
(* {3 Heap domain } *)
module AddrTracePair = struct
type t = AbstractAddress.t * PulseTrace.t [@@deriving compare]
let pp f addr_trace =
if Config.debug_level_analysis >= 3 then
Pp.pair ~fst:AbstractAddress.pp ~snd:PulseTrace.pp f addr_trace
else AbstractAddress.pp f (fst addr_trace)
end
module Attribute = struct
(* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more
efficient (only need to look at the first element in the set of attributes to know if an
@ -48,25 +57,18 @@ module Attribute = struct
type t =
(* DO NOT MOVE, see toplevel comment *)
| Invalid of Invalidation.t
| AddressOfCppTemporary of Var.t
| Closure of
Typ.Procname.t
* (AccessPath.base * HilExp.AccessExpression.t * AbstractAddress.t) list
* Location.t
| AddressOfCppTemporary of Var.t * Location.t option
| Closure of Typ.Procname.t * AddrTracePair.t list
| StdVectorReserve
[@@deriving compare]
let pp f = function
| Invalid invalidation ->
Invalidation.pp f invalidation
| AddressOfCppTemporary var ->
F.fprintf f "&%a" Var.pp var
| Closure (pname, captured, location) ->
F.fprintf f "%a[%a] (%a)" Typ.Procname.pp pname
(Pp.seq ~sep:","
(Pp.triple ~fst:AccessPath.pp_base ~snd:HilExp.AccessExpression.pp
~trd:AbstractAddress.pp))
captured Location.pp location
| AddressOfCppTemporary (var, location_opt) ->
F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt
| Closure (pname, captured) ->
F.fprintf f "%a[%a]" Typ.Procname.pp pname (Pp.seq ~sep:"," AddrTracePair.pp) captured
| StdVectorReserve ->
F.pp_print_string f "std::vector::reserve()"
end
@ -79,7 +81,7 @@ module Memory : sig
module Edges : PrettyPrintable.PPMap with type key = Access.t
type edges = AbstractAddress.t Edges.t
type edges = AddrTracePair.t Edges.t
type cell = edges * Attributes.t
@ -95,11 +97,11 @@ module Memory : sig
val pp : F.formatter -> t -> unit
val add_edge : AbstractAddress.t -> Access.t -> AbstractAddress.t -> t -> t
val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AbstractAddress.t -> t -> t
val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AbstractAddress.t option
val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option
val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
@ -120,7 +122,7 @@ end = struct
module Edges = PrettyPrintable.MakePPMap (Access)
type edges = AbstractAddress.t Edges.t [@@deriving compare]
type edges = AddrTracePair.t Edges.t [@@deriving compare]
type cell = edges * Attributes.t [@@deriving compare]
@ -129,33 +131,33 @@ end = struct
type t = cell Graph.t [@@deriving compare]
let pp =
Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AbstractAddress.pp) ~snd:Attributes.pp)
Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AddrTracePair.pp) ~snd:Attributes.pp)
(* {3 Helper functions to traverse the two maps at once } *)
let add_edge addr_src access addr_end memory =
let add_edge addr_src access value memory =
let edges, attrs =
match Graph.find_opt addr_src memory with
| Some edges_attrs ->
edges_attrs
| Some cell ->
cell
| None ->
(Edges.empty, Attributes.empty)
in
Graph.add addr_src (Edges.add access addr_end edges, attrs) memory
Graph.add addr_src (Edges.add access value edges, attrs) memory
(** [Dereference] edges induce a [TakeAddress] back edge and vice-versa, because
[*(&x) = &( *x ) = x]. *)
let add_edge_and_back_edge addr_src (access : Access.t) addr_end memory =
let memory = add_edge addr_src access addr_end memory in
let add_edge_and_back_edge addr_src (access : Access.t) addr_trace_dst memory =
let memory = add_edge addr_src access addr_trace_dst memory in
match access with
| ArrayAccess _ | FieldAccess _ ->
memory
| TakeAddress ->
add_edge addr_end Dereference addr_src memory
add_edge (fst addr_trace_dst) Dereference (addr_src, []) memory
| Dereference ->
add_edge addr_end TakeAddress addr_src memory
add_edge (fst addr_trace_dst) TakeAddress (addr_src, []) memory
let find_edge_opt addr access memory =
@ -217,7 +219,7 @@ end = struct
let fold = Graph.fold
end
(** Stacks: map addresses of variables to values.
(** Stacks: map addresses of variables to values and initialisation location.
This is defined as an abstract domain but the domain operations are mostly meaningless on their
own. It so happens that the join on abstract states uses the join of stacks provided by this
@ -238,15 +240,15 @@ module Stack = struct
end
module ValueDomain = struct
type t = AbstractAddress.t
type t = AbstractAddress.t * Location.t option [@@deriving compare]
let ( <= ) ~lhs ~rhs = AbstractAddress.equal lhs rhs
let join ((addr1, _) as v1) ((addr2, _) as v2) = if addr1 <= addr2 then v1 else v2
let join l1 l2 = min l1 l2
let ( <= ) ~lhs:(lhs_addr, _) ~rhs:(rhs_addr, _) = AbstractAddress.equal lhs_addr rhs_addr
let widen ~prev ~next ~num_iters:_ = join prev next
let pp = AbstractAddress.pp
let pp = Pp.pair ~fst:AbstractAddress.pp ~snd:(Pp.option Location.pp)
end
include AbstractDomain.Map (VarAddress) (ValueDomain)
@ -258,7 +260,7 @@ module Stack = struct
PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
let compare = compare AbstractAddress.compare
let compare = compare ValueDomain.compare
end
(** the domain *)
@ -284,11 +286,11 @@ module Domain : AbstractDomain.S with type t = astate = struct
(Option.map ~f:fst cell, Option.value_map ~default:Attributes.empty ~f:snd cell)
in
Memory.Edges.for_all
(fun access_lhs addr_dst ->
(fun access_lhs (addr_dst, _) ->
Option.bind edges_rhs_opt ~f:(fun edges_rhs ->
Memory.Edges.find_opt access_lhs edges_rhs )
|> Option.map ~f:(AbstractAddress.equal addr_dst)
|> Option.value ~default:false )
|> Option.exists ~f:(fun (addr_dst_rhs, _) ->
AbstractAddress.equal addr_dst_rhs addr_dst ) )
edges_lhs
&& Attributes.( <= ) ~lhs:attrs_lhs ~rhs:attrs_rhs )
lhs.heap
@ -318,22 +320,23 @@ module Domain : AbstractDomain.S with type t = astate = struct
type nonrec t = {subst: AddressUF.t; astate: t}
(** adds [(src_addr, access, dst_addr)] to [union_heap] and record potential new equality that
(** adds [(src_addr, access, value)] to [union_heap] and record potential new equality that
results from it in [subst] *)
let union_one_edge subst src_addr access dst_addr union_heap =
let union_one_edge subst src_addr access value union_heap =
let dst_addr, _ = value in
let src_addr = to_canonical_address subst src_addr in
let dst_addr = to_canonical_address subst dst_addr in
match (Memory.find_edge_opt src_addr access union_heap, (access : Memory.Access.t)) with
| Some dst_addr', _ when AbstractAddress.equal dst_addr dst_addr' ->
| Some (dst_addr', _), _ when AbstractAddress.equal dst_addr dst_addr' ->
(* same edge *)
(union_heap, `No_new_equality)
| _, ArrayAccess _ ->
(* do not trust array accesses for now, replace the destination of the edge by a fresh location *)
( Memory.add_edge src_addr access (AbstractAddress.mk_fresh ()) union_heap
( Memory.add_edge src_addr access (AbstractAddress.mk_fresh (), []) union_heap
, `No_new_equality )
| None, _ ->
(Memory.add_edge src_addr access dst_addr union_heap, `No_new_equality)
| Some dst_addr', _ ->
(Memory.add_edge src_addr access value union_heap, `No_new_equality)
| Some (dst_addr', _), _ ->
(* new equality [dst_addr = dst_addr'] found *)
ignore (AddressUF.union subst dst_addr dst_addr') ;
(union_heap, `New_equality)
@ -345,10 +348,10 @@ module Domain : AbstractDomain.S with type t = astate = struct
if Addresses.mem addr visited then (visited, union_heap)
else
let visited = Addresses.add addr visited in
let visit_edge access addr_dst (visited, union_heap) =
union_one_edge subst addr access addr_dst union_heap
let visit_edge access value (visited, union_heap) =
union_one_edge subst addr access value union_heap
|> fst
|> visit_address subst visited heap addr_dst
|> visit_address subst visited heap (fst value)
in
Memory.find_opt addr heap
|> Option.fold ~init:(visited, union_heap) ~f:(fun (visited, union_heap) (edges, attrs) ->
@ -361,7 +364,8 @@ module Domain : AbstractDomain.S with type t = astate = struct
let visited = Addresses.empty in
let _, union_heap =
Stack.fold
(fun _var addr (visited, union_heap) -> visit_address subst visited heap addr union_heap)
(fun _var (addr, _) (visited, union_heap) ->
visit_address subst visited heap addr union_heap )
stack (visited, union_heap)
in
union_heap
@ -374,7 +378,7 @@ module Domain : AbstractDomain.S with type t = astate = struct
Stack.merge
(fun _var addr1_opt addr2_opt ->
Option.both addr1_opt addr2_opt
|> Option.iter ~f:(fun (addr1, addr2) ->
|> Option.iter ~f:(fun ((addr1, _), (addr2, _)) ->
(* stack1 says [_var = addr1] and stack2 says [_var = addr2]: unify the
addresses since they are equal to the same variable *)
ignore (AddressUF.union subst addr1 addr2) ) ;
@ -420,7 +424,11 @@ module Domain : AbstractDomain.S with type t = astate = struct
AddressUnionSet.pp set )
in
L.d_printfln "Join unified addresses:@\n@[<v2> %a@]" pp_union_find_classes state.subst ;
let stack = Stack.map (to_canonical_address state.subst) state.astate.stack in
let stack =
Stack.map
(fun (addr, loc) -> (to_canonical_address state.subst addr, loc))
state.astate.stack
in
{heap; stack} )
else normalize {state with astate= {state.astate with heap}}
end
@ -487,30 +495,12 @@ end
type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare]
type allocator =
| Unknown
| Closure of
{ lambda: HilExp.AccessExpression.t (** some way to refer to the closure *)
; access_expr: HilExp.AccessExpression.t (** the access expr that was captured *)
; as_base: AccessPath.base (** the variable it was captured as *)
; location: Location.t }
let pp_allocator f = function
| Unknown ->
()
| Closure {lambda; access_expr; as_base} ->
F.fprintf f "`%a` captured by `%a` as `%a` " HilExp.AccessExpression.pp access_expr
HilExp.AccessExpression.pp lambda AccessPath.pp_base as_base
let location_of_allocator = function Unknown -> None | Closure {location} -> Some location
module Diagnostic = struct
type t =
| AccessToInvalidAddress of
{ allocated_by: allocator
; invalidated_by: Invalidation.t
{ invalidated_by: Invalidation.t
; accessed_by: actor
; trace: PulseTrace.t
; address: AbstractAddress.t }
| StackVariableAddressEscape of {variable: Var.t; location: Location.t}
@ -520,13 +510,13 @@ module Diagnostic = struct
let get_message = function
| AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by; address} ->
| AccessToInvalidAddress {accessed_by; invalidated_by; address; trace} ->
let pp_debug_address f =
if Config.debug_mode then F.fprintf f " (debug: %a)" AbstractAddress.pp address
in
F.asprintf "`%a` accesses address %a%a past its lifetime%t" HilExp.AccessExpression.pp
accessed_by.access_expr pp_allocator allocated_by Invalidation.pp invalidated_by
pp_debug_address
accessed_by.access_expr PulseTrace.pp_interesting_events trace Invalidation.pp
invalidated_by pp_debug_address
| StackVariableAddressEscape {variable} ->
let pp_var f var =
if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary"
@ -536,16 +526,7 @@ module Diagnostic = struct
let get_trace = function
| AccessToInvalidAddress {allocated_by; accessed_by; invalidated_by} ->
let allocated_by_trace =
match location_of_allocator allocated_by with
| None ->
[]
| Some location ->
[ Errlog.make_trace_element 0 location
(F.asprintf "%ahere" pp_allocator allocated_by)
[] ]
in
| AccessToInvalidAddress {accessed_by; invalidated_by; trace} ->
let invalidated_by_trace =
Invalidation.get_location invalidated_by
|> Option.map ~f:(fun location ->
@ -554,7 +535,8 @@ module Diagnostic = struct
[] )
|> Option.to_list
in
allocated_by_trace @ invalidated_by_trace
PulseTrace.make_errlog_trace ~depth:0 trace
@ invalidated_by_trace
@ [ Errlog.make_trace_element 0 accessed_by.location
(F.asprintf "accessed `%a` here" HilExp.AccessExpression.pp accessed_by.access_expr)
[] ]
@ -576,12 +558,11 @@ module Operations = struct
open Result.Monad_infix
(** Check that the address is not known to be invalid *)
let check_addr_access ?(allocated_by = Unknown) actor address astate =
let check_addr_access actor (address, trace) astate =
match Memory.get_invalidation address astate.heap with
| Some invalidated_by ->
Error
(Diagnostic.AccessToInvalidAddress
{invalidated_by; accessed_by= actor; address; allocated_by})
(Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; address; trace})
| None ->
Ok astate
@ -590,52 +571,55 @@ module Operations = struct
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
address reached is valid. *)
let rec walk ~dereference_to_ignore actor ~on_last addr path astate =
let check_addr_access_optional actor addr astate =
let rec walk ~dereference_to_ignore actor ~on_last addr_trace path astate =
let check_addr_access_optional actor addr_trace astate =
match dereference_to_ignore with
| Some 0 ->
Ok astate
| _ ->
check_addr_access actor addr astate
check_addr_access actor addr_trace astate
in
match (path, on_last) with
| [], `Access ->
Ok (astate, addr)
Ok (astate, addr_trace)
| [], `Overwrite _ ->
L.die InternalError "Cannot overwrite last address in empty path"
| [a], `Overwrite new_addr ->
check_addr_access_optional actor addr astate
| [a], `Overwrite new_addr_trace ->
check_addr_access_optional actor addr_trace astate
>>| fun astate ->
let heap = Memory.add_edge_and_back_edge addr a new_addr astate.heap in
({astate with heap}, new_addr)
let heap = Memory.add_edge_and_back_edge (fst addr_trace) a new_addr_trace astate.heap in
({astate with heap}, new_addr_trace)
| a :: path, _ -> (
check_addr_access_optional actor addr astate
check_addr_access_optional actor addr_trace astate
>>= fun astate ->
let dereference_to_ignore =
Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore
in
let addr = fst addr_trace in
match Memory.find_edge_opt addr a astate.heap with
| None ->
let addr' = AbstractAddress.mk_fresh () in
let heap = Memory.add_edge_and_back_edge addr a addr' astate.heap in
let addr_trace' = (AbstractAddress.mk_fresh (), []) in
let heap = Memory.add_edge_and_back_edge addr a addr_trace' astate.heap in
let astate = {astate with heap} in
walk ~dereference_to_ignore actor ~on_last addr' path astate
| Some addr' ->
walk ~dereference_to_ignore actor ~on_last addr' path astate )
walk ~dereference_to_ignore actor ~on_last addr_trace' path astate
| Some addr_trace' ->
walk ~dereference_to_ignore actor ~on_last addr_trace' path astate )
let write_var var new_addr astate =
let write_var var new_addr_trace astate =
let astate, var_address_of =
match Stack.find_opt var astate.stack with
| Some addr ->
| Some (addr, _) ->
(astate, addr)
| None ->
let addr = AbstractAddress.mk_fresh () in
let stack = Stack.add var addr astate.stack in
let stack = Stack.add var (addr, None) astate.stack in
({astate with stack}, addr)
in
(* Update heap with var_address_of -*-> new_addr *)
let heap = Memory.add_edge var_address_of HilExp.Access.Dereference new_addr astate.heap in
let heap =
Memory.add_edge var_address_of HilExp.Access.Dereference new_addr_trace astate.heap
in
{astate with heap}
@ -672,7 +656,7 @@ module Operations = struct
with Failed_fold diag -> Error diag
(** add addresses to the state to give a address to the destination of the given access path *)
(** add addresses to the state to give an address to the destination of the given access path *)
and walk_access_expr ~on_last astate access_expr location =
to_accesses location access_expr astate
>>= fun (astate, (access_var, _), access_list) ->
@ -684,24 +668,28 @@ module Operations = struct
(Pp.seq ~sep:"," Memory.Access.pp)
access_list ;
match (on_last, access_list) with
| `Overwrite new_addr, [] ->
Ok (write_var access_var new_addr astate, new_addr)
| `Overwrite new_addr_trace, [] ->
Ok (write_var access_var new_addr_trace astate, new_addr_trace)
| `Access, _ | `Overwrite _, _ :: _ -> (
let astate, base_addr =
let astate, base_addr_trace =
match Stack.find_opt access_var astate.stack with
| Some addr ->
(astate, addr)
| Some (addr, init_loc_opt) ->
let trace =
Option.value_map init_loc_opt ~default:[] ~f:(fun init_loc ->
[PulseTrace.VariableDeclaration init_loc] )
in
(astate, (addr, trace))
| None ->
let addr = AbstractAddress.mk_fresh () in
let stack = Stack.add access_var addr astate.stack in
({astate with stack}, addr)
let stack = Stack.add access_var (addr, None) astate.stack in
({astate with stack}, (addr, []))
in
match access_list with
| [HilExp.Access.TakeAddress] ->
Ok (astate, base_addr)
Ok (astate, base_addr_trace)
| _ ->
let actor = {access_expr; location} in
walk ~dereference_to_ignore actor ~on_last base_addr
walk ~dereference_to_ignore actor ~on_last base_addr_trace
(HilExp.Access.Dereference :: access_list)
astate )
@ -715,9 +703,9 @@ module Operations = struct
and read location access_expr astate =
materialize_address astate access_expr location
>>= fun (astate, addr) ->
>>= fun (astate, addr_trace) ->
let actor = {access_expr; location} in
check_addr_access actor addr astate >>| fun astate -> (astate, addr)
check_addr_access actor addr_trace astate >>| fun astate -> (astate, addr_trace)
and read_all location access_exprs astate =
@ -728,7 +716,7 @@ module Operations = struct
and eval_hil_exp location (hil_exp : HilExp.t) astate =
match hil_exp with
| AccessExpression access_expr ->
read location access_expr astate
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 ())
@ -739,8 +727,8 @@ module Operations = struct
address.
Return an error state if it traverses some known invalid address. *)
let overwrite_address astate access_expr new_addr =
walk_access_expr ~on_last:(`Overwrite new_addr) astate access_expr
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. *)
@ -748,10 +736,10 @@ module Operations = struct
{astate with heap= Memory.invalidate address actor astate.heap}
let havoc_var var astate = write_var var (AbstractAddress.mk_fresh ()) astate
let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate
let havoc location (access_expr : HilExp.AccessExpression.t) astate =
overwrite_address astate access_expr (AbstractAddress.mk_fresh ()) location >>| fst
let havoc trace location (access_expr : HilExp.AccessExpression.t) astate =
overwrite_address astate access_expr (AbstractAddress.mk_fresh (), trace) location >>| fst
let write location access_expr addr astate =
@ -760,21 +748,22 @@ module Operations = struct
let invalidate cause location access_expr astate =
materialize_address astate access_expr location
>>= fun (astate, addr) ->
check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr
>>= fun (astate, addr_trace) ->
check_addr_access {access_expr; location} addr_trace astate
>>| mark_invalid cause (fst addr_trace)
let invalidate_array_elements cause location access_expr astate =
materialize_address astate access_expr location
>>= fun (astate, addr) ->
check_addr_access {access_expr; location} addr astate
>>= fun (astate, addr_trace) ->
check_addr_access {access_expr; location} addr_trace astate
>>| fun astate ->
match Memory.find_opt addr astate.heap with
match Memory.find_opt (fst addr_trace) astate.heap with
| None ->
astate
| Some (edges, _) ->
Memory.Edges.fold
(fun access dest_addr astate ->
(fun access (dest_addr, _) astate ->
match (access : Memory.Access.t) with
| ArrayAccess _ ->
mark_invalid cause dest_addr astate
@ -792,62 +781,74 @@ module Operations = struct
Container.fold_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
attrs ~init:() ~f:(fun () attr ->
match attr with
| Attribute.AddressOfCppTemporary variable ->
Error
(Diagnostic.StackVariableAddressEscape {variable; location= proc_location})
| Attribute.AddressOfCppTemporary (variable, location_opt) ->
let location = Option.value ~default:proc_location location_opt in
Error (Diagnostic.StackVariableAddressEscape {variable; location})
| _ ->
Ok () ) )
in
let check_address_of_stack_variable () =
Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold)
astate.stack ~init:() ~f:(fun () (variable, var_address) ->
astate.stack ~init:() ~f:(fun () (variable, (var_address, init_location)) ->
if
AbstractAddress.equal var_address address
&& ( Var.is_cpp_temporary variable
|| Var.is_local_to_procedure proc_name variable
&& not (Procdesc.is_captured_var proc_desc variable) )
then Error (Diagnostic.StackVariableAddressEscape {variable; location= proc_location})
then
let location = Option.value ~default:proc_location init_location in
Error (Diagnostic.StackVariableAddressEscape {variable; location})
else Ok () )
in
check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate
let mark_address_of_cpp_temporary variable address heap =
Memory.add_attributes address (Attributes.singleton (AddressOfCppTemporary variable)) heap
let mark_address_of_cpp_temporary location variable address heap =
Memory.add_attributes address
(Attributes.singleton (AddressOfCppTemporary (variable, location)))
heap
let remove_vars vars astate =
let heap =
List.fold vars ~init:astate.heap ~f:(fun heap var ->
match Stack.find_opt var astate.stack with
| Some address when Var.is_cpp_temporary var ->
| Some (address, location) when Var.is_cpp_temporary var ->
(* TODO: it would be good to record the location of the temporary creation in the
stack and save it here in the attribute for reporting *)
mark_address_of_cpp_temporary var address heap
mark_address_of_cpp_temporary location var address heap
| _ ->
heap )
in
let stack = List.fold ~f:(fun stack var -> Stack.remove var stack) ~init:astate.stack vars in
if phys_equal stack astate.stack && phys_equal heap astate.heap then astate else {stack; heap}
let record_var_decl_location location var astate =
let addr =
match Stack.find_opt var astate.stack with
| Some (addr, _) ->
addr
| None ->
AbstractAddress.mk_fresh ()
in
let stack = Stack.add var (addr, Some location) astate.stack in
{astate with stack}
end
module Closures = struct
open Result.Monad_infix
let check_captured_addresses location lambda address astate =
match Memory.find_opt address astate.heap with
let check_captured_addresses location lambda addr astate =
match Memory.find_opt addr astate.heap with
| None ->
Ok astate
| Some (_, attributes) ->
IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
attributes ~f:(function
| Attribute.Closure (_, captured, lambda_location) ->
IContainer.iter_result ~fold:List.fold captured
~f:(fun (base, access_expr, address) ->
Operations.check_addr_access
~allocated_by:
(Closure {lambda; access_expr; as_base= base; location= lambda_location})
{access_expr= lambda; location} address astate
| Attribute.Closure (_, captured) ->
IContainer.iter_result ~fold:List.fold captured ~f:(fun addr_trace ->
Operations.check_addr_access {access_expr= lambda; location} addr_trace astate
>>| fun _ -> () )
| _ ->
Ok () )
@ -856,23 +857,28 @@ module Closures = struct
let write location access_expr pname captured astate =
let closure_addr = AbstractAddress.mk_fresh () in
Operations.write location access_expr closure_addr astate
Operations.write location access_expr
(closure_addr, [PulseTrace.Assignment {lhs= access_expr; location}])
astate
>>| fun astate ->
{ astate with
heap=
Memory.add_attributes closure_addr
(Attributes.singleton (Closure (pname, captured, location)))
(Attributes.singleton (Closure (pname, captured)))
astate.heap }
let record location access_expr pname captured astate =
List.fold_result captured ~init:(astate, [])
~f:(fun ((astate, captured) as result) (captured_base, captured_exp) ->
~f:(fun ((astate, captured) as result) (captured_as, captured_exp) ->
match captured_exp with
| HilExp.AccessExpression (AddressOf access_expr) ->
| HilExp.AccessExpression (AddressOf access_expr as captured_access_expr) ->
Operations.read location access_expr astate
>>= fun (astate, address) ->
Ok (astate, (captured_base, access_expr, address) :: captured)
>>= fun (astate, (address, trace)) ->
let new_trace =
PulseTrace.Capture {captured_as; captured= captured_access_expr; location} :: trace
in
Ok (astate, (address, new_trace) :: captured)
| _ ->
Ok result )
>>= fun (astate, captured_addresses) ->
@ -884,12 +890,12 @@ module StdVector = struct
let is_reserved location vector_access_expr astate =
Operations.read location vector_access_expr astate
>>| fun (astate, addr) -> (astate, Memory.is_std_vector_reserved addr astate.heap)
>>| fun (astate, (addr, _)) -> (astate, Memory.is_std_vector_reserved addr astate.heap)
let mark_reserved location vector_access_expr astate =
Operations.read location vector_access_expr astate
>>| fun (astate, addr) -> {astate with heap= Memory.std_vector_reserve addr astate.heap}
>>| fun (astate, (addr, _)) -> {astate with heap= Memory.std_vector_reserve addr astate.heap}
end
include Domain

@ -54,17 +54,26 @@ module StdVector : sig
val mark_reserved : Location.t -> HilExp.AccessExpression.t -> t -> t access_result
end
val read : Location.t -> HilExp.AccessExpression.t -> t -> (t * AbstractAddress.t) access_result
val read :
Location.t
-> HilExp.AccessExpression.t
-> t
-> (t * (AbstractAddress.t * PulseTrace.t)) access_result
val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result
val havoc_var : Var.t -> t -> t
val havoc_var : PulseTrace.t -> Var.t -> t -> t
val havoc : Location.t -> HilExp.AccessExpression.t -> t -> t access_result
val havoc : PulseTrace.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
val write_var : Var.t -> AbstractAddress.t -> t -> t
val write_var : Var.t -> AbstractAddress.t * PulseTrace.t -> t -> t
val write : Location.t -> HilExp.AccessExpression.t -> AbstractAddress.t -> t -> t access_result
val write :
Location.t
-> HilExp.AccessExpression.t
-> AbstractAddress.t * PulseTrace.t
-> t
-> t access_result
val invalidate :
PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
@ -72,6 +81,9 @@ val invalidate :
val invalidate_array_elements :
PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
val record_var_decl_location : Location.t -> Var.t -> t -> t
val remove_vars : Var.t list -> t -> t
(* TODO: better name and pass location to report where we returned *)
val check_address_of_local_variable : Procdesc.t -> AbstractAddress.t -> t -> t access_result

@ -18,7 +18,7 @@ type std_vector_function =
| ShrinkToFit
[@@deriving compare]
let std_vector_function_pp f = function
let pp_std_vector_function f = function
| Assign ->
F.fprintf f "std::vector::assign"
| Clear ->
@ -71,15 +71,15 @@ let get_location = function
let pp f = function
| CFree (access_expr, location) ->
F.fprintf f "invalidated by call to `free(%a)` at %a" HilExp.AccessExpression.pp access_expr
Location.pp location
Location.pp_line location
| CppDelete (access_expr, location) ->
F.fprintf f "invalidated by call to `delete %a` at %a" HilExp.AccessExpression.pp access_expr
Location.pp location
Location.pp_line location
| CppDestructor (proc_name, access_expr, location) ->
F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name
HilExp.AccessExpression.pp access_expr Location.pp location
HilExp.AccessExpression.pp access_expr Location.pp_line location
| Nullptr ->
F.fprintf f "null pointer"
| StdVector (std_vector_f, access_expr, location) ->
F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" std_vector_function_pp
std_vector_f HilExp.AccessExpression.pp access_expr Location.pp location
F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" pp_std_vector_function
std_vector_f HilExp.AccessExpression.pp access_expr Location.pp_line location

@ -17,6 +17,8 @@ type std_vector_function =
| ShrinkToFit
[@@deriving compare]
val pp_std_vector_function : Format.formatter -> std_vector_function -> unit
type t =
| CFree of HilExp.AccessExpression.t * Location.t
| CppDelete of HilExp.AccessExpression.t * Location.t

@ -34,8 +34,10 @@ module C = struct
let variable_initialization : model =
fun location ~ret:_ ~actuals astate ->
match actuals with
| [AccessExpression (AddressOf access_expr)] ->
PulseDomain.havoc location access_expr astate
| [AccessExpression (AddressOf (Base (var, _)))] ->
PulseDomain.havoc_var [PulseTrace.VariableDeclaration location] var astate
|> PulseDomain.record_var_decl_location location var
|> Result.return
| _ ->
L.die InternalError
"The frontend is not supposed to produce __variable_initialization(e) where e is not of \
@ -65,10 +67,10 @@ module Cplusplus = struct
| AccessExpression lambda :: _ ->
PulseDomain.read location HilExp.AccessExpression.(dereference lambda) astate
>>= fun (astate, address) ->
PulseDomain.Closures.check_captured_addresses location lambda address astate
PulseDomain.Closures.check_captured_addresses location lambda (fst address) astate
| _ ->
Ok astate )
>>| PulseDomain.havoc_var ret_var
>>| PulseDomain.havoc_var [PulseTrace.Call {f= `Model "<lambda>"; actuals; location}] ret_var
let placement_new : model =
@ -76,15 +78,16 @@ module Cplusplus = struct
let read_all args astate =
PulseDomain.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate
in
let crumb = PulseTrace.Call {f= `Model "<placement new>"; actuals; location} in
match List.rev actuals with
| HilExp.AccessExpression expr :: other_actuals ->
PulseDomain.read location expr astate
>>= fun (astate, address) ->
Ok (PulseDomain.write_var ret_var address astate) >>= read_all other_actuals
>>= fun (astate, (address, trace)) ->
PulseDomain.write_var ret_var (address, crumb :: trace) astate |> read_all other_actuals
| _ :: other_actuals ->
read_all other_actuals astate >>| PulseDomain.havoc_var ret_var
read_all other_actuals astate >>| PulseDomain.havoc_var [crumb] ret_var
| _ ->
Ok (PulseDomain.havoc_var ret_var astate)
Ok (PulseDomain.havoc_var [crumb] ret_var astate)
end
module StdVector = struct
@ -104,42 +107,50 @@ module StdVector = struct
HilExp.AccessExpression.array_offset (deref_internal_array vector) Typ.void index
let reallocate_internal_array vector vector_f location astate =
let reallocate_internal_array trace vector vector_f location astate =
let array_address = to_internal_array vector in
let array = deref_internal_array vector in
let invalidation = PulseInvalidation.StdVector (vector_f, vector, location) in
PulseDomain.invalidate_array_elements invalidation location array astate
>>= PulseDomain.invalidate invalidation location array
>>= PulseDomain.havoc location array_address
>>= PulseDomain.havoc trace location array_address
let invalidate_references invalidation : model =
let invalidate_references vector_f : model =
fun location ~ret:_ ~actuals astate ->
match actuals with
| AccessExpression vector :: _ ->
reallocate_internal_array vector invalidation location astate
let crumb =
PulseTrace.Call
{ f= `Model (Format.asprintf "%a" PulseInvalidation.pp_std_vector_function vector_f)
; actuals
; location }
in
reallocate_internal_array [crumb] vector vector_f location astate
| _ ->
Ok astate
let at : model =
fun location ~ret ~actuals astate ->
let crumb = PulseTrace.Call {f= `Model "std::vector::at"; actuals; location} in
match actuals with
| [AccessExpression vector_access_expr; index_exp] ->
PulseDomain.read location
(element_of_internal_array vector_access_expr (Some index_exp))
astate
>>= fun (astate, loc) ->
PulseDomain.write location (HilExp.AccessExpression.base ret) loc astate
>>= fun (astate, (addr, trace)) ->
PulseDomain.write location (HilExp.AccessExpression.base ret) (addr, crumb :: trace) astate
| _ ->
Ok (PulseDomain.havoc_var (fst ret) astate)
Ok (PulseDomain.havoc_var [crumb] (fst ret) astate)
let reserve : model =
fun location ~ret:_ ~actuals astate ->
match actuals with
| [AccessExpression vector; _value] ->
reallocate_internal_array vector Reserve location astate
let crumb = PulseTrace.Call {f= `Model "std::vector::reserve"; actuals; location} in
reallocate_internal_array [crumb] vector Reserve location astate
>>= PulseDomain.StdVector.mark_reserved location vector
| _ ->
Ok astate
@ -149,6 +160,7 @@ module StdVector = struct
fun location ~ret:_ ~actuals astate ->
match actuals with
| [AccessExpression vector; _value] ->
let crumb = PulseTrace.Call {f= `Model "std::vector::push_back"; actuals; location} in
PulseDomain.StdVector.is_reserved location vector astate
>>= fun (astate, is_reserved) ->
if is_reserved then
@ -157,7 +169,7 @@ module StdVector = struct
Ok astate
else
(* simulate a re-allocation of the underlying array every time an element is added *)
reallocate_internal_array vector PushBack location astate
reallocate_internal_array [crumb] vector PushBack location astate
| _ ->
Ok astate
end

@ -0,0 +1,72 @@
(*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
module F = Format
type breadcrumb =
| VariableDeclaration of Location.t
| Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
| Capture of
{ captured_as: AccessPath.base
; captured: HilExp.AccessExpression.t
; location: Location.t }
| Call of
{ f: [`HilCall of HilInstr.call | `Model of string]
; actuals: HilExp.t list
; location: Location.t }
[@@deriving compare]
let pp_breadcrumb_no_location fmt = function
| VariableDeclaration _ ->
F.fprintf fmt "variable declared"
| Capture {captured_as; captured; location= _} ->
F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured AccessPath.pp_base
captured_as
| Assignment {lhs; location= _} ->
F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs
| Call {f; actuals; location= _} ->
let pp_f fmt = function
| `HilCall call ->
F.fprintf fmt "%a" HilInstr.pp_call call
| `Model model ->
F.pp_print_string fmt model
in
F.fprintf fmt "returned from call to `%a(%a)`" pp_f f (Pp.seq ~sep:"," HilExp.pp) actuals
let location_of_breadcrumb = function
| VariableDeclaration location | Assignment {location} | Capture {location} | Call {location} ->
location
let pp_breadcrumb fmt crumb =
F.fprintf fmt "%a at %a" pp_breadcrumb_no_location crumb Location.pp_line
(location_of_breadcrumb crumb)
let errlog_trace_elem_of_breadcrumb ~depth crumb =
let location = location_of_breadcrumb crumb in
let description = F.asprintf "%a" pp_breadcrumb_no_location crumb in
let tags = [] in
Errlog.make_trace_element depth location description tags
type t = breadcrumb list [@@deriving compare]
let pp f trace = Pp.seq ~print_env:Pp.text_break pp_breadcrumb f trace
let make_errlog_trace ~depth trace = List.rev_map ~f:(errlog_trace_elem_of_breadcrumb ~depth) trace
let pp_last_event f = function
| [] ->
()
| crumb :: _ ->
pp_breadcrumb f crumb ;
(* HACK: needed by the call site *) F.pp_print_string f " "
let pp_interesting_events f trace = pp_last_event f trace

@ -0,0 +1,28 @@
(*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
type breadcrumb =
| VariableDeclaration of Location.t
| Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
| Capture of
{ captured_as: AccessPath.base
; captured: HilExp.AccessExpression.t
; location: Location.t }
| Call of
{ f: [`HilCall of HilInstr.call | `Model of string]
; actuals: HilExp.t list
; location: Location.t }
type t = breadcrumb list [@@deriving compare]
val pp : Format.formatter -> t -> unit
val make_errlog_trace : depth:int -> t -> Errlog.loc_trace
val pp_interesting_events : Format.formatter -> t -> unit

@ -171,5 +171,3 @@ let cli_args fmt args =
let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b
let triple ~fst ~snd ~trd fmt (a, b, c) = F.fprintf fmt "(%a,@,%a@,%a)" fst a snd b trd c

@ -100,11 +100,3 @@ val pair :
-> F.formatter
-> 'a * 'b
-> unit
val triple :
fst:(F.formatter -> 'a -> unit)
-> snd:(F.formatter -> 'b -> unit)
-> trd:(F.formatter -> 'c -> unit)
-> F.formatter
-> 'a * 'b * 'c
-> unit

@ -1,35 +1,35 @@
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58, column 5 here,accessed `*(ptr)` here]
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `ptr` here]
codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 29, column 3 here,accessed `&(f)` here]
codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [`s` captured by `&(f)` as `s` here,invalidated by destructor call `S_~S(s)` at line 20, column 3 here,accessed `&(f)` here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 25, column 5 here,accessed `*(result)` here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here]
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 here,accessed `*(ptr)` here]
codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 here,accessed `ptr` here]
codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$12))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 29 here,accessed `&(f)` here]
codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S_S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S_~S(s)` at line 20 here,accessed `&(f)` here]
codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 25 here,accessed `*(result)` here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(int))`,assigned to `x`,invalidated by call to `delete x` at line 112 here,accessed `x` here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 82, column 5 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 18, column 3 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 50, column 3 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 37, column 3 here,accessed `s->f` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 102, column 3 here,accessed `s->f` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64, column 3 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 148, column 3 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 156, column 3 here,accessed `alias` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 165, column 3 here,accessed `alias` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 71, column 3 here,accessed `*(s.f)` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::C_~C(c)` at line 210, column 3 here,accessed `pc->f` here]
codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15, column 3 here,accessed `x` here]
codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 64, column 5 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 126, column 5 here,accessed `&(this->x)` here]
codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::assign(vec, ..)` at line 83, column 3 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::clear(vec, ..)` at line 77, column 3 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::insert(vec, ..)` at line 95, column 3 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 71, column 3 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 89, column 3 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 57 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 82 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 18 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 50 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 37 here,accessed `s->f` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 24 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 73 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 102 here,accessed `s->f` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S_S(&(s),1)`,invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,invalidated by call to `delete alias` at line 148 here,accessed `s` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [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`,invalidated by call to `delete s` at line 156 here,accessed `alias` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `alias`,invalidated by call to `delete s` at line 165 here,accessed `alias` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S_S(&(s),1)`,invalidated by destructor call `use_after_destructor::S_~S(s)` at line 71 here,accessed `*(s.f)` here]
codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::C_C(&(c),3)`,invalidated by destructor call `use_after_destructor::C_~C(c)` at line 210 here,accessed `pc->f` here]
codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15 here,accessed `x` here]
codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10 here,accessed `*(x)` here]
codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 65 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, VectorA_FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 127 here,accessed `&(this->x)` here]
codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::assign(vec, ..)` at line 84 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::clear(vec, ..)` at line 78 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 20 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 13 here,accessed `*(y)` here]
codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::insert(vec, ..)` at line 96 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 72 here,accessed `*(elt)` here]
codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 90 here,accessed `*(elt)` here]

@ -9,8 +9,9 @@
void deref_vector_element_after_push_back_bad(std::vector<int>& vec) {
int* elt = &vec[1];
int* y = elt;
vec.push_back(42);
std::cout << *elt << "\n";
std::cout << *y << "\n";
}
void deref_local_vector_element_after_push_back_bad() {

Loading…
Cancel
Save