From ebe5028ca13cf6f83f3db96d2272205f02ce3d6e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 9 Apr 2019 06:53:42 -0700 Subject: [PATCH] [SIL] add `Skip` metadata instruction Summary: springcleaning2 Reviewed By: ezgicicek Differential Revision: D14827673 fbshipit-source-id: 0d3cf730b --- infer/src/IR/Sil.ml | 11 +++++++++-- infer/src/IR/Sil.mli | 1 + infer/src/backend/preanal.ml | 2 +- infer/src/biabduction/SymExec.ml | 2 ++ infer/src/bufferoverrun/bufferOverrunAnalysis.ml | 2 +- infer/src/checkers/cost.ml | 4 ++-- infer/src/nullsafe/typeCheck.ml | 2 +- infer/src/pulse/Pulse.ml | 2 +- infer/tests/codetoanalyze/cpp/pulse/issues.exp | 4 ++-- 9 files changed, 20 insertions(+), 10 deletions(-) diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index f387b0ca0..2d7206482 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -31,6 +31,7 @@ type instr_metadata = (** a good place to apply abstraction, mostly used in the biabduction analysis *) | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *) | Nullify of Pvar.t * Location.t (** nullify stack variable *) + | Skip (** no-op *) [@@deriving compare] (** An instruction. *) @@ -68,7 +69,7 @@ type instr = let equal_instr = [%compare.equal: instr] -let skip_instr = Metadata (ExitScope ([], Location.dummy)) +let skip_instr = Metadata Skip (** Check if an instruction is auxiliary, or if it comes from source instructions. *) let instr_is_auxiliary = function @@ -342,6 +343,8 @@ let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp let location_of_instr_metadata = function | Abstract loc | ExitScope (_, loc) | Nullify (_, loc) -> loc + | Skip -> + Location.dummy (** Get the location of the instruction *) @@ -359,6 +362,8 @@ let exps_of_instr_metadata = function List.map ~f:Var.to_exp vars | Nullify (pvar, _) -> [Exp.Lvar pvar] + | Skip -> + [] (** get the expressions occurring in the instruction *) @@ -400,6 +405,8 @@ let pp_instr_metadata pe f = function F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc | Nullify (pvar, loc) -> F.fprintf f "NULLIFY(%a); [%a]" (Pvar.pp pe) pvar Location.pp loc + | Skip -> + F.pp_print_string f "SKIP" let pp_instr ~print_types pe0 f instr = @@ -1304,7 +1311,7 @@ let instr_sub_ids ~sub_id_binders f instr = in let vars' = IList.map_changed ~equal:phys_equal ~f:sub_var vars in if phys_equal vars vars' then instr else Metadata (ExitScope (vars', loc)) - | Metadata (Abstract _ | Nullify _) -> + | Metadata (Abstract _ | Nullify _ | Skip) -> instr diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index 5409f2700..64f4bf2be 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -29,6 +29,7 @@ type instr_metadata = (** a good place to apply abstraction, mostly used in the biabduction analysis *) | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *) | Nullify of Pvar.t * Location.t (** nullify stack variable *) + | Skip (** no-op *) [@@deriving compare] (** An instruction. *) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index efb6c5333..322d4fd75 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -107,7 +107,7 @@ module NullifyTransferFunctions = struct (active_defs, to_nullify) | Sil.Store (Exp.Lvar lhs_pvar, _, _, _) -> (VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify) - | Sil.Store _ | Prune _ | Metadata (Abstract _ | ExitScope _) -> + | Sil.Store _ | Prune _ | Metadata (Abstract _ | ExitScope _ | Skip) -> astate | Sil.Metadata (Nullify _) -> L.(die InternalError) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 57206bd9f..a5b480be9 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1509,6 +1509,8 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) | Sil.Metadata (ExitScope (dead_vars, _)) -> let dead_ids = List.filter_map dead_vars ~f:Var.get_ident in ret_old_path [Prop.exist_quantify tenv dead_ids prop_] + | Sil.Metadata Skip -> + ret_old_path [prop_] and diverge prop path = diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index dcd791e11..1a9bd8203 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -272,7 +272,7 @@ module TransferFunctions = struct Dom.Mem.add_unknown id ~location mem | Metadata (ExitScope (dead_vars, _)) -> Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem - | Metadata (Abstract _ | Nullify _) -> + | Metadata (Abstract _ | Nullify _ | Skip) -> mem diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 16080e6a5..680d9b51f 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -602,13 +602,13 @@ module InstrBasicCost = struct CostDomain.zero_record | Sil.Load _ | Sil.Store _ | Sil.Call _ | Sil.Prune _ -> CostDomain.unit_cost_atomic_operation - | Sil.Metadata (ExitScope _) -> ( + | Sil.Metadata Skip -> ( match InstrCFG.Node.kind instr_node with | Procdesc.Node.Start_node -> CostDomain.unit_cost_atomic_operation | _ -> CostDomain.zero_record ) - | Sil.Metadata (Abstract _ | Nullify _) -> + | Sil.Metadata (Abstract _ | ExitScope _ | Nullify _) -> CostDomain.zero_record diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 30eae369c..62b5eaa01 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -423,7 +423,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p TypeState.remove_id id astate | Var.ProgramVar _ -> astate ) - | Sil.Metadata (Abstract _ | Nullify _) -> + | Sil.Metadata (Abstract _ | Nullify _ | Skip) -> typestate | Sil.Load (id, e, typ, loc) -> typecheck_expr_for_errors typestate e loc ; diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 36d86b885..f13c17d77 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -157,7 +157,7 @@ module PulseTransferFunctions = struct | Metadata (ExitScope (vars, _)) -> let post = PulseOperations.remove_vars vars astate in [post] - | Metadata (Abstract _ | Nullify _) -> + | Metadata (Abstract _ | Nullify _ | Skip) -> [astate] diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 069ce8548..c2376bec9 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 60 here,accessed `*(ptr)` here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 here,accessed `*(ptr)` here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 here,accessed `ptr` here] codetoanalyze/cpp/pulse/closures.cpp, delete_lambda_then_call_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `std::function<_fn_>::function(&(lambda),&(0$?%__sil_tmpSIL_materialize_temp__n$8))`,invalidated by destructor call `std::function<_fn_>::~function(lambda)` at line 102 here,accessed `lambda` here] codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$12))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 30 here,accessed `&(f)` here] @@ -7,7 +7,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ok, 2, USE_AFTE codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ptr_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 32 here,accessed `x` here] codetoanalyze/cpp/pulse/interprocedural.cpp, FP_may_return_invalid_ptr_ok, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Y))`,assigned to `y`,invalidated by call to `delete y` at line 81 here,accessed `y` here] codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 37 here,accessed `x` here] -codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 35 here,accessed `*(result)` here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 30 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(int))`,assigned to `x`,invalidated by call to `delete x` at line 112 here,accessed `x` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []