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

[inferbo] Refactor domain constructors for field

Browse Source 
Summary:
In inferbo's domain, `Loc.t` and `Symb.SymbolPath.partial` are defined with the same *field abstraction*.  The depth of appended fields were limited in both of them exactly in the same way, e.g. `x.*.field`. Problem is that the implementation related
to the field abstraction are duplicated in their code, which had been synchronized manually. This diff avoids the duplication by adding a `BufferOverrunField.t`.

Reviewed By: ezgicicek

Differential Revision: D21743728

fbshipit-source-id: 4b01d027c
master
Sungkeun Cho 5 years ago committed by Facebook GitHub Bot
parent 97ad5b9c96
commit 10a111d41b
16 changed files with 348 additions and 321 deletions
Show Stats Download Patch File Download Diff File

265
infer/src/bufferoverrun/absLoc.ml
Unescape View File

@ -9,6 +9,7 @@
open! IStd
module F = Format
module BoField = BufferOverrunField
module Allocsite = struct
type t =
@ -125,121 +126,86 @@ module Allocsite = struct
end
module Loc = struct
type field_typ = Typ.t option
let compare_field_typ _ _ = 0
include (* Enforce invariants on Field and StarField, see Symb.mli *) (
struct
type t =
| Var of Var.t
| Allocsite of Allocsite.t
| Field of {prefix: t; fn: Fieldname.t; typ: field_typ}
| StarField of {prefix: t; last_field: Fieldname.t}
[@@deriving compare]
let of_var v = Var v
let of_allocsite a = Allocsite a
let append_star_field l0 ~fn =
let rec aux l =
match l with
| Allocsite a when Allocsite.is_unknown a ->
l
| Var _ | Allocsite _ ->
StarField {prefix= l0; last_field= fn}
| StarField {last_field} when Fieldname.equal fn last_field ->
l
| StarField {prefix} ->
StarField {prefix; last_field= fn}
| Field {prefix= l} ->
aux l
in
aux l0
let append_field ?typ l0 ~fn =
let rec aux ~depth l =
if Symb.SymbolPath.is_field_depth_beyond_limit depth then append_star_field l0 ~fn
else
match l with
| Allocsite a when Allocsite.is_unknown a ->
l
| Var _ | Allocsite _ ->
Field {prefix= l0; fn; typ}
| StarField {last_field} as l when Fieldname.equal fn last_field ->
l
| StarField {prefix} ->
StarField {prefix; last_field= fn}
| Field {fn= fn'} when Fieldname.equal fn fn' ->
StarField {prefix= l0; last_field= fn}
| Field {prefix= l} ->
aux ~depth:(depth + 1) l
in
aux ~depth:0 l0
end :
sig
type t = private
| Var of Var.t
| Allocsite of Allocsite.t
| Field of {prefix: t; fn: Fieldname.t; typ: field_typ}
| StarField of {prefix: t; last_field: Fieldname.t}
[@@deriving compare]
val of_var : Var.t -> t
val of_allocsite : Allocsite.t -> t
val append_field : ?typ:Typ.t -> t -> fn:Fieldname.t -> t
val append_star_field : t -> fn:Fieldname.t -> t
end )
type prim = Var of Var.t | Allocsite of Allocsite.t [@@deriving compare]
type t = prim BoField.t [@@deriving compare]
let of_var v = BoField.Prim (Var v)
let of_allocsite a = BoField.Prim (Allocsite a)
let prim_append_field ?typ l0 fn _aux _depth = function
| Allocsite a as l when Allocsite.is_unknown a ->
BoField.Prim l
| Var _ | Allocsite _ ->
BoField.Field {prefix= l0; fn; typ}
let prim_append_star_field l0 fn _aux = function
| Allocsite a as l when Allocsite.is_unknown a ->
BoField.Prim l
| Var _ | Allocsite _ ->
BoField.StarField {prefix= l0; last_field= fn}
let append_field = BoField.mk_append_field ~prim_append_field ~prim_append_star_field
let append_star_field = BoField.mk_append_star_field ~prim_append_star_field
let equal = [%compare.equal: t]
let eq l1 l2 =
match (l1, l2) with Allocsite as1, Allocsite as2 -> Allocsite.eq as1 as2 | _ -> Boolean.Top
match (l1, l2) with
| BoField.Prim (Allocsite as1), BoField.Prim (Allocsite as2) ->
Allocsite.eq as1 as2
| _ ->
Boolean.Top
let unknown = of_allocsite Allocsite.unknown
let rec is_unknown = function
| Var _ ->
| BoField.Prim (Var _) ->
false
| Allocsite a ->
| BoField.Prim (Allocsite a) ->
Allocsite.is_unknown a
| Field {prefix= x} | StarField {prefix= x} ->
| BoField.(Field {prefix= x} | StarField {prefix= x}) ->
is_unknown x
let rec pp_paren ~paren fmt =
let module SP = Symb.SymbolPath in
function
| Var v ->
| BoField.Prim (Var v) ->
Var.pp F.str_formatter v ;
let s = F.flush_str_formatter () in
if Char.equal s.[0] '&' then
F.pp_print_string fmt (String.sub s ~pos:1 ~len:(String.length s - 1))
else F.pp_print_string fmt s
| Allocsite a ->
| BoField.Prim (Allocsite a) ->
Allocsite.pp_paren ~paren fmt a
| Field
| BoField.Field
{ prefix=
Allocsite
(Allocsite.Symbol (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p)))
Prim
(Allocsite
(Allocsite.Symbol
(BoField.Prim (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p)))))
; fn= f }
| Field
| BoField.Field
{ prefix=
Allocsite
(Allocsite.Known
{path= Some (SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p))})
Prim
(Allocsite
(Allocsite.Known
{ path=
Some
(BoField.Prim
(SP.Deref ((SP.Deref_COneValuePointer | SP.Deref_CPointer), p))) }))
; fn= f } ->
BufferOverrunField.pp ~pp_lhs:(SP.pp_partial_paren ~paren:true) ~sep:"->" fmt p f
| Field {prefix= l; fn= f} ->
BufferOverrunField.pp ~pp_lhs:(pp_paren ~paren:true) ~sep:"." fmt l f
| StarField {prefix; last_field} ->
BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field
BoField.pp ~pp_lhs:(SP.pp_partial_paren ~paren:true) ~sep:"->" fmt p f
| BoField.Field {prefix= l; fn= f} ->
BoField.pp ~pp_lhs:(pp_paren ~paren:true) ~sep:"." fmt l f
| BoField.StarField {prefix; last_field} ->
BoField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field
and pp_star ~paren fmt l =
@ -249,34 +215,39 @@ module Loc = struct
let pp = pp_paren ~paren:false
let is_var = function Var _ -> true | _ -> false
let is_var = function BoField.Prim (Var _) -> true | _ -> false
let is_c_strlen = function
| Field {fn} ->
Fieldname.equal fn (BufferOverrunField.c_strlen ())
| BoField.Field {fn} ->
Fieldname.equal fn (BoField.c_strlen ())
| _ ->
false
let is_java_collection_internal_array = function
| Field {fn} ->
Fieldname.equal fn BufferOverrunField.java_collection_internal_array
| BoField.Field {fn} ->
Fieldname.equal fn BoField.java_collection_internal_array
| _ ->
false
let is_frontend_tmp = function Var x -> not (Var.appears_in_source_code x) | _ -> false
let is_frontend_tmp = function
| BoField.Prim (Var x) ->
not (Var.appears_in_source_code x)
| _ ->
false
let rec is_pretty = function
| Var _ ->
| BoField.Prim (Var _) ->
true
| Allocsite a ->
| BoField.Prim (Allocsite a) ->
Allocsite.is_pretty a
| Field {prefix= loc} | StarField {prefix= loc} ->
| BoField.Field {prefix= loc} | StarField {prefix= loc} ->
is_pretty loc
let of_c_strlen loc = append_field loc ~fn:(BufferOverrunField.c_strlen ())
let of_c_strlen loc = append_field loc (BoField.c_strlen ())
let of_pvar pvar = of_var (Var.of_pvar pvar)
@ -284,42 +255,51 @@ module Loc = struct
let rec of_path path =
match path with
| Symb.SymbolPath.Pvar pvar ->
| BoField.Prim (Symb.SymbolPath.Pvar pvar) ->
of_pvar pvar
| Symb.SymbolPath.Deref _ | Symb.SymbolPath.Callsite _ ->
| BoField.Prim (Symb.SymbolPath.Deref _ | Symb.SymbolPath.Callsite _) ->
of_allocsite (Allocsite.make_symbol path)
| Symb.SymbolPath.Field {fn; prefix= path} ->
append_field (of_path path) ~fn
| Symb.SymbolPath.StarField {last_field= fn; prefix} ->
append_star_field (of_path prefix) ~fn
| BoField.Field {fn; prefix= path} ->
append_field (of_path path) fn
| BoField.StarField {last_field= fn; prefix} ->
append_star_field (of_path prefix) fn
let is_return = function
| Var (Var.ProgramVar x) ->
| BoField.Prim (Var (Var.ProgramVar x)) ->
Mangled.equal (Pvar.get_name x) Ident.name_return
| _ ->
false
let is_field_of ~loc ~field_loc =
match field_loc with Field {prefix= l} | StarField {prefix= l} -> equal loc l | _ -> false
match field_loc with
| BoField.(Field {prefix= l} | StarField {prefix= l}) ->
equal loc l
| _ ->
false
let get_literal_string = function
| BoField.Prim (Allocsite a) ->
Allocsite.get_literal_string a
| _ ->
None
let get_literal_string = function Allocsite a -> Allocsite.get_literal_string a | _ -> None
let get_literal_string_strlen = function
| Field {prefix= l; fn} when Fieldname.equal (BufferOverrunField.c_strlen ()) fn ->
| BoField.Field {prefix= l; fn} when Fieldname.equal (BoField.c_strlen ()) fn ->
get_literal_string l
| _ ->
None
let rec is_global = function
| Var (Var.ProgramVar pvar) ->
| BoField.Prim (Var (Var.ProgramVar pvar)) ->
Pvar.is_global pvar
| Var (Var.LogicalVar _) | Allocsite _ ->
| BoField.Prim (Var (Var.LogicalVar _) | Allocsite _) ->
false
| Field {prefix= loc} | StarField {prefix= loc} ->
| BoField.(Field {prefix= loc} | StarField {prefix= loc}) ->
is_global loc
@ -328,63 +308,64 @@ module Loc = struct
if Pvar.is_constant_array pvar then Pvar.get_initializer_pname pvar else None
in
function
| Var (Var.ProgramVar pvar) ->
| BoField.Prim (Var (Var.ProgramVar pvar)) ->
initializer_of_pvar pvar
| Var (Var.LogicalVar _) ->
| BoField.Prim (Var (Var.LogicalVar _)) ->
None
| Allocsite allocsite ->
| BoField.Prim (Allocsite allocsite) ->
Allocsite.get_path allocsite
|> Option.bind ~f:Symb.SymbolPath.get_pvar
|> Option.bind ~f:initializer_of_pvar
| Field {prefix= loc} | StarField {prefix= loc} ->
| BoField.(Field {prefix= loc} | StarField {prefix= loc}) ->
get_global_array_initializer loc
let rec get_path = function
| Var (LogicalVar _) ->
| BoField.Prim (Var (LogicalVar _)) ->
None
| Var (ProgramVar pvar) ->
| BoField.Prim (Var (ProgramVar pvar)) ->
Some (Symb.SymbolPath.of_pvar pvar)
| Allocsite allocsite ->
| BoField.Prim (Allocsite allocsite) ->
Allocsite.get_path allocsite
| Field {prefix= l; fn; typ} ->
Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field ?typ p fn)
| StarField {prefix; last_field} ->
get_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.star_field p last_field)
| BoField.Field {prefix= l; fn; typ} ->
Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.append_field ?typ p fn)
| BoField.StarField {prefix; last_field} ->
get_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.append_star_field p last_field)
let rec get_param_path = function
| Var _ ->
| BoField.Prim (Var _) ->
None
| Allocsite allocsite ->
| BoField.Prim (Allocsite allocsite) ->
Allocsite.get_param_path allocsite
| Field {prefix= l; fn} ->
Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
| StarField {prefix; last_field} ->
get_param_path prefix |> Option.map ~f:(fun p -> Symb.SymbolPath.star_field p last_field)
| BoField.Field {prefix= l; fn} ->
Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.append_field p fn)
| BoField.StarField {prefix; last_field} ->
get_param_path prefix
|> Option.map ~f:(fun p -> Symb.SymbolPath.append_star_field p last_field)
let rec represents_multiple_values = function
| Var _ ->
| BoField.Prim (Var _) ->
false
| Allocsite allocsite ->
| BoField.Prim (Allocsite allocsite) ->
Allocsite.represents_multiple_values allocsite
| Field _ as x when is_c_strlen x || is_java_collection_internal_array x ->
| BoField.Field _ as x when is_c_strlen x || is_java_collection_internal_array x ->
false
| Field {prefix= l} ->
| BoField.Field {prefix= l} ->
represents_multiple_values l
| StarField _ ->
| BoField.StarField _ ->
true
let rec exists_pvar ~f = function
| Var (LogicalVar _) ->
| BoField.Prim (Var (LogicalVar _)) ->
false
| Var (ProgramVar pvar) ->
| BoField.Prim (Var (ProgramVar pvar)) ->
f pvar
| Allocsite allocsite ->
| BoField.Prim (Allocsite allocsite) ->
Allocsite.exists_pvar ~f allocsite
| Field {prefix= l} | StarField {prefix= l} ->
| BoField.(Field {prefix= l} | StarField {prefix= l}) ->
exists_pvar ~f l
@ -394,9 +375,9 @@ module Loc = struct
let cast typ x =
match x with
| Field {prefix= l; fn} ->
append_field l ~fn ~typ
| StarField _ | Var _ | Allocsite _ ->
| BoField.Field {prefix= l; fn} ->
append_field l fn ~typ
| BoField.(StarField _ | Prim (Var _ | Allocsite _)) ->
x
end
@ -546,7 +527,7 @@ module PowLoc = struct
| Unknown ->
Unknown
| Known ploc ->
mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_field l ~fn)) ploc LocSet.empty)
mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_field l fn)) ploc LocSet.empty)
let append_star_field ploc ~fn =
@ -557,7 +538,7 @@ module PowLoc = struct
| Unknown ->
Unknown
| Known ploc ->
mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_star_field l ~fn)) ploc LocSet.empty)
mk_known (LocSet.fold (fun l -> LocSet.add (Loc.append_star_field l fn)) ploc LocSet.empty)
let lift_cmp cmp_loc ploc1 ploc2 =

