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

[SIL] remove dead `Typ substitution

Browse Source 
Summary:
The constructor `` `Typ`` is never used to build values. Removing type
substitutions from Sil.ml had knock-on effect on Typ.ml etc., resulting in more
deleted code around type substitutions \o/

Reviewed By: mbouaziz

Differential Revision: D9769340

fbshipit-source-id: 509cbd284
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent 888a169dce
commit 4ddbc714ba
18 changed files with 203 additions and 386 deletions
Show Stats Download Patch File Download Diff File

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

@ -1078,46 +1078,33 @@ type ident_exp = Ident.t * Exp.t [@@deriving compare]
let compare_ident_exp_ids (id1, _) (id2, _) = Ident.compare id1 id2
type exp_subst = ident_exp list [@@deriving compare]
type subst = ident_exp list [@@deriving compare]
type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare]
type subst_fun = Ident.t -> Exp.t
type subst_fun = [`Exp of Ident.t -> Exp.t | `Typ of (Typ.t -> Typ.t) * (Typ.Name.t -> Typ.Name.t)]
let equal_exp_subst = [%compare.equal: exp_subst]
let equal_subst = [%compare.equal: subst]
let sub_no_duplicated_ids sub = not (List.contains_dup ~compare:compare_ident_exp_ids sub)
(** Create a substitution from a list of pairs.
For all (id1, e1), (id2, e2) in the input list,
if id1 = id2, then e1 = e2. *)
let exp_subst_of_list sub =
let subst_of_list sub =
let sub' = List.dedup_and_sort ~compare:compare_ident_exp sub in
assert (sub_no_duplicated_ids sub') ;
sub'
let subst_of_list sub = `Exp (exp_subst_of_list sub)
(** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence *)
let exp_subst_of_list_duplicates sub = List.dedup_and_sort ~compare:compare_ident_exp_ids sub
(** like subst_of_list, but allow duplicate ids and only keep the first occurrence *)
let subst_of_list_duplicates sub = List.dedup_and_sort ~compare:compare_ident_exp_ids sub
(** Convert a subst to a list of pairs. *)
let sub_to_list sub = sub
(** The empty substitution. *)
let exp_sub_empty = exp_subst_of_list []
let sub_empty = `Exp exp_sub_empty
let is_sub_empty = function
| `Exp [] ->
true
| `Exp _ ->
false
| `Typ sub ->
Typ.is_type_subst_empty sub
let sub_empty = subst_of_list []
let is_sub_empty = List.is_empty
(** Join two substitutions into one.
For all id in dom(sub1) cap dom(sub2), sub1(id) = sub2(id). *)
@ -1150,11 +1137,11 @@ let sub_symmetric_difference sub1_in sub2_in =
(** [sub_find filter sub] returns the expression associated to the first identifier
that satisfies [filter]. Raise [Not_found] if there isn't one. *)
let sub_find filter (sub : exp_subst) = snd (List.find_exn ~f:(fun (i, _) -> filter i) sub)
let sub_find filter (sub : subst) = snd (List.find_exn ~f:(fun (i, _) -> filter i) sub)
(** [sub_filter filter sub] restricts the domain of [sub] to the
identifiers satisfying [filter]. *)
let sub_filter filter (sub : exp_subst) = List.filter ~f:(fun (i, _) -> filter i) sub
let sub_filter filter (sub : subst) = List.filter ~f:(fun (i, _) -> filter i) sub
(** [sub_filter_pair filter sub] restricts the domain of [sub] to the
identifiers satisfying [filter(id, sub(id))]. *)
@ -1162,15 +1149,11 @@ let sub_filter_pair = List.filter
(** [sub_range_partition filter sub] partitions [sub] according to
whether range expressions satisfy [filter]. *)
let sub_range_partition filter (sub : exp_subst) =
List.partition_tf ~f:(fun (_, e) -> filter e) sub
let sub_range_partition filter (sub : subst) = List.partition_tf ~f:(fun (_, e) -> filter e) sub
(** [sub_domain_partition filter sub] partitions [sub] according to
whether domain identifiers satisfy [filter]. *)
let sub_domain_partition filter (sub : exp_subst) =
List.partition_tf ~f:(fun (i, _) -> filter i) sub
let sub_domain_partition filter (sub : subst) = List.partition_tf ~f:(fun (i, _) -> filter i) sub
(** Return the list of identifiers in the domain of the substitution. *)
let sub_domain sub = List.map ~f:fst sub
@ -1179,42 +1162,36 @@ let sub_domain sub = List.map ~f:fst sub
let sub_range sub = List.map ~f:snd sub
(** [sub_range_map f sub] applies [f] to the expressions in the range of [sub]. *)
let sub_range_map f sub = exp_subst_of_list (List.map ~f:(fun (i, e) -> (i, f e)) sub)
let sub_range_map f sub = subst_of_list (List.map ~f:(fun (i, e) -> (i, f e)) sub)
(** [sub_map f g sub] applies the renaming [f] to identifiers in the domain
of [sub] and the substitution [g] to the expressions in the range of [sub]. *)
let sub_map f g sub = exp_subst_of_list (List.map ~f:(fun (i, e) -> (f i, g e)) sub)
let sub_map f g sub = subst_of_list (List.map ~f:(fun (i, e) -> (f i, g e)) sub)
let mem_sub id sub = List.exists ~f:(fun (id1, _) -> Ident.equal id id1) sub
(** Extend substitution and return [None] if not possible. *)
let extend_sub sub id exp : exp_subst option =
let extend_sub sub id exp : subst option =
let compare (id1, _) (id2, _) = Ident.compare id1 id2 in
if mem_sub id sub then None else Some (List.merge ~compare sub [(id, exp)])
(** Free auxilary variables in the domain and range of the substitution. *)
let exp_subst_gen_free_vars sub =
let 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 subst_free_vars sub = Sequence.Generator.run (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
let f_tname x = match f with `Exp _ -> x | `Typ (_, f) -> f x in
match (exp : Exp.t) with
| Var id -> (
match f with
| `Exp f_exp -> (
match f_exp id with
| Exp.Var id' when Ident.equal id id' ->
exp (* it will preserve physical equality when needed *)
| exp' ->
exp' )
| _ ->
exp )
match f id with
| Exp.Var id' when Ident.equal id id' ->
exp (* it will preserve physical equality when needed *)
| exp' ->
exp' )
| Lvar _ ->
exp
| Exn e ->
@ -1225,8 +1202,7 @@ let rec exp_sub_ids (f : subst_fun) exp =
IList.map_changed ~equal:[%compare.equal: Exp.t * Pvar.t * Typ.t]
~f:(fun ((e, pvar, typ) as captured) ->
let e' = exp_sub_ids f e in
let typ' = f_typ typ in
if phys_equal e' e && phys_equal typ typ' then captured else (e', pvar, typ') )
if phys_equal e' e then captured else (e', pvar, typ) )
c.captured_vars
in
if phys_equal captured_vars c.captured_vars then exp else Exp.Closure {c with captured_vars}
@ -1234,54 +1210,31 @@ let rec exp_sub_ids (f : subst_fun) exp =
exp
| Cast (t, e) ->
let e' = exp_sub_ids f e in
let t' = f_typ t in
if phys_equal e' e && phys_equal t' t then exp else Exp.Cast (t', e')
if phys_equal e' e then exp else Exp.Cast (t, e')
| UnOp (op, e, typ_opt) ->
let e' = exp_sub_ids f e in
let typ_opt' =
match typ_opt with
| Some t ->
let t' = f_typ t in
if phys_equal t t' then typ_opt else Some t'
| None ->
typ_opt
in
if phys_equal e' e && phys_equal typ_opt typ_opt' then exp else Exp.UnOp (op, e', typ_opt')
if phys_equal e' e then exp else Exp.UnOp (op, e', typ_opt)
| BinOp (op, e1, e2) ->
let e1' = exp_sub_ids f e1 in
let e2' = exp_sub_ids f e2 in
if phys_equal e1' e1 && phys_equal e2' e2 then exp else Exp.BinOp (op, e1', e2')
| Lfield (e, fld, typ) ->
let e' = exp_sub_ids f e in
let typ' = f_typ typ in
let fld' = Typ.Fieldname.class_name_replace ~f:f_tname fld in
if phys_equal e' e && phys_equal typ typ' && phys_equal fld fld' then exp
else Exp.Lfield (e', fld', typ')
if phys_equal e' e then exp else Exp.Lfield (e', fld, typ)
| Lindex (e1, e2) ->
let e1' = exp_sub_ids f e1 in
let e2' = exp_sub_ids f e2 in
if phys_equal e1' e1 && phys_equal e2' e2 then exp else Exp.Lindex (e1', e2')
| Sizeof ({typ; dynamic_length= Some l; subtype} as sizeof_data) ->
| Sizeof ({dynamic_length= Some l} as sizeof_data) ->
let l' = exp_sub_ids f l in
let typ' = f_typ typ in
let subtype' = Subtype.sub_type f_tname subtype in
if phys_equal l' l && phys_equal typ typ' && phys_equal subtype subtype' then exp
else Exp.Sizeof {sizeof_data with typ= typ'; dynamic_length= Some l'; subtype= subtype'}
| Sizeof ({typ; dynamic_length= None; subtype} as sizeof_data) ->
let typ' = f_typ typ in
let subtype' = Subtype.sub_type f_tname subtype in
if phys_equal typ typ' then exp
else Exp.Sizeof {sizeof_data with typ= typ'; subtype= subtype'}
if phys_equal l' l then exp else Exp.Sizeof {sizeof_data with dynamic_length= Some l'}
| Sizeof {dynamic_length= None} ->
exp
let apply_sub subst : subst_fun =
match subst with
| `Exp l ->
`Exp
(fun id ->
match List.Assoc.find l ~equal:Ident.equal id with Some x -> x | None -> Exp.Var id )
| `Typ typ_subst ->
`Typ (Typ.sub_type typ_subst, Typ.sub_tname typ_subst)
fun id ->
match List.Assoc.find subst ~equal:Ident.equal id with Some x -> x | None -> Exp.Var id
let exp_sub (subst : subst) e = exp_sub_ids (apply_sub subst) e
@ -1291,27 +1244,22 @@ let instr_sub_ids ~sub_id_binders f instr =
let sub_id id =
match exp_sub_ids f (Var id) with Var id' when not (Ident.equal id id') -> id' | _ -> id
in
let sub_typ x = match f with `Exp _ -> x | `Typ (f, _) -> f x in
match instr with
| Load (id, rhs_exp, typ, loc) ->
let id' = if sub_id_binders then sub_id id else id in
let rhs_exp' = exp_sub_ids f rhs_exp in
let typ' = sub_typ typ in
if phys_equal id' id && phys_equal rhs_exp' rhs_exp && phys_equal typ typ' then instr
else Load (id', rhs_exp', typ', loc)
if phys_equal id' id && phys_equal rhs_exp' rhs_exp then instr
else Load (id', rhs_exp', typ, loc)
| Store (lhs_exp, typ, rhs_exp, loc) ->
let lhs_exp' = exp_sub_ids f lhs_exp in
let typ' = sub_typ typ in
let rhs_exp' = exp_sub_ids f rhs_exp in
if phys_equal lhs_exp' lhs_exp && phys_equal typ typ' && phys_equal rhs_exp' rhs_exp then
instr
else Store (lhs_exp', typ', rhs_exp', loc)
if phys_equal lhs_exp' lhs_exp && phys_equal rhs_exp' rhs_exp then instr
else Store (lhs_exp', typ, rhs_exp', loc)
| Call (((id, typ) as ret_id_typ), fun_exp, actuals, call_flags, loc) ->
let ret_id' =
if sub_id_binders then
let id' = sub_id id in
let typ' = sub_typ typ in
if Ident.equal id id' && phys_equal typ typ' then ret_id_typ else (id', typ')
if Ident.equal id id' then ret_id_typ else (id', typ)
else ret_id_typ
in
let fun_exp' = exp_sub_ids f fun_exp in
@ -1319,9 +1267,7 @@ let instr_sub_ids ~sub_id_binders f instr =
IList.map_changed ~equal:[%compare.equal: Exp.t * Typ.t]
~f:(fun ((actual, typ) as actual_pair) ->
let actual' = exp_sub_ids f actual in
let typ' = sub_typ typ in
if phys_equal actual' actual && phys_equal typ typ' then actual_pair
else (actual', typ') )
if phys_equal actual' actual then actual_pair else (actual', typ) )
actuals
in
if
@ -1549,8 +1495,7 @@ let hpara_instantiate para e1 e2 elist =
try List.map2_exn ~f:g para.evars ids_evars with Invalid_argument _ -> assert false
in
let subst =
`Exp
(exp_subst_of_list (((para.root, e1) :: (para.next, e2) :: subst_for_svars) @ subst_for_evars))
subst_of_list (((para.root, e1) :: (para.next, e2) :: subst_for_svars) @ subst_for_evars)
in
(ids_evars, List.map ~f:(hpred_sub subst) para.body)
@ -1574,10 +1519,9 @@ let hpara_dll_instantiate (para : hpara_dll) cell blink flink elist =
try List.map2_exn ~f:g para.evars_dll ids_evars with Invalid_argument _ -> assert false
in
let subst =
`Exp
(exp_subst_of_list
( ((para.cell, cell) :: (para.blink, blink) :: (para.flink, flink) :: subst_for_svars)
@ subst_for_evars ))
subst_of_list
( ((para.cell, cell) :: (para.blink, blink) :: (para.flink, flink) :: subst_for_svars)
@ subst_for_evars )
in
(ids_evars, List.map ~f:(hpred_sub subst) para.body_dll)

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

