@ -11,11 +11,12 @@
open ! IStd
open ! IStd
(* * mutate the cfg/cg to add dynamic dispatch handling *)
(* * mutate the cfg/cg to add dynamic dispatch handling *)
let add_dispatch_calls pdesc cg tenv ~ handle_dynamic_dispatch =
let add_dispatch_calls pdesc cg tenv policy =
let sound_dynamic_dispatch = policy = ` Sound in
let node_add_dispatch_calls caller_pname node =
let node_add_dispatch_calls caller_pname node =
let call_flags_is_dispatch call_flags =
let call_flags_is_dispatch call_flags =
(* if sound dispatch is turned off, only consider dispatch for interface calls *)
(* if sound dispatch is turned off, only consider dispatch for interface calls *)
( handle _dynamic_dispatch && call_flags . CallFlags . cf_virtual ) | |
( sound _dynamic_dispatch && call_flags . CallFlags . cf_virtual ) | |
call_flags . CallFlags . cf_interface in
call_flags . CallFlags . cf_interface in
let instr_is_dispatch_call = function
let instr_is_dispatch_call = function
| Sil . Call ( _ , _ , _ , _ , call_flags ) -> call_flags_is_dispatch call_flags
| Sil . Call ( _ , _ , _ , _ , call_flags ) -> call_flags_is_dispatch call_flags
@ -39,7 +40,7 @@ let add_dispatch_calls pdesc cg tenv ~handle_dynamic_dispatch =
( match sorted_overrides with
( match sorted_overrides with
| ( ( _ , target_pname ) :: _ ) as all_targets ->
| ( ( _ , target_pname ) :: _ ) as all_targets ->
let targets_to_add =
let targets_to_add =
if handle _dynamic_dispatch then
if sound _dynamic_dispatch then
IList . map snd all_targets
IList . map snd all_targets
else
else
(* if sound dispatch is turned off, consider only the first target. we do this
(* if sound dispatch is turned off, consider only the first target. we do this
@ -302,19 +303,17 @@ let do_copy_propagation pdesc tenv =
let do_liveness pdesc tenv =
let do_liveness pdesc tenv =
let liveness_proc_cfg = BackwardCfg . from_pdesc pdesc in
let liveness_proc_cfg = BackwardCfg . from_pdesc pdesc in
LivenessAnalysis . exec_cfg liveness_proc_cfg ( ProcData . make_default pdesc tenv )
let liveness_inv_map =
LivenessAnalysis . exec_cfg liveness_proc_cfg ( ProcData . make_default pdesc tenv ) in
if Config . copy_propagation then do_copy_propagation pdesc tenv ;
add_nullify_instrs pdesc tenv liveness_inv_map ;
Procdesc . signal_did_preanalysis pdesc
let doit ? ( handle_dynamic_dispatch = ( Config . dynamic_dispatch = ` Sound ) ) pdesc cg tenv =
let do_abstraction pdesc =
if not ( Procdesc . did_preanalysis pdesc )
add_abstraction_instructions pdesc ;
then
Procdesc . signal_did_preanalysis pdesc
begin
Procdesc . signal_did_preanalysis pdesc ;
let do_dynamic_dispatch pdesc cg tenv policy =
if Config . copy_propagation then do_copy_propagation pdesc tenv ;
if policy < > ` Lazy
let liveness_inv_map = do_liveness pdesc tenv in
then add_dispatch_calls pdesc cg tenv policy ;
if Config . dynamic_dispatch < > ` Lazy && Config . copy_propagation
Procdesc . signal_did_preanalysis pdesc
then remove_dead_frontend_stores pdesc liveness_inv_map ;
add_nullify_instrs pdesc tenv liveness_inv_map ;
if Config . dynamic_dispatch < > ` Lazy
then add_dispatch_calls ~ handle_dynamic_dispatch pdesc cg tenv ;
add_abstraction_instructions pdesc ;
end