[topl] Generate simpler monitor for deterministic states.

Summary:
This is an optimization. We ask the user to tell us which states are nondeterministic, and we
generate code that handle nondeterminism only for those states. It is common for only one state per
TOPL property to be nondeterministic. This speeds up the biabduction-analysis of the monitor by a
factor of ~10. But, using the monitor is only a little faster.

Facebook

Reviewed By: jvillard

Differential Revision: D19160286

fbshipit-source-id: 4dd39769a

infer/src/topl/ToplAst.ml

@@ -42,4 +42,8 @@ type vertex = string [@@deriving compare, hash, sexp]
 type transition = {source: vertex; target: vertex; label: label}
 
 type t =
-  {name: property_name; message: string option; prefixes: string list; transitions: transition list}
+  { name: property_name
+  ; message: string option
+  ; prefixes: string list
+  ; nondet: string list
+  ; transitions: transition list }

infer/src/topl/ToplAutomaton.ml

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module L = Logging
 
 let tt = ToplUtils.debug
 
@@ -26,25 +27,39 @@ type tindex = int
 
 type transition = {source: vindex; target: vindex; label: ToplAst.label}
 
-(** - INV1: Array.length states = Array.length outgoing
+(** - INV1: Array.length states = Array.length outgoing = Array.length nondets
     - 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
+    - INV4: max_args is the maximum length of the arguments list in a label on a transition
-      fields marked as redundant are computed from the others (when the automaton is built), and are
+
-      cached for speed. *)
+    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
+  ; nondets: bool array (* redundant *)
   ; transitions: transition array
   ; skips: bool array (* redundant *)
   ; outgoing: tindex list array
   ; vindex: vname -> vindex
-  ; max_args: int (* redundant; cached for speed *) }
+  ; max_args: int (* redundant *) }
 
-(** [index_in H a x] is the (last) index of [x] in array [a]. *)
+(** [index_in H a] returns a pair of functions [(opt, err)] that lookup the (last) index of an
-let index_in (type k) (module H : Hashtbl_intf.S with type key = k) (a : k array) : k -> int =
+    element in [a]. The difference is that [opt x] returns an option, while [err msg x] makes Infer
+    die, mentioning [msg].*)
+let index_in (type k) (module H : Hashtbl_intf.S with type key = k) (a : k array) :
+    (k -> int option) * (string -> k -> int) =
   let h = H.create ~size:(2 * Array.length a) () in
   let f i x = H.set h ~key:x ~data:i in
-  Array.iteri ~f a ; H.find_exn h
+  Array.iteri ~f a ;
+  let opt = H.find h in
+  let err msg x =
+    match opt x with
+    | Some x ->
+        x
+    | None ->
+        L.die InternalError "ToplAutomaton.index_in out of bounds (%s)" msg
+  in
+  (opt, err)
 
 
 let make properties =
@@ -57,7 +72,8 @@ let make properties =
     Array.of_list (List.dedup_and_sort ~compare:Vname.compare (List.concat_map ~f properties))
   in
   Array.iteri ~f:(fun i (p, v) -> tt "state[%d]=(%s,%s)@\n" i p v) states ;
-  let vindex = index_in (module Vname.Table) states in
+  let vindex_opt, vindex = index_in (module Vname.Table) states in
+  let vindex = vindex "vertex" in
   let transitions : transition array =
     let f p =
       let prefix_pname pname =
@@ -92,6 +108,23 @@ let make properties =
     in
     Array.fold ~init:0 ~f transitions
   in
+  let nondets : bool array =
+    let vcount = Array.length states in
+    let a = Array.create ~len:vcount false in
+    let f ToplAst.{nondet; name; _} =
+      let set_nondet state =
+        match vindex_opt (name, state) with
+        | Some i ->
+            a.(i) <- true
+        | None ->
+            L.user_warning
+              "TOPL: %s declared as nondet, but it appears in no transition of property %s" state
+              name
+      in
+      List.iter ~f:set_nondet nondet
+    in
+    List.iter ~f properties ; a
+  in
   let skips : bool array =
     let is_skip {source; target; label} =
       let r = Int.equal source target in
@@ -104,13 +137,15 @@ let make properties =
     in
     Array.map ~f:is_skip transitions
   in
-  {states; transitions; skips; outgoing; vindex; max_args}
+  {states; nondets; transitions; skips; outgoing; vindex; max_args}
 
 
 let outgoing a i = a.outgoing.(i)
 
 let vname a i = a.states.(i)
 
+let is_nondet a i = a.nondets.(i)
+
 let vcount a = Array.length a.states
 
 let transition a i = a.transitions.(i)

infer/src/topl/ToplAutomaton.mli

@@ -37,6 +37,8 @@ val outgoing : t -> vindex -> tindex list
 
 val vname : t -> vindex -> vname
 
+val is_nondet : t -> vindex -> bool
+
 val vcount : t -> int
 
 val transition : t -> tindex -> transition

infer/src/topl/ToplLexer.mll

@@ -54,6 +54,7 @@ rule raw_token = parse
   | "prefix" { PREFIX }
   | "property" { PROPERTY }
   | "message" { MESSAGE }
+  | "nondet" { NONDET }
   | ['a'-'z'] id_tail as id { LID id }
   | ['A'-'Z'] id_tail as id { UID id }
   | eof { EOF }

infer/src/topl/ToplMonitor.ml

