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]