pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[topl] Switched to low-level syntax.

Browse Source 
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
master
Radu Grigore 5 years ago committed by Facebook Github Bot
parent 2888a90e2a
commit 5a095ca411
20 changed files with 195 additions and 165 deletions
Show Stats Download Patch File Download Diff File

68
infer/src/topl/Topl.ml
Unescape View File

@ -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 (** 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. *) transition label. Possible optimization: also evaluate if arguments equal certain constants. *)
let evaluate_static_guard label (e_fun, arg_ts) = let evaluate_static_guard label_o (e_fun, arg_ts) =
let match_name () = let evaluate_nonany label =
match e_fun with let match_name () =
| Exp.Const (Const.Cfun n) -> match e_fun with
(* TODO: perhaps handle inheritance *) | Exp.Const (Const.Cfun n) ->
let name = Procname.hashable_name n in (* TODO: perhaps handle inheritance *)
let re = Str.regexp label.ToplAst.procedure_name in let name = Procname.hashable_name n in
let result = Str.string_match re name 0 in let re = Str.regexp label.ToplAst.procedure_name in
tt "match name='%s' re='%s' result=%b@\n" name label.ToplAst.procedure_name result ; let result = Str.string_match re name 0 in
result tt " check name='%s'@\n" name ; result
| _ -> | _ ->
false tt " check name-unknown@\n" ; false
in in
let match_args () = let pattern_len = Option.map ~f:List.length label.ToplAst.arguments in
let same_length xs ys = Int.equal (Caml.List.compare_lengths xs ys) 0 in let match_args () =
Option.value_map label.ToplAst.arguments ~f:(same_length arg_ts) ~default:true 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 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. *) (** 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 call_save_args loc ret_id ret_typ arg_ts =
let dummy_ret_id = Ident.create_fresh Ident.knormal in let dummy_ret_id = Ident.create_fresh Ident.knormal in
[| ToplUtils.topl_call dummy_ret_id Tvoid loc ToplName.save_args [| 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 = 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 let is_interesting t active = active && not (ToplAutomaton.is_skip a t) in
Array.existsi ~f:is_interesting active_transitions Array.existsi ~f:is_interesting active_transitions
in in
if not instrument then (* optimization*) [|i|] if not instrument then (* optimization *) [|i|]
else else
let i1s = set_transitions loc active_transitions in let i1s = set_transitions loc active_transitions in
let i2s = call_save_args loc ret_id ret_typ arg_ts 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 get_registers () =
let a = Lazy.force automaton in let a = Lazy.force automaton in
let h = String.Table.create () in let h = String.Table.create () in
let record = let record reg = Hashtbl.set h ~key:reg ~data:() in
let open ToplAst in let record_value = function ToplAst.Register reg -> record reg | _ -> () in
function let record_predicate =
| SaveInRegister reg | EqualToRegister reg -> Hashtbl.set h ~key:reg ~data:() | _ -> () 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 in
for i = 0 to ToplAutomaton.tcount a - 1 do for i = 0 to ToplAutomaton.tcount a - 1 do
let label = (ToplAutomaton.transition a i).label in Option.iter ~f:record_label (ToplAutomaton.transition a i).label
record label.return ;
Option.iter ~f:(List.iter ~f:record) label.arguments
done ; done ;
Hashtbl.keys h Hashtbl.keys h
in in
@ -136,11 +149,10 @@ let add_types tenv =
let register_field name = (ToplUtils.make_field (ToplName.reg name), ToplUtils.any_type, []) in let register_field name = (ToplUtils.make_field (ToplName.reg name), ToplUtils.any_type, []) in
let statics = let statics =
let state = (ToplUtils.make_field ToplName.state, Typ.mk (Tint IInt), []) in 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 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 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 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 in
let _topl_class = Tenv.mk_struct tenv ToplUtils.topl_class_name ~statics in let _topl_class = Tenv.mk_struct tenv ToplUtils.topl_class_name ~statics in
() ()

23
infer/src/topl/ToplAst.ml
Unescape View File

@ -11,13 +11,11 @@ type property_name = string [@@deriving compare, hash, sexp]
type register_name = string type register_name = string
type constant = Exp.t type variable_name = string
type value_pattern = Ignore | SaveInRegister of register_name | EqualToRegister of register_name
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 *) type binop = (* all return booleans *)
| OpEq | OpNe | OpGe | OpGt | OpLe | OpLt | 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 condition = predicate list (* conjunction *)
type assignment = register_name * variable_name
(** a regular expression *) (** a regular expression *)
type procedure_name_pattern = string type procedure_name_pattern = string
(* Well-formedness condition (not currently checked): For all x, there are no repeated occurrences (* TODO(rgrigore): Check that variable names don't repeat. *)
of (SaveInRegister x). *) (* TODO(rgrigore): Check that registers are written at most once. *)
type label = type label =
{ arguments: value_pattern list option { arguments: variable_name list option
; condition: condition ; condition: condition
; procedure_name: procedure_name_pattern ; action: assignment list
; return: value_pattern } ; procedure_name: procedure_name_pattern }
type vertex = string [@@deriving compare, hash, sexp] 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 = type t =
{ name: property_name { name: property_name
; message: string option ; message: string option

12
infer/src/topl/ToplAstOps.ml
Unescape View File

@ -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

10
infer/src/topl/ToplAstOps.mli
Unescape View File

@ -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

31
infer/src/topl/ToplAutomaton.ml
Unescape View File

@ -25,7 +25,7 @@ type vindex = int
type tindex = 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 (** - INV1: Array.length states = Array.length outgoing = Array.length nondets
- INV2: Array.length transitions = Array.length skips - 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 let ps = List.map ~f:(fun p -> "\\|" ^ p ^ "\\.") p.ToplAst.prefixes in
"^\\(" ^ String.concat ps ^ "\\)" ^ pname ^ "(" "^\\(" ^ String.concat ps ^ "\\)" ^ pname ^ "("
in in
let prefix_label label =
ToplAst.{label with procedure_name= prefix_pname label.procedure_name}
in
let f t = let f t =
let source = vindex ToplAst.(p.name, t.source) in let source = vindex ToplAst.(p.name, t.source) in
let target = vindex ToplAst.(p.name, t.target) in let target = vindex ToplAst.(p.name, t.target) in
let procedure_name = prefix_pname ToplAst.(t.label.procedure_name) in let label = Option.map ~f:prefix_label t.ToplAst.label in
let label = {t.ToplAst.label with procedure_name} in
{source; target; label} {source; target; label}
in in
List.map ~f p.ToplAst.transitions List.map ~f p.ToplAst.transitions
@ -94,7 +96,7 @@ let make properties =
Array.of_list (List.concat_map ~f properties) Array.of_list (List.concat_map ~f properties)
in in
Array.iteri transitions ~f:(fun i {source; target; label} -> 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 outgoing : tindex list array =
let vcount = Array.length states in let vcount = Array.length states in
let a = Array.create ~len:vcount [] in let a = Array.create ~len:vcount [] in
@ -102,11 +104,11 @@ let make properties =
Array.iteri ~f transitions ; a Array.iteri ~f transitions ; a
in in
let max_args = let max_args =
let f x t = let llen l = Option.value_map ~default:0 ~f:List.length l.ToplAst.arguments in
let y = Option.value_map ~default:0 ~f:List.length t.label.ToplAst.arguments in let tlen t = Option.value_map ~default:0 ~f:llen t.label in
Int.max x y transitions |> Array.map ~f:tlen
in |> Array.max_elt ~compare:Int.compare
Array.fold ~init:0 ~f transitions |> Option.value ~default:0 |> succ
in in
let nondets : bool array = let nondets : bool array =
let vcount = Array.length states in let vcount = Array.length states in
@ -126,15 +128,8 @@ let make properties =
List.iter ~f properties ; a List.iter ~f properties ; a
in in
let skips : bool array = let skips : bool array =
let is_skip {source; target; label} = (* TODO(rgrigore): Rename "anys"? *)
let r = Int.equal source target in let is_skip {label} = Option.is_none label 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
Array.map ~f:is_skip transitions Array.map ~f:is_skip transitions
in in
{states; nondets; transitions; skips; outgoing; vindex; max_args} {states; nondets; transitions; skips; outgoing; vindex; max_args}

2
infer/src/topl/ToplAutomaton.mli
Unescape View File

@ -29,7 +29,7 @@ type vindex = int (* from 0 to vcount()-1, inclusive *)
type tindex = int (* from 0 to tcount()-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 val make : ToplAst.t list -> t

6
infer/src/topl/ToplLexer.mll
Unescape View File

@ -35,8 +35,10 @@ rule raw_token = parse
| ((' '* ("//" [^ '\n']*)? '\n')+ as x) (' '* as y) { new_line x y lexbuf } | ((' '* ("//" [^ '\n']*)? '\n')+ as x) (' '* as y) { new_line x y lexbuf }
| ' '+ { raw_token lexbuf } | ' '+ { raw_token lexbuf }
| "->" { ARROW } | "->" { ARROW }
| '=' { ASGN } | "=>" { ARROWARROW }
| ':' { COLON } | ':' { COLON }
| ":=" { COLONEQ }
| ';' { SEMI }
| ',' { COMMA } | ',' { COMMA }
| '(' { LP } | '(' { LP }
| ')' { RP } | ')' { RP }
@ -49,12 +51,12 @@ rule raw_token = parse
| ">=" { GE } | ">=" { GE }
| "==" { EQ } | "==" { EQ }
| "!=" { NE } | "!=" { NE }
| "if" { IF }
| "&&" { AND } | "&&" { AND }
| "prefix" { PREFIX } | "prefix" { PREFIX }
| "property" { PROPERTY } | "property" { PROPERTY }
| "message" { MESSAGE } | "message" { MESSAGE }
| "nondet" { NONDET } | "nondet" { NONDET }
| "when" { WHEN }
| ['a'-'z'] id_tail as id { LID id } | ['a'-'z'] id_tail as id { LID id }
| ['A'-'Z'] id_tail as id { UID id } | ['A'-'Z'] id_tail as id { UID id }
| eof { EOF } | eof { EOF }

88
infer/src/topl/ToplMonitor.ml
Unescape View File

@ -202,15 +202,12 @@ let arguments_count proc_name = List.length (Procname.get_parameters proc_name)
let generate_save_args automaton proc_name = let generate_save_args automaton proc_name =
if arguments_count proc_name < 1 then if arguments_count proc_name < 1 then
L.die InternalError "ToplMonitor: saveArgs() needs at least one argument" ; 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 let local_var = ToplUtils.local_var proc_name in
procedure proc_name procedure proc_name
(sequence (sequence
( assign (ToplUtils.static_var ToplName.retval) (local_var (ToplName.arg 0)) (List.init n ~f:(fun i ->
:: List.init n ~f:(fun i -> assign (ToplUtils.static_var (ToplName.saved_arg i)) (local_var (ToplName.arg i)) )))
assign
(ToplUtils.static_var (ToplName.saved_arg i))
(local_var (ToplName.arg (i + 1))) ) ))
let generate_execute automaton proc_name = 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 fresh_var () = Exp.Var (Ident.create_fresh Ident.knormal) in
let calls = List.init (ToplAutomaton.vcount automaton) ~f:call_execute_state in let calls = List.init (ToplAutomaton.vcount automaton) ~f:call_execute_state in
let havoc_event_data = let havoc_event_data =
assign (ToplUtils.static_var ToplName.retval) (fresh_var ()) List.init (ToplAutomaton.max_args automaton) ~f:(fun i ->
:: List.init (ToplAutomaton.max_args automaton) ~f:(fun i -> assign (ToplUtils.static_var (ToplName.saved_arg i)) (fresh_var ()) )
assign (ToplUtils.static_var (ToplName.saved_arg i)) (fresh_var ()) )
in in
let havoc_transitions = let havoc_transitions =
List.init (ToplAutomaton.tcount automaton) ~f:(fun i -> 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 re = Str.regexp "execute_state_\\([0-9]*\\)$" in
let mname = Procname.get_method proc_name 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) 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 in
let condition maybe t : Exp.t = let binding_of t : ToplAst.variable_name -> ToplName.t =
let conjunct variable pattern = match (ToplAutomaton.transition automaton t).label with
let open ToplAst in | None ->
match pattern with fun _ -> L.die InternalError "ToplMonitor: There are no bindings for any-labels."
| Ignore | SaveInRegister _ -> | Some label ->
[] (* 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 table = String.Table.create () in let table = String.Table.create () in
let add n = function let add n v =
| ToplAst.SaveInRegister i -> match Hashtbl.add ~key:v ~data:n table with
Hashtbl.add_exn ~key:i ~data:n table | `Duplicate ->
| _ -> L.die UserError "ToplMonitor: ill-formed label (%s bound multiple times)" v
| `Ok ->
() ()
in in
add ToplName.retval label.ToplAst.return ;
Option.iter ~f:(List.iteri ~f:(fun i -> add (ToplName.saved_arg i))) label.ToplAst.arguments ; Option.iter ~f:(List.iteri ~f:(fun i -> add (ToplName.saved_arg i))) label.ToplAst.arguments ;
Hashtbl.find_exn table let find v =
in 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 exp_of_value =
let open ToplAst in let open ToplAst in
function function
@ -294,29 +291,24 @@ let generate_execute_state automaton proc_name =
in in
List.map ~f:predicate label.ToplAst.condition List.map ~f:predicate label.ToplAst.condition
in in
let condition =
Option.value_map ~default:[] ~f:make_condition (ToplAutomaton.transition automaton t).label
in
let all_conjuncts = let all_conjuncts =
let arg_conjunct i pattern = conjunct (ToplUtils.static_var (ToplName.saved_arg i)) pattern in Option.to_list maybe @ (ToplUtils.static_var (ToplName.transition t) :: condition)
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 )
in in
Exp.and_nary all_conjuncts Exp.and_nary all_conjuncts
in in
let skip : node_generator = sequence [] in let skip : node_generator = sequence [] in
let action t : node_generator = let action t : node_generator =
let step variable pattern = let binding_of = binding_of t in
match pattern with
| ToplAst.SaveInRegister i ->
assign (ToplUtils.static_var (ToplName.reg i)) variable
| _ ->
skip
in
let transition = ToplAutomaton.transition automaton t in let transition = ToplAutomaton.transition automaton t in
let all_actions = 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 stmt_node
[ Sil.Store [ Sil.Store
{ e1= ToplUtils.static_var ToplName.state { e1= ToplUtils.static_var ToplName.state
@ -324,9 +316,7 @@ let generate_execute_state automaton proc_name =
; typ= Typ.mk (Tint IInt) ; typ= Typ.mk (Tint IInt)
; e2= Exp.int (IntLit.of_int transition.target) ; e2= Exp.int (IntLit.of_int transition.target)
; loc= sourcefile_location () } ] ; loc= sourcefile_location () } ]
:: step (ToplUtils.static_var ToplName.retval) transition.label.ToplAst.return :: lo_assign transition.label
:: Option.value_map ~default:[] ~f:(List.mapi ~f:arg_action)
transition.label.ToplAst.arguments
in in
sequence all_actions sequence all_actions
in in

2
infer/src/topl/ToplName.ml
Unescape View File

@ -17,8 +17,6 @@ let transition = p "transition%d"
let arg = p "arg%d" let arg = p "arg%d"
let retval = "retval"
let saved_arg = p "savedArg%d" let saved_arg = p "savedArg%d"
let reg = p "reg_%s" let reg = p "reg_%s"

2
infer/src/topl/ToplName.mli
Unescape View File

@ -15,8 +15,6 @@ val transition : int -> t
val arg : int -> t val arg : int -> t
val retval : t
val saved_arg : int -> t val saved_arg : int -> t
val reg : string -> t val reg : string -> t

38
infer/src/topl/ToplParser.mly
Unescape View File

@ -15,14 +15,14 @@
%token <string> UID %token <string> UID
%token AND %token AND
%token ARROW %token ARROW
%token ASGN %token ARROWARROW
%token COLON %token COLON
%token COLONEQ
%token COMMA %token COMMA
%token EOF %token EOF
%token EQ %token EQ
%token GE %token GE
%token GT %token GT
%token IF
%token LC %token LC
%token LE %token LE
%token LP %token LP
@ -34,7 +34,9 @@
%token PROPERTY %token PROPERTY
%token RC %token RC
%token RP %token RP
%token SEMI
%token STAR %token STAR
%token WHEN
%start <ToplAst.t list> properties %start <ToplAst.t list> properties
@ -60,16 +62,14 @@ transition:
state: i=identifier { i } state: i=identifier { i }
label: label:
return=value_pattern ASGN cp=call_pattern condition=condition? STAR { None }
{ let procedure_name, arguments = cp in | procedure_name=procedure_pattern arguments=arguments_pattern?
let condition = Option.value condition ~default:[] in condition=condition? action=action?
ToplAst.{return; procedure_name; arguments; condition} } { let condition = Option.value ~default:[] condition in
| cp=call_pattern condition=condition? let action = Option.value ~default:[] action in
{ let procedure_name, arguments = cp in Some ToplAst.{ arguments; condition; action; procedure_name } }
let condition = Option.value condition ~default:[] in
ToplAst.{return=Ignore; procedure_name; arguments; condition} }
condition: IF ps=condition_expression { ps } condition: WHEN ps=condition_expression { ps }
condition_expression: p=predicate ps=and_predicate* { p :: ps } condition_expression: p=predicate ps=and_predicate* { p :: ps }
@ -80,7 +80,7 @@ predicate:
value: value:
id=LID { ToplAst.Register id } 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=INTEGER { ToplAst.Constant (Exp.Const (Const.Cint (IntLit.of_int x))) }
| x=STRING { ToplAst.Constant (Exp.Const (Const.Cstr x)) } | x=STRING { ToplAst.Constant (Exp.Const (Const.Cstr x)) }
@ -96,19 +96,17 @@ predop:
and_predicate: AND p=predicate { p } and_predicate: AND p=predicate { p }
call_pattern: p=procedure_pattern a=arguments_pattern? { (p, a) }
procedure_pattern: procedure_pattern:
i=identifier { i } i=identifier { i }
| s=STRING { s } | 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: assignment:
i=LID { ToplAst.EqualToRegister i } r=LID COLONEQ v=UID { (r, v) }
| i=UID { ToplAst.SaveInRegister (String.uncapitalize i) }
| STAR { ToplAst.Ignore }
identifier: i=LID { i } | i=UID { i } identifier: i=LID { i } | i=UID { i }

11
infer/tests/codetoanalyze/java/topl/baos/BaosTest.java
Unescape View File

@ -63,4 +63,15 @@ class BaosTest {
y.finish(); y.finish();
return x.toByteArray(); 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();
}
} }

16
infer/tests/codetoanalyze/java/topl/baos/baos.topl
Unescape View File

@ -1,11 +1,11 @@
property BaosRetrieveWithoutFlush property BaosRetrieveWithoutFlush
nondet (start) nondet (start)
start -> start: * start -> start: *
start -> valid: ".*OutputStream"(X, Y) start -> valid: ".*OutputStream"(X, Y, Ret) => x := X; y := Y
valid -> invalid: ".*OutputStream.write.*"(x, *) valid -> invalid: ".*OutputStream.write.*"(X, Ia, Ret) when X == x
valid -> invalid: ".*OutputStream.write.*"(x, *, *) valid -> invalid: ".*OutputStream.write.*"(X, Ia, Ib, Ret) when X == x
valid -> invalid: ".*OutputStream.write.*"(x, *, *, *) valid -> invalid: ".*OutputStream.write.*"(X, Ia, Ib, Ic, Ret) when X == x
invalid -> valid: ".*OutputStream.flush"(x) invalid -> valid: ".*OutputStream.flush"(X, Ret) when X == x
invalid -> valid: ".*OutputStream.close"(x) invalid -> valid: ".*OutputStream.close"(X, Ret) when X == x
invalid -> error: "ByteArrayOutputStream.toByteArray"(y) invalid -> error: "ByteArrayOutputStream.toByteArray"(Y, Ret) when Y == y
invalid -> error: "ByteArrayOutputStream.toString"(y) invalid -> error: "ByteArrayOutputStream.toString"(Y, Ret) when Y == y

1
infer/tests/codetoanalyze/java/topl/baos/issues.exp
Unescape View File

@ -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_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.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.bBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, [] codetoanalyze/java/topl/baos/BaosTest.java, BaosTest.cBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []

10
infer/tests/codetoanalyze/java/topl/hasnext/hasnext.topl
Unescape View File

@ -4,9 +4,9 @@ property HasNext
prefix "Scanner" prefix "Scanner"
nondet (start) nondet (start)
start -> start: * start -> start: *
start -> invalid: I = iterator(*) start -> invalid: iterator(Ignore, RetIter) => i := RetIter
start -> invalid: Scanner(I, *) // For constructors, biabduction has "this" as first argument start -> invalid: Scanner(Iter, IgnoreA, IgnoreB) => i := Iter // For constructors, "this" is first argument, and there's a dummy return
invalid -> valid: B = hasNext(i) if B != 0 // in SIL, "true" is encoded as "not 0" invalid -> valid: hasNext(Iter, Ret) when Ret != 0 && Iter == i // in SIL, "true" is encoded as "not 0"
valid -> invalid: next(i) valid -> invalid: next(Iter, IgnoreRet) when Iter == i
invalid -> error: next(i) invalid -> error: next(Iter, IgnoreRet) when Iter == i

8
infer/tests/codetoanalyze/java/topl/hasnext/issues.exp
Unescape View File

@ -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, 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.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(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.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.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.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(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(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, [] codetoanalyze/java/topl/hasnext/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []

2
infer/tests/codetoanalyze/java/topl/servlet/ServletTests.java
Unescape View File

@ -20,8 +20,8 @@ class ServletTests {
} }
void bBad(ServletResponse response) throws IOException { void bBad(ServletResponse response) throws IOException {
PrintWriter w = response.getWriter();
ServletOutputStream s = response.getOutputStream(); ServletOutputStream s = response.getOutputStream();
PrintWriter w = response.getWriter();
} }
void cBad(ServletRequest request, ServletResponse response, RequestDispatcher dispatcher) void cBad(ServletRequest request, ServletResponse response, RequestDispatcher dispatcher)

14
infer/tests/codetoanalyze/java/topl/servlet/servlet.topl
Unescape View File

@ -10,16 +10,16 @@ property InterleavedResponse
prefix "ServletResponse" prefix "ServletResponse"
nondet (start) nondet (start)
start -> start: * start -> start: *
start -> gotWriter: getWriter(R) start -> gotWriter: getWriter(R, IgnoreRet) => r := R
start -> gotStream: getOutputStream(R) start -> gotStream: getOutputStream(R, IgnoreRet) => r := R
gotWriter -> error: getOutputStream(r) gotWriter -> error: getOutputStream(R, IgnoreRet) when R == r
gotStream -> error: getWriter(r) gotStream -> error: getWriter(R, IgnoreRet) when R == r
property ForwardUncommitted property ForwardUncommitted
message "A ServletResponse was forwarded before being committed." message "A ServletResponse was forwarded before being committed."
nondet (start) nondet (start)
start -> start: * start -> start: *
start -> gotChannel: C = "ServletResponse.\\(getWriter\\|getOutputStream\\)"(R) start -> gotChannel: "ServletResponse.\\(getWriter\\|getOutputStream\\)"(R, C) => r := R; c := C
gotChannel -> ok: "\\(PrintWriter\\|ServletOutputStream\\).flush.*"(c) gotChannel -> ok: "\\(PrintWriter\\|ServletOutputStream\\).flush.*"(C, IgnoreRet) when C == c
gotChannel -> error: "RequestDispatcher.forward"(*, *, r) gotChannel -> error: "RequestDispatcher.forward"(IgnoreDispatcher, IgnoreRequest, Response, IgnoreRet) when Response == r

8
infer/tests/codetoanalyze/java/topl/skip/SkipAfterRemove.topl
Unescape View File

@ -2,6 +2,8 @@ property SkipAfterRemove
prefix "ArrayList" prefix "ArrayList"
nondet (start) nondet (start)
start -> start: * start -> start: *
start -> removed: remove(Collection, Index) start -> removed: remove(Collection, Index, IgnoreRet) => c := Collection; i := Index
removed -> ok: get(collection, index) removed -> ok: get(Collection, Index, IgnoreRet) when i == Index && c == Collection
removed -> error: get(collection, J) if J != index 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.

8
infer/tests/codetoanalyze/java/topl/slowIter/slowIter.topl
Unescape View File

@ -1,8 +1,8 @@
property ShouldUseEntries property ShouldUseEntries
nondet (start iteratingKeys) nondet (start iteratingKeys)
start -> start: * start -> start: *
start -> gotKeys: S = "Map.keySet"(M) start -> gotKeys: "Map.keySet"(M, S) => m := M; s := S
gotKeys -> iteratingKeys: I = "Set.iterator"(s) gotKeys -> iteratingKeys: "Set.iterator"(S, I) when S == s => i := I
iteratingKeys -> iteratingKeys: * iteratingKeys -> iteratingKeys: *
iteratingKeys -> gotOneKey: K = "Iterator.next"(i) iteratingKeys -> gotOneKey: "Iterator.next"(I, K) when I == i => k := K
gotOneKey -> error: ".*Map.get"(m, k) gotOneKey -> error: ".*Map.get"(M, K, IgnoreRet) when M == m && K == k

Write Preview
Loading…
Cancel
Save