[topl] Optimize code instrumentation.

Summary:
Don't instrument SIL when we can determine statically that
biabduction symexec would be a no-op.

Reviewed By: ngorogiannis

Differential Revision: D19116849

fbshipit-source-id: 4d25462a3

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

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
+    - INV2: Array.length transitions = Array.length skips
-    - INV3: max_args is the maximum length of the arguments list in a label on a transition *)
+    - 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

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

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, []