Translate dynamic cast for C++

Summary: public Translate dynamic cast for C++.

Reviewed By: akotulski

Differential Revision: D2879867

fb-gh-sync-id: 04e3112

infer/src/backend/symExec.ml

@@ -1822,7 +1822,7 @@ module ModelBuiltins = struct
       non_null_case
     else if ((IList.length non_null_case) > 0) && (is_undefined_opt prop n_lexp) then
       non_null_case
-    else null_case@non_null_case
+    else null_case @ non_null_case
 
   let execute___get_type_of cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
     : Builtin.ret_typ =
@@ -1870,6 +1870,18 @@ module ModelBuiltins = struct
         let pname = Cfg.Procdesc.get_proc_name pdesc in
         let val1, __prop = exp_norm_check_arith pname _prop _val1 in
         let texp2, prop = exp_norm_check_arith pname __prop _texp2 in
+        let is_cast_to_reference =
+          match typ1 with
+          | Sil.Tptr (base_typ, Sil.Pk_reference) -> true
+          | _ -> false in
+        (* In Java, we throw an exception, in C++ we return 0 in case of a cast to a pointer, *)
+        (* 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 typ1 texp1 texp2 =
+          Tabulation.raise_cast_exception
+            (try assert false with Assert_failure ml_loc -> ml_loc)
+            None texp1 texp2 val1 in
         let exe_one_prop prop =
           if Sil.exp_equal texp2 Sil.exp_zero then
             [(return_result Sil.exp_zero prop ret_ids, path)]
@@ -1877,10 +1889,10 @@ module ModelBuiltins = struct
             begin
               try
                 let hpred = IList.find (function
-                    | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
+                    | Sil.Hpointsto (e1, _, _) -> Sil.exp_equal e1 val1
                     | _ -> false) (Prop.get_sigma prop) in
                 match hpred with
-                | Sil.Hpointsto(_, _, texp1) ->
+                | Sil.Hpointsto (_, _, texp1) ->
                     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
@@ -1890,33 +1902,32 @@ module ModelBuiltins = struct
                             if Sil.exp_equal texp1 texp1' then prop
                             else replace_ptsto_texp prop val1 texp1' in
                           [(return_result res_e prop' ret_ids, path)] in
-                    if (instof) then (* instanceof *)
+                    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
                         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
+                      pos_res @ neg_res
+                    else
                       begin
                         if (!Config.footprint = true) then
                           begin
                             match pos_type_opt with
-                            | None ->
-                                Tabulation.raise_cast_exception
-                                  (try assert false with Assert_failure ml_loc -> ml_loc)
-                                  None texp1 texp2 val1
-                            | Some texp1' -> (mk_res pos_type_opt val1)
+                            | None -> deal_with_failed_cast val1 typ1 texp1 texp2
+                            | Some texp1' -> mk_res pos_type_opt val1
                           end
                         else (* !Config.footprint = false *)
                           begin
                             match neg_type_opt with
                             | Some _ ->
-                                if (is_undefined_opt prop val1) then (mk_res pos_type_opt val1)
-                                else
-                                  Tabulation.raise_cast_exception
-                                    (try assert false with Assert_failure ml_loc -> ml_loc)
-                                    None texp1 texp2 val1
-                            | None -> (mk_res pos_type_opt val1)
+                                if is_undefined_opt 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
                       end
                 | _ -> []

infer/src/clang/cTrans.ml

@@ -1948,6 +1948,33 @@ struct
     let stmt = match stmt_list with [stmt] -> stmt | _ -> assert false in
     instruction trans_state' stmt
 
+  and cxxDynamicCastExpr_trans trans_state stmt_info stmts cast_type_ptr =
+    let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
+    let trans_state' = { trans_state_pri with succ_nodes = [] } in
+    let context = trans_state.context in
+    let subtypes = Sil.Subtype.subtypes_cast in
+    let tenv = context.CContext.tenv in
+    let sil_loc = CLocation.get_sil_location stmt_info context in
+    let cast_type = CTypes_decl.type_ptr_to_sil_type tenv cast_type_ptr in
+    let sizeof_expr = match cast_type with
+      | Sil.Tptr (typ, _) -> Sil.Sizeof (typ, subtypes)
+      | _ -> assert false in
+    let builtin = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__cast) in
+    let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
+    let res_trans_stmt = exec_with_lvalue_as_reference instruction trans_state' stmt in
+    let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in
+    let args = [exp; (sizeof_expr, Sil.Tvoid)] in
+    let ret_id = Ident.create_fresh Ident.knormal in
+    let call = Sil.Call ([ret_id], builtin, args, sil_loc, Sil.cf_default) in
+    let res_ex = Sil.Var ret_id in
+    let res_trans_dynamic_cast = { empty_res_trans with instrs = [call]; ids = [ret_id] } in
+    let all_res_trans = [ res_trans_stmt; res_trans_dynamic_cast ] in
+    let nname = "CxxDynamicCast" in
+    let res_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc nname
+        stmt_info all_res_trans in
+    { res_trans_to_parent with exps = [(res_ex, cast_type)] }
+
+
   (* Translates a clang instruction into SIL instructions. It takes a       *)
   (* a trans_state containing current info on the translation and it returns *)
   (* a result_state.*)
@@ -2173,9 +2200,14 @@ struct
         compoundLiteralExpr_trans trans_state stmt_info stmt_list expr_info
     | InitListExpr (stmt_info, stmts, expr_info) ->
         initListExpr_trans trans_state stmt_info expr_info stmts
-    | CXXBindTemporaryExpr (stmt_info, stmt_list, expr_info, cxx_bind_temp_expr_info)->
+
+    | CXXBindTemporaryExpr (stmt_info, stmt_list, expr_info, cxx_bind_temp_expr_info) ->
         (* right now we ignore this expression and try to translate the child node *)
         parenExpr_trans trans_state stmt_info stmt_list
+
+    | CXXDynamicCastExpr (stmt_info, stmts, expr_info, cast_expr_info, type_ptr, _) ->
+        cxxDynamicCastExpr_trans trans_state stmt_info stmts type_ptr
+
     | s -> (Printing.log_stats
               "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: Translation need to be defined. Statement ignored.... \n"
               (Ast_utils.string_of_stmt s);

infer/tests/codetoanalyze/cpp/errors/subtyping/dynamic_cast.cpp

@@ -0,0 +1,71 @@
+/*
+ * 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.
+ */
+
+class Base {
+    virtual void dummy() {}
+public:
+    int b;
+};
+class Derived: public Base {
+    int a;
+};
+
+int castOfArgumentPointer(Base* pb) {
+    if (dynamic_cast<Derived*>(pb)) {
+        return 1;
+    }
+    else return 0;
+}
+
+int castOfArgumentReference(Base& pdd) {
+    Derived& pdd2 = dynamic_cast<Derived&>(pdd);
+    return 0;
+}
+
+int wrongCastOfArgumentPointer(){
+    Base pdd;
+    return 1/castOfArgumentPointer(&pdd);
+}
+
+//This should give a CLASS_CAST_EXCEPTION error but doesn't yet.
+int wrongCastOfArgumentReference(){
+    Base pdd;
+    return castOfArgumentReference(pdd);
+}
+
+int wrongPointerCast() {
+    Base * pbb = new Base;
+    Derived * pd = dynamic_cast<Derived*>(pbb);
+    if (pd) return 1;
+    else return 1/0;
+}
+
+int rightPointerCast() {
+    Base * pbb = new Derived;
+    Derived * pd = dynamic_cast<Derived*>(pbb);
+    if (pd) return 1/0;
+    else return 1;
+}
+
+void rightReferenceCast() {
+    Base * pbb = new Derived;
+    Derived& pdd1 = dynamic_cast<Derived&>(*pbb);
+}
+
+void wrongReferenceCast() {
+    Base * pbb = new Base;
+    Base& pdd = *pbb;
+    Derived& pdd1 = dynamic_cast<Derived&>(pdd);
+}
+
+void wrongReferenceCastNotAssigned() {
+    Base * pbb = new Base;
+    Base& pdd = *pbb;
+    dynamic_cast<Derived&>(pdd);
+}

infer/tests/endtoend/cpp/DynamicCastTest.java

@@ -0,0 +1,110 @@
+/*
+ * 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.ResultContainsErrorInMethod.contains;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+import static utils.matchers.ResultContainsNoErrorInMethod.doesNotContain;
+
+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 DynamicCastTest {
+
+  public static final String FILE =
+      "infer/tests/codetoanalyze/cpp/errors/subtyping/dynamic_cast.cpp";
+
+  private static ImmutableList<String> inferCmd;
+
+  public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO";
+
+  public static final String CLASS_CAST_EXCEPTION = "CLASS_CAST_EXCEPTION";
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder =
+      new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createCPPInferCommand(folder, FILE);
+  }
+
+  @Test
+  public void whenInferRunsOnWrongCastOfArgumentPointerThenDivideByZeroIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    assertThat(
+        "Results should contain divide by zero, it shows a wrong cast to pointer to class",
+        inferResults,
+        contains(DIVIDE_BY_ZERO, FILE, "wrongCastOfArgumentPointer"));
+  }
+
+  @Test
+  public void whenInferRunsOnWrongPointerCastThenDivideByZeroIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    assertThat(
+        "Results should contain divide by zero, it shows a wrong cast to pointer to class",
+        inferResults,
+        contains(DIVIDE_BY_ZERO, FILE, "wrongPointerCast"));
+  }
+
+  @Test
+  public void whenInferRunsOnRightPointerCastThenDivideByZeroIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    assertThat(
+        "Results should contain divide by zero, it shows a correct cast to pointer to class",
+        inferResults,
+        contains(DIVIDE_BY_ZERO, FILE, "rightPointerCast"));
+  }
+
+  @Test
+  public void whenInferRunsOnRightReferenceCastThenClassCastExceptionIsNotFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    assertThat(
+        "Results should not contain class cast exception",
+        inferResults,
+        doesNotContain(CLASS_CAST_EXCEPTION, FILE, "rightReferenceCast"));
+  }
+
+  @Test
+  public void whenInferRunsOnWrongReferenceCastThenClassCastExceptionIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    assertThat(
+        "Results should contain class cast exception",
+        inferResults,
+        contains(CLASS_CAST_EXCEPTION, FILE, "wrongReferenceCast"));
+  }
+
+  @Test
+  public void whenInferRunsOnWrongReferenceCastNotAssignedThenClassCastExceptionIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    assertThat(
+        "Results should contain class cast exception",
+        inferResults,
+        contains(CLASS_CAST_EXCEPTION, FILE, "wrongReferenceCastNotAssigned"));
+  }
+
+}