[pulse] pulse models

Summary: Some mild refactoring to isolate the modelling part.

Reviewed By: mbouaziz

Differential Revision: D10406804

fbshipit-source-id: 3be76a5e9

infer/src/checkers/Pulse.ml

@@ -8,56 +8,47 @@ open! IStd
 module F = Format
 open Result.Monad_infix
 
-let read astate access_expr =
-  PulseDomain.materialize_location astate access_expr
-  >>= fun (astate, loc) -> PulseDomain.check_loc_access loc astate
-
-
-let read_all access_exprs astate = List.fold_result access_exprs ~init:astate ~f:read
-
-let write access_expr astate =
-  PulseDomain.overwrite_location astate access_expr (PulseDomain.AbstractLocation.mk_fresh ())
-  >>| fun (astate, _) -> astate
-
-
 let check_error summary loc = function
   | Ok astate ->
       astate
-  | Error (astate, message) ->
+  | Error (astate, diagnostic) ->
+      let message = PulseDomain.Diagnostic.to_string diagnostic in
       Reporting.log_error summary ~loc IssueType.use_after_lifetime message ;
       astate
 
 
-let invalidate access_expr astate =
-  PulseDomain.materialize_location astate access_expr
-  >>= fun (astate, loc) -> PulseDomain.check_loc_access loc astate >>| PulseDomain.mark_invalid loc
-
-
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = PulseDomain
 
   type extras = Summary.t
 
-  let exec_instr (astate : Domain.astate) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t)
+  let dispatch_call ret (call : HilInstr.call) (actuals : HilExp.t list) _flags _call_loc astate =
+    let model =
+      match call with
+      | Indirect _ ->
+          (* function pointer, etc.: skip for now *)
+          None
+      | Direct callee_pname ->
+          PulseModels.dispatch callee_pname
+    in
+    match model with None -> Ok astate | Some model -> model ~ret ~actuals astate
+
+
+  let exec_instr (astate : PulseDomain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t)
       =
     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
            record the value written instead of recording a fresh location *)
-        write lhs_access astate
+        PulseDomain.write lhs_access astate
-        >>= read_all (HilExp.get_access_exprs rhs_exp)
+        >>= PulseDomain.read_all (HilExp.get_access_exprs rhs_exp)
         |> check_error summary loc
     | Assume (condition, _, _, loc) ->
