diff --git a/facebook-clang-plugins b/facebook-clang-plugins index 02753b33f..9ce2266db 160000 --- a/facebook-clang-plugins +++ b/facebook-clang-plugins @@ -1 +1 @@ -Subproject commit 02753b33ffcdc9607907270b3d555c4c50738b95 +Subproject commit 9ce2266db9bdf23d70ddaed093decdeeb6bf8db3 diff --git a/infer/src/IR/ProcAttributes.re b/infer/src/IR/ProcAttributes.re index f925c6438..c707d5375 100644 --- a/infer/src/IR/ProcAttributes.re +++ b/infer/src/IR/ProcAttributes.re @@ -29,6 +29,7 @@ type t = { err_log: Errlog.t, /** Error log for the procedure */ exceptions: list string, /** exceptions thrown by the procedure */ formals: list (Mangled.t, Typ.t), /** name and type of formal parameters */ + const_formals: list int, /** list of indices of formals that are const-qualified */ func_attributes: list PredSymb.func_attribute, is_abstract: bool, /** the procedure is abstract */ mutable is_bridge_method: bool, /** the procedure is a bridge method */ @@ -54,6 +55,7 @@ let default proc_name language => { err_log: Errlog.empty (), exceptions: [], formals: [], + const_formals: [], func_attributes: [], is_abstract: false, is_bridge_method: false, diff --git a/infer/src/IR/ProcAttributes.rei b/infer/src/IR/ProcAttributes.rei index 38974d664..a7c8bfc1a 100644 --- a/infer/src/IR/ProcAttributes.rei +++ b/infer/src/IR/ProcAttributes.rei @@ -23,6 +23,7 @@ type t = { err_log: Errlog.t, /** Error log for the procedure */ exceptions: list string, /** exceptions thrown by the procedure */ formals: list (Mangled.t, Typ.t), /** name and type of formal parameters */ + const_formals: list int, /** list of indices of formals that are const-qualified */ func_attributes: list PredSymb.func_attribute, is_abstract: bool, /** the procedure is abstract */ mutable is_bridge_method: bool, /** the procedure is a bridge method */ diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 5f2acfa16..7f67f6125 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1289,77 +1289,91 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call | hpred -> hpred) prop.Prop.sigma in Prop.normalize (Prop.set prop ~sigma:sigma') in - if Config.angelic_execution then - let add_actual_by_ref_to_footprint prop (actual, actual_typ) = - match actual with - | Exp.Lvar actual_pv -> - (* introduce a fresh program variable to allow abduction on the return value *) - let abducted_ref_pv = - Pvar.mk_abducted_ref_param callee_pname actual_pv callee_loc in - let already_has_abducted_retval p = - IList.exists - (fun hpred -> match hpred with - | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abducted_ref_pv - | _ -> false) - p.Prop.sigma_fp in - (* prevent introducing multiple abducted retvals for a single call site in a loop *) - if already_has_abducted_retval prop then prop - else - if !Config.footprint then - let prop', abduced_strexp = match actual_typ with - | Typ.Tptr ((Typ.Tstruct _) as typ, _) -> - (* for struct types passed by reference, do abduction on the fields of the - struct *) - add_struct_value_to_footprint tenv abducted_ref_pv typ prop - | Typ.Tptr (typ, _) -> - (* for pointer types passed by reference, do abduction directly on the pointer *) - let (prop', fresh_fp_var) = - add_to_footprint abducted_ref_pv typ prop in - prop', Sil.Eexp (fresh_fp_var, Sil.Inone) - | typ -> - failwith - ("No need for abduction on non-pointer type " ^ - (Typ.to_string typ)) in - (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *) + let add_actual_by_ref_to_footprint prop (actual, actual_typ, _) = + match actual with + | Exp.Lvar actual_pv -> + (* introduce a fresh program variable to allow abduction on the return value *) + let abducted_ref_pv = + Pvar.mk_abducted_ref_param callee_pname actual_pv callee_loc in + let already_has_abducted_retval p = + IList.exists + (fun hpred -> match hpred with + | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abducted_ref_pv + | _ -> false) + p.Prop.sigma_fp in + (* prevent introducing multiple abducted retvals for a single call site in a loop *) + if already_has_abducted_retval prop then prop + else + if !Config.footprint then + let prop', abduced_strexp = match actual_typ with + | Typ.Tptr ((Typ.Tstruct _) as typ, _) -> + (* for struct types passed by reference, do abduction on the fields of the + struct *) + add_struct_value_to_footprint tenv abducted_ref_pv typ prop + | Typ.Tptr (typ, _) -> + (* for pointer types passed by reference, do abduction directly on the pointer *) + let (prop', fresh_fp_var) = + add_to_footprint abducted_ref_pv typ prop in + prop', Sil.Eexp (fresh_fp_var, Sil.Inone) + | typ -> + failwith + ("No need for abduction on non-pointer type " ^ + (Typ.to_string typ)) in + (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *) + let filtered_sigma = + IList.map + (function + | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual -> + Sil.Hpointsto (lhs, abduced_strexp, typ_exp) + | hpred -> hpred) + prop'.Prop.sigma in + Prop.normalize (Prop.set prop' ~sigma:filtered_sigma) + else + (* bind actual passed by ref to the abducted value pointed to by the synthetic pvar *) + let prop' = let filtered_sigma = - IList.map + IList.filter (function - | Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual -> - Sil.Hpointsto (lhs, abduced_strexp, typ_exp) - | hpred -> hpred) - prop'.Prop.sigma in - Prop.normalize (Prop.set prop' ~sigma:filtered_sigma) - else - (* bind actual passed by ref to the abducted value pointed to by the synthetic pvar *) - let prop' = - let filtered_sigma = - IList.filter - (function - | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual -> - false - | _ -> true) - prop.Prop.sigma in - Prop.normalize (Prop.set prop ~sigma:filtered_sigma) in - IList.fold_left - (fun p hpred -> - match hpred with - | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abducted_ref_pv -> - let new_hpred = Sil.Hpointsto (actual, rhs, texp) in - Prop.normalize (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma)) - | _ -> p) - prop' - prop'.Prop.sigma - | _ -> assert false in - IList.fold_left add_actual_by_ref_to_footprint prop actuals_by_ref - else - (* non-angelic mode; havoc each var passed by reference by assigning it to a fresh id *) - let havoc_actual_by_ref (actual, actual_typ) prop = - let actual_pt_havocd_var = - let havocd_var = Exp.Var (Ident.create_fresh Ident.kprimed) in - let sizeof_exp = Exp.Sizeof (Typ.strip_ptr actual_typ, None, Subtype.subtypes) in - Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in - replace_actual_hpred actual actual_pt_havocd_var prop in - IList.fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref + | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual -> + false + | _ -> true) + prop.Prop.sigma in + Prop.normalize (Prop.set prop ~sigma:filtered_sigma) in + IList.fold_left + (fun p hpred -> + match hpred with + | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abducted_ref_pv -> + let new_hpred = Sil.Hpointsto (actual, rhs, texp) in + Prop.normalize (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma)) + | _ -> p) + prop' + prop'.Prop.sigma + | _ -> assert false in + (* non-angelic mode; havoc each var passed by reference by assigning it to a fresh id *) + let havoc_actual_by_ref prop (actual, actual_typ, _) = + let actual_pt_havocd_var = + let havocd_var = Exp.Var (Ident.create_fresh Ident.kprimed) in + let sizeof_exp = Exp.Sizeof (Typ.strip_ptr actual_typ, None, Subtype.subtypes) in + Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in + replace_actual_hpred actual actual_pt_havocd_var prop in + let do_actual_by_ref = + if Config.angelic_execution then add_actual_by_ref_to_footprint + else havoc_actual_by_ref in + let non_const_actuals_by_ref = + let is_not_const (e, _, i) = + match AttributesTable.load_attributes callee_pname with + | Some attrs -> + let is_const = IList.mem int_equal i attrs.ProcAttributes.const_formals in + if is_const then ( + L.d_str (Printf.sprintf "Not havocing const argument number %d: " i); + Sil.d_exp e; + L.d_ln () + ); + not is_const + | None -> + true in + IList.filter is_not_const actuals_by_ref in + IList.fold_left do_actual_by_ref prop non_const_actuals_by_ref and check_untainted exp taint_kind caller_pname callee_pname prop = match Attribute.get_taint prop exp with @@ -1420,11 +1434,11 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots |> fst else prop in let actuals_by_ref = - IList.filter - (function - | Exp.Lvar _, Typ.Tptr _ -> true - | _ -> false) - args in + IList.flatten_options (IList.mapi + (fun i actual -> match actual with + | (Exp.Lvar _ as e, (Typ.Tptr _ as t)) -> Some (e, t, i) + | _ -> None) + args) in let has_nullable_annot = Annotations.ia_is_nullable ret_annots in let pre_final = (* in Java, assume that skip functions close resources passed as params *) @@ -1448,7 +1462,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots let exps_to_mark = let ret_exps = IList.map (fun ret_id -> Exp.Var ret_id) ret_ids in IList.fold_left - (fun exps_to_mark (exp, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in + (fun exps_to_mark (exp, _, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in let prop_with_undef_attr = let path_pos = State.get_path_pos () in Attribute.mark_vars_as_undefined diff --git a/infer/src/clang/ast_expressions.ml b/infer/src/clang/ast_expressions.ml index b9ffcf9cc..bc1b81c04 100644 --- a/infer/src/clang/ast_expressions.ml +++ b/infer/src/clang/ast_expressions.ml @@ -94,6 +94,7 @@ let create_char_type = let create_char_star_type = new_constant_type_ptr () +let create_char_star_qual_type ~is_const = create_qual_type ~is_const create_char_star_type let create_BOOL_type = new_constant_type_ptr () @@ -108,10 +109,13 @@ let create_void_void_type = new_constant_type_ptr () let create_class_type class_info = `ClassType class_info +let create_class_qual_type ?(is_const=false) class_info = + create_qual_type ~is_const @@ create_class_type class_info let create_struct_type struct_name = `StructType struct_name let create_pointer_type typ = `PointerOf typ +let create_pointer_qual_type ~is_const typ = create_qual_type ~is_const @@ create_pointer_type typ let create_reference_type typ = `ReferenceOf typ diff --git a/infer/src/clang/ast_expressions.mli b/infer/src/clang/ast_expressions.mli index aaa941d06..013b2cdb8 100644 --- a/infer/src/clang/ast_expressions.mli +++ b/infer/src/clang/ast_expressions.mli @@ -19,9 +19,12 @@ val dummy_source_range : unit -> source_range val dummy_stmt_info : unit -> stmt_info +val create_qual_type : ?is_const:bool -> type_ptr -> qual_type + val create_char_type : type_ptr val create_char_star_type : type_ptr +val create_char_star_qual_type : is_const:bool -> qual_type val create_id_type : type_ptr @@ -42,10 +45,12 @@ val create_void_unsigned_long_type : type_ptr val create_void_void_type : type_ptr val create_class_type : Clang_ast_types.class_info -> type_ptr +val create_class_qual_type : ?is_const:bool -> Clang_ast_types.class_info -> qual_type val create_struct_type : string -> type_ptr val create_pointer_type : type_ptr -> type_ptr +val create_pointer_qual_type : is_const:bool -> type_ptr -> qual_type val create_integer_literal : string -> stmt diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml index ed3efae39..458261df4 100644 --- a/infer/src/clang/cFrontend_utils.ml +++ b/infer/src/clang/cFrontend_utils.ml @@ -363,9 +363,14 @@ struct let string_of_type_ptr type_ptr = match get_desugared_type type_ptr with - | Some typ -> (Clang_ast_proj.get_type_tuple typ).Clang_ast_t.ti_raw + | Some typ -> + let type_info = Clang_ast_proj.get_type_tuple typ in + type_info.Clang_ast_t.ti_raw | None -> "" + let string_of_qual_type {Clang_ast_t.qt_type_ptr; qt_is_const} = + Printf.sprintf "%s%s" (if qt_is_const then "is_const " else "") (string_of_type_ptr qt_type_ptr) + let add_type_from_decl_ref type_ptr_to_sil_type tenv decl_ref_opt fail_if_not_found = match decl_ref_opt with (* translate interface first if found *) | Some dr -> @@ -426,8 +431,8 @@ struct let is_ptr_to_objc_class typ class_name = match typ with - | Some Clang_ast_t.ObjCObjectPointerType (_, typ_ptr) -> - (match get_desugared_type typ_ptr with + | Some Clang_ast_t.ObjCObjectPointerType (_, {Clang_ast_t.qt_type_ptr}) -> + (match get_desugared_type qt_type_ptr with | Some ObjCInterfaceType (_, ptr) -> (match get_decl ptr with | Some ObjCInterfaceDecl (_, ndi, _, _, _) -> diff --git a/infer/src/clang/cFrontend_utils.mli b/infer/src/clang/cFrontend_utils.mli index a0c504bbd..0d3e565a4 100644 --- a/infer/src/clang/cFrontend_utils.mli +++ b/infer/src/clang/cFrontend_utils.mli @@ -117,6 +117,7 @@ sig val get_decl_from_typ_ptr : Clang_ast_t.type_ptr -> Clang_ast_t.decl option val string_of_type_ptr : Clang_ast_t.type_ptr -> string + val string_of_qual_type : Clang_ast_t.qual_type -> string val make_name_decl : string -> Clang_ast_t.named_decl_info diff --git a/infer/src/clang/cMethod_signature.ml b/infer/src/clang/cMethod_signature.ml index 0c33421bd..e7ea3aadc 100644 --- a/infer/src/clang/cMethod_signature.ml +++ b/infer/src/clang/cMethod_signature.ml @@ -8,13 +8,14 @@ *) open! Utils +open CFrontend_utils (** Define the signature of a method consisting of its name, its arguments, *) (** return type, location and whether its an instance method. *) type method_signature = { mutable name : Procname.t; - args : (Mangled.t * Clang_ast_t.type_ptr) list; + args : (Mangled.t * Clang_ast_t.qual_type) list; ret_type : Clang_ast_t.type_ptr; attributes : Clang_ast_t.attribute list; loc : Clang_ast_t.source_range; @@ -99,7 +100,7 @@ let replace_name_ms ms name = let ms_to_string ms = "Method " ^ (Procname.to_string ms.name) ^ " " ^ IList.to_string - (fun (s1, s2) -> (Mangled.to_string s1) ^ ", " ^ (Clang_ast_j.string_of_type_ptr s2)) + (fun (s1, s2) -> (Mangled.to_string s1) ^ ", " ^ (Ast_utils.string_of_qual_type s2)) ms.args - ^ "->" ^ (Clang_ast_j.string_of_type_ptr ms.ret_type) ^ " " ^ + ^ "->" ^ (Ast_utils.string_of_type_ptr ms.ret_type) ^ " " ^ Clang_ast_j.string_of_source_range ms.loc diff --git a/infer/src/clang/cMethod_signature.mli b/infer/src/clang/cMethod_signature.mli index 9c9817626..6d8a95e6e 100644 --- a/infer/src/clang/cMethod_signature.mli +++ b/infer/src/clang/cMethod_signature.mli @@ -19,7 +19,7 @@ val ms_get_name : method_signature -> Procname.t val ms_set_name : method_signature -> Procname.t -> unit val ms_get_args : method_signature -> - (Mangled.t * Clang_ast_t.type_ptr) list + (Mangled.t * Clang_ast_t.qual_type) list val ms_get_ret_type : method_signature -> Clang_ast_t.type_ptr @@ -43,7 +43,7 @@ val ms_is_getter : method_signature -> bool val ms_is_setter : method_signature -> bool -val make_ms : Procname.t -> (Mangled.t * Clang_ast_t.type_ptr) list -> Clang_ast_t.type_ptr +val make_ms : Procname.t -> (Mangled.t * Clang_ast_t.qual_type) list -> Clang_ast_t.type_ptr -> Clang_ast_t.attribute list -> Clang_ast_t.source_range -> bool -> ?is_cpp_virtual:bool -> Config.clang_lang -> Clang_ast_t.pointer option -> Clang_ast_t.pointer option -> Typ.t option -> method_signature diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index ffcc4f112..a725152da 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -52,10 +52,10 @@ let get_class_param function_method_decl_info = if (is_instance_method function_method_decl_info) then match function_method_decl_info with | Cpp_Meth_decl_info (_, _, class_decl_ptr, _) -> - let class_type = `DeclPtr class_decl_ptr in + let class_type = Ast_expressions.create_qual_type (`DeclPtr class_decl_ptr) in [(Mangled.from_string CFrontend_config.this, class_type)] | ObjC_Meth_decl_info (_, class_decl_ptr) -> - let class_type = `DeclPtr class_decl_ptr in + let class_type = Ast_expressions.create_qual_type (`DeclPtr class_decl_ptr) in [(Mangled.from_string CFrontend_config.self, class_type)] | _ -> [] else [] @@ -77,7 +77,7 @@ let get_return_param tenv function_method_decl_info = let return_typ = CTypes_decl.type_ptr_to_sil_type tenv return_type_ptr in if should_add_return_param return_typ ~is_objc_method then [(Mangled.from_string CFrontend_config.return_param, - Ast_expressions.create_pointer_type return_type_ptr)] + Ast_expressions.create_pointer_qual_type ~is_const:false return_type_ptr)] else [] @@ -110,13 +110,12 @@ let get_parameters tenv function_method_decl_info = match par with | Clang_ast_t.ParmVarDecl (_, name_info, qt, var_decl_info) -> let _, mangled = General_utils.get_var_name_mangled name_info var_decl_info in - let type_ptr = qt.Clang_ast_t.qt_type_ptr in - let param_typ = CTypes_decl.type_ptr_to_sil_type tenv type_ptr in - let type_ptr' = match param_typ with + let param_typ = CTypes_decl.type_ptr_to_sil_type tenv qt.Clang_ast_t.qt_type_ptr in + let qt_type_ptr = match param_typ with | Typ.Tstruct _ when General_utils.is_cpp_translation Config.clang_lang -> - Ast_expressions.create_reference_type type_ptr - | _ -> type_ptr in - (mangled, type_ptr') + Ast_expressions.create_reference_type qt.Clang_ast_t.qt_type_ptr + | _ -> qt.Clang_ast_t.qt_type_ptr in + (mangled, {qt with qt_type_ptr}) | _ -> assert false in let pars = IList.map par_to_ms_par (get_param_decls function_method_decl_info) in get_class_param function_method_decl_info @ pars @ get_return_param tenv function_method_decl_info @@ -297,7 +296,7 @@ let get_formal_parameters tenv ms = let rec defined_parameters pl = match pl with | [] -> [] - | (mangled, raw_type):: pl' -> + | (mangled, {Clang_ast_t.qt_type_ptr}):: pl' -> let should_add_pointer name ms = let is_objc_self = name = CFrontend_config.self && CMethod_signature.ms_get_lang ms = Config.OBJC in @@ -305,8 +304,8 @@ let get_formal_parameters tenv ms = CMethod_signature.ms_get_lang ms = Config.CPP in (is_objc_self && CMethod_signature.ms_is_instance ms) || is_cxx_this in let tp = if should_add_pointer (Mangled.to_string mangled) ms then - (Ast_expressions.create_pointer_type raw_type) - else raw_type in + (Ast_expressions.create_pointer_type qt_type_ptr) + else qt_type_ptr in let typ = CTypes_decl.type_ptr_to_sil_type tenv tp in (mangled, typ):: defined_parameters pl' in defined_parameters (CMethod_signature.ms_get_args ms) @@ -342,9 +341,9 @@ let sil_method_annotation_of_args args : Typ.method_annotation = let mk_annot param_name annot_name = let annot = { Typ.class_name = annot_name; Typ.parameters = [param_name]; } in annot, default_visibility in - let arg_to_sil_annot (arg_mangled, type_ptr) acc = + let arg_to_sil_annot (arg_mangled, {Clang_ast_t.qt_type_ptr}) acc = let arg_name = Mangled.to_string arg_mangled in - if CFrontend_utils.Ast_utils.is_type_nullable type_ptr then + if CFrontend_utils.Ast_utils.is_type_nullable qt_type_ptr then [mk_annot arg_name Annotations.nullable] :: acc else Typ.item_annotation_empty::acc in let param_annots = IList.fold_right arg_to_sil_annot args [] in @@ -352,6 +351,31 @@ let sil_method_annotation_of_args args : Typ.method_annotation = let retval_annot = [] in retval_annot, param_annots + +let is_pointer_to_const type_ptr = match Ast_utils.get_type type_ptr with + | Some PointerType (_, {Clang_ast_t.qt_is_const}) + | Some ObjCObjectPointerType (_, {Clang_ast_t.qt_is_const}) + | Some RValueReferenceType (_, {Clang_ast_t.qt_is_const}) + | Some LValueReferenceType (_, {Clang_ast_t.qt_is_const}) -> + qt_is_const + | _ -> + false + +(** Returns a list of the indices of expressions in [args] which point to const-typed values. Each + index is offset by [shift]. *) +let get_const_args_indices ~shift args = + let i = ref shift in + let rec aux result = function + | [] -> + IList.rev result + | (_, {Clang_ast_t.qt_type_ptr})::tl -> + incr i; + if is_pointer_to_const qt_type_ptr then + aux (!i - 1::result) tl + else + aux result tl in + aux [] args + (** Creates a procedure description. *) let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let defined = not ((IList.length fbody) == 0) in @@ -367,19 +391,23 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let captured_mangled = IList.map (fun (var, t) -> (Pvar.get_name var), t) captured in (* Captured variables for blocks are treated as parameters *) let formals = captured_mangled @ formals in + let const_formals = get_const_args_indices + ~shift:(IList.length captured_mangled) + (CMethod_signature.ms_get_args ms) in let source_range = CMethod_signature.ms_get_loc ms in Printing.log_out "\nCreating a new procdesc for function: '%s'\n@." pname; + Printing.log_out "\nms = %s\n@." (CMethod_signature.ms_to_string ms); let loc_start = CLocation.get_sil_location_from_range source_range true in let loc_exit = CLocation.get_sil_location_from_range source_range false in let ret_type = get_return_type tenv ms in - let captured' = IList.map (fun (var, t) -> (Pvar.get_name var, t)) captured in if skip_property_accessor ms then () else let procdesc = let proc_attributes = { (ProcAttributes.default proc_name Config.Clang) with - ProcAttributes.captured = captured'; + ProcAttributes.captured = captured_mangled; formals; + const_formals; func_attributes = attributes; is_defined = defined; is_objc_instance_method = is_objc_inst_method; diff --git a/infer/src/clang/cTrans_models.ml b/infer/src/clang/cTrans_models.ml index d95a5f796..64b732596 100644 --- a/infer/src/clang/cTrans_models.ml +++ b/infer/src/clang/cTrans_models.ml @@ -140,7 +140,8 @@ let get_predefined_ms_stringWithUTF8String class_name method_name mk_procname la class_name = CFrontend_config.nsstring_cl && method_name = CFrontend_config.string_with_utf8_m in let id_type = Ast_expressions.create_id_type in - let args = [(Mangled.from_string "x", Ast_expressions.create_char_star_type)] in + let args = [(Mangled.from_string "x", + Ast_expressions.create_char_star_qual_type ~is_const:true)] in get_predefined_ms_method condition class_name method_name Procname.ObjCClassMethod mk_procname lang args id_type [] None @@ -150,7 +151,7 @@ let get_predefined_ms_retain_release method_name mk_procname lang = if is_retain_method method_name || is_autorelease_method method_name then Ast_expressions.create_id_type else Ast_expressions.create_void_type in let class_name = CFrontend_config.nsobject_cl in - let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in + let class_type = Ast_expressions.create_class_qual_type (class_name, `OBJC) in let args = [(Mangled.from_string CFrontend_config.self, class_type)] in get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod mk_procname lang args return_type [] (get_builtinname method_name) @@ -159,7 +160,7 @@ let get_predefined_ms_autoreleasepool_init class_name method_name mk_procname la let condition = method_name = CFrontend_config.init && class_name = CFrontend_config.nsautorelease_pool_cl in - let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in + let class_type = Ast_expressions.create_class_qual_type (class_name, `OBJC) in get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod mk_procname lang [(Mangled.from_string CFrontend_config.self, class_type)] Ast_expressions.create_void_type [] None @@ -168,7 +169,7 @@ let get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procna let condition = (method_name = CFrontend_config.release || method_name = CFrontend_config.drain) && class_name = CFrontend_config.nsautorelease_pool_cl in - let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in + let class_type = Ast_expressions.create_class_qual_type (class_name, `OBJC) in let args = [(Mangled.from_string CFrontend_config.self, class_type)] in get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod mk_procname lang args Ast_expressions.create_void_type @@ -176,7 +177,7 @@ let get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procna let get_predefined_ms_is_kind_of_class class_name method_name mk_procname lang = let condition = method_name = CFrontend_config.is_kind_of_class in - let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in + let class_type = Ast_expressions.create_class_qual_type (class_name, `OBJC) in let args = [(Mangled.from_string CFrontend_config.self, class_type)] in get_predefined_ms_method condition class_name method_name Procname.ObjCInstanceMethod mk_procname lang args Ast_expressions.create_BOOL_type diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml index 05a15c0b8..898eee67a 100644 --- a/infer/src/clang/cType_to_sil_type.ml +++ b/infer/src/clang/cType_to_sil_type.ml @@ -70,8 +70,8 @@ and sil_type_of_attr_type translate_decl tenv type_info attr_info = match type_info.Clang_ast_t.ti_desugared_type with | Some type_ptr -> (match Ast_utils.get_type type_ptr with - | Some Clang_ast_t.ObjCObjectPointerType (_, type_ptr') -> - let typ = type_ptr_to_sil_type translate_decl tenv type_ptr' in + | Some Clang_ast_t.ObjCObjectPointerType (_, {Clang_ast_t.qt_type_ptr}) -> + let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in Typ.Tptr (typ, pointer_attribute_of_objc_attribute attr_info) | _ -> type_ptr_to_sil_type translate_decl tenv type_ptr) | None -> Typ.Tvoid @@ -82,9 +82,9 @@ and sil_type_of_c_type translate_decl tenv c_type = | NoneType _ -> Typ.Tvoid | BuiltinType (_, builtin_type_kind) -> sil_type_of_builtin_type_kind builtin_type_kind - | PointerType (_, type_ptr) - | ObjCObjectPointerType (_, type_ptr) -> - let typ = type_ptr_to_sil_type translate_decl tenv type_ptr in + | PointerType (_, {Clang_ast_t.qt_type_ptr}) + | ObjCObjectPointerType (_, {Clang_ast_t.qt_type_ptr}) -> + let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in if Typ.equal typ (get_builtin_objc_type `ObjCClass) then typ else Typ.Tptr (typ, Typ.Pk_pointer) @@ -115,9 +115,9 @@ and sil_type_of_c_type translate_decl tenv c_type = | None -> Typ.Tvoid) | ObjCInterfaceType (_, pointer) -> decl_ptr_to_sil_type translate_decl tenv pointer - | RValueReferenceType (_, type_ptr) - | LValueReferenceType (_, type_ptr) -> - let typ = type_ptr_to_sil_type translate_decl tenv type_ptr in + | RValueReferenceType (_, {Clang_ast_t.qt_type_ptr}) + | LValueReferenceType (_, {Clang_ast_t.qt_type_ptr}) -> + let typ = type_ptr_to_sil_type translate_decl tenv qt_type_ptr in Typ.Tptr (typ, Typ.Pk_reference) | AttributedType (type_info, attr_info) -> sil_type_of_attr_type translate_decl tenv type_info attr_info diff --git a/infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp b/infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp new file mode 100644 index 000000000..063a8ee1a --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp @@ -0,0 +1,60 @@ +/* + * 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. + */ + +#include + +struct lol { + int f; +}; + +typedef const std::shared_ptr& const_lol; + +void skip_const(const std::shared_ptr& foo); +void skip_const2(int x, const std::shared_ptr& foo, int y, bool z); +void skip_no_const(std::shared_ptr& foo); +void skip_typedef(const_lol foo); + +void test_pointer(const std::shared_ptr& foo) { + // create a case split where one post-condition has foo == null + if (foo) { + foo->f = 4; + } +} + +void skip_then_split_case() { + auto foo = std::make_shared(); + skip_no_const(foo); // Infer havocs foo here since it's not const + test_pointer( + foo); // this call creates a case split, foo can be null in one branch + foo->f = 12; // error +} + +void const_skip_then_split_case() { + auto foo = std::make_shared(); + skip_const(foo); // Infer shouldn't havoc foo here since it's const... + test_pointer(foo); /* ...so foo cannot be null here, even if there is an + explicit null post... */ + foo->f = 12; // no error +} + +// same as above but make sure infer pinpoints the correct const argument +void const_skip2_then_split_case() { + auto foo = std::make_shared(); + skip_const2(0, foo, 0, 0); + test_pointer(foo); + foo->f = 12; // no error +} + +// same as above but hide the type under a typedef +void typedef_skip_then_split_case() { + auto foo = std::make_shared(); + skip_typedef(foo); + test_pointer(foo); + foo->f = 12; // no error +} diff --git a/infer/tests/endtoend/cpp/infer/SkipFunctionWithConstFormalsTest.java b/infer/tests/endtoend/cpp/infer/SkipFunctionWithConstFormalsTest.java new file mode 100644 index 000000000..c6e1dfc68 --- /dev/null +++ b/infer/tests/endtoend/cpp/infer/SkipFunctionWithConstFormalsTest.java @@ -0,0 +1,68 @@ +/* + * 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. + */ + +package endtoend.cpp.infer; + +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 SkipFunctionWithConstFormalsTest { + + public static final String FILE = + "infer/tests/codetoanalyze/cpp/errors/npe/skip_function_with_const_formals.cpp"; + + private static ImmutableList inferCmd; + + public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE"; + + @ClassRule + public static DebuggableTemporaryFolder folder = + new DebuggableTemporaryFolder(); + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferCmd = InferRunner.createCPPInferCommand(folder, FILE); + } + + @Test + public void whenInferRunsNullDerefFunctionsErrorIsFound() + throws InterruptedException, IOException, InferException { + String[] procedures = { + "skip_then_split_case", + "typedef_skip_then_split_case", // Infer should not report there + // but currently we don't look + // at const qualifiers + // underneath typedef's + }; + InferResults inferResults = InferRunner.runInferCPP(inferCmd); + assertThat( + "Results should contain null dereference", + inferResults, + containsExactly( + NULL_DEREFERENCE, + FILE, + procedures + ) + ); + } +}