diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index 5f67e6ad6..e7d03d941 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -138,7 +138,7 @@ let default translation_unit proc_name = ; method_annotation= Annot.Method.empty ; objc_accessor= None ; proc_name - ; ret_type= Typ.void } + ; ret_type= StdTyp.void } let pp_parameters = diff --git a/infer/src/IR/Procname.ml b/infer/src/IR/Procname.ml index 7f113db07..c09cfa413 100644 --- a/infer/src/IR/Procname.ml +++ b/infer/src/IR/Procname.ml @@ -110,7 +110,7 @@ module Java = struct let to_simplified_string ?(withclass = false) = Pp.string_of_pp (pp ~withclass Simple) - let get_return_typ pname_java = Option.value ~default:Typ.void pname_java.return_type + let get_return_typ pname_java = Option.value ~default:StdTyp.void pname_java.return_type let is_close {method_name} = String.equal method_name "close" @@ -120,7 +120,7 @@ module Java = struct { method_name= class_initializer_method_name ; parameters= [] ; class_name - ; return_type= Some Typ.void + ; return_type= Some StdTyp.void ; kind= Static } @@ -163,7 +163,7 @@ module Java = struct let is_vararg {parameters} = match List.last parameters with | Some {desc= Tptr ({desc= Tarray {elt}}, Pk_pointer)} -> - Typ.(equal pointer_to_java_lang_object elt) + Typ.equal StdTyp.Java.pointer_to_java_lang_object elt | _ -> false diff --git a/infer/src/IR/StdTyp.ml b/infer/src/IR/StdTyp.ml new file mode 100644 index 000000000..020aee6fc --- /dev/null +++ b/infer/src/IR/StdTyp.ml @@ -0,0 +1,71 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +type t = Typ.t + +let boolean = Typ.mk (Tint IBool) + +let char = Typ.mk (Tint IChar) + +let double = Typ.mk (Tfloat FDouble) + +let float = Typ.mk (Tfloat FFloat) + +let int = Typ.mk (Tint IInt) + +let long = Typ.mk (Tint ILong) + +let uint = Typ.mk (Tint IUInt) + +let void = Typ.mk Tvoid + +let void_star = Typ.mk_ptr void + +module Name = struct + type t = Typ.Name.t + + module Java = struct + open Typ.Name.Java + + let java_io_serializable = from_string "java.io.Serializable" + + let java_lang_class = from_string "java.lang.Class" + + let java_lang_cloneable = from_string "java.lang.Cloneable" + + let java_lang_object = from_string "java.lang.Object" + + let java_lang_string = from_string "java.lang.String" + end + + module Objc = struct + open Typ.Name.Objc + + let ns_enumerator = from_string "NSEnumerator" + end +end + +module Java = struct + let byte = Typ.mk (Tint ISChar) + + let char = Typ.mk (Tint IUShort) + + let short = Typ.mk (Tint IShort) + + let pointer_to_java_lang_class = Typ.mk_ptr (Typ.mk_struct Name.Java.java_lang_class) + + let pointer_to_java_lang_object = Typ.mk_ptr (Typ.mk_struct Name.Java.java_lang_object) + + let pointer_to_java_lang_string = Typ.mk_ptr (Typ.mk_struct Name.Java.java_lang_string) +end + +module Objc = struct + let pointer_to_nszone = + Typ.(mk_ptr (mk_struct (CStruct (QualifiedCppName.of_qual_string "NSZone")))) +end diff --git a/infer/src/IR/StdTyp.mli b/infer/src/IR/StdTyp.mli new file mode 100644 index 000000000..daf06c48b --- /dev/null +++ b/infer/src/IR/StdTyp.mli @@ -0,0 +1,67 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +type t = Typ.t + +val boolean : t + +val char : t [@@warning "-32"] + +val double : t + +val float : t + +val int : t + +val long : t + +val uint : t + +val void : t + +val void_star : t +(** [void*] type *) + +module Name : sig + type t = Typ.Name.t + + module Java : sig + val java_io_serializable : t + + val java_lang_class : t + + val java_lang_cloneable : t + + val java_lang_object : t + + val java_lang_string : t + end + + module Objc : sig + val ns_enumerator : t + end +end + +module Java : sig + val byte : t + + val char : t + + val short : t + + val pointer_to_java_lang_class : t + + val pointer_to_java_lang_object : t + + val pointer_to_java_lang_string : t +end + +module Objc : sig + val pointer_to_nszone : t +end diff --git a/infer/src/IR/Subtype.ml b/infer/src/IR/Subtype.ml index 502e9602c..e8abe9a4f 100644 --- a/infer/src/IR/Subtype.ml +++ b/infer/src/IR/Subtype.ml @@ -45,7 +45,7 @@ let is_interface tenv (class_name : Typ.Name.t) = let is_root_class class_name = match class_name with | Typ.JavaClass _ -> - Typ.Name.equal class_name Typ.Name.Java.java_lang_object + Typ.Name.equal class_name StdTyp.Name.Java.java_lang_object | _ -> false diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 1e353d9a5..582825744 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -261,30 +261,6 @@ let mk_struct name = mk (Tstruct name) let mk_ptr ?(ptr_kind = Pk_pointer) t = mk (Tptr (t, ptr_kind)) -let void = mk Tvoid - -let void_star = mk (Tptr (void, Pk_pointer)) - -let java_char = mk (Tint IUShort) - -let java_byte = mk (Tint ISChar) - -let java_short = mk (Tint IShort) - -let boolean = mk (Tint IBool) - -let char = mk (Tint IChar) - -let float = mk (Tfloat FFloat) - -let double = mk (Tfloat FDouble) - -let int = mk (Tint IInt) - -let uint = mk (Tint IUInt) - -let long = mk (Tint ILong) - let get_ikind_opt {desc} = match desc with Tint ikind -> Some ikind | _ -> None (* TODO: size_t should be implementation-dependent. *) @@ -447,16 +423,6 @@ module Name = struct let is_class = function JavaClass _ -> true | _ -> false - let java_io_serializable = from_string "java.io.Serializable" - - let java_lang_class = from_string "java.lang.Class" - - let java_lang_cloneable = from_string "java.lang.Cloneable" - - let java_lang_object = from_string "java.lang.Object" - - let java_lang_string = from_string "java.lang.String" - let get_java_class_name_opt typename = match typename with JavaClass java_class_name -> Some java_class_name | _ -> None @@ -518,9 +484,6 @@ module Name = struct |> QualifiedCppName.Set.of_list in function ObjcClass name -> not (QualifiedCppName.Set.mem name tagged_classes) | _ -> false - - - let objc_ns_enumerator = from_string "NSEnumerator" end module Set = PrettyPrintable.MakePPSet (struct @@ -626,8 +589,6 @@ let has_block_prefix s = false -type typ = t - let rec pp_java ~verbose f {desc} = let string_of_int = function | IInt -> @@ -695,12 +656,6 @@ let rec is_java_type t = false -let pointer_to_java_lang_object = mk_ptr (mk_struct Name.Java.java_lang_object) - -let pointer_to_java_lang_string = mk_ptr (mk_struct Name.Java.java_lang_string) - -let pointer_to_objc_nszone = mk_ptr (mk_struct (CStruct (QualifiedCppName.of_qual_string "NSZone"))) - module TypeQualsNormalizer = HashNormalizer.Make (struct type t = type_quals [@@deriving equal] diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index c4b8eeeba..18f992fcb 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -136,40 +136,6 @@ val mk_struct : name -> t val mk_ptr : ?ptr_kind:ptr_kind -> t -> t (** make a pointer to [t], default kind is [Pk_pointer] *) -val void : t -(** void type *) - -val java_char : t - -val java_byte : t - -val java_short : t - -val boolean : t - -val char : t [@@warning "-32"] - -val int : t -(** signed int type *) - -val uint : t -(** unsigned int type *) - -val long : t - -val float : t - -val double : t - -val void_star : t -(** void* type *) - -val pointer_to_java_lang_object : t - -val pointer_to_java_lang_string : t - -val pointer_to_objc_nszone : t - val get_ikind_opt : t -> ikind option (** Get ikind if the type is integer. *) @@ -241,16 +207,6 @@ module Name : sig val is_anonymous_inner_class_name_opt : t -> bool option (** return None if it is not a Java class *) - - val java_lang_object : t - - val java_io_serializable : t - - val java_lang_cloneable : t - - val java_lang_class : t - - val java_lang_string : t end module Cpp : sig @@ -268,8 +224,6 @@ module Name : sig val from_qual_name : QualifiedCppName.t -> t val protocol_from_qual_name : QualifiedCppName.t -> t - - val objc_ns_enumerator : t end module Set : PrettyPrintable.PPSet with type elt = t @@ -356,6 +310,4 @@ val has_block_prefix : string -> bool val unsome : string -> t option -> t -type typ = t - module Normalizer : HashNormalizer.S with type t = t diff --git a/infer/src/absint/HilExp.ml b/infer/src/absint/HilExp.ml index 049d99656..55f1b91cb 100644 --- a/infer/src/absint/HilExp.ml +++ b/infer/src/absint/HilExp.ml @@ -405,8 +405,7 @@ let rec get_typ tenv = function | Constant (Cfloat _) -> Some (Typ.mk (Typ.Tfloat Typ.FFloat)) | Constant (Cclass _) -> - let typ = Typ.(mk (Tstruct Name.Java.java_lang_class)) in - Some Typ.(mk (Tptr (typ, Pk_pointer))) + Some StdTyp.Java.pointer_to_java_lang_class | Constant (Cstr _) -> (* TODO: this will need to behave differently depending on whether we're in C++ or Java *) None @@ -470,7 +469,7 @@ and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp0 typ of_exp_ root_exp root_exp_typ add_field_access_expr acc | Exp.Lindex (root_exp, index_exp) -> let index = - let index_typ = (* TODO: bogus *) Typ.void in + let index_typ = (* TODO: bogus *) StdTyp.void in array_index_of_exp ~include_array_indexes ~f_resolve_id ~add_deref index_exp index_typ in let add_array_access_expr access_expr = @@ -698,6 +697,6 @@ let access_expr_of_exp ~include_array_indexes ~f_resolve_id exp typ = let dummy_base_var = Var.of_id (Ident.create_normal (Ident.string_to_name (IntLit.to_string i)) 0) in - Some (AccessExpression.base (dummy_base_var, Typ.void_star)) + Some (AccessExpression.base (dummy_base_var, StdTyp.void_star)) | _ -> None diff --git a/infer/src/absint/HilInstr.ml b/infer/src/absint/HilInstr.ml index b14a20ca5..a13eee413 100644 --- a/infer/src/absint/HilInstr.ml +++ b/infer/src/absint/HilInstr.ml @@ -85,7 +85,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = | Call ((ret_id, ret_typ), call_exp, formals, loc, call_flags) -> let hil_ret = (Var.of_id ret_id, ret_typ) in let hil_call = - match exp_of_sil call_exp Typ.void with + match exp_of_sil call_exp StdTyp.void with | Constant (Cfun procname) | Closure (procname, _) -> Direct procname | call_exp -> diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index d6da320ee..563226aed 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -49,7 +49,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) "dump" all of the temporaries out of the id map, then execute the unlock instruction. *) let actual_state' = Bindings.fold bindings ~init:actual_state ~f:(fun id access_expr astate_acc -> - let lhs_access_path = HilExp.AccessExpression.base (id, Typ.void) in + let lhs_access_path = HilExp.AccessExpression.base (id, StdTyp.void) in let dummy_assign = HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc) in diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 475b35877..d4727be7c 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -286,7 +286,7 @@ module Java = struct let is_override_of_lang_object_equals curr_pname = let is_only_param_of_object_type = function | [Procname.Parameter.JavaParameter param_type] - when Typ.equal param_type Typ.pointer_to_java_lang_object -> + when Typ.equal param_type StdTyp.Java.pointer_to_java_lang_object -> true | _ -> false diff --git a/infer/src/absint/SubtypingCheck.ml b/infer/src/absint/SubtypingCheck.ml index 399449e74..136c061c3 100644 --- a/infer/src/absint/SubtypingCheck.ml +++ b/infer/src/absint/SubtypingCheck.ml @@ -43,9 +43,9 @@ let rec check_subtype_java tenv (t1 : Typ.t) (t2 : Typ.t) = | Tptr (dom_type1, _), Tptr (dom_type2, _) -> check_subtype_java tenv dom_type1 dom_type2 | Tarray _, Tstruct (JavaClass _ as cn2) -> - Typ.Name.equal cn2 Typ.Name.Java.java_io_serializable - || Typ.Name.equal cn2 Typ.Name.Java.java_lang_cloneable - || Typ.Name.equal cn2 Typ.Name.Java.java_lang_object + Typ.Name.equal cn2 StdTyp.Name.Java.java_io_serializable + || Typ.Name.equal cn2 StdTyp.Name.Java.java_lang_cloneable + || Typ.Name.equal cn2 StdTyp.Name.Java.java_lang_object | _ -> check_subtype_basic_type t1 t2 @@ -66,9 +66,9 @@ let rec case_analysis_type tenv ((t1 : Typ.t), st1) ((t2 : Typ.t), st2) = | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> Subtype.case_analysis tenv (cn1, st1) (cn2, st2) | Tstruct (JavaClass _ as cn1), Tarray _ - when ( Typ.Name.equal cn1 Typ.Name.Java.java_io_serializable - || Typ.Name.equal cn1 Typ.Name.Java.java_lang_cloneable - || Typ.Name.equal cn1 Typ.Name.Java.java_lang_object ) + when ( Typ.Name.equal cn1 StdTyp.Name.Java.java_io_serializable + || Typ.Name.equal cn1 StdTyp.Name.Java.java_lang_cloneable + || Typ.Name.equal cn1 StdTyp.Name.Java.java_lang_object ) && not (Subtype.equal st1 Subtype.exact) -> (Some st1, None) | Tstruct cn1, Tstruct cn2 diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 2932fa9bd..909e184bf 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -107,7 +107,7 @@ module ReplaceObjCCopy = struct (Sil.Call ( ret_id_typ , function_exp - , params @ [(Exp.null, Typ.pointer_to_objc_nszone)] + , params @ [(Exp.null, StdTyp.Objc.pointer_to_nszone)] , loc , flags )) ) else None diff --git a/infer/src/biabduction/Absarray.ml b/infer/src/biabduction/Absarray.ml index c5d231bc0..0d993fc5a 100644 --- a/infer/src/biabduction/Absarray.ml +++ b/infer/src/biabduction/Absarray.ml @@ -616,7 +616,7 @@ let check_after_array_abstraction tenv prop = () | Predicates.Earray (_, esel, _) -> (* check that no more than 2 elements are in the array *) - let typ_elem = Typ.array_elem (Some Typ.void) typ in + let typ_elem = Typ.array_elem (Some StdTyp.void) typ in if List.length esel > 2 && array_typ_can_abstract typ then if List.for_all ~f:(check_index root offs) esel then () else report_error prop else @@ -626,13 +626,13 @@ let check_after_array_abstraction tenv prop = | Predicates.Estruct (fsel, _) -> List.iter ~f:(fun (f, se) -> - let typ_f = Struct.fld_typ ~lookup ~default:Typ.void f typ in + let typ_f = Struct.fld_typ ~lookup ~default:StdTyp.void f typ in check_se root (offs @ [Predicates.Off_fld (f, typ)]) typ_f se ) fsel in let check_hpred = function | Predicates.Hpointsto (root, se, texp) -> - let typ = Exp.texp_to_typ (Some Typ.void) texp in + let typ = Exp.texp_to_typ (Some StdTyp.void) texp in check_se root [] typ se | Predicates.Hlseg _ | Predicates.Hdllseg _ -> () diff --git a/infer/src/biabduction/Attribute.ml b/infer/src/biabduction/Attribute.ml index 851020e07..c7b3c1735 100644 --- a/infer/src/biabduction/Attribute.ml +++ b/infer/src/biabduction/Attribute.ml @@ -365,7 +365,7 @@ let find_equal_formal_path tenv e prop = | Predicates.Eexp (exp2, _) when Exp.equal exp2 e -> ( match find_in_sigma exp1 seen_hpreds with | Some vfs -> - Some (Exp.Lfield (vfs, field, Typ.void)) + Some (Exp.Lfield (vfs, field, StdTyp.void)) | None -> None ) | _ -> diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 246a52e11..4f450b0da 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -609,8 +609,8 @@ let execute___cxx_typeid ({Builtin.analysis_data; prop_; args; loc} as r) : Buil let set_instr = Sil.Store { e1= field_exp - ; root_typ= Typ.void - ; typ= Typ.void + ; root_typ= StdTyp.void + ; typ= StdTyp.void ; e2= Exp.Const (Const.Cstr typ_string) ; loc } in @@ -752,8 +752,8 @@ let execute___infer_fail {Builtin.analysis_data= {tenv} as analysis_data; prop_; let set_instr = Sil.Store { e1= Exp.Lvar Predicates.custom_error - ; root_typ= Typ.void - ; typ= Typ.void + ; root_typ= StdTyp.void + ; typ= StdTyp.void ; e2= Exp.Const (Const.Cstr error_str) ; loc } in @@ -772,8 +772,8 @@ let execute___assert_fail {Builtin.analysis_data; prop_; path; args; loc} : Buil let set_instr = Sil.Store { e1= Exp.Lvar Predicates.custom_error - ; root_typ= Typ.void - ; typ= Typ.void + ; root_typ= StdTyp.void + ; typ= StdTyp.void ; e2= Exp.Const (Const.Cstr error_str) ; loc } in @@ -786,7 +786,11 @@ let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt {Builtin.analysis_da let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in let sizeof_typ = Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in let alloc_fun_exp = - match alloc_fun_opt with Some pname -> [(Exp.Const (Const.Cfun pname), Typ.void)] | None -> [] + match alloc_fun_opt with + | Some pname -> + [(Exp.Const (Const.Cfun pname), StdTyp.void)] + | None -> + [] in let alloc_instr = Sil.Call (ret_id_typ, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index ed9955b23..90768b971 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -1565,7 +1565,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : | (f1, se1) :: fsel1', (f2, se2) :: fsel2' -> ( match Fieldname.compare f1 f2 with | 0 -> - let typ' = Struct.fld_typ ~lookup ~default:Typ.void f2 typ2 in + let typ' = Struct.fld_typ ~lookup ~default:StdTyp.void f2 typ2 in let subs', se_frame, se_missing = sexp_imply tenv (Exp.Lfield (source, f2, typ2)) false calc_missing subs se1 se2 typ' in @@ -1585,7 +1585,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : in (subs', (f1, se1) :: fld_frame, fld_missing) | _ -> - let typ' = Struct.fld_typ ~lookup ~default:Typ.void f2 typ2 in + let typ' = Struct.fld_typ ~lookup ~default:StdTyp.void f2 typ2 in let subs' = sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in @@ -1595,7 +1595,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : let fld_missing' = (f2, se2) :: fld_missing in (subs', fld_frame, fld_missing') ) | [], (f2, se2) :: fsel2' -> - let typ' = Struct.fld_typ ~lookup ~default:Typ.void f2 typ2 in + let typ' = Struct.fld_typ ~lookup ~default:StdTyp.void f2 typ2 in let subs' = sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in @@ -1607,7 +1607,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2 : subst2 * (Exp.t * Predicates.strexp) list * (Exp.t * Predicates.strexp) list = - let typ_elem = Typ.array_elem (Some Typ.void) typ2 in + let typ_elem = Typ.array_elem (Some StdTyp.void) typ2 in match (esel1, esel2) with | _, [] -> (subs, esel1, []) @@ -1971,7 +1971,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 match Prop.prop_iter_current tenv iter1' with | Predicates.Hpointsto (e1, se1, texp1), _ -> ( try - let typ2 = Exp.texp_to_typ (Some Typ.void) texp2 in + let typ2 = Exp.texp_to_typ (Some StdTyp.void) texp2 in let typing_frame, typing_missing = texp_imply tenv subs texp1 texp2 e1 calc_missing in let se1' = sexp_imply_preprocess se1 texp1 se2 in let subs', fld_frame, fld_missing = @@ -2214,7 +2214,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * , Predicates.inst_none ) | Java -> let mk_fld_sexp field_name = - let fld = Fieldname.make Typ.Name.Java.java_lang_string field_name in + let fld = Fieldname.make StdTyp.Name.Java.java_lang_string field_name in let se = Predicates.Eexp (Exp.Var (Ident.create_fresh Ident.kprimed), Predicates.Inone) in @@ -2232,7 +2232,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * ; dynamic_length= None ; subtype= Subtype.exact } | Java -> - let object_type = Typ.Name.Java.java_lang_string in + let object_type = StdTyp.Name.Java.java_lang_string in Exp.Sizeof { typ= Typ.mk (Tstruct object_type) ; nbytes= None @@ -2247,12 +2247,12 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * let sexp = (* TODO: add appropriate fields *) Predicates.Estruct - ( [ ( Fieldname.make Typ.Name.Java.java_lang_class "name" + ( [ ( Fieldname.make StdTyp.Name.Java.java_lang_class "name" , Predicates.Eexp (Exp.Const (Const.Cstr s), Predicates.Inone) ) ] , Predicates.inst_none ) in let class_texp = - let class_type = Typ.Name.Java.java_lang_class in + let class_type = StdTyp.Name.Java.java_lang_class in Exp.Sizeof { typ= Typ.mk (Tstruct class_type) ; nbytes= None @@ -2301,7 +2301,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * let subs' = match hpred2' with | Predicates.Hpointsto (e2, se2, te2) -> - let typ2 = Exp.texp_to_typ (Some Typ.void) te2 in + let typ2 = Exp.texp_to_typ (Some StdTyp.void) te2 in sexp_imply_nolhs tenv e2 calc_missing subs se2 typ2 | _ -> subs diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 5b4a32972..b873c4763 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -438,7 +438,7 @@ let strexp_extend_values analysis_data pname tenv orig_prop footprint_part kind | Exp.Sizeof sizeof_data -> sizeof_data | _ -> - {Exp.typ= Typ.void; nbytes= None; dynamic_length= None; subtype= Subtype.exact} + {Exp.typ= StdTyp.void; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in List.map ~f:(fun (atoms', se', typ') -> diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index cb8acd014..d712bf551 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -626,7 +626,8 @@ let call_constructor_url_update_args = Procname.make_java ~class_name:(Typ.Name.Java.from_string "java.net.URL") ~return_type:None ~method_name:Procname.Java.constructor_method_name - ~parameters:[Typ.pointer_to_java_lang_string] ~kind:Procname.Java.Non_Static () + ~parameters:[StdTyp.Java.pointer_to_java_lang_string] + ~kind:Procname.Java.Non_Static () in fun pname actual_params -> if Procname.equal url_pname pname then diff --git a/infer/src/bufferoverrun/absLoc.mli b/infer/src/bufferoverrun/absLoc.mli index a750ddd3a..061ee9aff 100644 --- a/infer/src/bufferoverrun/absLoc.mli +++ b/infer/src/bufferoverrun/absLoc.mli @@ -98,7 +98,7 @@ module Loc : sig val is_objc_collection_internal_array : t -> bool - val append_field : ?typ:Typ.typ -> t -> Fieldname.t -> t + val append_field : ?typ:Typ.t -> t -> Fieldname.t -> t (** It appends field. [typ] is the type of [fn]. *) end @@ -133,7 +133,7 @@ module PowLoc : sig val fold : (Loc.t -> 'a -> 'a) -> t -> 'a -> 'a - val cast : Typ.typ -> t -> t + val cast : Typ.t -> t -> t val of_c_strlen : t -> t (** It appends the [strlen] field. *) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 2433977a9..b9406be04 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -564,7 +564,7 @@ module Val = struct | Tptr ({desc= Tfun}, _) -> of_func_ptrs (FuncPtr.Set.of_path path) | Tptr ({desc= Tstruct name}, _) - when PatternMatch.is_subtype tenv name Typ.Name.Objc.objc_ns_enumerator -> + when PatternMatch.is_subtype tenv name StdTyp.Name.Objc.ns_enumerator -> (* NOTE: It generates a value of NSEnumerator specifically. Especially, it assigns zero to the offset, rather than a symbol, to avoid precision loss by limited handling of symbolic values in the domain. Although this is an unsound design choice, we expect it should not diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index 4a9441228..7f35a0211 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -29,24 +29,24 @@ let mk, get_type = (mk, get_type) -let java_collection_internal_array = mk "java.collection.elements" Typ.(mk_array void) +let java_collection_internal_array = mk "java.collection.elements" Typ.(mk_array StdTyp.void) -let java_linked_list_index = mk "java.linked_list_index" Typ.(int) +let java_linked_list_index = mk "java.linked_list_index" StdTyp.(int) -let java_linked_list_length = mk "java.linked_list_length" Typ.(int) +let java_linked_list_length = mk "java.linked_list_length" StdTyp.(int) let java_linked_list_next typ = mk "java.linked_list_next" typ -let java_list_files_length = mk "java.list_files_length" Typ.(int) +let java_list_files_length = mk "java.list_files_length" StdTyp.(int) let is_java_collection_internal_array fn = Fieldname.equal fn java_collection_internal_array -let objc_collection_internal_array = mk "nscollection.elements" Typ.(mk_array void) +let objc_collection_internal_array = mk "nscollection.elements" Typ.(mk_array StdTyp.void) -let objc_iterator_offset = mk "nsiterator.offset" Typ.(mk_array void) +let objc_iterator_offset = mk "nsiterator.offset" Typ.(mk_array StdTyp.void) let c_strlen () = - if Language.curr_language_is Java then mk "length" Typ.uint else mk "c.strlen" Typ.uint + if Language.curr_language_is Java then mk "length" StdTyp.uint else mk "c.strlen" StdTyp.uint let cpp_vector_elem_str = "cpp.vector_elem" diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index bee30f070..43e71ea1a 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -39,13 +39,13 @@ let mk pdesc = | Tarray {elt} -> Some elt | Tvoid -> - Some Typ.void + Some StdTyp.void | Tstruct typename -> ( match BufferOverrunTypModels.dispatch tenv typename with | Some (CArray {element_typ}) -> Some element_typ | Some CppStdVector -> - Some (Typ.mk (Typ.Tptr (Typ.void, Typ.Pk_pointer))) + Some (Typ.mk (Typ.Tptr (StdTyp.void, Typ.Pk_pointer))) | Some JavaCollection -> (* Current Java frontend does give element types of Java collection. *) None @@ -62,7 +62,7 @@ let mk pdesc = match BoField.get_type fn with | None -> let lookup = Tenv.lookup tenv in - Option.map (typ_of_param_path x) ~f:(Struct.fld_typ ~lookup ~default:Typ.void fn) + Option.map (typ_of_param_path x) ~f:(Struct.fld_typ ~lookup ~default:StdTyp.void fn) | some_typ -> some_typ ) | BoField.StarField {last_field} -> diff --git a/infer/src/clang/CAddImplicitDeallocImpl.ml b/infer/src/clang/CAddImplicitDeallocImpl.ml index b64b6630e..6573a3274 100644 --- a/infer/src/clang/CAddImplicitDeallocImpl.ml +++ b/infer/src/clang/CAddImplicitDeallocImpl.ml @@ -24,7 +24,7 @@ let get_dealloc_call_field (self_var, self_typ) location instrs (fieldname, fiel let ret_id = Ident.create_fresh Ident.knormal in let call_instr = Sil.Call - ( (ret_id, Typ.void) + ( (ret_id, StdTyp.void) , Const (Cfun field_class_dealloc_name) , [(Var id_field, field_typ)] , location diff --git a/infer/src/clang/CType_decl.ml b/infer/src/clang/CType_decl.ml index 384aa7e5c..e973031f1 100644 --- a/infer/src/clang/CType_decl.ml +++ b/infer/src/clang/CType_decl.ml @@ -151,7 +151,7 @@ module BuildMethodSignature = struct let return_typ_annot = CAst_utils.sil_annot_of_type return_qual_type in let is_objc_method = CMethodProperties.is_objc_method method_decl in if should_add_return_param return_typ ~is_objc_method then - (Typ.void, Some (CType.add_pointer_to_typ return_typ), Annot.Item.empty, true) + (StdTyp.void, Some (CType.add_pointer_to_typ return_typ), Annot.Item.empty, true) else (return_typ, None, return_typ_annot, false) diff --git a/infer/src/clang/CType_decl.mli b/infer/src/clang/CType_decl.mli index e1de737cc..90d548448 100644 --- a/infer/src/clang/CType_decl.mli +++ b/infer/src/clang/CType_decl.mli @@ -67,7 +67,7 @@ val method_signature_body_of_decl : * Clang_ast_t.stmt option * [> `CXXConstructorInit of Clang_ast_t.cxx_ctor_initializer] list -val should_add_return_param : Typ.typ -> is_objc_method:bool -> bool +val should_add_return_param : Typ.t -> is_objc_method:bool -> bool val type_of_captured_var : - Tenv.t -> is_block_inside_objc_class_method:bool -> Clang_ast_t.decl_ref -> Typ.typ option + Tenv.t -> is_block_inside_objc_class_method:bool -> Clang_ast_t.decl_ref -> Typ.t option diff --git a/infer/src/clang/cField_decl.ml b/infer/src/clang/cField_decl.ml index d12e25b45..48c5c55da 100644 --- a/infer/src/clang/cField_decl.ml +++ b/infer/src/clang/cField_decl.ml @@ -115,7 +115,7 @@ let add_missing_fields tenv class_name missing_fields = let modelled_fields_in_classes = - [ ("NSData", "_bytes", Typ.mk (Tptr (Typ.void, Typ.Pk_pointer))) + [ ("NSData", "_bytes", Typ.mk (Tptr (StdTyp.void, Typ.Pk_pointer))) ; ("NSArray", "elementData", Typ.mk (Tint Typ.IInt)) ] diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index 53ccac391..9563f0cd5 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -435,7 +435,7 @@ module CFrontend_decl_funct (T : CModule_type.CTranslation) : CModule_type.CFron ~set_objc_accessor_attr:false then ( let ms = - CMethodSignature.mk procname None [] (Typ.void, Annot.Item.empty) [] + CMethodSignature.mk procname None [] (StdTyp.void, Annot.Item.empty) [] decl_info.Clang_ast_t.di_source_range ClangMethodKind.C_FUNCTION None None None `None in diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 2dd3a56c1..906a04cbf 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -311,7 +311,7 @@ let create_external_procdesc trans_unit_ctx cfg proc_name clang_method_kind type | Some (ret_type, arg_types) -> (ret_type, List.map ~f:(fun typ -> (Mangled.from_string "x", typ)) arg_types) | None -> - (Typ.void, []) + (StdTyp.void, []) in let proc_attributes = { (ProcAttributes.default trans_unit_ctx.CFrontend_config.source_file proc_name) with diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 5eddb7f41..35c9b7a9c 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -758,7 +758,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let ret_id = Ident.create_fresh Ident.knormal in let call_instr = Sil.Call - ( (ret_id, Typ.void) + ( (ret_id, StdTyp.void) , Const (Cfun BuiltinDecl.zero_initialization) , [exp_typ] , sil_loc @@ -1240,7 +1240,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s decl_ref_trans ~context:(MemberOrIvar this_res_trans) trans_state si decl_ref in let res_trans = - cxx_method_construct_call_trans trans_state_pri res_trans_callee params_stmt si Typ.void + cxx_method_construct_call_trans trans_state_pri res_trans_callee params_stmt si StdTyp.void ~is_injected_destructor:false ~is_cpp_call_virtual:false (Some tmp_res_trans) ~is_inherited_ctor in @@ -1263,7 +1263,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s | Some res_trans_callee when Option.is_some res_trans_callee.method_name -> let is_cpp_call_virtual = res_trans_callee.is_cpp_call_virtual in Some - (cxx_method_construct_call_trans trans_state_pri res_trans_callee [] si' Typ.void + (cxx_method_construct_call_trans trans_state_pri res_trans_callee [] si' StdTyp.void ~is_injected_destructor ~is_cpp_call_virtual None ~is_inherited_ctor:false) | _ -> None @@ -2913,7 +2913,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s | Typ.{desc= Tptr (t, _)} -> Typ.mk_array ~length ~stride:(IntLit.of_int 8) t | _ -> - Typ.void_star + StdTyp.void_star in (Exp.Lvar temp, array_typ) in @@ -2938,7 +2938,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let res_trans_call = let method_type_no_ref = CType_decl.get_type_from_expr_info expr_info tenv in let method_type = add_reference_if_glvalue method_type_no_ref expr_info in - let actuals = [temp_with_typ; (Exp.Const (Cint length), Typ.int)] in + let actuals = [temp_with_typ; (Exp.Const (Cint length), StdTyp.int)] in let callee_name, method_call_type = let typ = CAst_utils.qual_type_of_decl_ptr @@ -3016,7 +3016,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s | Typ.{desc= Tptr (t, _)} -> Typ.mk_array ~length ~stride:(IntLit.of_int 8) t | _ -> - Typ.void_star + StdTyp.void_star in (Exp.Lvar temp, array_typ) in @@ -3057,7 +3057,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let actuals = [ temp1_with_typ ; temp2_with_typ - ; (Exp.Const (Cint (IntLit.div length (IntLit.of_int 2))), Typ.int) ] + ; (Exp.Const (Cint (IntLit.div length (IntLit.of_int 2))), StdTyp.int) ] in let callee_name, method_call_type = let typ = @@ -3496,7 +3496,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let stmt = match stmts with [stmt] -> stmt | _ -> assert false in let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in let exp = res_trans_stmt.return in - let args = [exp; (sizeof_expr, Typ.void)] in + let args = [exp; (sizeof_expr, StdTyp.void)] in let ret_id = Ident.create_fresh Ident.knormal in let call = Sil.Call ((ret_id, cast_type), builtin, args, sil_loc, CallFlags.default) in let res_ex = Exp.Var ret_id in @@ -3539,7 +3539,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s and gccAsmStmt_trans trans_state stmt_info stmts = call_function_with_args Procdesc.Node.GCCAsmStmt BuiltinDecl.__infer_skip_gcc_asm_stmt - trans_state stmt_info Typ.void stmts + trans_state stmt_info StdTyp.void stmts and offsetOf_trans trans_state expr_info offset_of_expr_info stmt_info = @@ -3557,17 +3557,17 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s and genericSelectionExprUnknown_trans trans_state stmt_info stmts = call_function_with_args Procdesc.Node.GenericSelectionExpr - BuiltinDecl.__infer_generic_selection_expr trans_state stmt_info Typ.void stmts + BuiltinDecl.__infer_generic_selection_expr trans_state stmt_info StdTyp.void stmts and objc_cxx_throw_trans trans_state stmt_info stmts = call_function_with_args Procdesc.Node.ObjCCPPThrow BuiltinDecl.objc_cpp_throw trans_state - stmt_info Typ.void stmts + stmt_info StdTyp.void stmts and cxxPseudoDestructorExpr_trans () = mk_trans_result - (Exp.Const (Const.Cfun BuiltinDecl.__infer_skip_function), Typ.void) + (Exp.Const (Const.Cfun BuiltinDecl.__infer_skip_function), StdTyp.void) empty_control @@ -3590,7 +3590,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let fun_name = BuiltinDecl.__cxx_typeid in let sil_fun = Exp.Const (Const.Cfun fun_name) in let ret_id = Ident.create_fresh Ident.knormal in - let void_typ = Typ.void in + let void_typ = StdTyp.void in let type_info_objc = (Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact}, void_typ) in @@ -4042,7 +4042,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s | None -> genericSelectionExprUnknown_trans trans_state stmt_info stmts ) | SizeOfPackExpr _ -> - mk_trans_result (Exp.get_undefined false, Typ.void) empty_control + mk_trans_result (Exp.get_undefined false, StdTyp.void) empty_control | GCCAsmStmt (stmt_info, stmts) -> gccAsmStmt_trans trans_state stmt_info stmts | CXXPseudoDestructorExpr _ -> @@ -4187,7 +4187,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s ((stmt_info, stmts), ret_typ) | None -> let stmt_tuple = Clang_ast_proj.get_stmt_tuple instr in - (stmt_tuple, Typ.void) + (stmt_tuple, StdTyp.void) in skip_unimplemented ~reason: diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 4a11cd90e..a67a2921f 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -395,7 +395,7 @@ let create_call_to_objc_bridge_transfer sil_loc exp typ = let pname = BuiltinDecl.__objc_bridge_transfer in let stmt_call = Sil.Call - ( (Ident.create_fresh Ident.knormal, Typ.void) + ( (Ident.create_fresh Ident.knormal, StdTyp.void) , Exp.Const (Const.Cfun pname) , [(exp, typ)] , sil_loc @@ -479,9 +479,9 @@ let cast_operation ?objc_bridge_cast_kind cast_kind ((exp, typ) as exp_typ) cast let trans_assertion_failure sil_loc (context : CContext.t) = let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in - let args = [(Exp.Const (Const.Cstr Config.default_failure_name), Typ.void)] in + let args = [(Exp.Const (Const.Cstr Config.default_failure_name), StdTyp.void)] in let ret_id = Ident.create_fresh Ident.knormal in - let ret_typ = Typ.void in + let ret_typ = StdTyp.void in let call_instr = Sil.Call ((ret_id, ret_typ), assert_fail_builtin, args, sil_loc, CallFlags.default) in @@ -625,12 +625,12 @@ let is_logical_negation_of_int tenv ei uoi = false -let mk_fresh_void_exp_typ () = (Exp.Var (Ident.create_fresh Ident.knormal), Typ.void) +let mk_fresh_void_exp_typ () = (Exp.Var (Ident.create_fresh Ident.knormal), StdTyp.void) -let mk_fresh_void_id_typ () = (Ident.create_fresh Ident.knormal, Typ.void) +let mk_fresh_void_id_typ () = (Ident.create_fresh Ident.knormal, StdTyp.void) let mk_fresh_void_return () = - let id = Ident.create_fresh Ident.knormal and void = Typ.void in + let id = Ident.create_fresh Ident.knormal and void = StdTyp.void in ((id, void), (Exp.Var id, void)) diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 2283185e2..c11897c85 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -59,7 +59,7 @@ val empty_control : control val mk_trans_result : ?method_name:BuiltinDecl.t -> ?is_cpp_call_virtual:bool - -> Exp.t * Typ.typ + -> Exp.t * Typ.t -> control -> trans_result @@ -129,12 +129,7 @@ val new_or_alloc_trans : -> trans_result val cpp_new_trans : - Typ.IntegerWidths.t - -> Location.t - -> Typ.t - -> Exp.t option - -> (Exp.t * Typ.typ) list - -> trans_result + Typ.IntegerWidths.t -> Location.t -> Typ.t -> Exp.t option -> (Exp.t * Typ.t) list -> trans_result (** Module for creating cfg nodes and other utility functions related to them. *) module Nodes : sig diff --git a/infer/src/clang/cVar_decl.mli b/infer/src/clang/cVar_decl.mli index 46e4509d2..bdf7ce663 100644 --- a/infer/src/clang/cVar_decl.mli +++ b/infer/src/clang/cVar_decl.mli @@ -23,7 +23,7 @@ val sil_var_of_captured_var : -> Clang_ast_t.source_range -> Procname.t -> Clang_ast_t.decl_ref - -> (Pvar.t * Typ.typ) option + -> (Pvar.t * Typ.t) option val captured_vars_from_block_info : CContext.t diff --git a/infer/src/concurrency/AbstractAddress.ml b/infer/src/concurrency/AbstractAddress.ml index aa9a5ca42..82de87df5 100644 --- a/infer/src/concurrency/AbstractAddress.ml +++ b/infer/src/concurrency/AbstractAddress.ml @@ -100,11 +100,11 @@ type t = (** method parameter represented by its 0-indexed position, root var is not used in comparison *) [@@deriving compare, equal] -let get_typ tenv = - let class_type = Typ.(mk (Tstruct Name.Java.java_lang_class)) in - let some_ptr_to_class_type = Some Typ.(mk (Tptr (class_type, Pk_pointer))) in - function - | Class _ -> some_ptr_to_class_type | Global {path} | Parameter {path} -> get_typ tenv path +let get_typ tenv = function + | Class _ -> + Some StdTyp.Java.pointer_to_java_lang_class + | Global {path} | Parameter {path} -> + get_typ tenv path let append ~on_to:(base, accesses) (_, accesses') = diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index a0cb8a206..66b1492b8 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/infer/src/concurrency/StarvationModels.ml @@ -402,7 +402,9 @@ let is_assume_true = let is_java_main_method (pname : Procname.t) = - let pointer_to_array_of_java_lang_string = Typ.(mk_ptr (mk_array pointer_to_java_lang_string)) in + let pointer_to_array_of_java_lang_string = + Typ.(mk_ptr (mk_array StdTyp.Java.pointer_to_java_lang_string)) + in let check_main_args args = match args with [arg] -> Typ.equal pointer_to_array_of_java_lang_string arg | _ -> false in @@ -412,5 +414,5 @@ let is_java_main_method (pname : Procname.t) = | Java java_pname -> Procname.Java.is_static java_pname && String.equal "main" (Procname.get_method pname) - && Typ.equal Typ.void (Procname.Java.get_return_typ java_pname) + && Typ.equal StdTyp.void (Procname.Java.get_return_typ java_pname) && check_main_args (Procname.Java.get_parameters java_pname) diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index c8defc6e6..569529f41 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -265,7 +265,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Metadata metadata -> do_metadata metadata astate | Prune (exp, _loc, _then_branch, _if_kind) -> - let hil_exp = hilexp_of_sil ~add_deref:false astate exp Typ.boolean in + let hil_exp = hilexp_of_sil ~add_deref:false astate exp StdTyp.boolean in do_assume hil_exp astate | Load {id} when Ident.is_none id -> astate diff --git a/infer/src/java/jAnnotation.ml b/infer/src/java/jAnnotation.ml index a2667b311..a13c771a2 100644 --- a/infer/src/java/jAnnotation.ml +++ b/infer/src/java/jAnnotation.ml @@ -11,21 +11,21 @@ open Javalib_pack let translate_basic_type = function | `Bool -> - Typ.boolean + StdTyp.boolean | `Byte -> - Typ.java_byte + StdTyp.Java.byte | `Char -> - Typ.java_char + StdTyp.Java.char | `Double -> - Typ.double + StdTyp.double | `Float -> - Typ.float + StdTyp.float | `Int -> - Typ.int + StdTyp.int | `Long -> - Typ.long + StdTyp.long | `Short -> - Typ.java_short + StdTyp.Java.short let rec translate_value_type = function @@ -56,7 +56,7 @@ let rec translate_value_exn = function | JBasics.EVClass (Some typ) -> Annot.Class (translate_value_type typ) | JBasics.EVClass _ -> - Annot.Class Typ.void + Annot.Class StdTyp.void | JBasics.EVAnnotation ann -> Annot.Annot (translate ann) | _ -> diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index d89d645bf..64eb1e346 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -160,7 +160,7 @@ let translate_locals program tenv formals bytecode jbir_code = Array.fold ~f:(fun accu jbir_var -> let var = Mangled.from_string (JBir.var_name_g jbir_var) in - collect accu (var, Typ.void) ) + collect accu (var, StdTyp.void) ) ~init:with_bytecode_vars (JBir.vars jbir_code) in snd with_jbir_vars @@ -546,7 +546,7 @@ let rec expression (context : JContext.t) pc expr = | _ -> assert false in - let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.void)] in + let args = [(sil_ex, type_of_ex); (sizeof_expr, StdTyp.void)] in let ret_id = Ident.create_fresh Ident.knormal in let call = Sil.Call ((ret_id, Typ.mk (Tint IBool)), builtin, args, loc, CallFlags.default) @@ -702,7 +702,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex let return_type = match JBasics.ms_rtype ms with | None -> - Typ.void + StdTyp.void | Some vt -> JTransType.value_type program tenv vt in @@ -719,7 +719,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex | None -> let call_instr = Sil.Call - ((Ident.create_fresh Ident.knormal, Typ.void), callee_fun, call_args, loc, call_flags) + ((Ident.create_fresh Ident.knormal, StdTyp.void), callee_fun, call_args, loc, call_flags) in instrs @ [call_instr] | Some var -> @@ -757,7 +757,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex let set_file_attr = let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_file_attribute) in Sil.Call - ( (Ident.create_fresh Ident.knormal, Typ.void) + ( (Ident.create_fresh Ident.knormal, StdTyp.void) , set_builtin , [exp] , loc @@ -770,7 +770,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex let set_mem_attr = let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_mem_attribute) in Sil.Call - ( (Ident.create_fresh Ident.knormal, Typ.void) + ( (Ident.create_fresh Ident.knormal, StdTyp.void) , set_builtin , [exp] , loc @@ -840,7 +840,7 @@ let assume_not_null loc sil_expr = let not_null_expr = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in let call_args = [(not_null_expr, Typ.mk (Tint Typ.IBool))] in Sil.Call - ( (Ident.create_fresh Ident.knormal, Typ.void) + ( (Ident.create_fresh Ident.knormal, StdTyp.void) , builtin_infer_assume , call_args , loc @@ -864,7 +864,7 @@ let instruction (context : JContext.t) pc instr : translation = let builtin_const = Exp.Const (Const.Cfun builtin) in let instr = Sil.Call - ( (Ident.create_fresh Ident.knormal, Typ.void) + ( (Ident.create_fresh Ident.knormal, StdTyp.void) , builtin_const , [(sil_expr, sil_type)] , loc diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index d8c6bdba8..0c3f17ea6 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -84,7 +84,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle [ (Exp.Var id_exn_val, Typ.mk (Tptr (exn_type, Typ.Pk_pointer))) ; ( Exp.Sizeof {typ= exn_type; nbytes= None; dynamic_length= None; subtype= Subtype.exact} - , Typ.void ) ] + , StdTyp.void ) ] in Sil.Call ( (id_instanceof, Typ.mk (Tint IBool)) diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 9c10c897a..a63a0bb8b 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -18,38 +18,38 @@ exception Type_tranlsation_error of string (** https://docs.oracle.com/javase/tutorial/java/nutsandbolts/datatypes.html *) let translate_basic_type = function | `Int -> - Typ.int + StdTyp.int | `Bool -> - Typ.boolean + StdTyp.boolean | `Byte -> - Typ.java_byte + StdTyp.Java.byte | `Char -> - Typ.java_char + StdTyp.Java.char | `Double -> - Typ.double + StdTyp.double | `Float -> - Typ.float + StdTyp.float | `Long -> - Typ.long + StdTyp.long | `Short -> - Typ.java_short + StdTyp.Java.short let cast_type = function | JBir.F2I | JBir.L2I | JBir.D2I -> - Typ.int + StdTyp.int | JBir.D2L | JBir.F2L | JBir.I2L -> - Typ.long + StdTyp.long | JBir.I2F | JBir.L2F | JBir.D2F -> - Typ.float + StdTyp.float | JBir.L2D | JBir.F2D | JBir.I2D -> - Typ.double + StdTyp.double | JBir.I2B -> - Typ.boolean + StdTyp.boolean | JBir.I2C -> - Typ.java_char + StdTyp.Java.char | JBir.I2S -> - Typ.java_short + StdTyp.Java.short let typename_of_classname cn = Typ.Name.Java.from_string (JBasics.cn_name cn) @@ -119,7 +119,7 @@ let method_signature_names ms = | None when String.equal method_name JConfig.constructor_name -> None | None -> - Some Typ.void + Some StdTyp.void | Some vt -> Some (get_named_type vt) in @@ -399,4 +399,4 @@ let rec expr_type (context : JContext.t) expr = (** Returns the return type of the method based on the return type specified in ms. *) let return_type program tenv ms = - match JBasics.ms_rtype ms with None -> Typ.void | Some vt -> value_type program tenv vt + match JBasics.ms_rtype ms with None -> StdTyp.void | Some vt -> value_type program tenv vt diff --git a/infer/src/nullsafe/models.ml b/infer/src/nullsafe/models.ml index 62ac731ab..aa227cf35 100644 --- a/infer/src/nullsafe/models.ml +++ b/infer/src/nullsafe/models.ml @@ -45,7 +45,7 @@ let get_special_method_modelled_nullability tenv java_proc_name = Some (false, []) (* valueOf() is a synthetic enum method that is never null *) | "valueOf", [Procname.Parameter.JavaParameter param_type_name] - when Typ.equal param_type_name Typ.pointer_to_java_lang_string -> + when Typ.equal param_type_name StdTyp.Java.pointer_to_java_lang_string -> Some (false, [false]) | _ -> None diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index fc65602a5..6bd821ccd 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -479,7 +479,7 @@ let typecheck_expr_for_errors analysis_data ~nullsafe_mode find_canonical_duplic checks node instr_ref typestate1 exp1 loc1 : unit = ignore (typecheck_expr_simple analysis_data ~nullsafe_mode find_canonical_duplicate calls_this checks - node instr_ref typestate1 exp1 Typ.void TypeOrigin.OptimisticFallback loc1) + node instr_ref typestate1 exp1 StdTyp.void TypeOrigin.OptimisticFallback loc1) (** Get the values of a vararg parameter given the pvar used to assign the elements by looking for @@ -634,7 +634,7 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_ typestate' -let object_typ = Typ.(mk_ptr (mk_struct Name.Java.java_lang_object)) +let object_typ = StdTyp.Java.pointer_to_java_lang_object (* Handle m.put(k,v) as assignment pvar = v for the pvar associated to m.get(k) *) let do_map_put ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as analysis_data) @@ -838,7 +838,9 @@ let rec check_condition_for_sil_prune | Some expr_str -> (* Add pvar representing call to `get` to a typestate, indicating that it is a non-nullable *) let pvar = Pvar.mk (Mangled.from_string expr_str) curr_pname in - let range = (Typ.void, InferredNullability.create TypeOrigin.CallToGetKnownToContainsKey) in + let range = + (StdTyp.void, InferredNullability.create TypeOrigin.CallToGetKnownToContainsKey) + in let typestate_with_new_pvar = TypeState.add pvar range typestate in typestate_with_new_pvar ~descr:"modelling result of Map.get() since containsKey() returned true" @@ -881,8 +883,8 @@ let rec check_condition_for_sil_prune *) let typ, inferred_nullability = typecheck_expr_simple analysis_data ~nullsafe_mode find_canonical_duplicate calls_this - checks original_node instr_ref typestate pvar_expr Typ.void TypeOrigin.OptimisticFallback - loc + checks original_node instr_ref typestate pvar_expr StdTyp.void + TypeOrigin.OptimisticFallback loc in if checks.eradicate then EradicateChecks.check_condition_for_redundancy analysis_data ~is_always_true:true_branch diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 7c3200d17..98e13a53b 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -188,7 +188,7 @@ module PulseTransferFunctions = struct let used_ids = Stack.keys astate |> List.filter_map ~f:(fun var -> Var.get_ident var) in Ident.update_name_generator used_ids ; let call_dealloc (astate_list : Domain.t list) (ret_id, id, typ, dealloc) = - let ret = (ret_id, Typ.void) in + let ret = (ret_id, StdTyp.void) in let call_flags = CallFlags.default in let call_exp = Exp.Const (Cfun dealloc) in let actuals = [(Exp.Var id, typ)] in diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 10373acf5..f6d6bf009 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -539,7 +539,7 @@ module GenericArrayBackedCollection = struct let eval_element location internal_array index astate = - PulseOperations.eval_access location internal_array (ArrayAccess (Typ.void, index)) astate + PulseOperations.eval_access location internal_array (ArrayAccess (StdTyp.void, index)) astate let element location collection index astate = diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 147760c22..81efa107a 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -107,7 +107,7 @@ let eval location exp0 astate = let* astate, addr_hist_index = eval exp_index astate in let* astate, addr_hist = eval exp' astate in let+ astate = check_addr_access location addr_hist astate in - Memory.eval_edge addr_hist (ArrayAccess (Typ.void, fst addr_hist_index)) astate + Memory.eval_edge addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate | Closure {name; captured_vars} -> let+ astate, rev_captured = List.fold_result captured_vars ~init:(astate, []) @@ -202,7 +202,7 @@ let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = let write_arr_index location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate = - write_access location addr_trace_ref (ArrayAccess (Typ.void, index)) addr_trace_obj astate + write_access location addr_trace_ref (ArrayAccess (StdTyp.void, index)) addr_trace_obj astate let havoc_field location addr_trace field trace_obj astate = diff --git a/infer/src/quandary/ClangTrace.ml b/infer/src/quandary/ClangTrace.ml index 40a14e145..599a0e00e 100644 --- a/infer/src/quandary/ClangTrace.ml +++ b/infer/src/quandary/ClangTrace.ml @@ -103,7 +103,7 @@ module SourceKind = struct | Some {Typ.desc} -> desc | None -> - Typ.void_star.desc + StdTyp.void_star.desc in [(CommandLineFlag (global_pvar, typ_desc), None)] else [] diff --git a/infer/src/test_determinator/JProcname.ml b/infer/src/test_determinator/JProcname.ml index 4ad879604..d742bb6e3 100644 --- a/infer/src/test_determinator/JProcname.ml +++ b/infer/src/test_determinator/JProcname.ml @@ -70,23 +70,23 @@ module JNI = struct let rec to_typ jni = match jni with | Boolean -> - Typ.boolean + StdTyp.boolean | Byte -> - Typ.java_byte + StdTyp.Java.byte | Char -> - Typ.java_char + StdTyp.Java.char | Short -> - Typ.java_short + StdTyp.Java.short | Int -> - Typ.int + StdTyp.int | Long -> - Typ.long + StdTyp.long | Float -> - Typ.float + StdTyp.float | Double -> - Typ.double + StdTyp.double | Void -> - Typ.void + StdTyp.void | FullyQualifiedClass (pkg, classname) -> Typ.(mk_ptr (mk_struct (JavaClass (JavaClassName.make ~package:(Some pkg) ~classname)))) | Array typ -> diff --git a/infer/src/topl/ToplUtils.ml b/infer/src/topl/ToplUtils.ml index 388f1c04e..14f292179 100644 --- a/infer/src/topl/ToplUtils.ml +++ b/infer/src/topl/ToplUtils.ml @@ -8,7 +8,7 @@ open! IStd let any_type : Typ.t = - let classname = Typ.mk (Tstruct Typ.Name.Java.java_lang_object) in + let classname = Typ.mk (Tstruct StdTyp.Name.Java.java_lang_object) in Typ.mk (Tptr (classname, Pk_pointer)) @@ -18,8 +18,8 @@ let topl_class_typ = Typ.mk (Tstruct topl_class_name) let topl_call ret_id (ret_typ : Typ.desc) loc method_name arg_ts : Sil.instr = let e_fun = - let return_type = Some Typ.void in - let parameters = List.map arg_ts ~f:(fun _ -> Typ.pointer_to_java_lang_object) in + let return_type = Some StdTyp.void in + let parameters = List.map arg_ts ~f:(fun _ -> StdTyp.Java.pointer_to_java_lang_object) in Exp.Const (Const.Cfun (Procname.make_java ~class_name:topl_class_name ~return_type ~method_name ~parameters diff --git a/infer/src/unit/JavaProfilerSamplesTest.ml b/infer/src/unit/JavaProfilerSamplesTest.ml index 1b576d59c..23922d181 100644 --- a/infer/src/unit/JavaProfilerSamplesTest.ml +++ b/infer/src/unit/JavaProfilerSamplesTest.ml @@ -150,27 +150,36 @@ let test_from_json_string_with_valid_input = make_java ~class_name:(Typ.Name.Java.from_string "lll.mmm.Nnn") ~return_type:None ~method_name:Java.constructor_method_name - ~parameters:[Typ.pointer_to_java_lang_string; Typ.(mk_ptr (mk_array int)); Typ.long] + ~parameters: + [ StdTyp.Java.pointer_to_java_lang_string + ; Typ.(mk_ptr (mk_array StdTyp.int)) + ; StdTyp.long ] ~kind:Java.Non_Static ()) ; Procname.( make_java ~class_name:(Typ.Name.Java.from_string "ggg.hhh.Iii") ~return_type:None ~method_name:Java.class_initializer_method_name - ~parameters:[Typ.pointer_to_java_lang_string; Typ.(mk_ptr (mk_array int)); Typ.long] + ~parameters: + [ StdTyp.Java.pointer_to_java_lang_string + ; Typ.(mk_ptr (mk_array StdTyp.int)) + ; StdTyp.long ] ~kind:Java.Non_Static ()) ] ) ; ( "label2" , Procname.Set.of_list [ Procname.( make_java ~class_name:(Typ.Name.Java.from_string "ddd.eee.Fff") - ~return_type:(Some Typ.(mk_ptr (mk_array (mk_ptr (mk_array java_char))))) + ~return_type:(Some Typ.(mk_ptr (mk_array (mk_ptr (mk_array StdTyp.Java.char))))) ~method_name:"methodTwo" - ~parameters:[Typ.pointer_to_java_lang_string; Typ.(mk_ptr (mk_array int)); Typ.long] + ~parameters: + [ StdTyp.Java.pointer_to_java_lang_string + ; Typ.(mk_ptr (mk_array StdTyp.int)) + ; StdTyp.long ] ~kind:Java.Non_Static ()) ; Procname.( make_java ~class_name:(Typ.Name.Java.from_string "aaa.bbb.Ccc") - ~return_type:(Some Typ.void) ~method_name:"methodOne" ~parameters:[] + ~return_type:(Some StdTyp.void) ~method_name:"methodOne" ~parameters:[] ~kind:Java.Non_Static ()) ] ) ] in let expected3 = @@ -191,12 +200,12 @@ let test_from_json_string_with_valid_input = [ Procname.( make_java ~class_name:(Typ.Name.Java.from_string "ddd.eee.Fff") - ~return_type:(Some Typ.void) ~method_name:"methodTwo" ~parameters:[] + ~return_type:(Some StdTyp.void) ~method_name:"methodTwo" ~parameters:[] ~kind:Java.Non_Static ()) ; Procname.( make_java ~class_name:(Typ.Name.Java.from_string "aaa.bbb.Ccc") - ~return_type:(Some Typ.void) ~method_name:"methodOne" ~parameters:[] + ~return_type:(Some StdTyp.void) ~method_name:"methodOne" ~parameters:[] ~kind:Java.Non_Static ()) ] ) ] in [ ("test_from_json_string_1", input1, expected1, true) diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 309fd88b4..37939a0b2 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -108,10 +108,10 @@ let tests = let call_sink actual_str = call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in let assign_id_to_field root_str fld_str rhs_id_str = let rhs_exp = Exp.Var (ident_of_str rhs_id_str) in - make_store ~rhs_typ:Typ.void (Exp.Var (ident_of_str root_str)) fld_str ~rhs_exp + make_store ~rhs_typ:StdTyp.void (Exp.Var (ident_of_str root_str)) fld_str ~rhs_exp in let read_field_to_id lhs_id_str root_str fld_str = - make_load_fld ~rhs_typ:Typ.void lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) + make_load_fld ~rhs_typ:StdTyp.void lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) in let assert_empty = invariant "{ }" in let exe_env = Exe_env.mk () in diff --git a/infer/src/unit/TraceTests.ml b/infer/src/unit/TraceTests.ml index 80d2647cd..acc9489e8 100644 --- a/infer/src/unit/TraceTests.ml +++ b/infer/src/unit/TraceTests.ml @@ -112,7 +112,9 @@ let tests = let append = let append_ _ = let call_site = CallSite.dummy in - let footprint_ap = AccessPath.Abs.Exact (AccessPath.of_id (Ident.create_none ()) Typ.void) in + let footprint_ap = + AccessPath.Abs.Exact (AccessPath.of_id (Ident.create_none ()) StdTyp.void) + in let source_trace = MockTrace.of_source source1 in let footprint_trace = MockTrace.of_footprint footprint_ap |> MockTrace.add_sink sink1 in let expected_trace = MockTrace.of_source source1 |> MockTrace.add_sink sink1 in diff --git a/infer/src/unit/accessPathTestUtils.ml b/infer/src/unit/accessPathTestUtils.ml index c87b7111c..81ff80914 100644 --- a/infer/src/unit/accessPathTestUtils.ml +++ b/infer/src/unit/accessPathTestUtils.ml @@ -9,7 +9,7 @@ open! IStd let make_var var_str = Pvar.mk (Mangled.from_string var_str) Procname.empty_block -let make_base ?(typ = Typ.void) base_str = AccessPath.base_of_pvar (make_var base_str) typ +let make_base ?(typ = StdTyp.void) base_str = AccessPath.base_of_pvar (make_var base_str) typ let make_fieldname field_name = assert (not (String.contains field_name '.')) ; diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 79571028f..ba24184cf 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -62,7 +62,7 @@ let tests = let z_base = make_base "z" in let f = make_field_access "f" in let g = make_field_access "g" in - let array = make_array_access Typ.void in + let array = make_array_access StdTyp.void in let x = AccessPath.Abs.Exact (make_access_path "x" []) in let xF = AccessPath.Abs.Exact (make_access_path "x" ["f"]) in let xG = AccessPath.Abs.Exact (make_access_path "x" ["g"]) in diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index b44e511a8..57fbacd1f 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -86,7 +86,7 @@ module StructuredSil = struct | Some ret_id_typ -> ret_id_typ | None -> - (Ident.create_fresh Ident.knormal, Typ.void) + (Ident.create_fresh Ident.knormal, StdTyp.void) in let call_exp = Exp.Const (Const.Cfun procname) in Cmd (Sil.Call (ret_id_typ, call_exp, args, dummy_loc, CallFlags.default))