@ -385,87 +385,79 @@ val hpara_dll_shallow_free_vars : hpara_dll -> Ident.t Sequence.t
(** {2 Substitution} *)
type exp_subst = private (Ident.t * Exp.t) list [@@deriving compare]
type subst = private (Ident.t * Exp.t) list [@@deriving compare]
type subst = [`Exp of exp_subst | `Typ of Typ.type_subst_t] [@@deriving compare]
val equal_exp_subst : exp_subst -> exp_subst -> bool
val equal_subst : subst -> subst -> bool
(** Equality for substitutions. *)
val exp_subst_of_list : (Ident.t * Exp.t) list -> exp_subst
val subst_of_list : (Ident.t * Exp.t) list -> subst
(** Create a substitution from a list of pairs.
For all (id1, e1), (id2, e2) in the input list,
if id1 = id2, then e1 = e2. *)
val subst_of_list : (Ident.t * Exp.t) list -> subst
val exp_subst_of_list_duplicates : (Ident.t * Exp.t) list -> exp_subst
(** like exp_subst_of_list, but allow duplicate ids and only keep the first occurrence *)
val subst_of_list_duplicates : (Ident.t * Exp.t) list -> subst
(** like subst_of_list, but allow duplicate ids and only keep the first occurrence *)
val sub_to_list : exp_subst -> (Ident.t * Exp.t) list
val sub_to_list : subst -> (Ident.t * Exp.t) list
(** Convert a subst to a list of pairs. *)
val sub_empty : subst
(** The empty substitution. *)
val exp_sub_empty : exp_subst
val is_sub_empty : subst -> bool
(* let to_exp_subst : [< `Exp exp_subst] => exp_subst; *)
val sub_join : exp_subst -> exp_subst -> exp_subst
val sub_join : subst -> subst -> subst
(** Compute the common id-exp part of two inputs [subst1] and [subst2].
The first component of the output is this common part.
The second and third components are the remainder of [subst1]
and [subst2], respectively. *)
val sub_symmetric_difference : exp_subst -> exp_subst -> exp_subst * exp_subst * exp_subst
val sub_symmetric_difference : subst -> subst -> subst * subst * subst
(** Compute the common id-exp part of two inputs [subst1] and [subst2].
The first component of the output is this common part.
The second and third components are the remainder of [subst1]
and [subst2], respectively. *)
val sub_find : (Ident.t -> bool) -> exp_subst -> Exp.t
val sub_find : (Ident.t -> bool) -> subst -> Exp.t
(** [sub_find filter sub] returns the expression associated to the first identifier
that satisfies [filter].
Raise [Not_found] if there isn't one. *)
val sub_filter : (Ident.t -> bool) -> exp_subst -> exp_subst
val sub_filter : (Ident.t -> bool) -> subst -> subst
(** [sub_filter filter sub] restricts the domain of [sub] to the
identifiers satisfying [filter]. *)
val sub_filter_pair : exp_subst -> f:(Ident.t * Exp.t -> bool) -> exp_subst
val sub_filter_pair : subst -> f:(Ident.t * Exp.t -> bool) -> subst
(** [sub_filter_exp filter sub] restricts the domain of [sub] to the
identifiers satisfying [filter(id, sub(id))]. *)
val sub_range_partition : (Exp.t -> bool) -> exp_subst -> exp_subst * exp_subst
val sub_range_partition : (Exp.t -> bool) -> subst -> subst * subst
(** [sub_range_partition filter sub] partitions [sub] according to
whether range expressions satisfy [filter]. *)
val sub_domain_partition : (Ident.t -> bool) -> exp_subst -> exp_subst * exp_subst
val sub_domain_partition : (Ident.t -> bool) -> subst -> subst * subst
(** [sub_domain_partition filter sub] partitions [sub] according to
whether domain identifiers satisfy [filter]. *)
val sub_domain : exp_subst -> Ident.t list
val sub_domain : subst -> Ident.t list
(** Return the list of identifiers in the domain of the substitution. *)
val sub_range : exp_subst -> Exp.t list
val sub_range : subst -> Exp.t list
(** Return the list of expressions in the range of the substitution. *)
val sub_range_map : (Exp.t -> Exp.t) -> exp_subst -> exp_subst
val sub_range_map : (Exp.t -> Exp.t) -> subst -> subst
(** [sub_range_map f sub] applies [f] to the expressions in the range of [sub]. *)
val sub_map : (Ident.t -> Ident.t) -> (Exp.t -> Exp.t) -> exp_subst -> exp_subst
val sub_map : (Ident.t -> Ident.t) -> (Exp.t -> Exp.t) -> subst -> subst
(** [sub_map f g sub] applies the renaming [f] to identifiers in the domain
of [sub] and the substitution [g] to the expressions in the range of [sub]. *)
val extend_sub : exp_subst -> Ident.t -> Exp.t -> exp_subst option
val extend_sub : subst -> Ident.t -> Exp.t -> subst option
(** Extend substitution and return [None] if not possible. *)
val exp_subst_free_vars : exp_subst -> Ident.t Sequence.t
val subst_free_vars : subst -> Ident.t Sequence.t
val exp_subst_gen_free_vars : exp_subst -> (unit, Ident.t) Sequence.Generator.t
val subst_gen_free_vars : subst -> (unit, Ident.t) Sequence.Generator.t
(** substitution functions
WARNING: these functions do not ensure that the results are normalized. *)

10
infer/src/IR/Subtype.ml
Unescape View File

@ -32,16 +32,6 @@ type result = No | Unknown | Yes [@@deriving compare]
let equal_result = [%compare.equal: result]
let sub_type tname_subst st_pair =
let st, kind = st_pair in
match st with
| Subtypes tnames ->
let tnames' = IList.map_changed ~equal:Typ.Name.equal ~f:tname_subst tnames in
if phys_equal tnames tnames' then st_pair else (Subtypes tnames', kind)
| Exact ->
st_pair
let max_result res1 res2 = if compare_result res1 res2 <= 0 then res2 else res1
let is_interface tenv (class_name : Typ.Name.t) =

2
infer/src/IR/Subtype.mli
Unescape View File

@ -15,8 +15,6 @@ type t [@@deriving compare]
val pp : F.formatter -> t -> unit
val sub_type : (Typ.Name.t -> Typ.Name.t) -> t -> t
val exact : t
val subtypes : t

63
infer/src/IR/Typ.ml
Unescape View File

@ -150,8 +150,6 @@ module T = struct
let equal_quals = [%compare.equal: type_quals]
let equal_template_arg = [%compare.equal: template_arg]
let equal = [%compare.equal: t]
end
@ -186,12 +184,6 @@ let void = mk Tvoid
let void_star = mk (Tptr (mk Tvoid, Pk_pointer))
let merge_quals quals1 quals2 =
{ is_const= quals1.is_const || quals2.is_const
; is_restrict= quals1.is_restrict || quals2.is_restrict
; is_volatile= quals1.is_volatile || quals2.is_volatile }
let escape pe = if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Escape.escape_xml else ident
(** Pretty print a type with all the details, using the C syntax. *)
@ -269,51 +261,6 @@ let to_string typ =
F.asprintf "%t" pp
type type_subst_t = (string * t) list [@@deriving compare]
let is_type_subst_empty = List.is_empty
(** Given the template type mapping and the type, substitute tvars within the type. *)
let rec sub_type subst generic_typ : t =
match generic_typ.desc with
| TVar tname -> (
match List.Assoc.find subst ~equal:String.equal tname with
| Some t ->
(* Type qualifiers may come from original type or be part of substitution. Merge them *)
mk ~quals:(merge_quals t.quals generic_typ.quals) t.desc
| None ->
generic_typ )
| Tarray {elt= typ; length; stride} ->
let typ' = sub_type subst typ in
if phys_equal typ typ' then generic_typ
else mk_array ~default:generic_typ typ' ?length ?stride
| Tptr (typ, arg) ->
let typ' = sub_type subst typ in
if phys_equal typ typ' then generic_typ else mk ~default:generic_typ (Tptr (typ', arg))
| Tstruct tname ->
let tname' = sub_tname subst tname in
if phys_equal tname tname' then generic_typ else mk ~default:generic_typ (Tstruct tname')
| _ ->
generic_typ
and sub_tname subst tname =
match tname with
| CppClass (name, Template {mangled; args}) ->
let sub_typ_opt typ_opt =
match typ_opt with
| TType typ ->
let typ' = sub_type subst typ in
if phys_equal typ typ' then typ_opt else TType typ'
| TInt _ | TNull | TNullPtr | TOpaque ->
typ_opt
in
let args' = IList.map_changed ~equal:equal_template_arg ~f:sub_typ_opt args in
if phys_equal args args' then tname else CppClass (name, Template {mangled; args= args'})
| _ ->
tname
module Name = struct
type t = name [@@deriving compare]
@ -1348,16 +1295,6 @@ module Fieldname = struct
let pp f = function Java field_name | Clang {field_name} -> Format.pp_print_string f field_name
let class_name_replace fname ~f =
match fname with
| Clang {class_name; field_name} ->
let class_name' = f class_name in
if phys_equal class_name class_name' then fname
else Clang {class_name= class_name'; field_name}
| _ ->
fname
let clang_get_qual_class = function
| Clang {class_name} ->
Some (Name.qual_name class_name)

11
infer/src/IR/Typ.mli
Unescape View File

@ -120,9 +120,6 @@ val void : t
val void_star : t
(** void* type *)
(** Stores information about type substitution *)
type type_subst_t [@@deriving compare]
module Name : sig
(** Named types. *)
type t = name [@@deriving compare]
@ -228,12 +225,6 @@ val equal_desc : desc -> desc -> bool
val equal_quals : type_quals -> type_quals -> bool
val sub_type : type_subst_t -> t -> t
val sub_tname : type_subst_t -> Name.t -> Name.t
val is_type_subst_empty : type_subst_t -> bool
val pp_full : Pp.env -> F.formatter -> t -> unit
(** Pretty print a type with all the details. *)
@ -611,8 +602,6 @@ module Fieldname : sig
val to_full_string : t -> string
val class_name_replace : t -> f:(Name.t -> Name.t) -> t
val to_simplified_string : t -> string
(** Convert a fieldname to a simplified string with at most one-level path. *)

36
infer/src/biabduction/Abs.ml
Unescape View File

@ -20,8 +20,8 @@ type rule =
; r_sigma: Match.hpred_pat list
; (* sigma should be in a specific order *)
r_new_sigma: Sil.hpred list
; r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Sil.exp_subst -> Sil.atom list
; r_condition: Prop.normal Prop.t -> Sil.exp_subst -> bool }
; r_new_pi: Prop.normal Prop.t -> Prop.normal Prop.t -> Sil.subst -> Sil.atom list
; r_condition: Prop.normal Prop.t -> Sil.subst -> bool }
let sigma_rewrite tenv p r : Prop.normal Prop.t option =
match Match.prop_match_with_impl tenv p r.r_condition r.r_vars r.r_root r.r_sigma with
@ -31,7 +31,7 @@ let sigma_rewrite tenv p r : Prop.normal Prop.t option =
if not (r.r_condition p_leftover sub) then None
else
let res_pi = r.r_new_pi p p_leftover sub in
let res_sigma = Prop.sigma_sub (`Exp sub) r.r_new_sigma in
let res_sigma = Prop.sigma_sub sub r.r_new_sigma in
let p_with_res_pi = List.fold ~f:(Prop.prop_atom_and tenv) ~init:p_leftover res_pi in
let p_new = Prop.prop_sigma_star p_with_res_pi res_sigma in
Some (Prop.normalize tenv p_new)
@ -56,7 +56,7 @@ let create_fresh_primeds_ls para =
(ids_tuple, exps_tuple)
let create_condition_ls ids_private id_base p_leftover (inst : Sil.exp_subst) =
let create_condition_ls ids_private id_base p_leftover (inst : Sil.subst) =
let insts_of_private_ids, insts_of_public_ids, inst_of_base =
let f id' = List.exists ~f:(fun id'' -> Ident.equal id' id'') ids_private in
let inst_private, inst_public = Sil.sub_domain_partition f inst in
@ -117,7 +117,7 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para : Sil.hpara) =
(ids, para_body_hpats)
in
let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
let gen_pi_res _ _ (_ : Sil.subst) = [] in
let condition =
let ids_private = id_next :: (ids_exist_fst @ ids_exist_snd) in
create_condition_ls ids_private id_base
@ -148,7 +148,7 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para =
{Match.hpred= Prop.mk_lseg tenv k2 para exp_next exp_end exps_shared; Match.flag= impl_ok2}
in
let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
let gen_pi_res _ _ (_ : Sil.subst) = [] in
let condition =
let ids_private = id_next :: ids_exist in
create_condition_ls ids_private id_base
@ -175,7 +175,7 @@ let mk_rule_lspts_ls tenv k1 impl_ok1 impl_ok2 para =
(ids, para_body_pat)
in
let lseg_res = Prop.mk_lseg tenv Sil.Lseg_NE para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
let gen_pi_res _ _ (_ : Sil.subst) = [] in
let condition =
let ids_private = id_next :: ids_exist in
create_condition_ls ids_private id_base
@ -208,7 +208,7 @@ let mk_rule_lsls_ls tenv k1 k2 impl_ok1 impl_ok2 para =
in
let k_res = lseg_kind_add k1 k2 in
let lseg_res = Prop.mk_lseg tenv k_res para exp_base exp_end exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) =
let gen_pi_res _ _ (_ : Sil.subst) =
[]
(*
let inst_base, inst_next, inst_end =
@ -295,7 +295,7 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para =
(ids, para_body_hpats)
in
let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
let gen_pi_res _ _ (_ : Sil.subst) = [] in
let condition =
(* for the case of ptspts since iF'=iB therefore iF' cannot be private*)
let ids_private = ids_exist_fst @ ids_exist_snd in
@ -346,7 +346,7 @@ let mk_rule_ptsdll_dll tenv k2 impl_ok1 impl_ok2 para =
; Match.flag= impl_ok2 }
in
let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iB exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
let gen_pi_res _ _ (_ : Sil.subst) = [] in
let condition =
let ids_private = id_iF' :: ids_exist in
create_condition_dll ids_private id_iF
@ -386,7 +386,7 @@ let mk_rule_dllpts_dll tenv k1 impl_ok1 impl_ok2 para =
; Match.flag= impl_ok1 }
in
let dllseg_res = Prop.mk_dllseg tenv Sil.Lseg_NE para exp_iF exp_oB exp_oF exp_iF' exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
let gen_pi_res _ _ (_ : Sil.subst) = [] in
let condition =
let ids_private = id_oB' :: ids_exist in
create_condition_dll ids_private id_iF
@ -428,7 +428,7 @@ let mk_rule_dlldll_dll tenv k1 k2 impl_ok1 impl_ok2 para =
in
let k_res = lseg_kind_add k1 k2 in
let lseg_res = Prop.mk_dllseg tenv k_res para exp_iF exp_oB exp_oF exp_iB exps_shared in
let gen_pi_res _ _ (_ : Sil.exp_subst) = [] in
let gen_pi_res _ _ (_ : Sil.subst) = [] in
let condition =
let ids_private = [id_iF'; id_oB'] in
create_condition_dll ids_private id_iF
@ -677,11 +677,11 @@ let set_current_rules rules = Global.current_rules := rules
let reset_current_rules () = Global.current_rules := []
let eqs_sub subst eqs =
List.map ~f:(fun (e1, e2) -> (Sil.exp_sub (`Exp subst) e1, Sil.exp_sub (`Exp subst) e2)) eqs
List.map ~f:(fun (e1, e2) -> (Sil.exp_sub subst e1, Sil.exp_sub subst e2)) eqs
let eqs_solve ids_in eqs_in =
let rec solve (sub : Sil.exp_subst) (eqs : (Exp.t * Exp.t) list) : Sil.exp_subst option =
let rec solve (sub : Sil.subst) (eqs : (Exp.t * Exp.t) list) : Sil.subst option =
let do_default id e eqs_rest =
if not (List.exists ~f:(fun id' -> Ident.equal id id') ids_in) then None
else
@ -719,7 +719,7 @@ let eqs_solve ids_in eqs_in =
let filter id = not (List.exists ~f:(fun id' -> Ident.equal id id') sub_dom) in
List.filter ~f:filter ids_in
in
match solve Sil.exp_sub_empty eqs_in with None -> None | Some sub -> Some (compute_ids sub, sub)
match solve Sil.sub_empty eqs_in with None -> None | Some sub -> Some (compute_ids sub, sub)
let sigma_special_cases_eqs sigma =
@ -757,7 +757,7 @@ let sigma_special_cases ids sigma : (Ident.t list * Sil.hpred list) list =
| None ->
acc
| Some (ids_res, sub) ->
(ids_res, List.map ~f:(Sil.hpred_sub (`Exp sub)) sigma_cur) :: acc
(ids_res, List.map ~f:(Sil.hpred_sub sub) sigma_cur) :: acc
in
List.fold ~f ~init:[] special_cases_eqs
in
@ -891,7 +891,7 @@ let abstract_pure_part tenv p ~(from_abstract_footprint : bool) =
List.rev new_pure
in
let new_pure = do_pure (Prop.get_pure p) in
let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.exp_sub_empty in
let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.sub_empty in
let eprop'' =
if !BiabductionConfig.footprint && not from_abstract_footprint then
let new_pi_footprint = do_pure p.Prop.pi_fp in
@ -1142,7 +1142,7 @@ let check_junk pname tenv prop =
else remove_junk fp_part fav_root sigma'
in
let sigma_new =
let fav_sub = Sil.exp_subst_free_vars prop.Prop.sub |> Ident.set_of_sequence in
let fav_sub = Sil.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

3
infer/src/biabduction/Absarray.ml
Unescape View File

@ -650,8 +650,7 @@ let remove_redundant_elements tenv prop =
let occurs_at_most_once : Ident.t -> bool =
let fav_curr =
let ( @@@ ) = Sequence.append in
Sil.exp_subst_free_vars prop.Prop.sub
@@@ Prop.pi_free_vars prop.Prop.pi
Sil.subst_free_vars prop.Prop.sub @@@ Prop.pi_free_vars prop.Prop.pi
@@@ Prop.sigma_free_vars prop.Prop.sigma
in
let fav_foot =

3
infer/src/biabduction/Attribute.ml
Unescape View File

@ -307,8 +307,7 @@ let deallocate_stack_vars tenv (p : 'a Prop.t) pvars =
let pi = List.map ~f:(Sil.atom_replace_exp exp_replace) (p.pi @ pi1) in
let p' =
Prop.normalize tenv
(Prop.set p ~sub:Sil.exp_sub_empty
~sigma:(Prop.sigma_replace_exp tenv exp_replace sigma_other))
(Prop.set p ~sub:Sil.sub_empty ~sigma:(Prop.sigma_replace_exp tenv exp_replace sigma_other))
in
let p'' =
let res = ref p' in

14
infer/src/biabduction/Dom.ml
Unescape View File

@ -524,9 +524,9 @@ module Rename : sig
val lookup_list_todo : side -> Exp.t list -> Exp.t list
val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.exp_subst
val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.subst
val to_subst_emb : side -> Sil.exp_subst
val to_subst_emb : side -> Sil.subst
(*
val get : Exp.t -> Exp.t -> Exp.t option
val pp : printenv -> Format.formatter -> (Exp.t * Exp.t * Exp.t) list -> unit
@ -652,7 +652,7 @@ end = struct
in
if find_duplicates sub_list_side_sorted then (
L.d_strln "failure reason 11" ; raise Sil.JoinFail )
else Sil.exp_subst_of_list sub_list_side
else Sil.subst_of_list sub_list_side
let to_subst_emb (side : side) =
@ -679,7 +679,7 @@ end = struct
false
in
if find_duplicates sub_list_sorted then ( L.d_strln "failure reason 12" ; raise Sil.JoinFail )
else Sil.exp_subst_of_list sub_list_sorted
else Sil.subst_of_list sub_list_sorted
let get_others' f_lookup side e =
@ -1376,7 +1376,7 @@ let sigma_renaming_check (lhs : side) (sigma : Prop.sigma) (sigma_new : Prop.sig
* and check that the renaming of primed vars is injective *)
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
let sigma' = Prop.sigma_sub sub sigma_new in
equal_sigma sigma sigma'
@ -1785,7 +1785,7 @@ let pi_partial_meet tenv (p : Prop.normal Prop.t) (ep1 : 'a Prop.t) (ep2 : 'b Pr
let dom2 = Ident.idlist_to_idset (Sil.sub_domain sub2) in
let handle_atom sub dom 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
Sil.atom_sub 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
@ -1815,7 +1815,7 @@ let eprop_partial_meet tenv (ep1 : 'a Prop.t) (ep2 : 'b Prop.t) : 'c Prop.t =
let sub2 = ep2.Prop.sub in
let range1 = Sil.sub_range sub1 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
Sil.equal_subst sub1 sub2 && List.for_all ~f range1
in
if not (sub_check ()) then ( L.d_strln "sub_check() failed" ; raise Sil.JoinFail )
else

42
infer/src/biabduction/Match.ml
Unescape View File

@ -21,9 +21,9 @@ type hpred_pat = {hpred: Sil.hpred; flag: bool}
(** Checks e1 = e2[sub ++ sub'] for some sub' with dom(sub') subseteq vars.
Returns (sub ++ sub', vars - dom(sub')). *)
let rec exp_match e1 sub vars e2 : (Sil.exp_subst * Ident.t list) option =
let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
let check_equal sub vars e1 e2 =
let e2_inst = Sil.exp_sub (`Exp sub) e2 in
let e2_inst = Sil.exp_sub sub e2 in
if Exp.equal e1 e2_inst then Some (sub, vars) else None
in
match (e1, e2) with
@ -97,7 +97,7 @@ let exp_list_match es1 sub vars es2 =
dom(sub') subseteq vars. Returns (sub ++ sub', vars - dom(sub')).
WARNING: This function does not consider the fact that the analyzer
sometimes forgets fields of hpred. It can possibly cause a problem. *)
let rec strexp_match sexp1 sub vars sexp2 : (Sil.exp_subst * Ident.t list) option =
let rec strexp_match sexp1 sub vars sexp2 : (Sil.subst * Ident.t list) option =
match (sexp1, sexp2) with
| Sil.Eexp (exp1, _), Sil.Eexp (exp2, _) ->
exp_match exp1 sub vars exp2
@ -148,7 +148,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 idx2 = Sil.exp_sub sub idx2 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
@ -168,13 +168,13 @@ and isel_match isel1 sub vars isel2 =
(* extends substitution sub by creating a new substitution for vars *)
let sub_extend_with_ren (sub : Sil.exp_subst) vars =
let sub_extend_with_ren (sub : Sil.subst) vars =
let f id = (id, Exp.Var (Ident.create_fresh Ident.kprimed)) in
let renaming_for_vars = Sil.exp_subst_of_list (List.map ~f vars) in
let renaming_for_vars = Sil.subst_of_list (List.map ~f vars) in
Sil.sub_join sub renaming_for_vars
type sidecondition = Prop.normal Prop.t -> Sil.exp_subst -> bool
type sidecondition = Prop.normal Prop.t -> Sil.subst -> bool
let rec execute_with_backtracking = function
| [] ->
@ -186,7 +186,7 @@ let rec execute_with_backtracking = function
match res_f with None -> execute_with_backtracking fs | Some _ -> res_f )
let rec instantiate_to_emp p condition (sub : Sil.exp_subst) vars = function
let rec instantiate_to_emp p condition (sub : Sil.subst) vars = function
| [] ->
if condition p sub then Some (sub, p) else None
| hpat :: hpats -> (
@ -201,7 +201,7 @@ let rec instantiate_to_emp p condition (sub : Sil.exp_subst) vars = function
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
let e1' = Sil.exp_sub sub e1 in
match exp_match e1' sub vars e2 with
| None ->
None
@ -213,8 +213,8 @@ let rec instantiate_to_emp p condition (sub : Sil.exp_subst) vars = function
in
if not fully_instantiated then None
else
let iF' = Sil.exp_sub (`Exp sub) iF in
let oB' = Sil.exp_sub (`Exp sub) oB in
let iF' = Sil.exp_sub sub iF in
let oB' = Sil.exp_sub sub oB in
match exp_list_match [iF'; oB'] sub vars [oF; iB] with
| None ->
None
@ -333,7 +333,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
in
if not fully_instantiated_start2 then None
else
let e_start2' = Sil.exp_sub (`Exp sub) e_start2 in
let e_start2' = Sil.exp_sub sub e_start2 in
match (exp_match e_start2' sub vars e_end2, hpats) with
| None, _ ->
(*
@ -402,8 +402,8 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
in
if not fully_instantiated_iFoB2 then None
else
let iF2' = Sil.exp_sub (`Exp sub) iF2 in
let oB2' = Sil.exp_sub (`Exp sub) oB2 in
let iF2' = Sil.exp_sub sub iF2 in
let oB2' = Sil.exp_sub sub oB2 in
match (exp_list_match [iF2'; oB2'] sub vars [oF2; iB2], hpats) with
| None, _ ->
None
@ -419,7 +419,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
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
let iF2' = Sil.exp_sub sub iF2 in
match exp_match iF2' sub vars iB2 with
| None ->
None
@ -495,23 +495,19 @@ and hpara_common_match_with_impl tenv impl_ok ids1 sigma1 eids2 ids2 sigma2 =
let sub_eids = List.map ~f:(fun (id2, id1) -> (id2, Exp.Var id1)) ren_eids in
(sub_eids, eids_fresh)
in
let sub = Sil.exp_subst_of_list (sub_ids @ sub_eids) in
let sub = Sil.subst_of_list (sub_ids @ sub_eids) in
match sigma2 with
| [] ->
if List.is_empty sigma1 then true else false
| hpred2 :: sigma2 -> (
let hpat2, hpats2 =
let hpred2_ren, sigma2_ren =
(Sil.hpred_sub (`Exp sub) hpred2, Prop.sigma_sub (`Exp sub) sigma2)
in
let hpred2_ren, sigma2_ren = (Sil.hpred_sub sub hpred2, Prop.sigma_sub sub sigma2) in
let allow_impl hpred = {hpred; flag= impl_ok} in
(allow_impl hpred2_ren, List.map ~f:allow_impl sigma2_ren)
in
let condition _ _ = true in
let p1 = Prop.normalize tenv (Prop.from_sigma sigma1) in
match
prop_match_with_impl_sub tenv p1 condition Sil.exp_sub_empty eids_fresh hpat2 hpats2
with
match prop_match_with_impl_sub tenv p1 condition Sil.sub_empty eids_fresh hpat2 hpats2 with
| None ->
false
| Some (_, p1') when Prop.prop_is_emp p1' ->
@ -551,7 +547,7 @@ and hpara_dll_match_with_impl tenv impl_ok para1 para2 : bool =
2) [p |- (hpat.hpred * hpats.hpred)[subst] * p_leftover].
Using the flag [field], we can control the strength of |-. *)
let prop_match_with_impl tenv p condition vars hpat hpats =
prop_match_with_impl_sub tenv p condition Sil.exp_sub_empty vars hpat hpats
prop_match_with_impl_sub tenv p condition Sil.sub_empty vars hpat hpats
let sigma_remove_hpred eq sigma e =

4
infer/src/biabduction/Match.mli
Unescape View File

@ -25,7 +25,7 @@ val hpara_dll_match_with_impl : Tenv.t -> bool -> Sil.hpara_dll -> Sil.hpara_dll
considered during pattern matching. *)
type hpred_pat = {hpred: Sil.hpred; flag: bool}
type sidecondition = Prop.normal Prop.t -> Sil.exp_subst -> bool
type sidecondition = Prop.normal Prop.t -> Sil.subst -> bool
val prop_match_with_impl :
Tenv.t
@ -34,7 +34,7 @@ val prop_match_with_impl :
-> Ident.t list
-> hpred_pat
-> hpred_pat list
-> (Sil.exp_subst * Prop.normal Prop.t) option
-> (Sil.subst * Prop.normal Prop.t) option
(** [prop_match_with_impl p condition vars hpat hpats]
returns [(subst, p_leftover)] such that
1) [dom(subst) = vars]

82
infer/src/biabduction/Prop.ml
Unescape View File

@ -41,7 +41,7 @@ module Core : sig
(** the kind 'a should range over [normal] and [exposed] *)
type 'a t = private
{ sigma: sigma (** spatial part *)
; sub: Sil.exp_subst (** substitution *)
; sub: Sil.subst (** substitution *)
; pi: pi (** pure part *)
; sigma_fp: sigma (** abduced spatial part *)
; pi_fp: pi (** abduced pure part *) }
@ -51,13 +51,7 @@ module Core : sig
(** Proposition [true /\ emp]. *)
val set :
?sub:Sil.exp_subst
-> ?pi:pi
-> ?sigma:sigma
-> ?pi_fp:pi
-> ?sigma_fp:sigma
-> 'a t
-> exposed t
?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t
(** Set individual fields of the prop. *)
val unsafe_cast_to_normal : exposed t -> normal t
@ -74,14 +68,14 @@ end = struct
normalized. *)
type 'a t =
{ sigma: sigma (** spatial part *)
; sub: Sil.exp_subst (** substitution *)
; sub: Sil.subst (** substitution *)
; pi: pi (** pure part *)
; sigma_fp: sigma (** abduced spatial part *)
; pi_fp: pi (** abduced pure part *) }
[@@deriving compare]
(** Proposition [true /\ emp]. *)
let prop_emp : normal t = {sub= Sil.exp_sub_empty; pi= []; sigma= []; pi_fp= []; sigma_fp= []}
let prop_emp : normal t = {sub= Sil.sub_empty; pi= []; sigma= []; pi_fp= []; sigma_fp= []}
let set ?sub ?pi ?sigma ?pi_fp ?sigma_fp p =
let set_ p ?(sub = p.sub) ?(pi = p.pi) ?(sigma = p.sigma) ?(pi_fp = p.pi_fp)
@ -134,12 +128,9 @@ let pp_hpred_stackvar pe0 f (hpred : Sil.hpred) =
(** Pretty print a substitution. *)
let pp_sub pe f = function
| `Exp sub ->
let pi_sub = List.map ~f:(fun (id, e) -> Sil.Aeq (Var id, e)) (Sil.sub_to_list sub) in
Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe) f pi_sub
| `Typ _ ->
F.pp_print_string f "Printing typ_subst not implemented."
let pp_sub pe f sub =
let pi_sub = List.map ~f:(fun (id, e) -> Sil.Aeq (Var id, e)) (Sil.sub_to_list sub) in
Pp.semicolon_seq ~print_env:{pe with break_lines= false} (Sil.pp_atom pe) f pi_sub
(** Dump a substitution. *)
@ -375,7 +366,7 @@ let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} =
>>= fun () ->
sigma_gen_free_vars sigma_fp
>>= fun () ->
Sil.exp_subst_gen_free_vars sub
Sil.subst_gen_free_vars sub
>>= fun () -> pi_gen_free_vars pi >>= fun () -> pi_gen_free_vars pi_fp
@ -1288,7 +1279,7 @@ module Normalize = struct
let normalize_and_strengthen_atom tenv (p : normal t) (a : Sil.atom) : Sil.atom =
let a' = atom_normalize tenv (`Exp p.sub) a in
let a' = atom_normalize tenv p.sub a in
match a' with
| Aeq (BinOp (Le, Var id, Const (Cint n)), Const (Cint i)) when IntLit.isone i ->
let lower = Exp.int (n -- IntLit.one) in
@ -1678,7 +1669,7 @@ module Normalize = struct
let sub_normalize sub =
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'
if Sil.equal_subst sub sub' then sub else sub'
(** Conjoin a pure atomic predicate by normal conjunction. *)
@ -1692,15 +1683,12 @@ module Normalize = struct
p
| Aeq (Var i, e) ->
let sub_list = [(i, e)] in
let mysub = Sil.exp_subst_of_list sub_list in
let mysub = Sil.subst_of_list sub_list in
let p_sub = Sil.sub_filter (fun i' -> not (Ident.equal i i')) p.sub in
let exp_sub' =
Sil.sub_join mysub (Sil.sub_range_map (Sil.exp_sub (`Exp mysub)) p_sub)
in
let sub' = `Exp exp_sub' in
let sub' = Sil.sub_join mysub (Sil.sub_range_map (Sil.exp_sub mysub) p_sub) in
let nsub', npi', nsigma' =
let nsigma' = sigma_normalize tenv sub' p.sigma in
(sub_normalize exp_sub', pi_normalize tenv sub' nsigma' p.pi, nsigma')
(sub_normalize sub', pi_normalize tenv sub' nsigma' p.pi, nsigma')
in
let eqs_zero, nsigma'' = sigma_remove_emptylseg nsigma' in
let p' = unsafe_cast_to_normal (set p ~sub:nsub' ~pi:npi' ~sigma:nsigma'') in
@ -1709,10 +1697,10 @@ module Normalize = struct
p
| Aneq (e1, e2) ->
let sigma' = sigma_intro_nonemptylseg e1 e2 p.sigma in
let pi' = pi_normalize tenv (`Exp p.sub) sigma' (a' :: p.pi) in
let pi' = pi_normalize tenv p.sub sigma' (a' :: p.pi) in
unsafe_cast_to_normal (set p ~pi:pi' ~sigma:sigma')
| _ ->
let pi' = pi_normalize tenv (`Exp p.sub) p.sigma (a' :: p.pi) in
let pi' = pi_normalize tenv p.sub p.sigma (a' :: p.pi) in
unsafe_cast_to_normal (set p ~pi:pi')
in
if not footprint then p'
@ -1744,7 +1732,7 @@ end
let exp_normalize_prop ?destructive tenv prop exp =
BiabductionConfig.run_with_abs_val_equal_zero
(Normalize.exp_normalize ?destructive tenv (`Exp prop.sub))
(Normalize.exp_normalize ?destructive tenv prop.sub)
exp
@ -1762,15 +1750,11 @@ let lexp_normalize_prop tenv p lexp =
let atom_normalize_prop tenv prop atom =
BiabductionConfig.run_with_abs_val_equal_zero
(Normalize.atom_normalize tenv (`Exp prop.sub))
atom
BiabductionConfig.run_with_abs_val_equal_zero (Normalize.atom_normalize tenv prop.sub) atom
let sigma_normalize_prop tenv prop sigma =
BiabductionConfig.run_with_abs_val_equal_zero
(Normalize.sigma_normalize tenv (`Exp prop.sub))
sigma
BiabductionConfig.run_with_abs_val_equal_zero (Normalize.sigma_normalize tenv prop.sub) sigma
let sigma_replace_exp tenv epairs sigma =
@ -2004,15 +1988,14 @@ let compute_reindexing_from_indices list =
(id, exp_new)
in
let reindexing = List.map ~f:transform list_passed in
Sil.exp_subst_of_list reindexing
Sil.subst_of_list reindexing
let apply_reindexing tenv (exp_subst : Sil.exp_subst) prop =
let subst = `Exp exp_subst in
let apply_reindexing tenv (subst : Sil.subst) prop =
let nsigma = Normalize.sigma_normalize tenv subst prop.sigma in
let npi = Normalize.pi_normalize tenv subst nsigma prop.pi in
let nsub, atoms =
let dom_subst = List.map ~f:fst (Sil.sub_to_list exp_subst) in
let dom_subst = List.map ~f:fst (Sil.sub_to_list 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 = Exp.free_vars e |> Sequence.exists ~f:in_dom_subst in
@ -2235,8 +2218,8 @@ let prop_sub subst (prop : 'a t) : exposed t =
(** Apply renaming substitution to a proposition. *)
let prop_ren_sub tenv (ren_sub : Sil.exp_subst) (prop : normal t) : normal t =
Normalize.normalize tenv (prop_sub (`Exp ren_sub) prop)
let prop_ren_sub tenv (ren_sub : Sil.subst) (prop : normal t) : normal t =
Normalize.normalize tenv (prop_sub ren_sub prop)
(** Existentially quantify the [ids] in [prop]. [ids] should not contain any primed variables. If
@ -2247,7 +2230,7 @@ let exist_quantify tenv ?ids_queue ids (prop : normal t) : normal t =
if List.is_empty ids then prop
else
let gen_fresh_id_sub id = (id, Exp.Var (Ident.create_fresh Ident.kprimed)) in
let ren_sub = Sil.exp_subst_of_list (List.map ~f:gen_fresh_id_sub ids) in
let ren_sub = Sil.subst_of_list (List.map ~f:gen_fresh_id_sub ids) in
let prop' =
(* throw away x=E if x becomes x_ *)
let filter =
@ -2259,7 +2242,7 @@ let exist_quantify tenv ?ids_queue ids (prop : normal t) : normal t =
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)
if Sil.equal_subst sub prop.sub then prop else unsafe_cast_to_normal (set prop ~sub)
in
(*
L.out "@[<2>.... Existential Quantification ....@\n";
@ -2296,8 +2279,7 @@ let prop_primed_vars_to_normal_vars tenv (prop : normal t) : normal t =
|> 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)
Sil.subst_of_list (List.map ~f:(fun i -> (i, Exp.Var (Ident.create_fresh Ident.knormal))) ids)
in
prop_ren_sub tenv ren_sub prop
@ -2310,7 +2292,7 @@ let from_sigma sigma = set prop_emp ~sigma
(** Iterator state over sigma. *)
type 'a prop_iter =
{ pit_sub: Sil.exp_subst (** substitution for equalities *)
{ pit_sub: Sil.subst (** substitution for equalities *)
; pit_pi: pi (** pure part *)
; pit_newpi: (bool * Sil.atom) list (** newly added atoms. *)
; (* The first records !BiabductionConfig.footprint. *)
@ -2362,7 +2344,7 @@ let prop_iter_add_atom footprint iter atom =
associated to the resulting iterator *)
let prop_iter_remove_curr_then_to_prop tenv iter : normal t =
let sigma = List.rev_append iter.pit_old iter.pit_new in
let normalized_sigma = Normalize.sigma_normalize tenv (`Exp iter.pit_sub) sigma in
let normalized_sigma = Normalize.sigma_normalize tenv iter.pit_sub sigma in
let prop =
set prop_emp ~sub:iter.pit_sub ~pi:iter.pit_pi ~sigma:normalized_sigma ~pi_fp:iter.pit_pi_fp
~sigma_fp:iter.pit_sigma_fp
@ -2372,7 +2354,7 @@ let prop_iter_remove_curr_then_to_prop tenv iter : normal t =
(** Return the current hpred and state. *)
let prop_iter_current tenv iter =
let curr = Normalize.hpred_normalize tenv (`Exp iter.pit_sub) iter.pit_curr in
let curr = Normalize.hpred_normalize tenv iter.pit_sub iter.pit_curr in
let prop = unsafe_cast_to_normal (set prop_emp ~sigma:[curr]) in
let prop' =
List.fold
@ -2457,7 +2439,7 @@ let prop_iter_make_id_primed tenv id iter =
let pairs_unpid, pairs_pid = split [] [] eqs in
match pairs_pid with
| [] ->
let sub_unpid = Sil.exp_subst_of_list pairs_unpid in
let sub_unpid = Sil.subst_of_list pairs_unpid in
let pairs = (id, Exp.Var pid) :: pairs_unpid in
(sub_unpid, Sil.subst_of_list pairs, [])
| (id1, e1) :: _ ->
@ -2465,7 +2447,7 @@ let prop_iter_make_id_primed tenv id iter =
let pairs_unpid' =
List.map ~f:(fun (id', e') -> (id', Sil.exp_sub sub_id1 e')) pairs_unpid
in
let sub_unpid = Sil.exp_subst_of_list pairs_unpid' in
let sub_unpid = Sil.subst_of_list pairs_unpid' in
let pairs = (id, e1) :: pairs_unpid' in
(sub_unpid, Sil.subst_of_list pairs, get_eqs [] pairs_pid)
in
@ -2490,7 +2472,7 @@ let prop_iter_footprint_free_vars iter =
(** Find fav of the iterator *)
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
Sil.subst_gen_free_vars pit_sub
>>= fun () ->
pi_gen_free_vars pit_pi
>>= fun () ->

4
infer/src/biabduction/Prop.mli
Unescape View File

@ -30,7 +30,7 @@ type sigma = Sil.hpred list
(** the kind 'a should range over [normal] and [exposed] *)
type 'a t = private
{ sigma: sigma (** spatial part *)
; sub: Sil.exp_subst (** substitution *)
; sub: Sil.subst (** substitution *)
; pi: pi (** pure part *)
; sigma_fp: sigma (** abduced spatial part *)
; pi_fp: pi (** abduced pure part *) }
@ -260,7 +260,7 @@ val from_sigma : sigma -> exposed t
(** Build an exposed prop from sigma *)
val set :
?sub:Sil.exp_subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t
?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sigma -> 'a t -> exposed t
(** Set individual fields of the prop. *)
(** {2 Prop iterators} *)

97
infer/src/biabduction/Prover.ml
Unescape View File

@ -1060,7 +1060,7 @@ let check_inconsistency_pi tenv pi =
(** {2 Abduction prover} *)
type subst2 = Sil.exp_subst * Sil.exp_subst
type subst2 = Sil.subst * Sil.subst
type exc_body =
| EXC_FALSE
@ -1310,25 +1310,22 @@ end = struct
L.d_ln ()
end
let d_impl (s1, s2) = ProverState.d_implication (`Exp s1, `Exp s2)
let d_impl_err (arg1, (s1, s2), arg3) =
ProverState.d_implication_error (arg1, (`Exp s1, `Exp s2), arg3)
let d_impl (s1, s2) = ProverState.d_implication (s1, s2)
let d_impl_err (arg1, (s1, s2), arg3) = ProverState.d_implication_error (arg1, (s1, s2), arg3)
(** extend a substitution *)
let extend_sub sub v e =
let new_exp_sub = Sil.exp_subst_of_list [(v, e)] in
let new_sub = `Exp new_exp_sub in
Sil.sub_join new_exp_sub (Sil.sub_range_map (Sil.exp_sub new_sub) sub)
let new_exp_sub = Sil.subst_of_list [(v, e)] in
Sil.sub_join new_exp_sub (Sil.sub_range_map (Sil.exp_sub new_exp_sub) sub)
(** Extend [sub1] and [sub2] to witnesses that each instance of
[e1[sub1]] is an instance of [e2[sub2]]. Raise IMPL_FALSE if not
possible. *)
let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
let e1 = Prop.exp_normalize_noabs tenv (`Exp (fst subs)) e1_in in
let e2 = Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2_in in
let e1 = Prop.exp_normalize_noabs tenv (fst subs) e1_in in
let e2 = Prop.exp_normalize_noabs tenv (snd subs) e2_in in
let var_imply (subs : subst2) v1 v2 : subst2 =
match (Ident.is_primed v1, Ident.is_primed v2) with
| false, false ->
@ -1340,7 +1337,7 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
| true, false ->
raise (IMPL_EXC ("exps", subs, EXC_FALSE_EXPS (e1, e2)))
| false, true ->
let sub2' = extend_sub (snd subs) v2 (Sil.exp_sub (`Exp (fst subs)) (Exp.Var v1)) in
let sub2' = extend_sub (snd subs) v2 (Sil.exp_sub (fst subs) (Exp.Var v1)) in
(fst subs, sub2')
| true, true ->
let v1' = Ident.create_fresh Ident.knormal in
@ -1514,7 +1511,7 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 :
in
(subs', fld_frame_opt, fld_missing_opt)
| Sil.Estruct _, Sil.Eexp (e2, _) -> (
let e2' = Sil.exp_sub (`Exp (snd subs)) e2 in
let e2' = Sil.exp_sub (snd subs) e2 in
match e2' with
| Exp.Var id2 when Ident.is_primed id2 ->
let id2' = Ident.create_fresh Ident.knormal in
@ -1624,8 +1621,8 @@ and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2
| _, [] ->
(subs, esel1, [])
| (e1, se1) :: esel1', (e2, se2) :: esel2' ->
let e1n = Prop.exp_normalize_noabs tenv (`Exp (fst subs)) e1 in
let e2n = Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2 in
let e1n = Prop.exp_normalize_noabs tenv (fst subs) e1 in
let e2n = Prop.exp_normalize_noabs tenv (snd subs) e2 in
let n = Exp.compare e1n e2n in
if n < 0 then array_imply tenv source calc_index_frame calc_missing subs esel1' esel2 typ2
else if n > 0 then
@ -1648,7 +1645,7 @@ and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2
and sexp_imply_nolhs tenv source calc_missing (subs : subst2) se2 typ2 =
match se2 with
| Sil.Eexp (e2_, _) -> (
let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in
let e2 = Sil.exp_sub (snd subs) e2_ in
match e2 with
| Exp.Var v2 when Ident.is_primed v2 ->
let v2' = path_to_id source in
@ -1694,7 +1691,7 @@ let filter_ne_lhs sub e0 = function
let filter_hpred sub hpred2 hpred1 =
match (Sil.hpred_sub (`Exp sub) hpred1, hpred2) with
match (Sil.hpred_sub sub hpred1, hpred2) with
| Sil.Hlseg (Sil.Lseg_NE, hpara1, e1, f1, el1), Sil.Hlseg (Sil.Lseg_PE, _, _, _, _) ->
if Sil.equal_hpred (Sil.Hlseg (Sil.Lseg_PE, hpara1, e1, f1, el1)) hpred2 then Some false
else None
@ -1734,9 +1731,9 @@ let move_primed_lhs_from_front subs sigma =
| [] ->
sigma
| hpred :: _ ->
if hpred_has_primed_lhs (`Exp (snd subs)) hpred then
if hpred_has_primed_lhs (snd subs) hpred then
let sigma_primed, sigma_unprimed =
List.partition_tf ~f:(hpred_has_primed_lhs (`Exp (snd subs))) sigma
List.partition_tf ~f:(hpred_has_primed_lhs (snd subs)) sigma
in
match sigma_unprimed with
| [] ->
@ -2060,7 +2057,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
subst2 * Prop.normal Prop.t =
match hpred2 with
| Sil.Hpointsto (e2_, se2, texp2) -> (
let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in
let e2 = Sil.exp_sub (snd subs) e2_ in
( match e2 with
| Exp.Lvar _ ->
()
@ -2074,7 +2071,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
| None ->
raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
| Some iter1 -> (
match Prop.prop_iter_find iter1 (filter_ne_lhs (`Exp (fst subs)) e2) with
match Prop.prop_iter_find iter1 (filter_ne_lhs (fst subs) e2) with
| None ->
raise (IMPL_EXC ("lhs does not have e|->", subs, EXC_FALSE_HPRED hpred2))
| Some iter1' -> (
@ -2129,7 +2126,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
in
L.d_decrease_indent 1 ; res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Sil.exp_sub (`Exp (fst subs)) iF1) e2 ->
when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 ->
(* Unroll dllseg forward *)
let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
let _, para_inst1 = Sil.hpara_dll_instantiate para1 iF1 oB1 n' elist1 in
@ -2146,7 +2143,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
in
L.d_decrease_indent 1 ; res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Sil.exp_sub (`Exp (fst subs)) iB1) e2 ->
when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 ->
(* Unroll dllseg backward *)
let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
let _, para_inst1 = Sil.hpara_dll_instantiate para1 iB1 n' oF1 elist1 in
@ -2166,7 +2163,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
assert false ) ) )
| Sil.Hlseg (k, para2, e2_, f2_, elist2_) -> (
(* for now ignore implications between PE and NE *)
let e2, f2 = (Sil.exp_sub (`Exp (snd subs)) e2_, Sil.exp_sub (`Exp (snd subs)) f2_) in
let e2, f2 = (Sil.exp_sub (snd subs) e2_, Sil.exp_sub (snd subs) f2_) in
( match e2 with
| Exp.Lvar _ ->
()
@ -2183,11 +2180,10 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
| Some iter1 -> (
match
Prop.prop_iter_find iter1
(filter_hpred (fst subs) (Sil.hpred_sub (`Exp (snd subs)) hpred2))
Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (snd subs) hpred2))
with
| None ->
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2_ in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in
let _, para_inst2 = Sil.hpara_instantiate para2 e2 f2 elist2 in
L.d_increase_indent 1 ;
let res =
@ -2197,7 +2193,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(* calc_missing is false as we're checking an instantiation of the original list *)
L.d_decrease_indent 1 ; res
| Some iter1' -> (
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2_ in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in
(* force instantiation of existentials *)
let subs' = exp_list_imply tenv calc_missing subs (f2 :: elist2) (f2 :: elist2) in
let prop1' = Prop.prop_iter_remove_curr_then_to_prop tenv iter1' in
@ -2234,8 +2230,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
raise (Exceptions.Abduction_case_not_implemented __POS__)
| Sil.Hdllseg (_, para2, iF2, oB2, oF2, iB2, elist2) -> (
(* for now ignore implications between PE and NE *)
let iF2, oF2 = (Sil.exp_sub (`Exp (snd subs)) iF2, Sil.exp_sub (`Exp (snd subs)) oF2) in
let iB2, oB2 = (Sil.exp_sub (`Exp (snd subs)) iB2, Sil.exp_sub (`Exp (snd subs)) oB2) in
let iF2, oF2 = (Sil.exp_sub (snd subs) iF2, Sil.exp_sub (snd subs) oF2) in
let iB2, oB2 = (Sil.exp_sub (snd subs) iB2, Sil.exp_sub (snd subs) oB2) in
( match oF2 with
| Exp.Lvar _ ->
()
@ -2259,11 +2255,10 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
| Some iter1 -> (
match
Prop.prop_iter_find iter1
(filter_hpred (fst subs) (Sil.hpred_sub (`Exp (snd subs)) hpred2))
Prop.prop_iter_find iter1 (filter_hpred (fst subs) (Sil.hpred_sub (snd subs) hpred2))
with
| None ->
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2 in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in
let _, para_inst2 =
if Exp.equal iF2 iB2 then Sil.hpara_dll_instantiate para2 iF2 oB2 oF2 elist2
else assert false
@ -2278,7 +2273,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
L.d_decrease_indent 1 ; res
| Some iter1' ->
(* Only consider implications between identical listsegs for now *)
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (`Exp (snd subs)) e) elist2 in
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in
(* force instantiation of existentials *)
let subs' =
exp_list_imply tenv calc_missing subs
@ -2298,7 +2293,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
let is_constant_string_class subs = function
(* if the hpred represents a constant string, return the string *)
| Sil.Hpointsto (e2_, _, _) -> (
let e2 = Sil.exp_sub (`Exp (snd subs)) e2_ in
let e2 = Sil.exp_sub (snd subs) e2_ in
match e2 with
| Exp.Const (Const.Cstr s) ->
Some (s, true)
@ -2432,7 +2427,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
| Sil.Hpointsto (e2_, se2, t) ->
let changed, calc_index_frame', hpred2' =
expand_hpred_pointer tenv calc_index_frame
(Sil.Hpointsto (Prop.exp_normalize_noabs tenv (`Exp (snd subs)) e2_, se2, t))
(Sil.Hpointsto (Prop.exp_normalize_noabs tenv (snd subs) e2_, se2, t))
in
if changed then
sigma_imply tenv calc_index_frame' calc_missing subs prop1 (hpred2' :: sigma2')
@ -2447,15 +2442,15 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
let prepare_prop_for_implication tenv (_, sub2) pi1 sigma1 =
let pi1' = Prop.pi_sub (`Exp sub2) (ProverState.get_missing_pi ()) @ pi1 in
let sigma1' = Prop.sigma_sub (`Exp sub2) (ProverState.get_missing_sigma ()) @ sigma1 in
let pi1' = Prop.pi_sub sub2 (ProverState.get_missing_pi ()) @ pi1 in
let sigma1' = Prop.sigma_sub sub2 (ProverState.get_missing_sigma ()) @ sigma1 in
let ep = Prop.set Prop.prop_emp ~sub:sub2 ~sigma:sigma1' ~pi:pi1' in
Prop.normalize tenv ep
let imply_pi tenv calc_missing (sub1, sub2) prop pi2 =
let do_atom a =
let a' = Sil.atom_sub (`Exp sub2) a in
let a' = Sil.atom_sub sub2 a in
try
if not (check_atom tenv prop a') then
raise (IMPL_EXC ("rhs atom missing in lhs", (sub1, sub2), EXC_FALSE_ATOM a'))
@ -2480,7 +2475,7 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
| [] ->
subs
| (Sil.Aeq (e2_in, f2_in) as a) :: pi2' when not (Prop.atom_is_inequality a) -> (
let e2, f2 = (Sil.exp_sub (`Exp (snd subs)) e2_in, Sil.exp_sub (`Exp (snd subs)) f2_in) in
let e2, f2 = (Sil.exp_sub (snd subs) e2_in, Sil.exp_sub (snd subs) f2_in) in
if Exp.equal e2 f2 then pre_check_pure_implication tenv calc_missing subs pi1 pi2'
else
match (e2, f2) with
@ -2493,7 +2488,7 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
let sub2' = extend_sub (snd subs) v2 e2 in
pre_check_pure_implication tenv calc_missing (fst subs, sub2') pi1 pi2'
| _ ->
let pi1' = Prop.pi_sub (`Exp (fst subs)) pi1 in
let pi1' = Prop.pi_sub (fst subs) pi1 in
let prop_for_impl = prepare_prop_for_implication tenv subs pi1' [] in
imply_atom tenv calc_missing subs prop_for_impl (Sil.Aeq (e2_in, f2_in)) ;
pre_check_pure_implication tenv calc_missing subs pi1 pi2' )
@ -2501,9 +2496,7 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
when (not calc_missing) && match e with Var v -> not (Ident.is_primed v) | _ -> true ->
raise
(IMPL_EXC
( "ineq e2=f2 in rhs with e2 not primed var"
, (Sil.exp_sub_empty, Sil.exp_sub_empty)
, EXC_FALSE ))
("ineq e2=f2 in rhs with e2 not primed var", (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
| (Sil.Aeq _ | Aneq _ | Apred _ | Anpred _) :: pi2' ->
pre_check_pure_implication tenv calc_missing subs pi1 pi2'
@ -2526,8 +2519,8 @@ let check_array_bounds tenv (sub1, sub2) prop =
in
let check_bound = function
| ProverState.BClen_imply (len1_, len2_, _indices2) ->
let len1 = Sil.exp_sub (`Exp sub1) len1_ in
let len2 = Sil.exp_sub (`Exp sub2) len2_ in
let len1 = Sil.exp_sub sub1 len1_ in
let len2 = Sil.exp_sub sub2 len2_ in
(* L.d_strln_color Orange "check_bound ";
Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
let indices_to_check =
@ -2536,7 +2529,7 @@ let check_array_bounds tenv (sub1, sub2) prop =
in
List.iter ~f:(fail_if_le len1) indices_to_check
| ProverState.BCfrom_pre atom_ ->
let atom_neg = atom_negate tenv (Sil.atom_sub (`Exp sub2) atom_) in
let atom_neg = atom_negate tenv (Sil.atom_sub sub2 atom_) in
(* L.d_strln_color Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *)
if check_atom tenv prop atom_neg then check_failed atom_neg
in
@ -2575,17 +2568,17 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
L.d_strln "returns" ;
L.d_strln "sub1: " ;
L.d_increase_indent 1 ;
Prop.d_sub (`Exp (fst subs)) ;
Prop.d_sub (fst subs) ;
L.d_decrease_indent 1 ;
L.d_ln () ;
L.d_strln "sub2: " ;
L.d_increase_indent 1 ;
Prop.d_sub (`Exp (snd subs)) ;
Prop.d_sub (snd subs) ;
L.d_decrease_indent 1 ;
L.d_ln () ;
let (sub1, sub2), frame_prop = sigma_imply tenv false calc_missing subs prop1 sigma2 in
let pi1' = Prop.pi_sub (`Exp sub1) pi1 in
let sigma1' = Prop.sigma_sub (`Exp sub1) sigma1 in
let pi1' = Prop.pi_sub sub1 pi1 in
let sigma1' = Prop.sigma_sub sub1 sigma1 in
L.d_ln () ;
let prop_for_impl = prepare_prop_for_implication tenv (sub1, sub2) pi1' sigma1' in
(* only deal with pi2 without bound checks *)
@ -2616,8 +2609,8 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
type implication_result =
| ImplOK of
( check list
* Sil.exp_subst
* Sil.exp_subst
* Sil.subst
* Sil.subst
* Sil.hpred list
* Sil.atom list
* Sil.hpred list

4
infer/src/biabduction/Prover.mli
Unescape View File

@ -70,8 +70,8 @@ val d_typings : (Exp.t * Exp.t) list -> unit
type implication_result =
| ImplOK of
( check list
* Sil.exp_subst
* Sil.exp_subst
* Sil.subst
* Sil.subst
* Sil.hpred list
* Sil.atom list
* Sil.hpred list

18
infer/src/biabduction/Tabulation.ml
Unescape View File

@ -198,7 +198,7 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
let sub1_inverse_list =
List.map ~f:(function id, Exp.Var id' -> (id', Exp.Var id) | _ -> assert false) sub1_list'
in
Sil.exp_subst_of_list_duplicates sub1_inverse_list
Sil.subst_of_list_duplicates sub1_inverse_list
in
let fav_actual_pre =
let fav_pre = Prop.free_vars actual_pre |> Ident.hashqueue_of_sequence in
@ -211,19 +211,18 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_
let fav_missing_primed =
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
Prop.sigma_sub 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
Prop.pi_sub 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
Prop.sigma_sub sub missing_fld |> Prop.sigma_free_vars |> Ident.hashqueue_of_sequence
in
let map_var_to_pre_var_or_fresh id =
match Sil.exp_sub (`Exp sub1_inverse) (Exp.Var id) with
match Sil.exp_sub sub1_inverse (Exp.Var id) with
| Exp.Var id' ->
if
Ident.HashQueue.mem fav_actual_pre id' || Ident.is_path id'
@ -1227,10 +1226,9 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
; vr_incons_res= inconsistent_results }
in
List.iter ~f:log_check_exn checks ;
let subbed_pre = Prop.prop_sub (`Exp sub1) actual_pre in
let subbed_pre = Prop.prop_sub sub1 actual_pre in
match
check_dereferences caller_pname tenv callee_pname subbed_pre (`Exp sub2) spec_pre
formal_params
check_dereferences caller_pname tenv callee_pname subbed_pre sub2 spec_pre formal_params
with
| Some (Deref_undef _, _) ->
let split = do_split () in

8
infer/src/biabduction/interproc.ml
Unescape View File

@ -294,7 +294,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P
let prop_incons =
let mk_incons prop =
let p_abs = Abs.abstract pname tenv prop in
let p_zero = Prop.set p_abs ~sub:Sil.exp_sub_empty ~sigma:[] in
let p_zero = Prop.set p_abs ~sub:Sil.sub_empty ~sigma:[] in
Prop.normalize tenv (Prop.set p_zero ~pi:[Sil.Aneq (Exp.zero, Exp.zero)])
in
Paths.PathSet.map mk_incons diverging_states
@ -586,7 +586,7 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list
|> 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
Sil.subst_of_list sub_list
in
let pre_post_visited_list =
let pplist = Paths.PathSet.elements pathset in
@ -594,10 +594,10 @@ let extract_specs tenv pdesc pathset : Prop.normal BiabductionSummary.spec list
let _, prop' = PropUtil.remove_locals_formals tenv pdesc prop in
let prop'' = Abs.abstract pname tenv prop' in
let pre, post = Prop.extract_spec prop'' in
let pre' = Prop.normalize tenv (Prop.prop_sub (`Exp sub) pre) in
let pre' = Prop.normalize tenv (Prop.prop_sub sub pre) in
let post' =
if Prover.check_inconsistency_base tenv prop then None
else Some (Prop.normalize tenv (Prop.prop_sub (`Exp sub) post), path)
else Some (Prop.normalize tenv (Prop.prop_sub sub post), path)
in
let visited =
let vset = vset_add_path Procdesc.NodeSet.empty path in

Write Preview
Loading…
Cancel
Save