14
infer/src/bufferoverrun/absLoc.mli
Unescape View File

@ -43,17 +43,9 @@ module Allocsite : sig
end
module Loc : sig
type field_typ
type prim = private Var of Var.t | Allocsite of Allocsite.t [@@deriving compare]
type t = private
| Var of Var.t (** abstract location of variable *)
| Allocsite of Allocsite.t (** abstract location of allocsites *)
| Field of {prefix: t; fn: Fieldname.t; typ: field_typ}
(** field appended abstract locations, i.e., [prefix.fn] *)
| StarField of {prefix: t; last_field: Fieldname.t}
(** field appended abstract locations, but some of intermediate fields are abstracted, i.e.,
[prefix.*.fn] *)
[@@deriving equal]
type t = prim BufferOverrunField.t [@@deriving compare, equal]
include PrettyPrintable.PrintableOrderedType with type t := t
@ -104,7 +96,7 @@ module Loc : sig
val represents_multiple_values : t -> bool
val append_field : ?typ:Typ.typ -> t -> fn:Fieldname.t -> t
val append_field : ?typ:Typ.typ -> t -> Fieldname.t -> t
(** It appends field. [typ] is the type of [fn]. *)
end

12
infer/src/bufferoverrun/arrayBlk.ml
Unescape View File

