[topl] Added the ArrayWrite event type.

Summary:
Now one can use the pattern #ArrayWrite(A,I) to match on a write at
index I in array A. This only works in the Pulse variant of Topl (not in
the one based on SIL instrumentation).

Reviewed By: jvillard

Differential Revision: D25202768

fbshipit-source-id: 479f434e3

infer/src/pulse/Pulse.ml

@@ -122,6 +122,19 @@ module PulseTransferFunctions = struct
     Result.map ~f:(List.map ~f:do_one_exec_state) exec_state_res
 
 
+  let topl_store_step loc ~lhs ~rhs:_ astate =
+    match (lhs : Exp.t) with
+    | Lindex (arr, index) ->
+        (let open IResult.Let_syntax in
+        let* _astate, (aw_array, _history) = PulseOperations.eval loc arr astate in
+        let+ _astate, (aw_index, _history) = PulseOperations.eval loc index astate in
+        let topl_event = PulseTopl.ArrayWrite {aw_array; aw_index} in
+        AbductiveDomain.Topl.small_step loc topl_event astate)
+        |> Result.ok (* don't emit Topl event if evals fail *) |> Option.value ~default:astate
+    | _ ->
+        astate
+
+
   let dispatch_call ({InterproceduralAnalysis.tenv} as analysis_data) ret call_exp actuals call_loc
       flags astate =
     (* evaluate all actuals *)
@@ -272,6 +285,10 @@ module PulseTransferFunctions = struct
                 ~obj:(rhs_addr, event :: rhs_history)
                 astate
             in
+            let astate =
+              if Topl.is_deep_active () then topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate
+              else astate
+            in
             match lhs_exp with
             | Lvar pvar when Pvar.is_return pvar ->
                 PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate

infer/src/pulse/PulseTopl.ml

@@ -11,14 +11,19 @@ module L = Logging
 
 type value = AbstractValue.t
 
-type event = Call of {return: value option; arguments: value list; procname: Procname.t}
+type event =
+  | ArrayWrite of {aw_array: value; aw_index: value}
+  | Call of {return: value option; arguments: value list; procname: Procname.t}
 
 let pp_comma_seq f xs = Pp.comma_seq ~print_env:Pp.text_break f xs
 
-let pp_event f (Call {return; arguments; procname}) =
+let pp_event f = function
-  let procname = Procname.hashable_name procname (* as in [static_match] *) in
+  | ArrayWrite {aw_array; aw_index} ->
-  Format.fprintf f "@[call@ %a=%s(%a)@]" (Pp.option AbstractValue.pp) return procname
+      Format.fprintf f "@[ArrayWrite %a[%a]@]" AbstractValue.pp aw_array AbstractValue.pp aw_index
-    (pp_comma_seq AbstractValue.pp) arguments
+  | Call {return; arguments; procname} ->
+      let procname = Procname.hashable_name procname (* as in [static_match] *) in
+      Format.fprintf f "@[call@ %a=%s(%a)@]" (Pp.option AbstractValue.pp) return procname
+        (pp_comma_seq AbstractValue.pp) arguments
 
 
 type vertex = ToplAutomaton.vindex
@@ -138,50 +143,70 @@ let pp_tcontext f tcontext =
   Format.fprintf f "@[[%a]@]" (pp_comma_seq (Pp.pair ~fst:String.pp ~snd:AbstractValue.pp)) tcontext
 
 
+let static_match_array_write arr index label : tcontext option =
+  match label.ToplAst.pattern with
+  | ArrayWritePattern ->
+      let v1, v2 =
+        match label.ToplAst.arguments with
+        | Some [v1; v2] ->
+            (v1, v2)
+        | _ ->
+            L.die InternalError "Topl: #ArrayWrite should have exactly two arguments"
+      in
+      Some [(v1, arr); (v2, index)]
+  | _ ->
+      None
+
+
+let static_match_call return arguments procname label : tcontext option =
+  let rev_arguments = List.rev arguments in
+  let procname = Procname.hashable_name procname in
+  let match_name () : bool =
+    match label.ToplAst.pattern with
+    | ProcedureNamePattern pname ->
+        Str.string_match (Str.regexp pname) procname 0
+    | _ ->
+        false
+  in
+  let match_args () : tcontext option =
+    let match_formals formals : tcontext option =
+      let bind ~init rev_formals =
+        let f tcontext variable value = (variable, value) :: tcontext in
+        match List.fold2 ~init ~f rev_formals rev_arguments with
+        | Ok c ->
+            Some c
+        | Unequal_lengths ->
+            None
+      in
+      match (List.rev formals, return) with
+      | [], Some _ ->
+          None
+      | rev_formals, None ->
+          bind ~init:[] rev_formals
+      | r :: rev_formals, Some v ->
+          bind ~init:[(r, v)] rev_formals
+    in
+    Option.value_map ~default:(Some []) ~f:match_formals label.ToplAst.arguments
+  in
+  if match_name () then match_args () else None
+
+
 (** Returns a list of transitions whose pattern matches (e.g., event type matches). Each match
     produces a tcontext (transition context), which matches transition-local variables to abstract
     values. *)
-let static_match (Call {return; arguments; procname} as event) :
+let static_match event : (ToplAutomaton.transition * tcontext) list =
-    (ToplAutomaton.transition * tcontext) list =
+  let match_one transition =
-  (* TODO(rgrigore): if both [Topl.evaluate_static_guard] and [PulseTopl.static_match] remain, try to factor code. *)
-  let rev_arguments = List.rev arguments in
-  let procname = Procname.hashable_name procname in
-  let match_one t =
-    let ret c = Some (t, c) in
     let f label =
-      let match_name () : bool =
+      match event with
-        let re = Str.regexp label.ToplAst.procedure_name in
+      | ArrayWrite {aw_array; aw_index} ->
-        Str.string_match re procname 0
+          static_match_array_write aw_array aw_index label
-      in
+      | Call {return; arguments; procname} ->
-      let match_args () : (ToplAutomaton.transition * tcontext) option =
+          static_match_call return arguments procname label
-        let match_formals formals =
-          let bind ~init rev_formals =
-            let f tcontext variable value = (variable, value) :: tcontext in
-            match List.fold2 ~init ~f rev_formals rev_arguments with
-            | Ok c ->
-                ret c
-            | Unequal_lengths ->
-                None
-          in
-          match (List.rev formals, return) with
-          | [], Some _ ->
-              None
-          | rev_formals, None ->
-              bind ~init:[] rev_formals
-          | r :: rev_formals, Some v ->
-              bind ~init:[(r, v)] rev_formals
-        in
-        Option.value_map ~default:(ret []) ~f:match_formals label.ToplAst.arguments
-      in
-      if match_name () then match_args () else None
     in
-    let result = Option.value_map ~default:(ret []) ~f t.ToplAutomaton.label in
+    let tcontext_opt = Option.value_map ~default:(Some []) ~f transition.ToplAutomaton.label in
-    let pp_second pp f (_, x) = pp f x in
     L.d_printfln "@[<2>PulseTopl.static_match:@;transition %a@;event %a@;result %a@]"
-      ToplAutomaton.pp_transition t pp_event event
+      ToplAutomaton.pp_transition transition pp_event event (Pp.option pp_tcontext) tcontext_opt ;
-      (Pp.option (pp_second pp_tcontext))
+    Option.map ~f:(fun tcontext -> (transition, tcontext)) tcontext_opt
-      result ;
-    result
   in
   ToplAutomaton.tfilter_map (Topl.automaton ()) ~f:match_one
 
@@ -393,14 +418,17 @@ let simplify ~keep state =
 
 
 let description_of_step_data step_data =
-  let procname =
+  ( match step_data with
-    match step_data with SmallStep (Call {procname}) | LargeStep (procname, _) -> procname
+  | SmallStep (Call {procname}) | LargeStep (procname, _) ->
-  in
+      Format.fprintf Format.str_formatter "@[call to %a@]" Procname.pp procname
-  Format.fprintf Format.str_formatter "@[call to %a@]" Procname.pp procname ;
+  | SmallStep (ArrayWrite _) ->
+      Format.fprintf Format.str_formatter "@[write to array@]" ) ;
   Format.flush_str_formatter ()
 
 
 let report_errors proc_desc err_log state =
+  (* TODO(rgrigore): Calling f() that has implementation leads to a large_step followed by a small_step,
+     which currently results in two trace elements (that look the same to the user). This is confusing. *)
   let a = Topl.automaton () in
   let rec make_trace nesting acc q =
     match q.last_step with

infer/src/pulse/PulseTopl.mli

@@ -9,7 +9,9 @@ open! IStd
 
 type value = PulseAbstractValue.t
 
-type event = Call of {return: value option; arguments: value list; procname: Procname.t}
+type event =
+  | ArrayWrite of {aw_array: value; aw_index: value}
+  | Call of {return: value option; arguments: value list; procname: Procname.t}
 
 type state
 

infer/src/topl/Topl.ml

@@ -50,16 +50,26 @@ let get_proc_attr proc_name =
 
 let get_transitions_count () = ToplAutomaton.tcount (Lazy.force automaton)
 
+(* NOTE: Code instrumentation only handles ProcedureNamePattern patterns. *)
+
 (** 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_o (e_fun, arg_ts) =
+  let pname_of_label label =
+    match label.ToplAst.pattern with
+    | ProcedureNamePattern pname ->
+        pname
+    | _ ->
+        L.die UserError
+          "Topl: The implementation based on SIL-instrumentation only supports ProcedureNamePattern"
+  in
   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 re = Str.regexp (pname_of_label label) in
           let result = Str.string_match re name 0 in
           tt "  check name='%s'@\n" name ;
           result
@@ -74,8 +84,8 @@ let evaluate_static_guard label_o (e_fun, arg_ts) =
       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
+    tt "match name-pattern='%s' arg-len-pattern=%a@\n" (pname_of_label label) (Pp.option Int.pp)
-      (Pp.option Int.pp) pattern_len ;
+      pattern_len ;
     let log f =
       f ()
       ||

infer/src/topl/ToplAst.ml

@@ -29,13 +29,17 @@ type assignment = register_name * variable_name
 (** a regular expression *)
 type procedure_name_pattern = string
 
+type label_pattern = ArrayWritePattern | ProcedureNamePattern of procedure_name_pattern
+
 (* TODO(rgrigore): Check that variable names don't repeat.  *)
 (* TODO(rgrigore): Check that registers are written at most once. *)
+(* INV: if [pattern] is ArrayWritePattern, then [arguments] has length 2.
+    (Now ensured by parser. TODO: refactor to ensure with types.) *)
 type label =
   { arguments: variable_name list option
   ; condition: condition
   ; action: assignment list
-  ; procedure_name: procedure_name_pattern }
+  ; pattern: label_pattern }
 
 type vertex = string [@@deriving compare, hash, sexp]
 

infer/src/topl/ToplAstOps.ml

@@ -7,6 +7,12 @@
 
 open! IStd
 
-let pp_raw_label f {ToplAst.procedure_name} = Format.fprintf f "%s" procedure_name
+let pp_raw_label f label =
+  match label.ToplAst.pattern with
+  | ArrayWritePattern ->
+      Format.fprintf f "#ArrayWrite"
+  | ProcedureNamePattern procedure_name ->
+      Format.fprintf f "%s" procedure_name
+
 
 let pp_label = Pp.option pp_raw_label

infer/src/topl/ToplAutomaton.ml

@@ -82,9 +82,12 @@ let make properties =
           let ps = List.map ~f:(fun p -> "\\|" ^ p ^ "\\.") p.ToplAst.prefixes in
           "^\\(" ^ String.concat ps ^ "\\)" ^ pname ^ "("
       in
-      let prefix_label label =
+      let prefix_pattern =
-        ToplAst.{label with procedure_name= prefix_pname label.procedure_name}
+        ToplAst.(
+          function
+          | ProcedureNamePattern pname -> ProcedureNamePattern (prefix_pname pname) | p -> p)
       in
+      let prefix_label label = ToplAst.{label with pattern= prefix_pattern label.pattern} in
       let f t =
         let source = vindex ToplAst.(p.name, t.source) in
         let target = vindex ToplAst.(p.name, t.target) in

infer/src/topl/ToplLexer.mll

@@ -52,6 +52,7 @@ rule raw_token = parse
   | "==" { EQ }
   | "!=" { NE }
   | "&&" { AND }
+  | "#ArrayWrite" { ARRAYWRITE }
   | "prefix" { PREFIX }
   | "property" { PROPERTY }
   | "message" { MESSAGE }

infer/src/topl/ToplParser.mly

@@ -14,6 +14,7 @@
 %token <string> STRING
 %token <string> UID
 %token AND
+%token ARRAYWRITE
 %token ARROW
 %token ARROWARROW
 %token COLON
@@ -63,11 +64,17 @@ state: i=identifier { i }
 
 label:
     STAR { None }
-  | procedure_name=procedure_pattern arguments=arguments_pattern?
+  | pattern=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 } }
+      Some ToplAst.{ arguments; condition; action; pattern } }
+  | ARRAYWRITE LP arr=UID COMMA index=UID RP
+    condition=condition? action=action?
+    { let arguments = Some [arr; index] in
+      let condition = Option.value ~default:[] condition in
+      let action = Option.value ~default:[] action in
+      Some ToplAst.{ arguments; condition; action; pattern= ToplAst.ArrayWritePattern } }
 
 condition: WHEN ps=condition_expression { ps }
 
