pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[infer][Java] more consistent names for env variables

Browse Source
master
jrm 10 years ago
parent d0ea01e354
commit 5e9f88eaeb
11 changed files with 60 additions and 62 deletions
Show Stats Download Patch File Download Diff File

2
infer/models/c/Makefile
Unescape View File

@ -5,7 +5,7 @@ LIBDIR = $(CWD)/../../lib
LIB_SPECS = $(LIBDIR)/specs LIB_SPECS = $(LIBDIR)/specs
C_MODELS_FILE = $(LIB_SPECS)/c_models C_MODELS_FILE = $(LIB_SPECS)/c_models
INFER = ANALYZE_MODELS=1 $(BINDIR)/infer INFER = INFER_ANALYZE_MODELS=1 $(BINDIR)/infer
default: run_infer default: run_infer

2
infer/models/cpp/Makefile
Unescape View File

@ -5,7 +5,7 @@ LIBDIR = $(CWD)/../../lib
LIB_SPECS = $(LIBDIR)/specs LIB_SPECS = $(LIBDIR)/specs
CPP_MODELS_FILE = $(LIB_SPECS)/cpp_models CPP_MODELS_FILE = $(LIB_SPECS)/cpp_models
INFER = ANALYZE_MODELS=1 $(BINDIR)/infer INFER = INFER_ANALYZE_MODELS=1 $(BINDIR)/infer
default: run_infer default: run_infer

2
infer/models/java/Makefile
Unescape View File

@ -2,7 +2,7 @@ SHELL := /bin/bash
CWD = $(shell pwd) CWD = $(shell pwd)
BINDIR = $(CWD)/../../bin BINDIR = $(CWD)/../../bin
INFERJ = ANALYZE_MODELS=1 $(BINDIR)/inferJ --buck --analyzer infer --multicore 1 INFERJ = INFER_ANALYZE_MODELS=1 $(BINDIR)/inferJ --buck --analyzer infer --multicore 1
ANDROID_JAR = ../../lib/java/android/android-19.jar ANDROID_JAR = ../../lib/java/android/android-19.jar
JACKSON_JAR = ../../../dependencies/java/jackson/jackson-2.2.3.jar JACKSON_JAR = ../../../dependencies/java/jackson/jackson-2.2.3.jar

2
infer/models/objc/Makefile
Unescape View File

@ -5,7 +5,7 @@ LIBDIR = $(CWD)/../../lib
LIB_SPECS = $(LIBDIR)/specs LIB_SPECS = $(LIBDIR)/specs
OBJC_MODELS_FILE = $(LIB_SPECS)/objc_models OBJC_MODELS_FILE = $(LIB_SPECS)/objc_models
INFER = ANALYZE_MODELS=1 $(BINDIR)/infer INFER = INFER_ANALYZE_MODELS=1 $(BINDIR)/infer
default: run_infer default: run_infer

4
infer/src/backend/config.ml
Unescape View File

@ -344,9 +344,11 @@ let arc_mode = ref false
let objc_memory_model_on = ref false let objc_memory_model_on = ref false
let report_assertion_failure = from_env_variable "REPORT_ASSERTION_FAILURE" let report_assertion_failure = from_env_variable "INFER_REPORT_ASSERTION_FAILURE"
let default_failure_name = "Assertion_failure" let default_failure_name = "Assertion_failure"
let analyze_models = from_env_variable "INFER_ANALYZE_MODELS"
module Experiment = struct module Experiment = struct
(** if true, activate the subtyping routines in C++ as well, not just in Java *) (** if true, activate the subtyping routines in C++ as well, not just in Java *)

3
infer/src/backend/utils.ml
Unescape View File

@ -423,8 +423,7 @@ let symops_timeout, seconds_timeout =
let default_seconds_timeout = 10 in let default_seconds_timeout = 10 in
let long_symops_timeout = 1000 in let long_symops_timeout = 1000 in
let long_seconds_timeout = 30 in let long_seconds_timeout = 30 in
let analyzing_models = Config.from_env_variable "ANALYZE_MODELS" in if Config.analyze_models then
if analyzing_models then
(* use longer timeouts when analyzing models *) (* use longer timeouts when analyzing models *)
long_symops_timeout, long_seconds_timeout long_symops_timeout, long_seconds_timeout
else else

5
infer/src/java/jMain.ml
Unescape View File

