From 5a095ca411a1eb8a40472597d67967bb997aab51 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Wed, 26 Feb 2020 08:52:54 -0800 Subject: [PATCH] [topl] Switched to low-level syntax. Summary: This syntax - is less confusing (according to several people who are not me); objectively, there's less magic under the hood - gives fine control over register number (because condition/action are separated) - lets one compare values of different arguments of the same call (e.g., one could have a transition that is taken only if two arguments of a method call are equal) Reviewed By: ngorogiannis Differential Revision: D20005403 fbshipit-source-id: fad8f3b3d --- infer/src/topl/Topl.ml | 68 ++++++++------ infer/src/topl/ToplAst.ml | 23 ++--- infer/src/topl/ToplAstOps.ml | 12 +++ infer/src/topl/ToplAstOps.mli | 10 +++ infer/src/topl/ToplAutomaton.ml | 31 +++---- infer/src/topl/ToplAutomaton.mli | 2 +- infer/src/topl/ToplLexer.mll | 6 +- infer/src/topl/ToplMonitor.ml | 88 ++++++++----------- infer/src/topl/ToplName.ml | 2 - infer/src/topl/ToplName.mli | 2 - infer/src/topl/ToplParser.mly | 38 ++++---- .../java/topl/baos/BaosTest.java | 11 +++ .../codetoanalyze/java/topl/baos/baos.topl | 16 ++-- .../codetoanalyze/java/topl/baos/issues.exp | 1 + .../java/topl/hasnext/hasnext.topl | 10 +-- .../java/topl/hasnext/issues.exp | 8 +- .../java/topl/servlet/ServletTests.java | 2 +- .../java/topl/servlet/servlet.topl | 14 +-- .../java/topl/skip/SkipAfterRemove.topl | 8 +- .../java/topl/slowIter/slowIter.topl | 8 +- 20 files changed, 195 insertions(+), 165 deletions(-) create mode 100644 infer/src/topl/ToplAstOps.ml create mode 100644 infer/src/topl/ToplAstOps.mli diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 43ea6a98b..e0d06aa51 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -43,24 +43,32 @@ 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 = Procname.hashable_name n in - let re = Str.regexp label.ToplAst.procedure_name in - let result = Str.string_match re name 0 in - tt "match name='%s' re='%s' result=%b@\n" name label.ToplAst.procedure_name result ; - result - | _ -> - false - in - let match_args () = - let same_length xs ys = Int.equal (Caml.List.compare_lengths xs ys) 0 in - Option.value_map label.ToplAst.arguments ~f:(same_length arg_ts) ~default:true +let evaluate_static_guard label_o (e_fun, arg_ts) = + let evaluate_nonany label = + let match_name () = + match e_fun with + | Exp.Const (Const.Cfun n) -> + (* TODO: perhaps handle inheritance *) + let name = Procname.hashable_name n in + let re = Str.regexp label.ToplAst.procedure_name in + let result = Str.string_match re name 0 in + tt " check name='%s'@\n" name ; result + | _ -> + tt " check name-unknown@\n" ; false + in + let pattern_len = Option.map ~f:List.length label.ToplAst.arguments in + let match_args () = + let arg_len = 1 + List.length arg_ts in + (* patterns include the return value *) + tt " check arg-len=%d@\n" arg_len ; + Option.value_map ~default:true ~f:(Int.equal arg_len) pattern_len + in + tt "match name-pattern='%s' arg-len-pattern=%a@\n" label.ToplAst.procedure_name + (Pp.option Int.pp) pattern_len ; + let log f = f () || (tt " match result FALSE@\n" ; false) in + log match_args && log match_name && (tt " match result TRUE@\n" ; true) in - match_name () && match_args () + Option.value_map ~default:true ~f:evaluate_nonany label_o (** For each transition in the automaton, evaluate its static guard. *) @@ -86,7 +94,7 @@ let set_transitions loc active_transitions = let call_save_args loc ret_id ret_typ arg_ts = let dummy_ret_id = Ident.create_fresh Ident.knormal in [| ToplUtils.topl_call dummy_ret_id Tvoid loc ToplName.save_args - ((Exp.Var ret_id, ret_typ) :: arg_ts) |] + (arg_ts @ [(Exp.Var ret_id, ret_typ)]) |] let call_execute loc = @@ -102,7 +110,7 @@ let instrument_instruction = function let is_interesting t active = active && not (ToplAutomaton.is_skip a t) in Array.existsi ~f:is_interesting active_transitions in - if not instrument then (* optimization*) [|i|] + if not instrument then (* optimization *) [|i|] else let i1s = set_transitions loc active_transitions in let i2s = call_save_args loc ret_id ret_typ arg_ts in @@ -117,15 +125,20 @@ let add_types tenv = let get_registers () = let a = Lazy.force automaton in let h = String.Table.create () in - let record = - let open ToplAst in - function - | SaveInRegister reg | EqualToRegister reg -> Hashtbl.set h ~key:reg ~data:() | _ -> () + let record reg = Hashtbl.set h ~key:reg ~data:() in + let record_value = function ToplAst.Register reg -> record reg | _ -> () in + let record_predicate = + ToplAst.( + function + | Binop (_, v1, v2) -> record_value v1 ; record_value v2 | Value v -> record_value v) + in + let record_assignment (reg, _) = record reg in + let record_label label = + List.iter ~f:record_predicate label.ToplAst.condition ; + List.iter ~f:record_assignment label.ToplAst.action in for i = 0 to ToplAutomaton.tcount a - 1 do - let label = (ToplAutomaton.transition a i).label in - record label.return ; - Option.iter ~f:(List.iter ~f:record) label.arguments + Option.iter ~f:record_label (ToplAutomaton.transition a i).label done ; Hashtbl.keys h in @@ -136,11 +149,10 @@ let add_types tenv = let register_field name = (ToplUtils.make_field (ToplName.reg name), ToplUtils.any_type, []) in let statics = let state = (ToplUtils.make_field ToplName.state, Typ.mk (Tint IInt), []) in - let retval = (ToplUtils.make_field ToplName.retval, ToplUtils.any_type, []) in let transitions = List.init (get_transitions_count ()) ~f:transition_field in let saved_args = List.init (ToplAutomaton.max_args (Lazy.force automaton)) ~f:saved_arg_field in let registers = List.map ~f:register_field (get_registers ()) in - List.concat [[retval; state]; transitions; saved_args; registers] + List.concat [[state]; transitions; saved_args; registers] in let _topl_class = Tenv.mk_struct tenv ToplUtils.topl_class_name ~statics in () diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml index 9bf8136a7..cbf50082b 100644 --- a/infer/src/topl/ToplAst.ml +++ b/infer/src/topl/ToplAst.ml @@ -11,13 +11,11 @@ type property_name = string [@@deriving compare, hash, sexp] type register_name = string -type constant = Exp.t - -type value_pattern = Ignore | SaveInRegister of register_name | EqualToRegister of register_name +type variable_name = string -type value = Constant of constant | Register of register_name | Binding of register_name +type constant = Exp.t -(* refers to the corresponding SaveInRegister, from the same label *) +type value = Constant of constant | Register of register_name | Binding of variable_name type binop = (* all return booleans *) | OpEq | OpNe | OpGe | OpGt | OpLe | OpLt @@ -26,21 +24,24 @@ type predicate = Binop of binop * value * value | Value of (* bool *) value type condition = predicate list (* conjunction *) +type assignment = register_name * variable_name + (** a regular expression *) type procedure_name_pattern = string -(* Well-formedness condition (not currently checked): For all x, there are no repeated occurrences -of (SaveInRegister x). *) +(* TODO(rgrigore): Check that variable names don't repeat. *) +(* TODO(rgrigore): Check that registers are written at most once. *) type label = - { arguments: value_pattern list option + { arguments: variable_name list option ; condition: condition - ; procedure_name: procedure_name_pattern - ; return: value_pattern } + ; action: assignment list + ; procedure_name: procedure_name_pattern } type vertex = string [@@deriving compare, hash, sexp] -type transition = {source: vertex; target: vertex; label: label} +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 diff --git a/infer/src/topl/ToplAstOps.ml b/infer/src/topl/ToplAstOps.ml new file mode 100644 index 000000000..f875aee53 --- /dev/null +++ b/infer/src/topl/ToplAstOps.ml @@ -0,0 +1,12 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +let pp_raw_label f {ToplAst.procedure_name} = Format.fprintf f "%s" procedure_name + +let pp_label = Pp.option pp_raw_label diff --git a/infer/src/topl/ToplAstOps.mli b/infer/src/topl/ToplAstOps.mli new file mode 100644 index 000000000..cfa226f17 --- /dev/null +++ b/infer/src/topl/ToplAstOps.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +val pp_label : Format.formatter -> ToplAst.label option -> unit diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index e569f089d..1097dae2e 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -25,7 +25,7 @@ type vindex = int type tindex = int -type transition = {source: vindex; target: vindex; label: ToplAst.label} +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 @@ -82,11 +82,13 @@ let make properties = let ps = List.map ~f:(fun p -> "\\|" ^ p ^ "\\.") p.ToplAst.prefixes in "^\\(" ^ String.concat ps ^ "\\)" ^ pname ^ "(" in + let prefix_label label = + ToplAst.{label with procedure_name= prefix_pname label.procedure_name} + 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 + let label = Option.map ~f:prefix_label t.ToplAst.label in {source; target; label} in List.map ~f p.ToplAst.transitions @@ -94,7 +96,7 @@ let make properties = Array.of_list (List.concat_map ~f properties) in Array.iteri transitions ~f:(fun i {source; target; label} -> - tt "transition%d %d -> %d on %s@\n" i source target label.ToplAst.procedure_name ) ; + tt "transition%d %d -> %d on %a@\n" i source target ToplAstOps.pp_label label ) ; let outgoing : tindex list array = let vcount = Array.length states in let a = Array.create ~len:vcount [] in @@ -102,11 +104,11 @@ let make properties = Array.iteri ~f transitions ; a in let max_args = - let f x t = - let y = Option.value_map ~default:0 ~f:List.length t.label.ToplAst.arguments in - Int.max x y - in - Array.fold ~init:0 ~f transitions + let llen l = Option.value_map ~default:0 ~f:List.length l.ToplAst.arguments in + let tlen t = Option.value_map ~default:0 ~f:llen t.label in + transitions |> Array.map ~f:tlen + |> Array.max_elt ~compare:Int.compare + |> Option.value ~default:0 |> succ in let nondets : bool array = let vcount = Array.length states in @@ -126,15 +128,8 @@ let make properties = List.iter ~f properties ; a in let skips : bool array = - let is_skip {source; target; label} = - let r = Int.equal source target in - let r = r && match label.return with Ignore -> true | _ -> false in - let r = r && Option.is_none label.arguments in - (* The next line conservatively evaluates if the regex on the label includes - * all other regexes. *) - let r = r && String.equal ".*" label.procedure_name in - r - in + (* 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} diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index 4d87817de..26b77eed6 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/infer/src/topl/ToplAutomaton.mli @@ -29,7 +29,7 @@ type vindex = int (* from 0 to vcount()-1, inclusive *) type tindex = int (* from 0 to tcount()-1, inclusive *) -type transition = {source: vindex; target: vindex; label: ToplAst.label} +type transition = {source: vindex; target: vindex; label: ToplAst.label option} val make : ToplAst.t list -> t diff --git a/infer/src/topl/ToplLexer.mll b/infer/src/topl/ToplLexer.mll index efcd54dfc..fbc024f47 100644 --- a/infer/src/topl/ToplLexer.mll +++ b/infer/src/topl/ToplLexer.mll @@ -35,8 +35,10 @@ rule raw_token = parse | ((' '* ("//" [^ '\n']*)? '\n')+ as x) (' '* as y) { new_line x y lexbuf } | ' '+ { raw_token lexbuf } | "->" { ARROW } - | '=' { ASGN } + | "=>" { ARROWARROW } | ':' { COLON } + | ":=" { COLONEQ } + | ';' { SEMI } | ',' { COMMA } | '(' { LP } | ')' { RP } @@ -49,12 +51,12 @@ rule raw_token = parse | ">=" { GE } | "==" { EQ } | "!=" { NE } - | "if" { IF } | "&&" { AND } | "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 } | eof { EOF } diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml index decb10076..74d508e00 100644 --- a/infer/src/topl/ToplMonitor.ml +++ b/infer/src/topl/ToplMonitor.ml @@ -202,15 +202,12 @@ let arguments_count proc_name = List.length (Procname.get_parameters proc_name) let generate_save_args automaton proc_name = if arguments_count proc_name < 1 then L.die InternalError "ToplMonitor: saveArgs() needs at least one argument" ; - let n = Int.min (arguments_count proc_name - 1) (ToplAutomaton.max_args automaton) in + let n = Int.min (arguments_count proc_name) (ToplAutomaton.max_args automaton) in let local_var = ToplUtils.local_var proc_name in procedure proc_name (sequence - ( assign (ToplUtils.static_var ToplName.retval) (local_var (ToplName.arg 0)) - :: List.init n ~f:(fun i -> - assign - (ToplUtils.static_var (ToplName.saved_arg i)) - (local_var (ToplName.arg (i + 1))) ) )) + (List.init n ~f:(fun i -> + assign (ToplUtils.static_var (ToplName.saved_arg i)) (local_var (ToplName.arg i)) ))) let generate_execute automaton proc_name = @@ -218,9 +215,8 @@ let generate_execute automaton proc_name = let fresh_var () = Exp.Var (Ident.create_fresh Ident.knormal) in let calls = List.init (ToplAutomaton.vcount automaton) ~f:call_execute_state in let havoc_event_data = - assign (ToplUtils.static_var ToplName.retval) (fresh_var ()) - :: List.init (ToplAutomaton.max_args automaton) ~f:(fun i -> - assign (ToplUtils.static_var (ToplName.saved_arg i)) (fresh_var ()) ) + List.init (ToplAutomaton.max_args automaton) ~f:(fun i -> + assign (ToplUtils.static_var (ToplName.saved_arg i)) (fresh_var ()) ) in let havoc_transitions = List.init (ToplAutomaton.tcount automaton) ~f:(fun i -> @@ -235,33 +231,34 @@ let generate_execute_state automaton proc_name = let re = Str.regexp "execute_state_\\([0-9]*\\)$" in let mname = Procname.get_method proc_name in if Str.string_match re mname 0 then int_of_string (Str.matched_group 1 mname) - else L.die InternalError "Topl.Monitor.generate_execute_state called for %s" mname + else L.die InternalError "ToplMonitor.generate_execute_state called for %s" mname in - let condition maybe t : Exp.t = - let conjunct variable pattern = - let open ToplAst in - match pattern with - | Ignore | SaveInRegister _ -> - [] (* true *) - | EqualToRegister i -> - [Exp.eq variable (ToplUtils.static_var (ToplName.reg i))] - in - let label = (ToplAutomaton.transition automaton t).label in - let explicit_condition = - (* computed from label.ToplAst.condition *) - let binding_of : ToplAst.register_name -> ToplName.t = - (* The _exn functions here should fail only if [label] is ill-formed. *) + let binding_of t : ToplAst.variable_name -> ToplName.t = + match (ToplAutomaton.transition automaton t).label with + | None -> + fun _ -> L.die InternalError "ToplMonitor: There are no bindings for any-labels." + | Some label -> let table = String.Table.create () in - let add n = function - | ToplAst.SaveInRegister i -> - Hashtbl.add_exn ~key:i ~data:n table - | _ -> + let add n v = + match Hashtbl.add ~key:v ~data:n table with + | `Duplicate -> + L.die UserError "ToplMonitor: ill-formed label (%s bound multiple times)" v + | `Ok -> () in - add ToplName.retval label.ToplAst.return ; Option.iter ~f:(List.iteri ~f:(fun i -> add (ToplName.saved_arg i))) label.ToplAst.arguments ; - Hashtbl.find_exn table - in + let find v = + match Hashtbl.find table v with + | Some arg -> + arg + | None -> + L.die UserError "ToplMonitor: ill-formed label (%s not bound)" v + in + find + in + let condition maybe t : Exp.t = + let binding_of = binding_of t in + let make_condition label = let exp_of_value = let open ToplAst in function @@ -294,29 +291,24 @@ let generate_execute_state automaton proc_name = in List.map ~f:predicate label.ToplAst.condition in + let condition = + Option.value_map ~default:[] ~f:make_condition (ToplAutomaton.transition automaton t).label + in let all_conjuncts = - let arg_conjunct i pattern = conjunct (ToplUtils.static_var (ToplName.saved_arg i)) pattern in - List.concat - ( Option.value_map ~default:[] ~f:(fun x -> [x]) maybe - :: [ToplUtils.static_var (ToplName.transition t)] - :: explicit_condition - :: conjunct (ToplUtils.static_var ToplName.retval) label.ToplAst.return - :: Option.value_map ~default:[] ~f:(List.mapi ~f:arg_conjunct) label.ToplAst.arguments ) + Option.to_list maybe @ (ToplUtils.static_var (ToplName.transition t) :: condition) in Exp.and_nary all_conjuncts in let skip : node_generator = sequence [] in let action t : node_generator = - let step variable pattern = - match pattern with - | ToplAst.SaveInRegister i -> - assign (ToplUtils.static_var (ToplName.reg i)) variable - | _ -> - skip - in + let binding_of = binding_of t in let transition = ToplAutomaton.transition automaton t in let all_actions = - let arg_action i pattern = step (ToplUtils.static_var (ToplName.saved_arg i)) pattern in + let reg_var_assign (reg, var) = + assign (ToplUtils.static_var (ToplName.reg reg)) (ToplUtils.static_var (binding_of var)) + in + let l_assign l = List.map ~f:reg_var_assign l.ToplAst.action in + let lo_assign = Option.value_map ~default:[] ~f:l_assign in stmt_node [ Sil.Store { e1= ToplUtils.static_var ToplName.state @@ -324,9 +316,7 @@ let generate_execute_state automaton proc_name = ; typ= Typ.mk (Tint IInt) ; e2= Exp.int (IntLit.of_int transition.target) ; loc= sourcefile_location () } ] - :: step (ToplUtils.static_var ToplName.retval) transition.label.ToplAst.return - :: Option.value_map ~default:[] ~f:(List.mapi ~f:arg_action) - transition.label.ToplAst.arguments + :: lo_assign transition.label in sequence all_actions in diff --git a/infer/src/topl/ToplName.ml b/infer/src/topl/ToplName.ml index b0cf11d39..1dd441ade 100644 --- a/infer/src/topl/ToplName.ml +++ b/infer/src/topl/ToplName.ml @@ -17,8 +17,6 @@ let transition = p "transition%d" let arg = p "arg%d" -let retval = "retval" - let saved_arg = p "savedArg%d" let reg = p "reg_%s" diff --git a/infer/src/topl/ToplName.mli b/infer/src/topl/ToplName.mli index 646c7fdec..8b226b9c5 100644 --- a/infer/src/topl/ToplName.mli +++ b/infer/src/topl/ToplName.mli @@ -15,8 +15,6 @@ val transition : int -> t val arg : int -> t -val retval : t - val saved_arg : int -> t val reg : string -> t diff --git a/infer/src/topl/ToplParser.mly b/infer/src/topl/ToplParser.mly index aa4fcab8f..5c8c1ab69 100644 --- a/infer/src/topl/ToplParser.mly +++ b/infer/src/topl/ToplParser.mly @@ -15,14 +15,14 @@ %token UID %token AND %token ARROW -%token ASGN +%token ARROWARROW %token COLON +%token COLONEQ %token COMMA %token EOF %token EQ %token GE %token GT -%token IF %token LC %token LE %token LP @@ -34,7 +34,9 @@ %token PROPERTY %token RC %token RP +%token SEMI %token STAR +%token WHEN %start properties @@ -60,16 +62,14 @@ transition: state: i=identifier { i } label: - return=value_pattern ASGN cp=call_pattern condition=condition? - { let procedure_name, arguments = cp in - let condition = Option.value condition ~default:[] in - ToplAst.{return; procedure_name; arguments; condition} } - | cp=call_pattern condition=condition? - { let procedure_name, arguments = cp in - let condition = Option.value condition ~default:[] in - ToplAst.{return=Ignore; procedure_name; arguments; condition} } + STAR { None } + | procedure_name=procedure_pattern arguments=arguments_pattern? + condition=condition? action=action? + { let condition = Option.value ~default:[] condition in + let action = Option.value ~default:[] action in + Some ToplAst.{ arguments; condition; action; procedure_name } } -condition: IF ps=condition_expression { ps } +condition: WHEN ps=condition_expression { ps } condition_expression: p=predicate ps=and_predicate* { p :: ps } @@ -80,7 +80,7 @@ predicate: value: id=LID { ToplAst.Register id } - | id=UID { ToplAst.Binding (String.uncapitalize id) } + | id=UID { ToplAst.Binding id } | x=INTEGER { ToplAst.Constant (Exp.Const (Const.Cint (IntLit.of_int x))) } | x=STRING { ToplAst.Constant (Exp.Const (Const.Cstr x)) } @@ -96,19 +96,17 @@ predop: and_predicate: AND p=predicate { p } -call_pattern: p=procedure_pattern a=arguments_pattern? { (p, a) } - procedure_pattern: i=identifier { i } | s=STRING { s } - | STAR { ".*" } -arguments_pattern: LP a=separated_list(COMMA, value_pattern) RP { a } +arguments_pattern: LP a=separated_list(COMMA, UID) RP { a } + +action: + ARROWARROW a=separated_nonempty_list(SEMI, assignment) { a } -value_pattern: - i=LID { ToplAst.EqualToRegister i } - | i=UID { ToplAst.SaveInRegister (String.uncapitalize i) } - | STAR { ToplAst.Ignore } +assignment: + r=LID COLONEQ v=UID { (r, v) } identifier: i=LID { i } | i=UID { i } diff --git a/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java b/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java index b661c95d1..b76b762a1 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java +++ b/infer/tests/codetoanalyze/java/topl/baos/BaosTest.java @@ -63,4 +63,15 @@ class BaosTest { y.finish(); return x.toByteArray(); } + + static byte[] FP_eOk(final byte[] src) throws IOException { + ByteArrayOutputStream x = new ByteArrayOutputStream(src.length); + GZIPOutputStream y = new GZIPOutputStream(x); + try { + y.write(src); + y.finish(); + } catch (Exception e) { + } + return x.toByteArray(); + } } diff --git a/infer/tests/codetoanalyze/java/topl/baos/baos.topl b/infer/tests/codetoanalyze/java/topl/baos/baos.topl index 539fc28f2..76bc0ce56 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/baos.topl +++ b/infer/tests/codetoanalyze/java/topl/baos/baos.topl @@ -1,11 +1,11 @@ property BaosRetrieveWithoutFlush nondet (start) start -> start: * - start -> valid: ".*OutputStream"(X, Y) - valid -> invalid: ".*OutputStream.write.*"(x, *) - valid -> invalid: ".*OutputStream.write.*"(x, *, *) - valid -> invalid: ".*OutputStream.write.*"(x, *, *, *) - invalid -> valid: ".*OutputStream.flush"(x) - invalid -> valid: ".*OutputStream.close"(x) - invalid -> error: "ByteArrayOutputStream.toByteArray"(y) - invalid -> error: "ByteArrayOutputStream.toString"(y) + start -> valid: ".*OutputStream"(X, Y, Ret) => x := X; y := Y + valid -> invalid: ".*OutputStream.write.*"(X, Ia, Ret) when X == x + valid -> invalid: ".*OutputStream.write.*"(X, Ia, Ib, Ret) when X == x + valid -> invalid: ".*OutputStream.write.*"(X, Ia, Ib, Ic, Ret) when X == x + invalid -> valid: ".*OutputStream.flush"(X, Ret) when X == x + invalid -> valid: ".*OutputStream.close"(X, Ret) when X == x + invalid -> error: "ByteArrayOutputStream.toByteArray"(Y, Ret) when Y == y + invalid -> error: "ByteArrayOutputStream.toString"(Y, Ret) when Y == y diff --git a/infer/tests/codetoanalyze/java/topl/baos/issues.exp b/infer/tests/codetoanalyze/java/topl/baos/issues.exp index 02a4cefe4..7831016ed 100644 --- a/infer/tests/codetoanalyze/java/topl/baos/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/baos/issues.exp @@ -1,4 +1,5 @@ codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_dOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.FP_eOk(byte[]):byte[], 0, TOPL_ERROR, no_bucket, ERROR, [] codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.aBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.bBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl b/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl index c9a598ed3..1a7b36740 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl +++ b/infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl @@ -4,9 +4,9 @@ property HasNext prefix "Scanner" nondet (start) start -> start: * - start -> invalid: I = iterator(*) - start -> invalid: Scanner(I, *) // For constructors, biabduction has "this" as first argument - invalid -> valid: B = hasNext(i) if B != 0 // in SIL, "true" is encoded as "not 0" - valid -> invalid: next(i) - invalid -> error: next(i) + 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 + invalid -> valid: hasNext(Iter, Ret) when Ret != 0 && Iter == i // in SIL, "true" is encoded as "not 0" + valid -> invalid: next(Iter, IgnoreRet) when Iter == i + invalid -> error: next(Iter, IgnoreRet) when Iter == i diff --git a/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp b/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp index de2b067e2..47737f0e2 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/hasnext/issues.exp @@ -1,7 +1,7 @@ codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextBad(...),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(),return from a call to void Property.execute()] -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),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(),return from a call to void Property.execute(),start of procedure getSingleElementOk(...)] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextBad(...),start of procedure saveArgs(...),return from a call to void Property.saveArgs(List,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(),return from a call to void Property.execute()] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),start of procedure saveArgs(...),return from a call to void Property.saveArgs(List,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(),return from a call to void Property.execute(),start of procedure getSingleElementOk(...)] codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [] -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralOk(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),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(),return from a call to void Property.execute()] -codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextOk(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),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(),return from a call to void Property.execute()] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextInterproceduralOk(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),start of procedure saveArgs(...),return from a call to void Property.saveArgs(List,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(),return from a call to void Property.execute()] +codetoanalyze/java/topl/hasnext/Iterators.java, Iterators.hasNextOk(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),start of procedure saveArgs(...),return from a call to void Property.saveArgs(List,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(),return from a call to void Property.execute()] codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] diff --git a/infer/tests/codetoanalyze/java/topl/servlet/ServletTests.java b/infer/tests/codetoanalyze/java/topl/servlet/ServletTests.java index 4e1163479..776c465a7 100644 --- a/infer/tests/codetoanalyze/java/topl/servlet/ServletTests.java +++ b/infer/tests/codetoanalyze/java/topl/servlet/ServletTests.java @@ -20,8 +20,8 @@ class ServletTests { } void bBad(ServletResponse response) throws IOException { - PrintWriter w = response.getWriter(); ServletOutputStream s = response.getOutputStream(); + PrintWriter w = response.getWriter(); } void cBad(ServletRequest request, ServletResponse response, RequestDispatcher dispatcher) diff --git a/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl b/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl index 6b4f4259c..005882cd4 100644 --- a/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl +++ b/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl @@ -10,16 +10,16 @@ property InterleavedResponse prefix "ServletResponse" nondet (start) start -> start: * - start -> gotWriter: getWriter(R) - start -> gotStream: getOutputStream(R) - gotWriter -> error: getOutputStream(r) - gotStream -> error: getWriter(r) + start -> gotWriter: getWriter(R, IgnoreRet) => r := R + start -> gotStream: getOutputStream(R, IgnoreRet) => r := R + gotWriter -> error: getOutputStream(R, IgnoreRet) when R == r + gotStream -> error: getWriter(R, IgnoreRet) when R == r property ForwardUncommitted message "A ServletResponse was forwarded before being committed." nondet (start) start -> start: * - start -> gotChannel: C = "ServletResponse.\\(getWriter\\|getOutputStream\\)"(R) - gotChannel -> ok: "\\(PrintWriter\\|ServletOutputStream\\).flush.*"(c) - gotChannel -> error: "RequestDispatcher.forward"(*, *, r) + start -> gotChannel: "ServletResponse.\\(getWriter\\|getOutputStream\\)"(R, C) => r := R; c := C + gotChannel -> ok: "\\(PrintWriter\\|ServletOutputStream\\).flush.*"(C, IgnoreRet) when C == c + gotChannel -> error: "RequestDispatcher.forward"(IgnoreDispatcher, IgnoreRequest, Response, IgnoreRet) when Response == r diff --git a/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl b/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl index fbc21e954..3d694c5a5 100644 --- a/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl +++ b/infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl @@ -2,6 +2,8 @@ property SkipAfterRemove prefix "ArrayList" nondet (start) start -> start: * - start -> removed: remove(Collection, Index) - removed -> ok: get(collection, index) - removed -> error: get(collection, J) if J != index + start -> removed: remove(Collection, Index, IgnoreRet) => c := Collection; i := Index + removed -> ok: get(Collection, Index, IgnoreRet) when i == Index && c == Collection + removed -> error: get(Collection, Index, IgnoreRet) when i != Index && c == Collection => j := Index + // TODO(rgrigore): Dropping the assignment above makes it slow. Also, swapping the conjuncts! + // This is weird prover-stuff to be investigated. diff --git a/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl index 54500efe0..9749c751b 100644 --- a/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl +++ b/infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl @@ -1,8 +1,8 @@ property ShouldUseEntries nondet (start iteratingKeys) start -> start: * - start -> gotKeys: S = "Map.keySet"(M) - gotKeys -> iteratingKeys: I = "Set.iterator"(s) + start -> gotKeys: "Map.keySet"(M, S) => m := M; s := S + gotKeys -> iteratingKeys: "Set.iterator"(S, I) when S == s => i := I iteratingKeys -> iteratingKeys: * - iteratingKeys -> gotOneKey: K = "Iterator.next"(i) - gotOneKey -> error: ".*Map.get"(m, k) + iteratingKeys -> gotOneKey: "Iterator.next"(I, K) when I == i => k := K + gotOneKey -> error: ".*Map.get"(M, K, IgnoreRet) when M == m && K == k