From 91ebfe9c2031939f43bbfeb2fa140d91e35b3557 Mon Sep 17 00:00:00 2001 From: Radu Grigore Date: Tue, 17 Dec 2019 04:26:52 -0800 Subject: [PATCH] [topl] Support side conditions for transitions. Summary: In addition to state1 -> state2: pattern one can now also write state1 -> state2: pattern if condition where "condition" is some conjunction of comparisons (==,<,>) that involve variables bound by "pattern", registers of the automaton, and constants. Reviewed By: ngorogiannis Differential Revision: D19035496 fbshipit-source-id: 6f6e6a9be --- infer/src/dune.in | 2 +- infer/src/topl/ToplAst.ml | 26 ++++-- infer/src/topl/ToplLexer.mll | 28 +++--- infer/src/topl/ToplMonitor.ml | 50 ++++++++++- infer/src/topl/ToplName.ml | 2 + infer/src/topl/ToplName.mli | 24 +++--- infer/src/topl/ToplParser.mly | 85 ++++++++++++------- .../codetoanalyze/java/topl/IndexSkip.java | 20 +++++ infer/tests/codetoanalyze/java/topl/Makefile | 2 +- .../java/topl/SkipAfterRemove.topl | 6 ++ .../codetoanalyze/java/topl/hasnext.topl | 2 +- .../tests/codetoanalyze/java/topl/issues.exp | 5 ++ 12 files changed, 182 insertions(+), 70 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/topl/IndexSkip.java create mode 100644 infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl diff --git a/infer/src/dune.in b/infer/src/dune.in index 6b295132a..f3ab86c5e 100644 --- a/infer/src/dune.in +++ b/infer/src/dune.in @@ -57,7 +57,7 @@ let stanzas = ( if clang then ["(ocamllex types_lexer ctl_lexer)"; "(menhir (modules types_parser ctl_parser))"] else [] ) @ [ "(ocamllex ToplLexer)" - ; "(menhir (flags --unused-token INDENT) (modules ToplParser))" + ; "(menhir (flags --unused-token INDENT --explain) (modules ToplParser))" ; Format.sprintf {| (library diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml index 04d4226a8..ceed58f0a 100644 --- a/infer/src/topl/ToplAst.ml +++ b/infer/src/topl/ToplAst.ml @@ -13,19 +13,31 @@ type register_name = string type constant = Exp.t -type value_pattern = - | Ignore - | SaveInRegister of register_name - | EqualToRegister of register_name - | EqualToConstant of constant +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 + +(* refers to the corresponding SaveInRegister, from the same label *) + +type binop = (* all return booleans *) + | OpEq | OpNe | OpGe | OpGt | OpLe | OpLt + +type predicate = Binop of binop * value * value | Value of value + +(* here, value should be a boolean *) + +type condition = predicate list (* conjunction *) (** 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). *) type label = - { return: value_pattern + { arguments: value_pattern list option + ; condition: condition ; procedure_name: procedure_name_pattern - ; arguments: value_pattern list option } + ; return: value_pattern } type vertex = string [@@deriving compare, hash, sexp] diff --git a/infer/src/topl/ToplLexer.mll b/infer/src/topl/ToplLexer.mll index ba39fedec..bc1cf1335 100644 --- a/infer/src/topl/ToplLexer.mll +++ b/infer/src/topl/ToplLexer.mll @@ -27,14 +27,13 @@ open! Caml } -let id_head = ['a'-'z' 'A'-'Z'] let id_tail = ['a'-'z' 'A'-'Z' '0'-'9']* let integer = ['0' - '9']+ -rule topl_token lexing_sil = parse +rule raw_token = parse | '\t' { raise Error } | ((' '* ("//" [^ '\n']*)? '\n')+ as x) (' '* as y) { new_line x y lexbuf } - | ' '+ { topl_token lexing_sil lexbuf } + | ' '+ { raw_token lexbuf } | "->" { ARROW } | '=' { ASGN } | ':' { COLON } @@ -43,25 +42,26 @@ rule topl_token lexing_sil = parse | ')' { RP } | '*' { STAR } | '"' (([^ '"' '\n' '\\'] | ('\\' _))* as x) '"' { STRING (unquote x) } - | '<' { lexing_sil := true ; LT } + | integer as x { INTEGER (int_of_string x) } + | '<' { LT } + | '>' { GT } + | "<=" { LE } + | ">=" { GE } + | "==" { EQ } + | "!=" { NE } + | "if" { IF } + | "&&" { AND } | "prefix" { PREFIX } | "property" { PROPERTY } | "message" { MESSAGE } - | id_head id_tail as id { ID id } + | ['a'-'z'] id_tail as id { LID id } + | ['A'-'Z'] id_tail as id { UID id } | eof { EOF } | _ { raise Error } -and sil_token lexing_sil = parse - | '>' { lexing_sil := false ; GT } - | "true" { TRUE } - | "false" { FALSE } - | integer as x { INTEGER (int_of_string x) } - { let token () = - let lexing_sil = ref false in - let raw_token lexbuf = (if !lexing_sil then sil_token else topl_token) lexbuf in let indents = ref [0] in let scheduled_rc = ref 0 in let last_indent () = match !indents with @@ -76,7 +76,7 @@ and sil_token lexing_sil = parse in let rec step lexbuf = if !scheduled_rc > 0 then (decr scheduled_rc; RC) - else match raw_token lexing_sil lexbuf with + else match raw_token lexbuf with | INDENT n when n > last_indent () -> (add_indent n; LC) | INDENT n when n < last_indent () -> (drop_to_indent n; step lexbuf) | INDENT _ -> step lexbuf diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml index 2159a4b56..40b428875 100644 --- a/infer/src/topl/ToplMonitor.ml +++ b/infer/src/topl/ToplMonitor.ml @@ -232,15 +232,61 @@ let generate_execute_state automaton proc_name = [] (* true *) | EqualToRegister i -> [Exp.eq variable (ToplUtils.static_var (ToplName.reg i))] - | EqualToConstant ct -> - [Exp.eq variable ct] 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 add n = function + | ToplAst.SaveInRegister i -> + Hashtbl.add_exn ~key:i ~data:n table + | _ -> + () + 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 exp_of_value = + let open ToplAst in + function + | Constant c -> + c + | Register i -> + ToplUtils.static_var (ToplName.reg i) + | Binding v -> + ToplUtils.static_var (binding_of v) + in + let expbinop = function + | ToplAst.OpEq -> + Binop.Eq + | ToplAst.OpNe -> + Binop.Ne + | ToplAst.OpGe -> + Binop.Ge + | ToplAst.OpGt -> + Binop.Gt + | ToplAst.OpLe -> + Binop.Le + | ToplAst.OpLt -> + Binop.Lt + in + let predicate = function + | ToplAst.Binop (op, v1, v2) -> + Exp.BinOp (expbinop op, exp_of_value v1, exp_of_value v2) + | ToplAst.Value v -> + exp_of_value v + in + List.map ~f:predicate label.ToplAst.condition + 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 ) in diff --git a/infer/src/topl/ToplName.ml b/infer/src/topl/ToplName.ml index fc968aab7..b0cf11d39 100644 --- a/infer/src/topl/ToplName.ml +++ b/infer/src/topl/ToplName.ml @@ -7,6 +7,8 @@ open! IStd +type t = string + let p = Printf.sprintf let topl_property = "topl.Property" diff --git a/infer/src/topl/ToplName.mli b/infer/src/topl/ToplName.mli index e63b44ef5..646c7fdec 100644 --- a/infer/src/topl/ToplName.mli +++ b/infer/src/topl/ToplName.mli @@ -7,24 +7,26 @@ open! IStd -val topl_property : string +type t = string -val transition : int -> string +val topl_property : t -val arg : int -> string +val transition : int -> t -val retval : string +val arg : int -> t -val saved_arg : int -> string +val retval : t -val reg : string -> string +val saved_arg : int -> t -val state : string +val reg : string -> t -val maybe : string +val state : t -val execute : string +val maybe : t -val execute_state : int -> string +val execute : t -val save_args : string +val execute_state : int -> t + +val save_args : t diff --git a/infer/src/topl/ToplParser.mly b/infer/src/topl/ToplParser.mly index 8ffd8ec8d..7ee1bdc50 100644 --- a/infer/src/topl/ToplParser.mly +++ b/infer/src/topl/ToplParser.mly @@ -6,44 +6,35 @@ */ %{ open !IStd - - let is_guard i = Char.is_lowercase i.[0] - - let normalize_id i = String.uncapitalize i - - let value_pattern_of_id i = - assert (String.length i > 0) ; - let j = normalize_id i in - if is_guard i then ToplAst.EqualToRegister j else ToplAst.SaveInRegister j %} -(* Switching and common tokens *) +%token INDENT (* The lexer uses this token only internally. *) %token INTEGER +%token LID %token STRING -%token GT -%token LT - -(* TOPL tokens *) -%token INDENT (* The lexer uses this token only internally. *) -%token ID +%token UID +%token AND %token ARROW %token ASGN %token COLON %token COMMA %token EOF +%token EQ +%token GE +%token GT +%token IF %token LC +%token LE %token LP +%token LT %token MESSAGE +%token NE %token PREFIX %token PROPERTY %token RC %token RP %token STAR -(* SIL tokens *) -%token FALSE -%token TRUE - %start properties %% @@ -51,7 +42,7 @@ properties: ps=one_property* EOF { ps } one_property: - PROPERTY name=ID LC message=message? prefixes=prefix* transitions=transition* RC + PROPERTY name=identifier LC message=message? prefixes=prefix* transitions=transition* RC { ToplAst.{name; message; prefixes; transitions} } message: MESSAGE s=STRING { s } @@ -59,32 +50,60 @@ message: MESSAGE s=STRING { s } prefix: PREFIX s=STRING { s } transition: - source=ID ARROW target=ID COLON label=label + source=identifier ARROW target=identifier COLON label=label { ToplAst.{source; target; label} } label: - return=value_pattern ASGN c=call_pattern - { let procedure_name, arguments = c in ToplAst.{return; procedure_name; arguments} } - | c=call_pattern - { let procedure_name, arguments = c in ToplAst.{return=Ignore; procedure_name; arguments} } + 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} } + +condition: IF ps=condition_expression { ps } + +condition_expression: p=predicate ps=and_predicate* { p :: ps } + +predicate: + v1=value ov2=predop_value? + { let f (o, v2) = ToplAst.Binop (o, v1, v2) in + Option.value_map ~default:(ToplAst.Value v1) ~f ov2 } + +value: + id=LID { ToplAst.Register id } + | id=UID { ToplAst.Binding (String.uncapitalize id) } + | x=INTEGER { ToplAst.Constant (Exp.Const (Const.Cint (IntLit.of_int x))) } + | x=STRING { ToplAst.Constant (Exp.Const (Const.Cstr x)) } + +predop_value: o=predop v=value { (o, v) } + +predop: + EQ { ToplAst.OpEq } + | NE { ToplAst.OpNe } + | LT { ToplAst.OpLt } + | LE { ToplAst.OpLe } + | GT { ToplAst.OpGt } + | GE { ToplAst.OpGe } + +and_predicate: AND p=predicate { p } call_pattern: p=procedure_pattern a=arguments_pattern? { (p, a) } procedure_pattern: - i=ID { i } + i=identifier { i } | s=STRING { s } | STAR { ".*" } arguments_pattern: LP a=separated_list(COMMA, value_pattern) RP { a } value_pattern: - i=ID { value_pattern_of_id i } + i=LID { ToplAst.EqualToRegister i } + | i=UID { ToplAst.SaveInRegister (String.uncapitalize i) } | STAR { ToplAst.Ignore } - | LT e=sil_expression GT { ToplAst.EqualToConstant e } -sil_expression: - TRUE { Exp.one } - | FALSE { Exp.zero } - | x=INTEGER { Exp.int (IntLit.of_int x) } +identifier: i=LID { i } | i=UID { i } %% diff --git a/infer/tests/codetoanalyze/java/topl/IndexSkip.java b/infer/tests/codetoanalyze/java/topl/IndexSkip.java new file mode 100644 index 000000000..7e2df00d1 --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/IndexSkip.java @@ -0,0 +1,20 @@ +/* + * 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. + */ +import java.util.*; + +public class IndexSkip { + public static void main(String[] args) { + foo(new ArrayList<>(Arrays.asList(1, 2, 3, 4))); + } + + static void foo(ArrayList xs) { + for (int i = 0; i < xs.size(); ++i) { + int x = xs.get(i); + if (x % 2 == 0) xs.remove(i); + } + } +} diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile index 4ba8f6464..eed31dbb6 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 hasnext.topl --biabduction-only +INFER_OPTIONS = --symops-per-iteration 10000 --topl-properties hasnext.topl --topl-properties SkipAfterRemove.topl --biabduction-only INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl b/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl new file mode 100644 index 000000000..57ab29b1b --- /dev/null +++ b/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl @@ -0,0 +1,6 @@ +property SkipAfterRemove + prefix "ArrayList" + start -> start: * + start -> removed: remove(Collection, Index) + removed -> ok: get(collection, index) + removed -> error: get(collection, J) if j != index diff --git a/infer/tests/codetoanalyze/java/topl/hasnext.topl b/infer/tests/codetoanalyze/java/topl/hasnext.topl index 47bf2a882..8ca797e06 100644 --- a/infer/tests/codetoanalyze/java/topl/hasnext.topl +++ b/infer/tests/codetoanalyze/java/topl/hasnext.topl @@ -3,6 +3,6 @@ property HasNext prefix "List" start -> start: * start -> invalid: I = iterator(*) - invalid -> valid: hasNext(i) + invalid -> valid: B = hasNext(i) if B != 0 // in SIL, "true" is encoded as "not 0" valid -> invalid: next(i) invalid -> error: next(i) diff --git a/infer/tests/codetoanalyze/java/topl/issues.exp b/infer/tests/codetoanalyze/java/topl/issues.exp index 6606e736d..f78c98e29 100644 --- a/infer/tests/codetoanalyze/java/topl/issues.exp +++ b/infer/tests/codetoanalyze/java/topl/issues.exp @@ -1,2 +1,7 @@ +codetoanalyze/java/topl/IndexSkip.java, IndexSkip.foo(java.util.ArrayList):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure foo(...),Skipping size(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,ArrayList),start of procedure execute(),start of procedure execute_state_0(),Taking true branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),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(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute(),Taking true branch,Skipping get(...): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,ArrayList,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,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false 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(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] codetoanalyze/java/topl/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/Iterators.java, Iterators.hasNextBad(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextBad(...),Skipping iterator(): unknown method,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,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false 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(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, [] +codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),Skipping iterator(): unknown method,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,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false 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(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute(),start of procedure getSingleElementOk(...),Skipping next(): unknown method] +codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),Skipping iterator(): unknown method,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,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false 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(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()] +codetoanalyze/java/topl/Iterators.java, Iterators.hasNextOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),Skipping iterator(): unknown method,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,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false 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(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]