From afd29e71de57a874c773a842bdce46888787dc58 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 23 Nov 2016 17:18:26 -0800 Subject: [PATCH] [infer][backend] Simplify the code doing the case analysis for execturing the cast instruction Summary: Pure refactoring simplifying the code doing the case analysis for execturing the cast instruction. Reviewed By: dulmarod Differential Revision: D4215238 fbshipit-source-id: 9f0f163 --- infer/src/IR/Subtype.re | 98 +++++++++++++++++++----------- infer/src/IR/Subtype.rei | 22 +++---- infer/src/IR/Typename.re | 4 +- infer/src/IR/Typename.rei | 4 +- infer/src/backend/BuiltinDefn.ml | 39 ++++++------ infer/src/backend/prover.ml | 59 ++++-------------- infer/src/backend/tabulation.ml | 5 +- infer/src/backend/tabulation.mli | 4 +- infer/src/checkers/patternMatch.ml | 2 +- 9 files changed, 110 insertions(+), 127 deletions(-) diff --git a/infer/src/IR/Subtype.re b/infer/src/IR/Subtype.re index f63ff8f30..5bbcae5ae 100644 --- a/infer/src/IR/Subtype.re +++ b/infer/src/IR/Subtype.re @@ -61,10 +61,38 @@ type subtMap = SubtypesMap.t bool; let subtMap: ref subtMap = ref SubtypesMap.empty; -let check_subtype f c1 c2 => +let is_interface tenv (class_name: Typename.t) => + switch (class_name, Tenv.lookup tenv class_name) { + | (TN_csu (Class Java) _, Some {fields: [], methods: []}) => true + | _ => false + }; + +let is_root_class class_name => + switch class_name { + | Typename.TN_csu (Csu.Class Csu.Java) _ => + Typename.equal class_name Typename.Java.java_lang_object + | Typename.TN_csu (Csu.Class Csu.CPP) _ => false + | _ => false + }; + + +/** check if c1 is a subclass of c2 */ +let check_subclass_tenv tenv c1 c2 => { + let rec check (cn: Typename.t) => + Typename.equal cn c2 || + is_root_class c2 || ( + switch (cn, Tenv.lookup tenv cn) { + | (TN_csu (Class _) _, Some {supers}) => IList.exists check supers + | _ => false + } + ); + check c1 +}; + +let check_subtype tenv c1 c2 => try (SubtypesMap.find (c1, c2) !subtMap) { | Not_found => - let is_subt = f c1 c2; + let is_subt = check_subclass_tenv tenv c1 c2; subtMap := SubtypesMap.add (c1, c2) is_subt !subtMap; is_subt }; @@ -190,26 +218,26 @@ let subtypes_to_string t => }; /* c is a subtype when it does not appear in the list l of no-subtypes */ -let is_subtype f c l => +let is_subtype tenv c l => try { - ignore (IList.find (f c) l); + ignore (IList.find (check_subtype tenv c) l); false } { | Not_found => true }; -let is_strict_subtype f c1 c2 => f c1 c2 && not (Typename.equal c1 c2); +let is_strict_subtype tenv c1 c2 => check_subtype tenv c1 c2 && not (Typename.equal c1 c2); /* checks for redundancies when adding c to l Xi in A - { X1,..., Xn } is redundant in two cases: 1) not (Xi <: A) because removing the subtypes of Xi has no effect unless Xi is a subtype of A 2) Xi <: Xj because the subtypes of Xi are a subset of the subtypes of Xj */ -let check_redundancies f c l => { +let check_redundancies tenv c l => { let aux (l, add) ci => { let (l, should_add) = - if (f ci c) { + if (check_subtype tenv ci c) { (l, true) - } else if (f c ci) { + } else if (check_subtype tenv c ci) { ([ci, ...l], false) } else { ([ci, ...l], true) @@ -232,16 +260,16 @@ let rec updates_head f c l => /* adds the classes of l2 to l1 and checks that no redundancies or inconsistencies will occur A - { X1,..., Xn } is inconsistent if A <: Xi for some i */ -let rec add_not_subtype f c1 l1 l2 => +let rec add_not_subtype tenv c1 l1 l2 => switch l2 { | [] => l1 | [c, ...rest] => - if (f c1 c) { - add_not_subtype f c1 l1 rest + if (check_subtype tenv c1 c) { + add_not_subtype tenv c1 l1 rest } else { /* checks for inconsistencies */ - let (l1', should_add) = check_redundancies f c l1; /* checks for redundancies */ - let rest' = add_not_subtype f c1 l1' rest; + let (l1', should_add) = check_redundancies tenv c l1; /* checks for redundancies */ + let rest' = add_not_subtype tenv c1 l1' rest; if should_add { [c, ...rest'] } else { @@ -250,8 +278,8 @@ let rec add_not_subtype f c1 l1 l2 => } }; -let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => { - let is_sub = f c1 c2; +let get_subtypes tenv (c1, (st1, flag1): t) (c2, (st2, flag2): t) => { + let is_sub = check_subtype tenv c1 c2; let (pos_st, neg_st) = switch (st1, st2) { | (Exact, Exact) => @@ -261,7 +289,7 @@ let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => { (None, Some st1) } | (Exact, Subtypes l2) => - if (is_sub && is_subtype f c1 l2) { + if (is_sub && is_subtype tenv c1 l2) { (Some st1, None) } else { (None, Some st1) @@ -270,28 +298,28 @@ let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => { if is_sub { (Some st1, None) } else { - let l1' = updates_head f c2 l1; - if (is_subtype f c2 l1) { - (Some (Subtypes l1'), Some (Subtypes (add_not_subtype f c1 l1 [c2]))) + let l1' = updates_head tenv c2 l1; + if (is_subtype tenv c2 l1) { + (Some (Subtypes l1'), Some (Subtypes (add_not_subtype tenv c1 l1 [c2]))) } else { (None, Some st1) } } | (Subtypes l1, Subtypes l2) => - if (is_interface c2 || is_sub) { - if (is_subtype f c1 l2) { - let l2' = updates_head f c1 l2; - (Some (Subtypes (add_not_subtype f c1 l1 l2')), None) + if (is_interface tenv c2 || is_sub) { + if (is_subtype tenv c1 l2) { + let l2' = updates_head tenv c1 l2; + (Some (Subtypes (add_not_subtype tenv c1 l1 l2')), None) } else { (None, Some st1) } } else if ( - (is_interface c1 || f c2 c1) && is_subtype f c2 l1 + (is_interface tenv c1 || check_subtype tenv c2 c1) && is_subtype tenv c2 l1 ) { - let l1' = updates_head f c2 l1; + let l1' = updates_head tenv c2 l1; ( - Some (Subtypes (add_not_subtype f c2 l1' l2)), - Some (Subtypes (add_not_subtype f c1 l1 [c2])) + Some (Subtypes (add_not_subtype tenv c2 l1' l2)), + Some (Subtypes (add_not_subtype tenv c1 l1 [c2])) ) } else { (None, Some st1) @@ -300,11 +328,11 @@ let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => { (normalize_subtypes pos_st c1 c2 flag1 flag2, normalize_subtypes neg_st c1 c2 flag1 flag2) }; -let case_analysis_basic (c1, st) (c2, (_, flag2)) f => { +let case_analysis_basic tenv (c1, st) (c2, (_, flag2)) => { let (pos_st, neg_st) = - if (f c1 c2) { + if (check_subtype tenv c1 c2) { (Some st, None) - } else if (f c2 c1) { + } else if (check_subtype tenv c2 c1) { switch st { | (Exact, _) => if (Typename.equal c1 c2) { @@ -333,11 +361,9 @@ let case_analysis_basic (c1, st) (c2, (_, flag2)) f => { - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1] - whether [st1] and [st2] admit [not(c1 <: c2)], and in case return the updated subtype [st1] */ -let case_analysis (c1, st1) (c2, st2) f is_interface => { - let f = check_subtype f; +let case_analysis tenv (c1, st1) (c2, st2) => if Config.subtype_multirange { - get_subtypes (c1, st1) (c2, st2) f is_interface + get_subtypes tenv (c1, st1) (c2, st2) } else { - case_analysis_basic (c1, st1) (c2, st2) f - } -}; + case_analysis_basic tenv (c1, st1) (c2, st2) + }; diff --git a/infer/src/IR/Subtype.rei b/infer/src/IR/Subtype.rei index 1c1c8adf3..622b958df 100644 --- a/infer/src/IR/Subtype.rei +++ b/infer/src/IR/Subtype.rei @@ -35,20 +35,14 @@ let subtypes_instof: t; let join: t => t => t; -/** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] according - to [st1] and [st2] where f c1 c2 is true if c1 is a subtype of c2. - get_subtypes returning a pair: - - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1] - - whether [st1] and [st2] admit [not(c1 <: c2)], and in case return - the updated subtype [st1] */ -let case_analysis: - (Typename.t, t) => - (Typename.t, t) => - (Typename.t => Typename.t => bool) => - (Typename.t => bool) => - (option t, option t); - -let check_subtype: (Typename.t => Typename.t => bool) => Typename.t => Typename.t => bool; +/** [case_analysis tenv (c1, st1) (c2,st2)] performs case analysis on [c1 <: c2] according + to [st1] and [st2]. + [case_analysis] returns a pair: + - whether [st1] and [st2] admit [c1 <: c2], and in case returns the updated subtype [st1] + - whether [st1] and [st2] admit [not(c1 <: c2)], and in case returns the updated subtype [st1] */ +let case_analysis: Tenv.t => (Typename.t, t) => (Typename.t, t) => (option t, option t); + +let check_subtype: Tenv.t => Typename.t => Typename.t => bool; let subtypes_to_string: t => string; diff --git a/infer/src/IR/Typename.re b/infer/src/IR/Typename.re index cf47386ff..f24d79044 100644 --- a/infer/src/IR/Typename.re +++ b/infer/src/IR/Typename.re @@ -45,7 +45,9 @@ let module Java = { fun | TN_csu (Class Java) _ => true | _ => false; - let java_lang_Object = from_string "java.lang.Object"; + let java_lang_object = from_string "java.lang.Object"; + let java_io_serializable = from_string "java.io.Serializable"; + let java_lang_cloneable = from_string "java.lang.Cloneable"; }; type typename_t = t; diff --git a/infer/src/IR/Typename.rei b/infer/src/IR/Typename.rei index 42c367ded..dbf571a29 100644 --- a/infer/src/IR/Typename.rei +++ b/infer/src/IR/Typename.rei @@ -38,7 +38,9 @@ let module Java: { /** [is_class name] holds if [name] names a Java class */ let is_class: t => bool; - let java_lang_Object: t; + let java_lang_object: t; + let java_io_serializable: t; + let java_lang_cloneable: t; }; let module Set: Set.S with type elt = t; diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index 6d013fac5..507dbaad6 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -244,9 +244,10 @@ let execute___instanceof_cast ~instof (* and throw an exception in case of a cast to a reference. *) let should_throw_exception = !Config.curr_language = Config.Java || is_cast_to_reference in - let deal_with_failed_cast val1 _ texp1 texp2 = - Tabulation.raise_cast_exception tenv - __POS__ None texp1 texp2 val1 in + let deal_with_failed_cast val1 texp1 texp2 = + raise + (Tabulation.create_cast_exception + tenv __POS__ None texp1 texp2 val1) in let exe_one_prop prop = if Exp.equal texp2 Exp.zero then [(return_result tenv Exp.zero prop ret_id, path)] @@ -268,11 +269,9 @@ let execute___instanceof_cast ~instof else replace_ptsto_texp tenv prop val1 texp1' in [(return_result tenv res_e prop' ret_id, path)] in if instof then (* instanceof *) - begin - 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 + 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 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 @@ -280,20 +279,16 @@ let execute___instanceof_cast ~instof pos_res @ neg_res else begin - if (!Config.footprint = true) then - begin - match pos_type_opt with - | None -> deal_with_failed_cast val1 typ1 texp1 texp2 - | Some _ -> mk_res pos_type_opt val1 - end - else (* !Config.footprint = false *) - begin - match neg_type_opt with - | Some _ -> - if is_undefined_opt tenv prop val1 then mk_res pos_type_opt val1 - else deal_with_failed_cast val1 typ1 texp1 texp2 - | None -> mk_res pos_type_opt val1 - end + if !Config.footprint then + match pos_type_opt with + | None -> deal_with_failed_cast val1 texp1 texp2 + | Some _ -> mk_res pos_type_opt val1 + else (* !Config.footprint is false *) + match neg_type_opt with + | Some _ -> + if is_undefined_opt tenv prop val1 then mk_res pos_type_opt val1 + else deal_with_failed_cast val1 texp1 texp2 + | None -> mk_res pos_type_opt val1 end | _ -> [] with Not_found -> diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index cb0dd4ddf..76f9c3b26 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1525,39 +1525,6 @@ let expand_hpred_pointer = module Subtyping_check = struct - let object_type = Typename.Java.java_lang_Object - - let serializable_type = Typename.Java.from_string "java.io.Serializable" - - let cloneable_type = Typename.Java.from_string "java.lang.Cloneable" - - let is_interface tenv (class_name: Typename.t) = - match class_name, Tenv.lookup tenv class_name with - | TN_csu (Class Java, _), Some { fields = []; methods = []; } -> true - | _ -> false - - let is_root_class class_name = - match class_name with - | Typename.TN_csu (Csu.Class Csu.Java, _) -> - Typename.equal class_name object_type - | Typename.TN_csu (Csu.Class Csu.CPP, _) -> - false - | _ -> false - - (** check if c1 is a subclass of c2 *) - let check_subclass_tenv tenv c1 c2 = - let rec check (cn: Typename.t) = - Typename.equal cn c2 || is_root_class c2 || - match cn, Tenv.lookup tenv cn with - | TN_csu (Class _, _), Some { supers } -> - IList.exists check supers - | _ -> false in - check c1 - - let check_subclass tenv c1 c2 = - let f = check_subclass_tenv tenv in - Subtype.check_subtype f c1 c2 - (** check that t1 and t2 are the same primitive type *) let check_subtype_basic_type t1 t2 = match t2 with @@ -1571,15 +1538,15 @@ struct let rec check_subtype_java tenv (t1: Typ.t) (t2: Typ.t) = match t1, t2 with | Tstruct (TN_csu (Class Java, _) as cn1), Tstruct (TN_csu (Class Java, _) as cn2) -> - check_subclass tenv cn1 cn2 + Subtype.check_subtype tenv cn1 cn2 | Tarray (dom_type1, _), Tarray (dom_type2, _) -> check_subtype_java tenv dom_type1 dom_type2 | Tptr (dom_type1, _), Tptr (dom_type2, _) -> check_subtype_java tenv dom_type1 dom_type2 | Tarray _, Tstruct (TN_csu (Class Java, _) as cn2) -> - Typename.equal cn2 serializable_type - || Typename.equal cn2 cloneable_type - || Typename.equal cn2 object_type + Typename.equal cn2 Typename.Java.java_io_serializable + || Typename.equal cn2 Typename.Java.java_lang_cloneable + || Typename.equal cn2 Typename.Java.java_lang_object | _ -> check_subtype_basic_type t1 t2 (** check if t1 is a subtype of t2 *) @@ -1589,18 +1556,17 @@ struct check_subtype_java tenv t1 t2 else match Typ.name t1, Typ.name t2 with - | Some cn1, Some cn2 -> check_subclass tenv cn1 cn2 + | Some cn1, Some cn2 -> Subtype.check_subtype tenv cn1 cn2 | _ -> false let rec case_analysis_type tenv ((t1: Typ.t), st1) ((t2: Typ.t), st2) = match t1, t2 with | Tstruct (TN_csu (Class Java, _) as cn1), Tstruct (TN_csu (Class Java, _) as cn2) -> - Subtype.case_analysis - (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv) + Subtype.case_analysis tenv (cn1, st1) (cn2, st2) | Tstruct (TN_csu (Class Java, _) as cn1), Tarray _ - when (Typename.equal cn1 serializable_type - || Typename.equal cn1 cloneable_type - || Typename.equal cn1 object_type) && + when (Typename.equal cn1 Typename.Java.java_io_serializable + || Typename.equal cn1 Typename.Java.java_lang_cloneable + || Typename.equal cn1 Typename.Java.java_lang_object) && st1 <> Subtype.exact -> Some st1, None | Tstruct cn1, Tstruct cn2 @@ -1608,9 +1574,8 @@ struct (* that get through the type system, but not in C++ because of multiple inheritance, *) (* and not in ObjC because of being weakly typed, *) (* and the algorithm will only work correctly if this is the case *) - when check_subclass tenv cn1 cn2 || check_subclass tenv cn2 cn1 -> - Subtype.case_analysis - (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv) + when Subtype.check_subtype tenv cn1 cn2 || Subtype.check_subtype tenv cn2 cn1 -> + Subtype.case_analysis tenv (cn1, st1) (cn2, st2) | Tarray (dom_type1, _), Tarray (dom_type2, _) -> case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) | Tptr (dom_type1, _), Tptr (dom_type2, _) -> @@ -1709,7 +1674,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing = | Some texp1' -> not (texp_equal_modulo_subtype_flag texp1' texp1) | None -> false in - if (calc_missing) then (* footprint *) + if calc_missing then (* footprint *) begin match pos_type_opt with | None -> cast_exception tenv texp1 texp2 e1 subs diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 32dd8a0ff..857c20366 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -986,9 +986,8 @@ let class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc = pname_opt texp1 texp2 exp (State.get_node ()) (State.get_loc ()) in Exceptions.Class_cast_exception (desc, ml_loc) -let raise_cast_exception tenv ml_loc pname_opt texp1 texp2 exp = - let exn = class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc in - raise exn +let create_cast_exception tenv ml_loc pname_opt texp1 texp2 exp = + class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc let get_check_exn tenv check callee_pname loc ml_loc = match check with | Prover.Bounds_check -> diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 22e456e34..416d31c86 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -27,8 +27,8 @@ val check_attr_dealloc_mismatch : PredSymb.t -> PredSymb.t -> unit val find_dereference_without_null_check_in_sexp : Sil.strexp -> (int * PredSymb.path_pos) option (** raise a cast exception *) -val raise_cast_exception : - Tenv.t -> Logging.ml_loc -> Procname.t option -> Exp.t -> Exp.t -> Exp.t -> 'a +val create_cast_exception : + Tenv.t -> Logging.ml_loc -> Procname.t option -> Exp.t -> Exp.t -> Exp.t -> exn (** check if a prop is an exception *) val prop_is_exn : Procname.t -> 'a Prop.t -> bool diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index 8a17885c7..76def35e0 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -26,7 +26,7 @@ type taint_spec = { let type_is_object typ = match typ with - | Typ.Tptr (Tstruct name, _) -> Typename.equal name Typename.Java.java_lang_Object + | Typ.Tptr (Tstruct name, _) -> Typename.equal name Typename.Java.java_lang_object | _ -> false let java_proc_name_with_class_method pn_java class_with_path method_name =