From 92c06e4f1f72dc5631b667886d3eef8c5a3e5511 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 10 Dec 2018 06:52:24 -0800 Subject: [PATCH] [HIL][4/4] array offsets are now HilExp.t Summary: `AccessExpression.t` represents array accesses as `ArrayOffset of t * Typ.t * t list`, i.e. the index is represented by a list of access expressions. This is not precise enough when indices cannot be represented as such. In fact, in general any `HilExp.t` can be an array index but this type was an approximation that was good enough for existing checkers based on HIL. This diff changes the type of access expressions to be parametric in the type of array offsets, and uses this to record `HilExp.t` into them when translating from SIL to HIL. To accomodate the option of not caring about array offsets (`include_array_indexes=false`), the type of array offsets is an option type. Reviewed By: mbouaziz Differential Revision: D13360944 fbshipit-source-id: b01442459 --- infer/src/IR/HilExp.ml | 111 +++++++++++++++------------- infer/src/IR/HilExp.mli | 26 +++---- infer/src/checkers/PulseModels.ml | 2 +- infer/src/checkers/uninit.ml | 2 +- infer/src/checkers/uninitDomain.ml | 2 +- infer/src/quandary/TaintAnalysis.ml | 8 +- 6 files changed, 81 insertions(+), 70 deletions(-) diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index d01dcaf04..f0e3e0366 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -32,22 +32,14 @@ module Access = struct F.pp_print_string fmt "*" end -(** Module where unsafe construction of [t] is allowed. In the rest of the code, and especially in - clients of the whole [AccessExpression] module, we do not want to allow constructing access - expressions directly as they could introduce de-normalized expressions of the form [AddressOf - (Dereference t)] or [Dereference (AddressOf t)]. +(** Module where unsafe construction of [access_expression] is allowed. In the rest of the code, and + especially in clients of the whole [AccessExpression] module, we do not want to allow + constructing access expressions directly as they could introduce de-normalized expressions of the + form [AddressOf (Dereference t)] or [Dereference (AddressOf t)]. We could make only the types of [AddressOf] and [Dereference] private but that proved too - cumbersome... *) + cumbersome... *) module T : sig - type access_expression = private - | Base of AccessPath.base - | FieldOffset of access_expression * Typ.Fieldname.t (** field access *) - | ArrayOffset of access_expression * typ_ * access_expression list (** array access *) - | AddressOf of access_expression (** "address of" operator [&] *) - | Dereference of access_expression (** "dereference" operator [*] *) - [@@deriving compare] - type t = | AccessExpression of access_expression | UnaryOperator of Unop.t * t * Typ.t option @@ -57,6 +49,13 @@ module T : sig | Constant of Const.t | Cast of Typ.t * t | Sizeof of Typ.t * t option + + and access_expression = private + | Base of AccessPath.base + | FieldOffset of access_expression * Typ.Fieldname.t + | ArrayOffset of access_expression * typ_ * t option + | AddressOf of access_expression + | Dereference of access_expression [@@deriving compare] module UnsafeAccessExpression : sig @@ -64,7 +63,7 @@ module T : sig val field_offset : access_expression -> Typ.Fieldname.t -> access_expression - val array_offset : access_expression -> Typ.t -> access_expression list -> access_expression + val array_offset : access_expression -> Typ.t -> t option -> access_expression val address_of : access_expression -> access_expression @@ -74,14 +73,6 @@ module T : sig remove_deref_after_base:bool -> AccessPath.base -> access_expression -> access_expression end end = struct - type access_expression = - | Base of AccessPath.base - | FieldOffset of access_expression * Typ.Fieldname.t (** field access *) - | ArrayOffset of access_expression * typ_ * access_expression list (** array access *) - | AddressOf of access_expression (** "address of" operator [&] *) - | Dereference of access_expression (** "dereference" operator [*] *) - [@@deriving compare] - type t = | AccessExpression of access_expression | UnaryOperator of Unop.t * t * Typ.t option @@ -91,6 +82,13 @@ end = struct | Constant of Const.t | Cast of Typ.t * t | Sizeof of Typ.t * t option + + and access_expression = + | Base of AccessPath.base + | FieldOffset of access_expression * Typ.Fieldname.t + | ArrayOffset of access_expression * typ_ * t option + | AddressOf of access_expression + | Dereference of access_expression [@@deriving compare] module UnsafeAccessExpression = struct @@ -98,7 +96,7 @@ end = struct let field_offset t field = FieldOffset (t, field) - let array_offset t typ elements = ArrayOffset (t, typ, elements) + let array_offset t typ index = ArrayOffset (t, typ, index) let address_of = function Dereference t -> t | t -> AddressOf t @@ -113,8 +111,8 @@ end = struct Base base_new | FieldOffset (ae, fld) -> FieldOffset (replace_base_inner ae, fld) - | ArrayOffset (ae, typ, aes) -> - ArrayOffset (replace_base_inner ae, typ, aes) + | ArrayOffset (ae, typ, x) -> + ArrayOffset (replace_base_inner ae, typ, x) | AddressOf ae -> AddressOf (replace_base_inner ae) | Dereference ae -> @@ -128,6 +126,13 @@ let may_pp_typ fmt typ = if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ +let pp_array_offset_opt pp_offset fmt = function + | None -> + F.pp_print_string fmt "_" + | Some offset -> + pp_offset fmt offset + + let rec pp_access_expr fmt = function | Base (pvar, typ) -> Var.pp fmt pvar ; may_pp_typ fmt typ @@ -135,19 +140,15 @@ let rec pp_access_expr fmt = function F.fprintf fmt "%a->%a" pp_access_expr ae Typ.Fieldname.pp fld | FieldOffset (ae, fld) -> F.fprintf fmt "%a.%a" pp_access_expr ae Typ.Fieldname.pp fld - | ArrayOffset (ae, typ, []) -> - F.fprintf fmt "%a[_]%a" pp_access_expr ae may_pp_typ typ - | ArrayOffset (ae, typ, index_aes) -> - F.fprintf fmt "%a[%a]%a" pp_access_expr ae - (PrettyPrintable.pp_collection ~pp_item:pp_access_expr) - index_aes may_pp_typ typ + | ArrayOffset (ae, typ, index) -> + F.fprintf fmt "%a[%a]%a" pp_access_expr ae (pp_array_offset_opt pp) index may_pp_typ typ | AddressOf ae -> F.fprintf fmt "&(%a)" pp_access_expr ae | Dereference ae -> F.fprintf fmt "*(%a)" pp_access_expr ae -let rec pp fmt = function +and pp fmt = function | AccessExpression access_expr -> pp_access_expr fmt access_expr | UnaryOperator (op, e, _) -> @@ -199,7 +200,7 @@ module AccessExpression = struct type nonrec t = access_expression = private | Base of AccessPath.base | FieldOffset of access_expression * Typ.Fieldname.t - | ArrayOffset of access_expression * typ_ * access_expression list + | ArrayOffset of access_expression * typ_ * t option | AddressOf of access_expression | Dereference of access_expression [@@deriving compare] @@ -212,8 +213,8 @@ module AccessExpression = struct (base, accesses) | FieldOffset (ae, fld) -> aux (Access.FieldAccess fld :: accesses) ae - | ArrayOffset (ae, typ, indexes) -> - aux (Access.ArrayAccess (typ, f_array_offset indexes) :: accesses) ae + | ArrayOffset (ae, typ, index) -> + aux (Access.ArrayAccess (typ, f_array_offset index) :: accesses) ae | AddressOf ae -> aux (Access.TakeAddress :: accesses) ae | Dereference ae -> @@ -231,8 +232,11 @@ module AccessExpression = struct | 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 + | ArrayOffset (ae, typ, index_opt) -> + let access_paths = + Option.value_map index_opt ~default:[] ~f:(fun index -> + to_access_paths (get_access_exprs index) ) + in let base, accesses = to_access_path_ ae in (base, AccessPath.ArrayAccess (typ, access_paths) :: accesses) | AddressOf ae | Dereference ae -> @@ -329,9 +333,14 @@ let rec get_typ tenv = function Some (Typ.mk (Typ.Tint Typ.IUInt)) +let rec array_index_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp typ = + if include_array_indexes then + Some (of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ) + else None + + (* Adapted from AccessPath.of_exp. *) -let access_exprs_of_exp ~include_array_indexes ~add_deref exp0 typ0 - ~(f_resolve_id : Var.t -> AccessExpression.t option) = +and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp0 typ0 = let rec of_exp_ exp typ (add_accesses : AccessExpression.t -> AccessExpression.t) acc : AccessExpression.t list = match exp with @@ -376,11 +385,12 @@ let access_exprs_of_exp ~include_array_indexes ~add_deref exp0 typ0 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 [] + let index = + let index_typ = (* TODO: bogus *) Typ.void in + array_index_of_exp ~include_array_indexes ~f_resolve_id ~add_deref index_exp index_typ in let add_array_access_expr access_expr = - add_accesses (AccessExpression.array_offset access_expr typ index_access_exprs) + add_accesses (AccessExpression.array_offset access_expr typ index) in let array_typ = Typ.mk_array typ in of_exp_ root_exp array_typ add_array_access_expr acc @@ -398,12 +408,11 @@ let access_exprs_of_exp ~include_array_indexes ~add_deref exp0 typ0 of_exp_ exp0 typ0 Fn.id [] -let access_expr_of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ - ~(f_resolve_id : Var.t -> AccessExpression.t option) = +and access_expr_of_lhs_exp ~include_array_indexes ~f_resolve_id ~add_deref lhs_exp typ = match lhs_exp with | Exp.Lfield _ when not add_deref -> ( let res = - access_exprs_of_exp ~include_array_indexes ~add_deref:true lhs_exp typ ~f_resolve_id + access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref:true lhs_exp typ in match res with [lhs_ae] -> Some (AccessExpression.address_of lhs_ae) | _ -> None ) | Exp.Lindex _ when not add_deref -> ( @@ -416,11 +425,11 @@ let access_expr_of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ (* T29630813 investigate cases where this is not a pointer *) typ in - access_exprs_of_exp ~include_array_indexes ~add_deref:true lhs_exp typ' ~f_resolve_id + access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref:true lhs_exp typ' in match res with [lhs_ae] -> Some (AccessExpression.address_of lhs_ae) | _ -> None ) | _ -> ( - let res = access_exprs_of_exp ~include_array_indexes ~add_deref lhs_exp typ ~f_resolve_id in + let res = access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref lhs_exp typ in match res with [lhs_ae] -> Some lhs_ae | _ -> None ) @@ -428,7 +437,7 @@ let access_expr_of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ 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 ~add_deref exp typ = +and 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 -> @@ -472,7 +481,7 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = in Closure (closure.name, environment) | Lfield (root_exp, fld, root_exp_typ) -> ( - match access_expr_of_lhs_exp ~include_array_indexes ~add_deref exp typ ~f_resolve_id with + match access_expr_of_lhs_exp ~include_array_indexes ~f_resolve_id ~add_deref exp typ with | Some access_expr -> AccessExpression access_expr | None -> @@ -490,7 +499,7 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = literal, e.g. using `const_cast` *) of_sil_ (Exp.Lindex (Var (Ident.create_normal (Ident.string_to_name s) 0), index_exp)) typ | Lindex (root_exp, index_exp) -> ( - match access_expr_of_lhs_exp ~include_array_indexes ~add_deref exp typ ~f_resolve_id with + match access_expr_of_lhs_exp ~include_array_indexes ~f_resolve_id ~add_deref exp typ with | Some access_expr -> AccessExpression access_expr | None -> @@ -501,7 +510,7 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = , index_exp )) typ ) | Lvar _ -> ( - match access_expr_of_lhs_exp ~include_array_indexes ~add_deref exp typ ~f_resolve_id with + match access_expr_of_lhs_exp ~include_array_indexes ~f_resolve_id ~add_deref exp typ with | Some access_expr -> AccessExpression access_expr | None -> diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index 585d76d47..52db9f620 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -19,13 +19,6 @@ module Access : sig val pp : (Format.formatter -> 'array_index -> unit) -> Format.formatter -> 'array_index t -> unit end -type access_expression = private - | Base of AccessPath.base - | FieldOffset of access_expression * Typ.Fieldname.t (** field access *) - | ArrayOffset of access_expression * Typ.t * access_expression list (** array access *) - | AddressOf of access_expression (** "address of" operator [&] *) - | Dereference of access_expression (** "dereference" operator [*] *) - type t = | AccessExpression of access_expression (** access path (e.g., x.f.g or x[i]) *) | UnaryOperator of Unop.t * t * Typ.t option @@ -38,6 +31,13 @@ type t = | Sizeof of Typ.t * t option (** C-style sizeof(), and also used to treate a type as an expression. Refer to [Exp] module for canonical documentation *) + +and access_expression = private + | Base of AccessPath.base + | FieldOffset of access_expression * Typ.Fieldname.t (** field access *) + | ArrayOffset of access_expression * Typ.t * t option (** array access *) + | AddressOf of access_expression (** "address of" operator [&] *) + | Dereference of access_expression (** "dereference" operator [*] *) [@@deriving compare] module AccessExpression : sig @@ -45,13 +45,13 @@ module AccessExpression : sig val field_offset : access_expression -> Typ.Fieldname.t -> access_expression - val array_offset : access_expression -> Typ.t -> access_expression list -> access_expression + val array_offset : access_expression -> Typ.t -> t option -> access_expression val dereference : access_expression -> access_expression (** guarantees that we never build [Dereference (AddressOf t)] expressions: these become [t] *) val to_accesses : - f_array_offset:(access_expression list -> 'array_index) + f_array_offset:(t option -> 'array_index) -> access_expression -> AccessPath.base * 'array_index Access.t list @@ -74,10 +74,10 @@ module AccessExpression : sig type nonrec t = access_expression = private | Base of AccessPath.base - | FieldOffset of access_expression * Typ.Fieldname.t (** field access *) - | ArrayOffset of access_expression * Typ.t * access_expression list (** array access *) - | AddressOf of access_expression (** "address of" operator [&] *) - | Dereference of access_expression (** "dereference" operator [*] *) + | FieldOffset of access_expression * Typ.Fieldname.t + | ArrayOffset of access_expression * Typ.t * t option + | AddressOf of access_expression + | Dereference of access_expression [@@deriving compare] end diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index 9a48e06aa..a77c120ea 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -83,7 +83,7 @@ module StdVector = struct let to_internal_array vector = HilExp.AccessExpression.field_offset vector internal_array let deref_internal_array vector = - HilExp.AccessExpression.(array_offset (dereference (to_internal_array vector)) Typ.void []) + HilExp.AccessExpression.(array_offset (dereference (to_internal_array vector)) Typ.void None) let reallocate_internal_array vector vector_f location astate = diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 7a14e414c..3661247b8 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -333,7 +333,7 @@ module Initial = struct | _ -> acc ) | Typ.Tarray {elt} -> - HilExp.AccessExpression.array_offset base_access_expr elt [] :: acc + HilExp.AccessExpression.array_offset base_access_expr elt None :: acc | Typ.Tptr _ -> base_access_expr :: HilExp.AccessExpression.dereference base_access_expr :: acc | _ -> diff --git a/infer/src/checkers/uninitDomain.ml b/infer/src/checkers/uninitDomain.ml index df9af18bf..8bb8315ee 100644 --- a/infer/src/checkers/uninitDomain.ml +++ b/infer/src/checkers/uninitDomain.ml @@ -73,7 +73,7 @@ module MaybeUninitVars = struct match base with | _, {Typ.desc= Tptr (elt, _)} -> remove - (HilExp.AccessExpression.array_offset (HilExp.AccessExpression.base base) elt []) + (HilExp.AccessExpression.array_offset (HilExp.AccessExpression.base base) elt None) maybe_uninit_vars | _ -> maybe_uninit_vars diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 068d838e7..a447d5d85 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -454,14 +454,16 @@ module Make (TaintSpecification : TaintSpec.S) = struct | HilExp.AccessExpression.Base _ -> astate_acc | HilExp.AccessExpression.FieldOffset (ae, _) - | ArrayOffset (ae, _, []) + | ArrayOffset (ae, _, None) | AddressOf ae | Dereference ae -> add_sinks_for_access astate_acc ae - | HilExp.AccessExpression.ArrayOffset (ae, _, indexes) -> + | HilExp.AccessExpression.ArrayOffset (ae, _, Some index) -> let dummy_call_site = CallSite.make BuiltinDecl.__array_access loc in let dummy_actuals = - List.map ~f:(fun index_ae -> HilExp.AccessExpression index_ae) indexes + List.map + ~f:(fun index_ae -> HilExp.AccessExpression index_ae) + (HilExp.get_access_exprs index) in let sinks = TraceDomain.Sink.get dummy_call_site dummy_actuals CallFlags.default