Summary: Instrument SIL according to TOPL properties. Roughly, the instrumentation is a set of calls into procedures that simulate a nondeterministic automaton. For now, those procedures are NOP dummies. Reviewed By: jvillard Differential Revision: D15063942 fbshipit-source-id: d22c2f6famaster
Radu Grigore
6 years ago
committed by
Facebook Github Bot
parent
6f422fb78f
commit
047c64c528
@ -0,0 +1,81 @@
|
||||
(*
|
||||
* Copyright (c) 2019-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
module Vname = struct
|
||||
module T = struct
|
||||
type t = ToplAst.property_name * ToplAst.vertex [@@deriving compare, hash, sexp]
|
||||
end
|
||||
|
||||
include T
|
||||
include Hashable.Make (T)
|
||||
end
|
||||
|
||||
type vname = Vname.t
|
||||
|
||||
type vindex = int
|
||||
|
||||
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 *)
|
||||
type t =
|
||||
{ states: vname array
|
||||
; transitions: transition array
|
||||
; outgoing: tindex list array
|
||||
; vindex: vname -> vindex }
|
||||
|
||||
(** [index_in H a x] is the (last) index of [x] in array [a]. *)
|
||||
let index_in (type k) (module H : Hashtbl_intf.S with type key = k) (a : k array) : 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 ;
|
||||
let find x = H.find_exn h x in
|
||||
find
|
||||
|
||||
|
||||
let make properties =
|
||||
let states : vname array =
|
||||
let open ToplAst in
|
||||
let f p =
|
||||
let f {source; target; _} = [(p.name, source); (p.name, target)] in
|
||||
List.concat_map ~f p.transitions
|
||||
in
|
||||
Array.of_list (List.concat_map ~f properties)
|
||||
in
|
||||
let vindex = index_in (module Vname.Table) states in
|
||||
let transitions : transition array =
|
||||
let f p =
|
||||
let prefix_pname pname =
|
||||
"^\\(\\|" ^ String.concat ~sep:"\\|" p.ToplAst.prefixes ^ "\\)\\." ^ pname ^ "()$"
|
||||
in
|
||||
let f t =
|
||||
let source = vindex ToplAst.(p.name, t.source) in
|
||||
let target = vindex ToplAst.(p.name, t.target) in
|
||||
let procedure_name = prefix_pname ToplAst.(t.label.procedure_name) in
|
||||
let label = {t.ToplAst.label with procedure_name} in
|
||||
{source; target; label}
|
||||
in
|
||||
List.map ~f p.ToplAst.transitions
|
||||
in
|
||||
Array.of_list (List.concat_map ~f properties)
|
||||
in
|
||||
let outgoing : tindex list array =
|
||||
let vcount = Array.length states in
|
||||
let a = Array.create ~len:vcount [] in
|
||||
let f i t = a.(t.source) <- i :: a.(t.source) in
|
||||
Array.iteri ~f transitions ; a
|
||||
in
|
||||
{states; transitions; outgoing; vindex}
|
||||
|
||||
|
||||
let transition a i = a.transitions.(i)
|
||||
|
||||
let tcount a = Array.length a.transitions
|
||||
@ -0,0 +1,39 @@
|
||||
(*
|
||||
* Copyright (c) 2019-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*)
|
||||
|
||||
open! IStd
|
||||
|
||||
(* An automaton is a different representation for a set of TOPL properties: states and transitions
|
||||
are identified by nonnegative integers; and transitions are grouped by their source. Also, the
|
||||
meaning of transition labels does not depend on context (e.g., prefixes are now included).
|
||||
|
||||
We identify states by integers because biabduction tracks integers well; for example, equality
|
||||
checks on integers are obvious, we don't need to worry about whether we should be using an
|
||||
equals() method.
|
||||
|
||||
We identify transitions by integers because, in the monitor code that we generate, we use a
|
||||
boolean variable transitionN to tell if the static part of a transition guard is satisfied. The N
|
||||
is just some identifier for the transition, and integers are convenient identifiers.
|
||||
|
||||
NOTE: Now, the signature is the minimal needed for code instrumentation, but the implementation
|
||||
does some extra work (such as grouping transitions by their source) that will be useful for
|
||||
code generation. (TODO: remove note once code generation is implemented.)
|
||||
*)
|
||||
|
||||
type t
|
||||
|
||||
type vindex = int
|
||||
|
||||
type tindex = int (* from 0 to tcount()-1, inclusive *)
|
||||
|
||||
type transition = {source: vindex; target: vindex; label: ToplAst.label}
|
||||
|
||||
val make : ToplAst.t list -> t
|
||||
|
||||
val transition : t -> tindex -> transition
|
||||
|
||||
val tcount : t -> int
|
||||
@ -0,0 +1,14 @@
|
||||
/*
|
||||
* Copyright (c) 2019-present, Facebook, Inc.
|
||||
*
|
||||
* This source code is licensed under the MIT license found in the
|
||||
* LICENSE file in the root directory of this source tree.
|
||||
*/
|
||||
import java.util.*;
|
||||
|
||||
class Iterators {
|
||||
void hasNextBad_FN(List<Integer> x) {
|
||||
Iterator<Integer> i = x.iterator();
|
||||
i.next();
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,29 @@
|
||||
property HasNext
|
||||
prefix <java.util.{Collection,Iterator}>
|
||||
start -> start: *
|
||||
start -> invalid: I = iterator(*)
|
||||
invalid -> valid: <true> = hasNext(i) // treat as shorthand for <B> = hasNext if (b)
|
||||
valid -> invalid: next(i)
|
||||
invalid -> error: next(i)
|
||||
|
||||
property UnsafeIterator
|
||||
prefix <java.util.{Collection,Iterator}>
|
||||
start -> iterating: I = iterator(C)
|
||||
iterating -> modified: remove(c, *)
|
||||
iterating -> modified: add(c, *)
|
||||
modified -> error: next(i)
|
||||
|
||||
property UnsafeMapIterator
|
||||
start -> start: *
|
||||
start -> gotView: View = keySet(M)
|
||||
start -> gotView: View = values(M)
|
||||
gotView -> iterating: I = iterator(view)
|
||||
iterating -> updated: put(m, *)
|
||||
updated -> error: next(i)
|
||||
|
||||
property SkipIndexAfterRemove
|
||||
prefix <java.util.ArrayList>
|
||||
start -> start: *
|
||||
start -> removed: remove(Collection, Index)
|
||||
removed -> ok: get(collection, index)
|
||||
removed -> error: get(collection, J) // TODO: if (j!=index)
|
||||
Loading…
Reference in new issue