From 047c64c528e1d6c8362b22912955f3369ecfb1ff Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Fri, 7 Jun 2019 07:17:41 -0700 Subject: [PATCH] [topl] Instrument SIL. 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: d22c2f6fa --- infer/man/man1/infer-full.txt | 4 + infer/src/IR/Instrs.ml | 8 + infer/src/IR/Instrs.mli | 6 + infer/src/IR/Procdesc.ml | 26 ++- infer/src/IR/Procdesc.mli | 4 + infer/src/IR/Typ.ml | 2 + infer/src/IR/Typ.mli | 2 + infer/src/backend/ondemand.ml | 16 +- infer/src/base/Config.ml | 6 + infer/src/base/Config.mli | 2 + infer/src/biabduction/interproc.ml | 2 +- infer/src/deadcode/dune.in | 2 +- infer/src/dune.in | 6 +- infer/src/istd/IList.ml | 2 + infer/src/istd/IList.mli | 4 + infer/src/topl/Topl.ml | 183 +++++++++++++++++- infer/src/topl/Topl.mli | 14 +- infer/src/topl/ToplAst.ml | 7 +- infer/src/topl/ToplAutomaton.ml | 81 ++++++++ infer/src/topl/ToplAutomaton.mli | 39 ++++ .../codetoanalyze/java/topl/Iterators.java | 14 ++ infer/tests/codetoanalyze/java/topl/Makefile | 2 +- .../codetoanalyze/java/topl/iterators.topl | 29 +++ 23 files changed, 434 insertions(+), 27 deletions(-) create mode 100644 infer/src/topl/ToplAutomaton.ml create mode 100644 infer/src/topl/ToplAutomaton.mli create mode 100644 infer/tests/codetoanalyze/java/topl/Iterators.java create mode 100644 infer/tests/codetoanalyze/java/topl/iterators.topl diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 080448dd6..402385e84 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1746,6 +1746,10 @@ INTERNAL OPTIONS Activates: Detailed tracing information during prop re-arrangement operations (Conversely: --no-trace-rearrange) + --trace-topl + Activates: Detailed tracing information during TOPL analysis + (Conversely: --no-trace-topl) + --tracing Activates: Report error traces for runtime exceptions (Java only): generate preconditions for runtimeexceptions in Java and report diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml index 886a6b025..7c7002389 100644 --- a/infer/src/IR/Instrs.ml +++ b/infer/src/IR/Instrs.ml @@ -91,6 +91,14 @@ let map_changed = if phys_equal instrs instrs' then t else NotReversed instrs' +let concat_map_changed ~equal (NotReversed instrs as t) ~f = + let instrs' = Array.concat_map ~f instrs in + if + Int.equal (Array.length instrs) (Array.length instrs') + && Array.for_all2_exn ~f:equal instrs instrs' + then t + else NotReversed instrs' + let reverse_order (NotReversed instrs) = Reversed (RevArray.of_rev_array instrs) (* Functions on both reversed and non-reversed arrays *) diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli index 80cd12c8f..a973d819a 100644 --- a/infer/src/IR/Instrs.mli +++ b/infer/src/IR/Instrs.mli @@ -33,6 +33,12 @@ val map_changed : -> f:(Sil.instr -> Sil.instr) -> not_reversed_t +val concat_map_changed : + equal:(Sil.instr -> Sil.instr -> bool) + -> not_reversed_t + -> f:(Sil.instr -> Sil.instr array) + -> not_reversed_t + val reverse_order : not_reversed_t -> reversed t val is_empty : _ t -> bool diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index b0305bfe2..ffdad67e2 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -228,6 +228,15 @@ module Node = struct true ) + (** Like [replace_instrs], but 1 instr gets replaced by 0, 1, or more instructions. *) + let replace_instrs_by node ~f = + let instrs' = Instrs.concat_map_changed ~equal:phys_equal node.instrs ~f:(f node) in + if phys_equal instrs' node.instrs then false + else ( + node.instrs <- instrs' ; + true ) + + let pp_stmt fmt = function | AssertionFailure -> F.pp_print_string fmt "Assertion failure" @@ -520,13 +529,22 @@ let find_map_instrs pdesc ~f = find_map_nodes ~f:find_map_node pdesc -let replace_instrs pdesc ~f = - let f updated node = - Node.replace_instrs ~f node || (* do not short-circuit [Node.replace_instrs] *) updated - in +let update_nodes pdesc ~(update : Node.t -> bool) : bool = + let f acc node = update node || acc in + (* do not shortcut call to [update] *) fold_nodes pdesc ~init:false ~f +let replace_instrs pdesc ~f = + let update node = Node.replace_instrs ~f node in + update_nodes pdesc ~update + + +let replace_instrs_by pdesc ~f = + let update node = Node.replace_instrs_by ~f node in + update_nodes pdesc ~update + + (** fold between two nodes or until we reach a branching structure *) let fold_slope_range = let rec aux node visited acc ~f = diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index cdf8bea73..fd1fae9d3 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -264,6 +264,10 @@ val replace_instrs : t -> f:(Node.t -> Sil.instr -> Sil.instr) -> bool (** Map and replace the instructions to be executed. Returns true if at least one substitution occured. *) +val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array) -> bool +(** Like [replace_instrs], but slower, and each instruction may be replaced +by 0, 1, or more instructions. *) + val iter_nodes : (Node.t -> unit) -> t -> unit (** iterate over all the nodes of a procedure *) diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index eda8c2c24..e0b38d589 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -447,6 +447,8 @@ module Name = struct let java_lang_object = make ~package:"java.lang" "Object" let java_lang_string = make ~package:"java.lang" "String" + + let void = make "void" end let from_string name_str = JavaClass (Mangled.from_string name_str) diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 1dda3515e..fb753554d 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -199,6 +199,8 @@ module Name : sig val java_lang_string : t + val void : t + val package : t -> string option val type_name : t -> string diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index ec3610792..df04ecfaf 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -59,8 +59,13 @@ let should_be_analyzed proc_attributes = (not (is_active proc_name)) (* avoid infinite loops *) && not (already_analyzed proc_name) +let get_proc_attr proc_name = + IList.force_until_first_some + [lazy (Summary.proc_resolve_attributes proc_name); lazy (Topl.get_proc_attr proc_name)] + + let procedure_should_be_analyzed proc_name = - match Summary.proc_resolve_attributes proc_name with + match get_proc_attr proc_name with | Some proc_attributes when Config.reactive_capture && not proc_attributes.is_defined -> (* try to capture procedure first *) let defined_proc_attributes = OndemandCapture.try_capture proc_attributes in @@ -270,11 +275,10 @@ let analyze_proc_desc ~caller_pdesc callee_pdesc = (** Find a proc desc for the procedure, perhaps loading it from disk. *) let get_proc_desc callee_pname = - match Procdesc.load callee_pname with - | Some _ as pdesc_opt -> - pdesc_opt - | None -> - Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname) + IList.force_until_first_some + [ lazy (Procdesc.load callee_pname) + ; lazy (Option.map ~f:Summary.get_proc_desc (Summary.get callee_pname)) + ; lazy (Topl.get_proc_desc callee_pname) ] (** analyze_proc_name ?caller_pdesc proc_name performs an on-demand analysis of proc_name triggered diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 12998691b..dad5100ea 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2289,6 +2289,10 @@ and trace_rearrange = "Detailed tracing information during prop re-arrangement operations" +and trace_topl = + CLOpt.mk_bool ~long:"trace-topl" "Detailed tracing information during TOPL analysis" + + and tracing = CLOpt.mk_bool ~deprecated:["tracing"] ~long:"tracing" "Report error traces for runtime exceptions (Java only): generate preconditions for \ @@ -3141,6 +3145,8 @@ and trace_join = !trace_join and trace_rearrange = !trace_rearrange +and trace_topl = !trace_topl + and tracing = !tracing and tv_commit = !tv_commit diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 9f3eed0bc..34aa73217 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -690,6 +690,8 @@ val trace_ondemand : bool val trace_rearrange : bool +val trace_topl : bool + val tracing : bool val tv_commit : string option diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 150ad011e..25bd97307 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -1253,7 +1253,7 @@ let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t = let analyze_procedure {Callbacks.summary; proc_desc; tenv; exe_env} : Summary.t = (* make sure models have been registered *) BuiltinDefn.init () ; - if not (List.is_empty Config.topl_properties) then Topl.init () ; + if Topl.is_active () then Topl.instrument tenv proc_desc ; try analyze_procedure_aux summary exe_env tenv proc_desc with exn -> IExn.reraise_if exn ~f:(fun () -> not (Exceptions.handle_exception exn)) ; diff --git a/infer/src/deadcode/dune.in b/infer/src/deadcode/dune.in index 05fb2563d..a7fd3335e 100644 --- a/infer/src/deadcode/dune.in +++ b/infer/src/deadcode/dune.in @@ -16,7 +16,7 @@ Format.sprintf (ocamlopt_flags (%s)) (libraries %s) (modules All_infer_in_one_file) - (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check)) + (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check)) ) |} (String.concat " " common_cflags) diff --git a/infer/src/dune.in b/infer/src/dune.in index dc6b26133..03aac3b64 100644 --- a/infer/src/dune.in +++ b/infer/src/dune.in @@ -64,7 +64,7 @@ let stanzas = (ocamlopt_flags (%s)) (libraries %s) (modules :standard \ %s infertop) - (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check)) + (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check)) ) (documentation @@ -84,7 +84,7 @@ let stanzas = (ocamlopt_flags (%s)) (libraries InferModules) (modules %s) - (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check)) + (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check)) ) |} (String.concat " " infer_binaries) @@ -98,7 +98,7 @@ let stanzas = (flags (%s)) (libraries utop InferModules) (modules Infertop) - (preprocess (pps ppx_compare ppx_fields_conv ppx_sexp_conv ppx_variants_conv -no-check)) + (preprocess (pps ppx_compare ppx_fields_conv ppx_hash ppx_sexp_conv ppx_variants_conv -no-check)) (link_flags (-linkall -warn-error -31)) ) |} diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index 74ebdb1ff..195bfff71 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -182,6 +182,8 @@ let remove_first = fun list ~f -> aux list ~f [] +let force_until_first_some lazies = List.find_map lazies ~f:Lazy.force + let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf = let rec aux n = function | [] -> diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 61d519ac1..17dd0386e 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -46,6 +46,10 @@ val opt_cons : 'a option -> 'a list -> 'a list val remove_first : 'a list -> f:('a -> bool) -> 'a list option +val force_until_first_some : 'a option lazy_t list -> 'a option +(** [force_until_first_some xs] forces the computation of each element of [xs] and returns the first +that matches (Some _); or, if no such element exists, it returns None. *) + val pp_print_list : max:int -> ?pp_sep:(Format.formatter -> unit -> unit) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index aaf393b00..fcd06064d 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -8,9 +8,7 @@ open! IStd module L = Logging -let initialized = ref false - -let properties = ref [] +let tt fmt = L.d_printf "ToplTrace: " ; L.d_printfln fmt let parse topl_file = let f ch = @@ -25,7 +23,178 @@ let parse topl_file = with Sys_error msg -> L.(die UserError) "@[topl:%s: %s@]@\n@?" topl_file msg -let init () = - if not !initialized then ( - properties := List.concat_map ~f:parse Config.topl_properties ; - initialized := true ) +let properties = lazy (List.concat_map ~f:parse Config.topl_properties) + +let automaton = lazy (ToplAutomaton.make (Lazy.force properties)) + +let is_active () = not (List.is_empty (Lazy.force properties)) + +let cfg = Cfg.create () + +let sourcefile = SourceFile.create "SynthesizedToplProperty.java" + +let sourcefile_location = Location.none sourcefile + +(* NOTE: For now, Topl is mostly untyped; that is, everything has type Object. *) +let type_of_paramtyp (_t : Typ.Procname.Parameter.t) : Typ.t = + let classname = Typ.mk (Tstruct Typ.Name.Java.java_lang_object) in + Typ.mk (Tptr (classname, Pk_pointer)) + + +(** NOTE: Similar to [JTrans.formals_from_signature]. *) +let formals_of_procname proc_name = + let params = Typ.Procname.get_parameters proc_name in + let new_arg_name = + let n = ref (-1) in + fun () -> incr n ; Printf.sprintf "arg%d" !n + in + let f t = + let name = Mangled.from_string (new_arg_name ()) in + let typ = type_of_paramtyp t in + (name, typ) + in + List.map ~f params + + +(** The procedure description and its nodes will have location [sourcefile_location]. *) +let empty_proc_desc proc_name = + let attr = + let formals = formals_of_procname proc_name in + let is_defined = true in + let loc = sourcefile_location in + {(ProcAttributes.default sourcefile proc_name) with formals; is_defined; loc} + in + let proc_desc = Cfg.create_proc_desc cfg attr in + let start_node = + Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Start_node [] + in + let exit_node = Procdesc.create_node proc_desc sourcefile_location Procdesc.Node.Exit_node [] in + Procdesc.node_set_succs_exn proc_desc start_node [exit_node] [exit_node] ; + Procdesc.set_start_node proc_desc start_node ; + Procdesc.set_exit_node proc_desc exit_node ; + proc_desc + + +let is_synthesized = function + | Typ.Procname.Java j -> + String.equal "topl.Property" (Typ.Procname.Java.get_class_name j) + | _ -> + false + + +let get_proc_desc proc_name = + if is_synthesized proc_name then Some ((* TODO *) empty_proc_desc proc_name) else None + + +let get_proc_attr proc_name = + (* TODO: optimize -- don't generate body just to get attributes *) + Option.map ~f:Procdesc.get_attributes (get_proc_desc proc_name) + + +let get_transitions_count () = ToplAutomaton.tcount (Lazy.force automaton) + +(** Checks whether the method name and the number of arguments matches the conditions in a +transition label. Possible optimization: also evaluate if arguments equal certain constants. *) +let evaluate_static_guard label (e_fun, arg_ts) = + let match_name () = + match e_fun with + | Exp.Const (Const.Cfun n) -> + (* TODO: perhaps handle inheritance *) + let name = Typ.Procname.hashable_name n in + let re = Str.regexp label.ToplAst.procedure_name in + let result = Str.string_match re name 0 in + if Config.trace_topl then + tt "match name='%s' re='%s' result=%b" name label.ToplAst.procedure_name result ; + result + | _ -> + false + in + let match_args () = + let same_length xs ys = Option.is_some (List.zip xs ys) in + Option.value_map label.ToplAst.arguments ~f:(same_length arg_ts) ~default:true + in + match_name () && match_args () + + +(** For each transition in the automaton, evaluate its static guard. *) +let get_active_transitions e_fun arg_ts = + let a = Lazy.force automaton in + let f i = evaluate_static_guard (ToplAutomaton.transition a i).label (e_fun, arg_ts) in + Array.init (ToplAutomaton.tcount a) ~f + + +let topl_class_exp = + let class_name = Mangled.from_string "topl.Property" in + let var_name = Pvar.mk_global class_name in + Exp.Lvar var_name + + +let topl_class_name : Typ.Name.t = Typ.Name.Java.from_string "topl.Property" + +let topl_class_typ = Typ.mk (Tstruct topl_class_name) + +let transition_field_name i = Typ.Fieldname.Java.from_string (Printf.sprintf "transition%d" i) + +let transition_var i = Exp.Lfield (topl_class_exp, transition_field_name i, topl_class_typ) + +let set_transitions loc active_transitions = + let store i b = + let value = if b then Exp.one else Exp.zero in + Sil.Store (transition_var i, topl_class_typ, value, loc) + in + Array.mapi ~f:store active_transitions + + +let topl_fun name n = + let ret_typ = Some Typ.Name.Java.Split.void in + let args_typ = List.init n ~f:(fun _ -> Typ.Name.Java.Split.java_lang_object) in + Exp.Const + (Const.Cfun + (Typ.Procname.Java + (Typ.Procname.Java.make topl_class_name ret_typ name args_typ Typ.Procname.Java.Static))) + + +let call_save_args loc ret_id ret_typ arg_ts = + let arg_ts = arg_ts @ [(Exp.Var ret_id, ret_typ)] in + let e_fun = topl_fun "saveArgs" (List.length arg_ts) in + let ret_id = Ident.create_fresh Ident.knormal in + let ret_typ = Typ.mk Tvoid in + [|Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, CallFlags.default)|] + + +let call_execute loc = + let e_fun = topl_fun "execute" 0 in + let ret_id = Ident.create_fresh Ident.knormal in + let ret_typ = Typ.mk Tvoid in + [|Sil.Call ((ret_id, ret_typ), e_fun, [], loc, CallFlags.default)|] + + +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|] + else + let i1s = set_transitions loc active_transitions in + let i2s = call_save_args loc ret_id ret_typ arg_ts in + let i3s = call_execute loc in + Array.concat [[|i|]; i1s; i2s; i3s] + | i -> + [|i|] + + +(* PRE: Calling [Tenv.mk_struct tenv ] twice is a no-op. *) +let add_types tenv = + let transition_field i = (transition_field_name i, Typ.mk (Tint IBool), []) in + let rec transitions n = + if Int.equal n 0 then [] else transition_field (n - 1) :: transitions (n - 1) + in + let statics = transitions (get_transitions_count ()) in + let _topl_class = Tenv.mk_struct tenv topl_class_name ~statics in + () + + +let instrument tenv procdesc = + add_types tenv ; + let f _node = instrument_instruction in + let _updated = Procdesc.replace_instrs_by procdesc ~f in + () diff --git a/infer/src/topl/Topl.mli b/infer/src/topl/Topl.mli index 324a04f88..550f9a075 100644 --- a/infer/src/topl/Topl.mli +++ b/infer/src/topl/Topl.mli @@ -7,5 +7,15 @@ open! IStd -val init : unit -> unit -(** Parse properties, mentioned by [Config.topl_properties]. Does this only once. *) +val is_active : unit -> bool +(** Returns whether the TOPL analysis is active. *) + +val get_proc_attr : Typ.Procname.t -> ProcAttributes.t option +(** [get_proc_attr proc_name] returns the attributes of [get_proc_desc proc_name] *) + +val get_proc_desc : Typ.Procname.t -> Procdesc.t option +(** Returns a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property. *) + +val instrument : Tenv.t -> Procdesc.t -> unit +(** Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility +to instrument procedures at most once. *) diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml index fd9f5a18d..0d236e8ec 100644 --- a/infer/src/topl/ToplAst.ml +++ b/infer/src/topl/ToplAst.ml @@ -7,6 +7,8 @@ open! IStd +type property_name = string [@@deriving compare, hash, sexp] + type register_name = string (** TODO: use Const.t *) @@ -26,8 +28,9 @@ type label = ; procedure_name: procedure_name_pattern ; arguments: value_pattern list option } -type vertex = string +type vertex = string [@@deriving compare, hash, sexp] type transition = {source: vertex; target: vertex; label: label} -type t = {name: string; message: string option; prefixes: string list; transitions: transition list} +type t = + {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 new file mode 100644 index 000000000..dd883a3cc --- /dev/null +++ b/infer/src/topl/ToplAutomaton.ml @@ -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 diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli new file mode 100644 index 000000000..b73d22043 --- /dev/null +++ b/infer/src/topl/ToplAutomaton.mli @@ -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 diff --git a/infer/tests/codetoanalyze/java/topl/Iterators.java b/infer/tests/codetoanalyze/java/topl/Iterators.java new file mode 100644 index 000000000..6bb0d3888 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/Iterators.java @@ -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 x) { + Iterator i = x.iterator(); + i.next(); + } +} diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile index ca917b0ff..7f8c2fd69 100644 --- a/infer/tests/codetoanalyze/java/topl/Makefile +++ b/infer/tests/codetoanalyze/java/topl/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../.. -INFER_OPTIONS = --topl-properties tomcat.topl --biabduction-only +INFER_OPTIONS = --topl-properties tomcat.topl --topl-properties iterators.topl --biabduction-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/iterators.topl b/infer/tests/codetoanalyze/java/topl/iterators.topl new file mode 100644 index 000000000..92cc32c51 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/iterators.topl @@ -0,0 +1,29 @@ +property HasNext + prefix + start -> start: * + start -> invalid: I = iterator(*) + invalid -> valid: = hasNext(i) // treat as shorthand for = hasNext if (b) + valid -> invalid: next(i) + invalid -> error: next(i) + +property UnsafeIterator + prefix + 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 + start -> start: * + start -> removed: remove(Collection, Index) + removed -> ok: get(collection, index) + removed -> error: get(collection, J) // TODO: if (j!=index)