[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

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

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]
 

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

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

infer/src/topl/ToplName.ml

@@ -7,6 +7,8 @@
 
 open! IStd
 
+type t = string
+
 let p = Printf.sprintf
 
 let topl_property = "topl.Property"

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

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 <int> INDENT (* The lexer uses this token only internally. *)
 %token <int> INTEGER
+%token <string> LID
 %token <string> STRING
-%token GT
-%token LT
-
-(* TOPL tokens *)
-%token <int> INDENT (* The lexer uses this token only internally. *)
-%token <string> ID
+%token <string> 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 <ToplAst.t list> 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 }
 
 %%

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<Integer> xs) {
+    for (int i = 0; i < xs.size(); ++i) {
+      int x = xs.get(i);
+      if (x % 2 == 0) xs.remove(i);
+    }
+  }
+}

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)

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

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)

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()]