From cbb71c62035e0f636f6fa452d387d59387c906a3 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Tue, 17 Dec 2019 04:26:56 -0800 Subject: [PATCH] [topl] Get number of arguments from property. Summary: It used to recompute the number of arguments during instrumentation, which is unnecessary. Reviewed By: ngorogiannis Differential Revision: D19035492 fbshipit-source-id: 0f58c8ae7 --- infer/src/topl/Topl.ml | 19 ++++--------------- infer/src/topl/ToplMonitor.ml | 10 ++++++---- 2 files changed, 10 insertions(+), 19 deletions(-) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 57d9b3c52..f8aac67be 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -39,14 +39,6 @@ let get_proc_attr proc_name = Option.map ~f:Procdesc.get_attributes (get_proc_desc proc_name) -let max_args = ref 0 - -let get_max_args () = - let instrument_max_args = !max_args in - let automaton_max_args = ToplAutomaton.max_args (Lazy.force automaton) in - Int.max instrument_max_args automaton_max_args - - let get_transitions_count () = ToplAutomaton.tcount (Lazy.force automaton) (** Checks whether the method name and the number of arguments matches the conditions in a @@ -103,18 +95,15 @@ let call_execute loc = [|ToplUtils.topl_call dummy_ret_id Tvoid loc ToplName.execute []|] -(* Side-effect: increases [!max_args] when it sees a call with more arguments. *) let instrument_instruction = function | Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, _call_flags) as i -> let active_transitions = get_active_transitions e_fun arg_ts in if not (Array.exists ~f:(fun x -> x) active_transitions) then [|i|] - else ( - max_args := Int.max !max_args (List.length arg_ts) ; - tt "found %d arguments@\n" (List.length arg_ts) ; + else let i1s = set_transitions loc active_transitions in let i2s = call_save_args loc ret_id ret_typ arg_ts in let i3s = call_execute loc in - Array.concat [[|i|]; i1s; i2s; i3s] ) + Array.concat [[|i|]; i1s; i2s; i3s] | i -> [|i|] @@ -145,7 +134,7 @@ let add_types tenv = let state = (ToplUtils.make_field ToplName.state, Typ.mk (Tint IInt), []) in let retval = (ToplUtils.make_field ToplName.retval, ToplUtils.any_type, []) in let transitions = List.init (get_transitions_count ()) ~f:transition_field in - let saved_args = List.init (get_max_args ()) ~f:saved_arg_field in + let saved_args = List.init (ToplAutomaton.max_args (Lazy.force automaton)) ~f:saved_arg_field in let registers = List.map ~f:register_field (get_registers ()) in List.concat [[retval; state]; transitions; saved_args; registers] in @@ -158,7 +147,7 @@ let instrument tenv procdesc = let f _node = instrument_instruction in tt "instrument@\n" ; let _updated = Procdesc.replace_instrs_by procdesc ~f in - tt "add types %d@\n" !max_args ; add_types tenv ; tt "done@\n" ) + tt "add types@\n" ; add_types tenv ; tt "done@\n" ) (** [lookup_static_var var prop] expects [var] to have the form [Exp.Lfield (obj, fieldname)], and diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml index 40b428875..e00112355 100644 --- a/infer/src/topl/ToplMonitor.ml +++ b/infer/src/topl/ToplMonitor.ml @@ -198,14 +198,16 @@ let gen_maybe_call ret_id : node_generator = let arguments_count proc_name = List.length (Typ.Procname.get_parameters proc_name) -(* NOTE: The order of parameters must correspond to what gets generated by [call_save_args]. *) -let generate_save_args _automaton proc_name = - let n = arguments_count proc_name in +(* NOTE: The order of parameters must correspond to what gets generated by [Topl.call_save_args]. *) +let generate_save_args automaton proc_name = + if arguments_count proc_name < 1 then + L.die InternalError "ToplMonitor: saveArgs() needs at least one argument" ; + let n = Int.min (arguments_count proc_name - 1) (ToplAutomaton.max_args automaton) in let local_var = ToplUtils.local_var proc_name in procedure proc_name (sequence ( assign (ToplUtils.static_var ToplName.retval) (local_var (ToplName.arg 0)) - :: List.init (n - 1) ~f:(fun i -> + :: List.init n ~f:(fun i -> assign (ToplUtils.static_var (ToplName.saved_arg i)) (local_var (ToplName.arg (i + 1))) ) ))