|
|
@ -124,11 +124,9 @@ module BoundMap = struct
|
|
|
|
type t = BasicCost.astate Node.IdMap.t
|
|
|
|
type t = BasicCost.astate Node.IdMap.t
|
|
|
|
|
|
|
|
|
|
|
|
let print_upper_bound_map bound_map =
|
|
|
|
let print_upper_bound_map bound_map =
|
|
|
|
L.(debug Analysis Medium) "@\n\n******* Bound Map ITV **** @\n" ;
|
|
|
|
L.(debug Analysis Medium)
|
|
|
|
Node.IdMap.iter
|
|
|
|
"@\n\n******* Bound Map : [node -> bound] ITV **** @\n %a @\n"
|
|
|
|
(fun nid b ->
|
|
|
|
(Node.IdMap.pp ~pp_value:BasicCost.pp)
|
|
|
|
L.(debug Analysis Medium) "@\n node: %a --> bound = %a @\n" Node.pp_id nid BasicCost.pp b
|
|
|
|
|
|
|
|
)
|
|
|
|
|
|
|
|
bound_map ;
|
|
|
|
bound_map ;
|
|
|
|
L.(debug Analysis Medium) "@\n******* END Bound Map ITV **** @\n\n"
|
|
|
|
L.(debug Analysis Medium) "@\n******* END Bound Map ITV **** @\n\n"
|
|
|
|
|
|
|
|
|
|
|
@ -987,7 +985,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t =
|
|
|
|
(* computes reaching defs: node -> (var -> node set) *)
|
|
|
|
(* computes reaching defs: node -> (var -> node set) *)
|
|
|
|
let reaching_defs_invariant_map =
|
|
|
|
let reaching_defs_invariant_map =
|
|
|
|
ReachingDefs.Analyzer.exec_cfg node_cfg proc_data ~initial:ReachingDefs.ReachingDefsMap.empty
|
|
|
|
ReachingDefs.Analyzer.exec_cfg node_cfg proc_data ~initial:ReachingDefs.ReachingDefsMap.empty
|
|
|
|
~debug:true
|
|
|
|
~debug:false
|
|
|
|
in
|
|
|
|
in
|
|
|
|
(* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *)
|
|
|
|
(* collect all prune nodes that occur in loop guards, needed for ControlDepAnalyzer *)
|
|
|
|
let control_maps, loop_head_to_loop_nodes = Loop_control.get_control_maps node_cfg in
|
|
|
|
let control_maps, loop_head_to_loop_nodes = Loop_control.get_control_maps node_cfg in
|
|
|
@ -995,14 +993,14 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t =
|
|
|
|
let control_dep_invariant_map =
|
|
|
|
let control_dep_invariant_map =
|
|
|
|
let proc_data = ProcData.make proc_desc tenv control_maps in
|
|
|
|
let proc_data = ProcData.make proc_desc tenv control_maps in
|
|
|
|
Control.ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:Control.ControlDepSet.empty
|
|
|
|
Control.ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:Control.ControlDepSet.empty
|
|
|
|
~debug:true
|
|
|
|
~debug:false
|
|
|
|
in
|
|
|
|
in
|
|
|
|
let instr_cfg = InstrCFG.from_pdesc proc_desc in
|
|
|
|
let instr_cfg = InstrCFG.from_pdesc proc_desc in
|
|
|
|
let invariant_map_NodesBasicCost =
|
|
|
|
let invariant_map_NodesBasicCost =
|
|
|
|
let proc_data = ProcData.make proc_desc tenv inferbo_invariant_map in
|
|
|
|
let proc_data = ProcData.make proc_desc tenv inferbo_invariant_map in
|
|
|
|
(*compute_WCET cfg invariant_map min_trees in *)
|
|
|
|
(*compute_WCET cfg invariant_map min_trees in *)
|
|
|
|
AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.empty
|
|
|
|
AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.empty
|
|
|
|
~debug:true
|
|
|
|
~debug:false
|
|
|
|
in
|
|
|
|
in
|
|
|
|
(* compute loop invariant map for control var analysis *)
|
|
|
|
(* compute loop invariant map for control var analysis *)
|
|
|
|
let loop_inv_map =
|
|
|
|
let loop_inv_map =
|
|
|
@ -1049,7 +1047,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t =
|
|
|
|
AnalyzerWCET.compute_post
|
|
|
|
AnalyzerWCET.compute_post
|
|
|
|
(ProcData.make proc_desc tenv
|
|
|
|
(ProcData.make proc_desc tenv
|
|
|
|
{basic_cost_map= invariant_map_NodesBasicCost; get_node_nb_exec; summary})
|
|
|
|
{basic_cost_map= invariant_map_NodesBasicCost; get_node_nb_exec; summary})
|
|
|
|
~debug:true ~initial:initWCET
|
|
|
|
~debug:false ~initial:initWCET
|
|
|
|
with
|
|
|
|
with
|
|
|
|
| Some (exit_cost, _) ->
|
|
|
|
| Some (exit_cost, _) ->
|
|
|
|
L.internal_error
|
|
|
|
L.internal_error
|
|
|
|