[inferbo] Move OndemandEnv to its own file

Reviewed By: jvillard

Differential Revision: D13449603

fbshipit-source-id: a253ef70b
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 52e09aed13
commit bb1a19b6f9

@ -12,6 +12,7 @@ open AbsLoc
open! AbstractDomain.Types
module F = Format
module L = Logging
module OndemandEnv = BufferOverrunOndemandEnv
module Relation = BufferOverrunDomainRelation
module SPath = Symb.SymbolPath
module Trace = BufferOverrunTrace
@ -22,90 +23,6 @@ type eval_sym_trace =
; trace_of_sym: Symb.Symbol.t -> Trace.Set.t
; eval_locpath: PowLoc.eval_locpath }
module OndemandEnv = struct
module FormalTyps = Caml.Map.Make (Pvar)
type t =
{ typ_of_param_path: SPath.partial -> Typ.t option
; may_last_field: SPath.partial -> bool
; entry_location: Location.t
; integer_type_widths: Typ.IntegerWidths.t }
let mk pdesc =
let formal_typs =
List.fold (Procdesc.get_pvar_formals pdesc) ~init:FormalTyps.empty
~f:(fun acc (formal, typ) -> FormalTyps.add formal typ acc )
in
fun tenv integer_type_widths ->
let rec typ_of_param_path = function
| SPath.Pvar x ->
FormalTyps.find_opt x formal_typs
| SPath.Deref (_, x) ->
Option.map (typ_of_param_path x) ~f:(fun typ ->
match typ.Typ.desc with
| Tptr (typ, _) ->
typ
| Tarray {elt} ->
elt
| Tvoid ->
Typ.void
| _ ->
L.(die InternalError) "Untyped expression is given." )
| SPath.Field (fn, x) ->
let lookup = Tenv.lookup tenv in
Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn)
| SPath.Callsite {ret_typ} ->
Some ret_typ
in
let is_last_field fn (fields : Typ.Struct.field list) =
Option.value_map (List.last fields) ~default:false ~f:(fun (last_fn, _, _) ->
Typ.Fieldname.equal fn last_fn )
in
let rec may_last_field = function
| SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ ->
true
| SPath.Field (fn, 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
| Tstruct typename ->
let opt_struct = Tenv.lookup tenv typename in
Option.value_map opt_struct ~default:false ~f:(fun str ->
is_last_field fn str.Typ.Struct.fields )
| _ ->
true )
in
let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in
{typ_of_param_path; may_last_field; entry_location; integer_type_widths}
let canonical_path typ_of_param_path path =
let module KnownFields = Caml.Map.Make (struct
type t = Typ.t option * Typ.Fieldname.t [@@deriving compare]
end) in
let rec helper path =
match path with
| SPath.Pvar _ | SPath.Callsite _ ->
(None, KnownFields.empty)
| SPath.Deref (deref_kind, ptr) ->
let ptr_opt, known_fields = helper ptr in
(Option.map ptr_opt ~f:(fun ptr -> SPath.deref ~deref_kind ptr), known_fields)
| SPath.Field (fn, struct_path) -> (
let struct_path_opt, known_fields = helper struct_path in
let key = (typ_of_param_path (Option.value ~default:struct_path struct_path_opt), fn) in
match KnownFields.find_opt key known_fields with
| Some _ as canonicalized ->
(canonicalized, known_fields)
| None ->
let field_path =
Option.value_map struct_path_opt ~default:path ~f:(fun struct_path ->
SPath.field struct_path fn )
in
(None, KnownFields.add key field_path known_fields) )
in
Option.value (helper path |> fst) ~default:path
end
module Val = struct
type t =
{ itv: Itv.t

@ -0,0 +1,91 @@
(*
* 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 L = Logging
module SPath = Symb.SymbolPath
module FormalTyps = Caml.Map.Make (Pvar)
type t =
{ typ_of_param_path: SPath.partial -> Typ.t option
; may_last_field: SPath.partial -> bool
; entry_location: Location.t
; integer_type_widths: Typ.IntegerWidths.t }
let mk pdesc =
let formal_typs =
List.fold (Procdesc.get_pvar_formals pdesc) ~init:FormalTyps.empty ~f:(fun acc (formal, typ) ->
FormalTyps.add formal typ acc )
in
fun tenv integer_type_widths ->
let rec typ_of_param_path = function
| SPath.Pvar x ->
FormalTyps.find_opt x formal_typs
| SPath.Deref (_, x) ->
Option.map (typ_of_param_path x) ~f:(fun typ ->
match typ.Typ.desc with
| Tptr (typ, _) ->
typ
| Tarray {elt} ->
elt
| Tvoid ->
Typ.void
| _ ->
L.(die InternalError) "Untyped expression is given." )
| SPath.Field (fn, x) ->
let lookup = Tenv.lookup tenv in
Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn)
| SPath.Callsite {ret_typ} ->
Some ret_typ
in
let is_last_field fn (fields : Typ.Struct.field list) =
Option.value_map (List.last fields) ~default:false ~f:(fun (last_fn, _, _) ->
Typ.Fieldname.equal fn last_fn )
in
let rec may_last_field = function
| SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ ->
true
| SPath.Field (fn, 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
| Tstruct typename ->
let opt_struct = Tenv.lookup tenv typename in
Option.value_map opt_struct ~default:false ~f:(fun str ->
is_last_field fn str.Typ.Struct.fields )
| _ ->
true )
in
let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in
{typ_of_param_path; may_last_field; entry_location; integer_type_widths}
let canonical_path typ_of_param_path path =
let module KnownFields = Caml.Map.Make (struct
type t = Typ.t option * Typ.Fieldname.t [@@deriving compare]
end) in
let rec helper path =
match path with
| SPath.Pvar _ | SPath.Callsite _ ->
(None, KnownFields.empty)
| SPath.Deref (deref_kind, ptr) ->
let ptr_opt, known_fields = helper ptr in
(Option.map ptr_opt ~f:(fun ptr -> SPath.deref ~deref_kind ptr), known_fields)
| SPath.Field (fn, struct_path) -> (
let struct_path_opt, known_fields = helper struct_path in
let key = (typ_of_param_path (Option.value ~default:struct_path struct_path_opt), fn) in
match KnownFields.find_opt key known_fields with
| Some _ as canonicalized ->
(canonicalized, known_fields)
| None ->
let field_path =
Option.value_map struct_path_opt ~default:path ~f:(fun struct_path ->
SPath.field struct_path fn )
in
(None, KnownFields.add key field_path known_fields) )
in
Option.value (helper path |> fst) ~default:path
Loading…
Cancel
Save