From 2c44035297b37b2adf1f0dcd1037af4255c0134e Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 13 Dec 2019 03:13:47 -0800 Subject: [PATCH] [typ][fieldname] eliminate uses of Java.from_string Summary: This function allows any string, and in particular empty class names. As a first step eliminate it in favour of a function that forces the caller to specify distinct class and field names. It turns out that the frontend already has them, so it saves effort along the way. Reviewed By: jvillard Differential Revision: D18953136 fbshipit-source-id: ff3cdfda5 --- infer/src/IR/Typ.ml | 11 +---------- infer/src/IR/Typ.mli | 3 +-- infer/src/biabduction/Prover.ml | 16 +++++++--------- infer/src/bufferoverrun/bufferOverrunAnalysis.ml | 5 ++++- infer/src/bufferoverrun/bufferOverrunField.ml | 6 +++--- infer/src/java/jTransType.ml | 6 +++--- infer/src/topl/Topl.ml | 14 +++++--------- infer/src/topl/ToplUtils.ml | 6 ++++-- infer/src/topl/ToplUtils.mli | 2 ++ infer/src/unit/accessPathTestUtils.ml | 5 ++++- 10 files changed, 34 insertions(+), 40 deletions(-) diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index e0b281fae..ea46e86ce 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -1486,16 +1486,7 @@ module Fieldname = struct end module Java = struct - let from_string full_fieldname = - let class_name, field_name = - match String.rsplit2 full_fieldname ~on:'.' with - | None -> - ("", full_fieldname) - | Some split -> - split - in - Java {class_name; field_name} - + let from_class_and_field ~class_name ~field_name = Java {class_name; field_name} let is_captured_parameter = function | Java {field_name} -> diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index 2bf60f097..41255d5d4 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -653,8 +653,7 @@ module Fieldname : sig end module Java : sig - val from_string : string -> t - (** Create a java field name from string *) + val from_class_and_field : class_name:string -> field_name:string -> t val is_captured_parameter : t -> bool (** Check if field is a captured parameter *) diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 3eb44d525..fbbc18418 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -2292,17 +2292,14 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * | Clang -> Sil.Earray (Exp.int len, [(index, Sil.Eexp (Exp.zero, Sil.inst_none))], Sil.inst_none) | Java -> - let mk_fld_sexp s = - let fld = Typ.Fieldname.Java.from_string s in + let mk_fld_sexp field_name = + let fld = + Typ.Fieldname.Java.from_class_and_field ~class_name:"java.lang.String" ~field_name + in let se = Sil.Eexp (Exp.Var (Ident.create_fresh Ident.kprimed), Sil.Inone) in (fld, se) in - let fields = - [ "java.lang.String.count" - ; "java.lang.String.hash" - ; "java.lang.String.offset" - ; "java.lang.String.value" ] - in + let fields = ["count"; "hash"; "offset"; "value"] in Sil.Estruct (List.map ~f:mk_fld_sexp fields, Sil.inst_none) in let const_string_texp = @@ -2329,7 +2326,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * let sexp = (* TODO: add appropriate fields *) Sil.Estruct - ( [ ( Typ.Fieldname.Java.from_string "java.lang.Class.name" + ( [ ( Typ.Fieldname.Java.from_class_and_field ~class_name:"java.lang.Class" + ~field_name:"name" , Sil.Eexp (Exp.Const (Const.Cstr s), Sil.Inone) ) ] , Sil.inst_none ) in diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index a70b9c246..2177caabf 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -214,7 +214,10 @@ module TransferFunctions = struct match Typ.Procname.get_class_type_name callee_pname with | Some (JavaClass class_name) -> let class_var = Loc.of_var (Var.of_pvar (Pvar.mk_global class_name)) in - let fn = Typ.Fieldname.Java.from_string (Mangled.to_string class_name ^ ".$VALUES") in + let fn = + Typ.Fieldname.Java.from_class_and_field ~class_name:(Mangled.to_string class_name) + ~field_name:"$VALUES" + in let v = Dom.Mem.find (Loc.append_field class_var ~fn) mem in Dom.Mem.add_stack (Loc.of_id id) v mem | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml index 4b0938aaa..649e94b59 100644 --- a/infer/src/bufferoverrun/bufferOverrunField.ml +++ b/infer/src/bufferoverrun/bufferOverrunField.ml @@ -26,14 +26,14 @@ let pp ~pp_lhs ~pp_lhs_alone ~sep f lhs fn = let mk, get_type = - let classname = "__infer__" in + let class_name = "__infer__" in let types = ref Typ.Fieldname.Map.empty in let mk ?cpp_classname name typ = let fieldname = match cpp_classname with | None -> - let fullname = Format.sprintf "%s.%s" classname name in - Typ.Fieldname.Java.from_string fullname + let class_name, field_name = String.rsplit2_exn ~on:'.' (class_name ^ "." ^ name) in + Typ.Fieldname.Java.from_class_and_field ~class_name ~field_name | Some classname -> Typ.Fieldname.Clang.from_class_name classname name in diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 7086a2e26..01150583a 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -201,9 +201,9 @@ let get_method_kind m = let create_fieldname cn fs = - let fieldname = JBasics.fs_name fs in - let classname = JBasics.cn_name cn in - Typ.Fieldname.Java.from_string (classname ^ "." ^ fieldname) + let field_name = JBasics.fs_name fs in + let class_name = JBasics.cn_name cn in + Typ.Fieldname.Java.from_class_and_field ~class_name ~field_name let create_sil_class_field cn {Javalib.cf_signature; cf_annotations; cf_kind} = diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index a5102cf56..57d9b3c52 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -137,17 +137,13 @@ let add_types tenv = Hashtbl.keys h in let transition_field i = - (Typ.Fieldname.Java.from_string (ToplName.transition i), Typ.mk (Tint IBool), []) - in - let saved_arg_field i = - (Typ.Fieldname.Java.from_string (ToplName.saved_arg i), ToplUtils.any_type, []) - in - let register_field name = - (Typ.Fieldname.Java.from_string (ToplName.reg name), ToplUtils.any_type, []) + (ToplUtils.make_field (ToplName.transition i), Typ.mk (Tint IBool), []) in + let saved_arg_field i = (ToplUtils.make_field (ToplName.saved_arg i), ToplUtils.any_type, []) in + let register_field name = (ToplUtils.make_field (ToplName.reg name), ToplUtils.any_type, []) in let statics = - let state = (Typ.Fieldname.Java.from_string ToplName.state, Typ.mk (Tint IInt), []) in - let retval = (Typ.Fieldname.Java.from_string ToplName.retval, ToplUtils.any_type, []) in + let state = (ToplUtils.make_field ToplName.state, Typ.mk (Tint IInt), []) in + let retval = (ToplUtils.make_field ToplName.retval, ToplUtils.any_type, []) in let transitions = List.init (get_transitions_count ()) ~f:transition_field in let saved_args = List.init (get_max_args ()) ~f:saved_arg_field in let registers = List.map ~f:register_field (get_registers ()) in diff --git a/infer/src/topl/ToplUtils.ml b/infer/src/topl/ToplUtils.ml index cbc032ed9..9e9b01b5b 100644 --- a/infer/src/topl/ToplUtils.ml +++ b/infer/src/topl/ToplUtils.ml @@ -34,10 +34,12 @@ let topl_class_exp = Exp.Lvar var_name -let static_var x : Exp.t = - Exp.Lfield (topl_class_exp, Typ.Fieldname.Java.from_string x, topl_class_typ) +let make_field field_name = + Typ.Fieldname.Java.from_class_and_field ~class_name:ToplName.topl_property ~field_name +let static_var x : Exp.t = Exp.Lfield (topl_class_exp, make_field x, topl_class_typ) + let local_var proc_name x : Exp.t = Exp.Lvar (Pvar.mk (Mangled.from_string x) proc_name) let constant_int (x : int) : Exp.t = Exp.int (IntLit.of_int x) diff --git a/infer/src/topl/ToplUtils.mli b/infer/src/topl/ToplUtils.mli index bc5b752ee..eba412e7b 100644 --- a/infer/src/topl/ToplUtils.mli +++ b/infer/src/topl/ToplUtils.mli @@ -30,3 +30,5 @@ val topl_call : Ident.t -> Typ.desc -> Location.t -> string -> (Exp.t * Typ.t) l val is_synthesized : Typ.Procname.t -> bool val debug : ('a, Format.formatter, unit) IStd.format -> 'a + +val make_field : string -> Typ.Fieldname.t diff --git a/infer/src/unit/accessPathTestUtils.ml b/infer/src/unit/accessPathTestUtils.ml index 4f11c05e2..9c9383aa7 100644 --- a/infer/src/unit/accessPathTestUtils.ml +++ b/infer/src/unit/accessPathTestUtils.ml @@ -11,7 +11,10 @@ let make_var var_str = Pvar.mk (Mangled.from_string var_str) Typ.Procname.empty_ let make_base ?(typ = Typ.mk Tvoid) base_str = AccessPath.base_of_pvar (make_var base_str) typ -let make_fieldname = Typ.Fieldname.Java.from_string +let make_fieldname field_name = + assert (not (String.contains field_name '.')) ; + Typ.Fieldname.Java.from_class_and_field ~class_name:"SomeClass" ~field_name + let make_field_access access_str = AccessPath.FieldAccess (make_fieldname access_str)