diff --git a/infer/models/c/Makefile b/infer/models/c/Makefile index ff2e36841..4388bb371 100644 --- a/infer/models/c/Makefile +++ b/infer/models/c/Makefile @@ -5,7 +5,7 @@ LIBDIR = $(CWD)/../../lib LIB_SPECS = $(LIBDIR)/specs C_MODELS_FILE = $(LIB_SPECS)/c_models -INFER = ANALYZE_MODELS=1 $(BINDIR)/infer +INFER = INFER_ANALYZE_MODELS=1 $(BINDIR)/infer default: run_infer diff --git a/infer/models/cpp/Makefile b/infer/models/cpp/Makefile index 4521fb9cb..11bbde7da 100644 --- a/infer/models/cpp/Makefile +++ b/infer/models/cpp/Makefile @@ -5,7 +5,7 @@ LIBDIR = $(CWD)/../../lib LIB_SPECS = $(LIBDIR)/specs CPP_MODELS_FILE = $(LIB_SPECS)/cpp_models -INFER = ANALYZE_MODELS=1 $(BINDIR)/infer +INFER = INFER_ANALYZE_MODELS=1 $(BINDIR)/infer default: run_infer diff --git a/infer/models/java/Makefile b/infer/models/java/Makefile index d77df5edd..565e3e74e 100644 --- a/infer/models/java/Makefile +++ b/infer/models/java/Makefile @@ -2,7 +2,7 @@ SHELL := /bin/bash CWD = $(shell pwd) 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 JACKSON_JAR = ../../../dependencies/java/jackson/jackson-2.2.3.jar diff --git a/infer/models/objc/Makefile b/infer/models/objc/Makefile index 67f9b6daa..4db11c499 100644 --- a/infer/models/objc/Makefile +++ b/infer/models/objc/Makefile @@ -5,7 +5,7 @@ LIBDIR = $(CWD)/../../lib LIB_SPECS = $(LIBDIR)/specs OBJC_MODELS_FILE = $(LIB_SPECS)/objc_models -INFER = ANALYZE_MODELS=1 $(BINDIR)/infer +INFER = INFER_ANALYZE_MODELS=1 $(BINDIR)/infer default: run_infer diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 12bd138b4..e6e32ae22 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -344,9 +344,11 @@ let arc_mode = 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 analyze_models = from_env_variable "INFER_ANALYZE_MODELS" + module Experiment = struct (** if true, activate the subtyping routines in C++ as well, not just in Java *) diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 342cd0d38..c2134fec6 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -423,8 +423,7 @@ let symops_timeout, seconds_timeout = let default_seconds_timeout = 10 in let long_symops_timeout = 1000 in let long_seconds_timeout = 30 in - let analyzing_models = Config.from_env_variable "ANALYZE_MODELS" in - if analyzing_models then + if Config.analyze_models then (* use longer timeouts when analyzing models *) long_symops_timeout, long_seconds_timeout else diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index ad7e843de..c80c8d890 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -37,11 +37,10 @@ let print_usage_exit () = exit(1) let () = - let analysing_models = Config.from_env_variable "ANALYZE_MODELS" in 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"; - if not analysing_models && !JClasspath.models_jar = "" then + if not Config.analyze_models && !JClasspath.models_jar = "" then failwith "Java model file is required" diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index a28f5d958..f87f70805 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -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. *) let fix_method_definition_line linereader proc_name loc = let method_name = - let raw = Procname.java_get_method proc_name in - if raw = "" - then + if Procname.is_constructor proc_name then let inner_class_name cname = snd (string_split_character cname '$') in 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 method_is_defined_here linenum = match Printer.LineReader.from_file_linenum_original linereader loc.Sil.file linenum with @@ -528,7 +526,7 @@ let rec expression context pc expr = begin match binop with | 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 fresh_id, deref_array_instr = create_sil_deref sil_ex1 array_typ loc in let id = Ident.create_fresh Ident.knormal in @@ -574,19 +572,20 @@ let rec expression context pc expr = let callee_procdesc = match get_method_procdesc program cfg tenv cn JBasics.clinit_signature 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 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 else - if JTransType.is_autogenerated_assert_field field_name - then - (* assume that reading from C.$assertionsDisabled always yields "false". this allows *) - (* Infer to understand the assert keyword in the expected way *) - (idl, instrs, Sil.exp_zero) - else - let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in - let tmp_id = Ident.create_fresh Ident.knormal in - let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in - (idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id) + if JTransType.is_autogenerated_assert_field field_name + then + (* assume that reading from C.$assertionsDisabled always yields "false". this allows *) + (* Infer to understand the assert keyword in the expected way *) + (idl, instrs, Sil.exp_zero) + else + let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in + let tmp_id = Ident.create_fresh Ident.knormal in + let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in + (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 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 | I_Virtual -> true | _ -> 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 = match get_method_procdesc program cfg tenv cn ms is_static with | 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 | None -> ([], [], []) | Some (sil_obj_expr, sil_obj_type) -> - (* for non-constructors, add an instruction that dereferences the receiver *) - let ids, instrs = - let is_non_constructor_call = - match invoke_code with - | I_Special -> false - | _ -> true in - match sil_obj_expr with - | Sil.Var id when is_non_constructor_call && not !JConfig.translate_checks -> - let obj_typ_no_ptr = - match sil_obj_type with - | Sil.Tptr (typ, _) -> typ - | _ -> sil_obj_type in - let fresh_id, deref = create_sil_deref sil_obj_expr obj_typ_no_ptr loc in - [fresh_id], [deref] - | _ -> [], [] in - (ids, instrs, [(sil_obj_expr, sil_obj_type)]) in + (* for non-constructors, add an instruction that dereferences the receiver *) + let ids, instrs = + let is_non_constructor_call = + match invoke_code with + | I_Special -> false + | _ -> true in + match sil_obj_expr with + | Sil.Var id when is_non_constructor_call && not !JConfig.translate_checks -> + let obj_typ_no_ptr = + match sil_obj_type with + | Sil.Tptr (typ, _) -> typ + | _ -> sil_obj_type in + let fresh_id, deref = create_sil_deref sil_obj_expr obj_typ_no_ptr loc in + [fresh_id], [deref] + | _ -> [], [] in + (ids, instrs, [(sil_obj_expr, sil_obj_type)]) in let (idl, instrs, call_args) = list_fold_left (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 Procname.from_string (JBasics.ms_name ms) 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 return_type = Cfg.Procdesc.get_ret_type callee_procdesc in let call_ret_instrs sil_var = 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 (idl @ [ret_id], instrs @ [call_instr; set_instr]) in match var_opt with | 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]) | Some var -> 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) -> 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_np = - try - JTransType.get_class_type_no_pointer program tenv cn - with _ -> assert false in + let class_type_np = JTransType.get_class_type_no_pointer program tenv cn in let sizeof_exp = Sil.Sizeof (class_type_np, Sil.Subtype.exact) in let args = [(sizeof_exp, class_type)] 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 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 node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string constr_procname)) in let ids = ret_id :: call_ids 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 caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in 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 = match args with | [arg] when is_clone ms -> - (* 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 *) - let (ids, instrs, sil_arg_expr) = expression context pc arg in - let arg_typ = JTransType.expr_type context arg in - Some (sil_arg_expr, arg_typ), [], ids, instrs + (* 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 *) + let (ids, instrs, sil_arg_expr) = expression context pc arg in + let arg_typ = JTransType.expr_type context arg in + Some (sil_arg_expr, arg_typ), [], ids, instrs | _ -> None, args, [], [] in 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 @@ -1026,7 +1023,7 @@ let rec instruction context pc instr : translation = Instr call_node | 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 this_not_null_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_procdesc, constr_procname, call_ids, call_instrs) = 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 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 diff --git a/infer/src/java/jTransType.mli b/infer/src/java/jTransType.mli index 1804d4cfa..626965f21 100644 --- a/infer/src/java/jTransType.mli +++ b/infer/src/java/jTransType.mli @@ -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. *) 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 -(** [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 (** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *) diff --git a/infer/tests/codetoanalyze/c/errors/BUCK b/infer/tests/codetoanalyze/c/errors/BUCK index 83f999092..3362eb5df 100644 --- a/infer/tests/codetoanalyze/c/errors/BUCK +++ b/infer/tests/codetoanalyze/c/errors/BUCK @@ -4,7 +4,7 @@ sources += glob(['**/Makefile']) out = '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', '--no-filtering', diff --git a/infer/tests/utils/InferRunner.java b/infer/tests/utils/InferRunner.java index cf08842d4..8b3018c54 100644 --- a/infer/tests/utils/InferRunner.java +++ b/infer/tests/utils/InferRunner.java @@ -471,7 +471,7 @@ public class InferRunner { ProcessBuilder pb = new ProcessBuilder(inferCmd); Map env = pb.environment(); - env.put("REPORT_ASSERTION_FAILURE", "1"); + env.put("INFER_REPORT_ASSERTION_FAILURE", "1"); Process process = pb.start(); StringBuilder stderr = new StringBuilder();