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

[IR] add API for Sil and Exp.FreeVar

Browse Source 
Summary:
`Sequence` API to walk over free variables in expressions, instead of computing lists with uniqueness constraints that make them have linear complexity for insertion.

Switch to a Set representation when we don't care about the order of elements,
otherwise to a `Hash_queue`:
https://ocaml.janestreet.com/ocaml-core/113.33/doc/core/Std/Hash_queue.mod/S.modt/

Often, we don't even need to compute the sequence of free variables, as we are
just testing membership/emptiness/...

Reviewed By: mbouaziz

Differential Revision: D7099294

fbshipit-source-id: e96f84b
master
Jules Villard 7 years ago committed by Facebook Github Bot
parent 6bacdf4a4d
commit bc7a71d413
27 changed files with 528 additions and 609 deletions
Show Stats Download Patch File Download Diff File

33
infer/src/IR/Exp.ml
Unescape View File

@ -292,6 +292,31 @@ let is_objc_block_closure = function
false
let rec gen_free_vars =
let open Sequence.Generator in
function
| Var id ->
yield id
| Cast (_, e)
| Exn e
| Lfield (e, _, _)
(* do nothing since we only count non-program variables *)
| UnOp (_, e, _) ->
gen_free_vars e
| Closure {captured_vars} ->
ISequence.gen_sequence_list captured_vars ~f:(fun (e, _, _) -> gen_free_vars e)
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _)
| Lvar _
| Sizeof _ (* TODO: Sizeof length expressions may contain variables, do not ignore them. *) ->
return ()
| BinOp (_, e1, e2) | Lindex (e1, e2) ->
gen_free_vars e1 >>= fun () -> gen_free_vars e2
let free_vars e = Sequence.Generator.run (gen_free_vars e)
let ident_mem e id = free_vars e |> Sequence.exists ~f:(Ident.equal id)
let rec gen_program_vars =
let open Sequence.Generator in
function
@ -304,13 +329,7 @@ let rec gen_program_vars =
| BinOp (_, e1, e2) | Lindex (e1, e2) ->
gen_program_vars e1 >>= fun () -> gen_program_vars e2
| Closure {captured_vars} ->
let rec aux = function
| (_, p, _) :: tl ->
yield p >>= fun () -> aux tl
| [] ->
return ()
in
aux captured_vars
ISequence.gen_sequence_list captured_vars ~f:(fun (_, p, _) -> yield p)
let program_vars e = Sequence.Generator.run (gen_program_vars e)

8
infer/src/IR/Exp.mli
Unescape View File

@ -119,6 +119,14 @@ val lt : t -> t -> t
val get_vars : t -> Ident.t list * Pvar.t list
(** Extract the ids and pvars from an expression *)
val free_vars : t -> Ident.t Sequence.t
(** all the idents appearing in the expression *)
val gen_free_vars : t -> (unit, Ident.t) Sequence.Generator.t
val ident_mem : t -> Ident.t -> bool
(** true if the identifier appears in the expression *)
val program_vars : t -> Pvar.t Sequence.t
(** all the program variables appearing in the expression *)

20
infer/src/IR/Ident.ml
Unescape View File

@ -236,3 +236,23 @@ let pp f id = F.fprintf f "%s" (to_string id)
(** pretty printer for lists of identifiers *)
let pp_list = Pp.comma_seq pp
module HashQueue = Hash_queue.Make (struct
type nonrec t = t
let compare = compare
let hash = Hashtbl.hash
let sexp_of_t id = Sexp.of_string (to_string id)
end)
let hashqueue_of_sequence ?init s =
let q = match init with None -> HashQueue.create () | Some q0 -> q0 in
Sequence.iter s ~f:(fun id ->
let _ : [`Key_already_present | `Ok] = HashQueue.enqueue q id () in
() ) ;
q
let set_of_sequence ?(init= Set.empty) s = Sequence.fold s ~init ~f:(fun ids id -> Set.add id ids)

6
infer/src/IR/Ident.mli
Unescape View File

@ -39,6 +39,8 @@ module Hash : Caml.Hashtbl.S with type key = t
(** Map with ident as key. *)
module Map : Caml.Map.S with type key = t
module HashQueue : Hash_queue.S with type Key.t = t
module NameGenerator : sig
type t
@ -134,3 +136,7 @@ val to_string : t -> string
val pp_list : Format.formatter -> t list -> unit
(** Pretty print a list of identifiers. *)
val hashqueue_of_sequence : ?init:unit HashQueue.t -> t Sequence.t -> unit HashQueue.t
val set_of_sequence : ?init:Set.t -> t Sequence.t -> Set.t

241
infer/src/IR/Sil.ml
Unescape View File

@ -1015,144 +1015,61 @@ let hpred_entries hpred = hpred_get_lexp [] hpred
(** {2 Functions for computing free non-program variables} *)
(** Type of free variables. These include primed, normal and footprint variables.
We keep a count of how many types the variables appear. *)
type fav = Ident.t list ref
let fav_new () = ref []
(** Emptyness check. *)
let fav_is_empty fav = match !fav with [] -> true | _ -> false
(** Check whether a predicate holds for all elements. *)
let fav_for_all fav predicate = List.for_all ~f:predicate !fav
(** Check whether a predicate holds for some elements. *)
let fav_exists fav predicate = List.exists ~f:predicate !fav
(** flag to indicate whether fav's are stored in duplicate form.
Only to be used with fav_to_list *)
let fav_duplicates = ref false
(** extend [fav] with a [id] *)
let ( ++ ) fav id =
if !fav_duplicates || not (List.exists ~f:(Ident.equal id) !fav) then fav := id :: !fav
(** extend [fav] with ident list [idl] *)
let ( +++ ) fav idl = List.iter ~f:(fun id -> fav ++ id) idl
(** add identity lists to fav *)
let ident_list_fav_add idl fav = fav +++ idl
(** Convert a list to a fav. *)
let fav_from_list l =
let fav = fav_new () in
let _ = List.iter ~f:(fun id -> fav ++ id) l in
fav
(** Convert a [fav] to a list of identifiers while preserving the order
that the identifiers were added to [fav]. *)
let fav_to_list fav = List.rev !fav
(** Pretty print a fav. *)
let pp_fav f fav = Pp.seq Ident.pp f (fav_to_list fav)
(** Turn a xxx_fav_add function into a xxx_fav function *)
let fav_imperative_to_functional f x =
let fav = fav_new () in
let _ = f fav x in
fav
(** [fav_filter_ident fav f] only keeps [id] if [f id] is true. *)
let fav_filter_ident fav filter = fav := List.filter ~f:filter !fav
(** Like [fav_filter_ident] but return a copy. *)
let fav_copy_filter_ident fav filter = ref (List.filter ~f:filter !fav)
let fav_mem fav id = List.exists ~f:(Ident.equal id) !fav
let rec exp_fav_add fav e =
match (e : Exp.t) with
| Var id ->
fav ++ id
| Exn e ->
exp_fav_add fav e
| Closure {captured_vars} ->
List.iter ~f:(fun (e, _, _) -> exp_fav_add fav e) captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _) ->
()
| Cast (_, e) | UnOp (_, e, _) ->
exp_fav_add fav e
| BinOp (_, e1, e2) ->
exp_fav_add fav e1 ; exp_fav_add fav e2
| Lvar _ ->
()
| Lfield (e, _, _) (* do nothing since we only count non-program variables *) ->
exp_fav_add fav e
| Lindex (e1, e2) ->
exp_fav_add fav e1 ; exp_fav_add fav e2
(* TODO: Sizeof length expressions may contain variables, do not ignore them. *)
| Sizeof _ ->
()
let exp_fav = fav_imperative_to_functional exp_fav_add
let exp_fav_list e = fav_to_list (exp_fav e)
let ident_in_exp id e =
let fav = fav_new () in
exp_fav_add fav e ; fav_mem fav id
let atom_fav_add fav = function
| Aeq (e1, e2) | Aneq (e1, e2) ->
exp_fav_add fav e1 ; exp_fav_add fav e2
| Apred (_, es) | Anpred (_, es) ->
List.iter ~f:(fun e -> exp_fav_add fav e) es
let atom_fav = fav_imperative_to_functional atom_fav_add
let rec strexp_fav_add fav = function
| Eexp (e, _) ->
exp_fav_add fav e
| Estruct (fld_se_list, _) ->
List.iter ~f:(fun (_, se) -> strexp_fav_add fav se) fld_se_list
| Earray (len, idx_se_list, _) ->
exp_fav_add fav len ;
List.iter ~f:(fun (e, se) -> exp_fav_add fav e ; strexp_fav_add fav se) idx_se_list
let hpred_fav_add fav = function
| Hpointsto (base, sexp, te) ->
exp_fav_add fav base ; strexp_fav_add fav sexp ; exp_fav_add fav te
| Hlseg (_, _, e1, e2, elist) ->
exp_fav_add fav e1 ;
exp_fav_add fav e2 ;
List.iter ~f:(exp_fav_add fav) elist
| Hdllseg (_, _, e1, e2, e3, e4, elist) ->
exp_fav_add fav e1 ;
exp_fav_add fav e2 ;
exp_fav_add fav e3 ;
exp_fav_add fav e4 ;
List.iter ~f:(exp_fav_add fav) elist
let atom_gen_free_vars =
let open Sequence.Generator in
function
| Aeq (e1, e2) | Aneq (e1, e2) ->
Exp.gen_free_vars e1 >>= fun () -> Exp.gen_free_vars e2
| Apred (_, es) | Anpred (_, es) ->
ISequence.gen_sequence_list es ~f:Exp.gen_free_vars
let hpred_fav = fav_imperative_to_functional hpred_fav_add
let atom_free_vars a = Sequence.Generator.run (atom_gen_free_vars a)
(** This function should be used before adding a new
index to Earray. The [exp] is the newly created
index. This function "cleans" [exp] according to whether it is
the footprint or current part of the prop.
The function faults in the re - execution mode, as an internal check of the tool. *)
let rec strexp_gen_free_vars =
let open Sequence.Generator in
function
| Eexp (e, _) ->
Exp.gen_free_vars e
| Estruct (fld_se_list, _) ->
ISequence.gen_sequence_list fld_se_list ~f:(fun (_, se) -> strexp_gen_free_vars se)
| Earray (len, idx_se_list, _) ->
Exp.gen_free_vars len
>>= fun () ->
ISequence.gen_sequence_list idx_se_list ~f:(fun (e, se) ->
Exp.gen_free_vars e >>= fun () -> strexp_gen_free_vars se )
let hpred_gen_free_vars =
let open Sequence.Generator in
function
| Hpointsto (base, sexp, te) ->
Exp.gen_free_vars base
>>= fun () -> strexp_gen_free_vars sexp >>= fun () -> Exp.gen_free_vars te
| Hlseg (_, _, e1, e2, elist) ->
Exp.gen_free_vars e1
>>= fun () ->
Exp.gen_free_vars e2 >>= fun () -> ISequence.gen_sequence_list elist ~f:Exp.gen_free_vars
| Hdllseg (_, _, e1, e2, e3, e4, elist) ->
Exp.gen_free_vars e1
>>= fun () ->
Exp.gen_free_vars e2
>>= fun () ->
Exp.gen_free_vars e3
>>= fun () ->
Exp.gen_free_vars e4 >>= fun () -> ISequence.gen_sequence_list elist ~f:Exp.gen_free_vars
let hpred_free_vars h = Sequence.Generator.run (hpred_gen_free_vars h)
(** This function should be used before adding a new index to Earray. The [exp] is the newly created
index. This function "cleans" [exp] according to whether it is the footprint or current part of
the prop. The function faults in the re - execution mode, as an internal check of the tool. *)
let array_clean_new_index footprint_part new_idx =
if footprint_part && not !Config.footprint then assert false ;
let fav = exp_fav new_idx in
if footprint_part && fav_exists fav (fun id -> not (Ident.is_footprint id)) then (
assert (not (footprint_part && not !Config.footprint)) ;
if footprint_part
&& Exp.free_vars new_idx |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id))
then (
L.d_warning
( "Array index " ^ Exp.to_string new_idx
^ " has non-footprint vars: replaced by fresh footprint var" ) ;
@ -1164,28 +1081,37 @@ let array_clean_new_index footprint_part new_idx =
(** {2 Functions for computing all free or bound non-program variables} *)
let hpara_shallow_av_add fav para =
List.iter ~f:(hpred_fav_add fav) para.body ;
fav ++ para.root ;
fav ++ para.next ;
fav +++ para.svars ;
fav +++ para.evars
(** Variables in hpara, excluding bound vars in the body *)
let hpara_shallow_gen_free_vars {body; root; next; svars; evars} =
let open Sequence.Generator in
ISequence.gen_sequence_list ~f:hpred_gen_free_vars body
>>= fun () ->
yield root
>>= fun () ->
yield next
>>= fun () ->
ISequence.gen_sequence_list ~f:yield svars
>>= fun () -> ISequence.gen_sequence_list ~f:yield evars
let hpara_dll_shallow_av_add fav para =
List.iter ~f:(hpred_fav_add fav) para.body_dll ;
fav ++ para.cell ;
fav ++ para.blink ;
fav ++ para.flink ;
fav +++ para.svars_dll ;
fav +++ para.evars_dll
(** Variables in hpara, excluding bound vars in the body *)
let hpara_shallow_av = fav_imperative_to_functional hpara_shallow_av_add
let hpara_shallow_free_vars h = Sequence.Generator.run (hpara_shallow_gen_free_vars h)
(** Variables in hpara_dll, excluding bound vars in the body *)
let hpara_dll_shallow_av = fav_imperative_to_functional hpara_dll_shallow_av_add
let hpara_dll_shallow_gen_free_vars {body_dll; cell; blink; flink; svars_dll; evars_dll} =
let open Sequence.Generator in
ISequence.gen_sequence_list ~f:hpred_gen_free_vars body_dll
>>= fun () ->
yield cell
>>= fun () ->
yield blink
>>= fun () ->
yield flink
>>= fun () ->
ISequence.gen_sequence_list ~f:yield svars_dll
>>= fun () -> ISequence.gen_sequence_list ~f:yield evars_dll
let hpara_dll_shallow_free_vars h = Sequence.Generator.run (hpara_dll_shallow_gen_free_vars h)
(** {2 Functions for Substitution} *)
@ -1200,7 +1126,6 @@ type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare]
type subst_fun = [`Exp of Ident.t -> Exp.t | `Typ of (Typ.t -> Typ.t) * (Typ.Name.t -> Typ.Name.t)]
(** Equality for substitutions. *)
let equal_exp_subst = [%compare.equal : exp_subst]
let sub_no_duplicated_ids sub = not (List.contains_dup ~compare:compare_ident_exp_ids sub)
@ -1308,11 +1233,13 @@ let extend_sub sub id exp : exp_subst option =
if mem_sub id sub then None else Some (List.merge ~cmp:compare sub [(id, exp)])
(** Free auxilary variables in the domain and range of the
substitution. *)
let sub_fav_add fav (sub: exp_subst) =
List.iter ~f:(fun (id, e) -> fav ++ id ; exp_fav_add fav e) sub
(** Free auxilary variables in the domain and range of the substitution. *)
let exp_subst_gen_free_vars sub =
let open Sequence.Generator in
ISequence.gen_sequence_list sub ~f:(fun (id, e) -> yield id >>= fun () -> Exp.gen_free_vars e)
let exp_subst_free_vars sub = Sequence.Generator.run (exp_subst_gen_free_vars sub)
let rec exp_sub_ids (f: subst_fun) exp =
let f_typ x = match f with `Exp _ -> x | `Typ (f, _) -> f x in

