From 6f83c45e475d10037082c501a1af8215010e7b1f Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Thu, 25 Mar 2021 07:39:39 -0700 Subject: [PATCH] [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 --- infer/src/topl/ToplAst.ml | 6 +--- infer/src/topl/ToplAutomaton.ml | 30 ++++--------------- infer/src/topl/ToplLexer.mll | 1 - infer/src/topl/ToplParser.mly | 7 ++--- .../codetoanalyze/java/topl/baos/baos.topl | 1 - .../java/topl/compareArgs/CompareArgs.topl | 1 - .../java/topl/hasnext/hasnext.topl | 1 - .../topl/immutableArray/immutableArray.topl | 1 - .../java/topl/servlet/servlet.topl | 2 -- .../java/topl/skip/SkipAfterRemove.topl | 1 - .../java/topl/slowIter/slowIter.topl | 1 - .../codetoanalyze/java/topl/taint/Taint.topl | 1 - 12 files changed, 8 insertions(+), 45 deletions(-) diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml index f75dd8183..c7770bd1b 100644 --- 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} diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index b3cdbc4ec..5f1493f7b 100644 --- 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) diff --git a/infer/src/topl/ToplLexer.mll b/infer/src/topl/ToplLexer.mll index 9dbf1e370..5611d19ac 100644 --- 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 } diff --git a/infer/src/topl/ToplParser.mly b/infer/src/topl/ToplParser.mly index 09f7d168f..612edd9b2 100644 --- 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} } diff --git a/infer/tests/codetoanalyze/java/topl/baos/baos.topl b/infer/tests/codetoanalyze/java/topl/baos/baos.topl index 76bc0ce56..410bb500a 100644 --- 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 diff --git a/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl b/infer/tests/codetoanalyze/java/topl/compareArgs/CompareArgs.topl index 2f640773a..6a97f68f4 100644 --- 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 diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl b/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl index 1a7b36740..4189af6ec 100644 --- 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 diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/immutableArray.topl b/infer/tests/codetoanalyze/java/topl/immutableArray/immutableArray.topl index e639a079c..073a85f03 100644 --- 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 diff --git a/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl b/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl index 005882cd4..94247c0a2 100644 --- 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 diff --git a/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl b/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl index 3d694c5a5..3afad6bb6 100644 --- 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 diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl index 9749c751b..347260682 100644 --- 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 diff --git a/infer/tests/codetoanalyze/java/topl/taint/Taint.topl b/infer/tests/codetoanalyze/java/topl/taint/Taint.topl index a21bfe54c..9ac2cdfde 100644 --- 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: *