[HIL] Implicit dereference in access expression

Reviewed By: sblackshear

Differential Revision: D7153744

fbshipit-source-id: f439e02
master
Daiva Naudziuniene 7 years ago committed by Facebook Github Bot
parent a0149872ad
commit 4157ba820a

@ -8,32 +8,146 @@
*)
open! IStd
module F = Format
type t =
| Base of AccessPath.base
| Offset of t * AccessPath.access
(* field/array access *)
| FieldOffset of t * Typ.Fieldname.t
| ArrayOffset of t * Typ.t * t list
| AddressOf of t
(* address of operator & *)
| Dereference of t
(* dereference operator * *)
[@@deriving compare]
(** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *)
let rec to_access_path t =
let rec to_access_path_ t =
match t with
| Base base ->
(base, [])
| Offset (ae, acc) ->
AccessPath.append (to_access_path ae) [acc]
| FieldOffset (ae, fld) ->
let base, accesses = to_access_path_ ae in
(base, AccessPath.FieldAccess fld :: accesses)
| ArrayOffset (ae, typ, index_aes) ->
let access_paths = to_access_paths index_aes in
let base, accesses = to_access_path_ ae in
(base, AccessPath.ArrayAccess (typ, access_paths) :: accesses)
| AddressOf ae ->
to_access_path ae
to_access_path_ ae
| Dereference ae ->
to_access_path ae
to_access_path_ ae
in
let base, accesses = to_access_path_ t in
(base, List.rev accesses)
and to_access_paths ts = List.map ~f:to_access_path ts
let rec get_base = function
| Base base ->
base
| FieldOffset (ae, _) | ArrayOffset (ae, _, _) | AddressOf ae | Dereference ae ->
get_base ae
let lookup_field_type_annot tenv base_typ field_name =
let lookup = Tenv.lookup tenv in
Typ.Struct.get_field_type_and_annotation ~lookup field_name base_typ
let of_access_path (base, accesses) =
let rec add_access accesses ae =
match accesses with [] -> ae | access :: rest -> add_access rest (Offset (ae, access))
let rec get_typ t tenv : Typ.t option =
match t with
| Base (_, typ) ->
Some typ
| FieldOffset (ae, fld)
-> (
let base_typ_opt = get_typ ae tenv in
match base_typ_opt with
| Some base_typ ->
Option.map (lookup_field_type_annot tenv base_typ fld) ~f:fst
| None ->
None )
| ArrayOffset (_, typ, _) ->
Some typ
| AddressOf ae ->
let base_typ_opt = get_typ ae tenv in
Option.map base_typ_opt ~f:(fun base_typ -> Typ.mk (Tptr (base_typ, Pk_pointer)))
| Dereference ae ->
let base_typ_opt = get_typ ae tenv in
match base_typ_opt with Some {Typ.desc= Tptr (typ, _)} -> Some typ | _ -> None
let rec pp fmt = function
| Base (pvar, _) ->
Var.pp fmt pvar
| FieldOffset (ae, fld) ->
F.fprintf fmt "%a.%a" pp ae Typ.Fieldname.pp fld
| ArrayOffset (ae, _, []) ->
F.fprintf fmt "%a[_]" pp ae
| ArrayOffset (ae, _, index_aes) ->
F.fprintf fmt "%a[%a]" pp ae (PrettyPrintable.pp_collection ~pp_item:pp) index_aes
| AddressOf ae ->
F.fprintf fmt "&(%a)" pp ae
| Dereference ae ->
F.fprintf fmt "*(%a)" pp ae
let equal = [%compare.equal : t]
let base_of_id id typ = (Var.of_id id, typ)
let base_of_pvar pvar typ = (Var.of_pvar pvar, typ)
let of_pvar pvar typ = Base (base_of_pvar pvar typ)
let of_id id typ = Base (base_of_id id typ)
(* Adapted from AccessPath.of_exp. *)
let of_exp ~include_array_indexes exp0 typ0 ~(f_resolve_id: Var.t -> t option) =
let rec of_exp_ exp typ (add_accesses: t -> t) acc : t list =
match exp with
| Exp.Var id -> (
match f_resolve_id (Var.of_id id) with
| Some access_expr ->
add_accesses access_expr :: acc
| None ->
add_accesses (of_id id typ) :: acc )
| Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> (
match f_resolve_id (Var.of_pvar pvar) with
| Some access_expr ->
add_accesses access_expr :: acc
| None ->
add_accesses (of_pvar pvar typ) :: acc )
| Exp.Lvar pvar ->
add_accesses (of_pvar pvar typ) :: acc
| Exp.Lfield (root_exp, fld, root_exp_typ) ->
let add_field_access_expr access_expr = add_accesses (FieldOffset (access_expr, fld)) in
of_exp_ root_exp root_exp_typ add_field_access_expr acc
| Exp.Lindex (root_exp, index_exp) ->
let index_access_exprs =
if include_array_indexes then of_exp_ index_exp typ Fn.id [] else []
in
let add_array_access_expr access_expr =
add_accesses (ArrayOffset (access_expr, typ, index_access_exprs))
in
add_access accesses (Base base)
let array_typ = Typ.mk_array typ in
of_exp_ root_exp array_typ add_array_access_expr acc
| Exp.Cast (cast_typ, cast_exp) ->
of_exp_ cast_exp cast_typ Fn.id acc
| Exp.UnOp (_, unop_exp, _) ->
of_exp_ unop_exp typ Fn.id acc
| Exp.Exn exn_exp ->
of_exp_ exn_exp typ Fn.id acc
| Exp.BinOp (_, exp1, exp2) ->
of_exp_ exp1 typ Fn.id acc |> of_exp_ exp2 typ Fn.id
| Exp.Const _ | Closure _ | Sizeof _ ->
acc
in
of_exp_ exp0 typ0 Fn.id []
let of_lhs_exp ~include_array_indexes lhs_exp typ ~(f_resolve_id: Var.t -> t option) =
match of_exp ~include_array_indexes lhs_exp typ ~f_resolve_id with
| [lhs_ae] ->
Some lhs_ae
| _ ->
None

