From ac6ef1d9f6f9fca73fce3b39a3aee83415da50f1 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 14 Apr 2016 15:24:57 -0700 Subject: [PATCH] kill Sil.Goto Summary:This wasn't used anywhere. Frontends that wish to do something like goto can just set the targets of the goto as successors of the current node, no need for a special instruction to do that. Reviewed By: sblackshear Differential Revision: D3179826 fb-gh-sync-id: 572a6f2 fbshipit-source-id: 572a6f2 --- infer/src/IR/sil.ml | 23 ++--------------------- infer/src/IR/sil.mli | 3 --- infer/src/backend/interproc.ml | 8 ++------ infer/src/backend/preanal.ml | 2 -- infer/src/backend/state.ml | 18 +++--------------- infer/src/backend/state.mli | 10 ++-------- infer/src/backend/symExec.ml | 12 ------------ infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/checkers.ml | 3 +-- infer/src/checkers/copyPropagation.ml | 2 +- infer/src/checkers/liveness.ml | 2 +- infer/src/eradicate/typeCheck.ml | 2 -- 12 files changed, 13 insertions(+), 74 deletions(-) diff --git a/infer/src/IR/sil.ml b/infer/src/IR/sil.ml index 838769e20..af6d03f54 100644 --- a/infer/src/IR/sil.ml +++ b/infer/src/IR/sil.ml @@ -752,13 +752,10 @@ type instr = | Remove_temps of Ident.t list * Location.t (** remove temporaries *) | Stackop of stackop * Location.t (** operation on the stack of propsets *) | Declare_locals of (Pvar.t * typ) list * Location.t (** declare local variables *) - (** jump to a specific cfg node, - assuming all the possible target nodes are successors of the current node *) - | Goto_node of exp * Location.t (** Check if an instruction is auxiliary, or if it comes from source instructions. *) let instr_is_auxiliary = function - | Letderef _ | Set _ | Prune _ | Call _ | Goto_node _ -> + | Letderef _ | Set _ | Prune _ | Call _ -> false | Nullify _ | Abstract _ | Remove_temps _ | Stackop _ | Declare_locals _ -> true @@ -2073,8 +2070,7 @@ let instr_get_loc = function | Abstract loc | Remove_temps (_, loc) | Stackop (_, loc) - | Declare_locals (_, loc) - | Goto_node (_, loc) -> + | Declare_locals (_, loc) -> loc (** get the expressions occurring in the instruction *) @@ -2097,8 +2093,6 @@ let instr_get_exps = function [] | Declare_locals _ -> [] - | Goto_node (e, _) -> - [e] (** Pretty print call flags *) let pp_call_flags f cf = @@ -2147,8 +2141,6 @@ let pp_instr pe0 f instr = | Declare_locals (ptl, loc) -> let pp_typ fmt (pvar, _) = F.fprintf fmt "%a" (Pvar.pp pe) pvar in F.fprintf f "DECLARE_LOCALS(%a); %a" (pp_comma_seq pp_typ) ptl Location.pp loc - | Goto_node (e, loc) -> - F.fprintf f "Goto_node %a %a" (pp_exp pe) e Location.pp loc ); color_post_wrapper changed pe0 f @@ -2243,8 +2235,6 @@ let instr_iter_types f instr = match instr with () | Declare_locals (ptl, _) -> IList.iter (fun (_, t) -> typ_iter_types f t) ptl - | Goto_node _ -> - () (** Dump an instruction. *) let d_instr (i: instr) = L.add_print_action (L.PTinstr, Obj.repr i) @@ -3430,8 +3420,6 @@ let instr_sub (subst: subst) instr = | Declare_locals (ptl, loc) -> let pt_s (pv, t) = (pv, typ_s t) in Declare_locals (IList.map pt_s ptl, loc) - | Goto_node (e, loc) -> - Goto_node (exp_s e, loc) let call_flags_compare cflag1 cflag2 = bool_compare cflag1.cf_virtual cflag2.cf_virtual @@ -3500,11 +3488,6 @@ let instr_compare instr1 instr2 = match instr1, instr2 with let n = IList.compare pt_compare ptl1 ptl2 in if n <> 0 then n else Location.compare loc1 loc2 - | Declare_locals _, _ -> -1 - | _, Declare_locals _ -> 1 - | Goto_node (e1, loc1), Goto_node (e2, loc2) -> - let n = exp_compare e1 e2 in - if n <> 0 then n else Location.compare loc1 loc2 (** compare expressions from different procedures without considering loc's, ident's, and pvar's. the [exp_map] param gives a mapping of names used in the procedure of [e1] to names used in the @@ -3627,8 +3610,6 @@ let instr_compare_structural instr1 instr2 exp_map = (0, exp_map) ptl1 ptl2 - | Goto_node (e1, _), Goto_node (e2, _) -> - exp_compare_structural e1 e2 exp_map | _ -> instr_compare instr1 instr2, exp_map let atom_sub subst = diff --git a/infer/src/IR/sil.mli b/infer/src/IR/sil.mli index 6365f3bb2..587be0dc2 100644 --- a/infer/src/IR/sil.mli +++ b/infer/src/IR/sil.mli @@ -407,9 +407,6 @@ type instr = | Remove_temps of Ident.t list * Location.t (** remove temporaries *) | Stackop of stackop * Location.t (** operation on the stack of propsets *) | Declare_locals of (Pvar.t * typ) list * Location.t (** declare local variables *) - (** jump to a specific cfg node, - assuming all the possible target nodes are successors of the current node *) - | Goto_node of exp * Location.t (** Check if an instruction is auxiliary, or if it comes from source instructions. *) val instr_is_auxiliary : instr -> bool diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 2ac94a460..31bc28826 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -274,13 +274,9 @@ let propagate (** propagate a set of results, including exceptions and divergence *) let propagate_nodes_divergence tenv (pdesc: Cfg.Procdesc.t) (pset: Paths.PathSet.t) - (succ_nodes_: Cfg.node list) (exn_nodes: Cfg.node list) (wl : Worklist.t) = + (succ_nodes: Cfg.node list) (exn_nodes: Cfg.node list) (wl : Worklist.t) = let pname = Cfg.Procdesc.get_proc_name pdesc in let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in - let succ_nodes = match State.get_goto_node () with (* handle Sil.Goto_node target, if any *) - | Some node_id -> - IList.filter (fun n -> Cfg.Node.get_id n = node_id) succ_nodes_ - | None -> succ_nodes_ in if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then begin Errdesc.warning_err (State.get_loc ()) "Propagating Divergence@."; @@ -581,7 +577,7 @@ let forward_tabulate tenv wl = L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths); L.d_increase_indent 1; - State.reset_diverging_states_goto_node (); + State.reset_diverging_states_node (); let pset = do_symbolic_execution (handle_exn curr_node) tenv curr_node prop path in L.d_decrease_indent 1; L.d_ln(); diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 6a860d9f2..142ff1ef2 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -81,7 +81,6 @@ and use_instr cfg (pdesc: Cfg.Procdesc.t) (instr: Sil.instr) acc = | Sil.Call (_, _, etl, _, _) -> use_etl cfg pdesc etl acc | Sil.Nullify _ -> acc | Sil.Abstract _ | Sil.Remove_temps _ | Sil.Stackop _ | Sil.Declare_locals _ -> acc - | Sil.Goto_node (e, _) -> use_exp cfg pdesc e acc (** variables written in the expression *) let rec def_exp cfg (exp: Sil.exp) acc = @@ -97,7 +96,6 @@ let rec def_instr cfg (instr: Sil.instr) acc = | Sil.Nullify (x, _, _) -> if is_not_function cfg x then Vset.add x acc else acc | Sil.Abstract _ | Sil.Remove_temps _ | Sil.Stackop _ | Sil.Declare_locals _ -> acc - | Sil.Goto_node _ -> acc and def_instrl cfg instrs acc = IList.fold_left (fun acc' i -> def_instr cfg i acc') acc instrs diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 78a7e3333..b2e15f54d 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -40,9 +40,6 @@ type t = { (** Diverging states since the last reset for the procedure *) mutable diverging_states_proc : Paths.PathSet.t; - (** Node target of a Sil.Goto_node instruction *) - mutable goto_node : int option; - (** Last instruction seen *) mutable last_instr : Sil.instr option; @@ -66,7 +63,6 @@ let initial () = { const_map = (fun _ _ -> None); diverging_states_node = Paths.PathSet.empty; diverging_states_proc = Paths.PathSet.empty; - goto_node = None; last_instr = None; last_node = Cfg.Node.dummy (); last_path = None; @@ -88,9 +84,8 @@ let save_state () = let restore_state st = gs := st -let reset_diverging_states_goto_node () = - !gs.diverging_states_node <- Paths.PathSet.empty; - !gs.goto_node <- None +let reset_diverging_states_node () = + !gs.diverging_states_node <- Paths.PathSet.empty let reset () = gs := initial () @@ -112,12 +107,6 @@ let get_diverging_states_node () = let get_diverging_states_proc () = !gs.diverging_states_proc -let set_goto_node node_id = - !gs.goto_node <- Some node_id - -let get_goto_node () = - !gs.goto_node - let get_instr () = !gs.last_instr @@ -144,8 +133,7 @@ let node_simple_key node = | Sil.Abstract _ -> add_key 6 | Sil.Remove_temps _ -> add_key 7 | Sil.Stackop _ -> add_key 8 - | Sil.Declare_locals _ -> add_key 9 - | Sil.Goto_node _ -> add_key 10 in + | Sil.Declare_locals _ -> add_key 9 in IList.iter do_instr (Cfg.Node.get_instrs node); Hashtbl.hash !key diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli index eb3e21528..ca08e54ed 100644 --- a/infer/src/backend/state.mli +++ b/infer/src/backend/state.mli @@ -29,9 +29,6 @@ val get_diverging_states_node : unit -> Paths.PathSet.t (** Get the diverging states for the procedure *) val get_diverging_states_proc : unit -> Paths.PathSet.t -(** Get the node target of a Sil.Goto_node instruction, if any *) -val get_goto_node : unit -> int option - (** Get update instrumentation for the current loc *) val get_inst_update : Sil.path_pos -> Sil.inst @@ -103,8 +100,8 @@ val process_execution_failures : log_issue -> Procname.t -> unit (** Reset all the global data. *) val reset : unit -> unit -(** Reset the diverging states and goto information for the node *) -val reset_diverging_states_goto_node : unit -> unit +(** Reset the diverging states information for the node *) +val reset_diverging_states_node : unit -> unit (** Restore the old state. *) val restore_state : t -> unit @@ -115,9 +112,6 @@ val save_state : unit -> t (** Set the constant map for the current procedure. *) val set_const_map : const_map -> unit -(** Set the node target of a Sil.Goto_node instruction *) -val set_goto_node : int -> unit - (** Set last instruction seen in symbolic execution *) val set_instr : Sil.instr -> unit diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index a8275bdac..cace1ed2a 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1190,18 +1190,6 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path ret_old_path [prop'] | Sil.Stackop _ -> (* this should be handled at the propset level *) assert false - | Sil.Goto_node (node_e, _) -> - let n_node_e, prop = check_arith_norm_exp current_pname node_e prop_ in - begin - match n_node_e with - | Sil.Const (Sil.Cint i) -> - let node_id = Sil.Int.to_int i in - State.set_goto_node node_id; - [(prop, path)] - | _ -> (* target not known, do nothing as the next nodes - are set to the possible targets by the front-end *) - [(prop, path)] - end and diverge prop path = State.add_diverging_states (Paths.PathSet.from_renamed_list [(prop, path)]); (* diverge *) [] diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 5a8d7fa44..754eedc20 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -42,7 +42,7 @@ module TransferFunctions = struct | _ -> astate_acc in IList.fold_left add_actual_by_ref astate actuals | Sil.Set _ | Letderef _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Stackop _ - | Declare_locals _ | Goto_node _ -> + | Declare_locals _ -> astate end diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index da8e11d37..d4f66f3bf 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -532,8 +532,7 @@ let callback_check_field_access { Callbacks.proc_desc } = | Sil.Abstract _ | Sil.Remove_temps _ | Sil.Stackop _ - | Sil.Declare_locals _ - | Sil.Goto_node _ -> + | Sil.Declare_locals _ -> () in Cfg.Procdesc.iter_instrs do_instr proc_desc diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index 565829374..efb21b044 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -114,7 +114,7 @@ module TransferFunctions = struct (* this should never happen *) assert false | Sil.Set _ | Sil.Prune _ | Sil.Nullify _ | Sil.Abstract _ | Sil.Remove_temps _ - | Sil.Declare_locals _ | Sil.Goto_node _ | Sil.Stackop _ -> + | Sil.Declare_locals _ | Sil.Stackop _ -> (* none of these can assign to program vars or logical vars *) astate end diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 192a37bff..a37900ac8 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -42,7 +42,7 @@ module TransferFunctions = struct | Sil.Set (lhs_exp, _, rhs_exp, _) -> exp_add_live lhs_exp astate |> exp_add_live rhs_exp - | Sil.Prune (exp, _, _, _) | Sil.Goto_node (exp, _) -> + | Sil.Prune (exp, _, _, _) -> exp_add_live exp astate | Sil.Call (ret_ids, call_exp, params, _, _) -> IList.fold_right diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 0a7e5b73e..3ff4ee7db 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -1072,8 +1072,6 @@ let typecheck_instr check_condition node' ncond | Sil.Stackop _ -> typestate - | Sil.Goto_node _ -> - typestate (** Typecheck the instructions in a cfg node. *) let typecheck_node