From 826fd8a9997e3f32ed54aa4808a4bce98c4fc14e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 17 Feb 2020 10:39:17 -0800 Subject: [PATCH] [pulse] monad, monads everywhere Summary: Add let*/+ syntax to `result` types to simplify all the applications of `>>=`, `>>|` that are followed by a binding (eg `>>= fun x -> ...`) in pulse. Reviewed By: skcho Differential Revision: D19940728 fbshipit-source-id: 4df159029 --- infer/src/istd/IResult.ml | 13 ++ infer/src/istd/IResult.mli | 13 ++ infer/src/pulse/Pulse.ml | 46 ++++--- infer/src/pulse/PulseAbductiveDomain.ml | 43 +++--- infer/src/pulse/PulseModels.ml | 165 +++++++++++++----------- infer/src/pulse/PulseOperations.ml | 113 ++++++++-------- 6 files changed, 213 insertions(+), 180 deletions(-) create mode 100644 infer/src/istd/IResult.ml create mode 100644 infer/src/istd/IResult.mli diff --git a/infer/src/istd/IResult.ml b/infer/src/istd/IResult.ml new file mode 100644 index 000000000..4319f11bb --- /dev/null +++ b/infer/src/istd/IResult.ml @@ -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. + *) +module Let_syntax = struct + include Result.Monad_infix + + let ( let+ ) x f = Result.map x ~f + + let ( let* ) x f = Result.bind x ~f +end diff --git a/infer/src/istd/IResult.mli b/infer/src/istd/IResult.mli new file mode 100644 index 000000000..4d0c2f13f --- /dev/null +++ b/infer/src/istd/IResult.mli @@ -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. + *) +module Let_syntax : sig + include module type of Result.Monad_infix + + val ( let+ ) : ('ok, 'err) result -> ('ok -> 'okk) -> ('okk, 'err) result + + val ( let* ) : ('ok, 'err) result -> ('ok -> ('okk, 'err) result) -> ('okk, 'err) result +end diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 53399da67..81cc9ddcb 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -4,10 +4,11 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd module F = Format module L = Logging -open Result.Monad_infix +open IResult.Let_syntax open PulseBasicInterface let report summary diagnostic = @@ -72,22 +73,21 @@ module PulseTransferFunctions = struct let exec_object_out_of_scope call_loc (pvar, typ) astate = let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in (* invalidate [&x] *) - PulseOperations.eval call_loc (Exp.Lvar pvar) astate - >>= fun (astate, out_of_scope_base) -> + let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate let dispatch_call tenv summary ret call_exp actuals call_loc flags get_formals astate = (* evaluate all actuals *) - List.fold_result actuals ~init:(astate, []) - ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) -> - PulseOperations.eval call_loc actual_exp astate - >>| fun (astate, actual_evaled) -> - ( astate - , ProcnameDispatcher.Call.FuncArg. - {exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ} - :: rev_func_args ) ) - >>= fun (astate, rev_func_args) -> + let* astate, rev_func_args = + List.fold_result actuals ~init:(astate, []) + ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) -> + let+ astate, actual_evaled = PulseOperations.eval call_loc actual_exp astate in + ( astate + , ProcnameDispatcher.Call.FuncArg. + {exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ} + :: rev_func_args ) ) + in let func_args = List.rev rev_func_args in let model = match proc_name_of_call call_exp with @@ -120,8 +120,7 @@ module PulseTransferFunctions = struct match get_out_of_scope_object call_exp actuals flags with | Some pvar_typ -> L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; - posts - >>= fun posts -> + let* posts = posts in List.map posts ~f:(fun astate -> exec_object_out_of_scope call_loc pvar_typ astate) |> Result.all | None -> @@ -134,22 +133,21 @@ module PulseTransferFunctions = struct | Load {id= lhs_id; e= rhs_exp; loc} -> (* [lhs_id := *rhs_exp] *) let result = - PulseOperations.eval_deref loc rhs_exp astate - >>| fun (astate, rhs_addr_hist) -> PulseOperations.write_id lhs_id rhs_addr_hist astate + let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in + PulseOperations.write_id lhs_id rhs_addr_hist astate in [check_error summary result] | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in let result = - PulseOperations.eval loc rhs_exp astate - >>= fun (astate, (rhs_addr, rhs_history)) -> - PulseOperations.eval loc lhs_exp astate - >>= fun (astate, lhs_addr_hist) -> - PulseOperations.write_deref loc ~ref:lhs_addr_hist - ~obj:(rhs_addr, event :: rhs_history) - astate - >>= fun astate -> + let* astate, (rhs_addr, rhs_history) = PulseOperations.eval loc rhs_exp astate in + let* astate, lhs_addr_hist = PulseOperations.eval loc lhs_exp astate in + let* astate = + PulseOperations.write_deref loc ~ref:lhs_addr_hist + ~obj:(rhs_addr, event :: rhs_history) + astate + in match lhs_exp with | Lvar pvar when Pvar.is_return pvar -> PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 433b5eed1..3be8b31ad 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -165,7 +165,7 @@ module Stack = struct end module AddressAttributes = struct - open Result.Monad_infix + open IResult.Let_syntax (** if [address] is in [pre] then add the attribute [attr] *) let abduce_attribute address attribute astate = @@ -180,8 +180,7 @@ module AddressAttributes = struct let check_valid access_trace addr astate = - BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs - >>| fun () -> + let+ () = BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs in (* if [address] is in [pre] and it should be valid then that fact goes in the precondition *) abduce_attribute addr (MustBeValid access_trace) astate @@ -559,11 +558,9 @@ module PrePost = struct [call_state.astate] *) let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state = L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractValue.pp (fst actual) ; - (let open Option.Monad_infix in - BaseStack.find_opt formal pre.BaseDomain.stack - >>= fun (addr_formal_pre, _) -> - BaseMemory.find_edge_opt addr_formal_pre Dereference pre.BaseDomain.heap - >>| fun (formal_pre, _) -> + (let open IOption.Let_syntax in + let* addr_formal_pre, _ = BaseStack.find_opt formal pre.BaseDomain.stack in + let+ formal_pre, _ = BaseMemory.find_edge_opt addr_formal_pre Dereference pre.BaseDomain.heap in materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre ~addr_hist_caller:actual call_state) |> function Some result -> result | None -> Ok call_state @@ -724,7 +721,7 @@ module PrePost = struct let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; let r = - let open Result.Monad_infix in + let open IResult.Let_syntax in (* first make as large a mapping as we can between callee values and caller values... *) materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state @@ -814,10 +811,11 @@ module PrePost = struct in let attrs = let written_to = - let open Option.Monad_infix in - BaseAddressAttributes.find_opt addr_caller attrs - >>= (fun attrs -> Attributes.get_written_to attrs) - |> fun written_to_callee_opt -> + let written_to_callee_opt = + let open IOption.Let_syntax in + let* attrs = BaseAddressAttributes.find_opt addr_caller attrs in + Attributes.get_written_to attrs + in let callee_trace = match written_to_callee_opt with | None -> @@ -872,12 +870,14 @@ module PrePost = struct L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp (fst actual) ; match - let open Option.Monad_infix in - BaseStack.find_opt formal (pre_post.pre :> BaseDomain.t).BaseDomain.stack - >>= fun (addr_formal_pre, _) -> - BaseMemory.find_edge_opt addr_formal_pre Dereference - (pre_post.pre :> BaseDomain.t).BaseDomain.heap - >>| fun (formal_pre, _) -> + let open IOption.Let_syntax in + let* addr_formal_pre, _ = + BaseStack.find_opt formal (pre_post.pre :> BaseDomain.t).BaseDomain.stack + in + let+ formal_pre, _ = + BaseMemory.find_edge_opt addr_formal_pre Dereference + (pre_post.pre :> BaseDomain.t).BaseDomain.heap + in record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre ~addr_hist_caller:actual call_state with @@ -1060,9 +1060,8 @@ module PrePost = struct | Ok call_state -> ( L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ; match - let open Result.Monad_infix in - check_all_valid callee_proc_name call_location pre_post call_state - >>| fun astate -> + let open IResult.Let_syntax in + let+ astate = check_all_valid callee_proc_name call_location pre_post call_state in (* reset [visited] *) let call_state = {call_state with astate; visited= AddressSet.empty} in (* apply the postcondition *) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index f5c934fbe..f3a3a27ec 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -5,7 +5,7 @@ * LICENSE file in the root directory of this source tree. *) open! IStd -open Result.Monad_infix +open IResult.Let_syntax open PulseBasicInterface open PulseDomainInterface @@ -24,14 +24,14 @@ module Misc = struct let shallow_copy model_desc dest_pointer_hist src_pointer_hist : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in - PulseOperations.eval_access location src_pointer_hist Dereference astate - >>= fun (astate, obj) -> - PulseOperations.shallow_copy location obj astate - >>= fun (astate, obj_copy) -> - PulseOperations.write_deref location ~ref:dest_pointer_hist - ~obj:(fst obj_copy, event :: snd obj_copy) - astate - >>| fun astate -> [PulseOperations.havoc_id ret_id [event] astate] + let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in + let* astate, obj_copy = PulseOperations.shallow_copy location obj astate in + let+ astate = + PulseOperations.write_deref location ~ref:dest_pointer_hist + ~obj:(fst obj_copy, event :: snd obj_copy) + astate + in + [PulseOperations.havoc_id ret_id [event] astate] let early_exit : model = fun ~caller_summary:_ _ ~ret:_ _ -> Ok [] @@ -85,8 +85,8 @@ module C = struct if is_known_zero then (* freeing 0 is a no-op *) Ok [astate] else - PulseOperations.invalidate location Invalidation.CFree deleted_access astate - >>| fun astate -> [astate] + let+ astate = PulseOperations.invalidate location Invalidation.CFree deleted_access astate in + [astate] end module Cplusplus = struct @@ -113,35 +113,35 @@ module StdAtomicInteger = struct let load_backing_int location this astate = - PulseOperations.eval_access location this Dereference astate - >>= fun (astate, obj) -> - PulseOperations.eval_access location obj (FieldAccess internal_int) astate - >>= fun (astate, int_addr) -> - PulseOperations.eval_access location int_addr Dereference astate - >>| fun (astate, int_val) -> (astate, int_addr, int_val) + let* astate, obj = PulseOperations.eval_access location this Dereference astate in + let* astate, int_addr = + PulseOperations.eval_access location obj (FieldAccess internal_int) astate + in + let+ astate, int_val = PulseOperations.eval_access location int_addr Dereference astate in + (astate, int_addr, int_val) let constructor this_address init_value : model = fun ~caller_summary:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::atomic::atomic()"; location; in_call= []} in let this = (AbstractValue.mk_fresh (), [event]) in - PulseOperations.eval_access location this (FieldAccess internal_int) astate - >>= fun (astate, int_field) -> - PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate - >>= fun astate -> - PulseOperations.write_deref location ~ref:this_address ~obj:this astate - >>| fun astate -> [astate] + let* astate, int_field = + PulseOperations.eval_access location this (FieldAccess internal_int) astate + in + let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in + let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in + [astate] let arith_bop prepost location event ret_id bop this operand astate = - load_backing_int location this astate - >>= fun (astate, int_addr, (old_int, old_int_hist)) -> + let* astate, int_addr, (old_int, old_int_hist) = load_backing_int location this astate in let astate, (new_int, hist) = PulseOperations.eval_binop location bop (AbstractValueOperand old_int) operand old_int_hist astate in - PulseOperations.write_deref location ~ref:int_addr ~obj:(new_int, event :: hist) astate - >>| fun astate -> + let+ astate = + PulseOperations.write_deref location ~ref:int_addr ~obj:(new_int, event :: hist) astate + in let ret_int = match prepost with `Pre -> new_int | `Post -> old_int in PulseOperations.write_id ret_id (ret_int, event :: hist) astate @@ -149,22 +149,30 @@ module StdAtomicInteger = struct let fetch_add this (increment, _) _memory_ordering : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::fetch_add()"; location; in_call= []} in - arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) astate - >>| fun astate -> [astate] + let+ astate = + arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) + astate + in + [astate] let fetch_sub this (increment, _) _memory_ordering : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::fetch_sub()"; location; in_call= []} in - arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) astate - >>| fun astate -> [astate] + let+ astate = + arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) + astate + in + [astate] let operator_plus_plus_pre this : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator++()"; location; in_call= []} in - arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate - >>| fun astate -> [astate] + let+ astate = + arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate + in + [astate] let operator_plus_plus_post this _int : model = @@ -172,15 +180,19 @@ module StdAtomicInteger = struct let event = ValueHistory.Call {f= Model "std::atomic::operator++(T)"; location; in_call= []} in - arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate - >>| fun astate -> [astate] + let+ astate = + arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate + in + [astate] let operator_minus_minus_pre this : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator--()"; location; in_call= []} in - arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate - >>| fun astate -> [astate] + let+ astate = + arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate + in + [astate] let operator_minus_minus_post this _int : model = @@ -188,15 +200,16 @@ module StdAtomicInteger = struct let event = ValueHistory.Call {f= Model "std::atomic::operator--(T)"; location; in_call= []} in - arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate - >>| fun astate -> [astate] + let+ astate = + arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate + in + [astate] let load_instr model_desc this _memory_ordering_opt : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in - load_backing_int location this astate - >>| fun (astate, _int_addr, (int, hist)) -> + let+ astate, _int_addr, (int, hist) = load_backing_int location this astate in [PulseOperations.write_id ret_id (int, event :: hist) astate] @@ -205,27 +218,26 @@ module StdAtomicInteger = struct let operator_t = load_instr "std::atomic::operator_T()" let store_backing_int location this_address new_value astate = - PulseOperations.eval_access location this_address Dereference astate - >>= fun (astate, this) -> - PulseOperations.eval_access location this (FieldAccess internal_int) astate - >>= fun (astate, int_field) -> + let* astate, this = PulseOperations.eval_access location this_address Dereference astate in + let* astate, int_field = + PulseOperations.eval_access location this (FieldAccess internal_int) astate + in PulseOperations.write_deref location ~ref:int_field ~obj:new_value astate let store this_address (new_value, new_hist) _memory_ordering : model = fun ~caller_summary:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::atomic::store()"; location; in_call= []} in - store_backing_int location this_address (new_value, event :: new_hist) astate - >>| fun astate -> [astate] + let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in + [astate] let exchange this_address (new_value, new_hist) _memory_ordering : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::exchange()"; location; in_call= []} in - load_backing_int location this_address astate - >>= fun (astate, _int_addr, (old_int, old_hist)) -> - store_backing_int location this_address (new_value, event :: new_hist) astate - >>| fun astate -> [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate] + let* astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in + let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in + [PulseOperations.write_id ret_id (old_int, event :: old_hist) astate] end module StdBasicString = struct @@ -244,10 +256,10 @@ module StdBasicString = struct let data this_hist : model = fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in - to_internal_string location this_hist astate - >>= fun (astate, string_addr_hist) -> - PulseOperations.eval_access location string_addr_hist Dereference astate - >>| fun (astate, (string, hist)) -> + let* astate, string_addr_hist = to_internal_string location this_hist astate in + let+ astate, (string, hist) = + PulseOperations.eval_access location string_addr_hist Dereference astate + in [PulseOperations.write_id ret_id (string, event :: hist) astate] @@ -255,12 +267,11 @@ module StdBasicString = struct fun ~caller_summary:_ location ~ret:_ astate -> let model = CallEvent.Model "std::basic_string::~basic_string()" in let call_event = ValueHistory.Call {f= model; location; in_call= []} in - to_internal_string location this_hist astate - >>= fun (astate, (string_addr, string_hist)) -> + let* astate, (string_addr, string_hist) = to_internal_string location this_hist astate in let string_addr_hist = (string_addr, call_event :: string_hist) in - PulseOperations.invalidate_deref location CppDelete string_addr_hist astate - >>= fun astate -> - PulseOperations.invalidate location CppDelete string_addr_hist astate >>| fun astate -> [astate] + let* astate = PulseOperations.invalidate_deref location CppDelete string_addr_hist astate in + let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in + [astate] end module StdFunction = struct @@ -270,10 +281,10 @@ module StdFunction = struct let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in [PulseOperations.havoc_id ret_id [event] astate] in - PulseOperations.eval_access location lambda_ptr_hist Dereference astate - >>= fun (astate, (lambda, _)) -> - PulseOperations.Closures.check_captured_addresses location lambda astate - >>= fun astate -> + let* astate, (lambda, _) = + PulseOperations.eval_access location lambda_ptr_hist Dereference astate + in + let* astate = PulseOperations.Closures.check_captured_addresses location lambda astate in match AddressAttributes.get_closure_proc_name lambda astate with | None -> (* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate) @@ -300,16 +311,14 @@ module StdVector = struct let element_of_internal_array location vector index astate = - to_internal_array location vector astate - >>= fun (astate, vector_internal_array) -> + let* astate, vector_internal_array = to_internal_array location vector astate in PulseOperations.eval_access location vector_internal_array (ArrayAccess (Typ.void, index)) astate let reallocate_internal_array trace vector vector_f location astate = - to_internal_array location vector astate - >>= fun (astate, array_address) -> + let* astate, array_address = to_internal_array location vector astate in PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate >>= PulseOperations.invalidate_deref location (StdVector vector_f) array_address >>= PulseOperations.havoc_field location vector internal_array trace @@ -329,8 +338,7 @@ module StdVector = struct let at ~desc vector index : model = fun ~caller_summary:_ location ~ret astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - element_of_internal_array location vector (fst index) astate - >>| fun (astate, (addr, hist)) -> + let+ astate, (addr, hist) = element_of_internal_array location vector (fst index) astate in [PulseOperations.write_id (fst ret) (addr, event :: hist) astate] @@ -358,13 +366,16 @@ module JavaCollection = struct let set coll index new_elem : model = fun ~caller_summary:_ location ~ret astate -> let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in - StdVector.element_of_internal_array location coll (fst index) astate - >>= fun (astate, ((old_addr, old_hist) as old_elem)) -> - PulseOperations.write_deref location ~ref:new_elem - ~obj:(old_addr, ValueHistory.Assignment location :: old_hist) - astate - >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem - >>| fun astate -> [PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate] + let* astate, ((old_addr, old_hist) as old_elem) = + StdVector.element_of_internal_array location coll (fst index) astate + in + let+ astate = + PulseOperations.write_deref location ~ref:new_elem + ~obj:(old_addr, ValueHistory.Assignment location :: old_hist) + astate + >>= PulseOperations.invalidate_deref location (StdVector Assign) old_elem + in + [PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate] end module StringSet = Caml.Set.Make (String) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index bffaf27c4..86baa234e 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -6,7 +6,7 @@ *) open! IStd module L = Logging -open Result.Monad_infix +open IResult.Let_syntax open PulseBasicInterface open PulseDomainInterface @@ -55,17 +55,20 @@ module Closures = struct | None -> Ok astate | Some (edges, attributes) -> - IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function - | Attribute.Closure _ -> - IContainer.iter_result - ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges - ~f:(fun (access, addr_trace) -> - if is_captured_fake_access access then - check_addr_access action addr_trace astate >>| fun _ -> () - else Ok () ) - | _ -> - Ok () ) - >>| fun () -> astate + let+ () = + IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function + | Attribute.Closure _ -> + IContainer.iter_result + ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges + ~f:(fun (access, addr_trace) -> + if is_captured_fake_access access then + let+ _ = check_addr_access action addr_trace astate in + () + else Ok () ) + | _ -> + Ok () ) + in + astate let record location pname captured astate = @@ -92,8 +95,8 @@ end let eval_var var astate = Stack.eval var astate let eval_access location addr_hist access astate = - check_addr_access location addr_hist astate - >>| fun astate -> Memory.eval_edge addr_hist access astate + let+ astate = check_addr_access location addr_hist astate in + Memory.eval_edge addr_hist access astate type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t @@ -180,29 +183,25 @@ let eval location exp0 astate = | Lvar pvar -> Ok (eval_var [ValueHistory.VariableAccessed (pvar, location)] (Var.of_pvar pvar) astate) | Lfield (exp', field, _) -> - eval exp' astate - >>= fun (astate, addr_hist) -> - check_addr_access location addr_hist astate - >>| fun astate -> Memory.eval_edge addr_hist (FieldAccess field) astate + let* astate, addr_hist = eval exp' astate in + let+ astate = check_addr_access location addr_hist astate in + Memory.eval_edge addr_hist (FieldAccess field) astate | Lindex (exp', exp_index) -> - eval exp_index astate - >>= fun (astate, addr_hist_index) -> - eval exp' astate - >>= fun (astate, addr_hist) -> - check_addr_access location addr_hist astate - >>| fun astate -> + let* astate, addr_hist_index = eval exp_index astate in + let* astate, addr_hist = eval exp' astate in + let+ astate = check_addr_access location addr_hist astate in Memory.eval_edge addr_hist (ArrayAccess (Typ.void, fst addr_hist_index)) astate | Closure {name; captured_vars} -> - List.fold_result captured_vars ~init:(astate, []) - ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) -> - eval capt_exp astate - >>| fun (astate, addr_trace) -> - let mode = - (* HACK: the frontend follows this discipline *) - match (capt_exp : Exp.t) with Lvar _ -> `ByReference | _ -> `ByValue - in - (astate, (captured_as, addr_trace, mode) :: rev_captured) ) - >>| fun (astate, rev_captured) -> + let+ astate, rev_captured = + List.fold_result captured_vars ~init:(astate, []) + ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) -> + let+ astate, addr_trace = eval capt_exp astate in + let mode = + (* HACK: the frontend follows this discipline *) + match (capt_exp : Exp.t) with Lvar _ -> `ByReference | _ -> `ByValue + in + (astate, (captured_as, addr_trace, mode) :: rev_captured) ) + in Closures.record location name (List.rev rev_captured) astate | Cast (_, exp') -> eval exp' astate @@ -220,15 +219,16 @@ let eval location exp0 astate = in Ok (astate, (addr, [])) | UnOp (unop, exp, _typ) -> - eval exp astate >>| fun (astate, (addr, hist)) -> eval_unop location unop addr hist astate + let+ astate, (addr, hist) = eval exp astate in + eval_unop location unop addr hist astate | BinOp (bop, e_lhs, e_rhs) -> - eval e_lhs astate - >>= fun (astate, (addr_lhs, hist_lhs)) -> - eval e_rhs astate - >>| fun ( astate - , ( addr_rhs - , (* NOTE: arbitrarily track only the history of the lhs, maybe not the brightest idea *) - _ ) ) -> + let* astate, (addr_lhs, hist_lhs) = eval e_lhs astate in + let+ ( astate + , ( addr_rhs + , (* NOTE: arbitrarily track only the history of the lhs, maybe not the brightest idea *) + _ ) ) = + eval e_rhs astate + in eval_binop location bop (AbstractValueOperand addr_lhs) (AbstractValueOperand addr_rhs) hist_lhs astate | Const _ | Sizeof _ | Exn _ -> @@ -248,8 +248,7 @@ let eval_arith location exp astate = , Trace.Immediate {location; history= [ValueHistory.Assignment location]} ) , Itv.ItvPure.of_int_lit i ) | exp -> - eval location exp astate - >>| fun (astate, (value, _)) -> + let+ astate, (value, _) = eval location exp astate in ( astate , Some value , AddressAttributes.get_arithmetic value astate @@ -296,10 +295,12 @@ let prune ~is_then_branch if_kind location ~condition astate = let rec prune_aux ~negated exp astate = match (exp : Exp.t) with | BinOp (bop, exp_lhs, exp_rhs) -> ( - eval_arith location exp_lhs astate - >>= fun (astate, value_lhs_opt, arith_lhs_opt, bo_itv_lhs) -> - eval_arith location exp_rhs astate - >>| fun (astate, value_rhs_opt, arith_rhs_opt, bo_itv_rhs) -> + let* astate, value_lhs_opt, arith_lhs_opt, bo_itv_lhs = + eval_arith location exp_lhs astate + in + let+ astate, value_rhs_opt, arith_rhs_opt, bo_itv_rhs = + eval_arith location exp_rhs astate + in match Arithmetic.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt) (Option.map ~f:fst arith_rhs_opt) @@ -340,10 +341,9 @@ let prune ~is_then_branch if_kind location ~condition astate = let eval_deref location exp astate = - eval location exp astate - >>= fun (astate, addr_hist) -> - check_addr_access location addr_hist astate - >>| fun astate -> Memory.eval_edge addr_hist Dereference astate + let* astate, addr_hist = eval location exp astate in + let+ astate = check_addr_access location addr_hist astate in + Memory.eval_edge addr_hist Dereference astate let realloc_pvar pvar location astate = @@ -387,8 +387,7 @@ let invalidate_deref location cause ref_addr_hist astate = let invalidate_array_elements location cause addr_trace astate = - check_addr_access location addr_trace astate - >>| fun astate -> + let+ astate = check_addr_access location addr_trace astate in match Memory.find_opt (fst addr_trace) astate with | None -> astate @@ -404,8 +403,7 @@ let invalidate_array_elements location cause addr_trace astate = let shallow_copy location addr_hist astate = - check_addr_access location addr_hist astate - >>| fun astate -> + let+ astate = check_addr_access location addr_hist astate in let cell = match AbductiveDomain.find_post_cell_opt (fst addr_hist) astate with | None -> @@ -458,7 +456,8 @@ let check_address_escape escape_location proc_desc address history astate = (Diagnostic.StackVariableAddressEscape {variable; location= escape_location; history}) ) else Ok () ) in - check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate + let+ () = check_address_of_cpp_temporary () >>= check_address_of_stack_variable in + astate let mark_address_of_cpp_temporary history variable address astate =