@ -11,14 +11,31 @@ open! IStd
type t =
| Base of AccessPath.base
| Offset of t * AccessPath.access
(* field/array access *)
| FieldOffset of t * Typ.Fieldname.t
(* field access *)
| ArrayOffset of t * Typ.t * t list
(* array access *)
| AddressOf of t
(* & *)
(* address of operator & *)
| Dereference of t
(* * *)
(* dereference operator * *)
[@@deriving compare]
val to_access_path : t -> AccessPath.t
val of_access_path : AccessPath.t -> t
val to_access_paths : t list -> AccessPath.t list
val of_id : Ident.t -> Typ.t -> t
(** create an access expression from an ident *)
val get_base : t -> AccessPath.base
val get_typ : t -> Tenv.t -> Typ.t option
val pp : Format.formatter -> t -> unit
val equal : t -> t -> bool
val of_lhs_exp :
include_array_indexes:bool -> Exp.t -> Typ.t -> f_resolve_id:(Var.t -> t option) -> t option
(** convert [lhs_exp] to an access expression, resolving identifiers using [f_resolve_id] *)

@ -24,7 +24,7 @@ type t =
let rec pp fmt = function
| AccessExpression access_expr ->
AccessPath.pp fmt (AccessExpression.to_access_path access_expr)
AccessExpression.pp fmt access_expr
| UnaryOperator (op, e, _) ->
F.fprintf fmt "%s%a" (Unop.str op) pp e
| BinaryOperator (op, e1, e2) ->
@ -53,7 +53,7 @@ let rec pp fmt = function
let rec get_typ tenv = function
| AccessExpression access_expr ->
AccessPath.get_typ (AccessExpression.to_access_path access_expr) tenv
AccessExpression.get_typ access_expr tenv
| UnaryOperator (_, _, typ_opt) ->
typ_opt
| BinaryOperator ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _) ->
@ -92,39 +92,39 @@ let rec get_typ tenv = function
Some (Typ.mk (Typ.Tint Typ.IUInt))
let get_access_paths exp0 =
let rec get_access_paths_ exp acc =
let get_access_exprs exp0 =
let rec get_access_exprs_ exp acc =
match exp with
| AccessExpression ae ->
AccessExpression.to_access_path ae :: acc
ae :: acc
| Cast (_, e) | UnaryOperator (_, e, _) | Exception e | Sizeof (_, Some e) ->
get_access_paths_ e acc
get_access_exprs_ e acc
| BinaryOperator (_, e1, e2) ->
get_access_paths_ e1 acc |> get_access_paths_ e2
get_access_exprs_ e1 acc |> get_access_exprs_ e2
| Closure (_, captured) ->
List.fold captured ~f:(fun acc (_, e) -> get_access_paths_ e acc) ~init:acc
List.fold captured ~f:(fun acc (_, e) -> get_access_exprs_ e acc) ~init:acc
| Constant _ | Sizeof _ ->
acc
in
get_access_paths_ exp0 []
get_access_exprs_ exp0 []
(* convert an SIL expression into an HIL expression. the [f_resolve_id] function should map an SSA
temporary variable to the access path it represents. evaluating the HIL expression should
produce the same result as evaluating the SIL expression and replacing the temporary variables
using [f_resolve_id] *)
let of_sil ~include_array_indexes ~f_resolve_id exp typ =
let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ =
let rec of_sil_ (exp: Exp.t) typ =
match exp with
| Var id ->
let ap =
let ae =
match f_resolve_id (Var.of_id id) with
| Some access_path ->
access_path
| Some access_expr ->
if add_deref then AccessExpression.Dereference access_expr else access_expr
| None ->
AccessPath.of_id id typ
AccessExpression.of_id id typ
in
AccessExpression (AccessExpression.of_access_path ap)
AccessExpression ae
| UnOp (op, e, typ_opt) ->
UnaryOperator (op, of_sil_ e typ, typ_opt)
| BinOp (op, e0, e1) ->
@ -156,9 +156,9 @@ let of_sil ~include_array_indexes ~f_resolve_id exp typ =
in
Closure (closure.name, environment)
| Lfield (root_exp, fld, root_exp_typ) -> (
match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
| Some access_path ->
AccessExpression (AccessExpression.of_access_path access_path)
match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
| Some access_expr ->
AccessExpression access_expr
| None ->
(* unsupported field expression: represent with a dummy variable *)
of_sil_
@ -173,9 +173,9 @@ let of_sil ~include_array_indexes ~f_resolve_id exp typ =
literal, e.g. using `const_cast<char*>` *)
of_sil_ (Exp.Lindex (Var (Ident.create_normal (Ident.string_to_name s) 0), index_exp)) typ
| Lindex (root_exp, index_exp) -> (
match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
| Some access_path ->
AccessExpression (AccessExpression.of_access_path access_path)
match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
| Some access_expr ->
AccessExpression access_expr
| None ->
(* unsupported index expression: represent with a dummy variable *)
of_sil_
@ -183,9 +183,9 @@ let of_sil ~include_array_indexes ~f_resolve_id exp typ =
( Var (Ident.create_normal (Ident.string_to_name (Exp.to_string root_exp)) 0)
, index_exp )) typ )
| Lvar _ ->
match AccessPath.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
| Some access_path ->
AccessExpression (AccessExpression.of_access_path access_path)
match AccessExpression.of_lhs_exp ~include_array_indexes exp typ ~f_resolve_id with
| Some access_expr ->
AccessExpression access_expr
| None ->
L.(die InternalError) "Couldn't convert var expression %a to access path" Exp.pp exp
in

@ -30,10 +30,11 @@ val get_typ : Tenv.t -> t -> Typ.t option
(** Get the type of the expression. Warning: not fully implemented *)
val of_sil :
include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessPath.t option) -> Exp.t -> Typ.t -> t
include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessExpression.t option) -> add_deref:bool
-> Exp.t -> Typ.t -> t
(** Convert SIL expression to HIL expression *)
val get_access_paths : t -> AccessPath.t list
val get_access_exprs : t -> AccessExpression.t list
(** Get all the access paths used in the given HIL expression, including duplicates if a path is
used more than once. *)

@ -11,13 +11,13 @@ open! IStd
module F = Format
module L = Logging
type call = Direct of Typ.Procname.t | Indirect of AccessPath.t [@@deriving compare]
type call = Direct of Typ.Procname.t | Indirect of AccessExpression.t [@@deriving compare]
let pp_call fmt = function
| Direct pname ->
Typ.Procname.pp fmt pname
| Indirect access_path ->
F.fprintf fmt "*%a" AccessPath.pp access_path
| Indirect access_expr ->
F.fprintf fmt "*%a" AccessExpression.pp access_expr
type t =
@ -28,9 +28,7 @@ type t =
let pp fmt = function
| Assign (access_expr, exp, loc) ->
F.fprintf fmt "%a := %a [%a]" AccessPath.pp
(AccessExpression.to_access_path access_expr)
HilExp.pp exp Location.pp loc
F.fprintf fmt "%a := %a [%a]" AccessExpression.pp access_expr HilExp.pp exp Location.pp loc
| Assume (exp, _, _, loc) ->
F.fprintf fmt "assume %a [%a]" HilExp.pp exp Location.pp loc
| Call (ret_opt, call, actuals, _, loc) ->
@ -39,25 +37,31 @@ let pp fmt = function
F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret_opt pp_call call pp_actuals actuals Location.pp loc
type translation = Instr of t | Bind of Var.t * AccessPath.t | Unbind of Var.t list | Ignore
type translation =
| Instr of t
| Bind of Var.t * AccessExpression.t
| Unbind of Var.t list
| Ignore
(* convert an SIL instruction into an HIL instruction. the [f_resolve_id] function should map an SSA
temporary variable to the access path it represents. evaluating the HIL instruction should
produce the same result as evaluating the SIL instruction and replacing the temporary variables
using [f_resolve_id]. *)
let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
let exp_of_sil = HilExp.of_sil ~include_array_indexes ~f_resolve_id in
let analyze_id_assignment lhs_id rhs_exp rhs_typ loc =
let rhs_hil_exp = exp_of_sil rhs_exp rhs_typ in
let exp_of_sil ?(add_deref= false) =
HilExp.of_sil ~include_array_indexes ~f_resolve_id ~add_deref
in
let analyze_id_assignment ?(add_deref= false) lhs_id rhs_exp rhs_typ loc =
let rhs_hil_exp = exp_of_sil ~add_deref rhs_exp rhs_typ in
match rhs_hil_exp with
| AccessExpression rhs_access_expr ->
Bind (lhs_id, AccessExpression.to_access_path rhs_access_expr)
Bind (lhs_id, rhs_access_expr)
| _ ->
Instr (Assign (AccessExpression.Base (lhs_id, rhs_typ), rhs_hil_exp, loc))
in
match instr with
| Load (lhs_id, rhs_exp, rhs_typ, loc) ->
analyze_id_assignment (Var.of_id lhs_id) rhs_exp rhs_typ loc
analyze_id_assignment ~add_deref:true (Var.of_id lhs_id) rhs_exp rhs_typ loc
| Store (Lvar lhs_pvar, lhs_typ, rhs_exp, loc) when Pvar.is_ssa_frontend_tmp lhs_pvar ->
analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc
| Call
@ -70,7 +74,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc
| Store (lhs_exp, typ, rhs_exp, loc) ->
let lhs_access_expr =
match exp_of_sil lhs_exp typ with
match exp_of_sil ~add_deref:true lhs_exp typ with
| AccessExpression access_expr ->
access_expr
| BinaryOperator (_, exp0, exp1) -> (
@ -79,14 +83,14 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
one pointer type represented as an access path. just use that access path and forget
about the arithmetic. if you need to model this more precisely, you should be using
SIL instead *)
HilExp.get_access_paths exp0
HilExp.get_access_exprs exp0
with
| ap :: _ ->
AccessExpression.of_access_path ap
ap
| [] ->
match HilExp.get_access_paths exp1 with
match HilExp.get_access_exprs exp1 with
| ap :: _ ->
AccessExpression.of_access_path ap
ap
| [] ->
L.(die InternalError)
"Invalid pointer arithmetic expression %a used as LHS at %a" Exp.pp lhs_exp
@ -110,7 +114,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr: Sil.instr) =
| Constant Cfun procname | Closure (procname, _) ->
Direct procname
| AccessExpression access_expr ->
Indirect (AccessExpression.to_access_path access_expr)
Indirect access_expr
| call_exp ->
L.(die InternalError) "Unexpected call expression %a" HilExp.pp call_exp
in

@ -11,7 +11,7 @@ open! IStd
module F = Format
(** type of a procedure call; either direct or via function pointer *)
type call = Direct of Typ.Procname.t | Indirect of AccessPath.t [@@deriving compare]
type call = Direct of Typ.Procname.t | Indirect of AccessExpression.t [@@deriving compare]
type t =
| Assign of AccessExpression.t * HilExp.t * Location.t
@ -27,11 +27,11 @@ val pp : F.formatter -> t -> unit
(** Result of translating an SIL instruction *)
type translation =
| Instr of t (** HIL instruction to execute *)
| Bind of Var.t * AccessPath.t (** add binding to identifier map *)
| Bind of Var.t * AccessExpression.t (** add binding to identifier map *)
| Unbind of Var.t list (** remove binding from identifier map *)
| Ignore (** no-op *)
val of_sil :
include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessPath.t option) -> Sil.instr
include_array_indexes:bool -> f_resolve_id:(Var.t -> AccessExpression.t option) -> Sil.instr
-> translation
(** Convert an SIL instruction to an HIL instruction *)

@ -67,13 +67,10 @@ struct
"dump" all of the temporaries out of the id map, then execute the unlock instruction. *)
let actual_state' =
IdAccessPathMapDomain.fold
(fun id access_path astate_acc ->
(fun id access_expr astate_acc ->
let lhs_access_path = AccessExpression.Base (id, Typ.mk Typ.Tvoid) in
let dummy_assign =
HilInstr.Assign
( lhs_access_path
, HilExp.AccessExpression (AccessExpression.of_access_path access_path)
, loc )
HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc)
in
TransferFunctions.exec_instr astate_acc extras node dummy_assign )
id_map actual_state

@ -11,20 +11,20 @@ open! IStd
module IdMap = Var.Map
module L = Logging
type astate = AccessPath.t IdMap.t
type astate = AccessExpression.t IdMap.t
include IdMap
let pp fmt astate = IdMap.pp ~pp_value:AccessPath.pp fmt astate
let pp fmt astate = IdMap.pp ~pp_value:AccessExpression.pp fmt astate
let check_invariant ap1 ap2 = function
| Var.ProgramVar pvar when Pvar.is_ssa_frontend_tmp pvar ->
(* Sawja reuses temporary variables which sometimes breaks this invariant *)
()
| id ->
if not (AccessPath.equal ap1 ap2) then
if not (AccessExpression.equal ap1 ap2) then
L.(die InternalError)
"Id %a maps to both %a and %a" Var.pp id AccessPath.pp ap1 AccessPath.pp ap2
"Id %a maps to both %a and %a" Var.pp id AccessExpression.pp ap1 AccessExpression.pp ap2
let ( <= ) ~lhs ~rhs =

@ -13,7 +13,7 @@ open! IStd
module IdMap = Var.Map
type astate = AccessPath.t IdMap.t
type astate = AccessExpression.t IdMap.t
include module type of IdMap

@ -124,8 +124,9 @@ module Domain = struct
let exp_add_reads exp loc summary astate =
List.fold
~f:(fun acc access_path -> access_path_add_read access_path loc summary acc)
(HilExp.get_access_paths exp) ~init:astate
~f:(fun acc access_expr ->
access_path_add_read (AccessExpression.to_access_path access_expr) loc summary acc )
(HilExp.get_access_exprs exp) ~init:astate
let actuals_add_reads actuals loc summary astate =
@ -144,8 +145,10 @@ module Domain = struct
let borrow_exp lhs_var rhs_exp astate =
let rhs_vars =
List.fold (HilExp.get_access_paths rhs_exp)
~f:(fun acc ((var, _), _) -> VarSet.add var acc)
List.fold (HilExp.get_access_exprs rhs_exp)
~f:(fun acc access_expr ->
let (var, _), _ = AccessExpression.to_access_path access_expr in
VarSet.add var acc )
~init:VarSet.empty
in
borrow_vars lhs_var rhs_vars astate

@ -164,9 +164,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_field_access pre
in
List.fold
~f:(fun acc (base, accesses) ->
~f:(fun acc access_expr ->
let base, accesses = AccessExpression.to_access_path access_expr in
if is_static_access (fst base) then acc else add_field_accesses (base, []) acc accesses )
~init:accesses (HilExp.get_access_paths exp)
~init:accesses (HilExp.get_access_exprs exp)
let is_synchronized_container callee_pname ((_, (base_typ: Typ.t)), accesses) tenv =
@ -584,7 +585,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_access rhs_exp loc ~is_write_access:false astate.accesses astate.locks astate.threads
astate.ownership proc_data
in
let rhs_access_paths = HilExp.get_access_paths rhs_exp in
let rhs_access_paths =
AccessExpression.to_access_paths (HilExp.get_access_exprs rhs_exp)
in
let is_functional =
not (List.is_empty rhs_access_paths)
&& List.for_all
@ -607,10 +610,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
report spurious read/write races *)
rhs_accesses
else
add_access
(AccessExpression (AccessExpression.of_access_path lhs_access_path))
loc ~is_write_access:true rhs_accesses astate.locks astate.threads astate.ownership
proc_data
add_access (AccessExpression lhs_access_expr) loc ~is_write_access:true rhs_accesses
astate.locks astate.threads astate.ownership proc_data
in
let ownership = propagate_ownership lhs_access_path rhs_exp astate.ownership in
let attribute_map = propagate_attributes lhs_access_path rhs_exp astate.attribute_map in
@ -674,9 +675,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate.threads astate.ownership proc_data
in
let astate' =
match HilExp.get_access_paths assume_exp with
| [access_path]
match HilExp.get_access_exprs assume_exp with
| [access_expr]
-> (
let access_path = AccessExpression.to_access_path access_expr in
let choices = AttributeMapDomain.get_choices access_path astate.attribute_map in
match eval_bexp access_path assume_exp with
| Some bool_value ->

@ -466,7 +466,7 @@ module StabilityDomain = struct
let add_wobbly_path_exp exp paths =
let access_paths = HilExp.get_access_paths exp in
let access_paths = AccessExpression.to_access_paths (HilExp.get_access_exprs exp) in
List.fold ~f:(fun acc p -> add_path p acc) access_paths ~init:paths
@ -529,9 +529,9 @@ module StabilityDomain = struct
| Some formal_index -> (
match List.nth actuals formal_index with
| Some actual_exp -> (
match HilExp.get_access_paths actual_exp with
match HilExp.get_access_exprs actual_exp with
| [actual] ->
AccessPath.append actual accesses
AccessPath.append (AccessExpression.to_access_path actual) accesses
| _ ->
path )
| None ->

@ -449,39 +449,46 @@ module Make (TaintSpecification : TaintSpec.S) = struct
(* not all sinks are function calls; we might want to treat an array or field access as a
sink too. do this by pretending an access is a call to a dummy function and using the
existing machinery for adding function call sinks *)
let add_sinks_for_access_path (_, accesses) loc astate =
let add_sinks_for_access astate_acc = function
| AccessPath.FieldAccess _ | AccessPath.ArrayAccess (_, []) ->
let add_sinks_for_access_path access_expr loc astate =
let rec add_sinks_for_access astate_acc = function
| AccessExpression.Base _ ->
astate_acc
| AccessPath.ArrayAccess (_, indexes) ->
| AccessExpression.FieldOffset (ae, _)
| ArrayOffset (ae, _, [])
| Dereference ae
| AddressOf ae ->
add_sinks_for_access astate_acc ae
| AccessExpression.ArrayOffset (ae, _, indexes) ->
let dummy_call_site = CallSite.make BuiltinDecl.__array_access loc in
let dummy_actuals =
List.map
~f:(fun index_ap ->
HilExp.AccessExpression (AccessExpression.of_access_path index_ap) )
indexes
List.map ~f:(fun index_ae -> HilExp.AccessExpression index_ae) indexes
in
let sinks =
TraceDomain.Sink.get dummy_call_site dummy_actuals proc_data.ProcData.tenv
in
let astate_acc_result =
match sinks with
| None ->
astate_acc
| Some sink ->
add_sink sink dummy_actuals astate proc_data dummy_call_site
in
List.fold ~f:add_sinks_for_access ~init:astate accesses
add_sinks_for_access astate_acc_result ae
in
add_sinks_for_access astate access_expr
in
let add_sources_for_access_path (((var, _), _) as ap) loc astate =
let add_sources_for_access_path access_expr loc astate =
let var, _ = AccessExpression.get_base access_expr in
if Var.is_global var then
let dummy_call_site = CallSite.make BuiltinDecl.__global_access loc in
match
TraceDomain.Source.get dummy_call_site
[HilExp.AccessExpression (AccessExpression.of_access_path ap)]
TraceDomain.Source.get dummy_call_site [HilExp.AccessExpression access_expr]
proc_data.tenv
with
| Some {TraceDomain.Source.source} ->
let access_path = AccessPath.Abs.Exact ap in
let access_path =
AccessPath.Abs.Exact (AccessExpression.to_access_path access_expr)
in
let trace, subtree =
Option.value ~default:TaintDomain.empty_node
(TaintDomain.get_node access_path astate)
@ -495,16 +502,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct
let add_sources_sinks_for_exp exp loc astate =
match exp with
| HilExp.AccessExpression access_expr ->
let access_path = AccessExpression.to_access_path access_expr in
add_sinks_for_access_path access_path loc astate
|> add_sources_for_access_path access_path loc
add_sinks_for_access_path access_expr loc astate
|> add_sources_for_access_path access_expr loc
| _ ->
astate
in
let exec_write lhs_access_path rhs_exp astate =
let exec_write lhs_access_expr rhs_exp astate =
let rhs_node =
Option.value (hil_exp_get_node rhs_exp astate proc_data) ~default:TaintDomain.empty_node
in
let lhs_access_path = AccessExpression.to_access_path lhs_access_expr in
TaintDomain.add_node (AccessPath.Abs.Exact lhs_access_path) rhs_node astate
in
match instr with
@ -522,9 +529,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct
`return null` in a void function *)
astate
| Assign (lhs_access_expr, rhs_exp, loc) ->
let lhs_access_path = AccessExpression.to_access_path lhs_access_expr in
add_sources_sinks_for_exp rhs_exp loc astate
|> add_sinks_for_access_path lhs_access_path loc |> exec_write lhs_access_path rhs_exp
|> add_sinks_for_access_path lhs_access_expr loc |> exec_write lhs_access_expr rhs_exp
| Assume (assume_exp, _, _, loc) ->
add_sources_sinks_for_exp assume_exp loc astate
| Call (ret_opt, Direct called_pname, actuals, _, callee_loc) ->
@ -614,18 +620,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct
match (* treat unknown calls to C++ operator= as assignment *)
actuals with
| [(AccessExpression lhs_access_expr); rhs_exp] ->
exec_write (AccessExpression.to_access_path lhs_access_expr) rhs_exp access_tree
exec_write lhs_access_expr rhs_exp access_tree
| [(AccessExpression lhs_access_expr); rhs_exp; (HilExp.AccessExpression access_expr)]
-> (
let dummy_ret_access_path = AccessExpression.to_access_path access_expr in
match dummy_ret_access_path with
| (Var.ProgramVar pvar, _), [] when Pvar.is_frontend_tmp pvar ->
let dummy_ret_access_expr = access_expr in
match dummy_ret_access_expr with
| AccessExpression.Base (Var.ProgramVar pvar, _) when Pvar.is_frontend_tmp pvar ->
(* the frontend translates operator=(x, y) as operator=(x, y, dummy_ret) when
operator= returns a value type *)
exec_write
(AccessExpression.to_access_path lhs_access_expr)
rhs_exp access_tree
|> exec_write dummy_ret_access_path rhs_exp
exec_write lhs_access_expr rhs_exp access_tree
|> exec_write dummy_ret_access_expr rhs_exp
| _ ->
L.internal_error "Unexpected call to operator= %a in %a" HilInstr.pp instr
Typ.Procname.pp callee_pname ;

@ -0,0 +1,71 @@
/*
* Copyright (c) 2018 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
#include <mutex>
namespace dereferencing {
struct B {
int c;
};
struct A {
B b;
};
struct X {
int w;
int u;
X* x1;
X** x2;
A a;
};
class Basic {
public:
Basic() {}
void pointer_deref_race(int* v1) { (*v1)++; } // HIL: *(&v1) := *(&v1) + 1
void pointer_arith_ok(int* v2) { v2++; } // HIL: &v2 := &v2 + 1
void value_ok(int v3) { v3++; } // HIL: &v3 := &v3 + 1
void field_race(int& f) { f++; } // HIL: *(&f) := *(&f) + 1
void mixed_deref_race(X& xparam) {
xparam.x1->w++; // HIL: &xparam.x1.w := &xparam.x1.w + 1
(*xparam.x1).u++; // HIL: &xparam.x1.u := &xparam.x1.u + 1
(**xparam.x2).a.b.c++; // HIL:*(&xparam.x2).a.b.c := *(&xparam.x2).a.b.c + 1
}
void call1() {
pointer_deref_race(&p); // race - FalseNegative
pointer_arith_ok(&q); // no race
value_ok(h); // no race
field_race(g); // race - FalseNegative
mixed_deref_race(x); // race
}
int test_lock() {
mutex_.lock();
call1();
}
int test_unlock() { call1(); }
private:
int g;
int h;
int p;
int q;
X x;
std::mutex mutex_;
};
} // namespace dereferencing

@ -3,6 +3,12 @@ codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get4, 0, LOCK_CONSISTENCY_VIO
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 0, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to basics::Basic_get_private_suspiciously_read,access to `&this.suspiciously_read`,<Write trace>,access to `&this.suspiciously_read`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 0, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,access to `&this.single_lock_suspiciously_read`,<Write trace>,access to `&this.single_lock_suspiciously_read`]
codetoanalyze/cpp/racerd/constructor_ownership.cpp, constructors::TSL_not_locked_race, 0, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `&this.type_`,<Write trace>,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `&this.type_`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 5, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 5, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 5, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 0, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 0, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x2.a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 0, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `&xparam.x1.u`]
codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership_test2_bad, 5, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,access to `&x.f`,<Write trace>,access to `&x.f`]
codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership_test3_bad, 5, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,access to `&x.f`,<Write trace>,access to `&x.f`]
codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard_get2, 3, LOCK_CONSISTENCY_VIOLATION, [<Read trace>,access to `&this.suspiciously_written`,<Write trace>,access to `&this.suspiciously_written`]

Loading…
Cancel
Save