@ -7,8 +7,7 @@
open ! IStd
module L = Logging
let nid_int n = ( Procdesc . Node . get_id n :> int )
open Control
type edge_type = { source : Procdesc . Node . t ; target : Procdesc . Node . t } [ @@ deriving compare ]
@ -48,7 +47,7 @@ let get_back_edges pdesc =
Visually :
target
target ( loop head )
/|
/ .
/ |
@ -64,12 +63,13 @@ let get_back_edges pdesc =
Often , exit_node is a prune node . * )
let get_exit_nodes_in_loop loop_nodes =
let succs_of_loop_nodes =
Control. GuardNodes. fold
GuardNodes. fold
( fun n acc ->
Procdesc . Node . get_succs n | > Control . GuardNodes . of_list | > Control . GuardNodes . union acc )
loop_nodes Control . GuardNodes . empty
Procdesc . Node . get_succs n
| > List . fold ~ init : acc ~ f : ( fun acc succ -> GuardNodes . add succ acc ) )
loop_nodes GuardNodes . empty
in
Control. GuardNodes. diff succs_of_loop_nodes loop_nodes | > Control . GuardNodes . elements
GuardNodes. diff succs_of_loop_nodes loop_nodes
(* * Starting from the start_nodes, find all the nodes upwards until the target is reached, i.e
@ -79,12 +79,12 @@ let get_all_nodes_upwards_until target start_nodes =
| [] ->
found_nodes
| node :: wl' ->
if Control. GuardNodes. mem node found_nodes then aux found_nodes wl'
if GuardNodes. mem node found_nodes then aux found_nodes wl'
else
let preds = Procdesc . Node . get_preds node in
aux ( Control. GuardNodes. add node found_nodes ) ( List . append preds wl' )
aux ( GuardNodes. add node found_nodes ) ( List . append preds wl' )
in
aux ( Control. GuardNodes. singleton target ) start_nodes
aux ( GuardNodes. singleton target ) start_nodes
let is_prune node =
@ -94,16 +94,14 @@ let is_prune node =
(* * Remove pairs of prune nodes that are for the same condition, i.e. sibling of the same parent.
This is necessary to prevent picking unnecessary control variables in do - while like loops * )
let remove_prune_node_pairs exit_nodes guard_nodes =
let exit_nodes = Control . GuardNodes . of_list exit_nodes in
let except_exit_nodes = Control . GuardNodes . diff guard_nodes exit_nodes in
L . ( debug Analysis Medium ) " Except exit nodes: [%a] \n " Control . GuardNodes . pp except_exit_nodes ;
let except_exit_nodes = GuardNodes . diff guard_nodes exit_nodes in
L . ( debug Analysis Medium ) " Except exit nodes: [%a] \n " GuardNodes . pp except_exit_nodes ;
except_exit_nodes
| > Control. GuardNodes. filter ( fun node ->
| > GuardNodes. filter ( fun node ->
is_prune node
&& Procdesc . Node . get_siblings node | > Sequence . hd
| > Option . value_map ~ default : false ~ f : ( fun sibling ->
not ( Control . GuardNodes . mem sibling except_exit_nodes ) ) )
| > Control . GuardNodes . union exit_nodes
| > Option . exists ~ f : ( fun sibling -> not ( GuardNodes . mem sibling except_exit_nodes ) ) )
| > GuardNodes . union exit_nodes
(* * Since there could be multiple back-edges per loop, collect all source nodes per loop head.
@ -120,63 +118,60 @@ let get_loop_head_to_source_nodes cfg =
set ( i . e . target of the back edges ) loop_head_to_guard_map : loop_head -> guard_nodes and
guard_nodes contains the nodes that may affect the looping behavior , i . e . occur in the guard of
the loop conditional . * )
let get_control_maps pdesc loop_head_to_source_nodes_map =
let nodes = lazy ( Procdesc . get_nodes pdesc ) in
let get_control_maps loop_head_to_loop_nodes =
let acc = ( ExitNodeToLoopHeads . empty , LoopHeadToGuardNodes . empty ) in
let exit_map , loop_head_to_guard_nodes =
Procdesc . NodeMap . fold
( fun loop_head loop_nodes ( exit_map , loop_head_to_guard_nodes ) ->
let exit_nodes = get_exit_nodes_in_loop loop_nodes in
L . ( debug Analysis Medium ) " Exit nodes: [%a] \n " GuardNodes . pp exit_nodes ;
(* find all the prune nodes in the loop guard *)
let guard_prune_nodes =
get_all_nodes_upwards_until loop_head ( GuardNodes . elements exit_nodes )
| > remove_prune_node_pairs exit_nodes
| > GuardNodes . filter is_prune
in
let exit_map' =
GuardNodes . fold
( fun exit_node exit_map_acc ->
ExitNodeToLoopHeads . update exit_node
( function
| Some existing_loop_heads ->
Some ( LoopHeads . add loop_head existing_loop_heads )
| None ->
Some ( LoopHeads . singleton loop_head ) )
exit_map_acc )
exit_nodes exit_map
in
let loop_head_to_guard_nodes' =
LoopHeadToGuardNodes . update loop_head
( function
| Some existing_guard_nodes ->
Some ( GuardNodes . union existing_guard_nodes guard_prune_nodes )
| None ->
Some guard_prune_nodes )
loop_head_to_guard_nodes
in
( exit_map' , loop_head_to_guard_nodes' ) )
loop_head_to_loop_nodes acc
in
{ exit_map ; loop_head_to_guard_nodes }
let get_loop_head_to_loop_nodes loop_head_to_source_nodes_map =
Procdesc . NodeMap . fold
( fun loop_head source_list
( Control . { exit_map ; loop_head_to_guard_nodes } , loop_head_to_loop_nodes ) ->
L . ( debug Analysis Medium )
" Back-edge source list : [%a] --> loop_head: %i \n " ( Pp . comma_seq Procdesc . Node . pp )
source_list ( nid_int loop_head ) ;
( fun loop_head source_list acc ->
let loop_nodes = get_all_nodes_upwards_until loop_head source_list in
let exit_nodes = get_exit_nodes_in_loop loop_nodes in
L . ( debug Analysis Medium ) " Exit nodes: [%a] \n " ( Pp . comma_seq Procdesc . Node . pp ) exit_nodes ;
(* find all the prune nodes in the loop guard *)
let guard_prune_nodes =
get_all_nodes_upwards_until loop_head exit_nodes
| > remove_prune_node_pairs exit_nodes
| > Control . GuardNodes . filter is_prune
in
let exit_map' =
( List . fold_left ~ init : exit_map ~ f : ( fun exit_map_acc exit_node ->
Control . ExitNodeToLoopHeads . update exit_node
( function
| Some existing_loop_heads ->
Some ( Control . LoopHeads . add loop_head existing_loop_heads )
| None ->
Some ( Control . LoopHeads . singleton loop_head ) )
exit_map_acc ) )
exit_nodes
in
let loop_head_to_guard_nodes' =
Control . LoopHeadToGuardNodes . update loop_head
( function
| Some existing_guard_nodes ->
Some ( Control . GuardNodes . union existing_guard_nodes guard_prune_nodes )
| None ->
Some guard_prune_nodes )
loop_head_to_guard_nodes
in
let loop_head_to_loop_nodes' =
LoopInvariant . LoopHeadToLoopNodes . update loop_head
( function
| Some existing_loop_nodes ->
Some ( LoopInvariant . LoopNodes . union existing_loop_nodes loop_nodes )
| None ->
Some loop_nodes )
loop_head_to_loop_nodes
in
let open Control in
( { exit_map = exit_map' ; loop_head_to_guard_nodes = loop_head_to_guard_nodes' ; nodes }
, loop_head_to_loop_nodes' ) )
loop_head_to_source_nodes_map
( Control .
{ exit_map = Control . ExitNodeToLoopHeads . empty
; loop_head_to_guard_nodes = Control . LoopHeadToGuardNodes . empty
; nodes }
, LoopInvariant . LoopHeadToLoopNodes . empty )
let get_loop_control_maps cfg =
let loop_head_to_source_nodes_map = get_loop_head_to_source_nodes cfg in
get_control_maps cfg loop_head_to_source_nodes_map
LoopInvariant . LoopHeadToLoopNodes . update loop_head
( function
| Some existing_loop_nodes ->
Some ( LoopInvariant . LoopNodes . union existing_loop_nodes loop_nodes )
| None ->
Some loop_nodes )
acc )
loop_head_to_source_nodes_map LoopInvariant . LoopHeadToLoopNodes . empty
let get_loop_control_maps loop_head_to_source_nodes_map =
let loop_head_to_loop_nodes = get_loop_head_to_loop_nodes loop_head_to_source_nodes_map in
get_control_maps loop_head_to_loop_nodes