diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index f8aac67be..7e57b7c36 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -98,7 +98,12 @@ let call_execute loc = 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|] + let instrument = + let a = Lazy.force automaton in + let is_interesting t active = active && not (ToplAutomaton.is_skip a t) in + Array.existsi ~f:is_interesting active_transitions + in + if not instrument then (* optimization*) [|i|] else let i1s = set_transitions loc active_transitions in let i2s = call_save_args loc ret_id ret_typ arg_ts in diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index aa5efc3af..e28adeb78 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -27,11 +27,15 @@ type tindex = int type transition = {source: vindex; target: vindex; label: ToplAst.label} (** - INV1: Array.length states = Array.length outgoing - - INV2: each index of [transitions] occurs exactly once in one of [outgoing]'s lists - - INV3: max_args is the maximum length of the arguments list in a label on a transition *) + - INV2: Array.length transitions = Array.length skips + - INV3: each index of [transitions] occurs exactly once in one of [outgoing]'s lists + - INV4: max_args is the maximum length of the arguments list in a label on a transition The + fields marked as redundant are computed from the others (when the automaton is built), and are + cached for speed. *) type t = { states: vname array ; transitions: transition array + ; skips: bool array (* redundant *) ; outgoing: tindex list array ; vindex: vname -> vindex ; max_args: int (* redundant; cached for speed *) } @@ -57,7 +61,8 @@ let make properties = let transitions : transition array = let f p = let prefix_pname pname = - "^\\(\\|" ^ String.concat ~sep:"\\|" p.ToplAst.prefixes ^ "\\)\\." ^ pname ^ "(" + if String.equal ".*" pname then pname + else "^\\(\\|" ^ String.concat ~sep:"\\|" p.ToplAst.prefixes ^ "\\)\\." ^ pname ^ "(" in let f t = let source = vindex ToplAst.(p.name, t.source) in @@ -86,7 +91,19 @@ let make properties = in Array.fold ~init:0 ~f transitions in - {states; transitions; outgoing; vindex; max_args} + let skips : bool array = + let is_skip {source; target; label} = + let r = Int.equal source target in + let r = r && match label.return with Ignore -> true | _ -> false in + let r = r && Option.is_none label.arguments in + (* The next line conservatively evaluates if the regex on the label includes + * all other regexes. *) + let r = r && String.equal ".*" label.procedure_name in + r + in + Array.map ~f:is_skip transitions + in + {states; transitions; skips; outgoing; vindex; max_args} let outgoing a i = a.outgoing.(i) @@ -97,6 +114,8 @@ let vcount a = Array.length a.states let transition a i = a.transitions.(i) +let is_skip a i = a.skips.(i) + let tcount a = Array.length a.transitions let max_args a = a.max_args diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index b02b617a3..7961b8974 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/infer/src/topl/ToplAutomaton.mli @@ -41,6 +41,10 @@ val vcount : t -> int val transition : t -> tindex -> transition +val is_skip : t -> tindex -> bool +(** A transition is *skip* when it has no action, its guard is implied by all other guards, and its + target equals its source. [is_skip automaton t] returns true when it can prove that [t] is skip.*) + val tcount : t -> int val max_args : t -> int diff --git a/infer/tests/codetoanalyze/java/topl/issues.exp b/infer/tests/codetoanalyze/java/topl/issues.exp index f78c98e29..97bf97ec0 100644 --- a/infer/tests/codetoanalyze/java/topl/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/java/topl/IndexSkip.java, IndexSkip.foo(java.util.ArrayList):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure foo(...),Skipping size(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,ArrayList),start of procedure execute(),start of procedure execute_state_0(),Taking true branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute(),Taking true branch,Skipping get(...): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,ArrayList,Object),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] +codetoanalyze/java/topl/IndexSkip.java, IndexSkip.foo(java.util.ArrayList):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure foo(...),Taking true branch,Skipping get(...): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,ArrayList,Object),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] codetoanalyze/java/topl/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [] codetoanalyze/java/topl/Iterators.java, Iterators.hasNextBad(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextBad(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, []