From 25a52c7bbcbe338800420cdf03d3d8f5cf9ca8b3 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 8 Aug 2016 09:48:01 -0700 Subject: [PATCH] Refactor operations on Exp.t in Sil to Exp Summary: No functional change. Reviewed By: cristianoc Differential Revision: D3669404 fbshipit-source-id: 1d1f11a --- infer/src/IR/Exp.re | 141 ++++++++++++ infer/src/IR/Exp.rei | 80 +++++++ infer/src/IR/Sil.re | 146 ------------ infer/src/IR/Sil.rei | 84 ------- infer/src/backend/absarray.ml | 14 +- infer/src/backend/dom.ml | 28 +-- infer/src/backend/dotty.ml | 22 +- infer/src/backend/interproc.ml | 4 +- infer/src/backend/modelBuiltins.ml | 20 +- infer/src/backend/prop.ml | 224 +++++++++---------- infer/src/backend/prover.ml | 46 ++-- infer/src/backend/rearrange.ml | 36 +-- infer/src/backend/symExec.ml | 26 +-- infer/src/backend/tabulation.ml | 16 +- infer/src/checkers/annotationReachability.ml | 4 +- infer/src/checkers/checkers.ml | 2 +- infer/src/checkers/codeQuery.ml | 2 +- infer/src/checkers/liveness.ml | 2 +- infer/src/checkers/patternMatch.ml | 4 +- infer/src/clang/cArithmetic_trans.ml | 2 +- infer/src/clang/cTrans.ml | 10 +- infer/src/clang/cTrans_utils.ml | 8 +- infer/src/eradicate/typeCheck.ml | 4 +- infer/src/java/jTrans.ml | 12 +- infer/src/llvm/lTrans.ml | 2 +- infer/src/unit/accessPathTests.ml | 2 +- infer/src/unit/analyzerTester.ml | 2 +- infer/src/unit/livenessTests.ml | 2 +- 28 files changed, 468 insertions(+), 477 deletions(-) diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re index a6a471ba1..231706953 100644 --- a/infer/src/IR/Exp.re +++ b/infer/src/IR/Exp.re @@ -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 ([], []) +}; diff --git a/infer/src/IR/Exp.rei b/infer/src/IR/Exp.rei index efe0e2130..0352bc3c9 100644 --- a/infer/src/IR/Exp.rei +++ b/infer/src/IR/Exp.rei @@ -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); diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 335f442cf..ccbcf6c05 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -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 => diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 880f861ce..964c5cb51 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -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; diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index 0496832b5..dab2ec5e5 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -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 diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 3808a9f4e..e8a10d0ac 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -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 = diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 73c5a7fdb..135550442 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -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 (_, _, _) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index ff861828e..ec74f919b 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -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 diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 736665686..e978f1e6e 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -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)] diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index e380530de..a56bf8056 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -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 diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index f8d9df7e8..be087e1a1 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -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 diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index d46222401..60871ae99 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -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 (); diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index d8abd7e53..788aef6ab 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -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 = diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 4e4e6ea70..d4ccca21b 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -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 *) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 8af5b2231..1a8a9b357 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -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 diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 7ed432d86..1024f7a1f 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -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 diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml index 5c3a45ab6..0b57d0e94 100644 --- a/infer/src/checkers/codeQuery.ml +++ b/infer/src/checkers/codeQuery.ml @@ -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 diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 43345d9ec..0af3e9883 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -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 diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index b9a56b962..5e4aab2eb 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -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, _) = diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index e75251729..31348515d 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -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 diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 01a3cf65f..7e8f41165 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -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 diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index f30276833..e22fa17c7 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -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] } diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index aa958a13f..56ac3315e 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -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 diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index d8aa690a5..54583670a 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -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 diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 615c0f8f7..f6cbbd80d 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -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 diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index eee810931..7f5c39a16 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -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 diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 8ca7bb6d0..448de6b6d 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -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 diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 5f39be30d..f64a28056 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -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", [