diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 44cd4f29b..377a92185 100644 --- a/infer/src/pulse/Pulse.ml +++ b/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 diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 183b1a30c..63bb16c29 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/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 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 +let pp_event f = function + | ArrayWrite {aw_array; aw_index} -> + Format.fprintf f "@[ArrayWrite %a[%a]@]" AbstractValue.pp aw_array AbstractValue.pp aw_index + | 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) : - (ToplAutomaton.transition * tcontext) list = - (* 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 static_match event : (ToplAutomaton.transition * tcontext) list = + let match_one transition = let f label = - let match_name () : bool = - let re = Str.regexp label.ToplAst.procedure_name in - Str.string_match re procname 0 - in - let match_args () : (ToplAutomaton.transition * tcontext) option = - 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 + match event with + | ArrayWrite {aw_array; aw_index} -> + static_match_array_write aw_array aw_index label + | Call {return; arguments; procname} -> + static_match_call return arguments procname label in - let result = Option.value_map ~default:(ret []) ~f t.ToplAutomaton.label in - let pp_second pp f (_, x) = pp f x in + let tcontext_opt = Option.value_map ~default:(Some []) ~f transition.ToplAutomaton.label in L.d_printfln "@[<2>PulseTopl.static_match:@;transition %a@;event %a@;result %a@]" - ToplAutomaton.pp_transition t pp_event event - (Pp.option (pp_second pp_tcontext)) - result ; - result + ToplAutomaton.pp_transition transition pp_event event (Pp.option pp_tcontext) tcontext_opt ; + Option.map ~f:(fun tcontext -> (transition, tcontext)) tcontext_opt 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 SmallStep (Call {procname}) | LargeStep (procname, _) -> procname - in - Format.fprintf Format.str_formatter "@[call to %a@]" Procname.pp procname ; + ( match step_data with + | SmallStep (Call {procname}) | LargeStep (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 diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli index aba4ececf..01f4023bd 100644 --- a/infer/src/pulse/PulseTopl.mli +++ b/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 diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 7cf680128..3565ea287 100644 --- a/infer/src/topl/Topl.ml +++ b/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 - (Pp.option Int.pp) pattern_len ; + tt "match name-pattern='%s' arg-len-pattern=%a@\n" (pname_of_label label) (Pp.option Int.pp) + pattern_len ; let log f = f () || diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml index ac6a2048d..326aa82ed 100644 --- a/infer/src/topl/ToplAst.ml +++ b/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] diff --git a/infer/src/topl/ToplAstOps.ml b/infer/src/topl/ToplAstOps.ml index f875aee53..7d0f268ce 100644 --- a/infer/src/topl/ToplAstOps.ml +++ b/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 diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index d3f7208dd..0fe24cef5 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/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 = - ToplAst.{label with procedure_name= prefix_pname label.procedure_name} + let prefix_pattern = + 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 diff --git a/infer/src/topl/ToplLexer.mll b/infer/src/topl/ToplLexer.mll index fbc024f47..9dbf1e370 100644 --- a/infer/src/topl/ToplLexer.mll +++ b/infer/src/topl/ToplLexer.mll @@ -52,6 +52,7 @@ rule raw_token = parse | "==" { EQ } | "!=" { NE } | "&&" { AND } + | "#ArrayWrite" { ARRAYWRITE } | "prefix" { PREFIX } | "property" { PROPERTY } | "message" { MESSAGE } diff --git a/infer/src/topl/ToplParser.mly b/infer/src/topl/ToplParser.mly index ef7b03264..09f7d168f 100644 --- a/infer/src/topl/ToplParser.mly +++ b/infer/src/topl/ToplParser.mly @@ -14,6 +14,7 @@ %token STRING %token 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 } - | s=STRING { s } + i=identifier { ToplAst.ProcedureNamePattern i } + | s=STRING { ToplAst.ProcedureNamePattern s } arguments_pattern: LP a=separated_list(COMMA, UID) RP { a } diff --git a/infer/tests/codetoanalyze/java/topl/Makefile b/infer/tests/codetoanalyze/java/topl/Makefile index d6dc01c3f..7566e8907 100644 --- a/infer/tests/codetoanalyze/java/topl/Makefile +++ b/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 diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/ImmutableArray.java b/infer/tests/codetoanalyze/java/topl/immutableArray/ImmutableArray.java new file mode 100644 index 000000000..667f10caa --- /dev/null +++ b/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; + } +} diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/Makefile b/infer/tests/codetoanalyze/java/topl/immutableArray/Makefile new file mode 100644 index 000000000..8328ddcb8 --- /dev/null +++ b/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 diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/immutableArray.topl b/infer/tests/codetoanalyze/java/topl/immutableArray/immutableArray.topl new file mode 100644 index 000000000..e639a079c --- /dev/null +++ b/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 + diff --git a/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp b/infer/tests/codetoanalyze/java/topl/immutableArray/issues.exp new file mode 100644 index 000000000..13f656a56 --- /dev/null +++ b/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]