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

Refactor operations on Exp.t in Sil to Exp

Browse Source 
Summary: No functional change.

Reviewed By: cristianoc

Differential Revision: D3669404

fbshipit-source-id: 1d1f11a
master
Josh Berdine 8 years ago committed by Facebook Github Bot 4
parent 8a90190309
commit 25a52c7bbc
28 changed files with 468 additions and 477 deletions
Show Stats Download Patch File Download Diff File

141
infer/src/IR/Exp.re
Unescape View File

@ -185,3 +185,144 @@ let module Hash = Hashtbl.Make {
let equal = equal;
let hash = hash;
};
let rec is_array_index_of exp1 exp2 =>
switch exp1 {
| Lindex exp _ => is_array_index_of exp exp2
| _ => equal exp1 exp2
};
let is_null_literal =
fun
| Const (Cint n) => IntLit.isnull n
| _ => false;
let is_this =
fun
| Lvar pvar => Pvar.is_this pvar
| _ => false;
let is_zero =
fun
| Const (Cint n) => IntLit.iszero n
| _ => false;
/** {2 Utility Functions for Expressions} */
/** Turn an expression representing a type into the type it represents
If not a sizeof, return the default type if given, otherwise raise an exception */
let texp_to_typ default_opt =>
fun
| Sizeof t _ _ => t
| _ => Typ.unsome "texp_to_typ" default_opt;
/** Return the root of [lexp]. */
let rec root_of_lexp lexp =>
switch (lexp: t) {
| Var _ => lexp
| Const _ => lexp
| Cast _ e => root_of_lexp e
| UnOp _
| BinOp _
| Exn _
| Closure _ => lexp
| Lvar _ => lexp
| Lfield e _ _ => root_of_lexp e
| Lindex e _ => root_of_lexp e
| Sizeof _ => lexp
};
/** Checks whether an expression denotes a location by pointer arithmetic.
Currently, catches array - indexing expressions such as a[i] only. */
let rec pointer_arith =
fun
| Lfield e _ _ => pointer_arith e
| Lindex _ => true
| _ => false;
let get_undefined footprint =>
Var (
Ident.create_fresh (
if footprint {
Ident.kfootprint
} else {
Ident.kprimed
}
)
);
/** Create integer constant */
let int i => Const (Cint i);
/** Create float constant */
let float v => Const (Cfloat v);
/** Integer constant 0 */
let zero = int IntLit.zero;
/** Null constant */
let null = int IntLit.null;
/** Integer constant 1 */
let one = int IntLit.one;
/** Integer constant -1 */
let minus_one = int IntLit.minus_one;
/** Create integer constant corresponding to the boolean value */
let bool b =>
if b {
one
} else {
zero
};
/** Create expresstion [e1 == e2] */
let eq e1 e2 => BinOp Eq e1 e2;
/** Create expresstion [e1 != e2] */
let ne e1 e2 => BinOp Ne e1 e2;
/** Create expression [e1 <= e2] */
let le e1 e2 => BinOp Le e1 e2;
/** Create expression [e1 < e2] */
let lt e1 e2 => BinOp Lt e1 e2;
/** Extract the ids and pvars from an expression */
let get_vars exp => {
let rec get_vars_ exp vars =>
switch exp {
| Lvar pvar => (fst vars, [pvar, ...snd vars])
| Var id => ([id, ...fst vars], snd vars)
| Cast _ e
| UnOp _ e _
| Lfield e _ _
| Exn e => get_vars_ e vars
| BinOp _ e1 e2
| Lindex e1 e2 => get_vars_ e1 vars |> get_vars_ e2
| Closure {captured_vars} =>
IList.fold_left
(fun vars_acc (captured_exp, _, _) => get_vars_ captured_exp vars_acc) vars captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => vars
/* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => vars */
/* | Sizeof _ (Some l) _ => get_vars_ l vars */
| Sizeof _ _ _ => vars
};
get_vars_ exp ([], [])
};

80
infer/src/IR/Exp.rei
Unescape View File

@ -74,3 +74,83 @@ let module Map: Map.S with type key = t;
/** Hashtable with expression keys. */
let module Hash: Hashtbl.S with type key = t;
/** returns true is index is an array index of arr. */
let is_array_index_of: t => t => bool;
let is_null_literal: t => bool;
/** return true if [exp] is the special this/self expression */
let is_this: t => bool;
let is_zero: t => bool;
/** {2 Utility Functions for Expressions} */
/** Turn an expression representing a type into the type it represents
If not a sizeof, return the default type if given, otherwise raise an exception */
let texp_to_typ: option Typ.t => t => Typ.t;
/** Return the root of [lexp]. */
let root_of_lexp: t => t;
/** Get an expression "undefined", the boolean indicates
whether the undefined value goest into the footprint */
let get_undefined: bool => t;
/** Checks whether an expression denotes a location using pointer arithmetic.
Currently, catches array - indexing expressions such as a[i] only. */
let pointer_arith: t => bool;
/** Integer constant 0 */
let zero: t;
/** Null constant */
let null: t;
/** Integer constant 1 */
let one: t;
/** Integer constant -1 */
let minus_one: t;
/** Create integer constant */
let int: IntLit.t => t;
/** Create float constant */
let float: float => t;
/** Create integer constant corresponding to the boolean value */
let bool: bool => t;
/** Create expresstion [e1 == e2] */
let eq: t => t => t;
/** Create expresstion [e1 != e2] */
let ne: t => t => t;
/** Create expresstion [e1 <= e2] */
let le: t => t => t;
/** Create expression [e1 < e2] */
let lt: t => t => t;
/** Extract the ids and pvars from an expression */
let get_vars: t => (list Ident.t, list Pvar.t);

146
infer/src/IR/Sil.re
Unescape View File

