[infer][java] Remove the code adding a special treatment for static final fields

Summary: This code is an old experiement and has never really be used in prod because it was creating false positive. Dealing static final fields should be done in the backend instead so that it can used by the different languages C, Objective C, C++ and Java.

Reviewed By: jberdine

Differential Revision: D4055292

fbshipit-source-id: f1dc715
master
Jeremy Dubreil 8 years ago committed by Facebook Github Bot
parent b1a2a304e2
commit a7d2eb1d02

@ -319,8 +319,6 @@ class AnalyzerWithFrontendWrapper(analyze.AnalyzerWrapper):
if os.path.isfile(config.MODELS_JAR): if os.path.isfile(config.MODELS_JAR):
infer_cmd += ['-models', config.MODELS_JAR] infer_cmd += ['-models', config.MODELS_JAR]
infer_cmd.append('-no-static_final')
if self.args.debug: if self.args.debug:
infer_cmd.append('-debug') infer_cmd.append('-debug')
if self.args.analyzer == config.ANALYZER_TRACING: if self.args.analyzer == config.ANALYZER_TRACING:

@ -1083,10 +1083,6 @@ and stacktraces_dir =
Used to guide the analysis (only with '-a crashcontext'). See \ Used to guide the analysis (only with '-a crashcontext'). See \
tests/codetoanalyze/java/crashcontext/*.json for examples of the expected format." tests/codetoanalyze/java/crashcontext/*.json for examples of the expected format."
and static_final =
CLOpt.mk_bool ~deprecated_no:["no-static_final"] ~long:"static-final" ~default:true
"Special treatment for static final fields"
and stats = and stats =
CLOpt.mk_bool ~deprecated:["stats"] ~long:"stats" "Stats mode (debugging)" CLOpt.mk_bool ~deprecated:["stats"] ~long:"stats" "Stats mode (debugging)"
@ -1474,7 +1470,6 @@ and models_mode = !models_mode
and modified_targets = !modified_targets and modified_targets = !modified_targets
and monitor_prop_size = !monitor_prop_size and monitor_prop_size = !monitor_prop_size
and nelseg = !nelseg and nelseg = !nelseg
and no_static_final = not !static_final
and no_translate_libs = not !headers and no_translate_libs = not !headers
and objc_memory_model_on = !objc_memory_model and objc_memory_model_on = !objc_memory_model
and only_footprint = !only_footprint and only_footprint = !only_footprint

@ -217,7 +217,6 @@ val models_mode : bool
val modified_targets : string option val modified_targets : string option
val monitor_prop_size : bool val monitor_prop_size : bool
val nelseg : bool val nelseg : bool
val no_static_final : bool
val no_translate_libs : bool val no_translate_libs : bool
val objc_memory_model_on : bool val objc_memory_model_on : bool
val only_footprint : bool val only_footprint : bool

@ -20,11 +20,7 @@ type jump_kind =
| Jump of int | Jump of int
| Exit | Exit
type meth_kind = (** Translation data *)
| Normal
| Init
(** data *)
type icfg = { type icfg = {
tenv : Tenv.t; tenv : Tenv.t;
cg : Cg.t; cg : Cg.t;
@ -39,12 +35,11 @@ type t =
if_jumps : int NodeTbl.t; if_jumps : int NodeTbl.t;
goto_jumps : (int, jump_kind) Hashtbl.t; goto_jumps : (int, jump_kind) Hashtbl.t;
cn : JBasics.class_name; cn : JBasics.class_name;
meth_kind : meth_kind;
source_file : DB.source_file; source_file : DB.source_file;
program : JClasspath.program; program : JClasspath.program;
} }
let create_context icfg procdesc impl cn meth_kind source_file program = let create_context icfg procdesc impl cn source_file program =
{ icfg; { icfg;
procdesc; procdesc;
impl; impl;
@ -52,7 +47,6 @@ let create_context icfg procdesc impl cn meth_kind source_file program =
if_jumps = NodeTbl.create 10; if_jumps = NodeTbl.create 10;
goto_jumps = Hashtbl.create 10; goto_jumps = Hashtbl.create 10;
cn; cn;
meth_kind;
source_file; source_file;
program; program;
} }

@ -20,11 +20,6 @@ type jump_kind =
| Exit | Exit
(** data structure for identifying whether a method is the initialiser of a class - that initialises the static fields- or a standard method *)
type meth_kind =
| Normal
| Init
(** Hastable for storing nodes that correspond to if-instructions. These are (** Hastable for storing nodes that correspond to if-instructions. These are
used when adding the edges in the contrl flow graph. *) used when adding the edges in the contrl flow graph. *)
module NodeTbl : Hashtbl.S with type key = Cfg.Node.t module NodeTbl : Hashtbl.S with type key = Cfg.Node.t
@ -48,7 +43,6 @@ type t = private
if_jumps : int NodeTbl.t; if_jumps : int NodeTbl.t;
goto_jumps : (int, jump_kind) Hashtbl.t; goto_jumps : (int, jump_kind) Hashtbl.t;
cn : JBasics.class_name; cn : JBasics.class_name;
meth_kind : meth_kind;
source_file : DB.source_file; source_file : DB.source_file;
program : JClasspath.program; program : JClasspath.program;
} }
@ -60,7 +54,6 @@ val create_context :
Cfg.Procdesc.t -> Cfg.Procdesc.t ->
JBir.t -> JBir.t ->
JBasics.class_name -> JBasics.class_name ->
meth_kind ->
DB.source_file -> DB.source_file ->
JClasspath.program -> JClasspath.program ->
t t

@ -74,40 +74,32 @@ let add_edges
Array.iteri connect_nodes method_body_nodes Array.iteri connect_nodes method_body_nodes
(** Add a concrete method. *) (** Add a concrete method. *)
let add_cmethod source_file program icfg node cm is_static = let add_cmethod source_file program icfg cm is_static =
let cfg = icfg.JContext.cfg in let cfg = icfg.JContext.cfg in
let tenv = icfg.JContext.tenv in let tenv = icfg.JContext.tenv in
let cn, ms = JBasics.cms_split cm.Javalib.cm_class_method_signature in let cn, ms = JBasics.cms_split cm.Javalib.cm_class_method_signature in
let is_clinit = JBasics.ms_equal ms JBasics.clinit_signature in match JTrans.get_method_procdesc program cfg tenv cn ms is_static with
if Config.no_static_final = false | JTrans.Defined procdesc when JClasspath.is_model (Cfg.Procdesc.get_proc_name procdesc) ->
&& is_clinit (* do not capture the method if there is a model for it *)
&& not (JTransStaticField.has_static_final_fields node) then JUtils.log
JUtils.log "\t\tskipping class initializer: %s@." (JBasics.ms_name ms) "Skipping method with a model: %s@."
else (Procname.to_string (Cfg.Procdesc.get_proc_name procdesc));
match JTrans.get_method_procdesc program cfg tenv cn ms is_static with | JTrans.Defined procdesc ->
| JTrans.Defined procdesc when JClasspath.is_model (Cfg.Procdesc.get_proc_name procdesc) -> let start_node = Cfg.Procdesc.get_start_node procdesc in
(* do not capture the method if there is a model for it *) let exit_node = Cfg.Procdesc.get_exit_node procdesc in
JUtils.log "Skipping method with a model: %s@." (Procname.to_string (Cfg.Procdesc.get_proc_name procdesc)); let exn_node =
| JTrans.Defined procdesc -> match JContext.get_exn_node procdesc with
let start_node = Cfg.Procdesc.get_start_node procdesc in | Some node -> node
let exit_node = Cfg.Procdesc.get_exit_node procdesc in | None -> assert false in
let exn_node = let impl = JTrans.get_implementation cm in
match JContext.get_exn_node procdesc with let instrs = JBir.code impl in
| Some node -> node let context =
| None -> assert false in JContext.create_context icfg procdesc impl cn source_file program in
let impl = JTrans.get_implementation cm in let method_body_nodes = Array.mapi (JTrans.instruction context) instrs in
let instrs, meth_kind = let procname = Cfg.Procdesc.get_proc_name procdesc in
if is_clinit && not Config.no_static_final then add_edges context start_node exn_node [exit_node] method_body_nodes impl false;
let instrs = JTransStaticField.static_field_init node cn (JBir.code impl) in Cg.add_defined_node icfg.JContext.cg procname;
(instrs, JContext.Init) | JTrans.Called _ -> ()
else (JBir.code impl), JContext.Normal in
let context =
JContext.create_context icfg procdesc impl cn meth_kind source_file program in
let method_body_nodes = Array.mapi (JTrans.instruction context) instrs in
let procname = Cfg.Procdesc.get_proc_name procdesc in
add_edges context start_node exn_node [exit_node] method_body_nodes impl false;
Cg.add_defined_node icfg.JContext.cg procname;
| JTrans.Called _ -> ()
(** Add an abstract method. *) (** Add an abstract method. *)
@ -163,14 +155,14 @@ let create_icfg source_file linereader program icfg cn node =
let cfg = icfg.JContext.cfg in let cfg = icfg.JContext.cfg in
let tenv = icfg.JContext.tenv in let tenv = icfg.JContext.tenv in
begin begin
Javalib.m_iter (JTrans.create_local_procdesc source_file program linereader cfg tenv node) node; Javalib.m_iter (JTrans.create_local_procdesc source_file program linereader cfg tenv) node;
Javalib.m_iter (fun m -> Javalib.m_iter (fun m ->
(* each procedure has different scope: start names from id 0 *) (* each procedure has different scope: start names from id 0 *)
Ident.NameGenerator.reset (); Ident.NameGenerator.reset ();
let method_kind = JTransType.get_method_kind m in let method_kind = JTransType.get_method_kind m in
match m with match m with
| Javalib.ConcreteMethod cm -> | Javalib.ConcreteMethod cm ->
add_cmethod source_file program icfg node cm method_kind add_cmethod source_file program icfg cm method_kind
| Javalib.AbstractMethod am -> | Javalib.AbstractMethod am ->
add_amethod program icfg am method_kind add_amethod program icfg am method_kind
) node ) node

@ -53,23 +53,18 @@ let fix_method_definition_line linereader proc_name_java loc =
{ loc with Location.line = !line } { loc with Location.line = !line }
with Not_found -> loc with Not_found -> loc
let get_location source_file impl pc meth_kind cn = let get_location source_file impl pc =
if meth_kind = JContext.Init then let line_number =
try let ln =
JBasics.ClassMap.find cn !init_loc_map try JBir.get_source_line_number pc impl
with Not_found -> Location.dummy with Invalid_argument _ -> None in
else match ln with
let line_number = | None -> 0
let ln = | Some n -> n in
try JBir.get_source_line_number pc impl { Location.line = line_number;
with Invalid_argument _ -> None in col = -1;
match ln with file = source_file;
| None -> 0 nLOC = !Config.nLOC }
| Some n -> n in
{ Location.line = line_number;
col = -1;
file = source_file;
nLOC = !Config.nLOC }
let get_undefined_method_call ovt = let get_undefined_method_call ovt =
let get_undefined_method ovt = let get_undefined_method ovt =
@ -147,12 +142,8 @@ let formals program tenv cn impl =
(** Creates the local and formal variables from a procedure based on the (** Creates the local and formal variables from a procedure based on the
impl argument. If the meth_kind is Init, we add a parameter field to impl argument. If the meth_kind is Init, we add a parameter field to
the initialiser method. *) the initialiser method. *)
let locals_formals program tenv cn impl meth_kind = let locals_formals program tenv cn impl =
let form_list = let form_list = formals program tenv cn impl in
if meth_kind = JContext.Init then
let string_type = (JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl)) in
[(JConfig.field_st, string_type) ]
else formals program tenv cn impl in
let is_formal p = let is_formal p =
IList.exists (fun (p', _) -> Mangled.equal p p') form_list in IList.exists (fun (p', _) -> Mangled.equal p p') form_list in
let collect l var = let collect l var =
@ -255,121 +246,112 @@ let update_init_loc cn ms loc_start =
with Not_found -> init_loc_map := (JBasics.ClassMap.add cn loc_start !init_loc_map) with Not_found -> init_loc_map := (JBasics.ClassMap.add cn loc_start !init_loc_map)
(** Creates a procedure description. *) (** Creates a procedure description. *)
let create_local_procdesc source_file program linereader cfg tenv node m = let create_local_procdesc source_file program linereader cfg tenv m =
let cn, ms = JBasics.cms_split (Javalib.get_class_method_signature m) in let cn, ms = JBasics.cms_split (Javalib.get_class_method_signature m) in
let meth_kind = let proc_name_java = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in
if JBasics.ms_equal ms JBasics.clinit_signature then JContext.Init let proc_name = Procname.Java proc_name_java in
else JContext.Normal in let create_new_procdesc () =
if not ( let trans_access = function
Config.no_static_final = false && | `Default -> PredSymb.Default
meth_kind = JContext.Init && | `Public -> PredSymb.Public
not (JTransStaticField.has_static_final_fields node)) | `Private -> PredSymb.Private
then | `Protected -> PredSymb.Protected in
let proc_name_java = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in try
let proc_name = Procname.Java proc_name_java in match m with
let create_new_procdesc () = | Javalib.AbstractMethod am -> (* create a procdesc with empty body *)
let trans_access = function let formals =
| `Default -> PredSymb.Default formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in
| `Public -> PredSymb.Public let method_annotation =
| `Private -> PredSymb.Private JAnnotation.translate_method proc_name_java am.Javalib.am_annotations in
| `Protected -> PredSymb.Protected in let procdesc =
try let proc_attributes =
match m with { (ProcAttributes.default proc_name Config.Java) with
| Javalib.AbstractMethod am -> (* create a procdesc with empty body *) ProcAttributes.access = trans_access am.Javalib.am_access;
let formals = exceptions = IList.map JBasics.cn_name am.Javalib.am_exceptions;
formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in formals;
let method_annotation = is_abstract = true;
JAnnotation.translate_method proc_name_java am.Javalib.am_annotations in is_bridge_method = am.Javalib.am_bridge;
let procdesc = is_defined = true;
let proc_attributes = is_synthetic_method = am.Javalib.am_synthetic;
{ (ProcAttributes.default proc_name Config.Java) with method_annotation;
ProcAttributes.access = trans_access am.Javalib.am_access; ret_type = JTransType.return_type program tenv ms;
exceptions = IList.map JBasics.cn_name am.Javalib.am_exceptions; } in
formals; Cfg.Procdesc.create cfg proc_attributes in
is_abstract = true; let start_kind = Cfg.Node.Start_node procdesc in
is_bridge_method = am.Javalib.am_bridge; let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc in
is_defined = true; let exit_kind = (Cfg.Node.Exit_node procdesc) in
is_synthetic_method = am.Javalib.am_synthetic; let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc in
method_annotation; Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node];
ret_type = JTransType.return_type program tenv ms meth_kind; Cfg.Procdesc.set_start_node procdesc start_node;
} in Cfg.Procdesc.set_exit_node procdesc exit_node
Cfg.Procdesc.create cfg proc_attributes in | Javalib.ConcreteMethod cm when is_java_native cm ->
let start_kind = Cfg.Node.Start_node procdesc in let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in
let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc in let method_annotation =
let exit_kind = (Cfg.Node.Exit_node procdesc) in JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in
let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc in let proc_attributes =
Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node]; { (ProcAttributes.default proc_name Config.Java) with
Cfg.Procdesc.set_start_node procdesc start_node; ProcAttributes.access = trans_access cm.Javalib.cm_access;
Cfg.Procdesc.set_exit_node procdesc exit_node exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions;
| Javalib.ConcreteMethod cm when is_java_native cm -> formals;
let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in is_bridge_method = cm.Javalib.cm_bridge;
let method_annotation = is_synthetic_method = cm.Javalib.cm_synthetic;
JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in 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 proc_attributes = let proc_attributes =
{ (ProcAttributes.default proc_name Config.Java) with { (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.access = trans_access cm.Javalib.cm_access; ProcAttributes.access = trans_access cm.Javalib.cm_access;
exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions;
formals; formals;
is_bridge_method = cm.Javalib.cm_bridge; is_bridge_method = cm.Javalib.cm_bridge;
is_defined = true;
is_synthetic_method = cm.Javalib.cm_synthetic; is_synthetic_method = cm.Javalib.cm_synthetic;
is_java_synchronized_method = cm.Javalib.cm_synchronized;
loc = loc_start;
locals;
method_annotation; method_annotation;
ret_type = JTransType.return_type program tenv ms meth_kind; ret_type = JTransType.return_type program tenv ms;
} in } in
ignore (Cfg.Procdesc.create cfg proc_attributes) Cfg.Procdesc.create cfg proc_attributes in
| Javalib.ConcreteMethod cm -> let start_kind = Cfg.Node.Start_node procdesc in
let impl = get_implementation cm in let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in
let locals, formals = locals_formals program tenv cn impl meth_kind in let exit_kind = (Cfg.Node.Exit_node procdesc) in
let loc_start = let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in
let loc = (get_location source_file impl 0 JContext.Normal cn) in let exn_kind = Cfg.Node.exn_sink_kind in
fix_method_definition_line linereader proc_name_java loc in let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc in
let loc_exit = JContext.add_exn_node proc_name exn_node;
get_location Cfg.Procdesc.set_start_node procdesc start_node;
source_file impl (Array.length (JBir.code impl) - 1) JContext.Normal cn in Cfg.Procdesc.set_exit_node procdesc exit_node;
let method_annotation = Cfg.Node.add_locals_ret_declaration start_node locals;
JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in with JBir.Subroutine | JBasics.Class_structure_error _ ->
update_constr_loc cn ms loc_start; L.err
update_init_loc cn ms loc_exit; "create_local_procdesc raised JBir.Subroutine or JBasics.Class_structure_error on %a@."
let procdesc = Procname.pp proc_name in
let proc_attributes = match lookup_procdesc cfg proc_name with
{ (ProcAttributes.default proc_name Config.Java) with | Unknown ->
ProcAttributes.access = trans_access cm.Javalib.cm_access; create_new_procdesc ()
exceptions = IList.map JBasics.cn_name cm.Javalib.cm_exceptions; | Created defined_status ->
formals; begin
is_bridge_method = cm.Javalib.cm_bridge; match defined_status with
is_defined = true; | Defined _ -> assert false
is_synthetic_method = cm.Javalib.cm_synthetic; | Called procdesc ->
is_java_synchronized_method = cm.Javalib.cm_synchronized; Cfg.Procdesc.remove cfg (Cfg.Procdesc.get_proc_name procdesc) false;
loc = loc_start; create_new_procdesc ()
locals; end
method_annotation;
ret_type = JTransType.return_type program tenv ms meth_kind;
} 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;
with JBir.Subroutine | JBasics.Class_structure_error _ ->
L.err
"create_local_procdesc raised JBir.Subroutine or JBasics.Class_structure_error on %a@."
Procname.pp proc_name in
match lookup_procdesc cfg proc_name with
| Unknown ->
create_new_procdesc ()
| Created defined_status ->
begin
match defined_status with
| Defined _ -> assert false
| Called procdesc ->
Cfg.Procdesc.remove cfg (Cfg.Procdesc.get_proc_name procdesc) false;
create_new_procdesc ()
end
let create_external_procdesc program cfg tenv cn ms kind = let create_external_procdesc program cfg tenv cn ms kind =
let return_type = let return_type =
@ -395,9 +377,6 @@ let rec get_method_procdesc program cfg tenv cn ms kind =
get_method_procdesc program cfg tenv cn ms kind get_method_procdesc program cfg tenv cn ms kind
| Created status -> status | Created status -> status
let use_static_final_fields (context : JContext.t) =
(not Config.no_static_final) && context.meth_kind <> JContext.Init
let builtin_new = let builtin_new =
Exp.Const (Const.Cfun ModelBuiltins.__new) Exp.Const (Const.Cfun ModelBuiltins.__new)
@ -411,15 +390,8 @@ let create_sil_deref exp typ loc =
(** translate an expression used as an r-value *) (** translate an expression used as an r-value *)
let rec expression (context : JContext.t) pc expr = let rec expression (context : JContext.t) pc expr =
(* JUtils.log "\t\t\t\texpr: %s@." (JBir.print_expr expr); *) (* JUtils.log "\t\t\t\texpr: %s@." (JBir.print_expr expr); *)
let cn = context.cn in
let program = context.program in let program = context.program in
let loc = let loc = get_location context.source_file context.impl pc in
get_location
context.source_file
context.impl
pc
context.meth_kind
cn in
let file = loc.Location.file in let file = loc.Location.file in
let tenv = JContext.get_tenv context in let tenv = JContext.get_tenv context in
let type_of_expr = JTransType.expr_type context expr in let type_of_expr = JTransType.expr_type context expr in
@ -518,20 +490,6 @@ let rec expression (context : JContext.t) pc expr =
let (instrs, sil_expr) = [], class_exp in let (instrs, sil_expr) = [], class_exp in
let field_name = get_field_name program true tenv cn fs in let field_name = get_field_name program true tenv cn fs in
let sil_type = JTransType.get_class_type_no_pointer program tenv cn in let sil_type = JTransType.get_class_type_no_pointer program tenv cn in
if JTransStaticField.is_static_final_field context cn fs && use_static_final_fields context
then
(* when accessing a static final field, we call the initialiser method. *)
let cfg = JContext.get_cfg context in
let callee_procdesc =
match get_method_procdesc program cfg tenv cn JBasics.clinit_signature Procname.Static with
| Called p | Defined p -> p in
let field_type =
JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl) in
let instrs', expr' =
JTransStaticField.translate_instr_static_field
context callee_procdesc fs field_type loc in
instrs', expr', type_of_expr
else
if JTransType.is_autogenerated_assert_field field_name if JTransType.is_autogenerated_assert_field field_name
then then
(* assume that reading from C.$assertionsDisabled always yields "false". this allows *) (* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
@ -779,27 +737,20 @@ let assume_not_null loc sil_expr =
let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in
Sil.Call (None, builtin_infer_assume, call_args, loc, assume_call_flag) Sil.Call (None, builtin_infer_assume, call_args, loc, assume_call_flag)
let rec instruction (context : JContext.t) pc instr : translation = let rec instruction (context : JContext.t) pc instr : translation =
let cfg = JContext.get_cfg context in let cfg = JContext.get_cfg context in
let tenv = JContext.get_tenv context in let tenv = JContext.get_tenv context in
let cg = JContext.get_cg context in let cg = JContext.get_cg context in
let cn = context.cn in
let program = context.program in let program = context.program in
let meth_kind = context.meth_kind in
let proc_name = Cfg.Procdesc.get_proc_name context.procdesc in let proc_name = Cfg.Procdesc.get_proc_name context.procdesc in
let ret_var = Pvar.get_ret_pvar proc_name in let ret_var = Pvar.get_ret_pvar proc_name in
let ret_type = Cfg.Procdesc.get_ret_type context.procdesc in let ret_type = Cfg.Procdesc.get_ret_type context.procdesc in
let loc = let loc = get_location context.source_file context.impl pc in
get_location context.source_file context.impl pc meth_kind cn in
let file = loc.Location.file in let file = loc.Location.file in
let match_never_null = Inferconfig.never_return_null_matcher in let match_never_null = Inferconfig.never_return_null_matcher in
let create_node node_kind sil_instrs = let create_node node_kind sil_instrs =
Cfg.Node.create Cfg.Node.create cfg loc node_kind sil_instrs context.procdesc in
cfg
(get_location context.source_file context.impl pc meth_kind cn)
node_kind
sil_instrs
context.procdesc in
let return_not_null () = let return_not_null () =
match_never_null loc.Location.file proc_name match_never_null loc.Location.file proc_name
|| ||

@ -31,8 +31,13 @@ val get_method_procdesc : JClasspath.program -> Cfg.cfg -> Tenv.t -> JBasics.cla
(** [create_local_procdesc linereader cfg tenv program m] creates a procedure description for the method m and adds it to cfg *) (** [create_local_procdesc linereader cfg tenv program m] creates a procedure description for the method m and adds it to cfg *)
val create_local_procdesc : val create_local_procdesc :
DB.source_file -> JClasspath.program -> Printer.LineReader.t -> Cfg.cfg -> Tenv.t -> DB.source_file ->
JCode.jcode Javalib.interface_or_class -> JCode.jcode Javalib.jmethod -> unit JClasspath.program ->
Printer.LineReader.t ->
Cfg.cfg ->
Tenv.t ->
JCode.jcode Javalib.jmethod ->
unit
(** returns the implementation of a given method *) (** returns the implementation of a given method *)
val get_implementation : JCode.jcode Javalib.concrete_method -> JBir.t val get_implementation : JCode.jcode Javalib.concrete_method -> JBir.t

@ -1,214 +0,0 @@
(*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! Utils
open Javalib_pack
open Sawja_pack
(* line numbers where the code for the initialization of the static final fields starts *)
let field_final_pcs : int list ref = ref []
(* line numbers where the code for the initialization of the static nonfinal fields starts *)
let field_nonfinal_pcs : int list ref = ref []
let reset_pcs () =
field_final_pcs := [];
field_nonfinal_pcs := []
let sort_pcs () =
field_final_pcs := (IList.sort Pervasives.compare !field_final_pcs);
field_nonfinal_pcs := (IList.sort Pervasives.compare !field_nonfinal_pcs)
(** Returns whether the node contains static final fields
that are not of a primitive type or String. *)
let has_static_final_fields node =
let detect _ f test =
test || (Javalib.is_static_field f && Javalib.is_final_field f) in
JBasics.FieldMap.fold detect (Javalib.get_fields node) false
(* Seems that there is no function "exists" on this implementation of *)
(* Patricia trees *)
(** collects the code line where the fields are initialised. The list is
reversed in order to access the previous element in the list easier (as the successor.) *)
let collect_field_pc instrs field_pc_list =
let aux pc instr =
match instr with
| JBir.AffectStaticField (_, fs, _) ->
field_pc_list := (fs, pc)::!field_pc_list
| _ -> () in
(Array.iteri aux instrs);
(IList.rev !field_pc_list)
(** Changes every position in the code where a static field is set to a value,
to returning that value *)
let add_return_field instrs =
let aux instr =
match instr with
| JBir.AffectStaticField (_, _, e) ->
JBir.Return (Some e)
| _ -> instr in
(Array.map aux instrs)
(** Given a list with the lines where the fields are initialised,
finds the line where the code for the initialisation of the given field starts,
which is the line after the previous field has been initialised. *)
let rec find_pc field list =
match list with
| (fs, _):: rest ->
if JBasics.fs_equal field fs then
try
let (_, npc) = IList.hd rest in
npc + 1
with _ -> 1
else (find_pc field rest)
| [] -> -1
(* Removes the lines of code for initializing nonfinal static fields. *)
let remove_nonfinal_instrs code end_pc =
try
sort_pcs ();
let rec aux2 pc =
let next_pc = pc + 1 in
if not (IList.mem (=) pc !field_final_pcs) && not (IList.mem (=) pc !field_nonfinal_pcs) then
begin
Array.set code pc JBir.Nop;
if next_pc < end_pc then aux2 next_pc
end
else () in
let aux pc _ =
if IList.mem (=) pc !field_nonfinal_pcs then
begin
Array.set code pc JBir.Nop;
aux2 (pc +1)
end
else () in
Array.iteri aux code
with Invalid_argument _ -> assert false
let has_unclear_control_flow code =
let aux instr nok =
match instr with
| JBir.Goto _ -> true
| _ -> nok in
Array.fold_right aux code false
(** In the initialiser of static fields, we add instructions
for returning the field selected by the parameter. *)
(* The constant s means the parameter field of the function.
Note that we remove the initialisation of non - final static fields. *)
let static_field_init_complex code fields length =
let code = Array.append [| (JBir.Goto length ) |] code in
let s = JConfig.field_cst in
let field_pc_list = ref [] in
let _ = collect_field_pc code field_pc_list in
let code = add_return_field code in
let rec aux s fields =
match fields with
| (fs, field):: rest ->
let pc = find_pc fs !field_pc_list in
if Javalib.is_static_field field && Javalib.is_final_field field && pc <> -1 then
let _ = field_final_pcs := pc::!field_final_pcs in
let fs_const = JBir.Const (`String (JBasics.make_jstr (JBasics.fs_name fs))) in
let arg_const = JBir.Const (`String (JBasics.make_jstr s)) in
let arr = [| JBir.Ifd ((`Eq, fs_const, arg_const), pc); JBir.Nop |] in
let rest_instrs = (aux s rest) in
Array.append arr rest_instrs
else
let _ =
if Javalib.is_static_field field && pc <> -1 then
field_nonfinal_pcs := pc::!field_nonfinal_pcs in
aux s rest
| [] -> [| JBir.Nop |] in
let new_instrs = aux s fields in
let code = Array.append code new_instrs in
remove_nonfinal_instrs code length;
reset_pcs ();
code
(** In the initialiser of static fields, we add instructions
for returning the field selected by the parameter without changing
the control flow of the original code. *)
let static_field_init_simple cn code fields length =
let s = JConfig.field_cst in
let rec aux s pc fields =
match fields with
| (fs, field):: rest ->
if Javalib.is_static_field field && Javalib.is_final_field field then
let npc = pc + 2 in
let fs_const = JBir.Const (`String (JBasics.make_jstr (JBasics.fs_name fs))) in
let arg_const = JBir.Const (`String (JBasics.make_jstr s)) in
let arr = [| JBir.Ifd ((`Ne, fs_const, arg_const), npc); JBir.Return (Some (JBir.StaticField (cn, fs))) |] in
let rest_instrs = (aux s npc rest) in
Array.append arr rest_instrs
else (aux s pc rest)
| [] -> [| JBir.Nop |] in
let new_instrs = aux s length fields in
let code = Array.append code new_instrs in
code
(** In the initialiser of static fields, we add instructions
for returning the field selected by the parameter. In normal
cases the code for the initialisation of each field is clearly separated
from the code for the initialisation of the next field. However, in some cases
the fields are initialised in static blocks in which they may use try and catch.
In these cases it is not possible to separate the code for the initialisation
of each field, so we do not change the original code, but append intructions
for returning the selected field. *)
let static_field_init node cn code =
try
let field_list = JBasics.FieldMap.elements (Javalib.get_fields node) in
(* TODO: this translation to a list can be removed and map iterators can be used afterward *)
let length = Array.length code in
Array.set code (length -1) JBir.Nop;
(* TODO: make sure this modification of the array has no side effect *)
let code =
if has_unclear_control_flow code then
static_field_init_simple cn code field_list length
else static_field_init_complex code field_list length in
code
with Not_found -> code
(* when accessing a static final field, we call the initialiser method. *)
let translate_instr_static_field (context : JContext.t) callee_procdesc fs field_type loc =
let cg = JContext.get_cg context in
let caller_procdesc = context.procdesc in
let ret_id = Ident.create_fresh Ident.knormal in
let caller_procname = (Cfg.Procdesc.get_proc_name caller_procdesc) in
let callee_procname = Cfg.Procdesc.get_proc_name callee_procdesc in
let callee_fun = Exp.Const (Const.Cfun callee_procname) in
let field_arg = Exp.Const (Const.Cstr (JBasics.fs_name fs)) in
let call_instr =
Sil.Call
(Some (ret_id, field_type), callee_fun, [field_arg, field_type], loc, CallFlags.default) in
Cg.add_edge cg caller_procname callee_procname;
([call_instr], Exp.Var ret_id)
let is_static_final_field (context : JContext.t) cn fs =
match JClasspath.lookup_node cn context.program with
| None -> false
| Some node ->
try
let f = Javalib.get_field node fs in
let is_static = Javalib.is_static_field f in
let is_final = Javalib.is_final_field f in
(is_static && is_final)
with Not_found -> false
(*
let is_basic_type fs =
let vt = (JBasics.fs_type fs) in
match vt with
| JBasics.TBasic bt -> true
| JBasics.TObject ot -> false
*)

@ -1,26 +0,0 @@
(*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! Utils
open Javalib_pack
open Sawja_pack
val is_static_final_field : JContext.t -> JBasics.class_name -> JBasics.field_signature -> bool
val has_static_final_fields : JCode.jcode Javalib.interface_or_class -> bool
val translate_instr_static_field :
JContext.t -> Cfg.Procdesc.t -> JBasics.field_signature -> Typ.t ->
Location.t -> Sil.instr list * Exp.t
val static_field_init : JCode.jcode Javalib.interface_or_class -> JBasics.class_name -> JBir.instr array -> JBir.instr array

@ -421,15 +421,11 @@ let rec expr_type (context : JContext.t) expr =
(** Returns the return type of the method based on the return type (** Returns the return type of the method based on the return type
specified in ms. If the method is the initialiser, return the type specified in ms. *)
Object instead. *) let return_type program tenv ms =
let return_type program tenv ms meth_kind = match JBasics.ms_rtype ms with
if meth_kind = JContext.Init then | None -> Typ.Tvoid
get_class_type program tenv JBasics.java_lang_object | Some vt -> value_type program tenv vt
else
match JBasics.ms_rtype ms with
| None -> Typ.Tvoid
| Some vt -> value_type program tenv vt
let add_models_types tenv = let add_models_types tenv =

@ -58,10 +58,8 @@ val value_type : JClasspath.program -> Tenv.t -> JBasics.value_type -> Typ.t
val param_type : val param_type :
JClasspath.program -> Tenv.t -> JBasics.class_name -> JBir.var -> JBasics.value_type -> Typ.t JClasspath.program -> Tenv.t -> JBasics.class_name -> JBir.var -> JBasics.value_type -> Typ.t
(** Returns the return type of the method based on the return type specified in ms. (** Returns the return type of the method based on the return type specified in ms. *)
If the method is the initialiser, return the type Object instead. *) val return_type : JClasspath.program -> Tenv.t -> JBasics.method_signature -> Typ.t
val return_type :
JClasspath.program -> Tenv.t -> JBasics.method_signature -> JContext.meth_kind -> Typ.t
(** translates the type of an expression *) (** translates the type of an expression *)
val expr_type : JContext.t -> JBir.expr -> Typ.t val expr_type : JContext.t -> JBir.expr -> Typ.t

Loading…
Cancel
Save