From 7bd4aaa819ac4ce788edddb4f6635f8fa6916775 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 16 Oct 2018 11:05:32 -0700 Subject: [PATCH] [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 | 51 ++++++++++++------------------ infer/src/checkers/PulseDomain.ml | 43 ++++++++++++++++++++++--- infer/src/checkers/PulseDomain.mli | 29 +++++------------ infer/src/checkers/PulseModels.ml | 41 ++++++++++++++++++++++++ infer/src/checkers/PulseModels.mli | 13 ++++++++ 5 files changed, 122 insertions(+), 55 deletions(-) create mode 100644 infer/src/checkers/PulseModels.ml create mode 100644 infer/src/checkers/PulseModels.mli diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index bd677b953..834b6684e 100644 --- a/infer/src/checkers/Pulse.ml +++ b/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 - >>= read_all (HilExp.get_access_exprs rhs_exp) + PulseDomain.write lhs_access astate + >>= 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 - | Call (_ret, HilInstr.Direct callee_pname, [AccessExpression deleted_access], _flags, loc) - when Typ.Procname.equal callee_pname BuiltinDecl.__delete -> - (* TODO: use {!ProcnameDispatcher.ProcName} instead of pattern matching name ourselves *) - 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 + PulseDomain.read_all (HilExp.get_access_exprs condition) astate |> check_error summary 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 diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 75cc0bcc3..ab483ed17 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/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 = - if AbstractLocationsDomain.mem loc astate.invalids then - (* TODO: more structured error type so that we can actually report something informative about +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 *) - 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 diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index df1478d91..c5b3fa578 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/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 -(** Check that the location is not known to be invalid *) +module Diagnostic : sig + type t -val materialize_location : - astate -> AccessExpression.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. + val to_string : t -> string +end - Return an error state if it traverses some known invalid location or if the end destination is - known to be invalid. *) +type access_result = (t, t * Diagnostic.t) result -val overwrite_location : - 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. +val read_all : AccessExpression.t list -> t -> access_result - 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 -(** Add the given location to the set of know invalid locations. *) +val invalidate : AccessExpression.t -> t -> access_result diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml new file mode 100644 index 000000000..e765891d5 --- /dev/null +++ b/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 diff --git a/infer/src/checkers/PulseModels.mli b/infer/src/checkers/PulseModels.mli new file mode 100644 index 000000000..cd61be5c9 --- /dev/null +++ b/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