From 0c5bca7a4b0dccb3e53e72fb1775419a1adf2f37 Mon Sep 17 00:00:00 2001 From: Dulma Rodriguez Date: Thu, 24 Mar 2016 08:57:20 -0700 Subject: [PATCH] Translate arrays created with new Reviewed By: ddino Differential Revision: D3088249 fb-gh-sync-id: 3eceba4 shipit-source-id: 3eceba4 --- infer/src/backend/abs.ml | 6 +- infer/src/clang/cTrans.ml | 87 +++++++++++-------- infer/src/clang/cTrans_utils.ml | 21 +++-- infer/src/clang/cTrans_utils.mli | 2 +- .../frontend/constructors/constructor_new.cpp | 12 +++ .../constructors/constructor_new.cpp.dot | 63 ++++++++++++++ .../endtoend/cpp/ConstructorNewTest.java | 4 +- 7 files changed, 149 insertions(+), 46 deletions(-) diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 54cc649d6..08e40b439 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1106,7 +1106,8 @@ let check_junk ?original_prop pname tenv prop = let ml_bucket_opt = match resource with | Sil.Rmemory Sil.Mobjc -> should_raise_objc_leak hpred - | Sil.Rmemory Sil.Mnew when !Config.curr_language = Config.C_CPP -> + | Sil.Rmemory Sil.Mnew | Sil.Rmemory Sil.Mnew_array + when !Config.curr_language = Config.C_CPP -> Mleak_buckets.should_raise_cpp_leak () | _ -> None in let exn_retain_cycle cycle = @@ -1133,7 +1134,8 @@ let check_junk ?original_prop pname tenv prop = (cycle_has_weak_or_unretained_or_assign_field cycle) in ignore_cycle, exn_retain_cycle cycle | Some _, Sil.Rmemory Sil.Mobjc - | Some _, Sil.Rmemory Sil.Mnew when !Config.curr_language = Config.C_CPP -> + | Some _, Sil.Rmemory Sil.Mnew + | Some _, Sil.Rmemory Sil.Mnew_array when !Config.curr_language = Config.C_CPP -> ml_bucket_opt = None, exn_leak | Some _, Sil.Rmemory _ -> !Config.curr_language = Config.Java, exn_leak | Some _, Sil.Rignore -> true, exn_leak diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index c40fa9735..0575ab1e3 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -1531,6 +1531,7 @@ struct and initListExpr_trans trans_state stmt_info expr_info stmts = let context = trans_state.context in let tenv = context.tenv in + let is_array typ = match typ with | Sil.Tarray _ -> true | _ -> false in let (var_exp, typ) = match trans_state.var_exp_typ with | Some var_exp_typ -> var_exp_typ @@ -1550,24 +1551,32 @@ struct if IList.length rh_exps == 0 then let exp = Sil.zero_value_of_numerical_type var_type in { empty_res_trans with root_nodes = trans_state.succ_nodes; exps = [(exp, typ)]; } - else if IList.length rh_exps != IList.length lh then - (* If the right hand expressions are not as many as the left hand expressions something's wrong *) - { empty_res_trans with root_nodes = trans_state.succ_nodes } else - (* Creating new instructions by assigning right hand side to left hand side expressions *) - let assign_instr (lh_exp, lh_t) (rh_exp, _) = Sil.Set (lh_exp, lh_t, rh_exp, sil_loc) in - let assign_instrs = IList.map2 assign_instr lh rh_exps in - let initlist_expr_res = - { empty_res_trans with - exps = [(var_exp, var_type)]; - initd_exps = [var_exp]; - instrs = assign_instrs; - } in - let all_res_trans = res_trans_subexpr_list @ [initlist_expr_res] in - let nname = "InitListExp" 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 = initlist_expr_res.exps } + (* For arrays, the size in the type may be an overapproximation of the number *) + (* of literals the array is initialized with *) + let lh = + if is_array var_type && IList.length lh > IList.length rh_exps then + let i = IList.length lh - IList.length rh_exps in + IList.drop_last i lh + else lh in + if IList.length rh_exps == IList.length lh then + (* Creating new instructions by assigning right hand side to left hand side expressions *) + let assign_instr (lh_exp, lh_t) (rh_exp, _) = Sil.Set (lh_exp, lh_t, rh_exp, sil_loc) in + let assign_instrs = IList.map2 assign_instr lh rh_exps in + let initlist_expr_res = + { empty_res_trans with + exps = [(var_exp, var_type)]; + initd_exps = [var_exp]; + instrs = assign_instrs; + } in + let all_res_trans = res_trans_subexpr_list @ [initlist_expr_res] in + let nname = "InitListExp" 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 = initlist_expr_res.exps } + else (* If the right hand expressions are not as many as the left hand expressions *) + (* something's wrong *) + { empty_res_trans with root_nodes = trans_state.succ_nodes } and init_expr_trans trans_state var_exp_typ var_stmt_info init_expr_opt = match init_expr_opt with @@ -1929,24 +1938,32 @@ struct let typ = CTypes_decl.get_type_from_expr_info expr_info context.CContext.tenv in let sil_loc = CLocation.get_sil_location stmt_info context in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in - let res_trans_new = cpp_new_trans trans_state_pri sil_loc typ in - if cxx_new_expr_info.Clang_ast_t.xnei_is_array then - assert false (* TODO *) - else - let stmt_opt = Ast_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in - let trans_state_init = { trans_state_pri with succ_nodes = []; } in - let var_exp_typ = match res_trans_new.exps with [exp] -> exp | _ -> assert false in - (* Need a new stmt_info for the translation of the initializer, so that it can create nodes *) - (* if it needs to, with the same stmt_info it doesn't work. *) - let init_stmt_info = { stmt_info with - Clang_ast_t.si_pointer = Ast_utils.get_fresh_pointer () } in - let res_trans_init = - init_expr_trans trans_state_init var_exp_typ init_stmt_info stmt_opt in - let all_res_trans = [res_trans_new; res_trans_init] in - let nname = "CXXNewExpr" in - let result_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc - nname stmt_info all_res_trans in - { result_trans_to_parent with exps = res_trans_new.exps } + let size_exp_opt, res_trans_size = + if cxx_new_expr_info.Clang_ast_t.xnei_is_array then + match Ast_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_array_size_expr with + | Some stmt -> + let trans_state_size = { trans_state_pri with succ_nodes = []; } in + let res_trans_size = instruction trans_state_size stmt in + (match res_trans_size.exps with + | [(exp, _)] -> Some exp, res_trans_size + | _ -> None, empty_res_trans) + | None -> Some (Sil.Const (Sil.Cint (Sil.Int.minus_one))), empty_res_trans + else None, empty_res_trans in + let res_trans_new = cpp_new_trans trans_state_pri sil_loc typ size_exp_opt in + let stmt_opt = Ast_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in + let trans_state_init = { trans_state_pri with succ_nodes = []; } in + let var_exp_typ = match res_trans_new.exps with [exp] -> exp | _ -> assert false in + (* Need a new stmt_info for the translation of the initializer, so that it can create nodes *) + (* if it needs to, with the same stmt_info it doesn't work. *) + let init_stmt_info = { stmt_info with + Clang_ast_t.si_pointer = Ast_utils.get_fresh_pointer () } in + let res_trans_init = + init_expr_trans trans_state_init var_exp_typ init_stmt_info stmt_opt in + let all_res_trans = [res_trans_size; res_trans_new; res_trans_init] in + let nname = "CXXNewExpr" in + let result_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc + nname stmt_info all_res_trans in + { result_trans_to_parent with exps = res_trans_new.exps } (* TODOs 7912220 - no usable information in json as of right now *) (* 1. Handle __new_array *) diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 42d1def3c..a2bdf9d4a 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -288,7 +288,7 @@ struct end (** This function handles ObjC new/alloc and C++ new calls *) -let create_alloc_instrs context sil_loc function_type fname = +let create_alloc_instrs context sil_loc function_type fname size_exp_opt = let function_type, function_type_np = match function_type with | Sil.Tptr (styp, Sil.Pk_pointer) @@ -298,7 +298,10 @@ let create_alloc_instrs context sil_loc function_type fname = function_type, styp | _ -> Sil.Tptr (function_type, Sil.Pk_pointer), function_type in let function_type_np = CTypes.expand_structured_type context.CContext.tenv function_type_np in - let sizeof_exp = Sil.Sizeof (function_type_np, Sil.Subtype.exact) in + let sizeof_exp_ = Sil.Sizeof (function_type_np, Sil.Subtype.exact) in + let sizeof_exp = match size_exp_opt with + | Some exp -> Sil.BinOp (Sil.Mult, sizeof_exp_, exp) + | None -> sizeof_exp_ in let exp = (sizeof_exp, Sil.Tint Sil.IULong) in let ret_id = Ident.create_fresh Ident.knormal in let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun fname)), [exp], sil_loc, Sil.cf_default) in @@ -309,7 +312,8 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc = SymExec.ModelBuiltins.__objc_alloc_no_fail else SymExec.ModelBuiltins.__objc_alloc in - let (function_type, ret_id, stmt_call, exp) = create_alloc_instrs trans_state.context loc function_type fname in + let (function_type, ret_id, stmt_call, exp) = + create_alloc_instrs trans_state.context loc function_type fname None in let res_trans_tmp = { empty_res_trans with ids =[ret_id]; instrs =[stmt_call]} in let res_trans = let nname = "Call alloc" in @@ -319,7 +323,7 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc = let objc_new_trans trans_state loc stmt_info cls_name function_type = let fname = SymExec.ModelBuiltins.__objc_alloc_no_fail in let (alloc_ret_type, alloc_ret_id, alloc_stmt_call, _) = - create_alloc_instrs trans_state.context loc function_type fname in + create_alloc_instrs trans_state.context loc function_type fname None in let init_ret_id = Ident.create_fresh Ident.knormal in let is_instance = true in let call_flags = { Sil.cf_default with Sil.cf_virtual = is_instance; } in @@ -348,10 +352,13 @@ let new_or_alloc_trans trans_state loc stmt_info type_ptr class_name_opt selecto objc_new_trans trans_state loc stmt_info class_name function_type else assert false -let cpp_new_trans trans_state sil_loc function_type = - let fname = SymExec.ModelBuiltins.__new in +let cpp_new_trans trans_state sil_loc function_type size_exp_opt = + let fname = + match size_exp_opt with + | Some _ -> SymExec.ModelBuiltins.__new_array + | None -> SymExec.ModelBuiltins.__new in let (function_type, ret_id, stmt_call, exp) = - create_alloc_instrs trans_state.context sil_loc function_type fname in + create_alloc_instrs trans_state.context sil_loc function_type fname size_exp_opt in { empty_res_trans with ids = [ret_id]; instrs = [stmt_call]; exps = [(exp, function_type)] } let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc = diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index f1a46c7b2..6abd406a3 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -107,7 +107,7 @@ val alloc_trans : val new_or_alloc_trans : trans_state -> Location.t -> Clang_ast_t.stmt_info -> Clang_ast_t.type_ptr -> string option -> string -> trans_result -val cpp_new_trans : trans_state -> Location.t -> Sil.typ -> trans_result +val cpp_new_trans : trans_state -> Location.t -> Sil.typ -> Sil.exp option -> trans_result val cast_trans : CContext.t -> (Sil.exp * Sil.typ) list -> Location.t -> Procname.t option -> Sil.typ -> diff --git a/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp b/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp index 59ad7ed32..3ea6ea846 100644 --- a/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp +++ b/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp @@ -70,3 +70,15 @@ int constructor_nodes() { Person* p = new Person(getValue(0) ? getValue(1) : 1 + z); return 1 / (p->x - 7); } + +int int_array() { + int* x2 = new int[getValue(5) ? getValue(5) : 3]; + x2[0] = 1; + x2[1] = 2; + return 1 / ((x2[0] + x2[1]) - 3); +} + +int int_array_init() { + int* arr = new int[100]{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}; + return 1 / ((arr[0] + arr[1] + arr[2] + arr[3] + arr[4]) - 15); +} diff --git a/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp.dot b/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp.dot index 853a8b494..d63d7b444 100644 --- a/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp.dot +++ b/infer/tests/codetoanalyze/cpp/frontend/constructors/constructor_new.cpp.dot @@ -1,4 +1,67 @@ digraph iCFG { +78 [label="78: DeclStmt \n n$10=_fun___new_array((sizeof(int ) * 100):unsigned long ) [line 82]\n *n$10[0]:int =1 [line 82]\n *n$10[1]:int =2 [line 82]\n *n$10[2]:int =3 [line 82]\n *n$10[3]:int =4 [line 82]\n *n$10[4]:int =5 [line 82]\n *n$10[5]:int =6 [line 82]\n *n$10[6]:int =7 [line 82]\n *n$10[7]:int =8 [line 82]\n *n$10[8]:int =9 [line 82]\n *n$10[9]:int =10 [line 82]\n *&arr:int *=n$10 [line 82]\n REMOVE_TEMPS(n$10); [line 82]\n " shape="box"] + + + 78 -> 77 ; +77 [label="77: Return Stmt \n n$0=*&arr:int * [line 83]\n n$1=*n$0[0]:int [line 83]\n n$2=*&arr:int * [line 83]\n n$3=*n$2[1]:int [line 83]\n n$4=*&arr:int * [line 83]\n n$5=*n$4[2]:int [line 83]\n n$6=*&arr:int * [line 83]\n n$7=*n$6[3]:int [line 83]\n n$8=*&arr:int * [line 83]\n n$9=*n$8[4]:int [line 83]\n *&return:int =(1 / (((((n$1 + n$3) + n$5) + n$7) + n$9) - 15)) [line 83]\n REMOVE_TEMPS(n$0,n$1,n$2,n$3,n$4,n$5,n$6,n$7,n$8,n$9); [line 83]\n NULLIFY(&arr,false); [line 83]\n APPLY_ABSTRACTION; [line 83]\n " shape="box"] + + + 77 -> 76 ; +76 [label="76: Exit int_array_init \n " color=yellow style=filled] + + +75 [label="75: Start int_array_init\nFormals: \nLocals: arr:int * \n DECLARE_LOCALS(&return,&arr); [line 81]\n NULLIFY(&arr,false); [line 81]\n " color=yellow style=filled] + + + 75 -> 78 ; +74 [label="74: DeclStmt \n n$8=*&SIL_temp_conditional___68:int [line 75]\n NULLIFY(&SIL_temp_conditional___68,true); [line 75]\n n$9=_fun___new_array((sizeof(int ) * n$8):unsigned long ) [line 75]\n *&x2:int *=n$9 [line 75]\n REMOVE_TEMPS(n$8,n$9); [line 75]\n " shape="box"] + + + 74 -> 67 ; +73 [label="73: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___68); [line 75]\n *&SIL_temp_conditional___68:int =3 [line 75]\n APPLY_ABSTRACTION; [line 75]\n " shape="box"] + + + 73 -> 68 ; +72 [label="72: ConditinalStmt Branch \n n$7=_fun_getValue(5:int ) [line 75]\n DECLARE_LOCALS(&SIL_temp_conditional___68); [line 75]\n *&SIL_temp_conditional___68:int =n$7 [line 75]\n REMOVE_TEMPS(n$7); [line 75]\n APPLY_ABSTRACTION; [line 75]\n " shape="box"] + + + 72 -> 68 ; +71 [label="71: Prune (false branch) \n PRUNE((n$6 == 0), false); [line 75]\n REMOVE_TEMPS(n$6); [line 75]\n " shape="invhouse"] + + + 71 -> 73 ; +70 [label="70: Prune (true branch) \n PRUNE((n$6 != 0), true); [line 75]\n REMOVE_TEMPS(n$6); [line 75]\n " shape="invhouse"] + + + 70 -> 72 ; +69 [label="69: Call _fun_getValue \n n$6=_fun_getValue(5:int ) [line 75]\n " shape="box"] + + + 69 -> 70 ; + 69 -> 71 ; +68 [label="68: + \n " ] + + + 68 -> 74 ; +67 [label="67: BinaryOperatorStmt: Assign \n n$5=*&x2:int * [line 76]\n *n$5[0]:int =1 [line 76]\n REMOVE_TEMPS(n$5); [line 76]\n " shape="box"] + + + 67 -> 66 ; +66 [label="66: BinaryOperatorStmt: Assign \n n$4=*&x2:int * [line 77]\n *n$4[1]:int =2 [line 77]\n REMOVE_TEMPS(n$4); [line 77]\n " shape="box"] + + + 66 -> 65 ; +65 [label="65: Return Stmt \n n$0=*&x2:int * [line 78]\n n$1=*n$0[0]:int [line 78]\n n$2=*&x2:int * [line 78]\n n$3=*n$2[1]:int [line 78]\n *&return:int =(1 / ((n$1 + n$3) - 3)) [line 78]\n REMOVE_TEMPS(n$0,n$1,n$2,n$3); [line 78]\n NULLIFY(&x2,false); [line 78]\n APPLY_ABSTRACTION; [line 78]\n " shape="box"] + + + 65 -> 64 ; +64 [label="64: Exit int_array \n " color=yellow style=filled] + + +63 [label="63: Start int_array\nFormals: \nLocals: x2:int * \n DECLARE_LOCALS(&return,&x2); [line 74]\n NULLIFY(&x2,false); [line 74]\n " color=yellow style=filled] + + + 63 -> 69 ; 62 [label="62: DeclStmt \n *&z:int =6 [line 69]\n " shape="box"] diff --git a/infer/tests/endtoend/cpp/ConstructorNewTest.java b/infer/tests/endtoend/cpp/ConstructorNewTest.java index fec1dd7fb..ad7971459 100644 --- a/infer/tests/endtoend/cpp/ConstructorNewTest.java +++ b/infer/tests/endtoend/cpp/ConstructorNewTest.java @@ -56,7 +56,9 @@ public class ConstructorNewTest { "int_init_empty_list", "int_init_empty_list_new", "int_init_nodes", - "constructor_nodes" + "constructor_nodes", + "int_array", + "int_array_init" }; assertThat( "Results should contain the expected divide by zero",