[topl] Remove nondet marker

Summary: The explicit marker for nondeterministic states was used to speed up the shallow implementations of Topl, which ar enow removed. Reviewed By: jvillard Differential Revision: D27297019 fbshipit-source-id: 0fce93817
4 years ago · 6f83c45e47
parent 55af83de03
commit 6f83c45e47
12 changed files with 8 additions and 45 deletions
--- a/infer/src/topl/ToplAst.ml
+++ b/infer/src/topl/ToplAst.ml
@ -47,8 +47,4 @@ type transition = {source: vertex; target: vertex; label: label option}

 (* TODO(rgrigore): Check that registers are read only after being initialized *)
 type t =
-  { name: property_name
-  ; message: string option
-  ; prefixes: string list
-  ; nondet: string list
-  ; transitions: transition list }
+  {name: property_name; message: string option; prefixes: string list; transitions: transition list}
--- a/infer/src/topl/ToplAutomaton.ml
+++ b/infer/src/topl/ToplAutomaton.ml
@ -31,16 +31,14 @@ type tindex = int

 type transition = {source: vindex; target: vindex; label: ToplAst.label option}

-(** - 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
+(** - INV1: Array.length transitions = Array.length skips
+    - 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

    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
@ -76,7 +74,7 @@ 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_opt, 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 =
@ -118,30 +116,12 @@ let make properties =
    |> Array.max_elt ~compare:Int.compare
    |> Option.value ~default:0 |> succ
  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 =
    (* TODO(rgrigore): Rename "anys"? *)
    let is_skip {label} = Option.is_none label in
    Array.map ~f:is_skip transitions
  in
-  {states; nondets; transitions; skips; outgoing; vindex; max_args}
+  {states; transitions; skips; outgoing; vindex; max_args}


 let vname a i = a.states.(i)
--- a/infer/src/topl/ToplLexer.mll
+++ b/infer/src/topl/ToplLexer.mll
@ -56,7 +56,6 @@ rule raw_token = parse
  | "prefix" { PREFIX }
  | "property" { PROPERTY }
  | "message" { MESSAGE }
-  | "nondet" { NONDET }
  | "when" { WHEN }
  | ['a'-'z'] id_tail as id { LID id }
  | ['A'-'Z'] id_tail as id { UID id }
--- a/infer/src/topl/ToplParser.mly
+++ b/infer/src/topl/ToplParser.mly
@ -30,7 +30,6 @@
 %token LT
 %token MESSAGE
 %token NE
-%token NONDET
 %token PREFIX
 %token PROPERTY
 %token RC
@ -46,16 +45,14 @@
 properties: ps=one_property* EOF { ps }

 one_property:
-    PROPERTY name=identifier LC message=message? prefixes=prefix* nondet=nondet
+    PROPERTY name=identifier LC message=message? prefixes=prefix*
      transitions=transition* RC
-    { ToplAst.{name; message; prefixes; nondet; transitions} }
+    { ToplAst.{name; message; prefixes; transitions} }

 message: MESSAGE s=STRING { s }

 prefix: PREFIX s=STRING { s }

-nondet: NONDET LP ns=state* RP { ns }
-
 transition:
    source=state ARROW target=state COLON label=label
    { ToplAst.{source; target; label} }
--- a/infer/tests/codetoanalyze/java/topl/baos/baos.topl
+++ b/infer/tests/codetoanalyze/java/topl/baos/baos.topl
@ -1,5 +1,4 @@
 property BaosRetrieveWithoutFlush
-  nondet (start)
  start -> start: *
  start -> valid: ".*OutputStream"(X, Y, Ret) => x := X; y := Y
  valid -> invalid: ".*OutputStream.write.*"(X, Ia, Ret) when X == x
--- a/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl
+++ b/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl
@ -1,4 +1,3 @@
 property MaxArgs
-  nondet (start)
  start -> start: *
  start -> error: "CompareArgs.max"(Ignore, I, J, IgnoreRet) when I >= J
--- a/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl
+++ b/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl
@ -2,7 +2,6 @@ property HasNext
  prefix "Iterator"
  prefix "List"
  prefix "Scanner"
-  nondet (start)
  start -> start: *
  start -> invalid: iterator(Ignore, RetIter) => i := RetIter
  start -> invalid: Scanner(Iter, IgnoreA, IgnoreB) => i := Iter // For constructors, "this" is first argument, and there's a dummy return
--- a/infer/tests/codetoanalyze/java/topl/immutableArray/immutableArray.topl
+++ b/infer/tests/codetoanalyze/java/topl/immutableArray/immutableArray.topl
@ -1,6 +1,5 @@
 property ImmutableArrayModified
  prefix "ImmutableArray"
-  nondet (start)
  start -> start: *
  start -> tracking: getTestArray(IgnoreObject, Array) => a := Array
  tracking -> error: #ArrayWrite(Array, IgnoreIndex) when a == Array
--- a/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl
+++ b/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl
@ -8,7 +8,6 @@
 property InterleavedResponse
  message "A ServletResponse was asked for both a writer and a stream."
  prefix "ServletResponse"
-  nondet (start)
  start -> start: *
  start -> gotWriter: getWriter(R, IgnoreRet) => r := R
  start -> gotStream: getOutputStream(R, IgnoreRet) => r := R
@ -17,7 +16,6 @@ property InterleavedResponse

 property ForwardUncommitted
  message "A ServletResponse was forwarded before being committed."
-  nondet (start)
  start -> start: *
  start -> gotChannel: "ServletResponse.\\(getWriter\\|getOutputStream\\)"(R, C) => r := R; c := C
  gotChannel -> ok: "\\(PrintWriter\\|ServletOutputStream\\).flush.*"(C, IgnoreRet) when C == c
--- a/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl
+++ b/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl
@ -1,6 +1,5 @@
 property SkipAfterRemove
  prefix "ArrayList"
-  nondet (start)
  start -> start: *
  start -> removed: remove(Collection, Index, IgnoreRet) => c := Collection; i := Index
  removed -> ok:    get(Collection, Index, IgnoreRet) when i == Index && c == Collection
--- a/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl
+++ b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl
@ -1,5 +1,4 @@
 property ShouldUseEntries
-  nondet (start iteratingKeys)
  start -> start: *
  start -> gotKeys: "Map.keySet"(M, S) => m := M; s := S
  gotKeys -> iteratingKeys: "Set.iterator"(S, I) when S == s => i := I
--- a/infer/tests/codetoanalyze/java/topl/taint/Taint.topl
+++ b/infer/tests/codetoanalyze/java/topl/taint/Taint.topl
@ -1,7 +1,6 @@
 property TaintTrack
  prefix "StringBuilder"
  prefix "Taint"
-  nondet (start building track)

  // We start tracking when we see calls to Taint.badString
  start -> start: *