pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

move remove_tmps and add_abstraction steps into the pre-analysis

Browse Source 
Summary: public Like the pre-analysis, these should be called for every CFG. This is a stepping stone toward getting rid of remove_tmps and making it part of the liveness analysis.

Reviewed By: jvillard

Differential Revision: D3059021

fb-gh-sync-id: 3a8d818
shipit-source-id: 3a8d818
master
Sam Blackshear 9 years ago committed by Facebook Github Bot 1
parent dec843f5f5
commit f9bffe1e87
7 changed files with 42 additions and 51 deletions
Show Stats Download Patch File Download Diff File

37
infer/src/backend/cfg.ml
Unescape View File

@ -817,43 +817,6 @@ let get_priority_procnames cfg =
let set_procname_priority cfg pname =
cfg.Node.priority_set <- Procname.Set.add pname cfg.Node.priority_set
(** add instructions to remove temporaries *)
let add_removetemps_instructions cfg =
let all_nodes = Node.get_all_nodes cfg in
let do_node node =
let loc = Node.get_last_loc node in
let temps = Node.get_temps node in
if temps != [] then Node.append_instrs_temps node [Sil.Remove_temps (temps, loc)] [] in
IList.iter do_node all_nodes
(** add instructions to perform abstraction *)
let add_abstraction_instructions cfg =
let converging_node node = (* true if there is a succ node s.t.: it is an exit node, or the succ of >1 nodes *)
let is_exit node = match Node.get_kind node with
| Node.Exit_node _ -> true
| _ -> false in
let succ_nodes = Node.get_succs node in
if IList.exists is_exit succ_nodes then true
else match succ_nodes with
| [] -> false
| [h] -> IList.length (Node.get_preds h) > 1
| _ -> false in
let node_requires_abstraction node =
match Node.get_kind node with
| Node.Start_node _
| Node.Join_node ->
false
| Node.Exit_node _
| Node.Stmt_node _
| Node.Prune_node _
| Node.Skip_node _ ->
converging_node node in
let all_nodes = Node.get_all_nodes cfg in
let do_node node =
let loc = Node.get_last_loc node in
if node_requires_abstraction node then Node.append_instrs_temps node [Sil.Abstract loc] [] in
IList.iter do_node all_nodes
let get_name_of_local (curr_f : Procdesc.t) (x, _) =
Sil.mk_pvar x (Procdesc.get_proc_name curr_f)

6
infer/src/backend/cfg.mli
Unescape View File

@ -291,12 +291,6 @@ val get_priority_procnames : cfg -> Procname.Set.t
(** set the function names whose address has been taken in this file *)
val set_procname_priority : cfg -> Procname.t -> unit
(** add instructions to remove temporaries *)
val add_removetemps_instructions : cfg -> unit
(** add instructions to perform abstraction *)
val add_abstraction_instructions : cfg -> unit
(** remove the return variable from the prop *)
val remove_ret : Procdesc.t -> Prop.normal Prop.t -> Prop.normal Prop.t

42
infer/src/backend/preanal.ml
Unescape View File

@ -421,12 +421,54 @@ let add_dispatch_calls cfg cg tenv f_translate_typ_opt =
Cfg.Procdesc.iter_nodes (node_add_dispatch_calls pname) pdesc in
Cfg.iter_proc_desc cfg proc_add_dispach_calls
(** add instructions to perform abstraction *)
let add_abstraction_instructions cfg =
let open Cfg in
(* true if there is a succ node s.t.: it is an exit node, or the succ of >1 nodes *)
let converging_node node =
let is_exit node = match Node.get_kind node with
| Node.Exit_node _ -> true
| _ -> false in
let succ_nodes = Node.get_succs node in
if IList.exists is_exit succ_nodes then true
else match succ_nodes with
| [] -> false
| [h] -> IList.length (Node.get_preds h) > 1
| _ -> false in
let node_requires_abstraction node =
match Node.get_kind node with
| Node.Start_node _
| Node.Join_node ->
false
| Node.Exit_node _
| Node.Stmt_node _
| Node.Prune_node _
| Node.Skip_node _ ->
converging_node node in
let all_nodes = Node.get_all_nodes cfg in
let do_node node =
let loc = Node.get_last_loc node in
if node_requires_abstraction node then Node.append_instrs_temps node [Sil.Abstract loc] [] in
IList.iter do_node all_nodes
(** add instructions to remove temporaries *)
let add_removetemps_instructions cfg =
let open Cfg in
let all_nodes = Node.get_all_nodes cfg in
let do_node node =
let loc = Node.get_last_loc node in
let temps = Node.get_temps node in
if temps != [] then Node.append_instrs_temps node [Sil.Remove_temps (temps, loc)] [] in
IList.iter do_node all_nodes
let doit ?(f_translate_typ=None) cfg cg tenv =
add_removetemps_instructions cfg;
AllPreds.mk_table cfg;
Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg);
AllPreds.clear_table ();
if !Config.curr_language = Config.Java
then add_dispatch_calls cfg cg tenv f_translate_typ;
add_abstraction_instructions cfg;
(*
Printing function useful for debugging

2
infer/src/clang/cFrontend.ml
Unescape View File

@ -54,9 +54,7 @@ let do_source_file source_file ast =
let tenv_file = DB.source_dir_get_internal_file source_dir ".tenv" in
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
Cfg.add_removetemps_instructions cfg;
Preanal.doit cfg call_graph tenv;
Cfg.add_abstraction_instructions cfg;
Cg.store_to_file cg_file call_graph;
Cfg.store_cfg_to_file cfg_file true cfg;
(*Logging.out "Tenv %a@." Sil.pp_tenv tenv;*)

2
infer/src/harness/inhabit.ml
Unescape View File

@ -291,8 +291,6 @@ let setup_harness_cfg harness_name env source_dir cg =
Cfg.Node.add_locals_ret_declaration start_node [];
Cfg.Node.set_succs_exn start_node [harness_node] [exit_node];
Cfg.Node.set_succs_exn harness_node [exit_node] [exit_node];
Cfg.add_removetemps_instructions harness_cfg;
Cfg.add_abstraction_instructions harness_cfg;
add_harness_to_cg harness_name harness_node cg;
(* save out the cg and cfg so that they will be accessible in the next phase of the analysis *)
Cg.store_to_file cg_file cg;

2
infer/src/java/jMain.ml
Unescape View File

@ -103,9 +103,7 @@ let store_icfg tenv cg cfg program =
begin
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
Cfg.add_removetemps_instructions cfg;
Preanal.doit ~f_translate_typ:(Some f_translate_typ) cfg cg tenv;
Cfg.add_abstraction_instructions cfg;
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file cfg_file true cfg;
if !JConfig.debug_mode then

2
infer/src/llvm/lMain.ml
Unescape View File

@ -48,9 +48,7 @@ let store_icfg tenv cg cfg =
let get_internal_file = DB.source_dir_get_internal_file source_dir in
let cg_file = get_internal_file ".cg" in
let cfg_file = get_internal_file ".cfg" in
Cfg.add_removetemps_instructions cfg;
Preanal.doit cfg cg tenv;
Cfg.add_abstraction_instructions cfg;
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file cfg_file true cfg;
if !LConfig.debug_mode then

Write Preview
Loading…
Cancel
Save