Extending subtyping to C++

Reviewed By: jvillard

Differential Revision: D2865009

fb-gh-sync-id: 998d82d

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

infer/src/backend/prover.ml

@@ -1446,6 +1446,9 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
     | _ -> changed, calc_index_frame, hpred in
   expand false calc_index_frame hpred
 
+module Subtyping_check =
+struct
+
   let object_type = Typename.Java.from_string "java.lang.Object"
 
   let serializable_type = Typename.Java.from_string "java.io.Serializable"
@@ -1454,15 +1457,23 @@ let cloneable_type = Typename.Java.from_string "java.lang.Cloneable"
 
   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 )) ->
+    | 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
 
+  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 || Typename.equal c2 object_type ||
+      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
@@ -1476,61 +1487,91 @@ let check_subclass tenv 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
+    | 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 =
+  (** 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 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.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 tenv dom_type1 dom_type2
+        check_subtype_java tenv dom_type1 dom_type2
 
     | Sil.Tptr (dom_type1, _), Sil.Tptr (dom_type2, _) ->
-      check_subtype tenv dom_type1 dom_type2
+        check_subtype_java tenv dom_type1 dom_type2
 
-  | Sil.Tarray _, Sil.Tstruct { Sil.csu = Csu.Class ck2; struct_name = Some c2 } ->
-      let cn2 = Typename.TN_csu (Csu.Class ck2, c2) in
+    | 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_subtype_basic_type t1 t2)
-
-let rec case_analysis_type tenv (t1, st1) (t2, st2) =
+  (** 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 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.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 tenv (dom_type1, st1) (dom_type2, st2))
+        case_analysis_type_java 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))
+        case_analysis_type_java 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
+    | 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)
+           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 *)
+    | _ -> 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) ->
@@ -1539,7 +1580,7 @@ let subtype_case_analysis tenv texp1 texp2 =
           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
+                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
@@ -1548,11 +1589,14 @@ let subtype_case_analysis tenv texp1 texp2 =
         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) ->

infer/src/backend/prover.mli

@@ -92,9 +92,11 @@ 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} *)
 
+module Subtyping_check :
+sig
+
   (** 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
 
@@ -102,8 +104,9 @@ val check_subtype : Sil.tenv -> Sil.typ -> Sil.typ -> bool
       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
 
-val get_overrides_of : Sil.tenv -> Sil.typ -> Procname.t -> (typ * Procname.t) list
+end
 
+val get_overrides_of : Sil.tenv -> Sil.typ -> Procname.t -> (typ * Procname.t) list
 
 
 

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' ->

infer/src/backend/tabulation.ml

@@ -494,8 +494,6 @@ 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
@@ -516,8 +514,6 @@ let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) lis
     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
 
 (** [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 =

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

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)

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
 
 

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;
+    }
+};

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<String> 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
+        )
+    );
+  }
+}