From 10fe998c122cb1e9646f2fbbcb20593a04bdf08c Mon Sep 17 00:00:00 2001 From: Dulma Rodriguez Date: Mon, 1 Feb 2016 10:19:48 -0800 Subject: [PATCH] Extending subtyping to C++ Reviewed By: jvillard Differential Revision: D2865009 fb-gh-sync-id: 998d82d --- infer/src/backend/config.ml | 3 - infer/src/backend/prover.ml | 263 +++++++++++------- infer/src/backend/prover.mli | 17 +- infer/src/backend/symExec.ml | 9 +- infer/src/backend/tabulation.ml | 44 ++- infer/src/backend/type_prop.ml | 4 +- infer/src/java/jContext.ml | 3 +- infer/src/java/jTransType.ml | 2 +- .../cpp/errors/subtyping/subtyping_check.cpp | 26 ++ .../endtoend/cpp/SubtypingCheckTest.java | 63 +++++ 10 files changed, 282 insertions(+), 152 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/errors/subtyping/subtyping_check.cpp create mode 100644 infer/tests/endtoend/cpp/SubtypingCheckTest.java diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 40c6971e4..1c1dc855c 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -367,9 +367,6 @@ let analyze_models = from_env_variable "INFER_ANALYZE_MODELS" module Experiment = struct - (** if true, activate the subtyping routines in C++ as well, not just in Java *) - let activate_subtyping_in_cpp = ref false - (** if true, a precondition with e.g. index 3 in an array does not require the caller to have index 3 too this mimics what happens with direct access to the array without a procedure call, where the index is simply materialized if not there *) let allow_missing_index_in_proc_call = ref true diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 906a5578c..872796492 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1446,113 +1446,157 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred = | _ -> changed, calc_index_frame, hpred in expand false calc_index_frame hpred -let object_type = Typename.Java.from_string "java.lang.Object" +module Subtyping_check = +struct -let serializable_type = Typename.Java.from_string "java.io.Serializable" + let object_type = Typename.Java.from_string "java.lang.Object" -let cloneable_type = Typename.Java.from_string "java.lang.Cloneable" + let serializable_type = Typename.Java.from_string "java.io.Serializable" -let is_interface tenv class_name = - match Sil.tenv_lookup tenv class_name with - | Some (Sil.Tstruct ( { Sil.csu = Csu.Class _; struct_name = Some _ } as struct_typ )) -> - (IList.length struct_typ.Sil.instance_fields = 0) && - (IList.length struct_typ.Sil.def_methods = 0) - | _ -> false - -(** check if c1 is a subclass of c2 *) -let check_subclass_tenv tenv c1 c2 = - let rec check cn = - Typename.equal cn c2 || Typename.equal c2 object_type || - match Sil.tenv_lookup tenv cn with - | Some (Sil.Tstruct { Sil.struct_name = Some _; csu = Csu.Class _; superclasses }) -> - IList.exists check superclasses - | _ -> false in - check c1 - -let check_subclass tenv c1 c2 = - let f = check_subclass_tenv tenv in - Sil.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 - | (Sil.Tint Sil.IInt) | (Sil.Tint Sil.IBool) - | (Sil.Tint Sil.IChar) | (Sil.Tfloat Sil.FDouble) - | (Sil.Tfloat Sil.FFloat) | (Sil.Tint Sil.ILong) - | (Sil.Tint Sil.IShort) -> Sil.typ_equal t1 t2 - | _ -> false - -(** check if t1 is a subtype of t2 *) -let rec check_subtype tenv t1 t2 = - match t1, t2 with - | Sil.Tstruct { Sil.csu = Csu.Class ck1; struct_name = Some c1 }, - Sil.Tstruct { Sil.csu = Csu.Class ck2; struct_name = Some c2 } -> - let cn1 = Typename.TN_csu (Csu.Class ck1, c1) - and cn2 = Typename.TN_csu (Csu.Class ck2, c2) in - (check_subclass tenv cn1 cn2) - - | Sil.Tarray (dom_type1, _), Sil.Tarray (dom_type2, _) -> - check_subtype tenv dom_type1 dom_type2 - - | Sil.Tptr (dom_type1, _), Sil.Tptr (dom_type2, _) -> - check_subtype tenv dom_type1 dom_type2 + let cloneable_type = Typename.Java.from_string "java.lang.Cloneable" - | Sil.Tarray _, Sil.Tstruct { Sil.csu = Csu.Class ck2; struct_name = Some c2 } -> - let cn2 = Typename.TN_csu (Csu.Class ck2, c2) in - Typename.equal cn2 serializable_type - || Typename.equal cn2 cloneable_type - || Typename.equal cn2 object_type + let is_interface tenv class_name = + match Sil.tenv_lookup tenv class_name with + | Some (Sil.Tstruct ( { Sil.csu = Csu.Class Csu.Java; struct_name = Some _ } as struct_typ )) -> + (IList.length struct_typ.Sil.instance_fields = 0) && + (IList.length struct_typ.Sil.def_methods = 0) + | _ -> false - | _ -> (check_subtype_basic_type t1 t2) + 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 (* TODO add ObjC case *) + + (** check if c1 is a subclass of c2 *) + let check_subclass_tenv tenv c1 c2 = + let rec check cn = + Typename.equal cn c2 || is_root_class c2 || + match Sil.tenv_lookup tenv cn with + | Some (Sil.Tstruct { Sil.struct_name = Some _; csu = Csu.Class _; superclasses }) -> + IList.exists check superclasses + | _ -> false in + check c1 + + let check_subclass tenv c1 c2 = + let f = check_subclass_tenv tenv in + Sil.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 + | Sil.Tint Sil.IInt | Sil.Tint Sil.IBool + | Sil.Tint Sil.IChar | Sil.Tfloat Sil.FDouble + | Sil.Tfloat Sil.FFloat | Sil.Tint Sil.ILong + | Sil.Tint Sil.IShort -> Sil.typ_equal t1 t2 + | _ -> false -let rec case_analysis_type tenv (t1, st1) (t2, st2) = - match t1, t2 with - | Sil.Tstruct { Sil.csu = Csu.Class ck1; struct_name = Some c1 }, - Sil.Tstruct { Sil.csu = Csu.Class ck2; struct_name = Some c2 } -> - let cn1 = Typename.TN_csu (Csu.Class ck1, c1) - and cn2 = Typename.TN_csu (Csu.Class ck2, c2) in - (Sil.Subtype.case_analysis (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv)) - - | Sil.Tarray (dom_type1, _), Sil.Tarray (dom_type2, _) -> - (case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)) - - | Sil.Tptr (dom_type1, _), Sil.Tptr (dom_type2, _) -> - (case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)) - - | Sil.Tstruct { Sil.csu = Csu.Class ck1; struct_name = Some c1 }, Sil.Tarray _ -> - let cn1 = Typename.TN_csu (Csu.Class ck1, c1) in - if (Typename.equal cn1 serializable_type - || Typename.equal cn1 cloneable_type - || Typename.equal cn1 object_type) && - (st1 <> Sil.Subtype.exact) then (Some st1, None) - else (None, Some st1) - - | _ -> if (check_subtype_basic_type t1 t2) then (Some st1, None) - else (None, Some st1) - -(** perform case analysis on [texp1 <: texp2], and return the updated types in the true and false case, if they are possible *) -let subtype_case_analysis tenv texp1 texp2 = - match texp1, texp2 with - | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> - begin - let pos_opt, neg_opt = case_analysis_type tenv (t1, st1) (t2, st2) in - let pos_type_opt = match pos_opt with - | None -> None - | Some st1' -> - let t1' = if (check_subtype tenv t1 t2) then t1 else t2 in - Some (Sil.Sizeof (t1', st1')) in - let neg_type_opt = match neg_opt with - | None -> None - | Some st1' -> Some (Sil.Sizeof (t1, st1')) in - pos_type_opt, neg_type_opt - end - | _ -> (* don't know, consider both possibilities *) - Some texp1, Some texp1 + (** check if t1 is a subtype of t2, in Java *) + let rec check_subtype_java tenv t1 t2 = + match t1, t2 with + | Sil.Tstruct { Sil.csu = Csu.Class Csu.Java; struct_name = Some c1 }, + Sil.Tstruct { Sil.csu = Csu.Class Csu.Java; struct_name = Some c2 } -> + let cn1 = Typename.TN_csu (Csu.Class Csu.Java, c1) + and cn2 = Typename.TN_csu (Csu.Class Csu.Java, c2) in + check_subclass tenv cn1 cn2 + + | Sil.Tarray (dom_type1, _), Sil.Tarray (dom_type2, _) -> + check_subtype_java tenv dom_type1 dom_type2 + + | Sil.Tptr (dom_type1, _), Sil.Tptr (dom_type2, _) -> + check_subtype_java tenv dom_type1 dom_type2 + + | Sil.Tarray _, Sil.Tstruct { Sil.csu = Csu.Class Csu.Java; struct_name = Some c2 } -> + let cn2 = Typename.TN_csu (Csu.Class Csu.Java, c2) in + Typename.equal cn2 serializable_type + || Typename.equal cn2 cloneable_type + || Typename.equal cn2 object_type + | _ -> check_subtype_basic_type t1 t2 + + (** check if t1 is a subtype of t2 *) + let check_subtype tenv t1 t2 = + if !Config.curr_language = Config.Java then + check_subtype_java tenv t1 t2 + else match t1, t2 with + | Sil.Tstruct { Sil.csu = Csu.Class Csu.CPP; struct_name = Some c1 }, + Sil.Tstruct { Sil.csu = Csu.Class Csu.CPP; struct_name = Some c2 } -> + let cn1 = Typename.TN_csu (Csu.Class Csu.CPP, c1) + and cn2 = Typename.TN_csu (Csu.Class Csu.CPP, c2) in + check_subclass tenv cn1 cn2 + | _ -> false (* TODO ObjC case *) + + let rec case_analysis_type_java tenv (t1, st1) (t2, st2) = + match t1, t2 with + | Sil.Tstruct { Sil.csu = Csu.Class Csu.Java; struct_name = Some c1 }, + Sil.Tstruct { Sil.csu = Csu.Class Csu.Java; struct_name = Some c2 } -> + let cn1 = Typename.TN_csu (Csu.Class Csu.Java, c1) + and cn2 = Typename.TN_csu (Csu.Class Csu.Java, c2) in + Sil.Subtype.case_analysis (cn1, st1) (cn2, st2) + (check_subclass tenv) (is_interface tenv) + + | Sil.Tarray (dom_type1, _), Sil.Tarray (dom_type2, _) -> + case_analysis_type_java tenv (dom_type1, st1) (dom_type2, st2) + + | Sil.Tptr (dom_type1, _), Sil.Tptr (dom_type2, _) -> + case_analysis_type_java tenv (dom_type1, st1) (dom_type2, st2) + + | Sil.Tstruct { Sil.csu = Csu.Class Csu.Java; struct_name = Some c1 }, Sil.Tarray _ -> + let cn1 = Typename.TN_csu (Csu.Class Csu.Java, c1) in + if (Typename.equal cn1 serializable_type + || Typename.equal cn1 cloneable_type + || Typename.equal cn1 object_type) && + st1 <> Sil.Subtype.exact then Some st1, None + else (None, Some st1) + + | _ -> if check_subtype_basic_type t1 t2 then Some st1, None + else None, Some st1 + + let case_analysis_type tenv (t1, st1) (t2, st2) = + if !Config.curr_language = Config.Java then + case_analysis_type_java tenv (t1, st1) (t2, st2) + else match t1, t2 with + | Sil.Tstruct { Sil.csu = Csu.Class Csu.CPP; struct_name = Some c1 }, + Sil.Tstruct { Sil.csu = Csu.Class Csu.CPP; struct_name = Some c2 } -> + let cn1 = Typename.TN_csu (Csu.Class Csu.CPP, c1) + and cn2 = Typename.TN_csu (Csu.Class Csu.CPP, c2) in + (* cn1 <: cn2 or cn2 <: cn1 is implied in Java when we get two types compared *) + (* that get through the type system, but not in C++ because of multiple inheritance, *) + (* and the algorithm will only work correctly if this is the case *) + if check_subclass tenv cn1 cn2 || check_subclass tenv cn2 cn1 then + Sil.Subtype.case_analysis (cn1, st1) (cn2, st2) (check_subclass tenv) + (is_interface tenv) + else None, Some st1 + | _ -> None, Some st1 (* TODO ObjC case *) + + (** perform case analysis on [texp1 <: texp2], and return the updated types in the true and false + case, if they are possible *) + let subtype_case_analysis tenv texp1 texp2 = + match texp1, texp2 with + | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> + begin + let pos_opt, neg_opt = case_analysis_type tenv (t1, st1) (t2, st2) in + let pos_type_opt = match pos_opt with + | None -> None + | Some st1' -> + let t1' = if check_subtype tenv t1 t2 then t1 else t2 in + Some (Sil.Sizeof (t1', st1')) in + let neg_type_opt = match neg_opt with + | None -> None + | Some st1' -> Some (Sil.Sizeof (t1, st1')) in + pos_type_opt, neg_type_opt + end + | _ -> (* don't know, consider both possibilities *) + Some texp1, Some texp1 +end let cast_exception tenv texp1 texp2 e1 subs = let _ = match texp1, texp2 with | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> - if (!Config.developer_mode) || ((Sil.Subtype.is_cast st2) && not (check_subtype tenv t1 t2)) then + if !Config.developer_mode || + (Sil.Subtype.is_cast st2 && + not (Subtyping_check.check_subtype tenv t1 t2)) then ProverState.checks := Class_cast_check (texp1, texp2, e1) :: !ProverState.checks | _ -> () in raise (IMPL_EXC ("class cast exception", subs, EXC_FALSE)) @@ -1567,7 +1611,7 @@ let get_overrides_of tenv supertype pname = | _ -> false in let gather_overrides tname typ overrides_acc = (* get all types in the type environment that are non-reflexive subtypes of [supertype] *) - if not (Sil.typ_equal typ supertype) && check_subtype tenv typ supertype then + if not (Sil.typ_equal typ supertype) && Subtyping_check.check_subtype tenv typ supertype then (* only select the ones that implement [pname] as overrides *) let resolved_pname = Procname.java_replace_class pname (Typename.name tname) in if typ_has_method resolved_pname typ then (typ, resolved_pname) :: overrides_acc @@ -1588,11 +1632,15 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing = | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tstruct _, _) | Sil.Sizeof (Sil.Tarray _, _), Sil.Sizeof (Sil.Tarray _, _) | Sil.Sizeof (Sil.Tarray _, _), Sil.Sizeof (Sil.Tstruct _, _) - | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tarray _, _) -> true + | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tarray _, _) -> + !Config.curr_language = Config.Java + + | Sil.Sizeof (typ1, _), Sil.Sizeof (typ2, _) -> Sil.is_cpp_class typ1 && Sil.is_cpp_class typ2 + (* TODO ObjC case *) | _ -> false in - if !Config.curr_language = Config.Java && types_subject_to_cast then + if types_subject_to_cast then begin - let pos_type_opt, neg_type_opt = subtype_case_analysis tenv texp1 texp2 in + let pos_type_opt, neg_type_opt = Subtyping_check.subtype_case_analysis tenv texp1 texp2 in let has_changed = match pos_type_opt with | Some texp1' -> not (texp_equal_modulo_subtype_flag texp1' texp1) @@ -1626,7 +1674,7 @@ let sexp_imply_preprocess se1 texp1 se2 = match se1, texp1, se2 with se1' | _ -> se1 -(** handle parameter subtype for java: when the type of a callee variable in the caller is a strict subtype +(** handle parameter subtype: when the type of a callee variable in the caller is a strict subtype of the one in the callee, add a type frame and type missing *) let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2) = let is_callee = match e1 with @@ -1651,9 +1699,11 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 let t1, t2 = Sil.expand_type tenv _t1, Sil.expand_type tenv _t2 in match type_rhs e2' with | Some (t2_ptsto , sub2) -> - if not (Sil.typ_equal t1 t2) && check_subtype tenv t1 t2 + if not (Sil.typ_equal t1 t2) && Subtyping_check.check_subtype tenv t1 t2 then begin - let pos_type_opt, _ = subtype_case_analysis tenv (Sil.Sizeof(t1, Sil.Subtype.subtypes)) (Sil.Sizeof(t2_ptsto, sub2)) in + let pos_type_opt, _ = + Subtyping_check.subtype_case_analysis tenv + (Sil.Sizeof (t1, Sil.Subtype.subtypes)) (Sil.Sizeof (t2_ptsto, sub2)) in match pos_type_opt with | Some t1_noptr -> ProverState.add_frame_typ (e1', t1_noptr); @@ -1663,10 +1713,7 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 | None -> () end | _ -> () in - if is_callee && - !Config.footprint && - (!Config.Experiment.activate_subtyping_in_cpp || !Config.curr_language = Config.Java) - then add_subtype () + if is_callee && !Config.footprint then add_subtype () let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 : subst2 * Prop.normal Prop.t = match hpred2 with | Sil.Hpointsto (_e2, se2, texp2) -> diff --git a/infer/src/backend/prover.mli b/infer/src/backend/prover.mli index d456ccafc..884abd76d 100644 --- a/infer/src/backend/prover.mli +++ b/infer/src/backend/prover.mli @@ -92,18 +92,21 @@ val find_minimum_pure_cover : (Sil.atom list * 'a) list -> (Sil.atom list * 'a) (** Computer an upper bound of an expression *) val compute_upper_bound_of_exp : Prop.normal Prop.t -> Sil.exp -> Sil.Int.t option - (** {2 Subtype checking} *) -(** check_subtype t1 t2 checks whether t1 is a subtype of t2, given the type environment tenv. *) -val check_subtype : Sil.tenv -> Sil.typ -> Sil.typ -> bool +module Subtyping_check : +sig -(** subtype_case_analysis tenv tecp1 texp2 performs case analysis on [texp1 <: texp2], - and returns the updated types in the true and false case, if they are possible *) -val subtype_case_analysis : Sil.tenv -> Sil.exp -> Sil.exp -> Sil.exp option * Sil.exp option + (** check_subtype t1 t2 checks whether t1 is a subtype of t2, given the type environment tenv. *) + val check_subtype : Sil.tenv -> Sil.typ -> Sil.typ -> bool -val get_overrides_of : Sil.tenv -> Sil.typ -> Procname.t -> (typ * Procname.t) list + (** subtype_case_analysis tenv tecp1 texp2 performs case analysis on [texp1 <: texp2], + and returns the updated types in the true and false case, if they are possible *) + val subtype_case_analysis : Sil.tenv -> Sil.exp -> Sil.exp -> Sil.exp option * Sil.exp option +end + +val get_overrides_of : Sil.tenv -> Sil.typ -> Procname.t -> (typ * Procname.t) list diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 5ff065e61..d3cc41132 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1517,11 +1517,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = match actual_pars, formal_types with | [], [] -> actual_pars | (e, t_e):: etl', t:: tl' -> - (e, - if - (!Config.Experiment.activate_subtyping_in_cpp || - !Config.curr_language = Config.Java) - then t_e else t) :: comb etl' tl' + (e, t_e) :: comb etl' tl' | _,[] -> Errdesc.warning_err (State.get_loc ()) @@ -1885,7 +1881,8 @@ module ModelBuiltins = struct | _ -> false) (Prop.get_sigma prop) in match hpred with | Sil.Hpointsto(_, _, texp1) -> - let pos_type_opt, neg_type_opt = Prover.subtype_case_analysis tenv texp1 texp2 in + let pos_type_opt, neg_type_opt = + Prover.Subtyping_check.subtype_case_analysis tenv texp1 texp2 in let mk_res type_opt res_e = match type_opt with | None -> [] | Some texp1' -> diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index caea1ca8d..482510cc9 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -494,30 +494,26 @@ let hpred_star_typing (hpred1 : Sil.hpred) (e2, te2) : Sil.hpred = (** Implementation of [*] between predicates and typings *) let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) list) : Sil.hpred list = - if !Config.Experiment.activate_subtyping_in_cpp || !Config.curr_language = Config.Java then - begin - let typing_lhs_compare (e1, _) (e2, _) = Sil.exp_compare e1 e2 in - let sigma1 = IList.stable_sort hpred_lhs_compare sigma1 in - let typings2 = IList.stable_sort typing_lhs_compare typings2 in - let rec star sg1 typ2 : Sil.hpred list = - match sg1, typ2 with - | [], _ -> [] - | sigma1,[] -> sigma1 - | hpred1:: sigma1', typing2:: typings2' -> - begin - match hpred_typing_lhs_compare hpred1 typing2 with - | 0 -> hpred_star_typing hpred1 typing2 :: star sigma1' typings2' - | n when n < 0 -> hpred1 :: star sigma1' typ2 - | _ -> star sg1 typings2' - end in - try star sigma1 typings2 - with exn when exn_not_failure exn -> - L.d_str "cannot star "; - Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2; - L.d_ln (); - raise (Prop.Cannot_star (try assert false with Assert_failure x -> x)) - end - else sigma1 + let typing_lhs_compare (e1, _) (e2, _) = Sil.exp_compare e1 e2 in + let sigma1 = IList.stable_sort hpred_lhs_compare sigma1 in + let typings2 = IList.stable_sort typing_lhs_compare typings2 in + let rec star sg1 typ2 : Sil.hpred list = + match sg1, typ2 with + | [], _ -> [] + | sigma1,[] -> sigma1 + | hpred1:: sigma1', typing2:: typings2' -> + begin + match hpred_typing_lhs_compare hpred1 typing2 with + | 0 -> hpred_star_typing hpred1 typing2 :: star sigma1' typings2' + | n when n < 0 -> hpred1 :: star sigma1' typ2 + | _ -> star sg1 typings2' + end in + try star sigma1 typings2 + with exn when exn_not_failure exn -> + L.d_str "cannot star "; + Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2; + L.d_ln (); + raise (Prop.Cannot_star (try assert false with Assert_failure x -> x)) (** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld] extends the footprint of [prop] with [pi,sigma] and extends the fields of |-> with [missing_fld] *) let prop_footprint_add_pi_sigma_starfld_sigma (prop : 'a Prop.t) pi_new sigma_new missing_fld missing_typ : Prop.normal Prop.t option = diff --git a/infer/src/backend/type_prop.ml b/infer/src/backend/type_prop.ml index 932f6b1c3..d14e6e26c 100644 --- a/infer/src/backend/type_prop.ml +++ b/infer/src/backend/type_prop.ml @@ -325,8 +325,8 @@ let rec lub tenv t1 t2 = let t1 = Sil.expand_type tenv t1 in let t2 = Sil.expand_type tenv t2 in if (Sil.typ_equal t1 t2) then t1 - else if (Prover.check_subtype tenv t1 t2) then t2 - else if (Prover.check_subtype tenv t2 t1) then t1 + else if (Prover.Subtyping_check.check_subtype tenv t1 t2) then t2 + else if (Prover.Subtyping_check.check_subtype tenv t2 t1) then t1 else let st1 = (super tenv t1) in let st2 = (super tenv t2) in diff --git a/infer/src/java/jContext.ml b/infer/src/java/jContext.ml index 0ae28914b..2a6df071e 100644 --- a/infer/src/java/jContext.ml +++ b/infer/src/java/jContext.ml @@ -76,7 +76,8 @@ let get_or_set_pvar_type context var typ = try let (pvar, otyp, _) = (JBir.VarMap.find var var_map) in let tenv = get_tenv context in - if Prover.check_subtype tenv typ otyp || (Prover.check_subtype tenv otyp typ) then + if Prover.Subtyping_check.check_subtype tenv typ otyp || + Prover.Subtyping_check.check_subtype tenv otyp typ then set_var_map context (JBir.VarMap.add var (pvar, otyp, typ) var_map) else set_var_map context (JBir.VarMap.add var (pvar, typ, typ) var_map); (pvar, typ) diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index fd36b0e9d..4bd793cfc 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -376,7 +376,7 @@ let is_closeable program tenv typ = let closeable_typ = get_class_type program tenv closeable_cn in let autocloseable_cn = JBasics.make_cn "java.lang.AutoCloseable" in let autocloseable_typ = get_class_type program tenv autocloseable_cn in - let implements t = Prover.check_subtype tenv typ t in + let implements t = Prover.Subtyping_check.check_subtype tenv typ t in implements closeable_typ || implements autocloseable_typ diff --git a/infer/tests/codetoanalyze/cpp/errors/subtyping/subtyping_check.cpp b/infer/tests/codetoanalyze/cpp/errors/subtyping/subtyping_check.cpp new file mode 100644 index 000000000..dcc8fb96f --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/errors/subtyping/subtyping_check.cpp @@ -0,0 +1,26 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +struct A { + int f; + void setF() { + f = 1; + } +}; + +struct B : public A { + int g; + void setFG() { + setF(); + g = 1; + if (g == 1) + g = 1/0; + else g = 0; + } +}; diff --git a/infer/tests/endtoend/cpp/SubtypingCheckTest.java b/infer/tests/endtoend/cpp/SubtypingCheckTest.java new file mode 100644 index 000000000..3e39dea31 --- /dev/null +++ b/infer/tests/endtoend/cpp/SubtypingCheckTest.java @@ -0,0 +1,63 @@ +/* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package endtoend.cpp; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +import com.google.common.collect.ImmutableList; + +import org.junit.BeforeClass; +import org.junit.ClassRule; +import org.junit.Test; + +import java.io.IOException; + +import utils.DebuggableTemporaryFolder; +import utils.InferException; +import utils.InferResults; +import utils.InferRunner; + +public class SubtypingCheckTest { + + public static final String FILE = + "infer/tests/codetoanalyze/cpp/errors/subtyping/subtyping_check.cpp"; + + private static ImmutableList inferCmd; + + public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO"; + + @ClassRule + public static DebuggableTemporaryFolder folder = + new DebuggableTemporaryFolder(); + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferCmd = InferRunner.createCPPInferCommand(folder, FILE); + } + + @Test + public void whenInferRunsOnDiv0MethodsErrorIsFound() + throws InterruptedException, IOException, InferException { + InferResults inferResults = InferRunner.runInferCPP(inferCmd); + String[] procedures = { + "B_setFG", + }; + assertThat( + "Results should contain the expected divide by zero", + inferResults, + containsExactly( + DIVIDE_BY_ZERO, + FILE, + procedures + ) + ); + } +}