[pulse] vector models

Summary:
Model `x[y]` and `x.push_back(i)` to catch the classic bug of "take
reference inside vector, invalidate, then use again".

Reviewed By: da319

Differential Revision: D10445824

fbshipit-source-id: 21ffd9677

infer/src/IR/ProcnameDispatcher.mli

@@ -198,15 +198,8 @@ module type NameCommon = sig
         accepts ALL function arguments, binds the function *)
 end
 
-(* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
+module ProcName :
-
+  NameCommon with type ('context, 'f) dispatcher = 'context -> Typ.Procname.t -> 'f option
-include
-  sig
-    [@@@warning "-60"]
-
-    module ProcName :
-      NameCommon with type ('context, 'f) dispatcher = 'context -> Typ.Procname.t -> 'f option
-end
 
 module TypName : NameCommon with type ('context, 'f) dispatcher = 'context -> Typ.name -> 'f option
 

infer/src/checkers/Pulse.ml

@@ -39,14 +39,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       =
     match instr with
     | Assign (lhs_access, rhs_exp, loc) ->
-        (* we could be more precise and try and evaluate [rhs_exp] down to a location and use it to
+        (* try to evaluate [rhs_exp] down to an abstract location or generate a fresh one *)
-           record the value written instead of recording a fresh location *)
+        let rhs_result =
-        PulseDomain.write lhs_access astate
+          match rhs_exp with
-        >>= PulseDomain.read_all (HilExp.get_access_exprs rhs_exp)
+          | AccessExpression rhs_access ->
+              PulseDomain.read rhs_access astate
+          | _ ->
+              PulseDomain.read_all (HilExp.get_access_exprs rhs_exp) astate
+              >>= fun astate -> Ok (astate, PulseDomain.AbstractLocation.mk_fresh ())
+        in
+        Result.bind rhs_result ~f:(fun (astate, rhs_value) ->
+            PulseDomain.write lhs_access rhs_value astate )
         |> check_error summary loc
     | Assume (condition, _, _, loc) ->
         PulseDomain.read_all (HilExp.get_access_exprs condition) astate |> check_error summary loc
-    | Call ((ret, _), call, actuals, flags, loc) ->
+    | Call (ret, call, actuals, flags, loc) ->
         PulseDomain.read_all (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
         >>= dispatch_call ret call actuals flags loc
         |> check_error summary loc

infer/src/checkers/PulseDomain.ml

@@ -130,16 +130,17 @@ include Domain
 module Diagnostic = struct
   (* TODO: more structured error type so that we can actually report something informative about
        the variables being accessed along with a trace *)
-  type t = InvalidLocation
+  type t = InvalidLocation of AbstractLocation.t
 
-  let to_string InvalidLocation = "invalid location"
+  let to_string (InvalidLocation loc) = F.asprintf "invalid location %a" AbstractLocation.pp loc
 end
 
-type access_result = (t, t * Diagnostic.t) result
+type 'a access_result = ('a, t * Diagnostic.t) result
 
 (** Check that the location is not known to be invalid *)
 let check_loc_access loc astate =
-  if AbstractLocationsDomain.mem loc astate.invalids then Error (astate, Diagnostic.InvalidLocation)
+  if AbstractLocationsDomain.mem loc astate.invalids then
+    Error (astate, Diagnostic.InvalidLocation loc)
   else Ok astate
 
 
@@ -212,15 +213,18 @@ let mark_invalid loc astate =
   {astate with invalids= AbstractLocationsDomain.add loc astate.invalids}
 
 
-let read astate access_expr =
+let read access_expr astate =
-  materialize_location astate access_expr >>= fun (astate, loc) -> check_loc_access loc astate
+  materialize_location astate access_expr
+  >>= fun (astate, loc) -> check_loc_access loc astate >>| fun astate -> (astate, loc)
+
 
+let read_all access_exprs astate =
+  List.fold_result access_exprs ~init:astate ~f:(fun astate access_expr ->
+      read access_expr astate >>| fst )
 
-let read_all access_exprs astate = List.fold_result access_exprs ~init:astate ~f:read
 
-let write access_expr astate =
+let write access_expr loc astate =
-  overwrite_location astate access_expr (AbstractLocation.mk_fresh ())
+  overwrite_location astate access_expr loc >>| fun (astate, _) -> astate
-  >>| fun (astate, _) -> astate
 
 
 let invalidate access_expr astate =

infer/src/checkers/PulseDomain.mli

@@ -11,6 +11,8 @@ module F = Format
 module AbstractLocation : sig
   type t = private int [@@deriving compare]
 
+  val mk_fresh : unit -> t
+
   val pp : F.formatter -> t -> unit
 end
 
@@ -52,10 +54,12 @@ module Diagnostic : sig
   val to_string : t -> string
 end
 
-type access_result = (t, t * Diagnostic.t) result
+type 'a access_result = ('a, t * Diagnostic.t) result
+
+val read : AccessExpression.t -> t -> (t * AbstractLocation.t) access_result
 
