@ -624,19 +624,28 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Typ.Procna
(* * Resolve the name of the procedure to call based on the type of the arguments *)
let resolve_pname tenv prop args pname call_flags : Typ . Procname . t =
let resolve_pname ~ caller_pdesc tenv prop args pname call_flags : Typ . Procname . t =
let resolve_from_args resolved_pname args =
let resolved_parameters = Typ . Procname . get_parameters resolved_pname in
let resolved_params =
List . fold2_exn
~ f : ( fun accu ( arg_exp , _ ) name ->
match resolve_typename prop arg_exp with
| Some class_name ->
Typ . Procname . parameter_of_name resolved_pname class_name :: accu
| None ->
name :: accu )
~ init : [] args
( Typ . Procname . get_parameters resolved_pname )
| > List . rev
try
List . fold2_exn
~ f : ( fun accu ( arg_exp , _ ) name ->
match resolve_typename prop arg_exp with
| Some class_name ->
Typ . Procname . parameter_of_name resolved_pname class_name :: accu
| None ->
name :: accu )
~ init : [] args resolved_parameters
| > List . rev
with Invalid_argument _ ->
let loc = ( Procdesc . get_attributes caller_pdesc ) . loc in
let file = loc . Location . file in
L . internal_error
" Call mismatch: method %a has %i paramters but is called with %i arguments, in %a, %a@. "
Typ . Procname . pp pname ( List . length resolved_parameters ) ( List . length args ) SourceFile . pp
file Location . pp loc ;
raise Procdesc . UnmatchedParameters
in
Typ . Procname . replace_parameters resolved_params resolved_pname
in
@ -661,22 +670,44 @@ let resolve_pname tenv prop args pname call_flags : Typ.Procname.t =
| args when match_parameters args (* Static call *) ->
( pname , args )
| args ->
L . ( die InternalError )
" Call mismatch: method %a has %i paramters but is called with %i arguments@. "
Typ . Procname . pp pname ( List . length parameters ) ( List . length args )
let loc = ( Procdesc . get_attributes caller_pdesc ) . loc in
let file = loc . Location . file in
L . internal_error
" Call mismatch: method %a has %i paramters but is called with %i arguments, in %a, %a@. "
Typ . Procname . pp pname ( List . length parameters ) ( List . length args ) SourceFile . pp file
Location . pp loc ;
raise Procdesc . UnmatchedParameters
in
resolve_from_args resolved_pname other_args
let resolve_args prop args =
List . map
~ f : ( fun ( ( arg_exp , arg_typ ) as arg ) ->
match ( resolve_typename prop arg_exp , arg_typ . Typ . desc ) with
| Some class_name , Tptr ( ( { desc = Tstruct typename } as inner_typ ) , p ) ->
let resolved_arg_typ =
if Typ . Name . equal class_name typename then arg_typ
else
let struct_typ = { inner_typ with desc = Tstruct class_name } in
( { arg_typ with desc = Tptr ( struct_typ , p ) } : Typ . t )
in
( arg_exp , resolved_arg_typ )
| _ ->
arg )
args
(* * Resolve the procedure name and run the analysis of the resolved procedure
if not already analyzed * )
let resolve_and_analyze tenv ~ caller_pdesc prop args callee_proc_name call_flags
: Typ . Procname . t * Summary . t option =
let resolve_and_analyze tenv ~ caller_pdesc ? ( has_clang_model = false ) prop args callee_proc_name
call_flags : Typ . Procname . t * ( Procdesc . t option * Summary . t option ) =
(* TODO ( #15748878 ) : Fix conflict with method overloading by encoding in the procedure name
whether the method is defined or generated by the specialization * )
let analyze_ondemand resolved_pname : Summary . t option =
let analyze_ondemand resolved_pname : Procdesc. t option * Summary. t option =
if Typ . Procname . equal resolved_pname callee_proc_name then
Ondemand . analyze_proc_name ~ caller_pdesc callee_proc_name
( Ondemand . get_proc_desc callee_proc_name
, Ondemand . analyze_proc_name ~ caller_pdesc callee_proc_name )
else
(* Create the type sprecialized procedure description and analyze it directly *)
let analyze specialized_pdesc = Ondemand . analyze_proc_desc ~ caller_pdesc specialized_pdesc in
@ -685,14 +716,29 @@ let resolve_and_analyze tenv ~caller_pdesc prop args callee_proc_name call_flags
| Some resolved_proc_desc ->
Some resolved_proc_desc
| None ->
let procdesc_opt =
(* If it is a model, we aim to get the procdesc stored in a summary rather than the
( empty ) procdesc stored in the caller's cfg . * )
if has_clang_model then
match Summary . get callee_proc_name with
| Some summary ->
Some ( Summary . get_proc_desc summary )
| None ->
Ondemand . get_proc_desc callee_proc_name
else Ondemand . get_proc_desc callee_proc_name
in
Option . map
~ f : ( fun callee_proc_desc ->
Procdesc . specialize_types callee_proc_desc resolved_pname args )
( Ondemand . get_proc_desc callee_proc_name )
(* It is possible that the types of the arguments are not as precise as the type of the objects
in the heap , so we should update them to get the best results . * )
let resolved_args = resolve_args prop args in
Procdesc . specialize_types ~ has_clang_model callee_proc_desc resolved_pname
resolved_args )
procdesc_opt
in
Option . bind resolved_proc_desc_option ~ f : analyze
( resolved_proc_desc_option , Option . bind resolved_proc_desc_option ~ f : analyze )
in
let resolved_pname = resolve_pname tenv prop args callee_proc_name call_flags in
let resolved_pname = resolve_pname ~ caller_pdesc tenv prop args callee_proc_name call_flags in
( resolved_pname , analyze_ondemand resolved_pname )
@ -1049,6 +1095,64 @@ let execute_store ?(report_deref_errors= true) pname pdesc tenv lhs_exp typ rhs_
with Rearrange . ARRAY_ACCESS -> if Int . equal Config . array_level 0 then assert false else [ prop_ ]
let is_variadic_procname callee_pname =
Option . value_map
( Ondemand . get_proc_desc callee_pname )
~ f : ( fun proc_desc -> ( Procdesc . get_attributes proc_desc ) . ProcAttributes . is_variadic )
~ default : false
let resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params callee_pname
call_flags =
let resolved_pname =
match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with
| resolved_pname :: _ ->
resolved_pname
| [] ->
callee_pname
in
let resolved_summary_opt =
Ondemand . analyze_proc_name ~ caller_pdesc : current_pdesc resolved_pname
in
( resolved_pname , ( Ondemand . get_proc_desc resolved_pname , resolved_summary_opt ) )
let resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_pname call_flags =
if
Config . dynamic_dispatch && not ( is_variadic_procname callee_pname )
&& Typ . Procname . is_objc_method callee_pname
(* to be extended to other methods *)
then
try
let has_clang_model = Summary . has_model callee_pname in
let resolved_pname , ( resolved_pdesc_opt , resolved_summary_opt ) =
resolve_and_analyze tenv ~ caller_pdesc : current_pdesc ~ has_clang_model prop_r
n_actual_params callee_pname call_flags
in
(* It could be useful to specialize a model, but also it could cause a failure,
because we don't have the correct fields in the tenv .
In that case , default to the non - specialized spec for the model . * )
let clang_model_specialized_failure =
match resolved_summary_opt with
| Some summary when has_clang_model ->
List . is_empty ( Tabulation . get_specs_from_payload summary )
| None ->
true
| _ ->
false
in
if clang_model_specialized_failure then
resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params
callee_pname call_flags
else ( resolved_pname , ( resolved_pdesc_opt , resolved_summary_opt ) )
with Procdesc . UnmatchedParameters ->
resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params
callee_pname call_flags
else
resolve_and_analyze_no_dynamic_dispatch current_pdesc tenv prop_r n_actual_params callee_pname
call_flags
(* * Execute [instr] with a symbolic heap [prop]. *)
let rec sym_exec exe_env tenv current_pdesc instr_ ( prop_ : Prop . normal Prop . t ) path
: ( Prop . normal Prop . t * Paths . Path . t ) list =
@ -1180,7 +1284,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
skip_call ~ reason norm_prop path skipped_pname ret_annots loc ret_id_typ ret_type
norm_args
in
let resolved_pname , resolved_summary_opt =
let resolved_pname , ( _ , resolved_summary_opt ) =
resolve_and_analyze tenv ~ caller_pdesc : current_pdesc norm_prop norm_args callee_pname
call_flags
in
@ -1229,18 +1333,11 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
| _ ->
(* Generic fun call with known name *)
let prop_r , n_actual_params = normalize_params tenv current_pname prop_ actual_params in
let resolved_pname =
match resolve_virtual_pname tenv prop_r n_actual_params callee_pname call_flags with
| resolved_pname :: _ ->
resolved_pname
| [] ->
callee_pname
in
(* method with block parameters *)
let with_block_parameters_summary_opt =
if call_flags . CallFlags . cf_with_block_parameters then
SymExecBlocks . resolve_method_with_block_args_and_analyze ~ caller_pdesc : current_pdesc
resolved _pname actual_params
callee_pname actual_params
else None
in
match with_block_parameters_summary_opt with
@ -1250,22 +1347,24 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
in
Logging . d_strln " Calling method specialized with blocks... " ;
proc_call exe_env resolved_summary
( call_args prop_r resolved _pname n_extended_actual_params ret_id_typ loc )
( call_args prop_r callee _pname n_extended_actual_params ret_id_typ loc )
| None ->
(* Generic fun call with known name *)
let resolved_summary_opt =
Ondemand . analyze_proc_name ~ caller_pdesc : current_pdesc resolved_pname
let resolved_pname , ( resolved_pdesc_opt , resolved_summary_opt ) =
resolve_and_analyze_clang current_pdesc tenv prop_r n_actual_params callee_pname
call_flags
in
let callee_pdesc_opt = Ondemand . get_proc_desc resolved_pname in
Logging . d_strln ( " Original callee " ^ Typ . Procname . to_unique_id callee_pname ) ;
Logging . d_strln ( " Resolved callee " ^ Typ . Procname . to_unique_id resolved_pname ) ;
let sentinel_result =
if Language . curr_language_is Clang then
check_variadic_sentinel_if_present
( call_args prop_r callee _pname actual_params ret_id_typ loc )
( call_args prop_r resolved _pname actual_params ret_id_typ loc )
else [ ( prop_r , path ) ]
in
let do_call ( prop , path ) =
let callee_desc =
match ( resolved_summary_opt , callee _pdesc_opt) with
match ( resolved_summary_opt , resolved _pdesc_opt) with
| Some summary , _ ->
` Summary summary
| None , Some pdesc ->
@ -1286,21 +1385,23 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_: Prop.normal Prop.t) p
| None ->
load_ret_annots resolved_pname
in
match callee _pdesc_opt with
| Some callee _pdesc
match resolved _pdesc_opt with
| Some resolved _pdesc
-> (
let attrs = Procdesc . get_attributes callee _pdesc in
let attrs = Procdesc . get_attributes resolved _pdesc in
let ret_type = attrs . ProcAttributes . ret_type in
let model_as_malloc = Objc_models . is_malloc_model ret_type callee_pname in
let model_as_malloc =
Objc_models . is_malloc_model ret_type resolved_pname
in
match ( attrs . ProcAttributes . objc_accessor , model_as_malloc ) with
| Some objc_accessor , _ ->
(* If it's an ObjC getter or setter, call the builtin rather than skipping *)
handle_objc_instance_method_call n_actual_params n_actual_params prop
tenv ( fst ret_id_typ ) current_pdesc callee _pname loc path
( sym_exec_objc_accessor callee _pname objc_accessor ret_type )
tenv ( fst ret_id_typ ) current_pdesc resolved _pname loc path
( sym_exec_objc_accessor resolved _pname objc_accessor ret_type )
| None , true ->
(* If it's an alloc model, call alloc rather than skipping *)
sym_exec_alloc_model exe_env callee _pname ret_type tenv ret_id_typ
sym_exec_alloc_model exe_env resolved _pname ret_type tenv ret_id_typ
current_pdesc loc prop path
| None , false ->
let is_objc_instance_method =