diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index dec698852..f1a5b71d7 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -18,7 +18,7 @@ type t = ; racerd: RacerDDomain.summary option ; resources: ResourceLeakDomain.summary option ; siof: SiofDomain.Summary.astate option - ; typestate: unit TypeState.t option + ; typestate: TypeState.t option ; uninit: UninitDomain.summary option ; cost: CostDomain.summary option ; starvation: StarvationDomain.summary option } @@ -44,9 +44,7 @@ let pp pe fmt in F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a@\n" (pp_opt "Biabduction" (BiabductionSummary.pp pe)) - biabduction - (pp_opt "TypeState" (TypeState.pp TypeState.unit_ext)) - typestate + biabduction (pp_opt "TypeState" TypeState.pp) typestate (pp_opt "CrashContext" Crashcontext.pp_stacktree) crashcontext_frame (pp_opt "Quandary" QuandarySummary.pp) diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 9593ccb41..ba887adfc 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -18,7 +18,7 @@ type t = ; racerd: RacerDDomain.summary option ; resources: ResourceLeakDomain.summary option ; siof: SiofDomain.Summary.astate option - ; typestate: unit TypeState.t option + ; typestate: TypeState.t option ; uninit: UninitDomain.summary option ; cost: CostDomain.summary option ; starvation: StarvationDomain.summary option } diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index bd6472867..65d93ffec 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -27,17 +27,13 @@ end (** Extension to the type checker. *) module type ExtensionT = sig - type extension - - val ext : extension TypeState.ext - - val update_payloads : extension TypeState.t option -> Payloads.t -> Payloads.t + val update_payloads : TypeState.t option -> Payloads.t -> Payloads.t end (** Create a module with the toplevel callback. *) module MkCallback (Extension : ExtensionT) : CallBackT = struct let callback1 tenv find_canonical_duplicate calls_this checks idenv curr_pname curr_pdesc - annotated_signature linereader proc_loc : bool * Extension.extension TypeState.t option = + annotated_signature linereader proc_loc : bool * TypeState.t option = let mk s = Pvar.mk s curr_pname in let add_formal typestate (s, ia, typ) = let pvar = mk s in @@ -48,7 +44,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct TypeState.add pvar (typ, ta, []) typestate in let get_initial_typestate () = - let typestate_empty = TypeState.empty Extension.ext in + let typestate_empty = TypeState.empty in List.fold ~f:add_formal ~init:typestate_empty annotated_signature.AnnotatedSignature.params in (* Check the nullable flag computed for the return value and report inconsistencies. *) @@ -74,18 +70,18 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct in let do_before_dataflow initial_typestate = if Config.eradicate_verbose then - L.result "Initial Typestate@\n%a@." (TypeState.pp Extension.ext) initial_typestate + L.result "Initial Typestate@\n%a@." TypeState.pp initial_typestate in let do_after_dataflow find_canonical_duplicate final_typestate = let exit_node = Procdesc.get_exit_node curr_pdesc in check_return find_canonical_duplicate exit_node final_typestate annotated_signature proc_loc in let module DFTypeCheck = MakeDF (struct - type t = Extension.extension TypeState.t + type t = TypeState.t let equal = TypeState.equal - let join = TypeState.join Extension.ext + let join = TypeState.join let pp_name fmt = F.pp_print_string fmt "eradicate" @@ -93,11 +89,11 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct NodePrinter.start_session ~pp_name node ; State.set_node node ; let typestates_succ, typestates_exn = - TypeCheck.typecheck_node tenv Extension.ext calls_this checks idenv curr_pname curr_pdesc + TypeCheck.typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc find_canonical_duplicate annotated_signature typestate node linereader in if Config.write_html then ( - let d_typestate ts = L.d_strln (F.asprintf "%a" (TypeState.pp Extension.ext) ts) in + let d_typestate ts = L.d_strln (F.asprintf "%a" TypeState.pp ts) in L.d_strln "before:" ; d_typestate typestate ; L.d_strln "after:" ; @@ -291,8 +287,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct EradicateChecks.check_constructor_initialization tenv find_canonical_duplicate curr_pname curr_pdesc start_node Initializers.final_initializer_typestates_lazy Initializers.final_constructor_typestates_lazy proc_loc ; - if Config.eradicate_verbose then - L.result "Final Typestate@\n%a@." (TypeState.pp Extension.ext) typestate + if Config.eradicate_verbose then L.result "Final Typestate@\n%a@." TypeState.pp typestate in match typestate_opt with None -> () | Some typestate -> do_typestate typestate in @@ -342,16 +337,6 @@ end (* MkCallback *) module EmptyExtension : ExtensionT = struct - type extension = unit - - let ext = - let empty = () in - let check_instr _ _ _ ext _ _ = ext in - let join () () = () in - let pp _ () = () in - {TypeState.empty; check_instr; join; pp} - - let update_payloads typestate_opt (payloads: Payloads.t) = {payloads with typestate= typestate_opt} end diff --git a/infer/src/eradicate/eradicate.mli b/infer/src/eradicate/eradicate.mli index f095912c0..e8327a26b 100644 --- a/infer/src/eradicate/eradicate.mli +++ b/infer/src/eradicate/eradicate.mli @@ -21,9 +21,5 @@ end (** Extension to the type checker. *) module type ExtensionT = sig - type extension - - val ext : extension TypeState.ext - - val update_payloads : extension TypeState.t option -> Payloads.t -> Payloads.t + val update_payloads : TypeState.t option -> Payloads.t -> Payloads.t end diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index b310646b6..7cf348eac 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -204,7 +204,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r (** Typecheck an instruction. *) -let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv curr_pname curr_pdesc +let typecheck_instr tenv calls_this checks (node: Procdesc.Node.t) idenv curr_pname curr_pdesc find_canonical_duplicate annotated_signature instr_ref linereader typestate instr = (* let print_current_state () = *) (* L.stdout "Current Typestate in node %a@\n%a@." *) @@ -826,28 +826,18 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv cur if checks.eradicate then EradicateChecks.check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_attributes resolved_params loc instr_ref ; - let typestate2 = - if checks.check_extension then - let etl' = List.map ~f:(fun ((_, e), t) -> (e, t)) call_params in - let extension = TypeState.get_extension typestate1 in - let extension' = - ext.TypeState.check_instr tenv curr_pname curr_pdesc extension instr etl' - in - TypeState.set_extension typestate1 extension' - else typestate1 - in if Models.is_check_not_null callee_pname then if Typ.Procname.Java.is_vararg callee_pname_java then let last_parameter = List.length call_params in - do_preconditions_check_not_null last_parameter ~is_vararg:true typestate2 + do_preconditions_check_not_null last_parameter ~is_vararg:true typestate1 else do_preconditions_check_not_null (Models.get_check_not_null_parameter callee_pname) - ~is_vararg:false typestate2 + ~is_vararg:false typestate1 else if Models.is_check_state callee_pname || Models.is_check_argument callee_pname - then do_preconditions_check_state typestate2 - else if Models.is_mapPut callee_pname then do_map_put typestate2 - else typestate2 ) + then do_preconditions_check_state typestate1 + else if Models.is_mapPut callee_pname then do_map_put typestate1 + else typestate1 ) else typestate1 in (typestate_after_call, resolved_ret) @@ -856,7 +846,7 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv cur | Sil.Call _ -> typestate | Sil.Prune (cond, loc, true_branch, _) -> - let rec check_condition node' c : _ TypeState.t = + let rec check_condition node' c : TypeState.t = (* check if the expression is coming from a call, and return the argument *) let from_call filter_callee e : Exp.t option = match e with @@ -1068,7 +1058,7 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv cur (** Typecheck the instructions in a cfg node. *) -let typecheck_node tenv ext calls_this checks idenv curr_pname curr_pdesc find_canonical_duplicate +let typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc find_canonical_duplicate annotated_signature typestate node linereader = let instrs = Procdesc.Node.get_instrs node in let instr_ref_gen = TypeErr.InstrRef.create_generator node in @@ -1099,13 +1089,13 @@ let typecheck_node tenv ext calls_this checks idenv curr_pname curr_pdesc find_c () in let canonical_node = find_canonical_duplicate node in - let do_instruction ext typestate instr = + let do_instruction typestate instr = let instr_ref = (* keep unique instruction reference per-node *) TypeErr.InstrRef.gen instr_ref_gen in let instr' = - typecheck_instr tenv ext calls_this checks node idenv curr_pname curr_pdesc + typecheck_instr tenv calls_this checks node idenv curr_pname curr_pdesc find_canonical_duplicate annotated_signature instr_ref linereader typestate instr in handle_exceptions typestate instr ; instr' @@ -1113,7 +1103,7 @@ let typecheck_node tenv ext calls_this checks idenv curr_pname curr_pdesc find_c (* Reset 'always' field for forall errors to false. *) (* This is used to track if it is set to true for all visit to the node. *) TypeErr.node_reset_forall canonical_node ; - let typestate_succ = Instrs.fold ~f:(do_instruction ext) ~init:typestate instrs in + let typestate_succ = Instrs.fold ~f:do_instruction ~init:typestate instrs in let dont_propagate = Procdesc.Node.equal_nodekind (Procdesc.Node.get_kind node) Procdesc.Node.exn_sink_kind (* don't propagate exceptions *) diff --git a/infer/src/eradicate/typeCheck.mli b/infer/src/eradicate/typeCheck.mli index 513cd928a..f54b9f646 100644 --- a/infer/src/eradicate/typeCheck.mli +++ b/infer/src/eradicate/typeCheck.mli @@ -17,6 +17,6 @@ type find_canonical_duplicate = Procdesc.Node.t -> Procdesc.Node.t type checks = {eradicate: bool; check_extension: bool; check_ret_type: check_return_type list} val typecheck_node : - Tenv.t -> 'a TypeState.ext -> bool ref -> checks -> Idenv.t -> Typ.Procname.t -> Procdesc.t - -> find_canonical_duplicate -> AnnotatedSignature.t -> 'a TypeState.t -> Procdesc.Node.t - -> Printer.LineReader.t -> 'a TypeState.t list * 'a TypeState.t list + Tenv.t -> bool ref -> checks -> Idenv.t -> Typ.Procname.t -> Procdesc.t + -> find_canonical_duplicate -> AnnotatedSignature.t -> TypeState.t -> Procdesc.Node.t + -> Printer.LineReader.t -> TypeState.t list * TypeState.t list diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index e374e7940..9d32d0a56 100644 --- a/infer/src/eradicate/typeState.ml +++ b/infer/src/eradicate/typeState.ml @@ -11,21 +11,6 @@ module F = Format (** Module for typestates: maps from expressions to annotated types, with extensions. *) -(** Parameters of a call. *) -type parameters = (Exp.t * Typ.t) list - -(** Extension to a typestate with values of type 'a. *) -type 'a ext = - { empty: 'a (** empty extension *) - ; check_instr: Tenv.t -> Typ.Procname.t -> Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a - (** check the extension for an instruction *) - ; join: 'a -> 'a -> 'a (** join two extensions *) - ; pp: Format.formatter -> 'a -> unit (** pretty print an extension *) } - -let unit_ext : unit ext = - {empty= (); check_instr= (fun _ _ _ () _ _ -> ()); join= (fun () () -> ()); pp= (fun _ () -> ())} - - module M = Caml.Map.Make (struct type t = Exp.t @@ -34,16 +19,13 @@ end) type range = Typ.t * TypeAnnotation.t * Location.t list [@@deriving compare] -type 'a t = {map: range M.t; extension: 'a} [@@deriving compare] - -(* Ignore the extension field, which is a pure instrumentation *) -let compare t1 t2 = compare (fun _ _ -> 0) t1 t2 +type t = range M.t [@@deriving compare] -let equal t1 t2 = Int.equal (compare t1 t2) 0 +let equal = [%compare.equal : t] -let empty ext = {map= M.empty; extension= ext.empty} +let empty = M.empty -let pp ext fmt typestate = +let pp fmt typestate = let pp_loc fmt loc = F.pp_print_int fmt loc.Location.line in let pp_locs fmt locs = F.fprintf fmt " [%a]" (Pp.seq pp_loc) locs in let pp_one exp (typ, ta, locs) = @@ -52,7 +34,7 @@ let pp ext fmt typestate = (TypeAnnotation.to_string ta) (Typ.pp_full Pp.text) typ pp_locs locs in let pp_map map = M.iter pp_one map in - pp_map typestate.map ; ext.pp fmt typestate.extension + pp_map typestate let type_join typ1 typ2 = if PatternMatch.type_is_object typ1 then typ2 else typ1 @@ -105,36 +87,20 @@ let map_join m1 m2 = if phys_equal m1 m2 then m1 else ( M.iter extend_lhs m2 ; M.iter missing_rhs m1 ; !tjoined ) -let join ext t1 t2 = - let tjoin = {map= map_join t1.map t2.map; extension= ext.join t1.extension t2.extension} in +let join t1 t2 = + let tjoin = map_join t1 t2 in ( if Config.write_html then - let s = - F.asprintf "State 1:@.%a@.State 2:@.%a@.After Join:@.%a@." (pp ext) t1 (pp ext) t2 (pp ext) - tjoin - in + let s = F.asprintf "State 1:@.%a@.State 2:@.%a@.After Join:@.%a@." pp t1 pp t2 pp tjoin in L.d_strln s ) ; tjoin -let lookup_id id typestate = M.find_opt (Exp.Var id) typestate.map - -let lookup_pvar pvar typestate = M.find_opt (Exp.Lvar pvar) typestate.map - -let add_id id range typestate = - let map' = M.add (Exp.Var id) range typestate.map in - if phys_equal map' typestate.map then typestate else {typestate with map= map'} - - -let add pvar range typestate = - let map' = M.add (Exp.Lvar pvar) range typestate.map in - if phys_equal map' typestate.map then typestate else {typestate with map= map'} - +let lookup_id id typestate = M.find_opt (Exp.Var id) typestate -let remove_id id typestate = - let map' = M.remove (Exp.Var id) typestate.map in - if phys_equal map' typestate.map then typestate else {typestate with map= map'} +let lookup_pvar pvar typestate = M.find_opt (Exp.Lvar pvar) typestate +let add_id id range typestate = M.add (Exp.Var id) range typestate -let get_extension typestate = typestate.extension +let add pvar range typestate = M.add (Exp.Lvar pvar) range typestate -let set_extension typestate extension = {typestate with extension} +let remove_id id typestate = M.remove (Exp.Var id) typestate diff --git a/infer/src/eradicate/typeState.mli b/infer/src/eradicate/typeState.mli index acebf7226..9f451e683 100644 --- a/infer/src/eradicate/typeState.mli +++ b/infer/src/eradicate/typeState.mli @@ -9,44 +9,27 @@ open! IStd (** Module for typestates: maps from expressions to annotated types, with extensions. *) -(** Parameters of a call. *) -type parameters = (Exp.t * Typ.t) list - -(** Extension to a typestate with values of type 'a. *) -type 'a ext = - { empty: 'a (** empty extension *) - ; check_instr: Tenv.t -> Typ.Procname.t -> Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a - (** check the extension for an instruction *) - ; join: 'a -> 'a -> 'a (** join two extensions *) - ; pp: Format.formatter -> 'a -> unit (** pretty print an extension *) } - -(** Typestate extended with elements of type 'a. *) -type 'a t +(** Typestate *) +type t type range = Typ.t * TypeAnnotation.t * Location.t list -val add_id : Ident.t -> range -> 'a t -> 'a t - -val add : Pvar.t -> range -> 'a t -> 'a t +val add_id : Ident.t -> range -> t -> t -val empty : 'a ext -> 'a t +val add : Pvar.t -> range -> t -> t -val equal : 'a t -> 'a t -> bool +val empty : t -val get_extension : 'a t -> 'a +val equal : t -> t -> bool -val join : 'a ext -> 'a t -> 'a t -> 'a t +val join : t -> t -> t -val lookup_id : Ident.t -> 'a t -> range option +val lookup_id : Ident.t -> t -> range option -val lookup_pvar : Pvar.t -> 'a t -> range option +val lookup_pvar : Pvar.t -> t -> range option -val pp : 'a ext -> Format.formatter -> 'a t -> unit +val pp : Format.formatter -> t -> unit val range_add_locs : range -> Location.t list -> range -val remove_id : Ident.t -> 'a t -> 'a t - -val set_extension : 'a t -> 'a -> 'a t - -val unit_ext : unit ext +val remove_id : Ident.t -> t -> t