diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index d3cc41132..4f024d256 100644 --- a/infer/src/backend/symExec.ml +++ b/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 | _ -> [] diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 142dfc781..868c33c85 100644 --- a/infer/src/clang/cTrans.ml +++ b/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); diff --git a/infer/tests/codetoanalyze/cpp/errors/subtyping/dynamic_cast.cpp b/infer/tests/codetoanalyze/cpp/errors/subtyping/dynamic_cast.cpp new file mode 100644 index 000000000..9ccf3f16b --- /dev/null +++ b/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(pb)) { + return 1; + } + else return 0; +} + +int castOfArgumentReference(Base& pdd) { + Derived& pdd2 = dynamic_cast(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(pbb); + if (pd) return 1; + else return 1/0; +} + +int rightPointerCast() { + Base * pbb = new Derived; + Derived * pd = dynamic_cast(pbb); + if (pd) return 1/0; + else return 1; +} + +void rightReferenceCast() { + Base * pbb = new Derived; + Derived& pdd1 = dynamic_cast(*pbb); +} + +void wrongReferenceCast() { + Base * pbb = new Base; + Base& pdd = *pbb; + Derived& pdd1 = dynamic_cast(pdd); +} + +void wrongReferenceCastNotAssigned() { + Base * pbb = new Base; + Base& pdd = *pbb; + dynamic_cast(pdd); +} diff --git a/infer/tests/endtoend/cpp/DynamicCastTest.java b/infer/tests/endtoend/cpp/DynamicCastTest.java new file mode 100644 index 000000000..27b7ccd08 --- /dev/null +++ b/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 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")); + } + +}