@@ -341,7 +341,9 @@ let generate_execute_state automaton proc_name =
     in
     let transitions = ToplAutomaton.outgoing automaton state in
     let fold f init = List.fold_right ~init ~f transitions in
-    fold check_transition_maybe (fold check_transition skip)
+    let detbranches = fold check_transition skip in
+    if ToplAutomaton.is_nondet automaton state then fold check_transition_maybe detbranches
+    else detbranches
   in
   let body =
     gen_if

infer/src/topl/ToplParser.mly

@@ -29,6 +29,7 @@
 %token LT
 %token MESSAGE
 %token NE
+%token NONDET
 %token PREFIX
 %token PROPERTY
 %token RC
@@ -42,17 +43,22 @@
 properties: ps=one_property* EOF { ps }
 
 one_property:
-    PROPERTY name=identifier LC message=message? prefixes=prefix* transitions=transition* RC
+    PROPERTY name=identifier LC message=message? prefixes=prefix* nondet=nondet
-    { ToplAst.{name; message; prefixes; transitions} }
+      transitions=transition* RC
+    { ToplAst.{name; message; prefixes; nondet; transitions} }
 
 message: MESSAGE s=STRING { s }
 
 prefix: PREFIX s=STRING { s }
 
+nondet: NONDET LP ns=state* RP { ns }
+
 transition:
-    source=identifier ARROW target=identifier COLON label=label
+    source=state ARROW target=state COLON label=label
     { ToplAst.{source; target; label} }
 
+state: i=identifier { i }
+
 label:
     return=value_pattern ASGN cp=call_pattern condition=condition?
     { let procedure_name, arguments = cp in

infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl

@@ -1,5 +1,6 @@
 property SkipAfterRemove
   prefix "ArrayList"
+  nondet (start)
   start -> start: *
   start -> removed: remove(Collection, Index)
   removed -> ok:    get(collection, index)

infer/tests/codetoanalyze/java/topl/hasnext.topl

@@ -2,6 +2,7 @@ property HasNext
   prefix "Iterator"
   prefix "List"
   prefix "Scanner"
+  nondet (start)
   start -> start: *
   start -> invalid: I = iterator(*)
   start -> invalid: Scanner(I, *)  // For constructors, biabduction has "this" as first argument

infer/tests/codetoanalyze/java/topl/issues.exp

@@ -1,8 +1,8 @@
-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/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,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.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,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, []
-codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),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(),start of procedure getSingleElementOk(...),Skipping next(): unknown method]
+codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),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,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(),start of procedure getSingleElementOk(...),Skipping next(): unknown method]
-codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),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.hasNextInterproceduralOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),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,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.hasNextOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),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.hasNextOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),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,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/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []

infer/tests/codetoanalyze/java/topl/iterators.topl

@@ -1,6 +1,7 @@
 property HasNext
   prefix "Iterator"
   prefix "List"
+  nondet (start)
   start -> start: *
   start -> invalid: I = iterator(*)
   invalid -> valid: <true> = hasNext(i) // treat as shorthand for <B> = hasNext if (b)
@@ -10,12 +11,15 @@ property HasNext
 property UnsafeIterator
   prefix "Collection"
   prefix "Iterator"
+  nondet (start)
+  start -> start: *
   start -> iterating: I = iterator(C)
   iterating -> modified: remove(c, *)
   iterating -> modified: add(c, *)
   modified -> error: next(i)
 
 property UnsafeMapIterator
+  nondet (start)
   start -> start: *
   start -> gotView: View = keySet(M)
   start -> gotView: View = values(M)
@@ -25,7 +29,8 @@ property UnsafeMapIterator
 
 property SkipIndexAfterRemove
   prefix "ArrayList"
+  nondet (start)
   start -> start: *
   start -> removed: remove(Collection, Index)
   removed -> ok:    get(collection, index)
-  removed -> error: get(collection, J) // TODO: if (j!=index)
+  removed -> error: get(collection, J) if J != index

infer/tests/codetoanalyze/java/topl/tomcat.topl

@@ -4,12 +4,13 @@ property ForwardUncommitted
   prefix "javax.servlet"
   prefix "javax.servlet.{ServletOutputStream,ServletResponse}"
   prefix "java.io.PrintWriter"
+  nondet (start)
   start -> start: *
   start -> tracking: R = "ServletResponse.\<init\>"
   tracking -> ok: flushBuffer(r)
   tracking -> gotWriter: W = getWriter(r)
   gotWriter -> ok: flush(w)
-  gotWrite -> ok: flushBuffer(r)
+  gotWriter -> ok: flushBuffer(r)
   tracking -> gotStream: S = getOutputStream(r)
   gotStream -> ok: flush(s)
   gotStream -> ok: flushBuffer(r)
@@ -24,6 +25,7 @@ property ForwardUncommitted
 property InterleavedResponse1
   message "A ServletResponse was asked for both a writer and a stream."
   prefix "javax.servlet.ServletResponse"
+  nondet (start)
   start -> start: *
   start -> gotWriter: W = getWriter(R)
   start -> gotStream: S = getOutputStream(R)
@@ -34,6 +36,7 @@ property InterleavedResponse2
   // vertex names: w = got writer; W = used writer; similarly for s, S
   message "Incompatible methods for putting data into a response were used."
   prefix "javax.servlet.ServletResponse"
+  nondet (start)
   start -> start: *
   start -> w: W = getWriter(R)
   start -> s: S = getOutputStream(R)