@ -37,11 +37,10 @@ let print_usage_exit () =
exit(1) exit(1)
let () = let () =
let analysing_models = Config.from_env_variable "ANALYZE_MODELS" in
Arg2.parse arg_desc (fun arg -> ()) usage; Arg2.parse arg_desc (fun arg -> ()) usage;
if analysing_models && !JClasspath.models_jar <> "" then if Config.analyze_models && !JClasspath.models_jar <> "" then
failwith "Not expecting model file when analyzing the models"; failwith "Not expecting model file when analyzing the models";
if not analysing_models && !JClasspath.models_jar = "" then if not Config.analyze_models && !JClasspath.models_jar = "" then
failwith "Java model file is required" failwith "Java model file is required"

93
infer/src/java/jTrans.ml
Unescape View File

@ -34,12 +34,10 @@ Since Sawja often reports a method off by a few lines, we search
backwards for a line where the method name is. *) backwards for a line where the method name is. *)
let fix_method_definition_line linereader proc_name loc = let fix_method_definition_line linereader proc_name loc =
let method_name = let method_name =
let raw = Procname.java_get_method proc_name in if Procname.is_constructor proc_name then
if raw = "<init>"
then
let inner_class_name cname = snd (string_split_character cname '$') in let inner_class_name cname = snd (string_split_character cname '$') in
inner_class_name (Procname.java_get_simple_class proc_name) inner_class_name (Procname.java_get_simple_class proc_name)
else raw in else Procname.java_get_method proc_name in
let regex = Str.regexp (Str.quote method_name) in let regex = Str.regexp (Str.quote method_name) in
let method_is_defined_here linenum = let method_is_defined_here linenum =
match Printer.LineReader.from_file_linenum_original linereader loc.Sil.file linenum with match Printer.LineReader.from_file_linenum_original linereader loc.Sil.file linenum with
@ -528,7 +526,7 @@ let rec expression context pc expr =
begin begin
match binop with match binop with
| JBir.ArrayLoad vt -> | JBir.ArrayLoad vt ->
(* add an instruction that dereferences the array *) (* add an instruction that dereferences the array *)
let array_typ = Sil.Tarray(type_of_expr, Sil.Var (Ident.create_fresh Ident.kprimed)) in let array_typ = Sil.Tarray(type_of_expr, Sil.Var (Ident.create_fresh Ident.kprimed)) in
let fresh_id, deref_array_instr = create_sil_deref sil_ex1 array_typ loc in let fresh_id, deref_array_instr = create_sil_deref sil_ex1 array_typ loc in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
@ -574,19 +572,20 @@ let rec expression context pc expr =
let callee_procdesc = let callee_procdesc =
match get_method_procdesc program cfg tenv cn JBasics.clinit_signature Static with match get_method_procdesc program cfg tenv cn JBasics.clinit_signature Static with
| Called p | Defined p -> p in | Called p | Defined p -> p in
let field_type = (JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl)) in let field_type =
JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl) in
JTransStaticField.translate_instr_static_field context callee_procdesc fs field_type loc JTransStaticField.translate_instr_static_field context callee_procdesc fs field_type loc
else 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 *)
(* Infer to understand the assert keyword in the expected way *) (* Infer to understand the assert keyword in the expected way *)
(idl, instrs, Sil.exp_zero) (idl, instrs, Sil.exp_zero)
else else
let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
let tmp_id = Ident.create_fresh Ident.knormal in let tmp_id = Ident.create_fresh Ident.knormal in
let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
(idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id) (idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id)
let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code is_static = let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code is_static =
let cfg = JContext.get_cfg context in let cfg = JContext.get_cfg context in
@ -595,7 +594,8 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
let cf_virtual = match invoke_code with let cf_virtual = match invoke_code with
| I_Virtual -> true | I_Virtual -> true
| _ -> false in | _ -> false in
let call_flags = { Sil.cf_virtual = cf_virtual; Sil.cf_noreturn = false; Sil.cf_is_objc_block = false; } in let call_flags =
{ Sil.cf_virtual = cf_virtual; Sil.cf_noreturn = false; Sil.cf_is_objc_block = false; } in
let callee_procdesc = let callee_procdesc =
match get_method_procdesc program cfg tenv cn ms is_static with match get_method_procdesc program cfg tenv cn ms is_static with
| Called p | Defined p -> p in | Called p | Defined p -> p in
@ -603,22 +603,22 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
match sil_obj_opt with match sil_obj_opt with
| None -> ([], [], []) | None -> ([], [], [])
| Some (sil_obj_expr, sil_obj_type) -> | Some (sil_obj_expr, sil_obj_type) ->
(* for non-constructors, add an instruction that dereferences the receiver *) (* for non-constructors, add an instruction that dereferences the receiver *)
let ids, instrs = let ids, instrs =
let is_non_constructor_call = let is_non_constructor_call =
match invoke_code with match invoke_code with
| I_Special -> false | I_Special -> false
| _ -> true in | _ -> true in
match sil_obj_expr with match sil_obj_expr with
| Sil.Var id when is_non_constructor_call && not !JConfig.translate_checks -> | Sil.Var id when is_non_constructor_call && not !JConfig.translate_checks ->
let obj_typ_no_ptr = let obj_typ_no_ptr =
match sil_obj_type with match sil_obj_type with
| Sil.Tptr (typ, _) -> typ | Sil.Tptr (typ, _) -> typ
| _ -> sil_obj_type in | _ -> sil_obj_type in
let fresh_id, deref = create_sil_deref sil_obj_expr obj_typ_no_ptr loc in let fresh_id, deref = create_sil_deref sil_obj_expr obj_typ_no_ptr loc in
[fresh_id], [deref] [fresh_id], [deref]
| _ -> [], [] in | _ -> [], [] in
(ids, instrs, [(sil_obj_expr, sil_obj_type)]) in (ids, instrs, [(sil_obj_expr, sil_obj_type)]) in
let (idl, instrs, call_args) = let (idl, instrs, call_args) =
list_fold_left list_fold_left
(fun (idl_accu, instrs_accu, args_accu) expr -> (fun (idl_accu, instrs_accu, args_accu) expr ->
@ -631,17 +631,17 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
if JBasics.cn_equal cn JConfig.infer_builtins_cl then if JBasics.cn_equal cn JConfig.infer_builtins_cl then
Procname.from_string (JBasics.ms_name ms) Procname.from_string (JBasics.ms_name ms)
else Cfg.Procdesc.get_proc_name callee_procdesc in else Cfg.Procdesc.get_proc_name callee_procdesc in
let (call_idl, call_instrs) = let call_idl, call_instrs =
let callee_fun = Sil.Const (Sil.Cfun callee_procname) in let callee_fun = Sil.Const (Sil.Cfun callee_procname) in
let return_type = Cfg.Procdesc.get_ret_type callee_procdesc in let return_type = Cfg.Procdesc.get_ret_type callee_procdesc in
let call_ret_instrs sil_var = let call_ret_instrs sil_var =
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call_instr = Sil.Call([ret_id], callee_fun, call_args, loc, call_flags) in let call_instr = Sil.Call ([ret_id], callee_fun, call_args, loc, call_flags) in
let set_instr = Sil.Set (Sil.Lvar sil_var, return_type, Sil.Var ret_id, loc) in let set_instr = Sil.Set (Sil.Lvar sil_var, return_type, Sil.Var ret_id, loc) in
(idl @ [ret_id], instrs @ [call_instr; set_instr]) in (idl @ [ret_id], instrs @ [call_instr; set_instr]) in
match var_opt with match var_opt with
| None -> | None ->
let call_instr = Sil.Call([], callee_fun, call_args, loc, call_flags) in let call_instr = Sil.Call ([], callee_fun, call_args, loc, call_flags) in
(idl, instrs @ [call_instr]) (idl, instrs @ [call_instr])
| Some var -> | Some var ->
let sil_var = JContext.set_pvar context var return_type in let sil_var = JContext.set_pvar context var return_type in
@ -925,10 +925,7 @@ let rec instruction context pc instr : translation =
| JBir.New (var, cn, constr_type_list, constr_arg_list) -> | JBir.New (var, cn, constr_type_list, constr_arg_list) ->
let builtin_new = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__new) in let builtin_new = Sil.Const (Sil.Cfun SymExec.ModelBuiltins.__new) in
let class_type = JTransType.get_class_type program tenv cn in let class_type = JTransType.get_class_type program tenv cn in
let class_type_np = let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in
try
JTransType.get_class_type_no_pointer program tenv cn
with _ -> assert false in
let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in
let args = [(sizeof_exp, class_type)] in let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
@ -940,9 +937,9 @@ let rec instruction context pc instr : translation =
context loc pc None cn constr_ms ret_opt constr_arg_list I_Special Static in context loc pc None cn constr_ms ret_opt constr_arg_list I_Special Static in
let pvar = JContext.set_pvar context var class_type in let pvar = JContext.set_pvar context var class_type in
let set_instr = Sil.Set (Sil.Lvar pvar, class_type, Sil.Var ret_id, loc) in let set_instr = Sil.Set (Sil.Lvar pvar, class_type, Sil.Var ret_id, loc) in
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string constr_procname)) in
let ids = ret_id :: call_ids in let ids = ret_id :: call_ids in
let instrs = (new_instr :: call_instrs) @ [set_instr] in let instrs = (new_instr :: call_instrs) @ [set_instr] in
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string constr_procname)) in
let node = create_node node_kind ids instrs in let node = create_node node_kind ids instrs in
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
Cg.add_edge cg caller_procname constr_procname; Cg.add_edge cg caller_procname constr_procname;
@ -965,11 +962,11 @@ let rec instruction context pc instr : translation =
let sil_obj_opt, args, ids, instrs = let sil_obj_opt, args, ids, instrs =
match args with match args with
| [arg] when is_clone ms -> | [arg] when is_clone ms ->
(* hack to null check the receiver of clone when clone is an array. in the array.clone() (* hack to null check the receiver of clone when clone is an array. in the array.clone()
case, clone is a virtual call that we translate as a static call *) case, clone is a virtual call that we translate as a static call *)
let (ids, instrs, sil_arg_expr) = expression context pc arg in let (ids, instrs, sil_arg_expr) = expression context pc arg in
let arg_typ = JTransType.expr_type context arg in let arg_typ = JTransType.expr_type context arg in
Some (sil_arg_expr, arg_typ), [], ids, instrs Some (sil_arg_expr, arg_typ), [], ids, instrs
| _ -> None, args, [], [] in | _ -> None, args, [], [] in
let (callee_procdesc, callee_procname, call_idl, call_instrs) = let (callee_procdesc, callee_procname, call_idl, call_instrs) =
method_invocation context loc pc var_opt cn ms sil_obj_opt args I_Static Static in method_invocation context loc pc var_opt cn ms sil_obj_opt args I_Static Static in
@ -1026,7 +1023,7 @@ let rec instruction context pc instr : translation =
Instr call_node Instr call_node
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks && is_this expr -> | JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks && is_this expr ->
(* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *) (* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *)
let (ids, instrs, sil_expr) = expression context pc expr in let (ids, instrs, sil_expr) = expression context pc expr in
let this_not_null_node = let this_not_null_node =
create_node create_node
@ -1151,7 +1148,7 @@ let rec instruction context pc instr : translation =
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
let (constr_procdesc, constr_procname, call_ids, call_instrs) = let (constr_procdesc, constr_procname, call_ids, call_instrs) =
method_invocation context loc pc None cce_cn constr_ms method_invocation context loc pc None cce_cn constr_ms
(Some (Sil.Var ret_id, class_type)) [] I_Special Static in (Some (Sil.Var ret_id, class_type)) [] I_Special Static in
let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in let ret_var = Cfg.Procdesc.get_ret_var (JContext.get_procdesc context) in
let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in

