From b665e1c575b00b7b9fd662ae586f6054253d9059 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 9 Apr 2019 06:53:37 -0700 Subject: [PATCH] [SIL][HIL] distinguish auxiliary instructions as `Metadata` Summary: Bundle all non-semantic-bearing instructions into a `Metadata _` instruction in SIL. - On a documentation level this makes clearer the distinction between instructions that encode the semantics of the program and those that are just hints for the various backend analysis. - This makes it easier to add more of these auxiliary instructions in the future. For example, the next diff introduces a new `Skip` auxiliary instruction to replace the hacky `ExitScope([], Location.dummy)`. - It also makes it easier to surface all current and future such auxiliary instructions to HIL as the datatype for these syntactic hints can be shared between SIL and HIL. This diff brings `Nullify` and `Abstract` to HIL for free. Reviewed By: ngorogiannis Differential Revision: D14827674 fbshipit-source-id: f68fe2110 --- infer/src/IR/HilInstr.ml | 15 ++- infer/src/IR/HilInstr.mli | 3 +- infer/src/IR/Procdesc.ml | 33 +++---- infer/src/IR/Sil.ml | 94 ++++++++++++------- infer/src/IR/Sil.mli | 19 +++- infer/src/IR/SpecializeProcdesc.ml | 6 +- infer/src/absint/LowerHil.ml | 8 +- infer/src/backend/errdesc.ml | 6 +- infer/src/backend/preanal.ml | 10 +- infer/src/biabduction/State.ml | 4 +- infer/src/biabduction/SymExec.ml | 8 +- infer/src/biabduction/interproc.ml | 4 +- .../bufferoverrun/bufferOverrunAnalysis.ml | 4 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- infer/src/checkers/Ownership.ml | 2 +- infer/src/checkers/Siof.ml | 2 +- infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/cost.ml | 4 +- infer/src/checkers/functionPointers.ml | 2 +- infer/src/checkers/liveness.ml | 4 +- infer/src/checkers/uninit.ml | 2 +- infer/src/concurrency/RacerD.ml | 2 +- infer/src/concurrency/starvation.ml | 2 +- infer/src/labs/ResourceLeaks.ml | 2 +- infer/src/nullsafe/NullabilitySuggest.ml | 2 +- infer/src/nullsafe/typeCheck.ml | 4 +- infer/src/pulse/Pulse.ml | 4 +- infer/src/unit/procCfgTests.ml | 8 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 2 +- 29 files changed, 141 insertions(+), 119 deletions(-) diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index d27f831a0..5d5865e1b 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -22,7 +22,7 @@ type t = | Assign of HilExp.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 * Location.t + | Metadata of Sil.instr_metadata [@@deriving compare] let pp fmt = function @@ -35,11 +35,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, loc) -> - F.fprintf fmt "exit scope(%a) [%a]" (Pp.seq ~sep:"; " Var.pp) vars Location.pp loc + | Metadata instr_metadata -> + Sil.pp_instr_metadata Pp.text fmt instr_metadata -type translation = Instr of t | Bind of Var.t * HilExp.AccessExpression.t | Ignore +type translation = Instr of t | Bind of Var.t * HilExp.AccessExpression.t (** 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 @@ -121,8 +121,5 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = let hil_exp = exp_of_sil exp (Typ.mk (Tint IBool)) in let branch = if true_branch then `Then else `Else in Instr (Assume (hil_exp, branch, if_kind, loc)) - | ExitScope (vars, loc) -> - Instr (ExitScope (vars, loc)) - | Abstract _ | Nullify _ -> - (* these don't seem useful for most analyses. can translate them later if we want to *) - Ignore + | Metadata metadata -> + Instr (Metadata metadata) diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index c7ec4ff75..8dbfeba6c 100644 --- a/infer/src/IR/HilInstr.mli +++ b/infer/src/IR/HilInstr.mli @@ -20,7 +20,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 * Location.t + | Metadata of Sil.instr_metadata (** see {!Sil.instr_metadata} *) [@@deriving compare] val pp : F.formatter -> t -> unit @@ -29,7 +29,6 @@ val pp : F.formatter -> t -> unit type translation = | Instr of t (** HIL instruction to execute *) | Bind of Var.t * HilExp.AccessExpression.t (** add binding to identifier map *) - | Ignore (** no-op *) val of_sil : include_array_indexes:bool diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 57c944ce1..f856acc82 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -187,7 +187,7 @@ module Node = struct (** Get the source location of the last instruction in the node *) let get_last_loc n = - n |> get_instrs |> Instrs.last |> Option.value_map ~f:Sil.instr_get_loc ~default:n.loc + n |> get_instrs |> Instrs.last |> Option.value_map ~f:Sil.location_of_instr ~default:n.loc let find_in_node_or_preds = @@ -360,26 +360,17 @@ module Node = struct (** simple key for a node: just look at the instructions *) let simple_key node = let add_instr instr = - if Sil.instr_is_auxiliary instr then None - else - let instr_key = - match instr with - | Sil.Load _ -> - 1 - | Sil.Store _ -> - 2 - | Sil.Prune _ -> - 3 - | Sil.Call _ -> - 4 - | Sil.Nullify _ -> - 5 - | Sil.Abstract _ -> - 6 - | Sil.ExitScope _ -> - 7 - in - Some instr_key + match instr with + | Sil.Load _ -> + Some 1 + | Sil.Store _ -> + Some 2 + | Sil.Prune _ -> + Some 3 + | Sil.Call _ -> + Some 4 + | Sil.Metadata _ -> + None in get_instrs node |> IContainer.rev_filter_map_to_list ~fold:Instrs.fold ~f:add_instr diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 16551e018..f387b0ca0 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -26,6 +26,13 @@ type if_kind = | Ik_switch [@@deriving compare] +type instr_metadata = + | Abstract of Location.t + (** 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 *) +[@@deriving compare] + (** An instruction. *) type instr = (* Note for frontend writers: @@ -33,34 +40,41 @@ type instr = `Load` instruction may be eliminated by copy-propagation. *) | Load of Ident.t * Exp.t * Typ.t * Location.t (** Load a value from the heap into an identifier. + [x = *lexp:typ] where - [lexp] is an expression denoting a heap address - [typ] is the root type of [lexp]. *) + + - [lexp] is an expression denoting a heap address + + - [typ] is the root type of [lexp]. *) | Store of Exp.t * Typ.t * Exp.t * Location.t (** Store the value of an expression into the heap. + [*lexp1:typ = exp2] where - [lexp1] is an expression denoting a heap address - [typ] is the root type of [lexp1] - [exp2] is the expression whose value is store. *) + + - [lexp1] is an expression denoting a heap address + + - [typ] is the root type of [lexp1] + + - [exp2] is the expression whose value is store. *) | Prune of Exp.t * Location.t * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t (** [Call ((ret_id, ret_typ), e_fun, arg_ts, loc, call_flags)] represents an instruction [ret_id = e_fun(arg_ts);] *) - | Nullify of Pvar.t * Location.t (** nullify stack variable *) - | Abstract of Location.t (** apply abstraction *) - | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *) + | Metadata of instr_metadata + (** hints about the program that are not strictly needed to understand its semantics, for + instance information about its original syntactic structure *) [@@deriving compare] let equal_instr = [%compare.equal: instr] -let skip_instr = ExitScope ([], Location.dummy) +let skip_instr = Metadata (ExitScope ([], Location.dummy)) (** Check if an instruction is auxiliary, or if it comes from source instructions. *) let instr_is_auxiliary = function | Load _ | Store _ | Prune _ | Call _ -> false - | Nullify _ | Abstract _ | ExitScope _ -> + | Metadata _ -> true @@ -325,20 +339,30 @@ let d_offset_list (offl : offset list) = L.d_pp_with_pe pp_offset_list offl let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp pe) t +let location_of_instr_metadata = function + | Abstract loc | ExitScope (_, loc) | Nullify (_, loc) -> + loc + + (** Get the location of the instruction *) -let instr_get_loc = function - | Load (_, _, _, loc) - | Store (_, _, _, loc) - | Prune (_, loc, _, _) - | Call (_, _, _, loc, _) - | Nullify (_, loc) - | Abstract loc - | ExitScope (_, loc) -> +let location_of_instr = function + | Load (_, _, _, loc) | Store (_, _, _, loc) | Prune (_, loc, _, _) | Call (_, _, _, loc, _) -> loc + | Metadata metadata -> + location_of_instr_metadata metadata + + +let exps_of_instr_metadata = function + | Abstract _ -> + [] + | ExitScope (vars, _) -> + List.map ~f:Var.to_exp vars + | Nullify (pvar, _) -> + [Exp.Lvar pvar] (** get the expressions occurring in the instruction *) -let instr_get_exps = function +let exps_of_instr = function | Load (id, e, _, _) -> [Exp.Var id; e] | Store (e1, _, e2, _) -> @@ -347,12 +371,8 @@ let instr_get_exps = function [cond] | Call ((id, _), e, _, _, _) -> [e; Exp.Var id] - | Nullify (pvar, _) -> - [Exp.Lvar pvar] - | Abstract _ -> - [] - | ExitScope (vars, _) -> - List.map ~f:Var.to_exp vars + | Metadata metadata -> + exps_of_instr_metadata metadata (** Convert an if_kind to string *) @@ -373,7 +393,15 @@ let if_kind_to_string = function "switch" -(** Pretty print an instruction. *) +let pp_instr_metadata pe f = function + | Abstract loc -> + F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc + | ExitScope (vars, loc) -> + 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 + + let pp_instr ~print_types pe0 f instr = let pp_typ = if print_types then Typ.pp_full else Typ.pp in color_wrapper pe0 f instr ~f:(fun pe f instr -> @@ -392,12 +420,8 @@ let pp_instr ~print_types pe0 f instr = F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv ~print_types pe) e (Pp.comma_seq (pp_exp_typ pe)) arg_ts CallFlags.pp cf Location.pp loc - | Nullify (pvar, loc) -> - F.fprintf f "NULLIFY(%a); [%a]" (Pvar.pp pe) pvar Location.pp loc - | Abstract loc -> - F.fprintf f "APPLY_ABSTRACTION; [%a]" Location.pp loc - | ExitScope (vars, loc) -> - F.fprintf f "EXIT_SCOPE(%a); [%a]" (Pp.seq ~sep:"," Var.pp) vars Location.pp loc ) + | Metadata metadata -> + pp_instr_metadata pe0 f metadata ) let add_with_block_parameters_flag instr = @@ -1269,7 +1293,7 @@ let instr_sub_ids ~sub_id_binders f instr = | Prune (exp, loc, true_branch, if_kind) -> let exp' = exp_sub_ids f exp in if phys_equal exp' exp then instr else Prune (exp', loc, true_branch, if_kind) - | ExitScope (vars, loc) -> + | Metadata (ExitScope (vars, loc)) -> let sub_var var = match var with | Var.ProgramVar _ -> @@ -1279,8 +1303,8 @@ let instr_sub_ids ~sub_id_binders f instr = if phys_equal ident ident' then var else Var.of_id ident' in let vars' = IList.map_changed ~equal:phys_equal ~f:sub_var vars in - if phys_equal vars vars' then instr else ExitScope (vars', loc) - | Nullify _ | Abstract _ -> + if phys_equal vars vars' then instr else Metadata (ExitScope (vars', loc)) + | Metadata (Abstract _ | Nullify _) -> instr diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index cdd54fd87..5409f2700 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -24,6 +24,13 @@ type if_kind = | Ik_switch [@@deriving compare] +type instr_metadata = + | Abstract of Location.t + (** 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 *) +[@@deriving compare] + (** An instruction. *) type instr = (* Note for frontend writers: @@ -45,9 +52,9 @@ type instr = | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t (** [Call ((ret_id, ret_typ), e_fun, arg_ts, loc, call_flags)] represents an instruction [ret_id = e_fun(arg_ts);] *) - | Nullify of Pvar.t * Location.t (** nullify stack variable *) - | Abstract of Location.t (** apply abstraction *) - | ExitScope of Var.t list * Location.t (** remove temporaries and dead program variables *) + | Metadata of instr_metadata + (** hints about the program that are not strictly needed to understand its semantics, for + instance information about its original syntactic structure *) [@@deriving compare] val equal_instr : instr -> instr -> bool @@ -275,15 +282,17 @@ val pp_offset : Pp.env -> F.formatter -> offset -> unit val d_offset_list : offset list -> unit (** Dump a list of offsets *) -val instr_get_loc : instr -> Location.t +val location_of_instr : instr -> Location.t (** Get the location of the instruction *) -val instr_get_exps : instr -> Exp.t list +val exps_of_instr : instr -> Exp.t list (** get the expressions occurring in the instruction *) val if_kind_to_string : if_kind -> string (** Pretty print an if_kind *) +val pp_instr_metadata : Pp.env -> F.formatter -> instr_metadata -> unit + val pp_instr : print_types:bool -> Pp.env -> F.formatter -> instr -> unit (** Pretty print an instruction. *) diff --git a/infer/src/IR/SpecializeProcdesc.ml b/infer/src/IR/SpecializeProcdesc.ml index dc0e3c29b..e77543291 100644 --- a/infer/src/IR/SpecializeProcdesc.ml +++ b/infer/src/IR/SpecializeProcdesc.ml @@ -113,7 +113,7 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions = Some call_instr | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) -> Some (Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind)) - | Sil.Nullify _ | Abstract _ | ExitScope _ -> + | Sil.Metadata _ -> (* these are generated instructions that will be replaced by the preanalysis *) None in @@ -206,7 +206,7 @@ let with_block_args_instrs resolved_pdesc substitutions = (Var.of_id id, (Exp.Var id, pvar, typ), Sil.Load (id, Exp.Lvar pvar, typ, loc)) ) |> List.unzip3 in - let remove_temps_instr = Sil.ExitScope (dead_vars, loc) in + let remove_temps_instr = Sil.Metadata (ExitScope (dead_vars, loc)) in (block_name, id_exp_typs, load_instrs, remove_temps_instr) in let convert_generic_call return_ids exp origin_args loc call_flags = @@ -261,7 +261,7 @@ let with_block_args_instrs resolved_pdesc substitutions = convert_generic_call return_ids origin_call_exp origin_args loc call_flags | Sil.Prune (origin_exp, loc, is_true_branch, if_kind) -> (Sil.Prune (convert_exp origin_exp, loc, is_true_branch, if_kind) :: instrs, id_map) - | Sil.Nullify _ | Abstract _ | Sil.ExitScope _ -> + | Sil.Metadata _ -> (* these are generated instructions that will be replaced by the preanalysis *) (instrs, id_map) in diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index a924e2134..c0fb86383 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -68,17 +68,17 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) HilInstr.of_sil ~include_array_indexes:HilConfig.include_array_indexes ~f_resolve_id instr in match hil_translation with - | Ignore -> - (None, bindings) | Bind (id, access_path) -> (None, Bindings.add id access_path bindings) - | Instr (ExitScope (vars, loc)) -> + | Instr (Metadata (ExitScope (vars, loc))) -> let bindings, vars = List.fold vars ~init:(bindings, []) ~f:(fun (bindings, vars) var -> let bindings, vars' = Bindings.exit_scope var bindings in (bindings, append_bindings vars vars') ) in - let instr = if List.is_empty vars then None else Some (HilInstr.ExitScope (vars, loc)) in + let instr = + if List.is_empty vars then None else Some (HilInstr.Metadata (ExitScope (vars, loc))) + in (instr, bindings) | Instr instr -> (Some instr, bindings) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 259341e01..edaac36cb 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -499,7 +499,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = | None -> if verbose then L.d_strln "explain_leak: no current instruction" ; value_str_from_pvars_vpath [] vpath - | Some (Sil.Nullify (pvar, _)) when check_pvar pvar -> ( + | Some (Sil.Metadata (Nullify (pvar, _))) when check_pvar pvar -> ( if verbose then ( L.d_str "explain_leak: current instruction is Nullify for pvar " ; Pvar.d pvar ; @@ -509,10 +509,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = Some (DExp.to_string de) | _ -> None ) - | Some (Sil.Abstract _) -> + | Some (Sil.Metadata (Abstract _)) -> if verbose then L.d_strln "explain_leak: current instruction is Abstract" ; let get_nullify = function - | Sil.Nullify (pvar, _) when check_pvar pvar -> + | Sil.Metadata (Nullify (pvar, _)) when check_pvar pvar -> if verbose then ( L.d_str "explain_leak: found nullify before Abstract for pvar " ; Pvar.d pvar ; diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 5bfa1a36b..efb6c5333 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -29,7 +29,7 @@ let add_abstraction_instructions pdesc = in let do_node node = let loc = Node.get_last_loc node in - if node_requires_abstraction node then Node.append_instrs node [Sil.Abstract loc] + if node_requires_abstraction node then Node.append_instrs node [Sil.Metadata (Abstract loc)] in Procdesc.iter_nodes do_node pdesc @@ -107,9 +107,9 @@ 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 _ | ExitScope _ | Abstract _ -> + | Sil.Store _ | Prune _ | Metadata (Abstract _ | ExitScope _) -> astate - | Sil.Nullify _ -> + | Sil.Metadata (Nullify _) -> L.(die InternalError) "Should not add nullify instructions before running nullify analysis!" in @@ -141,7 +141,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map = let is_local pvar = not (Pvar.is_return pvar || Pvar.is_global pvar) in let prepend_node_nullify_instructions loc pvars instrs = List.fold pvars ~init:instrs ~f:(fun instrs pvar -> - if is_local pvar then Sil.Nullify (pvar, loc) :: instrs else instrs ) + if is_local pvar then Sil.Metadata (Nullify (pvar, loc)) :: instrs else instrs ) in let node_deadvars_instruction loc vars = let local_vars = @@ -151,7 +151,7 @@ let add_nullify_instrs pdesc tenv liveness_inv_map = | Var.LogicalVar _ -> true ) in - if List.is_empty local_vars then None else Some (Sil.ExitScope (local_vars, loc)) + if List.is_empty local_vars then None else Some (Sil.Metadata (ExitScope (local_vars, loc))) in Container.iter nullify_proc_cfg ~fold:ProcCfg.Exceptional.fold_nodes ~f:(fun node -> match NullifyAnalysis.extract_post (ProcCfg.Exceptional.Node.id node) nullify_inv_map with diff --git a/infer/src/biabduction/State.ml b/infer/src/biabduction/State.ml index 131be7a3d..f4e614fbd 100644 --- a/infer/src/biabduction/State.ml +++ b/infer/src/biabduction/State.ml @@ -92,13 +92,13 @@ let get_node () = !gs.last_node let get_loc_exn () = match !gs.last_instr with | Some instr -> - Sil.instr_get_loc instr + Sil.location_of_instr instr | None -> get_node_exn () |> Procdesc.Node.get_loc let get_loc () = - match !gs.last_instr with Some instr -> Some (Sil.instr_get_loc instr) | None -> None + match !gs.last_instr with Some instr -> Some (Sil.location_of_instr instr) | None -> None (** normalize the list of instructions by renaming let-bound ids *) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 2912e60d5..57206bd9f 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1480,7 +1480,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) ; proc_name= callee_pname ; loc ; exe_env } ) - | Sil.Nullify (pvar, _) -> ( + | Sil.Metadata (Nullify (pvar, _)) -> ( let eprop = Prop.expose prop_ in match List.partition_tf @@ -1500,13 +1500,13 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t) L.internal_error "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp Pp.text) pvar ; assert false ) - | Sil.Abstract _ -> + | Sil.Metadata (Abstract _) -> if Prover.check_inconsistency tenv prop_ then ret_old_path [] else ret_old_path [ Abs.remove_redundant_array_elements current_pname tenv (Abs.abstract current_pname tenv prop_) ] - | Sil.ExitScope (dead_vars, _) -> + | 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_] @@ -1940,7 +1940,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr | _ -> () ) ; let node_has_abstraction node = - let instr_is_abstraction = function Sil.Abstract _ -> true | _ -> false in + let instr_is_abstraction = function Sil.Metadata (Abstract _) -> true | _ -> false in Instrs.exists ~f:instr_is_abstraction (ProcCfg.Exceptional.instrs node) in let curr_node = State.get_node_exn () in diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index f005404e8..490622132 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -373,7 +373,7 @@ let do_after_node node = Printer.node_finish_session node (** Return the list of normal ids occurring in the instructions *) let instrs_get_normal_vars instrs = let do_instr res instr = - Sil.instr_get_exps instr + Sil.exps_of_instr instr |> List.fold_left ~init:res ~f:(fun res e -> Exp.free_vars e |> Sequence.filter ~f:Ident.is_normal @@ -559,7 +559,7 @@ let compute_visited vset = let lines = node_loc.Location.line :: IContainer.rev_map_to_list ~fold:Instrs.fold - ~f:(fun instr -> (Sil.instr_get_loc instr).Location.line) + ~f:(fun instr -> (Sil.location_of_instr instr).Location.line) (ProcCfg.Exceptional.instrs n) in List.remove_consecutive_duplicates ~equal:Int.equal (List.sort ~compare:Int.compare lines) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index dd56931fa..dcd791e11 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -270,9 +270,9 @@ module TransferFunctions = struct let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ; Dom.Mem.add_unknown id ~location mem - | ExitScope (dead_vars, _) -> + | Metadata (ExitScope (dead_vars, _)) -> Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem - | Abstract _ | Nullify _ -> + | Metadata (Abstract _ | Nullify _) -> mem diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index ae7e567de..cb5d37a68 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -120,7 +120,7 @@ let add_unreachable_code (cfg : CFG.t) (node : CFG.Node.t) instr rem_instrs (che && ExitStatement.is_end_of_block_or_procedure cfg node rem_instrs -> checks | _ -> - let location = Sil.instr_get_loc instr in + let location = Sil.location_of_instr instr in let unreachable_statement = UnreachableStatement.{location} in {checks with unreachable_statements= unreachable_statement :: checks.unreachable_statements} diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml index f910de9e4..97ef8ca31 100644 --- a/infer/src/checkers/Ownership.ml +++ b/infer/src/checkers/Ownership.ml @@ -372,7 +372,7 @@ 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 _ -> + | Metadata _ -> astate diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 577ec0986..8bd6ebf35 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -205,7 +205,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_actuals_globals astate pdesc loc actuals |> (* make sure it's not Bottom: we made a function call so this needs initialization *) at_least_nonbottom - | ExitScope _ | Abstract _ | Nullify _ -> + | Metadata _ -> astate diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 2b2e5cd52..aa8bd3be1 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate_acc in List.fold ~f:add_actual_by_ref ~init:astate actuals - | Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | ExitScope _ -> + | Sil.Store _ | Load _ | Prune _ | Metadata _ -> astate diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 23d884435..16080e6a5 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.ExitScope _ -> ( + | Sil.Metadata (ExitScope _) -> ( match InstrCFG.Node.kind instr_node with | Procdesc.Node.Start_node -> CostDomain.unit_cost_atomic_operation | _ -> CostDomain.zero_record ) - | _ -> + | Sil.Metadata (Abstract _ | Nullify _) -> CostDomain.zero_record diff --git a/infer/src/checkers/functionPointers.ml b/infer/src/checkers/functionPointers.ml index 9de4d863f..0e895b0cf 100644 --- a/infer/src/checkers/functionPointers.ml +++ b/infer/src/checkers/functionPointers.ml @@ -35,7 +35,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.Store (Lvar lhs_pvar, _, Exp.Const (Const.Cfun pn), _) -> (* strong update *) Domain.add (Pvar.to_string lhs_pvar) (ProcnameSet.singleton pn) astate - | Sil.Abstract _ | Call _ | Load _ | Nullify _ | Prune _ | ExitScope _ | Store _ -> + | Sil.Load _ | Store _ | Call _ | Prune _ | Metadata _ -> astate diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index b35bf6719..4a59d4ea3 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -157,7 +157,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct Domain.remove (Var.of_id ret_id) astate |> exp_add_live call_exp |> add_live_actuals actuals_to_read call_exp - | Sil.ExitScope _ | Abstract _ | Nullify _ -> + | Sil.Metadata _ -> astate @@ -185,7 +185,7 @@ module CapturedByRefTransferFunctions (CFG : ProcCfg.S) = struct type extras = ProcData.no_extras let exec_instr astate _ _ instr = - List.fold (Sil.instr_get_exps instr) + List.fold (Sil.exps_of_instr instr) ~f:(fun acc exp -> Exp.fold_captured exp ~f:(fun acc exp -> diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index ee90fc482..f35391076 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -299,7 +299,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with maybe_uninit_vars} | Assume (expr, _, _, loc) -> check_hil_expr expr ~loc ; astate - | ExitScope _ -> + | Metadata _ -> astate diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 4717b3eb2..d853df239 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -497,7 +497,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct do_assignment lhs_access_expr rhs_exp loc proc_data astate | Assume (assume_exp, _, _, loc) -> do_assume assume_exp loc proc_data astate - | ExitScope _ -> + | Metadata _ -> astate diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 6208835ad..5890d2958 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -88,7 +88,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct |> Option.value_map ~default:astate ~f:(Domain.integrate_summary tenv astate callee loc) in match instr with - | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | ExitScope _ -> + | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | Metadata _ -> astate | Call (_, Direct callee, actuals, _, _) when should_skip_analysis tenv callee actuals -> astate diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 26a33f901..36c14cfef 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -72,7 +72,7 @@ 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 _ -> + | Metadata _ -> astate diff --git a/infer/src/nullsafe/NullabilitySuggest.ml b/infer/src/nullsafe/NullabilitySuggest.ml index 16901595b..c2eaf8b7d 100644 --- a/infer/src/nullsafe/NullabilitySuggest.ml +++ b/infer/src/nullsafe/NullabilitySuggest.ml @@ -112,7 +112,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | None -> astate else astate - | ExitScope _ -> + | Metadata _ -> astate diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index a210c16ab..30eae369c 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -416,14 +416,14 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p ignore (typecheck_expr_simple typestate1 exp1 (Typ.mk Tvoid) TypeOrigin.Undef loc1) in match instr with - | Sil.ExitScope (vars, _) -> + | Sil.Metadata (ExitScope (vars, _)) -> List.fold_right vars ~init:typestate ~f:(fun var astate -> match var with | Var.LogicalVar id -> TypeState.remove_id id astate | Var.ProgramVar _ -> astate ) - | Sil.Abstract _ | Sil.Nullify _ -> + | Sil.Metadata (Abstract _ | Nullify _) -> 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 07c6f5c35..36d86b885 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -154,9 +154,11 @@ module PulseTransferFunctions = struct dispatch_call summary ret call actuals flags loc astate |> check_error summary in [post] - | ExitScope (vars, _) -> + | Metadata (ExitScope (vars, _)) -> let post = PulseOperations.remove_vars vars astate in [post] + | Metadata (Abstract _ | Nullify _) -> + [astate] let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index 5259b9904..1e07f0667 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -17,12 +17,12 @@ let tests = Cfg.create_proc_desc cfg (ProcAttributes.default (SourceFile.invalid __FILE__) Typ.Procname.empty_block) in - let dummy_instr1 = Sil.ExitScope ([], Location.dummy) in - let dummy_instr2 = Sil.Abstract Location.dummy in + let dummy_instr1 = Sil.skip_instr in + let dummy_instr2 = Sil.Metadata (Abstract Location.dummy) in let dummy_instr3 = - Sil.ExitScope ([Var.of_id (Ident.create_fresh Ident.knormal)], Location.dummy) + Sil.Metadata (ExitScope ([Var.of_id (Ident.create_fresh Ident.knormal)], Location.dummy)) in - let dummy_instr4 = Sil.ExitScope ([], Location.dummy) in + let dummy_instr4 = Sil.skip_instr in let instrs1 = [dummy_instr1; dummy_instr2] in let instrs2 = [dummy_instr3] in let instrs3 = [dummy_instr4] in diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 23ba5d5db..069ce8548 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,5 +1,5 @@ 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_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 70 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] codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 21 here,accessed `&(f)` here]