diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index 097b94cea..73308f4ad 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -75,12 +75,12 @@ let add_edges (** Add a concrete method. *) -let add_cmethod source_file program icfg cm method_kind = - let cfg = icfg.JContext.cfg in +let add_cmethod source_file program linereader icfg cm method_kind = let cn, ms = JBasics.cms_split cm.Javalib.cm_class_method_signature in let proc_name_java = JTransType.get_method_procname cn ms method_kind in let proc_name = Procname.Java proc_name_java in - match Cfg.Procdesc.find_from_name cfg proc_name with + let jmethod = (Javalib.ConcreteMethod cm) in + match JTrans.create_procdesc source_file program linereader icfg jmethod with | None -> () | Some _ when JTrans.is_java_native cm -> () | Some procdesc -> @@ -101,15 +101,15 @@ let add_cmethod source_file program icfg cm method_kind = (** Add an abstract method. *) -let add_amethod icfg am method_kind = - let cfg = icfg.JContext.cfg in +let add_amethod source_file program linereader icfg am method_kind = let cn, ms = JBasics.cms_split am.Javalib.am_class_method_signature in let proc_name_java = JTransType.get_method_procname cn ms method_kind in let proc_name = Procname.Java proc_name_java in - match Cfg.Procdesc.find_from_name cfg proc_name with + let jmethod = (Javalib.AbstractMethod am) in + match JTrans.create_procdesc source_file program linereader icfg jmethod with | None -> () - | Some procdesc -> - Cg.add_defined_node icfg.JContext.cg (Cfg.Procdesc.get_proc_name procdesc) + | Some _ -> + Cg.add_defined_node icfg.JContext.cg proc_name let path_of_cached_classname cn = @@ -142,27 +142,23 @@ let cache_classname cn = let is_classname_cached cn = Sys.file_exists (path_of_cached_classname cn) + (* Given a source file and a class, translates the code of this class. In init - mode, finds out whether this class contains initializers at all, in this case translates it. In standard mode, all methods are translated *) let create_icfg source_file linereader program icfg cn node = JUtils.log "\tclassname: %s@." (JBasics.cn_name cn); cache_classname cn; - let cfg = icfg.JContext.cfg in - let tenv = icfg.JContext.tenv in - begin - Javalib.m_iter (JTrans.create_procdesc source_file program linereader cfg tenv) node; - Javalib.m_iter (fun m -> - (* each procedure has different scope: start names from id 0 *) - Ident.NameGenerator.reset (); - let method_kind = JTransType.get_method_kind m in - match m with - | Javalib.ConcreteMethod cm -> - add_cmethod source_file program icfg cm method_kind - | Javalib.AbstractMethod am -> - add_amethod icfg am method_kind - ) node - end + let translate m = + (* each procedure has different scope: start names from id 0 *) + Ident.NameGenerator.reset (); + let method_kind = JTransType.get_method_kind m in + match m with + | Javalib.ConcreteMethod cm -> + add_cmethod source_file program linereader icfg cm method_kind + | Javalib.AbstractMethod am -> + add_amethod source_file program linereader icfg am method_kind in + Javalib.m_iter translate node (* returns true for the set of classes that are selected to be translated *) diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 8255dc648..3c46a7034 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -202,10 +202,6 @@ let get_test_operator op = | `Lt -> Binop.Lt | `Ne -> Binop.Ne -type defined_status = - | Defined of Cfg.Procdesc.t - | Called of Cfg.Procdesc.t - let is_java_native cm = (cm.Javalib.cm_implementation = Javalib.Native) @@ -233,13 +229,18 @@ let update_init_loc cn ms loc_start = with Not_found -> init_loc_map := (JBasics.ClassMap.add cn loc_start !init_loc_map) (** Creates a procedure description. *) -let create_procdesc source_file program linereader cfg tenv m = +let create_procdesc source_file program linereader icfg m : Cfg.Procdesc.t option = + let cfg = icfg.JContext.cfg in + let tenv = icfg.JContext.tenv in let cn, ms = JBasics.cms_split (Javalib.get_class_method_signature m) in let proc_name_java = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in let proc_name = Procname.Java proc_name_java in if JClasspath.is_model proc_name then - (* do not translate the method if there is a model for it *) - JUtils.log "Skipping method with a model: %s@." (Procname.to_string proc_name) + begin + (* do not translate the method if there is a model for it *) + JUtils.log "Skipping method with a model: %s@." (Procname.to_string proc_name); + None + end else let trans_access = function | `Default -> PredSymb.Default @@ -247,90 +248,96 @@ let create_procdesc source_file program linereader cfg tenv m = | `Private -> PredSymb.Private | `Protected -> PredSymb.Protected in try - match m with - | Javalib.AbstractMethod am -> (* create a procdesc with empty body *) - let formals = - formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in - let method_annotation = - JAnnotation.translate_method proc_name_java am.Javalib.am_annotations in - let procdesc = - let proc_attributes = - { (ProcAttributes.default proc_name Config.Java) with - ProcAttributes.access = trans_access am.Javalib.am_access; - exceptions = IList.map JBasics.cn_name am.Javalib.am_exceptions; - formals; - is_abstract = true; - is_bridge_method = am.Javalib.am_bridge; - is_defined = true; - is_synthetic_method = am.Javalib.am_synthetic; - method_annotation; - ret_type = JTransType.return_type program tenv ms; - } in - Cfg.Procdesc.create cfg proc_attributes in - let start_kind = Cfg.Node.Start_node procdesc in - let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc in - let exit_kind = (Cfg.Node.Exit_node procdesc) in - let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc in - Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node]; - Cfg.Procdesc.set_start_node procdesc start_node; - Cfg.Procdesc.set_exit_node procdesc exit_node - | Javalib.ConcreteMethod cm when is_java_native cm -> - let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in - let method_annotation = - JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in - let proc_attributes = - { (ProcAttributes.default proc_name Config.Java) with - ProcAttributes.access = trans_access cm.Javalib.cm_access; - exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; - formals; - is_bridge_method = cm.Javalib.cm_bridge; - is_synthetic_method = cm.Javalib.cm_synthetic; - method_annotation; - ret_type = JTransType.return_type program tenv ms; - } in - ignore (Cfg.Procdesc.create cfg proc_attributes) - | Javalib.ConcreteMethod cm -> - let impl = get_implementation cm in - let locals, formals = locals_formals program tenv cn impl in - let loc_start = - let loc = get_location source_file impl 0 in - fix_method_definition_line linereader proc_name_java loc in - let loc_exit = - get_location source_file impl (Array.length (JBir.code impl) - 1) in - let method_annotation = - JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in - update_constr_loc cn ms loc_start; - update_init_loc cn ms loc_exit; - let procdesc = + let procdesc = + match m with + | Javalib.AbstractMethod am -> (* create a procdesc with empty body *) + let formals = + formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in + let method_annotation = + JAnnotation.translate_method proc_name_java am.Javalib.am_annotations in + let procdesc = + let proc_attributes = + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.access = trans_access am.Javalib.am_access; + exceptions = IList.map JBasics.cn_name am.Javalib.am_exceptions; + formals; + is_abstract = true; + is_bridge_method = am.Javalib.am_bridge; + is_defined = true; + is_synthetic_method = am.Javalib.am_synthetic; + method_annotation; + ret_type = JTransType.return_type program tenv ms; + } in + Cfg.Procdesc.create cfg proc_attributes in + let start_kind = Cfg.Node.Start_node procdesc in + let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc in + let exit_kind = (Cfg.Node.Exit_node procdesc) in + let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc in + Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node]; + Cfg.Procdesc.set_start_node procdesc start_node; + Cfg.Procdesc.set_exit_node procdesc exit_node; + procdesc + | Javalib.ConcreteMethod cm when is_java_native cm -> + let formals = + formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in + let method_annotation = + JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in let proc_attributes = { (ProcAttributes.default proc_name Config.Java) with ProcAttributes.access = trans_access cm.Javalib.cm_access; exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; formals; is_bridge_method = cm.Javalib.cm_bridge; - is_defined = true; is_synthetic_method = cm.Javalib.cm_synthetic; - is_java_synchronized_method = cm.Javalib.cm_synchronized; - loc = loc_start; - locals; method_annotation; ret_type = JTransType.return_type program tenv ms; } in - Cfg.Procdesc.create cfg proc_attributes in - let start_kind = Cfg.Node.Start_node procdesc in - let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in - let exit_kind = (Cfg.Node.Exit_node procdesc) in - let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in - let exn_kind = Cfg.Node.exn_sink_kind in - let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc in - JContext.add_exn_node proc_name exn_node; - Cfg.Procdesc.set_start_node procdesc start_node; - Cfg.Procdesc.set_exit_node procdesc exit_node; - Cfg.Node.add_locals_ret_declaration start_node locals; + Cfg.Procdesc.create cfg proc_attributes; + | Javalib.ConcreteMethod cm -> + let impl = get_implementation cm in + let locals, formals = locals_formals program tenv cn impl in + let loc_start = + let loc = get_location source_file impl 0 in + fix_method_definition_line linereader proc_name_java loc in + let loc_exit = + get_location source_file impl (Array.length (JBir.code impl) - 1) in + let method_annotation = + JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in + update_constr_loc cn ms loc_start; + update_init_loc cn ms loc_exit; + let procdesc = + let proc_attributes = + { (ProcAttributes.default proc_name Config.Java) with + ProcAttributes.access = trans_access cm.Javalib.cm_access; + exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; + formals; + is_bridge_method = cm.Javalib.cm_bridge; + is_defined = true; + is_synthetic_method = cm.Javalib.cm_synthetic; + is_java_synchronized_method = cm.Javalib.cm_synchronized; + loc = loc_start; + locals; + method_annotation; + ret_type = JTransType.return_type program tenv ms; + } in + Cfg.Procdesc.create cfg proc_attributes in + let start_kind = Cfg.Node.Start_node procdesc in + let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in + let exit_kind = (Cfg.Node.Exit_node procdesc) in + let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in + let exn_kind = Cfg.Node.exn_sink_kind in + let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc in + JContext.add_exn_node proc_name exn_node; + Cfg.Procdesc.set_start_node procdesc start_node; + Cfg.Procdesc.set_exit_node procdesc exit_node; + Cfg.Node.add_locals_ret_declaration start_node locals; + procdesc in + Some procdesc with JBir.Subroutine | JBasics.Class_structure_error _ -> - L.err + L.stderr "create_procdesc raised JBir.Subroutine or JBasics.Class_structure_error on %a@." - Procname.pp proc_name + Procname.pp proc_name; + None let builtin_new = Exp.Const (Const.Cfun ModelBuiltins.__new) diff --git a/infer/src/java/jTrans.mli b/infer/src/java/jTrans.mli index 6818938a4..7eca6ad86 100644 --- a/infer/src/java/jTrans.mli +++ b/infer/src/java/jTrans.mli @@ -20,11 +20,6 @@ type translation = | Prune of Cfg.Node.t * Cfg.Node.t | Loop of Cfg.Node.t * Cfg.Node.t * Cfg.Node.t -(** data structure to identify whether a method is defined in the given program *) -type defined_status = - | Defined of Cfg.Procdesc.t - | Called of Cfg.Procdesc.t - val is_java_native : JCode.jcode Javalib.concrete_method -> bool (** [create_procdesc linereader cfg tenv program m] creates a procedure description @@ -33,10 +28,9 @@ val create_procdesc : DB.source_file -> JClasspath.program -> Printer.LineReader.t -> - Cfg.cfg -> - Tenv.t -> + JContext.icfg -> JCode.jcode Javalib.jmethod -> - unit + Cfg.Procdesc.t option (** returns the implementation of a given method *) val get_implementation : JCode.jcode Javalib.concrete_method -> JBir.t