5
infer/src/java/jTransType.mli
Unescape View File

@ -13,10 +13,11 @@ val create_fieldname : JBasics.class_name -> JBasics.field_signature -> Ident.fi
(** returns a procedure name based on the class name and the method's signature. *) (** returns a procedure name based on the class name and the method's signature. *)
val get_method_procname : JBasics.class_name -> JBasics.method_signature -> Procname.t val get_method_procname : JBasics.class_name -> JBasics.method_signature -> Procname.t
(** [get_class_type_no_pointer tenv cn] returns the sil type representation of the class without the pointer part *) (** [get_class_type_no_pointer program tenv cn] returns the sil type representation of the class
without the pointer part *)
val get_class_type_no_pointer: JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ val get_class_type_no_pointer: JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ
(** [get_class_type tenv cn] returns the sil type representation of the class *) (** [get_class_type program tenv cn] returns the sil type representation of the class *)
val get_class_type : JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ val get_class_type : JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ
(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *) (** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)

2
infer/tests/codetoanalyze/c/errors/BUCK
Unescape View File

@ -4,7 +4,7 @@ sources += glob(['**/Makefile'])
out = 'out' out = 'out'
clean_cmd = ' '.join(['rm', '-rf', out]) clean_cmd = ' '.join(['rm', '-rf', out])
env_cmd = ' '.join(['export', 'REPORT_ASSERTION_FAILURE=1']) env_cmd = ' '.join(['export', 'INFER_REPORT_ASSERTION_FAILURE=1'])
infer_cmd = ' '.join([ infer_cmd = ' '.join([
'infer', 'infer',
'--no-filtering', '--no-filtering',

2
infer/tests/utils/InferRunner.java
Unescape View File

@ -471,7 +471,7 @@ public class InferRunner {
ProcessBuilder pb = new ProcessBuilder(inferCmd); ProcessBuilder pb = new ProcessBuilder(inferCmd);
Map<String, String> env = pb.environment(); Map<String, String> env = pb.environment();
env.put("REPORT_ASSERTION_FAILURE", "1"); env.put("INFER_REPORT_ASSERTION_FAILURE", "1");
Process process = pb.start(); Process process = pb.start();
StringBuilder stderr = new StringBuilder(); StringBuilder stderr = new StringBuilder();

Write Preview
Loading…
Cancel
Save