-val read_all : AccessExpression.t list -> t -> access_result
+val read_all : AccessExpression.t list -> t -> t access_result
 
-val write : AccessExpression.t -> t -> access_result
+val write : AccessExpression.t -> AbstractLocation.t -> t -> t access_result
 
-val invalidate : AccessExpression.t -> t -> access_result
+val invalidate : AccessExpression.t -> t -> t access_result

infer/src/checkers/PulseModels.ml

@@ -5,8 +5,13 @@
  * LICENSE file in the root directory of this source tree.
  *)
 open! IStd
+open Result.Monad_infix
 
-type exec_fun = ret:Var.t -> actuals:HilExp.t list -> PulseDomain.t -> PulseDomain.access_result
+type exec_fun =
+     ret:Var.t * Typ.t
+  -> actuals:HilExp.t list
+  -> PulseDomain.t
+  -> PulseDomain.t PulseDomain.access_result
 
 type model = exec_fun
 
@@ -20,6 +25,45 @@ module Cplusplus = struct
         Ok astate
 end
 
+module StdVector = struct
+  let internal_array =
+    Typ.Fieldname.Clang.from_class_name
+      (Typ.CStruct (QualifiedCppName.of_list ["std"; "vector"]))
+      "__internal_array"
+
+
+  let deref_internal_array vector =
+    AccessExpression.ArrayOffset
+      (AccessExpression.FieldOffset (vector, internal_array), Typ.void, [])
+
+
+  let at : model =
+   fun ~ret ~actuals astate ->
+    match actuals with
+    | [AccessExpression vector; _index] ->
+        PulseDomain.read (deref_internal_array vector) astate
+        >>= fun (astate, loc) -> PulseDomain.write (AccessExpression.Base ret) loc astate
+    | _ ->
+        Ok astate
+
+
+  let push_back : model =
+   fun ~ret:_ ~actuals astate ->
+    match actuals with
+    | [AccessExpression vector; _value] ->
+        PulseDomain.invalidate (deref_internal_array vector) astate
+    | _ ->
+        Ok astate
+end
+
+module ProcNameDispatcher = struct
+  let dispatch : (unit, model) ProcnameDispatcher.ProcName.dispatcher =
+    let open ProcnameDispatcher.ProcName in
+    make_dispatcher
+      [ -"std" &:: "vector" &:: "operator[]" &--> StdVector.at
+      ; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back ]
+end
+
 let builtins_dispatcher =
   let builtins = [(BuiltinDecl.__delete, Cplusplus.delete)] in
   let builtins_map =
@@ -38,4 +82,9 @@ let builtins_dispatcher =
   fun proc_name -> Hashtbl.find builtins_map proc_name
 
 
-let dispatch proc_name = builtins_dispatcher proc_name
+let dispatch proc_name =
+  match builtins_dispatcher proc_name with
+  | Some _ as result ->
+      result
+  | None ->
+      ProcNameDispatcher.dispatch () proc_name

infer/src/checkers/PulseModels.mli

@@ -6,7 +6,11 @@
  *)
 open! IStd
 
-type exec_fun = ret:Var.t -> actuals:HilExp.t list -> PulseDomain.t -> PulseDomain.access_result
+type exec_fun =
+     ret:Var.t * Typ.t
+  -> actuals:HilExp.t list
+  -> PulseDomain.t
+  -> PulseDomain.t PulseDomain.access_result
 
 type model = exec_fun
 

infer/tests/codetoanalyze/cpp/pulse/Makefile

@@ -10,7 +10,7 @@ CLANG_OPTIONS = -x c++ -std=c++14 -Wc++1z-extensions -nostdinc++ -isystem$(MODEL
 INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR)
 INFERPRINT_OPTIONS = --issues-tests
 
-SOURCES = $(wildcard ../ownership/*.cpp)
+SOURCES = $(wildcard ../ownership/*.cpp) $(wildcard *.cpp)
 
 include $(TESTS_DIR)/clang.make
 

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -10,3 +10,4 @@ codetoanalyze/cpp/ownership/use_after_delete.cpp, reassign_field_of_deleted_bad,
 codetoanalyze/cpp/ownership/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
 codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, []
 codetoanalyze/cpp/ownership/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, []
+codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_lifetime_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, []

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -7,11 +7,9 @@
 #include <iostream>
 #include <vector>
 
-void FN_deref_vector_element_after_lifetime_bad() {
+void deref_vector_element_after_lifetime_bad() {
   std::vector<int> x = {0, 0};
   int* y = &x[1];
   x.push_back(4);
   std::cout << *y << "\n";
 }
-
-int main() { FN_deref_vector_element_after_lifetime_bad(); }