@ -10,6 +10,7 @@
open! IStd
open AbsLoc
open! AbstractDomain.Types
module BoField = BufferOverrunField
module Bound = Bounds.Bound
module F = Format
module L = Logging
@ -136,9 +137,9 @@ module ArrInfo = struct
let is_pointer : Symb.SymbolPath.partial -> t -> bool =
fun path arr ->
match (path, arr) with
| Deref ((Deref_COneValuePointer | Deref_CPointer), path), C {offset; size} ->
| BoField.Prim (Deref ((Deref_COneValuePointer | Deref_CPointer), path)), C {offset; size} ->
Itv.is_offset_path_of path offset && Itv.is_length_path_of path size
| Deref (Deref_JavaPointer, path), Java {length} ->
| BoField.Prim (Deref (Deref_JavaPointer, path)), Java {length} ->
Itv.is_length_path_of path length
| _, _ ->
false
@ -274,7 +275,7 @@ module ArrInfo = struct
let is_symbolic_length_of_path path info =
match (path, info) with
| Symb.SymbolPath.Deref (_, prefix), Java {length} ->
| BoField.Prim (Symb.SymbolPath.Deref (_, prefix)), Java {length} ->
Itv.is_length_path_of prefix length
| _ ->
false
@ -341,11 +342,12 @@ let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> PowLoc.t * t =
let locs = eval_locpath path in
let add_allocsite l (powloc_acc, acc) =
match l with
| Loc.Allocsite (Symbol (Symb.SymbolPath.Deref (_, prefix)) as a)
| BoField.Prim
(Loc.Allocsite (Symbol (BoField.Prim (Symb.SymbolPath.Deref (_, prefix))) as a))
when ArrInfo.is_symbolic_length_of_path path info ->
let length = Itv.of_length_path ~is_void:false prefix in
(powloc_acc, add a (ArrInfo.make_java ~length) acc)
| Loc.Allocsite a ->
| BoField.Prim (Loc.Allocsite a) ->
(powloc_acc, add a info' acc)
| _ ->
if ArrInfo.is_pointer path info then (PowLoc.add l powloc_acc, acc)

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

@ -196,7 +196,7 @@ module TransferFunctions = struct
Loc.of_var (Var.of_pvar (Pvar.mk_global class_mangled))
in
let fn = Fieldname.make typename "$VALUES" in
Loc.append_field class_var ~fn
Loc.append_field class_var fn
in
let v = Dom.Mem.find loc clinit_mem in
let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
@ -229,7 +229,7 @@ module TransferFunctions = struct
~f:(fun (clinit_pname, pvar, fn, field_typ) ->
let copy_from_class_init () =
Option.value_map (get_summary clinit_pname) ~default:mem ~f:(fun clinit_mem ->
let field_loc = Loc.append_field ~typ:field_typ (Loc.of_pvar pvar) ~fn in
let field_loc = Loc.append_field ~typ:field_typ (Loc.of_pvar pvar) fn in
copy_reachable_locs_from field_loc ~from_mem:clinit_mem ~to_mem:mem )
in
match field_typ.Typ.desc with

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

@ -10,6 +10,7 @@
open! IStd
open AbsLoc
open! AbstractDomain.Types
module BoField = BufferOverrunField
module F = Format
module L = Logging
module OndemandEnv = BufferOverrunOndemandEnv
@ -1874,7 +1875,7 @@ module LatestPrune = struct
match PowLoc.is_singleton_or_more (PowLoc.subst_loc (Loc.of_pvar x) eval_locpath) with
| Empty ->
Error `SubstBottom
| Singleton (Loc.Var (Var.ProgramVar x')) ->
| Singleton (BoField.Prim (Loc.Var (Var.ProgramVar x'))) ->
Ok x'
| Singleton _ | More ->
Error `SubstFail
@ -2235,7 +2236,7 @@ module MemReach = struct
Some v1
in
let apply_simple_alias1 ((m_acc, prunes_acc) as acc) = function
| Loc.Var (Var.ProgramVar y), i when Pvar.equal x y && IntLit.iszero i ->
| BoField.Prim (Loc.Var (Var.ProgramVar y)), i when Pvar.equal x y && IntLit.iszero i ->
(apply_prunes prunes m_acc, PrunePairs.union pruned_val_meet prunes_acc prunes)
| _ ->
acc
@ -2259,7 +2260,7 @@ module MemReach = struct
let tgts = Alias.find_ret m.alias in
let replace_latest_prune l tgt acc =
match (l, tgt) with
| Loc.Var (ProgramVar pvar), AliasTarget.Simple {i} when IntLit.iszero i ->
| BoField.Prim (Loc.Var (ProgramVar pvar)), AliasTarget.Simple {i} when IntLit.iszero i ->
{acc with latest_prune= LatestPrune.replace ~from:pvar ~to_:return m.latest_prune}
| _ ->
acc
@ -2606,7 +2607,11 @@ module Mem = struct
let get_c_strlen locs m =
let get_c_strlen' loc acc =
match loc with Loc.Allocsite _ -> Val.join acc (find (Loc.of_c_strlen loc) m) | _ -> acc
match loc with
| BoField.Prim (Loc.Allocsite _) ->
Val.join acc (find (Loc.of_c_strlen loc) m)
| _ ->
acc
in
PowLoc.fold get_c_strlen' locs Val.bot

52
infer/src/bufferoverrun/bufferOverrunField.ml
Unescape View File

@ -56,3 +56,55 @@ let cpp_vector_elem ~vec_typ ~elt_typ =
let is_cpp_vector_elem fn = String.equal (Fieldname.to_simplified_string fn) cpp_vector_elem_str
(** Field domain constructor *)
type field_typ = Typ.t option
let compare_field_typ _ _ = 0
type 'prim t =
| Prim of 'prim
| Field of {prefix: 'prim t; fn: Fieldname.t; typ: field_typ}
| StarField of {prefix: 'prim t; last_field: Fieldname.t}
[@@deriving compare]
let is_field_depth_beyond_limit =
match Config.bo_field_depth_limit with
| None ->
fun _depth -> false
| Some limit ->
fun depth -> depth > limit
let mk_append_star_field ~prim_append_star_field p0 fn =
let rec aux = function
| Prim prim ->
prim_append_star_field p0 fn aux prim
| Field {prefix= p} ->
aux p
| StarField {last_field} as p when Fieldname.equal fn last_field ->
p
| StarField {prefix} ->
StarField {last_field= fn; prefix}
in
aux p0
let mk_append_field ~prim_append_field ~prim_append_star_field ?typ p0 fn =
let rec aux ~depth p =
if is_field_depth_beyond_limit depth then mk_append_star_field ~prim_append_star_field p0 fn
else
match p with
| Prim prim ->
prim_append_field ?typ p0 fn aux depth prim
| Field {fn= fn'} when Fieldname.equal fn fn' ->
StarField {last_field= fn; prefix= p0}
| Field {prefix= p} ->
aux ~depth:(depth + 1) p
| StarField {last_field} as p when Fieldname.equal fn last_field ->
p
| StarField {prefix} ->
StarField {prefix; last_field= fn}
in
aux ~depth:0 p0

39
infer/src/bufferoverrun/bufferOverrunField.mli
Unescape View File

@ -6,6 +6,8 @@
*)
open! IStd
(** {2 Inferbo-specific constant field names} *)
val pp :
pp_lhs:(Format.formatter -> 'a -> unit)
-> sep:string
@ -32,3 +34,40 @@ val is_cpp_vector_elem : Fieldname.t -> bool
val is_java_collection_internal_array : Fieldname.t -> bool
(** Check if the field is for Java collection's elements *)
(** {2 Field domain constructor} *)
type field_typ = Typ.t option
type 'prim t =
| Prim of 'prim
| Field of {prefix: 'prim t; fn: Fieldname.t; typ: field_typ}
| StarField of {prefix: 'prim t; last_field: Fieldname.t}
(** Represents a path starting with [prefix] and ending with the field [last_field], the
middle can be anything. Invariants:
- There is at most one StarField
- StarField excluded, there are no duplicate fieldnames
- StarField can only be followed by Deref elements *)
[@@deriving compare]
val mk_append_field :
prim_append_field:
( ?typ:Typ.t
-> 'prim t
-> Fieldname.t
-> (depth:int -> 'prim t -> 'prim t)
-> int
-> 'prim
-> 'prim t)
-> prim_append_star_field:('prim t -> Fieldname.t -> ('prim t -> 'prim t) -> 'prim -> 'prim t)
-> ?typ:Typ.t
-> 'prim t
-> Fieldname.t
-> 'prim t
val mk_append_star_field :
prim_append_star_field:('prim t -> Fieldname.t -> ('prim t -> 'prim t) -> 'prim -> 'prim t)
-> 'prim t
-> Fieldname.t
-> 'prim t

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

@ -9,6 +9,7 @@ open! IStd
open AbsLoc
open! AbstractDomain.Types
module L = Logging
module BoField = BufferOverrunField
module BoUtils = BufferOverrunUtils
module Dom = BufferOverrunDomain
module PO = BufferOverrunProofObligations
@ -525,7 +526,7 @@ module ArrObjCommon = struct
let size_exec exp ~fn ({integer_type_widths} as model_env) ~ret:(id, _) mem =
let locs = Sem.eval integer_type_widths exp mem |> Dom.Val.get_all_locs in
match PowLoc.is_singleton_or_more locs with
| Singleton (Loc.Allocsite (Allocsite.LiteralString s)) ->
| Singleton (BoField.Prim (Loc.Allocsite (Allocsite.LiteralString s))) ->
model_by_value (Dom.Val.of_int (String.length s)) id mem
| _ ->
let arr_locs = deref_of model_env exp ~fn mem in
@ -568,7 +569,7 @@ end
module StdVector = struct
let append_field loc ~vec_typ ~elt_typ =
Loc.append_field loc ~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
Loc.append_field loc (BufferOverrunField.cpp_vector_elem ~vec_typ ~elt_typ)
let append_fields locs ~vec_typ ~elt_typ =
@ -828,7 +829,7 @@ module Collection = struct
in
let coll_loc = Loc.of_allocsite coll_allocsite in
let internal_array_loc =
Loc.append_field coll_loc ~fn:BufferOverrunField.java_collection_internal_array
Loc.append_field coll_loc BufferOverrunField.java_collection_internal_array
in
mem
|> Dom.Mem.add_heap internal_array_loc internal_array
@ -1102,7 +1103,7 @@ module JavaString = struct
~represents_multiple_values:true
in
Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_loc arr_loc) mem
|> Dom.Mem.add_heap (Loc.append_field arr_loc ~fn)
|> Dom.Mem.add_heap (Loc.append_field arr_loc fn)
(Dom.Val.of_java_array_alloc elem_alloc ~length ~traces)
|> Dom.Mem.add_heap (Loc.of_allocsite elem_alloc) elem
in
@ -1224,7 +1225,7 @@ module JavaString = struct
in
let traces = Trace.(Set.singleton location ArrayDeclaration) in
Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_loc arr_loc) mem
|> Dom.Mem.add_heap (Loc.append_field arr_loc ~fn)
|> Dom.Mem.add_heap (Loc.append_field arr_loc fn)
(Dom.Val.of_java_array_alloc elem_alloc ~length:length_itv ~traces)

21
infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml
Unescape View File

@ -7,6 +7,7 @@
open! IStd
module L = Logging
module BoField = BufferOverrunField
module SPath = Symb.SymbolPath
module FormalTyps = Caml.Map.Make (Pvar)
@ -25,9 +26,9 @@ let mk pdesc =
in
fun tenv integer_type_widths ->
let rec typ_of_param_path = function
| SPath.Pvar x ->
| BoField.Prim (SPath.Pvar x) ->
FormalTyps.find_opt x formal_typs
| SPath.Deref (_, x) -> (
| BoField.Prim (SPath.Deref (_, x)) -> (
match typ_of_param_path x with
| None ->
None
@ -55,18 +56,18 @@ let mk pdesc =
L.(die InternalError) "Deref of unmodeled type `%a`" Typ.Name.pp typename )
| _ ->
L.(die InternalError) "Untyped expression is given." ) )
| SPath.Field {typ= Some _ as some_typ} ->
| BoField.Field {typ= Some _ as some_typ} ->
some_typ
| SPath.Field {fn; prefix= x} -> (
match BufferOverrunField.get_type fn with
| BoField.Field {fn; prefix= x} -> (
match BoField.get_type fn with
| None ->
let lookup = Tenv.lookup tenv in
Option.map (typ_of_param_path x) ~f:(Struct.fld_typ ~lookup ~default:Typ.void fn)
| some_typ ->
some_typ )
| SPath.StarField {last_field} ->
BufferOverrunField.get_type last_field
| SPath.Callsite {ret_typ} ->
| BoField.StarField {last_field} ->
BoField.get_type last_field
| BoField.Prim (SPath.Callsite {ret_typ}) ->
Some ret_typ
in
let is_last_field fn (fields : Struct.field list) =
@ -74,9 +75,9 @@ let mk pdesc =
Fieldname.equal fn last_fn )
in
let rec may_last_field = function
| SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ ->
| BoField.Prim (SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _) ->
true
| SPath.Field {fn; prefix= x} | SPath.StarField {last_field= fn; prefix= x} ->
| BoField.(Field {fn; prefix= x} | StarField {last_field= fn; prefix= x}) ->
may_last_field x
&& Option.value_map ~default:true (typ_of_param_path x) ~f:(fun parent_typ ->
match parent_typ.Typ.desc with

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

@ -11,6 +11,7 @@ open! IStd
open AbsLoc
open! AbstractDomain.Types
open BufferOverrunDomain
module BoField = BufferOverrunField
module L = Logging
module TraceSet = BufferOverrunTrace.Set
@ -376,7 +377,7 @@ let is_cost_mode = function EvalCost -> true | _ -> false
let eval_sympath_modeled_partial ~mode ~is_expensive p =
match (mode, p) with
| (EvalNormal | EvalCost), Symb.SymbolPath.Callsite _ ->
| (EvalNormal | EvalCost), BoField.Prim (Symb.SymbolPath.Callsite _) ->
Itv.of_modeled_path ~is_expensive p |> Val.of_itv
| _, _ ->
(* We only have modeled modeled function calls created in costModels. *)
@ -385,12 +386,12 @@ let eval_sympath_modeled_partial ~mode ~is_expensive p =
let rec eval_sympath_partial ~mode params p mem =
match p with
| Symb.SymbolPath.Pvar x -> (
| BoField.Prim (Symb.SymbolPath.Pvar x) -> (
try ParamBindings.find x params
with Caml.Not_found ->
L.d_printfln_escaped "Symbol %a is not found in parameters." (Pvar.pp Pp.text) x ;
Val.Itv.top )
| Symb.SymbolPath.Callsite {ret_typ; cs; obj_path} -> (
| BoField.Prim (Symb.SymbolPath.Callsite {ret_typ; cs; obj_path}) -> (
match mode with
| EvalNormal | EvalCost ->
L.d_printfln_escaped "Symbol for %a is not expected to be in parameters." Procname.pp
@ -404,7 +405,7 @@ let rec eval_sympath_partial ~mode params p mem =
Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
| EvalPOCond | EvalPOReachability ->
Val.Itv.top )
| Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ | Symb.SymbolPath.StarField _ ->
| BoField.(Prim (Symb.SymbolPath.Deref _) | Field _ | StarField _) ->
let locs = eval_locpath ~mode params p mem in
Mem.find_set locs mem
@ -412,16 +413,16 @@ let rec eval_sympath_partial ~mode params p mem =
and eval_locpath ~mode params p mem =
let res =
match p with
| Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ ->
| BoField.Prim (Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _) ->
let v = eval_sympath_partial ~mode params p mem in
Val.get_all_locs v
| Symb.SymbolPath.Deref (_, p) ->
| BoField.Prim (Symb.SymbolPath.Deref (_, p)) ->
let v = eval_sympath_partial ~mode params p mem in
Val.get_all_locs v
| Symb.SymbolPath.Field {fn; prefix= p} ->
| BoField.Field {fn; prefix= p} ->
let locs = eval_locpath ~mode params p mem in
PowLoc.append_field ~fn locs
| Symb.SymbolPath.StarField {last_field= fn; prefix} ->
| BoField.StarField {last_field= fn; prefix} ->
let locs = eval_locpath ~mode params prefix mem in
PowLoc.append_star_field ~fn locs
in

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

@ -103,7 +103,9 @@ module Exec = struct
let init_c_array_fields {pname; node_hash; tenv; integer_type_widths} path typ locs ?dyn_length
mem =
let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) =
let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in
let field_path =
Option.map path ~f:(fun path -> Symb.SymbolPath.append_field path field_name)
in
let field_loc = PowLoc.append_field locs ~fn:field_name in
let mem =
match field_typ.Typ.desc with

189
infer/src/bufferoverrun/symb.ml
Unescape View File

@ -7,6 +7,7 @@
open! IStd
module F = Format
module L = Logging
module BoField = BufferOverrunField
module BoundEnd = struct
type t = LowerBound | UpperBound [@@deriving compare]
@ -23,85 +24,37 @@ module SymbolPath = struct
let compare_deref_kind _ _ = 0
type field_typ = Typ.t option
let compare_field_typ _ _ = 0
let is_field_depth_beyond_limit =
match Config.bo_field_depth_limit with
| None ->
fun _depth -> false
| Some limit ->
fun depth -> depth > limit
include (* Enforce invariants on Field and StarField *) (
struct
type partial =
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of {fn: Fieldname.t; prefix: partial; typ: field_typ}
| Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option [@compare.ignore]}
| StarField of {last_field: Fieldname.t; prefix: partial}
[@@deriving compare]
let of_pvar pvar = Pvar pvar
let of_callsite ?obj_path ~ret_typ cs = Callsite {ret_typ; cs; obj_path}
let deref ~deref_kind p = Deref (deref_kind, p)
let star_field p0 fn =
let rec aux = function
| Pvar _ | Callsite _ ->
StarField {last_field= fn; prefix= p0}
| Deref (_, p) | Field {prefix= p} ->
aux p
| StarField {last_field} as p when Fieldname.equal fn last_field ->
p
| StarField {prefix} ->
StarField {last_field= fn; prefix}
in
aux p0
let field ?typ p0 fn =
let rec aux ~depth p =
if is_field_depth_beyond_limit depth then star_field p0 fn
else
match p with
| Pvar _ | Callsite _ ->
Field {fn; prefix= p0; typ}
| Field {fn= fn'} when Fieldname.equal fn fn' ->
StarField {last_field= fn; prefix= p0}
| Field {prefix= p} | Deref (_, p) ->
aux ~depth:(depth + 1) p
| StarField {last_field} as p when Fieldname.equal fn last_field ->
p
| StarField {prefix} ->
StarField {last_field= fn; prefix}
in
aux ~depth:0 p0
end :
sig
type partial = private
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of {fn: Fieldname.t; prefix: partial; typ: field_typ}
| Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option}
| StarField of {last_field: Fieldname.t; prefix: partial}
[@@deriving compare]
val of_pvar : Pvar.t -> partial
val of_callsite : ?obj_path:partial -> ret_typ:Typ.t -> CallSite.t -> partial
val deref : deref_kind:deref_kind -> partial -> partial
val field : ?typ:Typ.t -> partial -> Fieldname.t -> partial
val star_field : partial -> Fieldname.t -> partial
end )
type prim =
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option [@compare.ignore]}
[@@deriving compare]
and partial = prim BoField.t [@@deriving compare]
let of_pvar pvar = BoField.Prim (Pvar pvar)
let of_callsite ?obj_path ~ret_typ cs = BoField.Prim (Callsite {ret_typ; cs; obj_path})
let deref ~deref_kind p = BoField.Prim (Deref (deref_kind, p))
let prim_append_field ?typ p0 fn aux depth = function
| Pvar _ | Callsite _ ->
BoField.Field {fn; prefix= p0; typ}
| Deref (_, p) ->
aux ~depth:(depth + 1) p
let prim_append_star_field p0 fn aux = function
| Pvar _ | Callsite _ ->
BoField.StarField {prefix= p0; last_field= fn}
| Deref (_, p) ->
aux p
let append_field = BoField.mk_append_field ~prim_append_field ~prim_append_star_field
let append_star_field = BoField.mk_append_star_field ~prim_append_star_field
type t =
| Normal of partial
@ -122,14 +75,19 @@ module SymbolPath = struct
let modeled p ~is_expensive = Modeled {p; is_expensive}
let is_this = function Pvar pvar -> Pvar.is_this pvar || Pvar.is_self pvar | _ -> false
let is_this = function
| BoField.Prim (Pvar pvar) ->
Pvar.is_this pvar || Pvar.is_self pvar
| _ ->
false
let rec get_pvar = function
| Pvar pvar ->
| BoField.Prim (Pvar pvar) ->
Some pvar
| Deref (_, partial) | Field {prefix= partial} | StarField {prefix= partial} ->
| BoField.(Prim (Deref (_, partial)) | Field {prefix= partial} | StarField {prefix= partial}) ->
get_pvar partial
| Callsite _ ->
| BoField.Prim (Callsite _) ->
None
@ -139,27 +97,27 @@ module SymbolPath = struct
let rec pp_partial_paren ~paren fmt = function
| Pvar pvar ->
| BoField.Prim (Pvar pvar) ->
if Config.bo_debug >= 3 then Pvar.pp_value fmt pvar else Pvar.pp_value_non_verbose fmt pvar
| Deref (Deref_JavaPointer, p) when Config.bo_debug < 3 ->
| BoField.Prim (Deref (Deref_JavaPointer, p)) when Config.bo_debug < 3 ->
pp_partial_paren ~paren fmt p
| Deref (Deref_ArrayIndex, p) ->
| BoField.Prim (Deref (Deref_ArrayIndex, p)) ->
F.fprintf fmt "%a[*]" (pp_partial_paren ~paren:true) p
| Deref ((Deref_COneValuePointer | Deref_CPointer | Deref_JavaPointer), p) ->
| BoField.Prim (Deref ((Deref_COneValuePointer | Deref_CPointer | Deref_JavaPointer), p)) ->
pp_pointer ~paren fmt p
| Field {fn; prefix= Deref ((Deref_COneValuePointer | Deref_CPointer), p)} ->
| BoField.Field {fn; prefix= Prim (Deref ((Deref_COneValuePointer | Deref_CPointer), p))} ->
BufferOverrunField.pp ~pp_lhs:(pp_partial_paren ~paren:true) ~sep:"->" fmt p fn
| Field {fn; prefix= p} ->
| BoField.Field {fn; prefix= p} ->
BufferOverrunField.pp ~pp_lhs:(pp_partial_paren ~paren:true) ~sep:"." fmt p fn
| Callsite {cs; obj_path= Some obj_path} ->
| BoField.Prim (Callsite {cs; obj_path= Some obj_path}) ->
if paren then F.pp_print_string fmt "(" ;
F.fprintf fmt "%a.%a" (pp_partial_paren ~paren:false) obj_path
(Procname.pp_simplified_string ~withclass:false)
(CallSite.pname cs) ;
if paren then F.pp_print_string fmt ")"
| Callsite {cs; obj_path= None} ->
| BoField.Prim (Callsite {cs; obj_path= None}) ->
Procname.pp_simplified_string ~withclass:true fmt (CallSite.pname cs)
| StarField {last_field; prefix} ->
| BoField.StarField {last_field; prefix} ->
BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field
@ -200,54 +158,55 @@ module SymbolPath = struct
let rec represents_multiple_values = function
(* TODO depending on the result, the call might represent multiple values *)
| Callsite _ | Pvar _ ->
| BoField.Prim (Callsite _ | Pvar _) ->
false
| Deref (Deref_ArrayIndex, _) | StarField _ ->
| BoField.Prim (Deref (Deref_ArrayIndex, _)) | BoField.StarField _ ->
true
| Deref (Deref_CPointer, p)
| BoField.Prim (Deref (Deref_CPointer, p))
(* Deref_CPointer is unsound here but avoids many FPs for non-array pointers *)
| Deref ((Deref_COneValuePointer | Deref_JavaPointer), p)
| Field {prefix= p} ->
| BoField.Prim (Deref ((Deref_COneValuePointer | Deref_JavaPointer), p))
| BoField.Field {prefix= p} ->
represents_multiple_values p
let rec represents_multiple_values_sound = function
| Callsite _ | StarField _ ->
| BoField.Prim (Callsite _) | BoField.StarField _ ->
true
| Pvar _ ->
| BoField.Prim (Pvar _) ->
false
| Deref ((Deref_ArrayIndex | Deref_CPointer), _) ->
| BoField.Prim (Deref ((Deref_ArrayIndex | Deref_CPointer), _)) ->
true
| Deref ((Deref_COneValuePointer | Deref_JavaPointer), p) | Field {prefix= p} ->
| BoField.(Prim (Deref ((Deref_COneValuePointer | Deref_JavaPointer), p)) | Field {prefix= p})
->
represents_multiple_values_sound p
let rec represents_callsite_sound_partial = function
| Callsite _ ->
| BoField.Prim (Callsite _) ->
true
| Pvar _ ->
| BoField.Prim (Pvar _) ->
false
| Deref (_, p) | Field {prefix= p} | StarField {prefix= p} ->
| BoField.(Prim (Deref (_, p)) | Field {prefix= p} | StarField {prefix= p}) ->
represents_callsite_sound_partial p
let rec exists_pvar_partial ~f = function
| Pvar pvar ->
| BoField.Prim (Pvar pvar) ->
f pvar
| Deref (_, p) | Field {prefix= p} | StarField {prefix= p} ->
| BoField.(Prim (Deref (_, p)) | Field {prefix= p} | StarField {prefix= p}) ->
exists_pvar_partial ~f p
| Callsite _ ->
| BoField.Prim (Callsite _) ->
false
let rec exists_str_partial ~f = function
| Pvar pvar ->
| BoField.Prim (Pvar pvar) ->
f (Pvar.to_string pvar)
| Deref (_, x) ->
| BoField.Prim (Deref (_, x)) ->
exists_str_partial ~f x
| Field {fn= fld; prefix= x} | StarField {last_field= fld; prefix= x} ->
| BoField.(Field {fn= fld; prefix= x} | StarField {last_field= fld; prefix= x}) ->
f (Fieldname.to_string fld) || exists_str_partial ~f x
| Callsite _ ->
| BoField.Prim (Callsite _) ->
false
@ -264,18 +223,18 @@ module SymbolPath = struct
let is_cpp_vector_elem = function
| Field {fn} ->
| BoField.Field {fn} ->
BufferOverrunField.is_cpp_vector_elem fn
| _ ->
false
let rec is_global_partial = function
| Pvar pvar ->
| BoField.Prim (Pvar pvar) ->
Pvar.is_global pvar
| Deref (_, x) | Field {prefix= x} | StarField {prefix= x} ->
| BoField.(Prim (Deref (_, x)) | Field {prefix= x} | StarField {prefix= x}) ->
is_global_partial x
| Callsite _ ->
| BoField.Prim (Callsite _) ->
false

20
infer/src/bufferoverrun/symb.mli
Unescape View File

@ -18,22 +18,16 @@ module SymbolPath : sig
type deref_kind = Deref_ArrayIndex | Deref_COneValuePointer | Deref_CPointer | Deref_JavaPointer
[@@deriving compare]
type partial = private
type prim =
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of {fn: Fieldname.t; prefix: partial; typ: Typ.t option}
| Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option}
| Callsite of {ret_typ: Typ.t; cs: CallSite.t; obj_path: partial option [@compare.ignore]}
(** [obj_path] represents the varaible name object when a method of which is called at the
[cs] callsite. *)
| StarField of {last_field: Fieldname.t; prefix: partial}
(** Represents a path starting with [prefix] and ending with the field [last_field], the
middle can be anything. Invariants:
- There is at most one StarField
- StarField excluded, there are no duplicate fieldnames
- StarField can only be followed by Deref elements *)
[@@deriving compare]
and partial = prim BufferOverrunField.t [@@deriving compare]
type t = private
| Normal of partial
| Offset of {p: partial; is_void: bool}
@ -55,9 +49,9 @@ module SymbolPath : sig
val deref : deref_kind:deref_kind -> partial -> partial
val field : ?typ:Typ.t -> partial -> Fieldname.t -> partial
val append_field : ?typ:Typ.t -> partial -> Fieldname.t -> partial
val star_field : partial -> Fieldname.t -> partial
val append_star_field : partial -> Fieldname.t -> partial
val normal : partial -> t
@ -88,8 +82,6 @@ module SymbolPath : sig
val is_cpp_vector_elem : partial -> bool
val is_global_partial : partial -> bool
val is_field_depth_beyond_limit : int -> bool
end
module Symbol : sig

4
infer/src/cost/boundMap.ml
Unescape View File

@ -23,9 +23,9 @@ let print_upper_bound_map bound_map =
let filter_loc vars_to_keep = function
| AbsLoc.Loc.Var (Var.LogicalVar _) ->
| BufferOverrunField.Prim (AbsLoc.Loc.Var (Var.LogicalVar _)) ->
None
| AbsLoc.Loc.Var var ->
| BufferOverrunField.Prim (AbsLoc.Loc.Var var) ->
Control.ControlMap.find_opt var vars_to_keep
| _ ->
None

2
infer/src/cost/costDomain.ml
Unescape View File

@ -13,7 +13,7 @@ module BasicCost = struct
(* NOTE: Increment the version number if you changed the [t] type. This is for avoiding
demarshalling failure of cost analysis results in running infer-reportdiff. *)
let version = 5
let version = 6
end
(** Module to simulate a record

2
infer/src/cost/costModels.ml
Unescape View File

@ -54,7 +54,7 @@ module IntHashMap = struct
| Singleton this_loc -> (
match (AbsLoc.Loc.get_path this_loc, Typ.strip_ptr typ |> Typ.name) with
| Some path, Some typ_name ->
let path = Symb.SymbolPath.field path (Fieldname.make typ_name "size") in
let path = Symb.SymbolPath.append_field path (Fieldname.make typ_name "size") in
let itv = Itv.of_normal_path ~unsigned:true path in
CostUtils.of_itv ~itv ~degree_kind:Linear ~of_function:"IntHashMap.keys" location
| _, _ ->

Write Preview
Loading…
Cancel
Save