From 6d91199be7dab5c70d7ba874e776dee8c95e8b7d Mon Sep 17 00:00:00 2001 From: jrm Date: Mon, 4 Jan 2016 14:18:50 -0800 Subject: [PATCH] Generalize the detection of assertion failures to any kind of custom errors defined programatically in the orginal source code Summary: public This diff cleans up the detection of assertion failures in C, C++ and Objective C which was previously hacked on top of the tracing mode for Java. The code is also generalized to detect any custom errors which can be defined using the `__infer_fail` builtin, and the case of assertion failure is now just the specific case of translating `assert` using `__infer_fail` directly in the clang frontend. Reviewed By: jberdine Differential Revision: D2786574 fb-gh-sync-id: dd1e1cf --- infer/src/backend/config.ml | 2 +- infer/src/backend/exceptions.ml | 6 +- infer/src/backend/exceptions.mli | 2 +- infer/src/backend/interproc.ml | 58 +++++++++++++------ infer/src/backend/localise.ml | 4 +- infer/src/backend/localise.mli | 3 +- infer/src/backend/sil.ml | 4 +- infer/src/backend/sil.mli | 2 +- infer/src/backend/symExec.ml | 4 +- infer/src/backend/tabulation.ml | 6 +- infer/src/backend/tabulation.mli | 2 +- infer/src/clang/cTrans.ml | 4 +- infer/tests/codetoanalyze/c/errors/BUCK | 2 +- infer/tests/codetoanalyze/c/errors/Makefile | 2 + .../c/errors/custom_error/Makefile | 1 + .../c/errors/custom_error/custom.c | 42 ++++++++++++++ infer/tests/endtoend/c/CustomErrorTest.java | 55 ++++++++++++++++++ infer/tests/utils/InferRunner.java | 2 +- 18 files changed, 160 insertions(+), 41 deletions(-) create mode 120000 infer/tests/codetoanalyze/c/errors/custom_error/Makefile create mode 100644 infer/tests/codetoanalyze/c/errors/custom_error/custom.c create mode 100644 infer/tests/endtoend/c/CustomErrorTest.java diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 2ba6db400..127a4f781 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -355,7 +355,7 @@ let arc_mode = ref false let objc_memory_model_on = ref false -let report_assertion_failure = from_env_variable "INFER_REPORT_ASSERTION_FAILURE" +let report_custom_error = from_env_variable "INFER_REPORT_CUSTOM_ERROR" let default_failure_name = "ASSERTION_FAILURE" let analyze_models = from_env_variable "INFER_ANALYZE_MODELS" diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index 3700e9e65..5274a0367 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -35,7 +35,6 @@ exception Array_out_of_bounds_l1 of Localise.error_desc * ml_location exception Array_out_of_bounds_l2 of Localise.error_desc * ml_location exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location exception Array_of_pointsto of ml_location -exception Assertion_failure of string * Localise.error_desc exception Bad_footprint of ml_location exception Bad_pointer_comparison of Localise.error_desc * ml_location exception Class_cast_exception of Localise.error_desc * ml_location @@ -44,6 +43,7 @@ exception Comparing_floats_for_equality of Localise.error_desc * ml_location exception Condition_is_assignment of Localise.error_desc * ml_location exception Condition_always_true_false of Localise.error_desc * bool * ml_location exception Context_leak of Localise.error_desc * ml_location +exception Custom_error of string * Localise.error_desc exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_location exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc @@ -105,8 +105,6 @@ let recognize_exception exn = (Localise.array_out_of_bounds_l3, desc, Some mloc, Exn_developer, Medium, None, Nocat) | Assert_failure mloc -> (Localise.from_string "Assert_failure", Localise.no_desc, Some mloc, Exn_developer, High, None, Nocat) - | Assertion_failure (error_msg, desc) -> - (Localise.from_string error_msg, desc, None, Exn_user, High, None, Checker) | Bad_pointer_comparison (desc, mloc) -> (Localise.bad_pointer_comparison, desc, Some mloc, Exn_user, High, Some Kerror, Prover) | Bad_footprint mloc -> @@ -122,6 +120,8 @@ let recognize_exception exn = | Condition_always_true_false (desc, b, mloc) -> let name = if b then Localise.condition_always_true else Localise.condition_always_false in (name, desc, Some mloc, Exn_user, Medium, None, Nocat) + | Custom_error (error_msg, desc) -> + (Localise.from_string error_msg, desc, None, Exn_user, High, None, Checker) | Condition_is_assignment(desc, mloc) -> (Localise.condition_is_assignment, desc, Some mloc, Exn_user, Medium, None, Nocat) | Dangling_pointer_dereference (dko, desc, mloc) -> diff --git a/infer/src/backend/exceptions.mli b/infer/src/backend/exceptions.mli index a4f6caced..6c926fcc9 100644 --- a/infer/src/backend/exceptions.mli +++ b/infer/src/backend/exceptions.mli @@ -35,7 +35,6 @@ exception Array_of_pointsto of ml_location exception Array_out_of_bounds_l1 of Localise.error_desc * ml_location exception Array_out_of_bounds_l2 of Localise.error_desc * ml_location exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location -exception Assertion_failure of string * Localise.error_desc exception Bad_footprint of ml_location exception Bad_pointer_comparison of Localise.error_desc * ml_location exception Class_cast_exception of Localise.error_desc * ml_location @@ -44,6 +43,7 @@ exception Comparing_floats_for_equality of Localise.error_desc * ml_location exception Condition_always_true_false of Localise.error_desc * bool * ml_location exception Condition_is_assignment of Localise.error_desc * ml_location exception Context_leak of Localise.error_desc * ml_location +exception Custom_error of string * Localise.error_desc exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_location exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 86984ba53..710dedfda 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1012,32 +1012,35 @@ let reset_global_counters cfg proc_name proc_desc = Abs.abs_rules_reset (); set_current_language cfg proc_desc -(* Collect all pairs of the kind (precondition, exception) from a summary *) +(* Collect all pairs of the kind (precondition, runtime exception) from a summary *) let exception_preconditions tenv pname summary = - let collect_exceptions pre exns (prop, path) = + let collect_exceptions pre exns (prop, _) = if Tabulation.prop_is_exn pname prop then let exn_name = Tabulation.prop_get_exn_name pname prop in if AndroidFramework.is_runtime_exception tenv exn_name then (pre, exn_name):: exns else exns - else exns - and collect_errors pre errors (prop, path) = - match Tabulation.lookup_global_errors prop with + else exns in + let collect_spec errors spec = + IList.fold_left (collect_exceptions spec.Specs.pre) errors spec.Specs.posts in + IList.fold_left collect_spec [] (Specs.get_specs_from_payload summary) + +(* Collect all pairs of the kind (precondition, custom error) from a summary *) +let custom_error_preconditions tenv pname summary = + let collect_errors pre errors (prop, _) = + match Tabulation.lookup_custom_errors prop with | None -> errors | Some e -> (pre, e) :: errors in let collect_spec errors spec = - match !Config.curr_language with - | Config.Java -> - IList.fold_left (collect_exceptions spec.Specs.pre) errors spec.Specs.posts - | Config.C_CPP -> - IList.fold_left (collect_errors spec.Specs.pre) errors spec.Specs.posts in + IList.fold_left (collect_errors spec.Specs.pre) errors spec.Specs.posts in IList.fold_left collect_spec [] (Specs.get_specs_from_payload summary) (* Remove the constrain of the form this != null which is true for all Java virtual calls *) let remove_this_not_null prop = let collect_hpred (var_option, hpreds) = function - | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (Sil.Var var, _), _) when Sil.pvar_is_this pvar -> + | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (Sil.Var var, _), _) + when !Config.curr_language = Config.Java && Sil.pvar_is_this pvar -> (Some var, hpreds) | hpred -> (var_option, hpred:: hpreds) in let collect_atom var atoms = function @@ -1054,6 +1057,17 @@ let remove_this_not_null prop = Prop.normalize prop'' +(** Is true when the precondition does not contain constrains that can be false at call site. + This means that the post-conditions associated with this precondition cannot be prevented + by the calling context. *) +let is_unavoidable pre = + let prop = remove_this_not_null (Specs.Jprop.to_prop pre) in + match Prop.CategorizePreconditions.categorize [prop] with + | Prop.CategorizePreconditions.NoPres + | Prop.CategorizePreconditions.Empty -> true + | _ -> false + + (** Detects if there are specs of the form {precondition} proc {runtime exception} and report an error in that case, generating the trace that lead to the runtime exception if the method is called in the context { precondition } *) @@ -1071,12 +1085,6 @@ let report_runtime_exceptions tenv cfg pdesc summary = let annotated_signature = Annotations.get_annotated_signature proc_attributes in let ret_annotation, _ = annotated_signature.Annotations.ret in Annotations.ia_is_verify ret_annotation in - let is_unavoidable pre = - let prop = remove_this_not_null (Specs.Jprop.to_prop pre) in - match Prop.CategorizePreconditions.categorize [prop] with - | Prop.CategorizePreconditions.NoPres - | Prop.CategorizePreconditions.Empty -> true - | _ -> false in let should_report pre = is_main || is_annotated || is_unavoidable pre in let report (pre, runtime_exception) = @@ -1089,6 +1097,17 @@ let report_runtime_exceptions tenv cfg pdesc summary = IList.iter report (exception_preconditions tenv pname summary) +let report_custom_errors tenv cfg pdesc summary = + let pname = Specs.get_proc_name summary in + let report (pre, custom_error) = + if is_unavoidable pre then + let loc = summary.Specs.attributes.ProcAttributes.loc in + let err_desc = Localise.desc_custom_error loc in + let exn = Exceptions.Custom_error (custom_error, err_desc) in + Reporting.log_error pname ~pre: (Some (Specs.Jprop.to_prop pre)) exn in + IList.iter report (custom_error_preconditions tenv pname summary) + + (** update a summary after analysing a procedure *) let update_summary prev_summary specs proc_name elapsed res = let normal_specs = IList.map Specs.spec_normalize specs in @@ -1133,8 +1152,9 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary = let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in let updated_summary = update_summary prev_summary specs proc_name elapsed res in - if (!Config.curr_language <> Config.Java && Config.report_assertion_failure) - || !Config.report_runtime_exceptions then + if !Config.curr_language == Config.C_CPP && Config.report_custom_error then + report_custom_errors tenv cfg proc_desc updated_summary; + if !Config.curr_language == Config.Java && !Config.report_runtime_exceptions then report_runtime_exceptions tenv cfg proc_desc updated_summary; updated_summary diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 2a751d952..caf43d845 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -387,8 +387,8 @@ let desc_context_leak pname context_typ fieldname leak_path : error_desc = "Context " ^ context_str ^ "may leak during method " ^ pname_str ^ ":\n" in ([preamble; leak_root; path_str], None, []) -let desc_assertion_failure loc : error_desc = - (["could be raised"; at_line (Tags.create ()) loc], None, []) +let desc_custom_error loc : error_desc = + (["detected"; at_line (Tags.create ()) loc], None, []) let desc_bad_pointer_comparison dexp_opt loc : error_desc = let dexp_str = match dexp_opt with diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index b80376e14..5447b9842 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -201,10 +201,9 @@ val desc_context_leak : Procname.t -> Sil.typ -> Ident.fieldname -> (Ident.fieldname option * Sil.typ) list -> error_desc (* Create human-readable error description for assertion failures *) -val desc_assertion_failure : Location.t -> error_desc +val desc_custom_error : Location.t -> error_desc val desc_bad_pointer_comparison : Sil.dexp option -> Location.t -> error_desc - (** kind of precondition not met *) type pnm_kind = | Pnm_bounds diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 777f6a3c7..c1ef029ef 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -3906,8 +3906,8 @@ let rec strexp_get_target_exps = function (* We ignore size and indices since they are not quite outgoing arrows. *) IList.flatten (IList.map (fun (_, se) -> strexp_get_target_exps se) esel) -let global_error = - mk_pvar_global (Mangled.from_string "INFER_ERROR") +let custom_error = + mk_pvar_global (Mangled.from_string "INFER_CUSTOM_ERROR") (* A block pvar used to explain retain cycles *) let block_pvar = diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 0f03fe10f..fcada999f 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -1312,4 +1312,4 @@ val exp_iter_types : (typ -> unit) -> exp -> unit (** Iterate over all the types (and subtypes) in the instruction *) val instr_iter_types : (typ -> unit) -> instr -> unit -val global_error : pvar +val custom_error : pvar diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 889c4038d..7e1658210 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -2367,7 +2367,7 @@ module ModelBuiltins = struct | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in let set_instr = - Sil.Set (Sil.Lvar Sil.global_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in + Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)] (* translate builtin assertion failure *) @@ -2380,7 +2380,7 @@ module ModelBuiltins = struct | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in let set_instr = - Sil.Set (Sil.Lvar Sil.global_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in + Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)] let _ = Builtin.register "__method_set_ignore_attribute" execute___method_set_ignore_attribute diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 86eb4e342..366aa8989 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -611,11 +611,11 @@ let prop_get_exn_name pname prop = !exn_name (** search in prop for some assignment of global errors *) -let lookup_global_errors prop = +let lookup_custom_errors prop = let rec search_error = function | [] -> None - | Sil.Hpointsto (Sil.Lvar var, Sil.Eexp (Sil.Const (Sil.Cstr str), _), _) :: tl - when Sil.pvar_equal var Sil.global_error -> Some (Mangled.from_string str) + | Sil.Hpointsto (Sil.Lvar var, Sil.Eexp (Sil.Const (Sil.Cstr error_str), _), _) :: _ + when Sil.pvar_equal var Sil.custom_error -> Some error_str | _ :: tl -> search_error tl in search_error (Prop.get_sigma prop) diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 17dec4d73..a52477059 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -33,7 +33,7 @@ val prop_is_exn : Procname.t -> 'a Prop.t -> bool val prop_get_exn_name : Procname.t -> 'a Prop.t -> Mangled.t (** search in prop contains an error state *) -val lookup_global_errors : 'a Prop.t -> Mangled.t option +val lookup_custom_errors : 'a Prop.t -> string option (** Dump a splitting *) val d_splitting : splitting -> unit diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index b0e870171..e124f2b7c 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -657,7 +657,7 @@ struct res_trans_callee :: res_trans_p in let sil_fe, is_cf_retain_release = CTrans_models.builtin_predefined_model fun_exp_stmt sil_fe in if CTrans_models.is_assert_log sil_fe then - if Config.report_assertion_failure then + if Config.report_custom_error then CTrans_utils.trans_assertion_failure sil_loc context else CTrans_utils.trans_assume_false sil_loc context trans_state.succ_nodes @@ -794,7 +794,7 @@ struct | _ -> None (* assertions *) else if CTrans_models.is_handleFailureInMethod selector then - if Config.report_assertion_failure then + if Config.report_custom_error then Some (CTrans_utils.trans_assertion_failure sil_loc context) else Some (CTrans_utils.trans_assume_false sil_loc context trans_state.succ_nodes) else None diff --git a/infer/tests/codetoanalyze/c/errors/BUCK b/infer/tests/codetoanalyze/c/errors/BUCK index a542108dc..901c8a3dd 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', 'INFER_REPORT_ASSERTION_FAILURE=1']) +env_cmd = ' '.join(['export', 'INFER_REPORT_CUSTOM_ERROR=1']) infer_cmd = ' '.join([ 'infer', '--no-progress-bar', diff --git a/infer/tests/codetoanalyze/c/errors/Makefile b/infer/tests/codetoanalyze/c/errors/Makefile index dcb6924bb..5987f4b87 100644 --- a/infer/tests/codetoanalyze/c/errors/Makefile +++ b/infer/tests/codetoanalyze/c/errors/Makefile @@ -3,6 +3,7 @@ all: make -C arithmetic make -C assertions make -C attributes + make -C custom_error make -C initialization make -C local_vars make -C null_dereference @@ -14,6 +15,7 @@ all: clean: make -C arithmetic clean make -C assertions clean + make -C custom_error clean make -C attributes clean make -C initialization clean make -C local_vars clean diff --git a/infer/tests/codetoanalyze/c/errors/custom_error/Makefile b/infer/tests/codetoanalyze/c/errors/custom_error/Makefile new file mode 120000 index 000000000..67091171e --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/custom_error/Makefile @@ -0,0 +1 @@ +../generic.mk \ No newline at end of file diff --git a/infer/tests/codetoanalyze/c/errors/custom_error/custom.c b/infer/tests/codetoanalyze/c/errors/custom_error/custom.c new file mode 100644 index 000000000..526e18f5c --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/custom_error/custom.c @@ -0,0 +1,42 @@ +/* + * Copyright (c) 2015 - 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. + */ + +#import + +void __infer_fail(char*); + +void check_exponent(int x) { + if (x < 0) __infer_fail("UNEXPECTED_NEGATIVE_EXPONENT"); +} + +int power(int x) { + check_exponent(x); + return pow(2, x); +} + +int pif() { + int a = 3; + return power(a); +} + +int paf() { + int a = -3; + return power(a); +} + +int global; + +void set_global() { + global = -2; +} + +int pouf() { + set_global(); + return power(global); +} diff --git a/infer/tests/endtoend/c/CustomErrorTest.java b/infer/tests/endtoend/c/CustomErrorTest.java new file mode 100644 index 000000000..9b8b05b04 --- /dev/null +++ b/infer/tests/endtoend/c/CustomErrorTest.java @@ -0,0 +1,55 @@ +/* + * Copyright (c) 2015 - 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. + */ + +package endtoend.c; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +import org.junit.BeforeClass; +import org.junit.Test; + +import java.io.IOException; + +import utils.InferException; +import utils.InferResults; + +public class CustomErrorTest { + + public static final String SOURCE_FILE = + "custom_error/custom.c"; + + public static final String CUSTOM_ERROR = "UNEXPECTED_NEGATIVE_EXPONENT"; + + private static InferResults inferResults; + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferResults = InferResults.loadCInferResults(CustomErrorTest.class, SOURCE_FILE); + } + + @Test + public void whenRunsOnAssertionFailureThenAssertionFailureIsFound() + throws InterruptedException, IOException, InferException { + String[] methods = { + "paf", + "pouf", + }; + assertThat( + "Results should contain " + CUSTOM_ERROR, + inferResults, + containsExactly( + CUSTOM_ERROR, + SOURCE_FILE, + methods + ) + ); + } + +} diff --git a/infer/tests/utils/InferRunner.java b/infer/tests/utils/InferRunner.java index 06a8a7782..4595428e0 100644 --- a/infer/tests/utils/InferRunner.java +++ b/infer/tests/utils/InferRunner.java @@ -525,7 +525,7 @@ public class InferRunner { ProcessBuilder pb = new ProcessBuilder(inferCmd); Map env = pb.environment(); - env.put("INFER_REPORT_ASSERTION_FAILURE", "1"); + env.put("INFER_REPORT_CUSTOM_ERROR", "1"); Process process = pb.start(); StringBuilder stderr = new StringBuilder();