79
infer/src/IR/Sil.mli
Unescape View File

@ -405,81 +405,22 @@ val hpred_list_get_lexps : (Exp.t -> bool) -> hpred list -> Exp.t list
val hpred_entries : hpred -> Exp.t list
(** {2 Function for computing lexps in sigma} *)
val atom_free_vars : atom -> Ident.t Sequence.t
(** Type of free variables. These include primed, normal and footprint variables.
We remember the order in which variables are added. *)
type fav
val atom_gen_free_vars : atom -> (unit, Ident.t) Sequence.Generator.t
val fav_duplicates : bool ref
(** flag to indicate whether fav's are stored in duplicate form.
Only to be used with fav_to_list *)
val hpred_free_vars : hpred -> Ident.t Sequence.t
val pp_fav : F.formatter -> fav -> unit [@@warning "-32"]
(** Pretty print a fav. *)
val hpred_gen_free_vars : hpred -> (unit, Ident.t) Sequence.Generator.t
val fav_new : unit -> fav
(** Create a new [fav]. *)
val hpara_shallow_free_vars : hpara -> Ident.t Sequence.t
val fav_is_empty : fav -> bool
(** Emptyness check. *)
val fav_for_all : fav -> (Ident.t -> bool) -> bool
(** Check whether a predicate holds for all elements. *)
val fav_exists : fav -> (Ident.t -> bool) -> bool
(** Check whether a predicate holds for some elements. *)
val fav_mem : fav -> Ident.t -> bool
(** Membership test fot [fav] *)
val fav_from_list : Ident.t list -> fav
(** Convert a list to a fav. *)
val fav_to_list : fav -> Ident.t list
(** Convert a [fav] to a list of identifiers while preserving the order
that identifiers were added to [fav]. *)
val fav_imperative_to_functional : (fav -> 'a -> unit) -> 'a -> fav
(** Turn a xxx_fav_add function into a xxx_fav function *)
val fav_filter_ident : fav -> (Ident.t -> bool) -> unit
(** [fav_filter_ident fav f] only keeps [id] if [f id] is true. *)
val fav_copy_filter_ident : fav -> (Ident.t -> bool) -> fav
(** Like [fav_filter_ident] but return a copy. *)
val ident_list_fav_add : Ident.t list -> fav -> unit
(** add identifier list to fav *)
val exp_fav_add : fav -> Exp.t -> unit
(** [exp_fav_add fav exp] extends [fav] with the free variables of [exp] *)
val exp_fav : Exp.t -> fav
val exp_fav_list : Exp.t -> Ident.t list
val ident_in_exp : Ident.t -> Exp.t -> bool
val strexp_fav_add : fav -> strexp -> unit
val atom_fav_add : fav -> atom -> unit
val atom_fav : atom -> fav
val hpred_fav_add : fav -> hpred -> unit
val hpred_fav : hpred -> fav
val hpara_shallow_av : hpara -> fav
(** Variables in hpara, excluding bound vars in the body *)
val hpara_dll_shallow_av : hpara_dll -> fav
val hpara_dll_shallow_free_vars : hpara_dll -> Ident.t Sequence.t
(** Variables in hpara_dll, excluding bound vars in the body *)
(** {2 Substitution} *)
type exp_subst [@@deriving compare]
type exp_subst = private (Ident.t * Exp.t) list [@@deriving compare]
type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare]
@ -557,9 +498,9 @@ val sub_map : (Ident.t -> Ident.t) -> (Exp.t -> Exp.t) -> exp_subst -> exp_subst
val extend_sub : exp_subst -> Ident.t -> Exp.t -> exp_subst option
(** Extend substitution and return [None] if not possible. *)
val sub_fav_add : fav -> exp_subst -> unit
(** Free auxilary variables in the domain and range of the
substitution. *)
val exp_subst_free_vars : exp_subst -> Ident.t Sequence.t
val exp_subst_gen_free_vars : exp_subst -> (unit, Ident.t) Sequence.Generator.t
(** substitution functions
WARNING: these functions do not ensure that the results are normalized. *)

4
infer/src/backend/Attribute.ml
Unescape View File

@ -324,12 +324,12 @@ let deallocate_stack_vars tenv (p: 'a Prop.t) pvars =
in
let p'' =
let res = ref p' in
let p'_fav = Prop.prop_fav p' in
let p'_fav = Prop.free_vars p' |> Ident.set_of_sequence in
let do_var (v, freshv) =
(* static locals are not stack-allocated *)
if not (Pvar.is_static_local v) then
(* the address of a de-allocated stack var in in the post *)
if Sil.fav_mem p'_fav freshv then (
if Ident.Set.mem freshv p'_fav then (
stack_vars_address_in_post := v :: !stack_vars_address_in_post ;
let pred = Sil.Apred (Adangling DAaddr_stack_var, [Exp.Var freshv]) in
res := add_or_replace tenv !res pred )

4
infer/src/backend/BuiltinDefn.ml
Unescape View File

@ -195,7 +195,9 @@ let create_type tenv n_lexp typ prop =
let sigma_fp = prop.Prop.sigma_fp in
let prop' = Prop.set prop ~sigma:(hpred :: sigma) in
let prop'' =
let has_normal_variables = Sil.fav_exists (Sil.exp_fav n_lexp) Ident.is_normal in
let has_normal_variables =
Exp.free_vars n_lexp |> Sequence.exists ~f:Ident.is_normal
in
if is_undefined_opt tenv prop n_lexp || has_normal_variables then prop'
else Prop.set prop' ~sigma_fp:(hpred :: sigma_fp)
in

89
infer/src/backend/abs.ml
Unescape View File