@@ -97,8 +104,8 @@ predop:
 and_predicate: AND p=predicate { p }
 
 procedure_pattern:
-    i=identifier { i }
+    i=identifier { ToplAst.ProcedureNamePattern i }
-  | s=STRING { s }
+  | s=STRING { ToplAst.ProcedureNamePattern s }
 
 arguments_pattern: LP a=separated_list(COMMA, UID) RP { a }
 

infer/tests/codetoanalyze/java/topl/Makefile

@@ -5,7 +5,7 @@
 
 TESTS_DIR = ../../..
 
-SUBDIRS = baos compareArgs hasnext servlet slowIter
+SUBDIRS = baos compareArgs hasnext immutableArray servlet slowIter
 
 test-%:
 	$(MAKE) -C $* test

infer/tests/codetoanalyze/java/topl/immutableArray/ImmutableArray.java

@@ -0,0 +1,42 @@
+/*
+ * 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.
+ */
+class ImmutableArray {
+
+  final int[] testArray = new int[] {0, 1, 2, 4};
+
+  int[] getTestArray() {
+    return testArray;
+  }
+
+  void badA() {
+    int[] array = getTestArray();
+    array[2] = 7;
+  }
+
+  void badB() {
+    int[] array = getTestArray();
+    int[] otherArray = array;
+    otherArray[2] = 7;
+  }
+
+  void badC() {
+    int[] array = getTestArray();
+    otherMutateArray(array);
+  }
+
+  void badABC() {
+    int[] array = getTestArray();
+    array[2] = 7;
+    int[] otherArray = array;
+    otherArray[2] = 7;
+    otherMutateArray(array);
+  }
+
+  void otherMutateArray(int[] array) {
+    array[2] = 7;
+  }
+}

