diff --git a/infer/src/IR/tenv.ml b/infer/src/IR/tenv.ml index 99ce51308..f821a5c3b 100644 --- a/infer/src/IR/tenv.ml +++ b/infer/src/IR/tenv.ml @@ -32,36 +32,64 @@ let lookup tenv name = try Some (TypenameHash.find tenv name) with Not_found -> None -exception Cannot_convert_string_to_typ of string - (** Lookup Java types by name *) let lookup_java_typ_from_string tenv typ_str = let rec loop = function - | "" | "void" -> Sil.Tvoid - | "int" -> Sil.Tint Sil.IInt - | "byte" -> Sil.Tint Sil.IShort - | "short" -> Sil.Tint Sil.IShort - | "boolean" -> Sil.Tint Sil.IBool - | "char" -> Sil.Tint Sil.IChar - | "long" -> Sil.Tint Sil.ILong - | "float" -> Sil.Tfloat Sil.FFloat - | "double" -> Sil.Tfloat Sil.FDouble + | "" | "void" -> + Some Sil.Tvoid + | "int" -> + Some (Sil.Tint Sil.IInt) + | "byte" -> + Some (Sil.Tint Sil.IShort) + | "short" -> + Some (Sil.Tint Sil.IShort) + | "boolean" -> + Some (Sil.Tint Sil.IBool) + | "char" -> + Some (Sil.Tint Sil.IChar) + | "long" -> + Some (Sil.Tint Sil.ILong) + | "float" -> + Some (Sil.Tfloat Sil.FFloat) + | "double" -> + Some (Sil.Tfloat Sil.FDouble) | typ_str when String.contains typ_str '[' -> let stripped_typ = String.sub typ_str 0 ((String.length typ_str) - 2) in let array_typ_size = Sil.exp_get_undefined false in - Sil.Tptr (Sil.Tarray (loop stripped_typ, array_typ_size), Sil.Pk_pointer) + begin + match loop stripped_typ with + | Some typ -> Some (Sil.Tptr (Sil.Tarray (typ, array_typ_size), Sil.Pk_pointer)) + | None -> None + end | typ_str -> (* non-primitive/non-array type--resolve it in the tenv *) - let typename = Typename.TN_csu (Csu.Class Csu.Java, (Mangled.from_string typ_str)) in - match lookup tenv typename with - | Some struct_typ -> Sil.Tstruct struct_typ - | _ -> raise (Cannot_convert_string_to_typ typ_str) in + let typename = Typename.Java.from_string typ_str in + begin + match lookup tenv typename with + | Some struct_typ -> Some (Sil.Tstruct struct_typ) + | None -> None + end in loop typ_str +(** resolve a type string to a Java *class* type. For strings that may represent primitive or array + typs, use [lookup_java_typ_from_string] *) +let lookup_java_class_from_string tenv typ_str = + match lookup_java_typ_from_string tenv typ_str with + | Some (Sil.Tstruct struct_typ) -> Some struct_typ + | _ -> None + (** Add a (name,type) pair to the global type environment. *) let add tenv name struct_typ = TypenameHash.replace tenv name struct_typ +(** Return the declaring class type of [pname_java] *) +let proc_extract_declaring_class_typ tenv pname_java = + lookup_java_class_from_string tenv (Procname.java_get_class_name pname_java) + +(** Return the return type of [pname_java]. *) +let proc_extract_return_typ tenv pname_java = + lookup_java_typ_from_string tenv (Procname.java_get_return_type pname_java) + (** expand a type if it is a typename by looking it up in the type environment *) let expand_type tenv typ = match typ with diff --git a/infer/src/IR/tenv.mli b/infer/src/IR/tenv.mli index ad2dee200..0e24c7821 100644 --- a/infer/src/IR/tenv.mli +++ b/infer/src/IR/tenv.mli @@ -32,9 +32,18 @@ val load_from_file : DB.filename -> t option (** Look up a name in the global type environment. *) val lookup : t -> Typename.t -> Sil.struct_typ option -(** Lookup Java types by name. May raise [Cannot_convert_string_to_typ]. *) -exception Cannot_convert_string_to_typ of string -val lookup_java_typ_from_string : t -> string -> Sil.typ +(** Lookup Java types by name. *) +val lookup_java_typ_from_string : t -> string -> Sil.typ option + +(** resolve a type string to a Java *class* type. For strings that may represent primitive or array + typs, use [lookup_java_typ_from_string]. *) +val lookup_java_class_from_string : t -> string -> Sil.struct_typ option + +(** Return the declaring class type of [pname_java] *) +val proc_extract_declaring_class_typ : t -> Procname.java -> Sil.struct_typ option + +(** Return the return type of [pname_java]. *) +val proc_extract_return_typ : t -> Procname.java -> Sil.typ option (** Check if typename is found in t *) val mem : t -> Typename.t -> bool diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index dead77de4..b7f161bbb 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -538,10 +538,11 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t let get_receiver_typ pname fallback_typ = match pname with | Procname.Java pname_java -> - (try - let receiver_typ_str = Procname.java_get_class_name pname_java in - Sil.Tptr (Tenv.lookup_java_typ_from_string tenv receiver_typ_str, Sil.Pk_pointer) - with Tenv.Cannot_convert_string_to_typ _ -> fallback_typ) + begin + match Tenv.proc_extract_declaring_class_typ tenv pname_java with + | Some struct_typ -> Sil.Tptr (Tstruct struct_typ, Pk_pointer) + | None -> fallback_typ + end | _ -> fallback_typ in let receiver_types_equal pname actual_receiver_typ = @@ -1044,11 +1045,11 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path begin match summary_opt with | None -> - let ret_typ_str = Procname.java_get_return_type callee_pname_java in let ret_typ = - match Tenv.lookup_java_typ_from_string tenv ret_typ_str with - | Sil.Tstruct _ as typ -> Sil.Tptr (typ, Sil.Pk_pointer) - | typ -> typ in + match Tenv.proc_extract_return_typ tenv callee_pname_java with + | Some (Sil.Tstruct _ as typ) -> Sil.Tptr (typ, Pk_pointer) + | Some typ -> typ + | None -> Sil.Tvoid in exec_skip_call resolved_pname ret_typ | Some summary when call_should_be_skipped resolved_pname summary -> exec_skip_call resolved_pname summary.Specs.attributes.ProcAttributes.ret_type @@ -1057,7 +1058,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path end | Sil.Call (ret_ids, - Sil.Const (Sil.Cfun ((Procname.Java _) as callee_pname)), + Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)), actual_params, loc, call_flags) -> do_error_checks (Paths.Path.curr_node path) instr current_pname current_pdesc; let norm_prop, norm_args = normalize_params current_pname prop_ actual_params in @@ -1071,15 +1072,11 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path skip_call norm_prop path pname loc ret_ids (Some ret_type) url_handled_args in match Specs.get_summary pname with | None -> - let ret_typ_str = match pname with - | Procname.Java pname_java -> - Procname.java_get_return_type pname_java - | _ -> - "unknown_return_type" in let ret_typ = - match Tenv.lookup_java_typ_from_string tenv ret_typ_str with - | Sil.Tstruct _ as typ -> Sil.Tptr (typ, Sil.Pk_pointer) - | typ -> typ in + match Tenv.proc_extract_return_typ tenv callee_pname_java with + | Some (Sil.Tstruct _ as typ) -> Sil.Tptr (typ, Pk_pointer) + | Some typ -> typ + | None -> Sil.Tvoid in exec_skip_call ret_typ | Some summary when call_should_be_skipped pname summary -> exec_skip_call summary.Specs.attributes.ProcAttributes.ret_type diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 4316bf185..13c1940d6 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -46,16 +46,9 @@ let get_field_type_and_annotation fn = function (** Return the annotations on the declaring class of [pname]. Only works for Java *) let get_declaring_class_annotations pname tenv = - match pname with - | Procname.Java pname_java -> - let receiver_typ_str = Procname.java_get_class_name pname_java in - begin - match Tenv.lookup_java_typ_from_string tenv receiver_typ_str with - | Sil.Tstruct { struct_annotations; } -> Some struct_annotations - | exception Tenv.Cannot_convert_string_to_typ _ -> None - | _ -> None - end - | _ -> None + match Tenv.proc_extract_declaring_class_typ tenv pname with + | Some { Sil.struct_annotations } -> Some struct_annotations + | None -> None let ia_iter f = let ann_iter (a, _) = f a in diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index d87602f01..b7f23ddec 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -54,8 +54,8 @@ val get_annotated_signature : ProcAttributes.t -> annotated_signature val get_field_type_and_annotation : Ident.fieldname -> Sil.typ -> (Sil.typ * Sil.item_annotation) option -(** Return the annotations on the declaring class of [pname]. Only works for Java *) -val get_declaring_class_annotations : Procname.t -> Tenv.t -> Sil.item_annotation option +(** Return the annotations on the declaring class of [java_pname]. *) +val get_declaring_class_annotations : Procname.java -> Tenv.t -> Sil.item_annotation option val nullable : string diff --git a/infer/src/checkers/performanceCritical.ml b/infer/src/checkers/performanceCritical.ml index 9ce222f8c..1409926bc 100644 --- a/infer/src/checkers/performanceCritical.ml +++ b/infer/src/checkers/performanceCritical.ml @@ -40,10 +40,14 @@ let is_modeled_expensive = let check_attributes check tenv pname = - let check_class_attributes check tenv pname = - match Annotations.get_declaring_class_annotations pname tenv with - | Some annotations -> check annotations - | None -> false in + let check_class_attributes check tenv = function + | Procname.Java java_pname -> + begin + match Annotations.get_declaring_class_annotations java_pname tenv with + | Some annotations -> check annotations + | None -> false + end + | _ -> false in let check_method_attributes check pname = match Specs.proc_resolve_attributes pname with | None -> false diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 7cc453ece..9278ebadc 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -582,11 +582,15 @@ let typecheck_instr else Printf.sprintf "arg%d" i in (Mangled.from_string arg, typ)) etl_ in - let ret_typ_str = Procname.java_get_return_type callee_pname_java in let ret_type = - match Tenv.lookup_java_typ_from_string tenv ret_typ_str with - | Sil.Tstruct _ as typ -> Sil.Tptr (typ, Sil.Pk_pointer) - | typ -> typ in + match Tenv.proc_extract_return_typ tenv callee_pname_java with + | Some (Sil.Tstruct _ as typ) -> + Sil.Tptr (typ, Pk_pointer) + | Some typ -> + typ + | None -> + let ret_typ_string = Procname.java_get_return_type callee_pname_java in + Sil.Tptr (Tvar (Typename.Java.from_string ret_typ_string), Pk_pointer) in let proc_attributes = { (ProcAttributes.default callee_pname Config.Java) with ProcAttributes.formals;