@ -40,12 +40,6 @@ let sigma_rewrite tenv p r : Prop.normal Prop.t option =
Some (Prop.normalize tenv p_new)
let sigma_fav_list sigma = Sil.fav_to_list (Prop.sigma_fav sigma)
let sigma_fav_in_pvars = Sil.fav_imperative_to_functional Prop.sigma_fav_in_pvars_add
let sigma_fav_in_pvars_list sigma = Sil.fav_to_list (sigma_fav_in_pvars sigma)
(******************** Start of SLL abstraction rules *****************)
let create_fresh_primeds_ls para =
let id_base = Ident.create_fresh Ident.kprimed in
@ -76,24 +70,30 @@ let create_condition_ls ids_private id_base p_leftover (inst: Sil.exp_subst) =
let insts_of_private_ids = Sil.sub_range inst_private in
(insts_of_private_ids, insts_of_public_ids, inst_of_base)
in
let fav_insts_of_public_ids = List.concat_map ~f:Sil.exp_fav_list insts_of_public_ids in
let fav_insts_of_private_ids = List.concat_map ~f:Sil.exp_fav_list insts_of_private_ids in
let fav_p_leftover, _ =
let sigma = p_leftover.Prop.sigma in
(sigma_fav_list sigma, sigma_fav_in_pvars_list sigma)
in
(*
let fav_inst_of_base = Sil.exp_fav_list inst_of_base in
L.out "@[.... application of condition ....@\n@.";
L.out "@[<4> private ids : %a@\n@." pp_exp_list insts_of_private_ids;
L.out "@[<4> public ids : %a@\n@." pp_exp_list insts_of_public_ids;
*)
(* (not (IList.intersect compare fav_inst_of_base fav_in_pvars)) && *)
Exp.program_vars inst_of_base |> Sequence.is_empty
&& List.for_all ~f:(fun e -> Exp.program_vars e |> Sequence.is_empty) insts_of_private_ids
&& not (List.exists ~f:Ident.is_normal fav_insts_of_private_ids)
&& not (IList.intersect Ident.compare fav_insts_of_private_ids fav_p_leftover)
&& not (IList.intersect Ident.compare fav_insts_of_private_ids fav_insts_of_public_ids)
&&
let fav_insts_of_private_ids =
Sequence.of_list insts_of_private_ids |> Sequence.concat_map ~f:Exp.free_vars
|> Sequence.memoize
in
not (Sequence.exists fav_insts_of_private_ids ~f:Ident.is_normal)
&&
let fav_insts_of_private_ids = Ident.set_of_sequence fav_insts_of_private_ids in
let intersects_fav_insts_of_private_ids s =
Sequence.exists s ~f:(fun id -> Ident.Set.mem id fav_insts_of_private_ids)
in
(* [fav_insts_of_private_ids] does not intersect the free vars in [p_leftover.sigma] *)
Prop.sigma_free_vars p_leftover.Prop.sigma |> Fn.non intersects_fav_insts_of_private_ids
&& (* [fav_insts_of_private_ids] does not intersect the free vars in [insts_of_public_ids] *)
List.for_all insts_of_public_ids ~f:(fun e ->
Exp.free_vars e |> Fn.non intersects_fav_insts_of_private_ids )
let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) =
@ -860,15 +860,15 @@ let abstract_pure_part tenv p ~(from_abstract_footprint: bool) =
let do_pure pure =
let pi_filtered =
let sigma = p.Prop.sigma in
let fav_sigma = Prop.sigma_fav sigma in
let fav_nonpure = Prop.prop_fav_nonpure p in
let fav_sigma = Prop.sigma_free_vars sigma |> Ident.set_of_sequence in
let fav_nonpure = Prop.non_pure_free_vars p |> Ident.set_of_sequence in
(* vars in current and footprint sigma *)
let filter atom =
let fav' = Sil.atom_fav atom in
Sil.fav_for_all fav' (fun id ->
if Ident.is_primed id then Sil.fav_mem fav_sigma id
else if Ident.is_footprint id then Sil.fav_mem fav_nonpure id
else true )
Sil.atom_free_vars atom
|> Sequence.for_all ~f:(fun id ->
if Ident.is_primed id then Ident.Set.mem id fav_sigma
else if Ident.is_footprint id then Ident.Set.mem id fav_nonpure
else true )
in
List.filter ~f:filter pure
in
@ -908,27 +908,20 @@ let abstract_pure_part tenv p ~(from_abstract_footprint: bool) =
let abstract_gc tenv p =
let pi = p.Prop.pi in
let p_without_pi = Prop.normalize tenv (Prop.set p ~pi:[]) in
let fav_p_without_pi = Prop.prop_fav p_without_pi in
let fav_p_without_pi = Prop.free_vars p_without_pi |> Ident.set_of_sequence in
(* let weak_filter atom =
let fav_atom = atom_fav atom in
IList.intersect compare fav_p_without_pi fav_atom in *)
let check fav_seq =
Sequence.is_empty fav_seq
|| (* non-empty intersection with [fav_p_without_pi] *)
Sequence.exists fav_seq ~f:(fun id -> Ident.Set.mem id fav_p_without_pi)
in
let strong_filter = function
| Sil.Aeq (e1, e2) | Sil.Aneq (e1, e2) ->
let fav_e1 = Sil.exp_fav e1 in
let fav_e2 = Sil.exp_fav e2 in
let intersect_e1 _ =
IList.intersect Ident.compare (Sil.fav_to_list fav_e1) (Sil.fav_to_list fav_p_without_pi)
in
let intersect_e2 _ =
IList.intersect Ident.compare (Sil.fav_to_list fav_e2) (Sil.fav_to_list fav_p_without_pi)
in
let no_fav_e1 = Sil.fav_is_empty fav_e1 in
let no_fav_e2 = Sil.fav_is_empty fav_e2 in
(no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ())
check (Exp.free_vars e1) && check (Exp.free_vars e2)
| (Sil.Apred _ | Anpred _) as a ->
let fav_a = Sil.atom_fav a in
Sil.fav_is_empty fav_a
|| IList.intersect Ident.compare (Sil.fav_to_list fav_a) (Sil.fav_to_list fav_p_without_pi)
check (Sil.atom_free_vars a)
in
let new_pi = List.filter ~f:strong_filter pi in
let prop = Prop.normalize tenv (Prop.set p ~pi:new_pi) in
@ -950,11 +943,10 @@ end)
(** find the id's in sigma reachable from the given roots *)
let sigma_reachable root_fav sigma =
let fav_to_set fav = Ident.idlist_to_idset (Sil.fav_to_list fav) in
let reach_set = ref (fav_to_set root_fav) in
let reach_set = ref root_fav in
let edges = ref [] in
let do_hpred hpred =
let hp_fav_set = fav_to_set (Sil.hpred_fav hpred) in
let hp_fav_set = Sil.hpred_free_vars hpred |> Ident.set_of_sequence in
let add_entry e = edges := (e, hp_fav_set) :: !edges in
List.iter ~f:add_entry (Sil.hpred_entries hpred)
in
@ -1012,9 +1004,6 @@ let check_observer_is_unsubscribed_deallocation tenv prop e =
let check_junk ?original_prop pname tenv prop =
let fav_sub_sigmafp = Sil.fav_new () in
Sil.sub_fav_add fav_sub_sigmafp prop.Prop.sub ;
Prop.sigma_fav_add fav_sub_sigmafp prop.Prop.sigma_fp ;
let leaks_reported = ref [] in
let remove_junk_once fp_part fav_root sigma =
let id_considered_reachable =
@ -1025,7 +1014,7 @@ let check_junk ?original_prop pname tenv prop =
let should_remove_hpred entries =
let predicate = function
| Exp.Var id ->
(Ident.is_primed id || Ident.is_footprint id) && not (Sil.fav_mem fav_root id)
(Ident.is_primed id || Ident.is_footprint id) && not (Ident.Set.mem id fav_root)
&& not (id_considered_reachable id)
| _ ->
false
@ -1169,8 +1158,14 @@ let check_junk ?original_prop pname tenv prop =
if Int.equal (List.length sigma') (List.length sigma) then sigma'
else remove_junk fp_part fav_root sigma'
in
let sigma_new = remove_junk false fav_sub_sigmafp prop.Prop.sigma in
let sigma_fp_new = remove_junk true (Sil.fav_new ()) prop.Prop.sigma_fp in
let sigma_new =
let fav_sub = Sil.exp_subst_free_vars prop.Prop.sub |> Ident.set_of_sequence in
let fav_sub_sigmafp =
Prop.sigma_free_vars prop.Prop.sigma_fp |> Ident.set_of_sequence ~init:fav_sub
in
remove_junk false fav_sub_sigmafp prop.Prop.sigma
in
let sigma_fp_new = remove_junk true Ident.Set.empty prop.Prop.sigma_fp in
if Prop.equal_sigma prop.Prop.sigma sigma_new && Prop.equal_sigma prop.Prop.sigma_fp sigma_fp_new
then prop
else Prop.normalize tenv (Prop.set prop ~sigma:sigma_new ~sigma_fp:sigma_fp_new)

30
infer/src/backend/absarray.ml
Unescape View File

@ -586,7 +586,7 @@ let check_after_array_abstraction tenv prop =
if !Config.footprint then
let path = StrexpMatch.path_from_exp_offsets root offs in
index_is_pointed_to tenv prop path ind
else not (Sil.fav_exists (Sil.exp_fav ind) Ident.is_primed)
else not (Exp.free_vars ind |> Sequence.exists ~f:Ident.is_primed)
in
let rec check_se root offs typ = function
| Sil.Eexp _ ->
@ -631,21 +631,19 @@ let remove_redundant_elements tenv prop =
Prop.d_prop prop ;
L.d_ln () ;
let occurs_at_most_once : Ident.t -> bool =
(* the variable occurs at most once in the footprint or current part *)
let fav_curr = Sil.fav_new () in
let fav_foot = Sil.fav_new () in
Sil.fav_duplicates := true ;
Sil.sub_fav_add fav_curr prop.Prop.sub ;
Prop.pi_fav_add fav_curr prop.Prop.pi ;
Prop.sigma_fav_add fav_curr prop.Prop.sigma ;
Prop.pi_fav_add fav_foot prop.Prop.pi_fp ;
Prop.sigma_fav_add fav_foot prop.Prop.sigma_fp ;
let favl_curr = Sil.fav_to_list fav_curr in
let favl_foot = Sil.fav_to_list fav_foot in
Sil.fav_duplicates := false ;
let num_occur l id = List.length (List.filter ~f:(fun id' -> Ident.equal id id') l) in
let at_most_once v = num_occur favl_curr v <= 1 && num_occur favl_foot v <= 1 in
at_most_once
let fav_curr =
let ( @@@ ) = Sequence.append in
Sil.exp_subst_free_vars prop.Prop.sub @@@ Prop.pi_free_vars prop.Prop.pi
@@@ Prop.sigma_free_vars prop.Prop.sigma
in
let fav_foot =
Sequence.append (Prop.pi_free_vars prop.Prop.pi_fp) (Prop.sigma_free_vars prop.Prop.sigma_fp)
in
let at_most_once seq id =
Sequence.filter seq ~f:(Ident.equal id) |> Sequence.length_is_bounded_by ~max:1
in
let at_most_once_in_curr_or_foot v = at_most_once fav_curr v && at_most_once fav_foot v in
at_most_once_in_curr_or_foot
in
let modified = ref false in
let filter_redundant_e_se fp_part (e, se) =

45
infer/src/backend/dom.ml
Unescape View File

@ -44,7 +44,7 @@ let equal_sigma sigma1 sigma2 =
let sigma_get_start_lexps_sort sigma =
let exp_compare_neg e1 e2 = -Exp.compare e1 e2 in
let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
let filter e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
let lexps = Sil.hpred_list_get_lexps filter sigma in
List.sort ~cmp:exp_compare_neg lexps
@ -576,7 +576,7 @@ module Rename : sig
val lookup_list_todo : side -> Exp.t list -> Exp.t list
val to_subst_proj : side -> Sil.fav -> Sil.exp_subst
val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.exp_subst
val to_subst_emb : side -> Sil.exp_subst
(*
@ -596,7 +596,7 @@ end = struct
let f = function
| Exp.Var id, e, _ | e, Exp.Var id, _ ->
Ident.is_footprint id
&& Sil.fav_for_all (Sil.exp_fav e) (fun id -> not (Ident.is_primed id))
&& Exp.free_vars e |> Sequence.for_all ~f:(fun id -> not (Ident.is_primed id))
| _ ->
false
in
@ -684,7 +684,9 @@ end = struct
let to_subst_proj (side: side) vars =
let renaming_restricted =
List.filter ~f:(function _, _, Exp.Var i -> Sil.fav_mem vars i | _ -> assert false) !tbl
List.filter
~f:(function _, _, Exp.Var i -> Ident.HashQueue.mem vars i | _ -> assert false)
!tbl
in
let sub_list_side =
List.map
@ -780,13 +782,9 @@ end = struct
L.d_ln () ) ;
Some (a_res, a_op)
in
let exp_contains_only_normal_ids e =
let fav = Sil.exp_fav e in
Sil.fav_for_all fav Ident.is_normal
in
let exp_contains_only_normal_ids e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
let atom_contains_only_normal_ids a =
let fav = Sil.atom_fav a in
Sil.fav_for_all fav Ident.is_normal
Sil.atom_free_vars a |> Sequence.for_all ~f:Ident.is_normal
in
let normal_ids_only = atom_contains_only_normal_ids atom_in in
if normal_ids_only then Some (atom_in, atom_in)
@ -840,15 +838,14 @@ end = struct
| Some res ->
res
| None ->
let fav1 = Sil.exp_fav e1 in
let fav2 = Sil.exp_fav e2 in
let no_ren1 = not (Sil.fav_exists fav1 can_rename) in
let no_ren2 = not (Sil.fav_exists fav2 can_rename) in
let some_primed () =
Sil.fav_exists fav1 Ident.is_primed || Sil.fav_exists fav2 Ident.is_primed
Exp.free_vars e1 |> Sequence.exists ~f:Ident.is_primed
|| Exp.free_vars e2 |> Sequence.exists ~f:Ident.is_primed
in
let e =
if no_ren1 && no_ren2 then
if not (Exp.free_vars e1 |> Sequence.exists ~f:can_rename)
&& not (Exp.free_vars e2 |> Sequence.exists ~f:can_rename)
then
if Exp.equal e1 e2 then e1 else ( L.d_strln "failure reason 13" ; raise Sil.JoinFail )
else
match default_op with
@ -1432,7 +1429,7 @@ let same_pred (hpred1: Sil.hpred) (hpred2: Sil.hpred) : bool =
let sigma_renaming_check (lhs: side) (sigma: Prop.sigma) (sigma_new: Prop.sigma) =
(* apply the lhs / rhs of the renaming to sigma,
* and check that the renaming of primed vars is injective *)
let fav_sigma = Prop.sigma_fav sigma_new in
let fav_sigma = Prop.sigma_free_vars sigma_new |> Ident.hashqueue_of_sequence in
let sub = Rename.to_subst_proj lhs fav_sigma in
let sigma' = Prop.sigma_sub (`Exp sub) sigma_new in
equal_sigma sigma sigma'
@ -1840,8 +1837,8 @@ let pi_partial_meet tenv (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop.
let dom1 = Ident.idlist_to_idset (Sil.sub_domain sub1) in
let dom2 = Ident.idlist_to_idset (Sil.sub_domain sub2) in
let handle_atom sub dom atom =
let fav_list = Sil.fav_to_list (Sil.atom_fav atom) in
if List.for_all ~f:(fun id -> Ident.Set.mem id dom) fav_list then Sil.atom_sub (`Exp sub) atom
if Sil.atom_free_vars atom |> Sequence.for_all ~f:(fun id -> Ident.Set.mem id dom) then
Sil.atom_sub (`Exp sub) atom
else ( L.d_str "handle_atom failed on " ; Sil.d_atom atom ; L.d_ln () ; raise Sil.JoinFail )
in
let f1 p' atom = Prop.prop_atom_and tenv p' (handle_atom sub1 dom1 atom) in
@ -1870,7 +1867,7 @@ let eprop_partial_meet tenv (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t =
let sub1 = ep1.Prop.sub in
let sub2 = ep2.Prop.sub in
let range1 = Sil.sub_range sub1 in
let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
Sil.equal_exp_subst sub1 sub2 && List.for_all ~f range1
in
if not (sub_check ()) then ( L.d_strln "sub_check() failed" ; raise Sil.JoinFail )
@ -1920,7 +1917,7 @@ let eprop_partial_join' tenv mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed
let sub2 = ep2.Prop.sub in
let sub_common, sub1_only, sub2_only = Sil.sub_symmetric_difference sub1 sub2 in
let sub_common_normal, sub_common_other =
let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
Sil.sub_range_partition f sub_common
in
let eqs1, eqs2 =
@ -1970,12 +1967,14 @@ let footprint_partial_join' tenv (p1: Prop.normal Prop.t) (p2: Prop.normal Prop.
let efp = eprop_partial_join' tenv JoinState.Pre fp1 fp2 in
let pi_fp =
let pi_fp0 = Prop.get_pure efp in
let f a = Sil.fav_for_all (Sil.atom_fav a) Ident.is_footprint in
let f a = Sil.atom_free_vars a |> Sequence.for_all ~f:Ident.is_footprint in
List.filter ~f pi_fp0
in
let sigma_fp =
let sigma_fp0 = efp.Prop.sigma in
let f a = Sil.fav_exists (Sil.hpred_fav a) (fun a -> not (Ident.is_footprint a)) in
let f a =
Sil.hpred_free_vars a |> Sequence.exists ~f:(fun a -> not (Ident.is_footprint a))
in
if List.exists ~f sigma_fp0 then ( L.d_strln "failure reason 66" ; raise Sil.JoinFail ) ;
sigma_fp0
in

28
infer/src/backend/interproc.ml
Unescape View File

@ -365,15 +365,13 @@ let do_after_node node = Printer.node_finish_session node
(** Return the list of normal ids occurring in the instructions *)
let instrs_get_normal_vars instrs =
let fav = Sil.fav_new () in
let do_instr instr =
let do_e e = Sil.exp_fav_add fav e in
let exps = Sil.instr_get_exps instr in
List.iter ~f:do_e exps
let do_instr res instr =
Sil.instr_get_exps instr
|> List.fold_left ~init:res ~f:(fun res e ->
Exp.free_vars e |> Sequence.filter ~f:Ident.is_normal
|> Ident.hashqueue_of_sequence ~init:res )
in
List.iter ~f:do_instr instrs ;
Sil.fav_filter_ident fav Ident.is_normal ;
Sil.fav_to_list fav
List.fold_left ~init:(Ident.HashQueue.create ()) ~f:do_instr instrs |> Ident.HashQueue.keys
(** Perform symbolic execution for a node starting from an initial prop *)
@ -571,13 +569,13 @@ let compute_visited vset =
let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
let pname = Procdesc.get_proc_name pdesc in
let sub =
let fav = Sil.fav_new () in
Paths.PathSet.iter (fun prop _ -> Prop.prop_fav_add fav prop) pathset ;
let sub_list =
List.map
~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.knormal)))
(Sil.fav_to_list fav)
let fav =
Paths.PathSet.fold
(fun prop _ res -> Prop.free_vars prop |> Ident.hashqueue_of_sequence ~init:res)
pathset (Ident.HashQueue.create ())
|> Ident.HashQueue.keys
in
let sub_list = List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.knormal))) fav in
Sil.exp_subst_of_list sub_list
in
let pre_post_visited_list =
@ -736,7 +734,7 @@ let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop.prop_emp t
(** Construct an initial prop from an existing pre with formals *)
let initial_prop_from_pre tenv curr_f pre =
if !Config.footprint then
let vars = Sil.fav_to_list (Prop.prop_fav pre) in
let vars = Prop.free_vars pre |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in
let sub_list =
List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.kfootprint))) vars
in

