From dd220a0fb40084c67169882cbc844752ef5dbcbc Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 18 Oct 2018 07:54:12 -0700 Subject: [PATCH] [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 | 11 +--- infer/src/checkers/Pulse.ml | 17 ++++-- infer/src/checkers/PulseDomain.ml | 24 +++++---- infer/src/checkers/PulseDomain.mli | 12 +++-- infer/src/checkers/PulseModels.ml | 53 ++++++++++++++++++- infer/src/checkers/PulseModels.mli | 6 ++- infer/tests/codetoanalyze/cpp/pulse/Makefile | 2 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../tests/codetoanalyze/cpp/pulse/vector.cpp | 4 +- 9 files changed, 95 insertions(+), 35 deletions(-) diff --git a/infer/src/IR/ProcnameDispatcher.mli b/infer/src/IR/ProcnameDispatcher.mli index 7c934311c..d3d63cd2d 100644 --- a/infer/src/IR/ProcnameDispatcher.mli +++ b/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 *) - -include - sig - [@@@warning "-60"] - - module ProcName : - NameCommon with type ('context, 'f) dispatcher = 'context -> Typ.Procname.t -> 'f option -end +module ProcName : + NameCommon with type ('context, 'f) dispatcher = 'context -> Typ.Procname.t -> 'f option module TypName : NameCommon with type ('context, 'f) dispatcher = 'context -> Typ.name -> 'f option diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 834b6684e..a67646f1d 100644 --- a/infer/src/checkers/Pulse.ml +++ b/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 - record the value written instead of recording a fresh location *) - PulseDomain.write lhs_access astate - >>= PulseDomain.read_all (HilExp.get_access_exprs rhs_exp) + (* try to evaluate [rhs_exp] down to an abstract location or generate a fresh one *) + let rhs_result = + match rhs_exp with + | 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 diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index f86bcc70a..c3e9d3736 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/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 = - materialize_location astate access_expr >>= fun (astate, loc) -> check_loc_access loc astate +let read access_expr 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 = - overwrite_location astate access_expr (AbstractLocation.mk_fresh ()) - >>| fun (astate, _) -> astate +let write access_expr loc astate = + overwrite_location astate access_expr loc >>| fun (astate, _) -> astate let invalidate access_expr astate = diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 603affa3b..c897feb08 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/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 diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index e765891d5..6ef471bcf 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/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 diff --git a/infer/src/checkers/PulseModels.mli b/infer/src/checkers/PulseModels.mli index cd61be5c9..b91074e27 100644 --- a/infer/src/checkers/PulseModels.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/pulse/Makefile b/infer/tests/codetoanalyze/cpp/pulse/Makefile index 4929e6ca6..3e1d1d1e7 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/Makefile +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 5db7b8a7e..7276aba99 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/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, [] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index d05ea203c..12bd392c8 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -7,11 +7,9 @@ #include #include -void FN_deref_vector_element_after_lifetime_bad() { +void deref_vector_element_after_lifetime_bad() { std::vector x = {0, 0}; int* y = &x[1]; x.push_back(4); std::cout << *y << "\n"; } - -int main() { FN_deref_vector_element_after_lifetime_bad(); }