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

@@ -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"

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) ->

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

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
+    else exns in
-  and collect_errors pre errors (prop, path) =
+  let collect_spec errors spec =
-    match Tabulation.lookup_global_errors prop with
+    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
+    IList.fold_left (collect_errors spec.Specs.pre) errors spec.Specs.posts in
-    | 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_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)
+  if !Config.curr_language == Config.C_CPP && Config.report_custom_error then
-  || !Config.report_runtime_exceptions 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
 

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 =
+let desc_custom_error loc : error_desc =
-  (["could be raised"; at_line (Tags.create ()) loc], None, [])
+  (["detected"; at_line (Tags.create ()) loc], None, [])
 
 let desc_bad_pointer_comparison dexp_opt loc : error_desc =
   let dexp_str = match dexp_opt with

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

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 =
+let custom_error =
-  mk_pvar_global (Mangled.from_string "INFER_ERROR")
+  mk_pvar_global (Mangled.from_string "INFER_CUSTOM_ERROR")
 
 (* A block pvar used to explain retain cycles *)
 let block_pvar =

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

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

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
+    | Sil.Hpointsto (Sil.Lvar var, Sil.Eexp (Sil.Const (Sil.Cstr error_str), _), _) :: _
-      when Sil.pvar_equal var Sil.global_error -> Some (Mangled.from_string str)
+      when Sil.pvar_equal var Sil.custom_error -> Some error_str
     | _ :: tl -> search_error tl in
   search_error (Prop.get_sigma prop)
 

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

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

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',

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

infer/tests/codetoanalyze/c/errors/custom_error/Makefile

@@ -0,0 +1 @@
+../generic.mk

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 <math.h>
+
+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);
+}

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
+        )
+    );
+  }
+
+}

infer/tests/utils/InferRunner.java

@@ -525,7 +525,7 @@ public class InferRunner {
     ProcessBuilder pb = new ProcessBuilder(inferCmd);
 
     Map<String, String> 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();