17
infer/src/backend/match.ml
Unescape View File

@ -152,7 +152,7 @@ and isel_match isel1 sub vars isel2 =
None
| (idx1, se1') :: isel1', (idx2, se2') :: isel2' ->
let idx2 = Sil.exp_sub (`Exp sub) idx2 in
let sanity_check = not (List.exists ~f:(fun id -> Sil.ident_in_exp id idx2) vars) in
let sanity_check = not (List.exists ~f:(fun id -> Exp.ident_mem idx2 id) vars) in
if not sanity_check then (
let pe = Pp.text in
L.internal_error "@[.... Sanity Check Failure while Matching Index-Strexps ....@\n" ;
@ -202,9 +202,7 @@ let rec instantiate_to_emp p condition (sub: Sil.exp_subst) vars = function
None
| Sil.Hlseg (_, _, e1, e2, _)
-> (
let fully_instantiated =
not (List.exists ~f:(fun id -> Sil.ident_in_exp id e1) vars)
in
let fully_instantiated = not (List.exists ~f:(fun id -> Exp.ident_mem e1 id) vars) in
if not fully_instantiated then None
else
let e1' = Sil.exp_sub (`Exp sub) e1 in
@ -215,8 +213,7 @@ let rec instantiate_to_emp p condition (sub: Sil.exp_subst) vars = function
instantiate_to_emp p condition sub_new vars_leftover hpats )
| Sil.Hdllseg (_, _, iF, oB, oF, iB, _) ->
let fully_instantiated =
not
(List.exists ~f:(fun id -> Sil.ident_in_exp id iF || Sil.ident_in_exp id oB) vars)
not (List.exists ~f:(fun id -> Exp.ident_mem iF id || Exp.ident_mem oB id) vars)
in
if not fully_instantiated then None
else
@ -338,7 +335,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
let filter = gen_filter_lseg k2 para2 e_start2 e_end2 es_shared2 in
let do_emp_lseg _ =
let fully_instantiated_start2 =
not (List.exists ~f:(fun id -> Sil.ident_in_exp id e_start2) vars)
not (List.exists ~f:(fun id -> Exp.ident_mem e_start2 id) vars)
in
if not fully_instantiated_start2 then None
else
@ -407,7 +404,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
let filter = gen_filter_dllseg k2 para2 iF2 oB2 oF2 iB2 es_shared2 in
let do_emp_dllseg _ =
let fully_instantiated_iFoB2 =
not (List.exists ~f:(fun id -> Sil.ident_in_exp id iF2 || Sil.ident_in_exp id oB2) vars)
not (List.exists ~f:(fun id -> Exp.ident_mem iF2 id || Exp.ident_mem oB2 id) vars)
in
if not fully_instantiated_iFoB2 then None
else
@ -425,9 +422,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
prop_match_with_impl_sub tenv p condition sub_new vars_leftover hpat_next hpats_rest
in
let do_para_dllseg _ =
let fully_instantiated_iF2 =
not (List.exists ~f:(fun id -> Sil.ident_in_exp id iF2) vars)
in
let fully_instantiated_iF2 = not (List.exists ~f:(fun id -> Exp.ident_mem iF2 id) vars) in
if not fully_instantiated_iF2 then None
else
let iF2' = Sil.exp_sub (`Exp sub) iF2 in

3
infer/src/backend/paths.ml
Unescape View File

@ -632,7 +632,8 @@ end = struct
(!el1, !el2)
(** It's the caller's resposibility to ensure that Prop.prop_rename_primed_footprint_vars was called on the prop *)
(** It's the caller's responsibility to ensure that [Prop.prop_rename_primed_footprint_vars] was
called on the prop *)
let add_renamed_prop (p: Prop.normal Prop.t) (path: Path.t) (ps: t) : t =
let path_new =
try

229
infer/src/backend/prop.ml
Unescape View File

@ -28,6 +28,9 @@ type normal
(** kind for exposed props *)
type exposed
(** kind for sorted props *)
type sorted
type pi = Sil.atom list [@@deriving compare]
type sigma = Sil.hpred list [@@deriving compare]
@ -56,6 +59,8 @@ module Core : sig
val unsafe_cast_to_normal : exposed t -> normal t
(** Cast an exposed prop to a normalized one by just changing the type *)
val unsafe_cast_to_sorted : exposed t -> sorted t
end = struct
(** A proposition. The following invariants are mantained. [sub] is of
the form id1 = e1 ... idn = en where: the id's are distinct and do not
@ -84,12 +89,18 @@ end = struct
let unsafe_cast_to_normal (p: exposed t) : normal t = (p :> normal t)
let unsafe_cast_to_sorted (p: exposed t) : sorted t = (p :> sorted t)
end
include Core
(** {2 Basic Functions for Propositions} *)
let expose (p: normal t) : exposed t = Obj.magic p
let expose_sorted (p: sorted t) : exposed t = Obj.magic p
(** {1 Functions for Comparison} *)
(** Comparison between propositions. Lexicographical order. *)
@ -357,44 +368,45 @@ let d_proplist_with_typ (pl: 'a t list) = L.add_print_action (PTprop_list_with_t
(** {1 Functions for computing free non-program variables} *)
let pi_fav_add fav pi = List.iter ~f:(Sil.atom_fav_add fav) pi
let pi_gen_free_vars pi = ISequence.gen_sequence_list pi ~f:Sil.atom_gen_free_vars
let pi_fav = Sil.fav_imperative_to_functional pi_fav_add
let pi_free_vars pi = Sequence.Generator.run (pi_gen_free_vars pi)
let sigma_fav_add fav sigma = List.iter ~f:(Sil.hpred_fav_add fav) sigma
let sigma_gen_free_vars sigma = ISequence.gen_sequence_list sigma ~f:Sil.hpred_gen_free_vars
let sigma_fav = Sil.fav_imperative_to_functional sigma_fav_add
let sigma_free_vars sigma = Sequence.Generator.run (sigma_gen_free_vars sigma)
let prop_footprint_fav_add fav prop = sigma_fav_add fav prop.sigma_fp ; pi_fav_add fav prop.pi_fp
(** Find free variables in the footprint part of the prop *)
let footprint_gen_free_vars {sigma_fp; pi_fp} =
Sequence.Generator.(sigma_gen_free_vars sigma_fp >>= fun () -> pi_gen_free_vars pi_fp)
(** Find fav of the footprint part of the prop *)
let prop_footprint_fav prop = Sil.fav_imperative_to_functional prop_footprint_fav_add prop
let prop_fav_add fav prop =
sigma_fav_add fav prop.sigma ;
sigma_fav_add fav prop.sigma_fp ;
Sil.sub_fav_add fav prop.sub ;
pi_fav_add fav prop.pi ;
pi_fav_add fav prop.pi_fp
let footprint_free_vars prop = Sequence.Generator.run (footprint_gen_free_vars prop)
let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} =
let open Sequence.Generator in
sigma_gen_free_vars sigma
>>= fun () ->
sigma_gen_free_vars sigma_fp
>>= fun () ->
Sil.exp_subst_gen_free_vars sub
>>= fun () -> pi_gen_free_vars pi >>= fun () -> pi_gen_free_vars pi_fp
let prop_fav p = Sil.fav_imperative_to_functional prop_fav_add p
(** free vars of the prop, excluding the pure part *)
let prop_fav_nonpure_add fav prop = sigma_fav_add fav prop.sigma ; sigma_fav_add fav prop.sigma_fp
let free_vars prop = Sequence.Generator.run (gen_free_vars prop)
(** free vars, except pi and sub, of current and footprint parts *)
let prop_fav_nonpure = Sil.fav_imperative_to_functional prop_fav_nonpure_add
let exposed_gen_free_vars prop = gen_free_vars (unsafe_cast_to_normal prop)
let hpred_fav_in_pvars_add fav (hpred: Sil.hpred) =
match hpred with
| Hpointsto (Lvar _, sexp, _) ->
Sil.strexp_fav_add fav sexp
| Hpointsto _ | Hlseg _ | Hdllseg _ ->
()
let sorted_gen_free_vars prop = exposed_gen_free_vars (expose_sorted prop)
let sorted_free_vars prop = Sequence.Generator.run (sorted_gen_free_vars prop)
(** free vars of the prop, excluding the pure part *)
let non_pure_gen_free_vars {sigma; sigma_fp} =
Sequence.Generator.(sigma_gen_free_vars sigma >>= fun () -> sigma_gen_free_vars sigma_fp)
let sigma_fav_in_pvars_add fav sigma = List.iter ~f:(hpred_fav_in_pvars_add fav) sigma
let non_pure_free_vars prop = Sequence.Generator.run (non_pure_gen_free_vars prop)
(** {2 Functions for Subsitition} *)
@ -1629,17 +1641,18 @@ module Normalize = struct
let footprint_normalize tenv prop =
let nsigma = sigma_normalize tenv Sil.sub_empty prop.sigma_fp in
let npi = pi_normalize tenv Sil.sub_empty nsigma prop.pi_fp in
let fp_vars =
let fav = pi_fav npi in
sigma_fav_add fav nsigma ; fav
let ids_primed =
let fav =
pi_free_vars npi |> Sequence.filter ~f:Ident.is_primed |> Ident.hashqueue_of_sequence
in
sigma_free_vars nsigma |> Sequence.filter ~f:Ident.is_primed
|> Ident.hashqueue_of_sequence ~init:fav |> Ident.HashQueue.keys
in
Sil.fav_filter_ident fp_vars Ident.is_primed ;
(* only keep primed vars *)
let npi', nsigma' =
if Sil.fav_is_empty fp_vars then (npi, nsigma)
if List.is_empty ids_primed then (npi, nsigma)
else
(* replace primed vars by fresh footprint vars *)
let ids_primed = Sil.fav_to_list fp_vars in
let ids_footprint =
List.map ~f:(fun id -> (id, Ident.create_fresh Ident.kfootprint)) ids_primed
in
@ -1655,7 +1668,7 @@ module Normalize = struct
(** This function assumes that if (x,Exp.Var(y)) in sub, then compare x y = 1 *)
let sub_normalize sub =
let f (id, e) = not (Ident.is_primed id) && not (Sil.ident_in_exp id e) in
let f (id, e) = not (Ident.is_primed id) && not (Exp.ident_mem e id) in
let sub' = Sil.sub_filter_pair ~f sub in
if Sil.equal_exp_subst sub sub' then sub else sub'
@ -1667,7 +1680,7 @@ module Normalize = struct
else
let p' =
match a' with
| Aeq (Var i, e) when Sil.ident_in_exp i e ->
| Aeq (Var i, e) when Exp.ident_mem e i ->
p
| Aeq (Var i, e) ->
let sub_list = [(i, e)] in
@ -1698,7 +1711,7 @@ module Normalize = struct
else
let p'' =
match a' with
| Aeq (Exp.Var i, e) when not (Sil.ident_in_exp i e) ->
| Aeq (Exp.Var i, e) when not (Exp.ident_mem e i) ->
let mysub = Sil.subst_of_list [(i, e)] in
let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in
let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in
@ -1854,7 +1867,7 @@ end
let sigma_get_start_lexps_sort sigma =
let exp_compare_neg e1 e2 = -Exp.compare e1 e2 in
let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
let filter e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in
let lexps = Sil.hpred_list_get_lexps filter sigma in
List.sort ~cmp:exp_compare_neg lexps
@ -1908,17 +1921,15 @@ let sigma_dfs_sort tenv sigma =
final () ; sigma'
let prop_dfs_sort tenv p =
let dfs_sort tenv p : sorted t =
let sigma = p.sigma in
let sigma' = sigma_dfs_sort tenv sigma in
let sigma_fp = p.sigma_fp in
let sigma_fp' = sigma_dfs_sort tenv sigma_fp in
let p' = set p ~sigma:sigma' ~sigma_fp:sigma_fp' in
(* L.out "@[<2>P SORTED:@\n%a@\n@." pp_prop p'; *)
p'
unsafe_cast_to_sorted p'
let prop_fav_add_dfs tenv fav prop = prop_fav_add fav (prop_dfs_sort tenv prop)
let rec strexp_get_array_indices acc (se: Sil.strexp) =
match se with
@ -1946,7 +1957,14 @@ let sigma_get_array_indices sigma =
List.rev indices
let compute_reindexing fav_add get_id_offset list =
let compute_reindexing_from_indices list =
let get_id_offset (e: Exp.t) =
match e with
| BinOp (PlusA, Var id, Const Cint offset) ->
if Ident.is_primed id then Some (id, offset) else None
| _ ->
None
in
let rec select list_passed list_seen = function
| [] ->
list_passed
@ -1957,10 +1975,9 @@ let compute_reindexing fav_add get_id_offset list =
| None ->
list_passed
| Some (id, _) ->
let fav = Sil.fav_new () in
List.iter ~f:(fav_add fav) list_seen ;
List.iter ~f:(fav_add fav) list_passed ;
if Sil.fav_exists fav (Ident.equal id) then list_passed else x :: list_passed
let find_id_in_list l = List.exists l ~f:(fun e -> Exp.ident_mem e id) in
if find_id_in_list list_seen || find_id_in_list list_passed then list_passed
else x :: list_passed
in
let list_seen_new = x :: list_seen in
select list_passed_new list_seen_new list_rest
@ -1977,18 +1994,6 @@ let compute_reindexing fav_add get_id_offset list =
Sil.exp_subst_of_list reindexing
let compute_reindexing_from_indices indices =
let get_id_offset (e: Exp.t) =
match e with
| BinOp (PlusA, Var id, Const Cint offset) ->
if Ident.is_primed id then Some (id, offset) else None
| _ ->
None
in
let fav_add = Sil.exp_fav_add in
compute_reindexing fav_add get_id_offset indices
let apply_reindexing tenv (exp_subst: Sil.exp_subst) prop =
let subst = `Exp exp_subst in
let nsigma = Normalize.sigma_normalize tenv subst prop.sigma in
@ -1997,7 +2002,7 @@ let apply_reindexing tenv (exp_subst: Sil.exp_subst) prop =
let dom_subst = List.map ~f:fst (Sil.sub_to_list exp_subst) in
let in_dom_subst id = List.exists ~f:(Ident.equal id) dom_subst in
let sub' = Sil.sub_filter (fun id -> not (in_dom_subst id)) prop.sub in
let contains_substituted_id e = Sil.fav_exists (Sil.exp_fav e) in_dom_subst in
let contains_substituted_id e = Exp.free_vars e |> Sequence.exists ~f:in_dom_subst in
let sub_eqs, sub_keep = Sil.sub_range_partition contains_substituted_id sub' in
let eqs = Sil.sub_to_list sub_eqs in
let atoms =
@ -2034,9 +2039,8 @@ let prop_rename_array_indices tenv prop =
apply_reindexing tenv subst prop
let compute_renaming fav =
let ids = Sil.fav_to_list fav in
let ids_primed, ids_nonprimed = List.partition_tf ~f:Ident.is_primed ids in
let compute_renaming free_vars =
let ids_primed, ids_nonprimed = List.partition_tf ~f:Ident.is_primed free_vars in
let ids_footprint = List.filter ~f:Ident.is_footprint ids_nonprimed in
let id_base_primed = Ident.create Ident.kprimed 0 in
let id_base_footprint = Ident.create Ident.kfootprint 0 in
@ -2149,7 +2153,9 @@ and hpred_captured_ren ren (hpred: Sil.hpred) : Sil.hpred =
and hpara_ren (para: Sil.hpara) : Sil.hpara =
let av = Sil.hpara_shallow_av para in
let av =
Sil.hpara_shallow_free_vars para |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys
in
let ren = compute_renaming av in
let root = ident_captured_ren ren para.root in
let next = ident_captured_ren ren para.next in
@ -2160,7 +2166,9 @@ and hpara_ren (para: Sil.hpara) : Sil.hpara =
and hpara_dll_ren (para: Sil.hpara_dll) : Sil.hpara_dll =
let av = Sil.hpara_dll_shallow_av para in
let av =
Sil.hpara_dll_shallow_free_vars para |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys
in
let ren = compute_renaming av in
let iF = ident_captured_ren ren para.cell in
let oF = ident_captured_ren ren para.flink in
@ -2182,10 +2190,8 @@ let prop_rename_primed_footprint_vars tenv (p: normal t) : normal t =
let p = prop_rename_array_indices tenv p in
let bound_vars =
let filter id = Ident.is_footprint id || Ident.is_primed id in
let p_dfs = prop_dfs_sort tenv p in
let fvars_in_p = prop_fav p_dfs in
Sil.fav_filter_ident fvars_in_p filter ;
fvars_in_p
dfs_sort tenv p |> sorted_free_vars |> Sequence.filter ~f:filter |> Ident.hashqueue_of_sequence
|> Ident.HashQueue.keys
in
let ren = compute_renaming bound_vars in
let sub' = sub_captured_ren ren p.sub in
@ -2206,8 +2212,6 @@ let prop_rename_primed_footprint_vars tenv (p: normal t) : normal t =
unsafe_cast_to_normal p'
let expose (p: normal t) : exposed t = Obj.magic p
(** Apply subsitution to prop. *)
let prop_sub subst (prop: 'a t) : exposed t =
let pi = pi_sub subst (prop.pi @ pi_of_subst prop.sub) in
@ -2222,11 +2226,10 @@ let prop_ren_sub tenv (ren_sub: Sil.exp_subst) (prop: normal t) : normal t =
Normalize.normalize tenv (prop_sub (`Exp ren_sub) prop)
(** Existentially quantify the [fav] in [prop].
[fav] should not contain any primed variables. *)
let exist_quantify tenv fav (prop: normal t) : normal t =
let ids = Sil.fav_to_list fav in
if List.exists ~f:Ident.is_primed ids then assert false ;
(** Existentially quantify the [ids] in [prop]. [ids] should not contain any primed variables. If
[ids_queue] is passed then the function uses it instead of [ids] for membership tests. *)
let exist_quantify tenv ?ids_queue ids (prop: normal t) : normal t =
assert (not (List.exists ~f:Ident.is_primed ids)) ;
(* sanity check *)
if List.is_empty ids then prop
else
@ -2234,8 +2237,15 @@ let exist_quantify tenv fav (prop: normal t) : normal t =
let ren_sub = Sil.exp_subst_of_list (List.map ~f:gen_fresh_id_sub ids) in
let prop' =
(* throw away x=E if x becomes x_ *)
let mem_idlist i = List.exists ~f:(fun id -> Ident.equal i id) in
let sub = Sil.sub_filter (fun i -> not (mem_idlist i ids)) prop.sub in
let filter =
match ids_queue with
| Some q ->
(* this is more efficient than a linear scan of [ids] *)
fun id -> not (Ident.HashQueue.mem q id)
| None ->
fun id -> not (List.mem ~equal:Ident.equal ids id)
in
let sub = Sil.sub_filter filter prop.sub in
if Sil.equal_exp_subst sub prop.sub then prop else unsafe_cast_to_normal (set prop ~sub)
in
(*
@ -2257,9 +2267,20 @@ let prop_expmap (fe: Exp.t -> Exp.t) prop =
set prop ~pi ~sigma ~pi_fp ~sigma_fp
(** convert identifiers in fav to kind [k] *)
let vars_make_unprimed tenv fav prop =
let ids = Sil.fav_to_list fav in
(** convert the normal vars to primed vars *)
let prop_normal_vars_to_primed_vars tenv p =
let ids_queue =
free_vars p |> Sequence.filter ~f:Ident.is_normal |> Ident.hashqueue_of_sequence
in
exist_quantify tenv ~ids_queue (Ident.HashQueue.keys ids_queue) p
(** convert the primed vars to normal vars. *)
let prop_primed_vars_to_normal_vars tenv (prop: normal t) : normal t =
let ids =
free_vars prop |> Sequence.filter ~f:Ident.is_primed |> Ident.hashqueue_of_sequence
|> Ident.HashQueue.keys
in
let ren_sub =
Sil.exp_subst_of_list
(List.map ~f:(fun i -> (i, Exp.Var (Ident.create_fresh Ident.knormal))) ids)
@ -2267,20 +2288,6 @@ let vars_make_unprimed tenv fav prop =
prop_ren_sub tenv ren_sub prop
(** convert the normal vars to primed vars. *)
let prop_normal_vars_to_primed_vars tenv p =
let fav = prop_fav p in
Sil.fav_filter_ident fav Ident.is_normal ;
exist_quantify tenv fav p
(** convert the primed vars to normal vars. *)
let prop_primed_vars_to_normal_vars tenv (p: normal t) : normal t =
let fav = prop_fav p in
Sil.fav_filter_ident fav Ident.is_primed ;
vars_make_unprimed tenv fav p
let from_pi pi = set prop_emp ~pi
let from_sigma sigma = set prop_emp ~sigma
@ -2412,7 +2419,7 @@ let prop_iter_make_id_primed tenv id iter =
(List.rev pairs_unpid, List.rev pairs_pid)
| (eq :: eqs_cur: pi) ->
match eq with
| Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 ->
| Aeq (Var id1, e1) when Exp.ident_mem e1 id1 ->
L.internal_error "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n" ;
L.internal_error "Broken Assumption: id notin e for all (id,e) in sub@\n" ;
L.internal_error "(id,e) : (%a,%a)@\n" Ident.pp id1 Exp.pp e1 ;
@ -2457,28 +2464,32 @@ let prop_iter_make_id_primed tenv id iter =
; pit_new= sigma_sub sub_use iter.pit_new }
let prop_iter_footprint_fav_add fav iter =
sigma_fav_add fav iter.pit_sigma_fp ;
pi_fav_add fav iter.pit_pi_fp
(** Find fav of the footprint part of the iterator *)
let prop_iter_footprint_fav iter =
Sil.fav_imperative_to_functional prop_iter_footprint_fav_add iter
let prop_iter_footprint_gen_free_vars {pit_sigma_fp; pit_pi_fp} =
Sequence.Generator.(sigma_gen_free_vars pit_sigma_fp >>= fun () -> pi_gen_free_vars pit_pi_fp)
let prop_iter_fav_add fav iter =
Sil.sub_fav_add fav iter.pit_sub ;
pi_fav_add fav iter.pit_pi ;
pi_fav_add fav (List.map ~f:snd iter.pit_newpi) ;
sigma_fav_add fav iter.pit_old ;
sigma_fav_add fav iter.pit_new ;
Sil.hpred_fav_add fav iter.pit_curr ;
prop_iter_footprint_fav_add fav iter
let prop_iter_footprint_free_vars iter =
Sequence.Generator.run (prop_iter_footprint_gen_free_vars iter)
(** Find fav of the iterator *)
let prop_iter_fav iter = Sil.fav_imperative_to_functional prop_iter_fav_add iter
let prop_iter_gen_free_vars ({pit_sub; pit_pi; pit_newpi; pit_old; pit_new; pit_curr} as iter) =
let open Sequence.Generator in
Sil.exp_subst_gen_free_vars pit_sub
>>= fun () ->
pi_gen_free_vars pit_pi
>>= fun () ->
pi_gen_free_vars (List.map ~f:snd pit_newpi)
>>= fun () ->
sigma_gen_free_vars pit_old
>>= fun () ->
sigma_gen_free_vars pit_new
>>= fun () ->
Sil.hpred_gen_free_vars pit_curr >>= fun () -> prop_iter_footprint_gen_free_vars iter
let prop_iter_free_vars iter = Sequence.Generator.run (prop_iter_gen_free_vars iter)
(** Extract the sigma part of the footprint *)
let prop_iter_get_footprint_sigma iter = iter.pit_sigma_fp

38
infer/src/backend/prop.mli
Unescape View File

@ -20,6 +20,9 @@ type normal
(** kind for exposed props *)
type exposed
(** kind for sorted props *)
type sorted
(** Proposition. *)
type pi = Sil.atom list
@ -93,33 +96,21 @@ val pp_proplist_with_typ : Pp.env -> Format.formatter -> normal t list -> unit
val d_proplist_with_typ : 'a t list -> unit
val pi_fav : atom list -> fav
(** Compute free non-program variables of pi *)
val pi_fav_add : fav -> atom list -> unit
val sigma_fav_add : fav -> hpred list -> unit
(** Compute free non-program variables of sigma *)
val pi_free_vars : pi -> Ident.t Sequence.t
val sigma_fav : hpred list -> fav
val sigma_free_vars : sigma -> Ident.t Sequence.t
val sigma_fav_in_pvars_add : fav -> hpred list -> unit
(** returns free non-program variables that are used to express
the contents of stack variables *)
val free_vars : normal t -> Ident.t Sequence.t
val prop_fav_add : fav -> 'a t -> unit
(** Compute free non-program variables of prop *)
val gen_free_vars : normal t -> (unit, Ident.t) Sequence.Generator.t
val prop_fav_add_dfs : Tenv.t -> fav -> 'a t -> unit
(** Compute free non-program variables of prop, visited in depth first order *)
val footprint_free_vars : normal t -> Ident.t Sequence.t
val prop_fav : normal t -> fav
val sorted_gen_free_vars : sorted t -> (unit, Ident.t) Sequence.Generator.t
val prop_fav_nonpure : normal t -> fav
(** free vars, except pi and sub, of current and footprint parts *)
val non_pure_free_vars : normal t -> Ident.t Sequence.t
val prop_footprint_fav : 'a t -> fav
(** Find fav of the footprint part of the prop *)
val dfs_sort : Tenv.t -> normal t -> sorted t
val pi_sub : subst -> atom list -> atom list
(** Apply substitution for pi *)
@ -266,7 +257,8 @@ val prop_expand : Tenv.t -> normal t -> normal t list
(** {2 Functions for existentially quantifying and unquantifying variables} *)
val exist_quantify : Tenv.t -> fav -> normal t -> normal t
val exist_quantify :
Tenv.t -> ?ids_queue:unit Ident.HashQueue.t -> Ident.t list -> normal t -> normal t
(** Existentially quantify the [ids] in [prop]. *)
val prop_normal_vars_to_primed_vars : Tenv.t -> normal t -> normal t
@ -317,10 +309,10 @@ val prop_iter_update_current : 'a prop_iter -> hpred -> 'a prop_iter
val prop_iter_prev_then_insert : 'a prop_iter -> hpred -> 'a prop_iter
(** Insert before the current element of the iterator. *)
val prop_iter_footprint_fav : 'a prop_iter -> fav
val prop_iter_footprint_free_vars : 'a prop_iter -> Ident.t Sequence.t
(** Find fav of the footprint part of the iterator *)
val prop_iter_fav : 'a prop_iter -> fav
val prop_iter_free_vars : 'a prop_iter -> Ident.t Sequence.t
(** Find fav of the iterator *)
val prop_iter_get_footprint_sigma : 'a prop_iter -> hpred list

28
infer/src/backend/prover.ml
Unescape View File

@ -1127,7 +1127,7 @@ end = struct
let implication_rhs = ref (Prop.expose Prop.prop_emp)
let fav_in_array_len = ref (Sil.fav_new ())
let fav_in_array_len = ref Ident.Set.empty
(* free variables in array len position *)
let bounds_checks = ref []
@ -1149,15 +1149,13 @@ end = struct
(** free vars in array len position in current strexp part of prop *)
let prop_fav_len prop =
let fav = Sil.fav_new () in
let do_hpred = function
let do_hpred fav = function
| Sil.Hpointsto (_, Sil.Earray ((Exp.Var _ as len), _, _), _) ->
Sil.exp_fav_add fav len
Exp.free_vars len |> Ident.set_of_sequence ~init:fav
| _ ->
()
fav
in
List.iter ~f:do_hpred prop.Prop.sigma ;
fav
List.fold_left ~init:Ident.Set.empty ~f:do_hpred prop.Prop.sigma
let reset lhs rhs =
@ -1191,8 +1189,8 @@ end = struct
(** atom considered array bounds check if it contains vars present in array length position in the
pre *)
let atom_is_array_bounds_check atom =
let fav_a = Sil.atom_fav atom in
Prop.atom_is_inequality atom && Sil.fav_exists fav_a (fun a -> Sil.fav_mem !fav_in_array_len a)
Prop.atom_is_inequality atom
&& Sil.atom_free_vars atom |> Sequence.exists ~f:(fun id -> Ident.Set.mem id !fav_in_array_len)
let get_bounds_checks () = !bounds_checks
@ -1368,10 +1366,8 @@ let exp_imply tenv calc_missing (subs: subst2) e1_in e2_in : subst2 =
| e1, Exp.Var v2 ->
let occurs_check v e =
(* check whether [v] occurs in normalized [e] *)
if Sil.fav_mem (Sil.exp_fav e) v
&& Sil.fav_mem
(Sil.exp_fav (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e))
v
if Exp.ident_mem e v
&& Exp.ident_mem (Prop.exp_normalize_prop ~destructive:true tenv Prop.prop_emp e) v
then raise (IMPL_EXC ("occurs check", subs, EXC_FALSE_EXPS (e1, e2)))
in
if Ident.is_primed v2 then
@ -1723,7 +1719,7 @@ let hpred_has_primed_lhs sub hpred =
| Exp.BinOp (Binop.PlusPI, e1, _) ->
find_primed e1
| _ ->
Sil.fav_exists (Sil.exp_fav e) Ident.is_primed
Exp.free_vars e |> Sequence.exists ~f:Ident.is_primed
in
let exp_has_primed e = find_primed (Sil.exp_sub sub e) in
match hpred with
@ -2565,7 +2561,9 @@ let check_array_bounds tenv (sub1, sub2) prop =
let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2 =
try
ProverState.reset prop1 prop2 ;
let filter (id, e) = Ident.is_normal id && Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
let filter (id, e) =
Ident.is_normal id && Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal
in
let sub1_base = Sil.sub_filter_pair ~f:filter prop1.Prop.sub in
let pi1, pi2 = (Prop.get_pure prop1, Prop.get_pure prop2) in
let sigma1, sigma2 = (prop1.Prop.sigma, prop2.Prop.sigma) in

41
infer/src/backend/rearrange.ml
Unescape View File

@ -379,11 +379,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
handle_case [] [] array_cont
let exp_has_only_footprint_ids e =
let fav = Sil.exp_fav e in
Sil.fav_filter_ident fav (fun id -> not (Ident.is_footprint id)) ;
Sil.fav_is_empty fav
let exp_has_only_footprint_ids e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_footprint
let laundry_offset_for_footprint max_stamp offs_in =
let rec laundry offs_seen eqs offs =
@ -543,12 +539,7 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp =
check_offset se offset
let fav_max_stamp fav =
let max_stamp = ref 0 in
let f id = max_stamp := max !max_stamp (Ident.get_stamp id) in
List.iter ~f (Sil.fav_to_list fav) ;
max_stamp
let id_max_stamp curr_max id = max curr_max (Ident.get_stamp id)
(** [prop_iter_extend_ptsto iter lexp] extends the current psto
predicate in [iter] with enough fields to follow the path in
@ -560,12 +551,11 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
Sil.d_exp lexp ;
L.d_ln () ) ;
let offset = Sil.exp_get_offsets lexp in
let max_stamp = fav_max_stamp (Prop.prop_iter_fav iter) in
let max_stamp_val = !max_stamp in
let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in
let extend_footprint_pred = function
| Sil.Hpointsto (e, se, te) ->
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp_val) se te
strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp) se te
offset inst
in
List.map
@ -575,8 +565,8 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
match hpara.Sil.body with
| (Sil.Hpointsto (e', se', te')) :: body_rest ->
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp_val) se'
te' offset inst
strexp_extend_values pname tenv orig_prop true Ident.kfootprint (ref max_stamp) se' te'
offset inst
in
let atoms_body_list =
List.map
@ -624,7 +614,8 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
in
let iter_list =
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop false extend_kind max_stamp se te offset inst
strexp_extend_values pname tenv orig_prop false extend_kind (ref max_stamp) se te offset
inst
in
List.map ~f:(atoms_se_te_to_iter e) atoms_se_te_list
in
@ -702,9 +693,9 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
that [root(lexp): typ] is the current hpred of the iterator. typ
is the type of the root of lexp. *)
let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
let max_stamp = fav_max_stamp (Prop.prop_footprint_fav prop) in
let max_stamp = Prop.footprint_free_vars prop |> Sequence.fold ~init:0 ~f:id_max_stamp in
let ptsto, ptsto_foot, atoms =
mk_ptsto_exp_footprint pname tenv prop (lexp, typ) max_stamp inst
mk_ptsto_exp_footprint pname tenv prop (lexp, typ) (ref max_stamp) inst
in
L.d_strln "++++ Adding footprint frame" ;
Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto) ;
@ -1068,9 +1059,11 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
L.d_str "typ:" ;
Typ.d_full typ ;
L.d_ln () ) ;
let max_stamp = fav_max_stamp (Prop.prop_iter_footprint_fav iter) in
let max_stamp =
Prop.prop_iter_footprint_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp
in
let ptsto, ptsto_foot, atoms =
mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst
mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) (ref max_stamp) inst
in
L.d_strln "++++ Adding footprint frame" ;
Prop.d_prop (Prop.prop_hpred_star Prop.prop_emp ptsto) ;
@ -1147,10 +1140,10 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
check_field_splitting () ;
match Prop.prop_iter_current tenv iter with
| Sil.Hpointsto (e, se, te), offset ->
let max_stamp = fav_max_stamp (Prop.prop_iter_fav iter) in
let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in
let atoms_se_te_list =
strexp_extend_values pname tenv orig_prop false Ident.kprimed max_stamp se te offset
inst
strexp_extend_values pname tenv orig_prop false Ident.kprimed (ref max_stamp) se te
offset inst
in
let handle_case (atoms', se', te') =
let iter' =

43
infer/src/backend/specs.ml
Unescape View File

@ -40,11 +40,14 @@ module Jprop = struct
let to_prop = function Prop (_, p) -> p | Joined (_, p, _, _) -> p
let rec fav_add_dfs tenv fav = function
| Prop (_, p) ->
Prop.prop_fav_add_dfs tenv fav p
| Joined (_, p, jp1, jp2) ->
Prop.prop_fav_add_dfs tenv fav p ; fav_add_dfs tenv fav jp1 ; fav_add_dfs tenv fav jp2
let rec sorted_gen_free_vars tenv =
let open Sequence.Generator in
function
| Prop (_, p) ->
Prop.dfs_sort tenv p |> Prop.sorted_gen_free_vars
| Joined (_, p, jp1, jp2) ->
Prop.dfs_sort tenv p |> Prop.sorted_gen_free_vars
>>= fun () -> sorted_gen_free_vars tenv jp1 >>= fun () -> sorted_gen_free_vars tenv jp2
let rec normalize tenv = function
@ -94,13 +97,17 @@ module Jprop = struct
L.add_print_action (L.PTjprop_list, Obj.repr (shallow, jplist))
let rec fav_add fav = function
| Prop (_, p) ->
Prop.prop_fav_add fav p
| Joined (_, p, jp1, jp2) ->
Prop.prop_fav_add fav p ; fav_add fav jp1 ; fav_add fav jp2
let rec gen_free_vars =
let open Sequence.Generator in
function
| Prop (_, p) ->
Prop.gen_free_vars p
| Joined (_, p, jp1, jp2) ->
Prop.gen_free_vars p >>= fun () -> gen_free_vars jp1 >>= fun () -> gen_free_vars jp2
let free_vars jp = Sequence.Generator.run (gen_free_vars jp)
let rec jprop_sub sub = function
| Prop (n, p) ->
Prop (n, Prop.prop_sub sub p)
@ -190,12 +197,15 @@ end = struct
let tospecs specs = specs
let spec_fav tenv (spec: Prop.normal spec) : Sil.fav =
let fav = Sil.fav_new () in
Jprop.fav_add_dfs tenv fav spec.pre ;
List.iter ~f:(fun (p, _) -> Prop.prop_fav_add_dfs tenv fav p) spec.posts ;
fav
let gen_free_vars tenv (spec: Prop.normal spec) =
let open Sequence.Generator in
Jprop.sorted_gen_free_vars tenv spec.pre
>>= fun () ->
ISequence.gen_sequence_list spec.posts ~f:(fun (p, _) ->
Prop.dfs_sort tenv p |> Prop.sorted_gen_free_vars )
let free_vars tenv spec = Sequence.Generator.run (gen_free_vars tenv spec)
let spec_sub tenv sub spec =
{ pre= Jprop.normalize tenv (Jprop.jprop_sub sub spec.pre)
@ -206,8 +216,7 @@ end = struct
(** Convert spec into normal form w.r.t. variable renaming *)
let normalize tenv (spec: Prop.normal spec) : Prop.normal spec =
let fav = spec_fav tenv spec in
let idlist = Sil.fav_to_list fav in
let idlist = free_vars tenv spec |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in
let count = ref 0 in
let sub =
Sil.subst_of_list

3
infer/src/backend/specs.mli
Unescape View File

@ -31,8 +31,7 @@ module Jprop : sig
val d_list : bool -> Prop.normal t list -> unit
(** dump a joined prop list, the boolean indicates whether to print toplevel props only *)
val fav_add : Sil.fav -> 'a t -> unit
(** Add fav to a jprop *)
val free_vars : Prop.normal t -> Ident.t Sequence.t
val filter : ('a t -> 'b option) -> 'a t list -> 'b list
(** [jprop_filter filter joinedprops] applies [filter] to the elements

3
infer/src/backend/state.ml
Unescape View File

@ -250,8 +250,7 @@ let get_prop_tenv_pdesc () = !gs.last_prop_tenv_pdesc
(** extract the footprint of the prop, and turn it into a normalized precondition using spec variables *)
let extract_pre p tenv pdesc abstract_fun =
let sub =
let fav = Prop.prop_fav p in
let idlist = Sil.fav_to_list fav in
let idlist = Prop.free_vars p |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in
let count = ref 0 in
Sil.subst_of_list
(List.map

17
infer/src/backend/symExec.ml
Unescape View File

@ -1346,7 +1346,7 @@ let rec sym_exec tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) path
[ Abs.remove_redundant_array_elements current_pname tenv
(Abs.abstract current_pname tenv prop_) ]
| Sil.Remove_temps (temps, _) ->
ret_old_path [Prop.exist_quantify tenv (Sil.fav_from_list temps) prop_]
ret_old_path [Prop.exist_quantify tenv temps prop_]
| Sil.Declare_locals (ptl, _) ->
let sigma_locals =
let add_None (x, typ) =
@ -1742,9 +1742,10 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t),
let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
let prop_primed_to_normal p =
(* Rename primed vars with fresh normal vars, and return them *)
let fav = Prop.prop_fav p in
Sil.fav_filter_ident fav Ident.is_primed ;
let ids_primed = Sil.fav_to_list fav in
let ids_primed =
Prop.free_vars p |> Sequence.filter ~f:Ident.is_primed |> Ident.hashqueue_of_sequence
|> Ident.HashQueue.keys
in
let ids_primed_normal =
List.map ~f:(fun id -> (id, Ident.create_fresh Ident.knormal)) ids_primed
in
@ -1752,18 +1753,16 @@ and sym_exec_wrapper handle_exn tenv proc_cfg instr ((prop: Prop.normal Prop.t),
Sil.subst_of_list (List.map ~f:(fun (id1, id2) -> (id1, Exp.Var id2)) ids_primed_normal)
in
let p' = Prop.normalize tenv (Prop.prop_sub ren_sub p) in
let fav_normal = Sil.fav_from_list (List.map ~f:snd ids_primed_normal) in
let fav_normal = List.map ~f:snd ids_primed_normal in
(p', fav_normal)
in
let prop_normal_to_primed fav_normal p =
(* rename given normal vars to fresh primed *)
if List.is_empty (Sil.fav_to_list fav_normal) then p else Prop.exist_quantify tenv fav_normal p
if List.is_empty fav_normal then p else Prop.exist_quantify tenv fav_normal p
in
try
let pre_process_prop p =
let p', fav =
if Sil.instr_is_auxiliary instr then (p, Sil.fav_new ()) else prop_primed_to_normal p
in
let p', fav = if Sil.instr_is_auxiliary instr then (p, []) else prop_primed_to_normal p in
let p'' =
let map_res_action e ra =
(* update the vpath in resource attributes *)

81
infer/src/backend/tabulation.ml
Unescape View File

@ -110,10 +110,12 @@ let spec_rename_vars pname spec =
| Specs.Jprop.Joined (n, p, jp1, jp2) ->
Specs.Jprop.Joined (n, prop_add_callee_suffix p, jp1, jp2)
in
let fav = Sil.fav_new () in
Specs.Jprop.fav_add fav spec.Specs.pre ;
List.iter ~f:(fun (p, _) -> Prop.prop_fav_add fav p) spec.Specs.posts ;
let ids = Sil.fav_to_list fav in
let fav =
let fav = Specs.Jprop.free_vars spec.Specs.pre |> Ident.hashqueue_of_sequence in
List.fold_left spec.Specs.posts ~init:fav ~f:(fun fav (p, _) ->
Prop.free_vars p |> Ident.hashqueue_of_sequence ~init:fav )
in
let ids = Ident.HashQueue.keys fav in
let ids' = List.map ~f:(fun i -> (i, Ident.create_fresh Ident.kprimed)) ids in
let ren_sub = Sil.subst_of_list (List.map ~f:(fun (i, i') -> (i, Exp.Var i')) ids') in
let pre' = Specs.Jprop.jprop_sub ren_sub spec.Specs.pre in
@ -154,9 +156,7 @@ let spec_find_rename trace_call summary : (int * Prop.exposed Specs.spec) list *
let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld
frame_typ missing_typ =
let hpred_has_only_footprint_vars hpred =
let fav = Sil.fav_new () in
Sil.hpred_fav_add fav hpred ;
Sil.fav_for_all fav Ident.is_footprint
Sil.hpred_free_vars hpred |> Sequence.for_all ~f:Ident.is_footprint
in
let sub = Sil.sub_join sub1 sub2 in
let sub1_inverse =
@ -168,28 +168,29 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
Sil.exp_subst_of_list_duplicates sub1_inverse_list
in
let fav_actual_pre =
let fav_sub2 =
(* vars which represent expansions of fields *)
let fav = Sil.fav_new () in
List.iter ~f:(Sil.exp_fav_add fav) (Sil.sub_range sub2) ;
let filter id = Int.equal (Ident.get_stamp id) (-1) in
Sil.fav_filter_ident fav filter ; fav
in
let fav_pre = Prop.prop_fav actual_pre in
Sil.ident_list_fav_add (Sil.fav_to_list fav_sub2) fav_pre ;
fav_pre
let fav_pre = Prop.free_vars actual_pre |> Ident.hashqueue_of_sequence in
let filter id = Int.equal (Ident.get_stamp id) (-1) in
(* vars which represent expansions of fields *)
Sil.sub_range sub2
|> List.fold_left ~init:fav_pre ~f:(fun res e ->
Exp.free_vars e |> Sequence.filter ~f:filter |> Ident.hashqueue_of_sequence ~init:res )
in
let fav_missing = Prop.sigma_fav (Prop.sigma_sub (`Exp sub) missing_sigma) in
Prop.pi_fav_add fav_missing (Prop.pi_sub (`Exp sub) missing_pi) ;
let fav_missing_primed =
let filter id = Ident.is_primed id && not (Sil.fav_mem fav_actual_pre id) in
Sil.fav_copy_filter_ident fav_missing filter
let filter id = Ident.is_primed id && not (Ident.HashQueue.mem fav_actual_pre id) in
let fav =
Prop.sigma_sub (`Exp sub) missing_sigma |> Prop.sigma_free_vars |> Sequence.filter ~f:filter
|> Ident.hashqueue_of_sequence
in
Prop.pi_sub (`Exp sub) missing_pi |> Prop.pi_free_vars |> Sequence.filter ~f:filter
|> Ident.hashqueue_of_sequence ~init:fav |> Ident.HashQueue.keys
in
let fav_missing_fld =
Prop.sigma_sub (`Exp sub) missing_fld |> Prop.sigma_free_vars |> Ident.hashqueue_of_sequence
in
let fav_missing_fld = Prop.sigma_fav (Prop.sigma_sub (`Exp sub) missing_fld) in
let map_var_to_pre_var_or_fresh id =
match Sil.exp_sub (`Exp sub1_inverse) (Exp.Var id) with
| Exp.Var id' ->
if Sil.fav_mem fav_actual_pre id' || Ident.is_path id'
if Ident.HashQueue.mem fav_actual_pre id' || Ident.is_path id'
(* a path id represents a position in the pre *)
then Exp.Var id'
else Exp.Var (Ident.create_fresh Ident.kprimed)
@ -197,16 +198,11 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
assert false
in
let sub_list = Sil.sub_to_list sub in
let fav_sub_list =
let fav_sub = Sil.fav_new () in
List.iter ~f:(fun (_, e) -> Sil.exp_fav_add fav_sub e) sub_list ;
Sil.fav_to_list fav_sub
in
let sub1 =
let f id =
if Sil.fav_mem fav_actual_pre id then (id, Exp.Var id)
if Ident.HashQueue.mem fav_actual_pre id then (id, Exp.Var id)
else if Ident.is_normal id then (id, map_var_to_pre_var_or_fresh id)
else if Sil.fav_mem fav_missing_fld id then (id, Exp.Var id)
else if Ident.HashQueue.mem fav_missing_fld id then (id, Exp.Var id)
else if Ident.is_footprint id then (id, Exp.Var id)
else
let dom1 = Sil.sub_domain sub1 in
@ -214,7 +210,7 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
let dom2 = Sil.sub_domain sub2 in
let rng2 = Sil.sub_range sub2 in
let vars_actual_pre =
List.map ~f:(fun id -> Exp.Var id) (Sil.fav_to_list fav_actual_pre)
List.map ~f:(fun id -> Exp.Var id) (Ident.HashQueue.keys fav_actual_pre)
in
L.d_str "fav_actual_pre: " ;
Sil.d_exp_list vars_actual_pre ;
@ -236,11 +232,16 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
L.d_ln () ;
assert false
in
let fav_sub_list =
List.fold_left sub_list ~init:(Ident.HashQueue.create ()) ~f:(fun fav (_, e) ->
Exp.free_vars e |> Ident.hashqueue_of_sequence ~init:fav )
|> Ident.HashQueue.keys
in
Sil.subst_of_list (List.map ~f fav_sub_list)
in
let sub2_list =
let f id = (id, Exp.Var (Ident.create_fresh Ident.kfootprint)) in
List.map ~f (Sil.fav_to_list fav_missing_primed)
List.map ~f fav_missing_primed
in
let sub_list' = List.map ~f:(fun (id, e) -> (id, Sil.exp_sub sub1 e)) sub_list in
let sub' = Sil.subst_of_list (sub2_list @ sub_list') in
@ -683,8 +684,7 @@ let prop_footprint_add_pi_sigma_starfld_sigma tenv (prop: 'a Prop.t) pi_new sigm
| [] ->
current_pi
| a :: new_pi' ->
let fav = Prop.pi_fav [a] in
if Sil.fav_exists fav (fun id -> not (Ident.is_footprint id)) then (
if Sil.atom_free_vars a |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id)) then (
L.d_warning "dropping atom with non-footprint variable" ;
L.d_ln () ;
Sil.d_atom a ;
@ -1187,18 +1187,17 @@ let remove_constant_string_class tenv prop =
and remove pointsto's whose lhs is a constant string *)
let quantify_path_idents_remove_constant_strings tenv (prop: Prop.normal Prop.t)
: Prop.normal Prop.t =
let fav = Prop.prop_fav prop in
Sil.fav_filter_ident fav Ident.is_path ;
remove_constant_string_class tenv (Prop.exist_quantify tenv fav prop)
let ids_queue =
Prop.free_vars prop |> Sequence.filter ~f:Ident.is_path |> Ident.hashqueue_of_sequence
in
let ids_list = Ident.HashQueue.keys ids_queue in
remove_constant_string_class tenv (Prop.exist_quantify tenv ~ids_queue ids_list prop)
(** Strengthen the footprint by adding pure facts from the current part *)
let prop_pure_to_footprint tenv (p: 'a Prop.t) : Prop.normal Prop.t =
let is_footprint_atom_not_attribute a =
not (Attribute.is_pred a)
&&
let a_fav = Sil.atom_fav a in
Sil.fav_for_all a_fav Ident.is_footprint
not (Attribute.is_pred a) && Sil.atom_free_vars a |> Sequence.for_all ~f:Ident.is_footprint
in
let pure = Prop.get_pure p in
let new_footprint_atoms = List.filter ~f:is_footprint_atom_not_attribute pure in

14
infer/src/base/ISequence.ml
Unescape View File

@ -0,0 +1,14 @@
(*
* 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.
*)
open! IStd
let rec gen_sequence_list ~f =
let open Sequence.Generator in
function [] -> return () | x :: tl -> f x >>= fun () -> gen_sequence_list ~f tl

15
infer/src/base/ISequence.mli
Unescape View File

@ -0,0 +1,15 @@
(*
* 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.
*)
open! IStd
(** Utility functions for sequences *)
val gen_sequence_list :
f:('a -> (unit, 'b) Sequence.Generator.t) -> 'a list -> (unit, 'b) Sequence.Generator.t

14
infer/src/istd/IList.ml
Unescape View File

@ -65,20 +65,6 @@ let rec merge_sorted_nodup compare res xs1 xs2 =
else merge_sorted_nodup compare (x2 :: res) xs1 xs2'
let intersect compare l1 l2 =
let l1_sorted = List.sort compare l1 in
let l2_sorted = List.sort compare l2 in
let rec f l1 l2 =
match (l1, l2) with
| [], _ | _, [] ->
false
| x1 :: l1', x2 :: l2' ->
let x_comparison = compare x1 x2 in
if x_comparison = 0 then true else if x_comparison < 0 then f l1' l2 else f l1 l2'
in
f l1_sorted l2_sorted
let inter compare xs ys =
let rev_sort xs = List.sort (fun x y -> compare y x) xs in
let rev_xs = rev_sort xs in

4
infer/src/istd/IList.mli
Unescape View File

@ -19,10 +19,6 @@ val remove_irrelevant_duplicates : ('a -> 'a -> int) -> ('a -> bool) -> 'a list
val merge_sorted_nodup : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list -> 'a list
(** The function works on sorted lists without duplicates *)
val intersect : ('a -> 'a -> int) -> 'a list -> 'a list -> bool
(** Returns whether there is an intersection in the elements of the two lists.
The compare function is required to sort the lists. *)
val inter : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
(** [inter cmp xs ys] are the elements in both [xs] and [ys], sorted according to [cmp]. *)

Write Preview
Loading…
Cancel
Save