infer/tests/codetoanalyze/java/topl/immutableArray/Makefile

@@ -0,0 +1,13 @@
+# 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.
+
+TESTS_DIR = ../../../..
+
+INFER_OPTIONS = --topl-properties immutableArray.topl --pulse-only
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.java)
+
+include $(TESTS_DIR)/javac.make

infer/tests/codetoanalyze/java/topl/immutableArray/immutableArray.topl

@@ -0,0 +1,7 @@
+property ImmutableArrayModified
+  prefix "ImmutableArray"
+  nondet (start)
+  start -> start: *
+  start -> tracking: getTestArray(IgnoreObject, Array) => a := Array
+  tracking -> error: #ArrayWrite(Array, IgnoreIndex) when a == Array
+

infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp

@@ -0,0 +1,4 @@
+codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badA():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),write to array]
+codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badABC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),write to array,call to void ImmutableArray.otherMutateArray(int[])]
+codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badB():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),write to array]
+codetoanalyze/java/topl/immutableArray/ImmutableArray.java, ImmutableArray.badC():void, 0, TOPL_PULSE_ERROR, no_bucket, ERROR, [call to int[] ImmutableArray.getTestArray(),call to int[] ImmutableArray.getTestArray(),call to void ImmutableArray.otherMutateArray(int[]),write to array]