diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 75e71d8d8..a166b86c5 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -76,6 +76,129 @@ module Cplusplus = struct Ok [PulseOperations.havoc_id ret_id [event] astate] end +module StdAtomicInteger = struct + let internal_int = + Typ.Fieldname.Clang.from_class_name + (Typ.CStruct (QualifiedCppName.of_list ["std"; "atomic"])) + "__infer_model_backing_int" + + + 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 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 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, (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 ret_int = match prepost with `Pre -> new_int | `Post -> old_int in + PulseOperations.write_id ret_id (ret_int, event :: hist) astate + + + 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 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 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 operator_plus_plus_post this _int : model = + fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> + 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 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 operator_minus_minus_post this _int : model = + fun ~caller_summary:_ location ~ret:(ret_id, _) astate -> + 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 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)) -> + [PulseOperations.write_id ret_id (int, event :: hist) astate] + + + let load = load_instr "std::atomic::load()" + + 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) -> + 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 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] +end + module StdBasicString = struct let internal_string = Typ.Fieldname.Clang.from_class_name @@ -222,6 +345,29 @@ module ProcNameDispatcher = struct ; -"std" &:: "function" &:: "operator()" $ capt_arg_payload $++$--> StdFunction.operator_call ; -"std" &:: "function" &:: "operator=" $ capt_arg_payload $+ capt_arg_payload $--> Misc.shallow_copy "std::function::operator=" + ; -"std" &:: "atomic" &:: "atomic" <>$ capt_arg_payload $+ capt_arg_payload + $--> StdAtomicInteger.constructor + ; -"std" &:: "__atomic_base" &:: "fetch_add" <>$ capt_arg_payload $+ capt_arg_payload + $+ capt_arg_payload $--> StdAtomicInteger.fetch_add + ; -"std" &:: "__atomic_base" &:: "fetch_sub" <>$ capt_arg_payload $+ capt_arg_payload + $+ capt_arg_payload $--> StdAtomicInteger.fetch_sub + ; -"std" &:: "__atomic_base" &:: "exchange" <>$ capt_arg_payload $+ capt_arg_payload + $+ capt_arg_payload $--> StdAtomicInteger.exchange + ; -"std" &:: "__atomic_base" &:: "load" <>$ capt_arg_payload $+? capt_arg_payload + $--> StdAtomicInteger.load + ; -"std" &:: "__atomic_base" &:: "store" <>$ capt_arg_payload $+ capt_arg_payload + $+ capt_arg_payload $--> StdAtomicInteger.store + ; -"std" &:: "__atomic_base" &:: "operator++" <>$ capt_arg_payload + $--> StdAtomicInteger.operator_plus_plus_pre + ; -"std" &:: "__atomic_base" &:: "operator++" <>$ capt_arg_payload $+ capt_arg_payload + $--> StdAtomicInteger.operator_plus_plus_post + ; -"std" &:: "__atomic_base" &:: "operator--" <>$ capt_arg_payload + $--> StdAtomicInteger.operator_minus_minus_pre + ; -"std" &:: "__atomic_base" &:: "operator--" <>$ capt_arg_payload $+ capt_arg_payload + $--> StdAtomicInteger.operator_minus_minus_post + ; -"std" &:: "__atomic_base" + &::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name) + <>$ capt_arg_payload $+? capt_arg_payload $--> StdAtomicInteger.operator_t ; -"std" &:: "integral_constant" < any_typ &+ capt_int >::+ (fun _ name -> String.is_prefix ~prefix:"operator_" name) <>--> Misc.return_int diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 381a9bf1c..71ef788d1 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -96,6 +96,52 @@ let eval_access location addr_hist access astate = >>| fun astate -> Memory.eval_edge addr_hist access astate +type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t + +let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate = + let arith_of_op op astate = + match op with + | LiteralOperand i -> + Some (Arithmetic.equal_to i) + | AbstractValueOperand v -> + Memory.get_arithmetic v astate |> Option.map ~f:fst + in + match + Option.both (arith_of_op op_lhs astate) (arith_of_op op_rhs astate) + |> Option.bind ~f:(fun (addr_lhs, addr_rhs) -> Arithmetic.binop bop addr_lhs addr_rhs) + with + | None -> + astate + | Some binop_a -> + let binop_trace = Trace.Immediate {location; history= binop_hist} in + let astate = Memory.add_attribute binop_addr (Arithmetic (binop_a, binop_trace)) astate in + astate + + +let eval_bo_itv_binop binop_addr bop op_lhs op_rhs astate = + let bo_itv_of_op op astate = + match op with + | LiteralOperand i -> + Itv.of_int_lit i + | AbstractValueOperand v -> + Memory.get_bo_itv v astate + in + match Itv.arith_binop bop (bo_itv_of_op op_lhs astate) (bo_itv_of_op op_rhs astate) with + | None -> + astate + | Some itv -> + Memory.add_attribute binop_addr (BoItv itv) astate + + +let eval_binop location binop op_lhs op_rhs binop_hist astate = + let binop_addr = AbstractValue.mk_fresh () in + let astate = + eval_arith_operand location binop_addr binop_hist binop op_lhs op_rhs astate + |> eval_bo_itv_binop binop_addr binop op_lhs op_rhs + in + (astate, (binop_addr, binop_hist)) + + let eval location exp0 astate = let rec eval exp astate = match (exp : Exp.t) with @@ -162,27 +208,12 @@ let eval location exp0 astate = eval e_lhs astate >>= fun (astate, (addr_lhs, hist_lhs)) -> eval e_rhs astate - >>| fun (astate, (addr_rhs, _hist_rhs)) -> - let binop_addr = AbstractValue.mk_fresh () in - ( match - Option.both - (Memory.get_arithmetic addr_lhs astate) - (Memory.get_arithmetic addr_rhs astate) - |> Option.bind ~f:(function (a1, _), (a2, _) -> Arithmetic.binop bop a1 a2) - with - | None -> - (astate, (binop_addr, (* TODO history *) [])) - | Some binop_a -> - let binop_hist = (* TODO: add event *) hist_lhs in - let binop_trace = Trace.Immediate {location; history= binop_hist} in - let astate = - Memory.add_attribute binop_addr (Arithmetic (binop_a, binop_trace)) astate - in - (astate, (binop_addr, binop_hist)) ) - |> fun ((astate, ((addr, _) as addr_hist)) as default) -> - Itv.arith_binop bop (Memory.get_bo_itv addr_lhs astate) (Memory.get_bo_itv addr_rhs astate) - |> Option.value_map ~default ~f:(fun itv -> - (Memory.add_attribute addr (BoItv itv) astate, addr_hist) ) + >>| fun ( astate + , ( addr_rhs + , (* NOTE: arbitrarily track only the history of the lhs, maybe not the brightest idea *) + _ ) ) -> + eval_binop location bop (AbstractValueOperand addr_lhs) (AbstractValueOperand addr_rhs) + hist_lhs astate | Const _ | Sizeof _ | Exn _ -> Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) in @@ -208,12 +239,11 @@ let eval_arith location exp astate = (astate, Some addr, None) ) -let record_abduced ~is_then_branch if_kind location addr_opt orig_arith_hist_opt arith_opt astate = +let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate = match Option.both addr_opt arith_opt with | None -> astate | Some (addr, arith) -> - let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in let trace = match orig_arith_hist_opt with | None -> @@ -240,9 +270,10 @@ let prune ~is_then_branch if_kind location ~condition astate = | Unsatisfiable -> (astate, false) | Satisfiable (abduced1, abduced2) -> + let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in let astate = - record_abduced ~is_then_branch if_kind location addr1 eval1 abduced1 astate - |> record_abduced ~is_then_branch if_kind location addr2 eval2 abduced2 + record_abduced event location addr1 eval1 abduced1 astate + |> record_abduced event location addr2 eval2 abduced2 in (astate, true) ) | UnOp (LNot, exp', _) -> diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 7d6c1afe1..4c5e2441c 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -45,6 +45,17 @@ val eval_access : (** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if so dereferences it according to the access. *) +type operand = LiteralOperand of IntLit.t | AbstractValueOperand of AbstractValue.t + +val eval_binop : + Location.t + -> Binop.t + -> operand + -> operand + -> ValueHistory.t + -> t + -> t * (AbstractValue.t * ValueHistory.t) + val havoc_id : Ident.t -> ValueHistory.t -> t -> t val havoc_deref : diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index fb7709a41..5ea42fa36 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -33,6 +33,13 @@ codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,assigned,returned here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_strong_impossible_npe1_ok, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_strong_impossible_npe2_ok, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_weak_impossible_npe1_ok, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_weak_impossible_npe2_ok, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::exchange_possible_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::load_store_possible_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::pre_increment_decrement_test_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr::~UniquePtr` here,parameter `this` of temporaries::UniquePtr::~UniquePtr,when calling `temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::get`,return from call to `temporaries::UniquePtr::get`,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/std_atomics.cpp b/infer/tests/codetoanalyze/cpp/pulse/std_atomics.cpp new file mode 100644 index 000000000..5a0248fe6 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/std_atomics.cpp @@ -0,0 +1,169 @@ +/* + * 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. + */ +#include + +namespace atomic_test { + +void fetch_sub_add_ok() { + std::atomic a{0}; + int* p = nullptr; + a.fetch_add(1, std::memory_order_acq_rel); + a.fetch_add(1); + a.fetch_sub(1, std::memory_order_acq_rel); + a.fetch_sub(1); + int result_zero = a.fetch_sub(1); + if (result_zero != 0) { + *p = 42; + } +} + +void pre_increment_decrement_test_ok() { + std::atomic a{0}; + int* p = nullptr; + int x = ++a; + int y = --a; + if (a != 0 || x != 1 || y != a) { + *p = 42; + } +} + +void pre_increment_decrement_test_bad() { + std::atomic a{0}; + int* p = nullptr; + ++a; + --a; + if (a == 0) { + *p = 42; + } +} + +void post_increment_decrement_test_ok() { + std::atomic a{0}; + int* p = nullptr; + int x = a++; + int y = a--; + if (a != 0 || x != 0 || y != 1) { + *p = 42; + } +} + +void load_store_impossible_npe_ok() { + std::atomic a(0); + int* p = nullptr; + a.store(1); + if (a.load() != 1) { + *p = 42; + } +} + +void load_store_possible_npe_bad() { + std::atomic a(0); + int* p = nullptr; + a.store(1); + if (a.load() == 1) { + *p = 42; + } +} + +void exchange_impossible_npe_ok() { + std::atomic a(0); + int* p = nullptr; + int b = a.exchange(1); + if (a != 1 || b != 0) { + *p = 42; + } +} + +void exchange_possible_npe_bad() { + std::atomic a(0); + int* p = nullptr; + int b = a.exchange(1); + if (a == 1 && b == 0) { + *p = 42; + } +} + +void FP_compare_exchange_weak_impossible_npe1_ok() { + std::atomic a(0); + int b = 0; + int* p = nullptr; + int succ = a.compare_exchange_weak(b, 2); + if (a != 2 || b != 0 || !succ) { + *p = 42; + } +} + +void compare_exchange_weak_possible_npe1_bad() { + std::atomic a(0); + int b = 0; + int* p = nullptr; + int succ = a.compare_exchange_weak(b, 2); + if (a == 2 && b == 0 && succ) { + *p = 42; + } +} + +void FP_compare_exchange_weak_impossible_npe2_ok() { + std::atomic a(0); + int b = 1; + int* p = nullptr; + int succ = a.compare_exchange_weak(b, 2); + if (a != 0 || b != 0 || succ) { + *p = 42; + } +} + +void compare_exchange_weak_possible_npe2_bad() { + std::atomic a(0); + int b = 1; + int* p = nullptr; + int succ = a.compare_exchange_weak(b, 2); + if (a == 0 && b == 0 && !succ) { + *p = 42; + } +} + +void FP_compare_exchange_strong_impossible_npe1_ok() { + std::atomic a(0); + int b = 0; + int* p = nullptr; + int succ = a.compare_exchange_strong(b, 2); + if (a != 2 || b != 0 || !succ) { + *p = 42; + } +} + +void compare_exchange_strong_possible_npe1_bad() { + std::atomic a(0); + int b = 0; + int* p = nullptr; + int succ = a.compare_exchange_strong(b, 2); + if (a == 2 && b == 0 && succ) { + *p = 42; + } +} + +void FP_compare_exchange_strong_impossible_npe2_ok() { + std::atomic a(0); + int b = 1; + int* p = nullptr; + int succ = a.compare_exchange_strong(b, 2); + if (a != 0 || b != 0 || succ) { + *p = 42; + } +} + +void compare_exchange_strong_possible_npe2_bad() { + std::atomic a(0); + int b = 1; + int* p = nullptr; + int succ = a.compare_exchange_strong(b, 2); + if (a == 0 && b == 0 && !succ) { + *p = 42; + } +} +} // namespace atomic_test