diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index 9185be8e3..d69085b10 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -22,6 +22,7 @@ type t = | Assign of AccessExpression.t * HilExp.t * Location.t | Assume of HilExp.t * [`Then | `Else] * Sil.if_kind * Location.t | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t + | ExitScope of Var.t list [@@deriving compare] let pp fmt = function @@ -33,13 +34,11 @@ let pp fmt = function let pp_ret fmt = F.fprintf fmt "%a := " AccessPath.pp_base in let pp_actuals fmt = PrettyPrintable.pp_collection ~pp_item:HilExp.pp fmt in F.fprintf fmt "%a%a(%a) [%a]" pp_ret ret pp_call call pp_actuals actuals Location.pp loc + | ExitScope vars -> + F.fprintf fmt "exit scope [%a]" (Pp.seq ~sep:"; " Var.pp) vars -type translation = - | Instr of t - | Bind of Var.t * AccessExpression.t - | Unbind of Var.t list - | Ignore +type translation = Instr of t | Bind of Var.t * AccessExpression.t | Ignore (** convert an SIL instruction into an HIL instruction. The [f_resolve_id] function should map an SSA temporary variable to the access path it represents. Evaluating the HIL instruction should @@ -122,8 +121,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = let branch = if true_branch then `Then else `Else in Instr (Assume (hil_exp, branch, if_kind, loc)) | ExitScope (vars, _) -> - Unbind vars - (* ignoring for now; will translate as builtin function call if needed *) + Instr (ExitScope vars) | Abstract _ | Nullify _ -> (* these don't seem useful for most analyses. can translate them later if we want to *) Ignore diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index 124434773..92a6f1913 100644 --- a/infer/src/IR/HilInstr.mli +++ b/infer/src/IR/HilInstr.mli @@ -18,6 +18,7 @@ type t = (** Assumed expression, true_branch boolean, source of the assume (conditional, ternary, etc.) *) | Call of AccessPath.base * call * HilExp.t list * CallFlags.t * Location.t (** Var to hold the return, call expression, formals *) + | ExitScope of Var.t list [@@deriving compare] val pp : F.formatter -> t -> unit @@ -26,7 +27,6 @@ val pp : F.formatter -> t -> unit type translation = | Instr of t (** HIL instruction to execute *) | Bind of Var.t * AccessExpression.t (** add binding to identifier map *) - | Unbind of Var.t list (** remove binding from identifier map *) | Ignore (** no-op *) val of_sil : diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index ba9e72806..a5eab3d23 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -19,8 +19,8 @@ let update_id_map hil_translation id_map = match (hil_translation : HilInstr.translation) with | Bind (id, access_path) -> IdAccessPathMapDomain.add id access_path id_map - | Unbind ids -> - List.fold ~f:(fun acc id -> IdAccessPathMapDomain.remove id acc) ~init:id_map ids + | Instr (ExitScope vars) -> + List.fold ~f:(fun acc var -> IdAccessPathMapDomain.remove var acc) ~init:id_map vars | Instr _ | Ignore -> id_map @@ -80,14 +80,14 @@ struct let hil_translation = HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr in - let id_map' = update_id_map hil_translation id_map in let actual_state', id_map' = match hil_translation with | Instr hil_instr -> - exec_instr_actual extras id_map' node hil_instr actual_state - | Bind _ | Unbind _ | Ignore -> - (actual_state, id_map') + exec_instr_actual extras id_map node hil_instr actual_state + | Bind _ | Ignore -> + (actual_state, id_map) in + let id_map' = update_id_map hil_translation id_map' in if phys_equal id_map id_map' && phys_equal actual_state actual_state' then astate else (actual_state', id_map') end @@ -111,7 +111,7 @@ struct match hil_translation with | Instr hil_instr -> Some (fun f -> Format.fprintf f "@[%a@];@;" HilInstr.pp hil_instr) - | Bind _ | Unbind _ | Ignore -> + | Bind _ | Ignore -> None in Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 30d11c18d..fd4fa8750 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -111,6 +111,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> astate else astate + | ExitScope _ -> + astate let pp_session_name _node fmt = F.pp_print_string fmt "nullability suggest" diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml index 209e7df76..9e95e2026 100644 --- a/infer/src/checkers/Ownership.ml +++ b/infer/src/checkers/Ownership.ml @@ -371,6 +371,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Domain.remove ret_id_typ astate' ) | Assume (assume_exp, _, _, loc) -> Domain.exp_add_reads assume_exp loc summary astate + | ExitScope _ -> + astate let pp_session_name _node fmt = F.pp_print_string fmt "ownership" diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index 37ceb15e6..dda249144 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -122,6 +122,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct PulseDomain.read_all loc (HilExp.get_access_exprs condition) astate |> check_error summary | Call (ret, call, actuals, flags, loc) -> dispatch_call ret call actuals flags loc astate |> check_error summary + | ExitScope vars -> + PulseDomain.remove_vars vars astate let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 681f6cbe8..5626fecc3 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -611,6 +611,11 @@ module Operations = struct materialize_address astate access_expr location >>= fun (astate, addr) -> check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr + + + let remove_vars vars astate = + let stack = List.fold ~f:(fun var stack -> Stack.remove stack var) ~init:astate.stack vars in + if phys_equal stack astate.stack then astate else {astate with stack} end module StdVector = struct diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 246f9e8f6..72a54a7cc 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -52,3 +52,5 @@ val write_var : Var.t -> AbstractAddress.t -> t -> t val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result val invalidate : PulseInvalidation.t -> Location.t -> AccessExpression.t -> t -> t access_result + +val remove_vars : Var.t list -> t -> t diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index ef085c70e..2f425c52a 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -298,7 +298,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with maybe_uninit_vars} | Assume (expr, _, _, loc) -> check_hil_expr expr ~loc ; astate - + | ExitScope _ -> + astate let pp_session_name node fmt = F.fprintf fmt "uninit %a" CFG.Node.pp_id (CFG.Node.id node) end diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index cf20d3c00..77d8eab36 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -591,6 +591,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct L.(die InternalError) "Unexpected indirect call instruction %a" HilInstr.pp instr | _ -> astate ) + | ExitScope _ -> + astate let pp_session_name _node fmt = F.pp_print_string fmt "racerd" diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index fa1cc745a..3f7434276 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -85,6 +85,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (_, Indirect _, _, _, _) -> (* This should never happen in Java. Fail if it does. *) L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr + | ExitScope _ -> + astate let pp_session_name _node fmt = F.pp_print_string fmt "resource leaks" diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 26078a187..0424cdad1 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -12,7 +12,6 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 24, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 73, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 102, column 3 here,accessed `s->f` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_allocate_in_branch_ok, 9, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `std::unique_ptr>_~unique_ptr(a2)` at line 244, column 1 here,accessed `a1` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `use_after_destructor::S_~S(s)` at line 64, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete alias` at line 142, column 3 here,accessed `s` here] codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 150, column 3 here,accessed `alias` here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp index 2edd8e252..a0c88c2cd 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp @@ -232,7 +232,7 @@ void FP_destructor_order_empty_destructor_ok() { a.f = &b; } -void FP_allocate_in_branch_ok(bool b) { +void allocate_in_branch_ok(bool b) { std::unique_ptr a1; std::unique_ptr a2; std::unique_ptr* a3 = &a1;