@ -312,22 +312,6 @@ let is_static_local_name pname pvar =>
}
};
let exp_is_zero =
fun
| Exp.Const (Cint n) => IntLit.iszero n
| _ => false;
let exp_is_null_literal =
fun
| Exp.Const (Cint n) => IntLit.isnull n
| _ => false;
let exp_is_this =
fun
| Exp.Lvar pvar => Pvar.is_this pvar
| _ => false;
let path_pos_compare (pn1, nid1) (pn2, nid2) => {
let n = Procname.compare pn1 pn2;
if (n != 0) {
@ -510,20 +494,12 @@ let attribute_compare (att1: attribute) (att2: attribute) :int =>
| (_, Aunsubscribed_observer) => 1
};
let rec exp_is_array_index_of exp1 exp2 =>
switch exp1 {
| Exp.Lindex exp _ => exp_is_array_index_of exp exp2
| _ => Exp.equal exp1 exp2
};
let ident_exp_compare = pair_compare Ident.compare Exp.compare;
let ident_exp_equal ide1 ide2 => ident_exp_compare ide1 ide2 == 0;
let exp_list_compare = IList.compare Exp.compare;
let exp_list_equal el1 el2 => exp_list_compare el1 el2 == 0;
let attribute_equal att1 att2 => attribute_compare att1 att2 == 0;
@ -1795,101 +1771,6 @@ let hpred_list_get_lexps (filter: Exp.t => bool) (hlist: list hpred) :list Exp.t
};
/** {2 Utility Functions for Expressions} */
/** Turn an expression representing a type into the type it represents
If not a sizeof, return the default type if given, otherwise raise an exception */
let texp_to_typ default_opt =>
fun
| Exp.Sizeof t _ _ => t
| _ => Typ.unsome "texp_to_typ" default_opt;
/** Return the root of [lexp]. */
let rec root_of_lexp lexp =>
switch (lexp: Exp.t) {
| Var _ => lexp
| Const _ => lexp
| Cast _ e => root_of_lexp e
| UnOp _
| BinOp _
| Exn _
| Closure _ => lexp
| Lvar _ => lexp
| Lfield e _ _ => root_of_lexp e
| Lindex e _ => root_of_lexp e
| Sizeof _ => lexp
};
/** Checks whether an expression denotes a location by pointer arithmetic.
Currently, catches array - indexing expressions such as a[i] only. */
let rec exp_pointer_arith =
fun
| Exp.Lfield e _ _ => exp_pointer_arith e
| Exp.Lindex _ => true
| _ => false;
let exp_get_undefined footprint =>
Exp.Var (
Ident.create_fresh (
if footprint {
Ident.kfootprint
} else {
Ident.kprimed
}
)
);
/** Create integer constant */
let exp_int i => Exp.Const (Cint i);
/** Create float constant */
let exp_float v => Exp.Const (Cfloat v);
/** Integer constant 0 */
let exp_zero = exp_int IntLit.zero;
/** Null constant */
let exp_null = exp_int IntLit.null;
/** Integer constant 1 */
let exp_one = exp_int IntLit.one;
/** Integer constant -1 */
let exp_minus_one = exp_int IntLit.minus_one;
/** Create integer constant corresponding to the boolean value */
let exp_bool b =>
if b {
exp_one
} else {
exp_zero
};
/** Create expresstion [e1 == e2] */
let exp_eq e1 e2 => Exp.BinOp Eq e1 e2;
/** Create expresstion [e1 != e2] */
let exp_ne e1 e2 => Exp.BinOp Ne e1 e2;
/** Create expression [e1 <= e2] */
let exp_le e1 e2 => Exp.BinOp Le e1 e2;
/** Create expression [e1 < e2] */
let exp_lt e1 e2 => Exp.BinOp Lt e1 e2;
/** {2 Functions for computing program variables} */
let rec exp_fpv e =>
switch (e: Exp.t) {
@ -3141,33 +3022,6 @@ let hpred_compact sh hpred =>
/** {2 Functions for constructing or destructing entities in this module} */
/** Extract the ids and pvars from an expression */
let exp_get_vars exp => {
let rec exp_get_vars_ exp vars =>
switch (exp: Exp.t) {
| Lvar pvar => (fst vars, [pvar, ...snd vars])
| Var id => ([id, ...fst vars], snd vars)
| Cast _ e
| UnOp _ e _
| Lfield e _ _
| Exn e => exp_get_vars_ e vars
| BinOp _ e1 e2
| Lindex e1 e2 => exp_get_vars_ e1 vars |> exp_get_vars_ e2
| Closure {captured_vars} =>
IList.fold_left
(fun vars_acc (captured_exp, _, _) => exp_get_vars_ captured_exp vars_acc)
vars
captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _ | Cptr_to_fld _) => vars
/* TODO: Sizeof length expressions may contain variables, do not ignore them. */
/* | Sizeof _ None _ => vars */
/* | Sizeof _ (Some l) _ => exp_get_vars_ l vars */
| Sizeof _ _ _ => vars
};
exp_get_vars_ exp ([], [])
};
/** Compute the offset list of an expression */
let exp_get_offsets exp => {
let rec f offlist_past e =>

84
infer/src/IR/Sil.rei
Unescape View File

@ -318,14 +318,6 @@ let hpred_compact: sharing_env => hpred => hpred;
/** {2 Comparision And Inspection Functions} */
let has_objc_ref_counter: hpred => bool;
let exp_is_zero: Exp.t => bool;
let exp_is_null_literal: Exp.t => bool;
/** return true if [exp] is the special this/self expression */
let exp_is_this: Exp.t => bool;
let path_pos_equal: path_pos => path_pos => bool;
@ -384,10 +376,6 @@ let attribute_to_category: attribute => attribute_category;
let attr_is_undef: attribute => bool;
/** exp_is_array_index_of index arr returns true is index is an array index of arr. */
let exp_is_array_index_of: Exp.t => Exp.t => bool;
let exp_typ_compare: (Exp.t, Typ.t) => (Exp.t, Typ.t) => int;
let instr_compare: instr => instr => int;
@ -398,10 +386,6 @@ let instr_compare: instr => instr => int;
used in the procedure of [instr2] */
let instr_compare_structural: instr => instr => Exp.Map.t Exp.t => (int, Exp.Map.t Exp.t);
let exp_list_compare: list Exp.t => list Exp.t => int;
let exp_list_equal: list Exp.t => list Exp.t => bool;
let atom_compare: atom => atom => int;
let atom_equal: atom => atom => bool;
@ -669,70 +653,6 @@ let atom_list_expmap: (Exp.t => Exp.t) => list atom => list atom;
let hpred_list_get_lexps: (Exp.t => bool) => list hpred => list Exp.t;
/** {2 Utility Functions for Expressions} */
/** Turn an expression representing a type into the type it represents
If not a sizeof, return the default type if given, otherwise raise an exception */
let texp_to_typ: option Typ.t => Exp.t => Typ.t;
/** Return the root of [lexp]. */
let root_of_lexp: Exp.t => Exp.t;
/** Get an expression "undefined", the boolean indicates
whether the undefined value goest into the footprint */
let exp_get_undefined: bool => Exp.t;
/** Checks whether an expression denotes a location using pointer arithmetic.
Currently, catches array - indexing expressions such as a[i] only. */
let exp_pointer_arith: Exp.t => bool;
/** Integer constant 0 */
let exp_zero: Exp.t;
/** Null constant */
let exp_null: Exp.t;
/** Integer constant 1 */
let exp_one: Exp.t;
/** Integer constant -1 */
let exp_minus_one: Exp.t;
/** Create integer constant */
let exp_int: IntLit.t => Exp.t;
/** Create float constant */
let exp_float: float => Exp.t;
/** Create integer constant corresponding to the boolean value */
let exp_bool: bool => Exp.t;
/** Create expresstion [e1 == e2] */
let exp_eq: Exp.t => Exp.t => Exp.t;
/** Create expresstion [e1 != e2] */
let exp_ne: Exp.t => Exp.t => Exp.t;
/** Create expresstion [e1 <= e2] */
let exp_le: Exp.t => Exp.t => Exp.t;
/** Create expression [e1 < e2] */
let exp_lt: Exp.t => Exp.t => Exp.t;
/** {2 Functions for computing program variables} */
let exp_fpv: Exp.t => list Pvar.t;
@ -999,10 +919,6 @@ let hpred_replace_exp: list (Exp.t, Exp.t) => hpred => hpred;
/** {2 Functions for constructing or destructing entities in this module} */
/** Extract the ids and pvars from an expression */
let exp_get_vars: Exp.t => (list Ident.t, list Pvar.t);
/** Compute the offset list of an expression */
let exp_get_offsets: Exp.t => list offset;

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

@ -182,7 +182,7 @@ end = struct
match hpred with
| Sil.Hpointsto (root, se, te) ->
let sigma_other = sigma_seen @ sigma_rest in
find_offset_sexp sigma_other hpred root [] se (Sil.texp_to_typ None te)
find_offset_sexp sigma_other hpred root [] se (Exp.texp_to_typ None te)
| _ -> ()
end;
iterate (hpred:: sigma_seen) sigma_rest in
@ -194,7 +194,7 @@ end = struct
(** Get the matched strexp *)
let get_data ((_ , hpred, syn_offs) : t) = match hpred with
| Sil.Hpointsto (root, se, te) ->
let t = Sil.texp_to_typ None te in
let t = Exp.texp_to_typ None te in
let se', t' = get_strexp_at_syn_offsets se t syn_offs in
let path' = (root, syn_offs) in
(path', se', t')
@ -220,7 +220,7 @@ end = struct
begin
match hpred with
| Sil.Hpointsto (root, se, te) ->
let t = Sil.texp_to_typ None te in
let t = Exp.texp_to_typ None te in
let se' = replace_strexp_at_syn_offsets se t syn_offs update in
Sil.Hpointsto (root, se', te)
| _ -> assert false
@ -354,7 +354,7 @@ let generic_strexp_abstract
(** Return [true] if there's a pointer to the index *)
let index_is_pointed_to (p: Prop.normal Prop.t) (path: StrexpMatch.path) (index: Exp.t) : bool =
let indices =
let index_plus_one = Exp.BinOp(Binop.PlusA, index, Sil.exp_one) in
let index_plus_one = Exp.BinOp(Binop.PlusA, index, Exp.one) in
[index; index_plus_one] in
let add_index_to_paths =
let elist_path = StrexpMatch.path_to_exps path in
@ -393,8 +393,8 @@ let blur_array_index
let sigma' = StrexpMatch.replace_index false matched index fresh_index in
Prop.replace_sigma sigma' p2 in
let p4 =
let index_next = Exp.BinOp(Binop.PlusA, index, Sil.exp_one) in
let fresh_index_next = Exp.BinOp (Binop.PlusA, fresh_index, Sil.exp_one) in
let index_next = Exp.BinOp(Binop.PlusA, index, Exp.one) in
let fresh_index_next = Exp.BinOp (Binop.PlusA, fresh_index, Exp.one) in
let map = [(index, fresh_index); (index_next, fresh_index_next)] in
prop_replace_path_index p3 path map in
Prop.normalize p4
@ -545,7 +545,7 @@ let check_after_array_abstraction prop =
check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se) fsel in
let check_hpred = function
| Sil.Hpointsto (root, se, texp) ->
let typ = Sil.texp_to_typ (Some Typ.Tvoid) texp in
let typ = Exp.texp_to_typ (Some Typ.Tvoid) texp in
check_se root [] typ se
| Sil.Hlseg _ | Sil.Hdllseg _ -> () in
let check_sigma sigma = IList.iter check_hpred sigma in

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

@ -255,7 +255,7 @@ module CheckJoinPre : InfoLossCheckerSig = struct
| Exp.Var id when Ident.is_normal id -> IList.length es >= 1
| Exp.Var _ ->
if Config.join_cond = 0 then
IList.exists (Exp.equal Sil.exp_zero) es
IList.exists (Exp.equal Exp.zero) es
else if Dangling.check side e then
begin
let r = IList.exists (fun e' -> not (Dangling.check side_op e')) es in
@ -457,7 +457,7 @@ end = struct
let (_, _, e) = IList.find (fun (e1', e2', _) -> Exp.equal e1 e1' && Exp.equal e2 e2') !t in
e
with Not_found ->
let e = Sil.exp_get_undefined (JoinState.get_footprint ()) in
let e = Exp.get_undefined (JoinState.get_footprint ()) in
t := (e1, e2, e)::!t;
e
@ -476,7 +476,7 @@ end = struct
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n1') -> IntLit.eq (n1 ++ n) n1'
| _ -> false in
let add_and_gen_eq e e' n =
let e_plus_n = Exp.BinOp(Binop.PlusA, e, Sil.exp_int n) in
let e_plus_n = Exp.BinOp(Binop.PlusA, e, Exp.int n) in
Prop.mk_eq e_plus_n e' in
let rec f_eqs_entry ((e1, e2, e) as entry) eqs_acc t_seen = function
| [] -> eqs_acc, t_seen
@ -502,8 +502,8 @@ end = struct
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) ->
let strict_lower1, upper1 =
if IntLit.leq n1 n2 then (n1 -- IntLit.one, n2) else (n2 -- IntLit.one, n1) in
let e_strict_lower1 = Sil.exp_int strict_lower1 in
let e_upper1 = Sil.exp_int upper1 in
let e_strict_lower1 = Exp.int strict_lower1 in
let e_upper1 = Exp.int upper1 in
get_induced_atom acc e_strict_lower1 e_upper1 e
| _ -> acc in
IList.fold_left f_ineqs eqs t_minimal
@ -593,12 +593,12 @@ end = struct
let f v = match v, side with
| (Exp.BinOp (Binop.PlusA, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs
when Exp.equal e e1' ->
let c' = Sil.exp_int (IntLit.neg i) in
let c' = Exp.int (IntLit.neg i) in
let v' = (e1', Exp.BinOp(Binop.PlusA, e2, c'), Exp.BinOp (Binop.PlusA, e', c')) in
res := v'::!res
| (e1, Exp.BinOp (Binop.PlusA, e2', Exp.Const (Const.Cint i)), e'), Rhs
when Exp.equal e e2' ->
let c' = Sil.exp_int (IntLit.neg i) in
let c' = Exp.int (IntLit.neg i) in
let v' = (Exp.BinOp(Binop.PlusA, e1, c'), e2', Exp.BinOp (Binop.PlusA, e', c')) in
res := v'::!res
| _ -> () in
@ -930,13 +930,13 @@ let rec exp_partial_join (e1: Exp.t) (e2: Exp.t) : Exp.t =
| Exp.BinOp(Binop.PlusA, Exp.Var id1, Exp.Const (Const.Cint c1)), Exp.Const (Const.Cint c2)
when can_rename id1 ->
let c2' = c2 -- c1 in
let e_res = Rename.extend (Exp.Var id1) (Sil.exp_int c2') Rename.ExtFresh in
Exp.BinOp(Binop.PlusA, e_res, Sil.exp_int c1)
let e_res = Rename.extend (Exp.Var id1) (Exp.int c2') Rename.ExtFresh in
Exp.BinOp(Binop.PlusA, e_res, Exp.int c1)
| Exp.Const (Const.Cint c1), Exp.BinOp(Binop.PlusA, Exp.Var id2, Exp.Const (Const.Cint c2))
when can_rename id2 ->
let c1' = c1 -- c2 in
let e_res = Rename.extend (Sil.exp_int c1') (Exp.Var id2) Rename.ExtFresh in
Exp.BinOp(Binop.PlusA, e_res, Sil.exp_int c2)
let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in
Exp.BinOp(Binop.PlusA, e_res, Exp.int c2)
| Exp.Cast(t1, e1), Exp.Cast(t2, e2) ->
if not (Typ.equal t1 t2) then (L.d_strln "failure reason 22"; raise IList.Fail)
else
@ -1603,11 +1603,11 @@ let pi_partial_join mode
if IntLit.leq n first_try then
if IntLit.leq n second_try then second_try else first_try
else widening_top in
let a' = Prop.mk_inequality (Exp.BinOp(Binop.Le, e, Sil.exp_int bound)) in
let a' = Prop.mk_inequality (Exp.BinOp(Binop.Le, e, Exp.int bound)) in
Some a'
| Some (e, _), [] ->
let bound = widening_top in
let a' = Prop.mk_inequality (Exp.BinOp(Binop.Le, e, Sil.exp_int bound)) in
let a' = Prop.mk_inequality (Exp.BinOp(Binop.Le, e, Exp.int bound)) in
Some a'
| _ ->
begin
@ -1616,7 +1616,7 @@ let pi_partial_join mode
| Some (n, e) ->
let bound =
if IntLit.leq IntLit.minus_one n then IntLit.minus_one else widening_bottom in
let a' = Prop.mk_inequality (Exp.BinOp(Binop.Lt, Sil.exp_int bound, e)) in
let a' = Prop.mk_inequality (Exp.BinOp(Binop.Lt, Exp.int bound, e)) in
Some a'
end in
let is_stronger_le e n a =

22
infer/src/backend/dotty.ml
Unescape View File

@ -180,8 +180,8 @@ let is_source_node_of_exp e node =
(* make sense for that case *)
let get_coordinate_and_exp dotnode =
match dotnode with
| Dotnil(coo) -> (coo, Sil.exp_minus_one)
| Dotarray (coo, _, _, _, _, _) -> (coo, Sil.exp_minus_one)
| Dotnil(coo) -> (coo, Exp.minus_one)
| Dotarray (coo, _, _, _, _, _) -> (coo, Exp.minus_one)
| Dotpointsto (coo, b, _)
| Dotlseg (coo, b, _, _, _, _)
| Dotdllseg (coo, b, _, _, _, _, _, _)
@ -246,19 +246,19 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
let coo = mk_coordinate n lambda in
(match hpred with
| Sil.Hpointsto (_, Sil.Eexp (e, _), _)
when not (Exp.equal e Sil.exp_zero) && !print_full_prop ->
when not (Exp.equal e Exp.zero) && !print_full_prop ->
let e_color_str = color_to_str (exp_color hpred e) in
[Dotdangling(coo, e, e_color_str)]
| Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Sil.exp_zero) ->
| Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Exp.zero) ->
let e2_color_str = color_to_str (exp_color hpred e2) in
[Dotdangling(coo, e2, e2_color_str)]
| Sil.Hdllseg (_, _, _, e2, e3, _, _) ->
let e2_color_str = color_to_str (exp_color hpred e2) in
let e3_color_str = color_to_str (exp_color hpred e3) in
let ll = if not (Exp.equal e2 Sil.exp_zero) then
let ll = if not (Exp.equal e2 Exp.zero) then
[Dotdangling(coo, e2, e2_color_str)]
else [] in
if not (Exp.equal e3 Sil.exp_zero) then Dotdangling(coo, e3, e3_color_str):: ll
if not (Exp.equal e3 Exp.zero) then Dotdangling(coo, e3, e3_color_str):: ll
else ll
| Sil.Hpointsto (_, _, _)
| _ -> [] (* arrays and struct do not give danglings*)
@ -377,7 +377,7 @@ let compute_struct_exp_nodes sigma =
let get_node_exp n = snd (get_coordinate_and_exp n)
let is_nil e prop =
(Exp.equal e Sil.exp_zero) || (Prover.check_equal prop e Sil.exp_zero)
(Exp.equal e Exp.zero) || (Prover.check_equal prop e Exp.zero)
(* an edge is in cycle *)
let in_cycle cycle edge =
@ -1172,11 +1172,11 @@ let make_set_dangling_nodes allocated_nodes (sigma: Sil.hpred list) =
VH_dangling(n, e) in
let get_rhs_predicate hpred =
(match hpred with
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) when not (Exp.equal e Sil.exp_zero) -> [e]
| Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Sil.exp_zero) -> [e2]
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) when not (Exp.equal e Exp.zero) -> [e]
| Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Exp.zero) -> [e2]
| Sil.Hdllseg (_, _, _, e2, e3, _, _) ->
if (Exp.equal e2 Sil.exp_zero) then
if (Exp.equal e3 Sil.exp_zero) then []
if (Exp.equal e2 Exp.zero) then
if (Exp.equal e3 Exp.zero) then []
else [e3]
else [e2; e3]
| Sil.Hpointsto (_, _, _)

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

@ -282,7 +282,7 @@ let propagate_nodes_divergence
let mk_incons prop =
let p_abs = Abs.abstract pname tenv prop in
let p_zero = Prop.replace_sigma [] (Prop.replace_sub Sil.sub_empty p_abs) in
Prop.normalize (Prop.replace_pi [Sil.Aneq (Sil.exp_zero, Sil.exp_zero)] p_zero) in
Prop.normalize (Prop.replace_pi [Sil.Aneq (Exp.zero, Exp.zero)] p_zero) in
Paths.PathSet.map mk_incons diverging_states in
(L.d_strln_color Orange) "Propagating Divergence -- diverging states:";
Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons); L.d_ln ();
@ -1120,7 +1120,7 @@ let remove_this_not_null prop =
| hpred -> (var_option, hpred:: hpreds) in
let collect_atom var atoms = function
| Sil.Aneq (Exp.Var v, e)
when Ident.equal v var && Exp.equal e Sil.exp_null -> atoms
when Ident.equal v var && Exp.equal e Exp.null -> atoms
| a -> a:: atoms in
match IList.fold_left collect_hpred (None, []) (Prop.get_sigma prop) with
| None, _ -> prop

20
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -24,7 +24,7 @@ let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_ids; args;
: Builtin.ret_typ =
match args, ret_ids with
| [_; _; (lexp3, typ3)], _ ->
let instr' = Sil.Set (lexp3, typ3, Sil.exp_zero, loc) in
let instr' = Sil.Set (lexp3, typ3, Exp.zero, loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)]
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -179,7 +179,7 @@ let create_type tenv n_lexp typ prop =
let prop''= Prop.normalize prop'' in
prop''
| None -> prop in
let sil_is_null = Exp.BinOp (Binop.Eq, n_lexp, Sil.exp_zero) in
let sil_is_null = Exp.BinOp (Binop.Eq, n_lexp, Exp.zero) in
let sil_is_nonnull = Exp.UnOp (Unop.LNot, sil_is_null, None) in
let null_case = Propset.to_proplist (prune ~positive:true sil_is_null prop) in
let non_null_case = Propset.to_proplist (prune ~positive:true sil_is_nonnull prop_type) in
@ -206,7 +206,7 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; }
| Sil.Hpointsto(_, _, texp) ->
(return_result texp prop ret_ids), path
| _ -> assert false
with Not_found -> (return_result Sil.exp_zero prop ret_ids), path
with Not_found -> (return_result Exp.zero prop ret_ids), path
end in
(IList.map aux props)
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -247,8 +247,8 @@ let execute___instanceof_cast ~instof
Tabulation.raise_cast_exception
__POS__ None texp1 texp2 val1 in
let exe_one_prop prop =
if Exp.equal texp2 Sil.exp_zero then
[(return_result Sil.exp_zero prop ret_ids, path)]
if Exp.equal texp2 Exp.zero then
[(return_result Exp.zero prop ret_ids, path)]
else
begin
try
@ -268,14 +268,14 @@ let execute___instanceof_cast ~instof
[(return_result res_e prop' ret_ids, path)] in
if instof then (* instanceof *)
begin
let pos_res = mk_res pos_type_opt Sil.exp_one in
let neg_res = mk_res neg_type_opt Sil.exp_zero in
let pos_res = mk_res pos_type_opt Exp.one in
let neg_res = mk_res neg_type_opt Exp.zero in
pos_res @ neg_res
end
else (* cast *)
if not should_throw_exception then (* C++ case when negative cast returns 0 *)
let pos_res = mk_res pos_type_opt val1 in
let neg_res = mk_res neg_type_opt Sil.exp_zero in
let neg_res = mk_res neg_type_opt Exp.zero in
pos_res @ neg_res
else
begin
@ -799,7 +799,7 @@ let execute_alloc mk can_return_null
Prop.add_or_replace_attribute prop' (Apred (Aresource ra, [exp_new])) in
let prop_alloc = Prop.conjoin_eq (Exp.Var ret_id) exp_new prop_plus_ptsto in
if can_return_null then
let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Sil.exp_zero prop in
let prop_null = Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop in
[(prop_alloc, path); (prop_null, path)]
else [(prop_alloc, path)]
@ -918,7 +918,7 @@ let execute___infer_assume { Builtin.prop_; path; args; }
: Builtin.ret_typ =
match args with
| [(lexp, _)] ->
let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop_ in
let prop_assume = Prop.conjoin_eq lexp (Exp.bool true) prop_ in
if Prover.check_inconsistency prop_assume
then SymExec.diverge prop_assume path
else [(prop_assume, path)]

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

@ -471,13 +471,13 @@ let sym_eval abs e =
begin
match eval e1 with
| Exp.Const (Const.Cint i) when IntLit.iszero i ->
Sil.exp_one
Exp.one
| Exp.Const (Const.Cint _) ->
Sil.exp_zero
Exp.zero
| Exp.UnOp(Unop.LNot, e1', _) ->
e1'
| e1' ->
if abs then Sil.exp_get_undefined false else Exp.UnOp(Unop.LNot, e1', topt)
if abs then Exp.get_undefined false else Exp.UnOp(Unop.LNot, e1', topt)
end
| Exp.UnOp (Unop.Neg, e1, topt) ->
begin
@ -485,13 +485,13 @@ let sym_eval abs e =
| Exp.UnOp (Unop.Neg, e2', _) ->
e2'
| Exp.Const (Const.Cint i) ->
Sil.exp_int (IntLit.neg i)
Exp.int (IntLit.neg i)
| Exp.Const (Const.Cfloat v) ->
Sil.exp_float (-. v)
Exp.float (-. v)
| Exp.Var id ->
Exp.UnOp (Unop.Neg, Exp.Var id, topt)
| e1' ->
if abs then Sil.exp_get_undefined false else Exp.UnOp (Unop.Neg, e1', topt)
if abs then Exp.get_undefined false else Exp.UnOp (Unop.Neg, e1', topt)
end
| Exp.UnOp (Unop.BNot, e1, topt) ->
begin
@ -499,62 +499,62 @@ let sym_eval abs e =
| Exp.UnOp(Unop.BNot, e2', _) ->
e2'
| Exp.Const (Const.Cint i) ->
Sil.exp_int (IntLit.lognot i)
Exp.int (IntLit.lognot i)
| e1' ->
if abs then Sil.exp_get_undefined false else Exp.UnOp (Unop.BNot, e1', topt)
if abs then Exp.get_undefined false else Exp.UnOp (Unop.BNot, e1', topt)
end
| Exp.BinOp (Binop.Le, e1, e2) ->
begin
match eval e1, eval e2 with
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_bool (IntLit.leq n m)
Exp.bool (IntLit.leq n m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_bool (v <= w)
Exp.bool (v <= w)
| Exp.BinOp (Binop.PlusA, e3, Exp.Const (Const.Cint n)), Exp.Const (Const.Cint m) ->
Exp.BinOp (Binop.Le, e3, Sil.exp_int (m -- n))
Exp.BinOp (Binop.Le, e3, Exp.int (m -- n))
| e1', e2' ->
Sil.exp_le e1' e2'
Exp.le e1' e2'
end
| Exp.BinOp (Binop.Lt, e1, e2) ->
begin
match eval e1, eval e2 with
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_bool (IntLit.lt n m)
Exp.bool (IntLit.lt n m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_bool (v < w)
Exp.bool (v < w)
| Exp.Const (Const.Cint n), Exp.BinOp (Binop.MinusA, f1, f2) ->
Exp.BinOp
(Binop.Le, Exp.BinOp (Binop.MinusA, f2, f1), Sil.exp_int (IntLit.minus_one -- n))
(Binop.Le, Exp.BinOp (Binop.MinusA, f2, f1), Exp.int (IntLit.minus_one -- n))
| Exp.BinOp(Binop.MinusA, f1 , f2), Exp.Const(Const.Cint n) ->
Sil.exp_le (Exp.BinOp(Binop.MinusA, f1 , f2)) (Sil.exp_int (n -- IntLit.one))
Exp.le (Exp.BinOp(Binop.MinusA, f1 , f2)) (Exp.int (n -- IntLit.one))
| Exp.BinOp (Binop.PlusA, e3, Exp.Const (Const.Cint n)), Exp.Const (Const.Cint m) ->
Exp.BinOp (Binop.Lt, e3, Sil.exp_int (m -- n))
Exp.BinOp (Binop.Lt, e3, Exp.int (m -- n))
| e1', e2' ->
Sil.exp_lt e1' e2'
Exp.lt e1' e2'
end
| Exp.BinOp (Binop.Ge, e1, e2) ->
eval (Sil.exp_le e2 e1)
eval (Exp.le e2 e1)
| Exp.BinOp (Binop.Gt, e1, e2) ->
eval (Sil.exp_lt e2 e1)
eval (Exp.lt e2 e1)
| Exp.BinOp (Binop.Eq, e1, e2) ->
begin
match eval e1, eval e2 with
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_bool (IntLit.eq n m)
Exp.bool (IntLit.eq n m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_bool (v = w)
Exp.bool (v = w)
| e1', e2' ->
Sil.exp_eq e1' e2'
Exp.eq e1' e2'
end
| Exp.BinOp (Binop.Ne, e1, e2) ->
begin
match eval e1, eval e2 with
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_bool (IntLit.neq n m)
Exp.bool (IntLit.neq n m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_bool (v <> w)
Exp.bool (v <> w)
| e1', e2' ->
Sil.exp_ne e1' e2'
Exp.ne e1' e2'
end
| Exp.BinOp (Binop.LAnd, e1, e2) ->
let e1' = eval e1 in
@ -627,9 +627,9 @@ let sym_eval abs e =
| _, Exp.Const c when iszero_int_float c ->
e1'
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_int (n ++ m)
Exp.int (n ++ m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_float (v +. w)
Exp.float (v +. w)
| Exp.UnOp(Unop.Neg, f1, _), f2
| f2, Exp.UnOp(Unop.Neg, f1, _) ->
Exp.BinOp (ominus, f2, f1)
@ -637,10 +637,10 @@ let sym_eval abs e =
| Exp.BinOp (Binop.PlusPI, e, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2)
| Exp.Const (Const.Cint n2), Exp.BinOp (Binop.PlusA, e, Exp.Const (Const.Cint n1))
| Exp.Const (Const.Cint n2), Exp.BinOp (Binop.PlusPI, e, Exp.Const (Const.Cint n1)) ->
e +++ (Sil.exp_int (n1 ++ n2))
e +++ (Exp.int (n1 ++ n2))
| Exp.BinOp (Binop.MinusA, Exp.Const (Const.Cint n1), e), Exp.Const (Const.Cint n2)
| Exp.Const (Const.Cint n2), Exp.BinOp (Binop.MinusA, Exp.Const (Const.Cint n1), e) ->
Sil.exp_int (n1 ++ n2) --- e
Exp.int (n1 ++ n2) --- e
| Exp.BinOp (Binop.MinusA, e1, e2), e3 -> (* (e1-e2)+e3 --> e1 + (e3-e2) *)
(* progress: brings + to the outside *)
eval (e1 +++ (e3 --- e2))
@ -651,8 +651,8 @@ let sym_eval abs e =
| Exp.Var _, Exp.Var _ ->
e1' +++ e2'
| _ ->
if abs && isPlusA then Sil.exp_get_undefined false else
if abs && not isPlusA then e1' +++ (Sil.exp_get_undefined false)
if abs && isPlusA then Exp.get_undefined false else
if abs && not isPlusA then e1' +++ (Exp.get_undefined false)
else e1' +++ e2'
end
| Exp.BinOp (Binop.MinusA as ominus, e1, e2)
@ -663,7 +663,7 @@ let sym_eval abs e =
let oplus = if isMinusA then Binop.PlusA else Binop.PlusPI in
let (+++) x y = Exp.BinOp (oplus, x, y) in
let (---) x y = Exp.BinOp (ominus, x, y) in
if Exp.equal e1' e2' then Sil.exp_zero
if Exp.equal e1' e2' then Exp.zero
else begin
match e1', e2' with
| Exp.Const c, _ when iszero_int_float c ->
@ -671,22 +671,22 @@ let sym_eval abs e =
| _, Exp.Const c when iszero_int_float c ->
e1'
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_int (n -- m)
Exp.int (n -- m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_float (v -. w)
Exp.float (v -. w)
| _, Exp.UnOp (Unop.Neg, f2, _) ->
eval (e1 +++ f2)
| _ , Exp.Const(Const.Cint n) ->
eval (e1' +++ (Sil.exp_int (IntLit.neg n)))
eval (e1' +++ (Exp.int (IntLit.neg n)))
| Exp.Const _, _ ->
e1' --- e2'
| Exp.Var _, Exp.Var _ ->
e1' --- e2'
| _, _ ->
if abs then Sil.exp_get_undefined false else e1' --- e2'
if abs then Exp.get_undefined false else e1' --- e2'
end
| Exp.BinOp (Binop.MinusPP, e1, e2) ->
if abs then Sil.exp_get_undefined false
if abs then Exp.get_undefined false
else Exp.BinOp (Binop.MinusPP, eval e1, eval e2)
| Exp.BinOp (Binop.Mult, e1, e2) ->
let e1' = eval e1 in
@ -694,28 +694,28 @@ let sym_eval abs e =
begin
match e1', e2' with
| Exp.Const c, _ when iszero_int_float c ->
Sil.exp_zero
Exp.zero
| Exp.Const c, _ when isone_int_float c ->
e2'
| Exp.Const c, _ when isminusone_int_float c ->
eval (Exp.UnOp (Unop.Neg, e2', None))
| _, Exp.Const c when iszero_int_float c ->
Sil.exp_zero
Exp.zero
| _, Exp.Const c when isone_int_float c ->
e1'
| _, Exp.Const c when isminusone_int_float c ->
eval (Exp.UnOp (Unop.Neg, e1', None))
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_int (IntLit.mul n m)
Exp.int (IntLit.mul n m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_float (v *. w)
Exp.float (v *. w)
| Exp.Var _, Exp.Var _ ->
Exp.BinOp(Binop.Mult, e1', e2')
| _, Exp.Sizeof _
| Exp.Sizeof _, _ ->
Exp.BinOp(Binop.Mult, e1', e2')
| _, _ ->
if abs then Sil.exp_get_undefined false else Exp.BinOp(Binop.Mult, e1', e2')
if abs then Exp.get_undefined false else Exp.BinOp(Binop.Mult, e1', e2')
end
| Exp.BinOp (Binop.Div, e1, e2) ->
let e1' = eval e1 in
@ -723,15 +723,15 @@ let sym_eval abs e =
begin
match e1', e2' with
| _, Exp.Const c when iszero_int_float c ->
Sil.exp_get_undefined false
Exp.get_undefined false
| Exp.Const c, _ when iszero_int_float c ->
e1'
| _, Exp.Const c when isone_int_float c ->
e1'
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_int (IntLit.div n m)
Exp.int (IntLit.div n m)
| Exp.Const (Const.Cfloat v), Exp.Const (Const.Cfloat w) ->
Sil.exp_float (v /.w)
Exp.float (v /.w)
| Exp.Sizeof (Typ.Tarray (elt, _), Some len, _), Exp.Sizeof (elt2, None, _)
(* pattern: sizeof(elt[len]) / sizeof(elt) = len *)
when Typ.equal elt elt2 ->
@ -741,7 +741,7 @@ let sym_eval abs e =
when Typ.equal elt elt2 ->
Exp.Const (Const.Cint len)
| _ ->
if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Div, e1', e2')
if abs then Exp.get_undefined false else Exp.BinOp (Binop.Div, e1', e2')
end
| Exp.BinOp (Binop.Mod, e1, e2) ->
let e1' = eval e1 in
@ -749,20 +749,20 @@ let sym_eval abs e =
begin
match e1', e2' with
| _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
Sil.exp_get_undefined false
Exp.get_undefined false
| Exp.Const (Const.Cint i), _ when IntLit.iszero i ->
e1'
| _, Exp.Const (Const.Cint i) when IntLit.isone i ->
Sil.exp_zero
Exp.zero
| Exp.Const (Const.Cint n), Exp.Const (Const.Cint m) ->
Sil.exp_int (IntLit.rem n m)
Exp.int (IntLit.rem n m)
| _ ->
if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Mod, e1', e2')
if abs then Exp.get_undefined false else Exp.BinOp (Binop.Mod, e1', e2')
end
| Exp.BinOp (Binop.Shiftlt, e1, e2) ->
if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Shiftlt, eval e1, eval e2)
if abs then Exp.get_undefined false else Exp.BinOp (Binop.Shiftlt, eval e1, eval e2)
| Exp.BinOp (Binop.Shiftrt, e1, e2) ->
if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.Shiftrt, eval e1, eval e2)
if abs then Exp.get_undefined false else Exp.BinOp (Binop.Shiftrt, eval e1, eval e2)
| Exp.BinOp (Binop.BAnd, e1, e2) ->
let e1' = eval e1 in
let e2' = eval e2 in
@ -772,9 +772,9 @@ let sym_eval abs e =
| _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
e2'
| Exp.Const (Const.Cint i1), Exp.Const(Const.Cint i2) ->
Sil.exp_int (IntLit.logand i1 i2)
Exp.int (IntLit.logand i1 i2)
| _ ->
if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.BAnd, e1', e2')
if abs then Exp.get_undefined false else Exp.BinOp (Binop.BAnd, e1', e2')
end
| Exp.BinOp (Binop.BOr, e1, e2) ->
let e1' = eval e1 in
@ -785,9 +785,9 @@ let sym_eval abs e =
| _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
e1'
| Exp.Const (Const.Cint i1), Exp.Const(Const.Cint i2) ->
Sil.exp_int (IntLit.logor i1 i2)
Exp.int (IntLit.logor i1 i2)
| _ ->
if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.BOr, e1', e2')
if abs then Exp.get_undefined false else Exp.BinOp (Binop.BOr, e1', e2')
end
| Exp.BinOp (Binop.BXor, e1, e2) ->
let e1' = eval e1 in
@ -798,9 +798,9 @@ let sym_eval abs e =
| _, Exp.Const (Const.Cint i) when IntLit.iszero i ->
e1'
| Exp.Const (Const.Cint i1), Exp.Const(Const.Cint i2) ->
Sil.exp_int (IntLit.logxor i1 i2)
Exp.int (IntLit.logxor i1 i2)
| _ ->
if abs then Sil.exp_get_undefined false else Exp.BinOp (Binop.BXor, e1', e2')
if abs then Exp.get_undefined false else Exp.BinOp (Binop.BXor, e1', e2')
end
| Exp.BinOp (Binop.PtrFld, e1, e2) ->
let e1' = eval e1 in
@ -810,7 +810,7 @@ let sym_eval abs e =
| Exp.Const (Const.Cptr_to_fld (fn, typ)) ->
eval (Exp.Lfield(e1', fn, typ))
| Exp.Const (Const.Cint i) when IntLit.iszero i ->
Sil.exp_zero (* cause a NULL dereference *)
Exp.zero (* cause a NULL dereference *)
| _ -> Exp.BinOp (Binop.PtrFld, e1', e2')
end
| Exp.Exn _ ->
@ -875,54 +875,54 @@ let mk_inequality e =
let nbase = exp_normalize_noabs Sil.sub_empty base in
(match nbase with
| Exp.BinOp(Binop.PlusA, base', Exp.Const (Const.Cint n')) ->
let new_offset = Sil.exp_int (n -- n') in
let new_offset = Exp.int (n -- n') in
let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.BinOp(Binop.PlusA, Exp.Const (Const.Cint n'), base') ->
let new_offset = Sil.exp_int (n -- n') in
let new_offset = Exp.int (n -- n') in
let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.BinOp(Binop.MinusA, base', Exp.Const (Const.Cint n')) ->
let new_offset = Sil.exp_int (n ++ n') in
let new_offset = Exp.int (n ++ n') in
let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.BinOp(Binop.MinusA, Exp.Const (Const.Cint n'), base') ->
let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
let new_offset = Exp.int (n' -- n -- IntLit.one) in
let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.UnOp(Unop.Neg, new_base, _) ->
(* In this case, base = -new_base. Construct -n-1 < new_base. *)
let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
let new_offset = Exp.int (IntLit.zero -- n -- IntLit.one) in
let new_e = Exp.BinOp (Binop.Lt, new_offset, new_base) in
Sil.Aeq (new_e, Sil.exp_one)
| _ -> Sil.Aeq (e, Sil.exp_one))
Sil.Aeq (new_e, Exp.one)
| _ -> Sil.Aeq (e, Exp.one))
| Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n), base) ->
(* n < base case *)
let nbase = exp_normalize_noabs Sil.sub_empty base in
(match nbase with
| Exp.BinOp(Binop.PlusA, base', Exp.Const (Const.Cint n')) ->
let new_offset = Sil.exp_int (n -- n') in
let new_offset = Exp.int (n -- n') in
let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.BinOp(Binop.PlusA, Exp.Const (Const.Cint n'), base') ->
let new_offset = Sil.exp_int (n -- n') in
let new_offset = Exp.int (n -- n') in
let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.BinOp(Binop.MinusA, base', Exp.Const (Const.Cint n')) ->
let new_offset = Sil.exp_int (n ++ n') in
let new_offset = Exp.int (n ++ n') in
let new_e = Exp.BinOp (Binop.Lt, new_offset, base') in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.BinOp(Binop.MinusA, Exp.Const (Const.Cint n'), base') ->
let new_offset = Sil.exp_int (n' -- n -- IntLit.one) in
let new_offset = Exp.int (n' -- n -- IntLit.one) in
let new_e = Exp.BinOp (Binop.Le, base', new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| Exp.UnOp(Unop.Neg, new_base, _) ->
(* In this case, base = -new_base. Construct new_base <= -n-1 *)
let new_offset = Sil.exp_int (IntLit.zero -- n -- IntLit.one) in
let new_offset = Exp.int (IntLit.zero -- n -- IntLit.one) in
let new_e = Exp.BinOp (Binop.Le, new_base, new_offset) in
Sil.Aeq (new_e, Sil.exp_one)
| _ -> Sil.Aeq (e, Sil.exp_one))
| _ -> Sil.Aeq (e, Sil.exp_one)
Sil.Aeq (new_e, Exp.one)
| _ -> Sil.Aeq (e, Exp.one))
| _ -> Sil.Aeq (e, Exp.one)
(** Normalize an inequality *)
let inequality_normalize a =
@ -964,12 +964,12 @@ let inequality_normalize a =
| e:: el -> Exp.BinOp(Binop.PlusA, e, exp_list_to_sum el) in
let norm_from_exp e =
match normalize_posnegoff (exp_to_posnegoff e) with
| [],[], n -> Exp.BinOp(Binop.Le, Sil.exp_int n, Sil.exp_zero)
| [], neg, n -> Exp.BinOp(Binop.Lt, Sil.exp_int (n -- IntLit.one), exp_list_to_sum neg)
| pos, [], n -> Exp.BinOp(Binop.Le, exp_list_to_sum pos, Sil.exp_int (IntLit.zero -- n))
| [],[], n -> Exp.BinOp(Binop.Le, Exp.int n, Exp.zero)
| [], neg, n -> Exp.BinOp(Binop.Lt, Exp.int (n -- IntLit.one), exp_list_to_sum neg)
| pos, [], n -> Exp.BinOp(Binop.Le, exp_list_to_sum pos, Exp.int (IntLit.zero -- n))
| pos, neg, n ->
let lhs_e = Exp.BinOp(Binop.MinusA, exp_list_to_sum pos, exp_list_to_sum neg) in
Exp.BinOp(Binop.Le, lhs_e, Sil.exp_int (IntLit.zero -- n)) in
Exp.BinOp(Binop.Le, lhs_e, Exp.int (IntLit.zero -- n)) in
let ineq = match a with
| Sil.Aeq (ineq, Exp.Const (Const.Cint i)) when IntLit.isone i ->
ineq
@ -979,7 +979,7 @@ let inequality_normalize a =
let e = Exp.BinOp(Binop.MinusA, e1, e2) in
mk_inequality (norm_from_exp e)
| Exp.BinOp(Binop.Lt, e1, e2) ->
let e = Exp.BinOp(Binop.MinusA, Exp.BinOp(Binop.MinusA, e1, e2), Sil.exp_minus_one) in
let e = Exp.BinOp(Binop.MinusA, Exp.BinOp(Binop.MinusA, e1, e2), Exp.minus_one) in
mk_inequality (norm_from_exp e)
| _ -> a
@ -994,14 +994,14 @@ let atom_normalize sub a0 =
| Exp.BinOp(Binop.PlusA, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2)
(* e1+n1==n2 ---> e1==n2-n1 *)
| Exp.BinOp(Binop.PlusPI, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2) ->
(e1, Sil.exp_int (n2 -- n1))
(e1, Exp.int (n2 -- n1))
| Exp.BinOp(Binop.MinusA, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2)
(* e1-n1==n2 ---> e1==n1+n2 *)
| Exp.BinOp(Binop.MinusPI, e1, Exp.Const (Const.Cint n1)), Exp.Const (Const.Cint n2) ->
(e1, Sil.exp_int (n1 ++ n2))
(e1, Exp.int (n1 ++ n2))
| Exp.BinOp(Binop.MinusA, Exp.Const (Const.Cint n1), e1), Exp.Const (Const.Cint n2) ->
(* n1-e1 == n2 -> e1==n1-n2 *)
(e1, Sil.exp_int (n1 -- n2))
(e1, Exp.int (n1 -- n2))
| Exp.Lfield (e1', fld1, _), Exp.Lfield (e2', fld2, _) ->
if Ident.fieldname_equal fld1 fld2
then normalize_eq (e1', e2')
@ -1015,7 +1015,7 @@ let atom_normalize sub a0 =
match e1, e2 with
| Exp.UnOp (Unop.LNot, e1', _), Exp.Const (Const.Cint i)
| Exp.Const (Const.Cint i), Exp.UnOp (Unop.LNot, e1', _) when IntLit.iszero i ->
(e1', Sil.exp_zero, true)
(e1', Exp.zero, true)
| _ -> (e1, e2, false) in
let handle_boolean_operation from_equality e1 e2 =
let ne1 = exp_normalize sub e1 in
@ -1043,9 +1043,9 @@ let atom_normalize sub a0 =
(** Negate an atom *)
let atom_negate = function
| Sil.Aeq (Exp.BinOp (Binop.Le, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
mk_inequality (Sil.exp_lt e2 e1)
mk_inequality (Exp.lt e2 e1)
| Sil.Aeq (Exp.BinOp (Binop.Lt, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
mk_inequality (Sil.exp_le e2 e1)
mk_inequality (Exp.le e2 e1)
| Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
| Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
| Sil.Apred (a, es) -> Sil.Anpred (a, es)
@ -1093,7 +1093,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
then
match typ with
| Typ.Tfloat _ -> Exp.Const (Const.Cfloat 0.0)
| _ -> Sil.exp_zero
| _ -> Exp.zero
else
create_fresh_var () in
match typ, len with
@ -1108,7 +1108,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
field, but always return None so that only the last field receives len *)
let f (fld, t, a) (flds, len) =
if Typ.is_objc_ref_counter_field (fld, t, a) then
((fld, Sil.Eexp (Sil.exp_one, inst)) :: flds, None)
((fld, Sil.Eexp (Exp.one, inst)) :: flds, None)
else
((fld, create_strexp_of_type tenvo struct_init_mode t len inst) :: flds, None) in
let flds, _ = IList.fold_right f instance_fields ([], len) in
@ -1116,7 +1116,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ len inst =
)
| Typ.Tarray (_, len_opt), None ->
let len = match len_opt with
| None -> Sil.exp_get_undefined false
| None -> Exp.get_undefined false
| Some len -> Exp.Const (Const.Cint len) in
Sil.Earray (len, [], inst)
| Typ.Tarray _, Some len ->
@ -1249,11 +1249,11 @@ let pi_tighten_ineq pi =
let ineq_list' =
let le_ineq_list =
IList.map
(fun (e, n) -> mk_inequality (Exp.BinOp(Binop.Le, e, Sil.exp_int n)))
(fun (e, n) -> mk_inequality (Exp.BinOp(Binop.Le, e, Exp.int n)))
le_list_tightened in
let lt_ineq_list =
IList.map
(fun (n, e) -> mk_inequality (Exp.BinOp(Binop.Lt, Sil.exp_int n, e)))
(fun (n, e) -> mk_inequality (Exp.BinOp(Binop.Lt, Exp.int n, e)))
lt_list_tightened in
le_ineq_list @ lt_ineq_list in
let nonineq_list' =
@ -1380,7 +1380,7 @@ let exp_normalize_prop prop exp =
Config.run_with_abs_val_equal_zero (exp_normalize prop.sub) exp
let lexp_normalize_prop p lexp =
let root = Sil.root_of_lexp lexp in
let root = Exp.root_of_lexp lexp in
let offsets = Sil.exp_get_offsets lexp in
let nroot = exp_normalize_prop p root in
let noffsets =
@ -1642,13 +1642,13 @@ let sigma_remove_emptylseg sigma =
| Sil.Hpointsto _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
| Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) :: sigma'
when (Exp.equal e1 Sil.exp_zero) || (Exp.Set.mem e1 alloc_set) ->
when (Exp.equal e1 Exp.zero) || (Exp.Set.mem e1 alloc_set) ->
f (Sil.Aeq(e1, e2) :: eqs_zero) sigma_passed sigma'
| Sil.Hlseg _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
| Sil.Hdllseg (Sil.Lseg_PE, _, iF, oB, oF, iB, _) :: sigma'
when (Exp.equal iF Sil.exp_zero) || (Exp.Set.mem iF alloc_set)
|| (Exp.equal iB Sil.exp_zero) || (Exp.Set.mem iB alloc_set) ->
when (Exp.equal iF Exp.zero) || (Exp.Set.mem iF alloc_set)
|| (Exp.equal iB Exp.zero) || (Exp.Set.mem iB alloc_set) ->
f (Sil.Aeq(iF, oF):: Sil.Aeq(iB, oB):: eqs_zero) sigma_passed sigma'
| Sil.Hdllseg _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
@ -1683,14 +1683,14 @@ let normalize_and_strengthen_atom (p : normal t) (a : Sil.atom) : Sil.atom =
match a' with
| Sil.Aeq (Exp.BinOp (Binop.Le, Exp.Var id, Exp.Const (Const.Cint n)), Exp.Const (Const.Cint i))
when IntLit.isone i ->
let lower = Sil.exp_int (n -- IntLit.one) in
let a_lower = Sil.Aeq (Exp.BinOp (Binop.Lt, lower, Exp.Var id), Sil.exp_one) in
let lower = Exp.int (n -- IntLit.one) in
let a_lower = Sil.Aeq (Exp.BinOp (Binop.Lt, lower, Exp.Var id), Exp.one) in
if not (IList.mem Sil.atom_equal a_lower p.pi) then a'
else Sil.Aeq (Exp.Var id, Sil.exp_int n)
else Sil.Aeq (Exp.Var id, Exp.int n)
| Sil.Aeq (Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n), Exp.Var id), Exp.Const (Const.Cint i))
when IntLit.isone i ->
let upper = Sil.exp_int (n ++ IntLit.one) in
let a_upper = Sil.Aeq (Exp.BinOp (Binop.Le, Exp.Var id, upper), Sil.exp_one) in
let upper = Exp.int (n ++ IntLit.one) in
let a_upper = Sil.Aeq (Exp.BinOp (Binop.Le, Exp.Var id, upper), Exp.one) in
if not (IList.mem Sil.atom_equal a_upper p.pi) then a'
else Sil.Aeq (Exp.Var id, upper)
| Sil.Aeq (Exp.BinOp (Binop.Ne, e1, e2), Exp.Const (Const.Cint i)) when IntLit.isone i ->
@ -1924,7 +1924,7 @@ let replace_objc_null prop lhs_exp rhs_exp =
match get_objc_null_attribute prop rhs_exp, rhs_exp with
| Some atom, Exp.Var _ ->
let prop = remove_attribute_from_exp prop atom in
let prop = conjoin_eq rhs_exp Sil.exp_zero prop in
let prop = conjoin_eq rhs_exp Exp.zero prop in
let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in
add_or_replace_attribute prop natom
| _ -> prop
@ -1940,7 +1940,7 @@ let rec nullify_exp_with_objc_null prop exp =
(match get_objc_null_attribute prop exp with
| Some atom ->
let prop' = remove_attribute_from_exp prop atom in
conjoin_eq exp Sil.exp_zero prop'
conjoin_eq exp Exp.zero prop'
| _ -> prop)
| _ -> prop
@ -2194,7 +2194,7 @@ let compute_reindexing fav_add get_id_offset list =
let transform x =
let id, offset = match get_id_offset x with None -> assert false | Some io -> io in
let base_new = Exp.Var (Ident.create_fresh Ident.kprimed) in
let offset_new = Sil.exp_int (IntLit.neg offset) in
let offset_new = Exp.int (IntLit.neg offset) in
let exp_new = Exp.BinOp(Binop.PlusA, base_new, offset_new) in
(id, exp_new) in
let reindexing = IList.map transform list_passed in
@ -2794,7 +2794,7 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc =
| Binop.LOr -> Exp.UnOp(Unop.LNot, e1, None), e1, IntLit.one
| _ -> assert false in
let cond_res1 = Exp.BinOp(Binop.Eq, Exp.Var id, e2) in
let cond_res2 = Exp.BinOp(Binop.Eq, Exp.Var id, Sil.exp_int res) in
let cond_res2 = Exp.BinOp(Binop.Eq, Exp.Var id, Exp.int res) in
let mk_prune cond =
(* don't report always true/false *)
Sil.Prune (cond, loc, true, Sil.Ik_land_lor) in

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

@ -72,9 +72,9 @@ end = struct
let equal entry1 entry2 = compare entry1 entry2 = 0
let to_leq (e1, e2, n) =
Exp.BinOp(Binop.MinusA, e1, e2), Sil.exp_int n
Exp.BinOp(Binop.MinusA, e1, e2), Exp.int n
let to_lt (e1, e2, n) =
Sil.exp_int (IntLit.zero -- n -- IntLit.one), Exp.BinOp(Binop.MinusA, e2, e1)
Exp.int (IntLit.zero -- n -- IntLit.one), Exp.BinOp(Binop.MinusA, e2, e1)
let to_triple entry = entry
let from_leq acc (e1, e2) =
@ -253,7 +253,7 @@ end = struct
mutable neqs: (Exp.t * Exp.t) list; (** ne facts [e1 != e2] *)
}
let inconsistent_ineq = { leqs = [(Sil.exp_one, Sil.exp_zero)]; lts = []; neqs = [] }
let inconsistent_ineq = { leqs = [(Exp.one, Exp.zero)]; lts = []; neqs = [] }
let leq_compare (e1, e2) (f1, f2) =
let c1 = Exp.compare e1 f1 in
@ -336,7 +336,7 @@ end = struct
let umap = umap_create_from_leqs Exp.Map.empty leqs in
let umap' = umap_improve_by_difference_constraints umap diff_constraints2 in
let leqs' = Exp.Map.fold
(fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs)
(fun e upper acc_leqs -> (e, Exp.int upper):: acc_leqs)
umap' [] in
let leqs'' = (IList.map DiffConstr.to_leq diff_constraints2) @ leqs' in
leqs_sort_then_remove_redundancy leqs'' in
@ -344,7 +344,7 @@ end = struct
let lmap = lmap_create_from_lts Exp.Map.empty lts in
let lmap' = lmap_improve_by_difference_constraints lmap diff_constraints2 in
let lts' = Exp.Map.fold
(fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts)
(fun e lower acc_lts -> (Exp.int lower, e):: acc_lts)
lmap' [] in
let lts'' = (IList.map DiffConstr.to_lt diff_constraints2) @ lts' in
lts_sort_then_remove_redundancy lts'' in
@ -372,7 +372,7 @@ end = struct
let leqs = ref [] in
let lts = ref [] in
let add_lt_minus1_e e =
lts := (Sil.exp_minus_one, e)::!lts in
lts := (Exp.minus_one, e)::!lts in
let texp_is_unsigned = function
| Exp.Sizeof (Typ.Tint ik, _, _) -> Typ.ikind_is_unsigned ik
| _ -> false in
@ -545,7 +545,7 @@ let check_equal prop e1 e2 =
(** Check [ |- e=0]. Result [false] means "don't know". *)
let check_zero e =
check_equal Prop.prop_emp e Sil.exp_zero
check_equal Prop.prop_emp e Exp.zero
(** [is_root prop base_exp exp] checks whether [base_exp =
exp.offlist] for some list of offsets [offlist]. If so, it returns
@ -631,7 +631,7 @@ let check_disequal prop e1 e2 =
if (k == Sil.Lseg_NE || check_pi_implies_disequal e1 e2) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (true, sigma_irrelevant')
else if (Exp.equal e2 Sil.exp_zero) then
else if (Exp.equal e2 Exp.zero) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (false, sigma_irrelevant')
else
@ -653,14 +653,14 @@ let check_disequal prop e1 e2 =
if (check_pi_implies_disequal iF oF) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (true, sigma_irrelevant')
else if (Exp.equal oF Sil.exp_zero) then
else if (Exp.equal oF Exp.zero) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (false, sigma_irrelevant')
else
let sigma_rest' = (IList.rev sigma_irrelevant) @ sigma_rest
in f [] oF sigma_rest') in
let f_null_check sigma_irrelevant e sigma_rest =
if not (Exp.equal e Sil.exp_zero) then f sigma_irrelevant e sigma_rest
if not (Exp.equal e Exp.zero) then f sigma_irrelevant e sigma_rest
else
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (false, sigma_irrelevant')
@ -680,7 +680,7 @@ let check_le_normalized prop e1 e2 =
let eL, eR, off = match e1, e2 with
| Exp.BinOp(Binop.MinusA, f1, f2), Exp.Const (Const.Cint n) ->
if Exp.equal f1 f2
then Sil.exp_zero, Sil.exp_zero, n
then Exp.zero, Exp.zero, n
else f1, f2, n
| _ ->
e1, e2, IntLit.zero in
@ -827,7 +827,7 @@ let check_inconsistency_base prop =
let pi = Prop.get_pi prop in
let sigma = Prop.get_sigma prop in
let inconsistent_ptsto _ =
check_allocatedness prop Sil.exp_zero in
check_allocatedness prop Exp.zero in
let inconsistent_this_self_var () =
let procdesc =
Cfg.Node.get_proc_desc (State.get_node ()) in
@ -845,7 +845,7 @@ let check_inconsistency_base prop =
procedure_attr.ProcAttributes.is_cpp_instance_method in
let do_hpred = function
| Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) ->
Exp.equal e Sil.exp_zero &&
Exp.equal e Exp.zero &&
Pvar.is_seed pv &&
(is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
| _ -> false in
@ -1174,7 +1174,7 @@ let exp_imply calc_missing subs e1_in e2_in : subst2 =
| Exp.Const (Const.Cint _), Exp.BinOp (Binop.PlusPI, _, _) ->
raise (IMPL_EXC ("pointer+index cannot evaluate to a constant", subs, (EXC_FALSE_EXPS (e1, e2))))
| Exp.Const (Const.Cint n1), Exp.BinOp (Binop.PlusA, f1, Exp.Const (Const.Cint n2)) ->
do_imply subs (Sil.exp_int (n1 -- n2)) f1
do_imply subs (Exp.int (n1 -- n2)) f1
| Exp.BinOp(op1, e1, f1), Exp.BinOp(op2, e2, f2) when op1 == op2 ->
do_imply (do_imply subs e1 e2) f1 f2
| Exp.BinOp (Binop.PlusA, Exp.Var v1, e1), e2 ->
@ -1286,10 +1286,10 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs
sexp_imply source calc_index_frame calc_missing subs (Sil.Estruct (fsel', inst')) se2 typ2
| Sil.Eexp _, Sil.Earray (len, _, inst)
| Sil.Estruct _, Sil.Earray (len, _, inst) ->
let se1' = Sil.Earray (len, [(Sil.exp_zero, se1)], inst) in
let se1' = Sil.Earray (len, [(Exp.zero, se1)], inst) in
sexp_imply source calc_index_frame calc_missing subs se1' se2 typ2
| Sil.Earray (len, _, _), Sil.Eexp (_, inst) ->
let se2' = Sil.Earray (len, [(Sil.exp_zero, se2)], inst) in
let se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in
let typ2' = Typ.Tarray (typ2, None) in
(* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2
argument is only used by eventually passing its value to Typ.struct_typ_fld, Exp.Lfield,
@ -1468,7 +1468,7 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
| _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
let len = match t' with
| Exp.Sizeof (_, Some len, _) -> len
| _ -> Sil.exp_get_undefined false in
| _ -> Exp.get_undefined false in
let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in
expand true true hpred'
| Sil.Hpointsto (Exp.BinOp (Binop.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) ->
@ -1713,7 +1713,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
of length given by its type only active in type_size mode *)
let sexp_imply_preprocess se1 texp1 se2 = match se1, texp1, se2 with
| Sil.Eexp (_, inst), Exp.Sizeof _, Sil.Earray _ when Config.type_size ->
let se1' = Sil.Earray (texp1, [(Sil.exp_zero, se1)], inst) in
let se1' = Sil.Earray (texp1, [(Exp.zero, se1)], inst) in
L.d_strln_color Orange "sexp_imply_preprocess"; L.d_str " se1: "; Sil.d_sexp se1; L.d_ln (); L.d_str " se1': "; Sil.d_sexp se1'; L.d_ln ();
se1'
| _ -> se1
@ -1780,7 +1780,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
(match Prop.prop_iter_current iter1' with
| Sil.Hpointsto (e1, se1, texp1), _ ->
(try
let typ2 = Sil.texp_to_typ (Some Typ.Tvoid) texp2 in
let typ2 = Exp.texp_to_typ (Some Typ.Tvoid) texp2 in
let typing_frame, typing_missing = texp_imply tenv subs texp1 texp2 e1 calc_missing in
let se1' = sexp_imply_preprocess se1 texp1 se2 in
let subs', fld_frame, fld_missing = sexp_imply e1 calc_index_frame calc_missing subs se1' se2 typ2 in
@ -1970,11 +1970,11 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
let len = IntLit.of_int (1 + String.length s) in
let root = Exp.Const (Const.Cstr s) in
let sexp =
let index = Sil.exp_int (IntLit.of_int (String.length s)) in
let index = Exp.int (IntLit.of_int (String.length s)) in
match !Config.curr_language with
| Config.Clang ->
Sil.Earray
(Sil.exp_int len, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none)
(Exp.int len, [(index, Sil.Eexp (Exp.zero, Sil.inst_none))], Sil.inst_none)
| Config.Java ->
let mk_fld_sexp s =
let fld = Ident.create_fieldname (Mangled.from_string s) 0 in
@ -2040,7 +2040,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
| None ->
let subs' = match hpred2' with
| Sil.Hpointsto (e2, se2, te2) ->
let typ2 = Sil.texp_to_typ (Some Typ.Tvoid) te2 in
let typ2 = Exp.texp_to_typ (Some Typ.Tvoid) te2 in
sexp_imply_nolhs e2 calc_missing subs se2 typ2
| _ -> subs in
ProverState.add_missing_sigma [hpred2'];
@ -2139,7 +2139,7 @@ let check_array_bounds (sub1, sub2) prop =
(* 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 = match len2 with
| _ -> [Exp.BinOp(Binop.PlusA, len2, Sil.exp_minus_one)] (* only check len *) in
| _ -> [Exp.BinOp(Binop.PlusA, len2, Exp.minus_one)] (* only check len *) in
IList.iter (fail_if_le len1) indices_to_check
| ProverState.BCfrom_pre _atom ->
let atom_neg = Prop.atom_negate (Sil.atom_sub sub2 _atom) in

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

@ -38,12 +38,12 @@ let check_bad_index pname p len index loc =
| _ -> false in
let index_provably_out_of_bound () =
let index_too_large = Prop.mk_inequality (Exp.BinOp (Binop.Le, len, index)) in
let index_negative = Prop.mk_inequality (Exp.BinOp (Binop.Le, index, Sil.exp_minus_one)) in
let index_negative = Prop.mk_inequality (Exp.BinOp (Binop.Le, index, Exp.minus_one)) in
(Prover.check_atom p index_too_large) || (Prover.check_atom p index_negative) in
let index_provably_in_bound () =
let len_minus_one = Exp.BinOp(Binop.PlusA, len, Sil.exp_minus_one) in
let len_minus_one = Exp.BinOp(Binop.PlusA, len, Exp.minus_one) in
let index_not_too_large = Prop.mk_inequality (Exp.BinOp(Binop.Le, index, len_minus_one)) in
let index_nonnegative = Prop.mk_inequality (Exp.BinOp(Binop.Le, Sil.exp_zero, index)) in
let index_nonnegative = Prop.mk_inequality (Exp.BinOp(Binop.Le, Exp.zero, index)) in
Prover.check_zero index || (* index 0 always in bound, even when we know nothing about len *)
((Prover.check_atom p index_not_too_large) && (Prover.check_atom p index_nonnegative)) in
let index_has_bounds () =
@ -199,11 +199,11 @@ let rec _strexp_extend_values
| [], Sil.Estruct _, _ ->
[([], se, typ)]
| [], Sil.Earray _, _ ->
let off_new = Sil.Off_index(Sil.exp_zero):: off in
let off_new = Sil.Off_index(Exp.zero):: off in
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
| (Sil.Off_fld _) :: _, Sil.Earray _, Typ.Tarray _ ->
let off_new = Sil.Off_index(Sil.exp_zero):: off in
let off_new = Sil.Off_index(Exp.zero):: off in
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
| (Sil.Off_fld (f, _)):: off', Sil.Estruct (fsel, inst'),
@ -253,11 +253,11 @@ let rec _strexp_extend_values
| (Sil.Off_index _):: _, Sil.Estruct _, Typ.Tstruct _ ->
(* L.d_strln_color Orange "turn into an array"; *)
let len = match se with
| Sil.Eexp (_, Sil.Ialloc) -> Sil.exp_one (* if allocated explicitly, we know len is 1 *)
| Sil.Eexp (_, Sil.Ialloc) -> Exp.one (* if allocated explicitly, we know len is 1 *)
| _ ->
if Config.type_size then Sil.exp_one (* Exp.Sizeof (typ, Subtype.exact) *)
if Config.type_size then Exp.one (* Exp.Sizeof (typ, Subtype.exact) *)
else Exp.Var (new_id ()) in
let se_new = Sil.Earray (len, [(Sil.exp_zero, se)], inst) in
let se_new = Sil.Earray (len, [(Exp.zero, se)], inst) in
let typ_new = Typ.Tarray (typ, None) in
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst
@ -384,7 +384,7 @@ let laundry_offset_for_footprint max_stamp offs_in =
let strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp
se te (off : Sil.offset list) inst =
let typ = Sil.texp_to_typ None te in
let typ = Exp.texp_to_typ None te in
let off', laundry_atoms =
let off', eqs = laundry_offset_for_footprint max_stamp off in
(* do laundry_offset whether footprint_part is true or not, so max_stamp is modified anyway *)
@ -410,7 +410,7 @@ let strexp_extend_values
atoms_se_typ_list_filtered
let collect_root_offset exp =
let root = Sil.root_of_lexp exp in
let root = Exp.root_of_lexp exp in
let offsets = Sil.exp_get_offsets exp in
(root, offsets)
@ -854,7 +854,7 @@ let rearrange_arith lexp prop =
end;
if (Config.array_level >= 2) then raise ARRAY_ACCESS
else
let root = Sil.root_of_lexp lexp in
let root = Exp.root_of_lexp lexp in
if Prover.check_allocatedness prop root then
raise ARRAY_ACCESS
else
@ -1103,7 +1103,7 @@ let rec iter_rearrange
if !Config.footprint then
prop_iter_add_hpred_footprint pname tenv prop iter' (lexp, typ) inst
else
if (Config.array_level >= 1 && not !Config.footprint && Sil.exp_pointer_arith lexp)
if (Config.array_level >= 1 && not !Config.footprint && Exp.pointer_arith lexp)
then rearrange_arith lexp prop
else begin
pp_rearrangement_error "cannot find predicate with root" prop lexp;
@ -1225,10 +1225,10 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
| _ -> true)
(Prop.get_sigma prop) &&
!nullable_obj_str <> None in
let root = Sil.root_of_lexp lexp in
let root = Exp.root_of_lexp lexp in
let is_deref_of_nullable =
let is_definitely_non_null exp prop =
Prover.check_disequal prop exp Sil.exp_zero in
Prover.check_disequal prop exp Exp.zero in
Config.report_nullable_inconsistency && not (is_definitely_non_null root prop)
&& is_only_pt_by_nullable_fld_or_param root in
let relevant_attributes_getters = [
@ -1249,7 +1249,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
| Exp.BinOp((Binop.PlusPI | Binop.PlusA | Binop.MinusPI | Binop.MinusA), base, _) -> base
| _ -> root in
get_relevant_attributes root_no_offset in
if Prover.check_zero (Sil.root_of_lexp root) || is_deref_of_nullable then
if Prover.check_zero (Exp.root_of_lexp root) || is_deref_of_nullable then
begin
let deref_str =
if is_deref_of_nullable then
@ -1287,7 +1287,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
let err_desc = Errdesc.explain_dereference ~use_buckets: true deref_str prop loc in
raise (Exceptions.Use_after_free (err_desc, __POS__))
| _ ->
if Prover.check_equal Prop.prop_emp (Sil.root_of_lexp root) Sil.exp_minus_one then
if Prover.check_equal Prop.prop_emp (Exp.root_of_lexp root) Exp.minus_one then
let deref_str = Localise.deref_str_dangling None in
let err_desc = Errdesc.explain_dereference deref_str prop loc in
raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__))
@ -1296,7 +1296,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
(* It's used to check that we don't call possibly null blocks *)
let check_call_to_objc_block_error pdesc prop fun_exp loc =
let fun_exp_may_be_null () = (* may be null if we don't know if it is definitely not null *)
not (Prover.check_disequal prop (Sil.root_of_lexp fun_exp) Sil.exp_zero) in
not (Prover.check_disequal prop (Exp.root_of_lexp fun_exp) Exp.zero) in
let try_explaining_exp e = (* when e is a temp var, try to find the pvar defining e*)
match e with
| Exp.Var id ->
@ -1366,7 +1366,7 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc
Exp.Lindex(ep, e)
| e -> e in
let ptr_tested_for_zero =
Prover.check_disequal prop (Sil.root_of_lexp nlexp) Sil.exp_zero in
Prover.check_disequal prop (Exp.root_of_lexp nlexp) Exp.zero in
let inst = Sil.inst_rearrange (not ptr_tested_for_zero) loc (State.get_path_pos ()) in
L.d_strln ".... Rearrangement Start ....";
L.d_str "Exp: "; Sil.d_exp nlexp; L.d_ln ();

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

@ -131,11 +131,11 @@ let rec apply_offlist
(f None, Prop.create_strexp_of_type (Some tenv) Prop.Fld_init typ None inst, typ, None)
end
| [], Sil.Earray _ ->
let offlist' = (Sil.Off_index Sil.exp_zero):: offlist in
let offlist' = (Sil.Off_index Exp.zero):: offlist in
apply_offlist
pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist' f inst lookup_inst
| (Sil.Off_fld _):: _, Sil.Earray _ ->
let offlist_new = Sil.Off_index(Sil.exp_zero) :: offlist in
let offlist_new = Sil.Off_index(Exp.zero) :: offlist in
apply_offlist
pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist_new f inst lookup_inst
| (Sil.Off_fld (fld, fld_typ)):: offlist', Sil.Estruct (fsel, inst') ->
@ -262,7 +262,7 @@ let update_iter iter pi sigma =
that could mean nonempty heaps. *)
let rec execute_nullify_se = function
| Sil.Eexp _ ->
Sil.Eexp (Sil.exp_zero, Sil.inst_nullify)
Sil.Eexp (Exp.zero, Sil.inst_nullify)
| Sil.Estruct (fsel, _) ->
let fsel' = IList.map (fun (fld, se) -> (fld, execute_nullify_se se)) fsel in
Sil.Estruct (fsel', Sil.inst_nullify)
@ -309,13 +309,13 @@ let prune_ineq ~is_strict ~positive prop e1 e2 =
if is_inconsistent then Propset.empty
else
let footprint = !Config.footprint in
let prop_with_ineq = Prop.conjoin_eq ~footprint prune_cond Sil.exp_one prop in
let prop_with_ineq = Prop.conjoin_eq ~footprint prune_cond Exp.one prop in
Propset.singleton prop_with_ineq
let rec prune ~positive condition prop =
match condition with
| Exp.Var _ | Exp.Lvar _ ->
prune_ne ~positive condition Sil.exp_zero prop
prune_ne ~positive condition Exp.zero prop
| Exp.Const (Const.Cint i) when IntLit.iszero i ->
if positive then Propset.empty else Propset.singleton prop
| Exp.Const (Const.Cint _ | Const.Cstr _ | Const.Cclass _) | Exp.Sizeof _ ->
@ -351,7 +351,7 @@ let rec prune ~positive condition prop =
let pruner = if positive then prune_union else prune_inter in
pruner ~positive condition1 condition2 prop
| Exp.BinOp _ | Exp.Lfield _ | Exp.Lindex _ ->
prune_ne ~positive condition Sil.exp_zero prop
prune_ne ~positive condition Exp.zero prop
| Exp.Exn _ ->
assert false
| Exp.Closure _ ->
@ -401,7 +401,7 @@ let call_should_be_skipped callee_pname summary =
let check_constant_string_dereference lexp =
let string_lookup s n =
let c = try Char.code (String.get s (IntLit.to_int n)) with Invalid_argument _ -> 0 in
Sil.exp_int (IntLit.of_int c) in
Exp.int (IntLit.of_int c) in
match lexp with
| Exp.BinOp(Binop.PlusPI, Exp.Const (Const.Cstr s), e)
| Exp.Lindex (Exp.Const (Const.Cstr s), e) ->
@ -410,7 +410,7 @@ let check_constant_string_dereference lexp =
when IntLit.geq n IntLit.zero &&
IntLit.leq n (IntLit.of_int (String.length s)) ->
string_lookup s n
| _ -> Sil.exp_get_undefined false in
| _ -> Exp.get_undefined false in
Some value
| Exp.Const (Const.Cstr s) ->
Some (string_lookup s IntLit.zero)
@ -730,7 +730,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
let is_receiver_null =
match actual_pars with
| (e, _) :: _
when Exp.equal e Sil.exp_zero ||
when Exp.equal e Exp.zero ||
Option.is_some (Prop.get_objc_null_attribute pre e) -> true
| _ -> false in
let add_objc_null_attribute_or_nullify_result prop =
@ -740,7 +740,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
| Some vfs ->
Prop.add_or_replace_attribute prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs]))
| None ->
Prop.conjoin_eq (Exp.Var ret_id) Sil.exp_zero prop
Prop.conjoin_eq (Exp.Var ret_id) Exp.zero prop
)
| _ -> prop in
if is_receiver_null then
@ -760,7 +760,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
if !Config.footprint && not is_undef then
let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *)
let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in
let propset = prune_ne ~positive:false receiver Sil.exp_zero pre_with_attr_or_null in
let propset = prune_ne ~positive:false receiver Exp.zero pre_with_attr_or_null in
if Propset.is_empty propset then []
else
let prop = IList.hd (Propset.to_proplist propset) in
@ -840,7 +840,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
prop (* don't assume nonnull if the procedure is annotated with @Nullable *)
else
match typ with
| Typ.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop
| Typ.Tptr _ -> Prop.conjoin_neq exp Exp.zero prop
| _ -> prop in
let add_tainted_post ret_exp callee_pname prop =
Prop.add_or_replace_attribute prop (Apred (Ataint callee_pname, [ret_exp])) in
@ -953,7 +953,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
with Rearrange.ARRAY_ACCESS ->
if (Config.array_level = 0) then assert false
else
let undef = Sil.exp_get_undefined false in
let undef = Exp.get_undefined false in
[Prop.conjoin_eq (Exp.Var id) undef prop_]
let load_ret_annots pname =

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

@ -298,7 +298,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
L.d_strln (" desc: " ^ (pp_to_string Localise.pp_error_desc error_desc));
error_desc in
let deref_no_null_check_pos =
if Exp.equal e_sub Sil.exp_zero then
if Exp.equal e_sub Exp.zero then
match find_dereference_without_null_check_in_sexp sexp with
| Some (_, pos) -> Some pos
| None -> None
@ -315,7 +315,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
(* In that case it raise a dangling pointer dereferece *)
if Prop.has_dangling_uninit_attribute spec_pre e then
Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some Sil.DAuninit)) )
else if Exp.equal e_sub Sil.exp_minus_one
else if Exp.equal e_sub Exp.minus_one
then Some (Deref_minusone, desc true (Localise.deref_str_dangling None))
else match Prop.get_resource_attribute actual_pre e_sub with
| Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) ->
@ -327,7 +327,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
| _ -> None) in
let check_hpred = function
| Sil.Hpointsto (lexp, se, _) ->
check_dereference (Sil.root_of_lexp lexp) se
check_dereference (Exp.root_of_lexp lexp) se
| _ -> None in
let deref_err_list = IList.fold_left (fun deref_errs hpred -> match check_hpred hpred with
| Some reason -> reason :: deref_errs
@ -449,7 +449,7 @@ and sexp_star_fld se1 se2 : Sil.strexp =
| Sil.Earray (len1, esel1, _), Sil.Earray (_, esel2, inst2) ->
Sil.Earray (len1, esel_star_fld esel1 esel2, inst2)
| Sil.Eexp (_, inst1), Sil.Earray (len2, esel2, _) ->
let esel1 = [(Sil.exp_zero, se1)] in
let esel1 = [(Exp.zero, se1)] in
Sil.Earray (len2, esel_star_fld esel1 esel2, inst1)
| _ ->
L.d_str "cannot star ";
@ -678,7 +678,7 @@ let combine
if !Config.footprint && posts = []
then (* in case of divergence, produce a prop *)
(* with updated footprint and inconsistent current *)
[(Prop.replace_pi [Sil.Aneq (Sil.exp_zero, Sil.exp_zero)] Prop.prop_emp, path_pre)]
[(Prop.replace_pi [Sil.Aneq (Exp.zero, Exp.zero)] Prop.prop_emp, path_pre)]
else
IList.map
(fun (p, path_post) ->
@ -885,7 +885,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
IList.exists
(function
| Sil.Apred (Aretval (pname, _), [exp]) when Procname.equal callee_pname pname ->
Prover.check_disequal prop exp Sil.exp_zero
Prover.check_disequal prop exp Exp.zero
| _ -> false)
(Prop.get_all_attributes prop) in
if last_call_ret_non_null then
@ -893,7 +893,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
IList.exists
(function
| Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (e, _), _) when Pvar.is_return pvar ->
Prover.check_equal (Prop.normalize prop) e Sil.exp_zero
Prover.check_equal (Prop.normalize prop) e Exp.zero
| _ -> false)
(Prop.get_sigma prop) in
IList.filter (fun (prop, _) -> not (returns_null prop)) posts
@ -1321,7 +1321,7 @@ let check_splitting_precondition sub1 sub2 =
let sigma_has_null_pointer sigma =
let hpred_null_pointer = function
| Sil.Hpointsto (e, _, _) ->
Exp.equal e Sil.exp_zero
Exp.equal e Exp.zero
| _ -> false in
IList.exists hpred_null_pointer sigma
*)

4
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -294,10 +294,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let prunes_tracking_var astate = function
| Exp.BinOp (Binop.Eq, lhs, rhs)
when is_tracking_exp astate lhs ->
Exp.equal rhs Sil.exp_one
Exp.equal rhs Exp.one
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, lhs, rhs), _)
when is_tracking_exp astate lhs ->
Exp.equal rhs Sil.exp_zero
Exp.equal rhs Exp.zero
| _ ->
false

2
infer/src/checkers/checkers.ml
Unescape View File

@ -199,7 +199,7 @@ let callback_check_write_to_parcel_java
let is_write_to_parcel this_expr this_type =
let method_match () =
Procname.java_get_method pname_java = "writeToParcel" in
let expr_match () = Sil.exp_is_this this_expr in
let expr_match () = Exp.is_this this_expr in
let type_match () =
let class_name =
Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "android.os.Parcelable") in

2
infer/src/checkers/codeQuery.ml
Unescape View File

@ -98,7 +98,7 @@ module Match = struct
Hashtbl.iter pp_item env
let exp_match env ae value = match ae, value with
| CodeQueryAst.Null, Vval e -> Exp.equal e Sil.exp_zero
| CodeQueryAst.Null, Vval e -> Exp.equal e Exp.zero
| CodeQueryAst.Null, _ -> false
| CodeQueryAst.ConstString s, (Vfun pn) -> string_contains s (Procname.to_string pn)
| CodeQueryAst.ConstString _, _ -> false

2
infer/src/checkers/liveness.ml
Unescape View File

@ -25,7 +25,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(* add all of the vars read in [exp] to the live set *)
let exp_add_live exp astate =
let (ids, pvars) = Sil.exp_get_vars exp in
let (ids, pvars) = Exp.get_vars exp in
let astate' =
IList.fold_left (fun astate_acc id -> Domain.add (Var.of_id id) astate_acc) astate ids in
IList.fold_left (fun astate_acc pvar -> Domain.add (Var.of_pvar pvar) astate_acc) astate' pvars

4
infer/src/checkers/patternMatch.ml
Unescape View File

@ -388,9 +388,9 @@ let get_fields_nullified procdesc =
(* walk through the instructions and look for instance fields that are assigned to null *)
let collect_nullified_flds (nullified_flds, this_ids) _ = function
| Sil.Set (Exp.Lfield (Exp.Var lhs, fld, _), _, rhs, _)
when Sil.exp_is_null_literal rhs && Ident.IdentSet.mem lhs this_ids ->
when Exp.is_null_literal rhs && Ident.IdentSet.mem lhs this_ids ->
(Ident.FieldSet.add fld nullified_flds, this_ids)
| Sil.Letderef (id, rhs, _, _) when Sil.exp_is_this rhs ->
| Sil.Letderef (id, rhs, _, _) when Exp.is_this rhs ->
(nullified_flds, Ident.IdentSet.add id this_ids)
| _ -> (nullified_flds, this_ids) in
let (nullified_flds, _) =

2
infer/src/clang/cArithmetic_trans.ml
Unescape View File

@ -134,7 +134,7 @@ let binary_operation_instruction context boi e1 typ e2 loc rhs_owning_method =
Printing.log_stats
"\nWARNING: Missing translation for Binary Operator Kind %s. Construct ignored...\n"
(Clang_ast_j.string_of_binary_operator_kind bok);
(Sil.exp_minus_one, [])
(Exp.minus_one, [])
let unary_operation_instruction uoi e typ loc =
let uok = Clang_ast_j.string_of_unary_operator_kind (uoi.Clang_ast_t.uoi_kind) in

10
infer/src/clang/cTrans.ml
Unescape View File

@ -347,7 +347,7 @@ struct
let nullPtrExpr_trans trans_state expr_info =
let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in
{ empty_res_trans with exps = [(Sil.exp_null, typ)]}
{ empty_res_trans with exps = [(Exp.null, typ)]}
let objCSelectorExpr_trans trans_state expr_info selector =
stringLiteral_trans trans_state expr_info selector
@ -381,7 +381,7 @@ struct
let exp =
try
let i = Int64.of_string integer_literal_info.Clang_ast_t.ili_value in
let exp = Sil.exp_int (IntLit.of_int64 i) in
let exp = Exp.int (IntLit.of_int64 i) in
exp
with
| Failure _ ->
@ -432,7 +432,7 @@ struct
"\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \
%s . Expression ignored, returned -1... \n"
(Clang_ast_j.string_of_unary_expr_or_type_trait_kind k);
{ empty_res_trans with exps =[(Sil.exp_minus_one, typ)]}
{ empty_res_trans with exps =[(Exp.minus_one, typ)]}
(* search the label into the hashtbl - create a fake node eventually *)
(* connect that node with this stmt *)
@ -1610,7 +1610,7 @@ struct
(* in initd_exps, then we assume that all the indices were initialized and *)
(* we don't need any assignments. *)
if IList.exists
((fun arr index -> Sil.exp_is_array_index_of index arr) var_exp)
((fun arr index -> Exp.is_array_index_of index arr) var_exp)
initd_exps
then []
else IList.map2 assign_instr lh rh_exps in
@ -2566,7 +2566,7 @@ struct
implicitValueInitExpr_trans trans_state expr_info
| GenericSelectionExpr _ (* to be fixed when we dump the right info in the ast *)
| SizeOfPackExpr _ ->
{ empty_res_trans with exps = [(Sil.exp_get_undefined false, Typ.Tvoid)] }
{ empty_res_trans with exps = [(Exp.get_undefined false, Typ.Tvoid)] }
| GCCAsmStmt (stmt_info, stmts) ->
gccAsmStmt_trans trans_state stmt_info stmts

8
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -24,7 +24,7 @@ let extract_item_from_singleton l warning_string failure_val =
| [item] -> item
| _ -> Printing.log_err "%s" warning_string; failure_val
let dummy_exp = (Sil.exp_minus_one, Typ.Tint Typ.IInt)
let dummy_exp = (Exp.minus_one, Typ.Tint Typ.IInt)
(* Extract the element of a singleton list. If the list is not a singleton *)
(* Gives a warning and return -1 as standard value indicating something *)
@ -61,9 +61,9 @@ struct
"\nWARNING: Missing expression for Conditional operator. Need to be fixed" in
let e_cond'' =
if branch then
Exp.BinOp(Binop.Ne, e_cond', Sil.exp_zero)
Exp.BinOp(Binop.Ne, e_cond', Exp.zero)
else
Exp.BinOp(Binop.Eq, e_cond', Sil.exp_zero) in
Exp.BinOp(Binop.Eq, e_cond', Exp.zero) in
let instrs_cond'= instrs_cond @ [Sil.Prune(e_cond'', loc, branch, ik)] in
create_node (prune_kind branch) instrs_cond' loc context
@ -449,7 +449,7 @@ let trans_assertion_failure sil_loc context =
{ empty_res_trans with root_nodes = [failure_node]; }
let trans_assume_false sil_loc context succ_nodes =
let instrs_cond = [Sil.Prune (Sil.exp_zero, sil_loc, true, Sil.Ik_land_lor)] in
let instrs_cond = [Sil.Prune (Exp.zero, sil_loc, true, Sil.Ik_land_lor)] in
let prune_node = Nodes.create_node (Nodes.prune_kind true) instrs_cond sil_loc context in
Cfg.Node.set_succs_exn context.CContext.cfg prune_node succ_nodes [];
{ empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] }

4
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -354,7 +354,7 @@ let typecheck_instr
Pvar.is_global pvar in
let pvar_to_str pvar =
if Sil.exp_is_this (Exp.Lvar pvar) then ""
if Exp.is_this (Exp.Lvar pvar) then ""
else Pvar.to_string pvar ^ "_" in
let res = match exp' with
@ -651,7 +651,7 @@ let typecheck_instr
not (TypeAnnotation.origin_is_fun_library ta) in
if checks.eradicate && should_report then
begin
let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Sil.exp_null) in
let cond = Exp.BinOp (Binop.Ne, Exp.Lvar pvar, Exp.null) in
EradicateChecks.report_error
find_canonical_duplicate
node

12
infer/src/java/jTrans.ml
Unescape View File

@ -525,7 +525,7 @@ let rec expression context pc expr =
then
(* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
(* Infer to understand the assert keyword in the expected way *)
(instrs, Sil.exp_zero, type_of_expr)
(instrs, Exp.zero, type_of_expr)
else
let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in
let tmp_id = Ident.create_fresh Ident.knormal in
@ -761,7 +761,7 @@ let is_this expr =
let assume_not_null loc sil_expr =
let builtin_infer_assume = Exp.Const (Const.Cfun ModelBuiltins.__infer_assume) in
let not_null_expr =
Exp.BinOp (Binop.Ne, sil_expr, Sil.exp_null) in
Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in
let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in
Sil.Call ([], builtin_infer_assume, call_args, loc, assume_call_flag)
@ -1003,12 +1003,12 @@ let rec instruction context pc instr : translation =
| JBir.Check (JBir.CheckNullPointer expr) when Config.report_runtime_exceptions ->
let (instrs, sil_expr, _) = expression context pc expr in
let not_null_node =
let sil_not_null = Exp.BinOp (Binop.Ne, sil_expr, Sil.exp_null) in
let sil_not_null = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
let sil_prune_not_null = Sil.Prune (sil_not_null, loc, true, Sil.Ik_if)
and not_null_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Not null") in
create_node not_null_kind (instrs @ [sil_prune_not_null]) in
let throw_npe_node =
let sil_is_null = Exp.BinOp (Binop.Eq, sil_expr, Sil.exp_null) in
let sil_is_null = Exp.BinOp (Binop.Eq, sil_expr, Exp.null) in
let sil_prune_null = Sil.Prune (sil_is_null, loc, true, Sil.Ik_if)
and npe_kind = Cfg.Node.Stmt_node "Throw NPE"
and npe_cn = JBasics.make_cn JConfig.npe_cl in
@ -1095,12 +1095,12 @@ let rec instruction context pc instr : translation =
let call = Sil.Call([ret_id], check_cast, args, loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in
let is_instance_node =
let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Sil.exp_zero) in
let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Exp.zero) in
let asssume_instance_of = Sil.Prune (check_is_false, loc, true, Sil.Ik_if)
and instance_of_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Is instance") in
create_node instance_of_kind (instrs @ [call; asssume_instance_of])
and throw_cast_exception_node =
let check_is_true = Exp.BinOp (Binop.Ne, res_ex, Sil.exp_one) in
let check_is_true = Exp.BinOp (Binop.Ne, res_ex, Exp.one) in
let asssume_not_instance_of = Sil.Prune (check_is_true, loc, true, Sil.Ik_if)
and throw_cast_exception_kind = Cfg.Node.Stmt_node "Class cast exception"
and cce_cn = JBasics.make_cn JConfig.cce_cl in

2
infer/src/llvm/lTrans.ml
Unescape View File

@ -25,7 +25,7 @@ let trans_variable (var : LAst.variable) : Exp.t = Exp.Var (ident_of_variable va
let trans_constant : LAst.constant -> Exp.t = function
| Cint i -> Exp.Const (Const.Cint (IntLit.of_int i))
| Cnull -> Sil.exp_null
| Cnull -> Exp.null
let trans_operand : LAst.operand -> Exp.t = function
| Var var -> trans_variable var

2
infer/src/unit/accessPathTests.ml
Unescape View File

@ -100,7 +100,7 @@ let tests =
check_make_ap xF_exp xF ~f_resolve_id;
let xFG_exp = Exp.Lfield (xF_exp, g_fieldname, dummy_typ) in
check_make_ap xFG_exp xFG ~f_resolve_id;
let xArr_exp = Exp.Lindex (x_exp, Sil.exp_zero) in
let xArr_exp = Exp.Lindex (x_exp, Exp.zero) in
check_make_ap xArr_exp xArr ~f_resolve_id;
(* make sure [f_resolve_id] works *)
let f_resolve_id_to_xF _ = Some xF in

2
infer/src/unit/analyzerTester.ml
Unescape View File

@ -114,7 +114,7 @@ module StructuredSil = struct
make_set ~rhs_typ ~lhs_exp ~rhs_exp
let var_assign_int lhs rhs =
let rhs_exp = Sil.exp_int (IntLit.of_int rhs) in
let rhs_exp = Exp.int (IntLit.of_int rhs) in
let rhs_typ = Typ.Tint Typ.IInt in
var_assign_exp ~rhs_typ lhs rhs_exp

2
infer/src/unit/livenessTests.ml
Unescape View File

@ -28,7 +28,7 @@ let tests =
Exp.Closure closure in
let unknown_cond =
(* don't want to use AnalyzerTest.unknown_exp because we'll treat it as a live var! *)
Sil.exp_zero in
Exp.zero in
let test_list = [
"basic_live",
[

Write Preview
Loading…
Cancel
Save