-        read_all (HilExp.get_access_exprs condition) astate |> check_error summary loc
+        PulseDomain.read_all (HilExp.get_access_exprs condition) astate |> check_error summary loc
-    | Call (_ret, HilInstr.Direct callee_pname, [AccessExpression deleted_access], _flags, loc)
+    | Call ((ret, _), call, actuals, flags, loc) ->
-      when Typ.Procname.equal callee_pname BuiltinDecl.__delete ->
+        PulseDomain.read_all (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
-        (* TODO: use {!ProcnameDispatcher.ProcName} instead of pattern matching name ourselves *)
+        >>= dispatch_call ret call actuals flags loc
-        invalidate deleted_access astate |> check_error summary loc
-    | Call (_ret, HilInstr.Direct _, actuals, _flags, loc)
-    | Call (_ret, HilInstr.Indirect _, actuals, _flags, loc) ->
-        (* TODO: function calls, right now we just register the reads of the arguments *)
-        read_all (List.concat_map actuals ~f:HilExp.get_access_exprs) astate
         |> check_error summary loc
 
 

infer/src/checkers/PulseDomain.ml

@@ -111,11 +111,19 @@ let initial =
   {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= AbstractLocationsDomain.empty}
 
 
-let check_loc_access loc astate =
+module Diagnostic = struct
-  if AbstractLocationsDomain.mem loc astate.invalids then
+  (* TODO: more structured error type so that we can actually report something informative about
-    (* TODO: more structured error type so that we can actually report something informative about
        the variables being accessed along with a trace *)
-    Error (astate, "invalid loc")
+  type t = InvalidLocation
+
+  let to_string InvalidLocation = "invalid location"
+end
+
+type access_result = (t, 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)
   else Ok astate
 
 
@@ -167,11 +175,38 @@ let walk_access_expr ?overwrite_last astate access_expr =
       walk ~overwrite_last base_loc access_list astate
 
 
+(** Use the stack and heap to walk the access path represented by the given expression down to an
+    abstract location representing what the expression points to.
+
+    Return an error state if it traverses some known invalid location or if the end destination is
+    known to be invalid. *)
 let materialize_location astate access_expr = walk_access_expr astate access_expr
 
+(** Use the stack and heap to walk the access path represented by the given expression down to an
+    abstract location representing what the expression points to, and replace that with the given
+    location.
+
+    Return an error state if it traverses some known invalid location. *)
 let overwrite_location astate access_expr new_loc =
   walk_access_expr ~overwrite_last:new_loc astate access_expr
 
 
+(** Add the given location to the set of know invalid locations. *)
 let mark_invalid loc astate =
   {astate with invalids= AbstractLocationsDomain.add loc astate.invalids}
+
+
+let read astate access_expr =
+  materialize_location astate access_expr >>= fun (astate, loc) -> check_loc_access loc astate
+
+
+let read_all access_exprs astate = List.fold_result access_exprs ~init:astate ~f:read
+
+let write access_expr astate =
+  overwrite_location astate access_expr (AbstractLocation.mk_fresh ())
+  >>| fun (astate, _) -> astate
+
+
+let invalidate access_expr astate =
+  materialize_location astate access_expr
+  >>= fun (astate, loc) -> check_loc_access loc astate >>| mark_invalid loc

infer/src/checkers/PulseDomain.mli

@@ -11,8 +11,6 @@ module F = Format
 module AbstractLocation : sig
   type t = private int [@@deriving compare]
 
-  val mk_fresh : unit -> t
-
   val pp : F.formatter -> t -> unit
 end
 
@@ -46,27 +44,16 @@ include AbstractDomain.S with type astate = t
 
 val initial : t
 
-val check_loc_access : AbstractLocation.t -> astate -> (astate, astate * string) result
+module Diagnostic : sig
-(** Check that the location is not known to be invalid *)
+  type t
 
-val materialize_location :
+  val to_string : t -> string
-  astate -> AccessExpression.t -> (astate * AbstractLocation.t, astate * string) result
+end
-(** Use the stack and heap to walk the access path represented by the given expression down to an
-    abstract location representing what the expression points to.
 
-    Return an error state if it traverses some known invalid location or if the end destination is
+type access_result = (t, t * Diagnostic.t) result
-    known to be invalid. *)
 
-val overwrite_location :
+val read_all : AccessExpression.t list -> t -> access_result
-     astate
-  -> AccessExpression.t
-  -> AbstractLocation.t
-  -> (astate * AbstractLocation.t, astate * string) result
-(** Use the stack and heap to walk the access path represented by the given expression down to an
-    abstract location representing what the expression points to, and replace that with the given
-    location.
 
-    Return an error state if it traverses some known invalid location. *)
+val write : AccessExpression.t -> t -> access_result
 
-val mark_invalid : AbstractLocation.t -> astate -> astate
+val invalidate : AccessExpression.t -> t -> access_result
-(** Add the given location to the set of know invalid locations. *)

infer/src/checkers/PulseModels.ml

@@ -0,0 +1,41 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type exec_fun = ret:Var.t -> actuals:HilExp.t list -> PulseDomain.t -> PulseDomain.access_result
+
+type model = exec_fun
+
+module Cplusplus = struct
+  let delete : model =
+   fun ~ret:_ ~actuals astate ->
+    match actuals with
+    | [AccessExpression deleted_access] ->
+        PulseDomain.invalidate deleted_access astate
+    | _ ->
+        Ok astate
+end
+
+let builtins_dispatcher =
+  let builtins = [(BuiltinDecl.__delete, Cplusplus.delete)] in
+  let builtins_map =
+    Hashtbl.create
+      ( module struct
+        include Typ.Procname
+
+        let hash = Caml.Hashtbl.hash
+
+        let sexp_of_t _ = assert false
+      end )
+  in
+  List.iter builtins ~f:(fun (builtin, model) ->
+      let open PolyVariantEqual in
+      assert (Hashtbl.add builtins_map ~key:builtin ~data:model = `Ok) ) ;
+  fun proc_name -> Hashtbl.find builtins_map proc_name
+
+
+let dispatch proc_name = builtins_dispatcher proc_name

infer/src/checkers/PulseModels.mli

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type exec_fun = ret:Var.t -> actuals:HilExp.t list -> PulseDomain.t -> PulseDomain.access_result
+
+type model = exec_fun
+
+val dispatch : Typ.Procname.t -> model option