[infer][biabduction] remove the flag to trigger on/off the angelic mode in the backend

Reviewed By: sblackshear

Differential Revision: D5819488

fbshipit-source-id: 0095ec8

infer/src/backend/BuiltinDefn.ml

@@ -145,9 +145,7 @@ let execute___print_value {Builtin.tenv; pdesc; prop_; path; args} : Builtin.ret
   in
   List.iter ~f:do_arg args ; L.(debug Analysis Medium) "@." ; [(prop_, path)]
 
-let is_undefined_opt tenv prop n_lexp =
+let is_undefined_opt tenv prop n_lexp = Option.is_some (Attribute.get_undef tenv prop n_lexp)
-  let is_undef = Option.is_some (Attribute.get_undef tenv prop n_lexp) in
-  is_undef && Config.angelic_execution
 
 (** Creates an object in the heap with a given type, when the object is not known to be null or when
     it doesn't appear already in the heap. *)

infer/src/backend/PropUtil.ml

@@ -143,7 +143,7 @@ let remove_locals tenv (curr_f: Procdesc.t) p =
      -> names_of_locals
   in
   let removed, p' = Attribute.deallocate_stack_vars tenv p names_of_locals' in
-  (removed, if Config.angelic_execution then remove_abduced_retvars tenv p' else p')
+  (removed, remove_abduced_retvars tenv p')
 
 let remove_formals tenv (curr_f: Procdesc.t) p =
   let pname = Procdesc.get_proc_name curr_f in

infer/src/backend/prop.ml

@@ -1605,14 +1605,6 @@ module Normalize = struct
       let fav = pi_fav npi in
       sigma_fav_add fav nsigma ; fav
     in
-    (* TODO (t4893479): make this check less angelic *)
-    if Sil.fav_exists fp_vars Ident.is_normal && not Config.angelic_execution then (
-      L.d_strln "footprint part contains normal variables" ;
-      d_pi npi ;
-      L.d_ln () ;
-      d_sigma nsigma ;
-      L.d_ln () ;
-      assert false ) ;
     Sil.fav_filter_ident fp_vars Ident.is_primed ;
     (* only keep primed vars *)
     let npi', nsigma' =

infer/src/backend/rearrange.ml

@@ -449,7 +449,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst
   if not (exp_has_only_footprint_ids root) then
     if (* in angelic mode, purposely ignore dangling pointer warnings during the footprint phase -- we
      * will fix them during the re - execution phase *)
-       not (Config.angelic_execution && !Config.footprint)
+       not !Config.footprint
     then (
       L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ;
       let deref_str = Localise.deref_str_dangling None in
@@ -1589,12 +1589,8 @@ let check_dereference_error tenv pdesc (prop: Prop.normal Prop.t) lexp loc =
    -> let deref_str = Localise.deref_str_dangling (Some dk) in
       let err_desc = Errdesc.explain_dereference tenv deref_str prop (State.get_loc ()) in
       raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__))
-  | Some Apred (Aundef (s, _, undef_loc, _), _)
+  | Some Apred (Aundef _, _)
-   -> if Config.angelic_execution then ()
+   -> ()
-      else
-        let deref_str = Localise.deref_str_undef (s, undef_loc) in
-        let err_desc = Errdesc.explain_dereference tenv deref_str prop loc in
-        raise (Exceptions.Skip_pointer_dereference (err_desc, __POS__))
   | Some Apred (Aresource ({ra_kind= Rrelease} as ra), _)
    -> let deref_str = Localise.deref_str_freed ra in
       let err_desc = Errdesc.explain_dereference tenv ~use_buckets:true deref_str prop loc in

infer/src/backend/symExec.ml

@@ -402,8 +402,8 @@ let reason_to_skip callee_summary : string option =
   let attributes = callee_summary.Specs.attributes in
   if attributes.ProcAttributes.is_abstract then Some "abstract method"
   else if not attributes.ProcAttributes.is_defined then Some "method has no implementation"
-  else if Config.angelic_execution && List.is_empty (Specs.get_specs_from_payload callee_summary)
+  else if List.is_empty (Specs.get_specs_from_payload callee_summary) then
-  then Some "empty list of specs"
+    Some "empty list of specs"
   else None
 
 (** In case of constant string dereference, return the result immediately *)
@@ -945,7 +945,7 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca
       else
         match typ.Typ.desc with Typ.Tptr _ -> Prop.conjoin_neq tenv exp Exp.zero prop | _ -> prop
     in
-    if Config.angelic_execution && not (is_rec_call callee_pname) then
+    if not (is_rec_call callee_pname) then
       (* introduce a fresh program variable to allow abduction on the return value *)
       let prop_with_abduced_var =
         let abduced_ret_pv =
@@ -1413,16 +1413,6 @@ and instrs ?(mask_errors= false) tenv pdesc instrs ppl =
   List.fold ~f ~init:ppl instrs
 
 and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname callee_loc =
-  (* replace an hpred of the form actual_var |-> _ with new_hpred in prop *)
-  let replace_actual_hpred actual_var new_hpred prop =
-    let sigma' =
-      List.map
-        ~f:(function
-            | Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual_var -> new_hpred | hpred -> hpred)
-        prop.Prop.sigma
-    in
-    Prop.normalize tenv (Prop.set prop ~sigma:sigma')
-  in
   let add_actual_by_ref_to_footprint prop (actual, actual_typ, actual_index) =
     let abduced =
       match actual with
@@ -1489,24 +1479,6 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
            -> p)
         ~init:prop' prop'.Prop.sigma
   in
-  (* non-angelic mode; havoc each var passed by reference by assigning it to a fresh id *)
-  let havoc_actual_by_ref prop (actual, actual_typ, _) =
-    let actual_pt_havocd_var =
-      let havocd_var = Exp.Var (Ident.create_fresh Ident.kprimed) in
-      let sizeof_exp =
-        Exp.Sizeof
-          { typ= Typ.strip_ptr actual_typ
-          ; nbytes= None
-          ; dynamic_length= None
-          ; subtype= Subtype.subtypes }
-      in
-      Prop.mk_ptsto tenv actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp
-    in
-    replace_actual_hpred actual actual_pt_havocd_var prop
-  in
-  let do_actual_by_ref =
-    if Config.angelic_execution then add_actual_by_ref_to_footprint else havoc_actual_by_ref
-  in
   let non_const_actuals_by_ref =
     let is_not_const (e, _, i) =
       match AttributesTable.load_attributes ~cache:true callee_pname with
@@ -1522,7 +1494,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
     in
     List.filter ~f:is_not_const actuals_by_ref
   in
-  List.fold ~f:do_actual_by_ref ~init:prop non_const_actuals_by_ref
+  List.fold ~f:add_actual_by_ref_to_footprint ~init:prop non_const_actuals_by_ref
 
 (** execute a call for an unknown or scan function *)
 and unknown_or_scan_call ~is_scan ~reason ret_type_option ret_annots

infer/src/backend/tabulation.ml

@@ -348,14 +348,13 @@ let check_dereferences tenv callee_pname actual_pre sub spec_pre formal_params =
   match deref_err_list with
   | []
    -> None
-  | deref_err :: _
+  | deref_err :: _ ->
-   -> if Config.angelic_execution then
+    match
-        (* In angelic mode, prefer to report Deref_null over other kinds of deref errors. this
+      (* Prefer to report Deref_null over other kinds of deref errors. this
          * makes sure we report a NULL_DEREFERENCE instead of
            a less interesting PRECONDITION_NOT_MET
          * whenever possible *)
       (* TOOD (t4893533): use this trick outside of angelic mode and in other parts of the code *)
-        match
       List.find
         ~f:(fun err -> match err with Deref_null _, _ -> true | _ -> false)
         deref_err_list
@@ -364,7 +363,6 @@ let check_dereferences tenv callee_pname actual_pre sub spec_pre formal_params =
      -> Some x
     | None
      -> Some deref_err
-      else Some deref_err
 
 let post_process_sigma tenv (sigma: Sil.hpred list) loc : Sil.hpred list =
   let map_inst inst = Sil.inst_new_loc loc inst in
@@ -622,17 +620,8 @@ let prop_footprint_add_pi_sigma_starfld_sigma tenv (prop: 'a Prop.t) pi_new sigm
     | []
      -> Some current_sigma
     | hpred :: new_sigma'
-     -> let fav = Prop.sigma_fav [hpred] in
+     -> (* TODO (t4893479): make this check less angelic *)
-        (* TODO (t4893479): make this check less angelic *)
+        extend_sigma (hpred :: current_sigma) new_sigma'
-        if Sil.fav_exists fav (fun id ->
-               not (Ident.is_footprint id) && not Config.angelic_execution )
-        then (
-          L.d_warning "found hpred with non-footprint variable, dropping the spec" ;
-          L.d_ln () ;
-          Sil.d_hpred hpred ;
-          L.d_ln () ;
-          None )
-        else extend_sigma (hpred :: current_sigma) new_sigma'
   in
   let rec extend_pi current_pi new_pi =
     match new_pi with
@@ -1068,7 +1057,7 @@ let exe_spec tenv ret_id_opt (n, nspecs) caller_pdesc callee_pname loc prop path
       List.iter ~f:log_check_exn checks ;
       let subbed_pre = Prop.prop_sub (`Exp sub1) actual_pre in
       match check_dereferences tenv callee_pname subbed_pre (`Exp sub2) spec_pre formal_params with
-      | Some (Deref_undef _, _) when Config.angelic_execution
+      | Some (Deref_undef _, _)
        -> let split = do_split () in
           report_valid_res split
       | Some (deref_error, desc)

infer/src/base/Config.ml

@@ -587,10 +587,6 @@ and android_harness =
   CLOpt.mk_bool ~deprecated:["harness"] ~long:"android-harness"
     "(Experimental) Create harness to detect issues involving the Android lifecycle"
 
-and angelic_execution =
-  CLOpt.mk_bool ~deprecated:["angelic_execution"] ~long:"angelic-execution" ~default:true
-    "Angelic execution, where the analysis ignores errors caused by unknown procedure calls"
-
 and ( annotation_reachability
     , biabduction
     , bufferoverrun
@@ -1942,8 +1938,6 @@ and analysis_suppress_errors_options =
 
 and analysis_stops = !analysis_stops
 
-and angelic_execution = !angelic_execution
-
 and annotation_reachability = !annotation_reachability
 
 and annotation_reachability_custom_pairs = !annotation_reachability_custom_pairs

infer/src/base/Config.mli

@@ -273,8 +273,6 @@ val analysis_suppress_errors : analyzer -> string list
 
 val analyzer : analyzer
 
-val angelic_execution : bool
-
 val annotation_reachability : bool
 
 val annotation_reachability_custom_pairs : Yojson.Basic.json