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

Move biabduction config/state to its own module

Browse Source 
Reviewed By: jeremydubreil

Differential Revision: D9754963

fbshipit-source-id: cc44998e6
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 247e785ae4
commit bc737851b1
19 changed files with 222 additions and 169 deletions
Show Stats Download Patch File Download Diff File

18
infer/src/IR/Sil.ml
Unescape View File

@ -1037,24 +1037,6 @@ let hpred_gen_free_vars =
let hpred_free_vars h = Sequence.Generator.run (hpred_gen_free_vars h) let hpred_free_vars h = Sequence.Generator.run (hpred_gen_free_vars h)
(** This function should be used before adding a new index to Earray. The [exp] is the newly created
index. This function "cleans" [exp] according to whether it is the footprint or current part of
the prop. The function faults in the re - execution mode, as an internal check of the tool. *)
let array_clean_new_index footprint_part new_idx =
assert (not (footprint_part && not !Config.footprint)) ;
if
footprint_part
&& Exp.free_vars new_idx |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id))
then (
L.d_warning
( "Array index " ^ Exp.to_string new_idx
^ " has non-footprint vars: replaced by fresh footprint var" ) ;
L.d_ln () ;
let id = Ident.create_fresh Ident.kfootprint in
Exp.Var id )
else new_idx
(** {2 Functions for computing all free or bound non-program variables} *) (** {2 Functions for computing all free or bound non-program variables} *)
(** Variables in hpara, excluding bound vars in the body *) (** Variables in hpara, excluding bound vars in the body *)

7
infer/src/IR/Sil.mli
Unescape View File

@ -347,13 +347,6 @@ val pp_hpred_env : Pp.env -> Predicates.env option -> F.formatter -> hpred -> un
(** {2 Functions for traversing SIL data types} *) (** {2 Functions for traversing SIL data types} *)
val array_clean_new_index : bool -> Exp.t -> Exp.t
(** This function should be used before adding a new
index to Earray. The [exp] is the newly created
index. This function "cleans" [exp] according to whether it is the
footprint or current part of the prop.
The function faults in the re - execution mode, as an internal check of the tool. *)
val strexp_expmap : (Exp.t * inst option -> Exp.t * inst option) -> strexp -> strexp val strexp_expmap : (Exp.t * inst option -> Exp.t * inst option) -> strexp -> strexp
(** Change exps in strexp using [f]. (** Change exps in strexp using [f].
WARNING: the result might not be normalized. *) WARNING: the result might not be normalized. *)

8
infer/src/backend/ondemand.ml
Unescape View File

@ -92,10 +92,10 @@ type global_state =
let save_global_state () = let save_global_state () =
Timeout.suspend_existing_timeout ~keep_symop_total:false ; Timeout.suspend_existing_timeout ~keep_symop_total:false ;
(* use a new global counter for the callee *) (* use a new global counter for the callee *)
{ abs_val= !Config.abs_val { abs_val= !BiabductionConfig.abs_val
; abstraction_rules= Abs.get_current_rules () ; abstraction_rules= Abs.get_current_rules ()
; delayed_prints= L.get_delayed_prints () ; delayed_prints= L.get_delayed_prints ()
; footprint_mode= !Config.footprint ; footprint_mode= !BiabductionConfig.footprint
; html_formatter= !Printer.curr_html_formatter ; html_formatter= !Printer.curr_html_formatter
; name_generator= Ident.NameGenerator.get_current () ; name_generator= Ident.NameGenerator.get_current ()
; proc_analysis_time= ; proc_analysis_time=
@ -105,10 +105,10 @@ let save_global_state () =
let restore_global_state st = let restore_global_state st =
Config.abs_val := st.abs_val ; BiabductionConfig.abs_val := st.abs_val ;
Abs.set_current_rules st.abstraction_rules ; Abs.set_current_rules st.abstraction_rules ;
L.set_delayed_prints st.delayed_prints ; L.set_delayed_prints st.delayed_prints ;
Config.footprint := st.footprint_mode ; BiabductionConfig.footprint := st.footprint_mode ;
Printer.curr_html_formatter := st.html_formatter ; Printer.curr_html_formatter := st.html_formatter ;
Ident.NameGenerator.set_current st.name_generator ; Ident.NameGenerator.set_current st.name_generator ;
State.restore_state st.symexec_state ; State.restore_state st.symexec_state ;

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

@ -50,7 +50,7 @@ let log_issue_from_summary severity summary ~node ~session ~loc ~ltr ?extras exn
let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn = let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn =
if !Config.footprint then if !BiabductionConfig.footprint then
match Summary.get proc_name with match Summary.get proc_name with
| Some summary -> | Some summary ->
let node = let node =
@ -85,7 +85,7 @@ let log_issue_external procname severity ~loc ~ltr ?access issue_type error_mess
let log_error_using_state summary exn = let log_error_using_state summary exn =
if !Config.footprint then if !BiabductionConfig.footprint then
let node = Errlog.BackendNode {node= State.get_node_exn ()} in let node = Errlog.BackendNode {node= State.get_node_exn ()} in
let session = State.get_session () in let session = State.get_session () in
let loc = State.get_loc_exn () in let loc = State.get_loc_exn () in

27
infer/src/base/Config.ml
Unescape View File

@ -2463,7 +2463,9 @@ and rest = !rest
and abs_struct = !abs_struct and abs_struct = !abs_struct
and abs_val_orig = !abs_val and abs_val = !abs_val
and allow_leak = !allow_leak
and analysis_path_regex_whitelist_options = and analysis_path_regex_whitelist_options =
List.map ~f:(fun (a, b) -> (a, !b)) analysis_path_regex_whitelist_options List.map ~f:(fun (a, b) -> (a, !b)) analysis_path_regex_whitelist_options
@ -3010,29 +3012,6 @@ let dynamic_dispatch = !dynamic_dispatch
let specs_library = !specs_library let specs_library = !specs_library
(** Global variables *)
let set_reference_and_call_function reference value f x =
let saved = !reference in
let restore () = reference := saved in
Utils.try_finally_swallow_timeout
~f:(fun () ->
reference := value ;
f x )
~finally:restore
(** Flag for footprint discovery mode *)
let footprint = ref true
let run_in_footprint_mode f x = set_reference_and_call_function footprint true f x
let run_in_re_execution_mode f x = set_reference_and_call_function footprint false f x
let reset_abs_val () = abs_val := abs_val_orig
let run_with_abs_val_equal_zero f x = set_reference_and_call_function abs_val 0 f x
(** Check if a Java package is external to the repository *) (** Check if a Java package is external to the repository *)
let java_package_is_external package = let java_package_is_external package =
match external_java_packages with match external_java_packages with

26
infer/src/base/Config.mli
Unescape View File

@ -216,6 +216,10 @@ val rest : string list
val abs_struct : int val abs_struct : int
val abs_val : int
val allow_leak : bool
val analysis_path_regex_whitelist : analyzer -> string list val analysis_path_regex_whitelist : analyzer -> string list
val analysis_path_regex_blacklist : analyzer -> string list val analysis_path_regex_blacklist : analyzer -> string list
@ -668,30 +672,8 @@ val xcode_developer_dir : string option
val xcpretty : bool val xcpretty : bool
(** {2 Global variables} *)
val footprint : bool ref
val run_in_footprint_mode : ('a -> 'b) -> 'a -> 'b
(** Call f x with footprint set to true.
Restore the initial value of footprint also in case of exception. *)
val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b
(** Call f x with footprint set to false.
Restore the initial value of footprint also in case of exception. *)
(** {2 Global variables with initial values specified by command-line options} *) (** {2 Global variables with initial values specified by command-line options} *)
val abs_val : int ref
val reset_abs_val : unit -> unit
val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b
(** Call f x with abs_val set to zero.
Restore the initial value also in case of exception. *)
val allow_leak : bool ref
val clang_compilation_dbs : [`Escaped of string | `Raw of string] list ref val clang_compilation_dbs : [`Escaped of string | `Raw of string] list ref
(** {2 Command Line Interface Documentation} *) (** {2 Command Line Interface Documentation} *)

11
infer/src/biabduction/Abs.ml
Unescape View File

@ -893,7 +893,7 @@ let abstract_pure_part tenv p ~(from_abstract_footprint : bool) =
let new_pure = do_pure (Prop.get_pure p) in let new_pure = do_pure (Prop.get_pure p) in
let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.exp_sub_empty in let eprop' = Prop.set p ~pi:new_pure ~sub:Sil.exp_sub_empty in
let eprop'' = let eprop'' =
if !Config.footprint && not from_abstract_footprint then if !BiabductionConfig.footprint && not from_abstract_footprint then
let new_pi_footprint = do_pure p.Prop.pi_fp in let new_pi_footprint = do_pure p.Prop.pi_fp in
Prop.set eprop' ~pi_fp:new_pi_footprint Prop.set eprop' ~pi_fp:new_pi_footprint
else eprop' else eprop'
@ -1117,9 +1117,12 @@ let check_junk pname tenv prop =
List.mem ~equal:attr_opt_equal !leaks_reported alloc_attribute List.mem ~equal:attr_opt_equal !leaks_reported alloc_attribute
in in
let ignore_leak = let ignore_leak =
!Config.allow_leak || ignore_resource || is_undefined || already_reported () !BiabductionConfig.allow_leak || ignore_resource || is_undefined
|| already_reported ()
in
let report_and_continue =
Language.curr_language_is Java || !BiabductionConfig.footprint
in in
let report_and_continue = Language.curr_language_is Java || !Config.footprint in
let report_leak () = let report_leak () =
if not report_and_continue then raise exn if not report_and_continue then raise exn
else ( else (
@ -1256,7 +1259,7 @@ let abstract_footprint pname (tenv : Tenv.t) (prop : Prop.normal Prop.t) : Prop.
let abstract_ pname pay tenv p = let abstract_ pname pay tenv p =
if pay then SymOp.pay () ; if pay then SymOp.pay () ;
(* pay one symop *) (* pay one symop *)
let p' = if !Config.footprint then abstract_footprint pname tenv p else p in let p' = if !BiabductionConfig.footprint then abstract_footprint pname tenv p else p in
abstract_prop pname tenv ~rename_primed:true ~from_abstract_footprint:false p' abstract_prop pname tenv ~rename_primed:true ~from_abstract_footprint:false p'

35
infer/src/biabduction/Absarray.ml
Unescape View File

@ -7,10 +7,27 @@
*) *)
open! IStd open! IStd
module L = Logging
(** Abstraction for Arrays *) (** This function should be used before adding a new index to Earray. The [exp] is the newly created
index. This function "cleans" [exp] according to whether it is the footprint or current part of
the prop. The function faults in the re - execution mode, as an internal check of the tool. *)
let array_clean_new_index footprint_part new_idx =
assert (not (footprint_part && not !BiabductionConfig.footprint)) ;
if
footprint_part
&& Exp.free_vars new_idx |> Sequence.exists ~f:(fun id -> not (Ident.is_footprint id))
then (
L.d_warning
( "Array index " ^ Exp.to_string new_idx
^ " has non-footprint vars: replaced by fresh footprint var" ) ;
L.d_ln () ;
let id = Ident.create_fresh Ident.kfootprint in
Exp.Var id )
else new_idx
module L = Logging
(** Abstraction for Arrays *)
type sigma = Sil.hpred list type sigma = Sil.hpred list
@ -243,7 +260,7 @@ end = struct
let orig_indices = List.map ~f:fst esel in let orig_indices = List.map ~f:fst esel in
let index_is_not_new idx = List.exists ~f:(Exp.equal idx) orig_indices in let index_is_not_new idx = List.exists ~f:(Exp.equal idx) orig_indices in
let process_index idx = let process_index idx =
if index_is_not_new idx then idx else Sil.array_clean_new_index footprint_part idx if index_is_not_new idx then idx else array_clean_new_index footprint_part idx
in in
let esel_in' = List.map ~f:(fun (idx, se) -> (process_index idx, se)) esel_in in let esel_in' = List.map ~f:(fun (idx, se) -> (process_index idx, se)) esel_in in
Sil.Earray (len, esel_in', inst2) Sil.Earray (len, esel_in', inst2)
@ -318,7 +335,7 @@ let prop_update_sigma_and_fp_sigma tenv (p : Prop.normal Prop.t)
let sigma', changed = update false p.Prop.sigma in let sigma', changed = update false p.Prop.sigma in
let ep1 = Prop.set p ~sigma:sigma' in let ep1 = Prop.set p ~sigma:sigma' in
let ep2, changed2 = let ep2, changed2 =
if !Config.footprint then if !BiabductionConfig.footprint then
let sigma_fp', changed' = update true ep1.Prop.sigma_fp in let sigma_fp', changed' = update true ep1.Prop.sigma_fp in
(Prop.set ep1 ~sigma_fp:sigma_fp', changed') (Prop.set ep1 ~sigma_fp:sigma_fp', changed')
else (ep1, false) else (ep1, false)
@ -411,11 +428,13 @@ let blur_array_index tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (in
Prop.normal Prop.t = Prop.normal Prop.t =
try try
let fresh_index = let fresh_index =
Exp.Var (Ident.create_fresh (if !Config.footprint then Ident.kfootprint else Ident.kprimed)) Exp.Var
(Ident.create_fresh
(if !BiabductionConfig.footprint then Ident.kfootprint else Ident.kprimed))
in in
let p2 = let p2 =
try try
if !Config.footprint then if !BiabductionConfig.footprint then
let sigma_fp = p.Prop.sigma_fp in let sigma_fp = p.Prop.sigma_fp in
let matched_fp = StrexpMatch.find_path sigma_fp path in let matched_fp = StrexpMatch.find_path sigma_fp path in
let sigma_fp' = StrexpMatch.replace_index tenv true matched_fp index fresh_index in let sigma_fp' = StrexpMatch.replace_index tenv true matched_fp index fresh_index in
@ -563,7 +582,7 @@ let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.str
let do_reexecution () = let do_reexecution () =
match se_in with Sil.Earray (_, esel, _) -> do_array_reexecution esel | _ -> assert false match se_in with Sil.Earray (_, esel, _) -> do_array_reexecution esel | _ -> assert false
in in
if !Config.footprint then do_footprint () else do_reexecution () if !BiabductionConfig.footprint then do_footprint () else do_reexecution ()
let strexp_abstract tenv (p : Prop.normal Prop.t) : Prop.normal Prop.t = let strexp_abstract tenv (p : Prop.normal Prop.t) : Prop.normal Prop.t =
@ -581,7 +600,7 @@ let report_error prop =
let check_after_array_abstraction tenv prop = let check_after_array_abstraction tenv prop =
let lookup = Tenv.lookup tenv in let lookup = Tenv.lookup tenv in
let check_index root offs (ind, _) = let check_index root offs (ind, _) =
if !Config.footprint then if !BiabductionConfig.footprint then
let path = StrexpMatch.path_from_exp_offsets root offs in let path = StrexpMatch.path_from_exp_offsets root offs in
index_is_pointed_to tenv prop path ind index_is_pointed_to tenv prop path ind
else not (Exp.free_vars ind |> Sequence.exists ~f:Ident.is_primed) else not (Exp.free_vars ind |> Sequence.exists ~f:Ident.is_primed)

7
infer/src/biabduction/Absarray.mli
Unescape View File

@ -8,6 +8,13 @@
open! IStd open! IStd
val array_clean_new_index : bool -> Exp.t -> Exp.t
(** This function should be used before adding a new
index to Earray. The [exp] is the newly created
index. This function "cleans" [exp] according to whether it is the
footprint or current part of the prop.
The function faults in the re - execution mode, as an internal check of the tool. *)
(** Abstraction for Arrays *) (** Abstraction for Arrays *)
val abstract_array_check : Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t val abstract_array_check : Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t

36
infer/src/biabduction/BiabductionConfig.ml
Unescape View File

@ -0,0 +1,36 @@
(*
* Copyright (c) 2009-2013, Monoidics ltd.
* Copyright (c) 2013-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
(** Global variables *)
let set_reference_and_call_function reference value f x =
let saved = !reference in
let restore () = reference := saved in
Utils.try_finally_swallow_timeout
~f:(fun () ->
reference := value ;
f x )
~finally:restore
(** Flag for footprint discovery mode *)
let footprint = ref true
let run_in_footprint_mode f x = set_reference_and_call_function footprint true f x
let run_in_re_execution_mode f x = set_reference_and_call_function footprint false f x
let abs_val = ref Config.abs_val
let reset_abs_val () = abs_val := Config.abs_val
let run_with_abs_val_equal_zero f x = set_reference_and_call_function abs_val 0 f x
let allow_leak = ref Config.allow_leak

33
infer/src/biabduction/BiabductionConfig.mli
Unescape View File

@ -0,0 +1,33 @@
(*
* Copyright (c) 2009-2013, Monoidics ltd.
* Copyright (c) 2013-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*)
open! IStd
(** {2 Global variables} *)
val footprint : bool ref
val run_in_footprint_mode : ('a -> 'b) -> 'a -> 'b
(** Call f x with footprint set to true.
Restore the initial value of footprint also in case of exception. *)
val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b
(** Call f x with footprint set to false.
Restore the initial value of footprint also in case of exception. *)
(** {2 Global variables with initial values specified by command-line options} *)
val abs_val : int ref
val reset_abs_val : unit -> unit
val run_with_abs_val_equal_zero : ('a -> 'b) -> 'a -> 'b
(** Call f x with abs_val set to zero.
Restore the initial value also in case of exception. *)
val allow_leak : bool ref

6
infer/src/biabduction/BuiltinDefn.ml
Unescape View File

@ -206,7 +206,7 @@ let create_type tenv n_lexp typ prop =
let sil_is_nonnull = Exp.UnOp (Unop.LNot, sil_is_null, None) in let sil_is_nonnull = Exp.UnOp (Unop.LNot, sil_is_null, None) in
let null_case = Propset.to_proplist (prune tenv ~positive:true sil_is_null prop) in let null_case = Propset.to_proplist (prune tenv ~positive:true sil_is_null prop) in
let non_null_case = Propset.to_proplist (prune tenv ~positive:true sil_is_nonnull prop_type) in let non_null_case = Propset.to_proplist (prune tenv ~positive:true sil_is_nonnull prop_type) in
if List.length non_null_case > 0 && !Config.footprint then non_null_case if List.length non_null_case > 0 && !BiabductionConfig.footprint then non_null_case
else if List.length non_null_case > 0 && is_undefined_opt tenv prop n_lexp then non_null_case else if List.length non_null_case > 0 && is_undefined_opt tenv prop n_lexp then non_null_case
else null_case @ non_null_case else null_case @ non_null_case
@ -306,14 +306,14 @@ let execute___instanceof_cast ~instof {Builtin.pdesc; tenv; prop_; path; ret_id_
let pos_res = mk_res pos_type_opt val1 in let pos_res = mk_res pos_type_opt val1 in
let neg_res = mk_res neg_type_opt Exp.zero in let neg_res = mk_res neg_type_opt Exp.zero in
pos_res @ neg_res pos_res @ neg_res
else if !Config.footprint then else if !BiabductionConfig.footprint then
match pos_type_opt with match pos_type_opt with
| None -> | None ->
deal_with_failed_cast val1 texp1 texp2 deal_with_failed_cast val1 texp1 texp2
| Some _ -> | Some _ ->
mk_res pos_type_opt val1 mk_res pos_type_opt val1
else else
(* !Config.footprint is false *) (* !BiabductionConfig.footprint is false *)
match neg_type_opt with match neg_type_opt with
| Some _ -> | Some _ ->
if is_undefined_opt tenv prop val1 then mk_res pos_type_opt val1 if is_undefined_opt tenv prop val1 then mk_res pos_type_opt val1

11
infer/src/biabduction/Dom.ml
Unescape View File

@ -925,7 +925,8 @@ let const_partial_join c1 c2 =
if Const.equal c1 c2 then Exp.Const c1 if Const.equal c1 c2 then Exp.Const c1
else if Const.kind_equal c1 c2 && not (is_int c1) then ( else if Const.kind_equal c1 c2 && not (is_int c1) then (
L.d_strln "failure reason 18" ; raise Sil.JoinFail ) L.d_strln "failure reason 18" ; raise Sil.JoinFail )
else if !Config.abs_val >= 2 then FreshVarExp.get_fresh_exp (Exp.Const c1) (Exp.Const c2) else if !BiabductionConfig.abs_val >= 2 then
FreshVarExp.get_fresh_exp (Exp.Const c1) (Exp.Const c2)
else ( L.d_strln "failure reason 19" ; raise Sil.JoinFail ) else ( L.d_strln "failure reason 19" ; raise Sil.JoinFail )
@ -1906,7 +1907,7 @@ let eprop_partial_join' tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.expose
let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Prop.t) : let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Prop.t) :
Prop.normal Prop.t * Prop.normal Prop.t = Prop.normal Prop.t * Prop.normal Prop.t =
if not !Config.footprint then (p1, p2) if not !BiabductionConfig.footprint then (p1, p2)
else else
let fp1 = Prop.extract_footprint p1 in let fp1 = Prop.extract_footprint p1 in
let fp2 = Prop.extract_footprint p2 in let fp2 = Prop.extract_footprint p2 in
@ -1931,14 +1932,14 @@ let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Pro
let prop_partial_join pname tenv mode p1 p2 = let prop_partial_join pname tenv mode p1 p2 =
let res_by_implication_only = let res_by_implication_only =
if !Config.footprint then None if !BiabductionConfig.footprint then None
else if Prover.check_implication pname tenv p1 (Prop.expose p2) then Some p2 else if Prover.check_implication pname tenv p1 (Prop.expose p2) then Some p2
else if Prover.check_implication pname tenv p2 (Prop.expose p1) then Some p1 else if Prover.check_implication pname tenv p2 (Prop.expose p1) then Some p1
else None else None
in in
match res_by_implication_only with match res_by_implication_only with
| None -> ( | None -> (
if !Config.footprint then JoinState.set_footprint true ; if !BiabductionConfig.footprint then JoinState.set_footprint true ;
Rename.init () ; Rename.init () ;
FreshVarExp.init () ; FreshVarExp.init () ;
Todo.init () ; Todo.init () ;
@ -1949,7 +1950,7 @@ let prop_partial_join pname tenv mode p1 p2 =
let rename_footprint = Rename.reset () in let rename_footprint = Rename.reset () in
Todo.reset rename_footprint ; Todo.reset rename_footprint ;
let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in
if !Config.footprint then JoinState.set_footprint false ; if !BiabductionConfig.footprint then JoinState.set_footprint false ;
Some res ) Some res )
~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ()) ~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ())
with Sil.JoinFail -> None ) with Sil.JoinFail -> None )

23
infer/src/biabduction/Prop.ml
Unescape View File

@ -448,7 +448,8 @@ let rec create_strexp_of_type ~path tenv struct_init_mode (typ : Typ.t) len inst
let init_value () = let init_value () =
let create_fresh_var () = let create_fresh_var () =
let fresh_id = let fresh_id =
Ident.create_fresh (if !Config.footprint then Ident.kfootprint else Ident.kprimed) Ident.create_fresh
(if !BiabductionConfig.footprint then Ident.kfootprint else Ident.kprimed)
in in
Exp.Var fresh_id Exp.Var fresh_id
in in
@ -1058,7 +1059,7 @@ module Normalize = struct
let exp_normalize ?destructive tenv sub exp = let exp_normalize ?destructive tenv sub exp =
let exp' = Sil.exp_sub sub exp in let exp' = Sil.exp_sub sub exp in
let abstract_expressions = !Config.abs_val >= 1 in let abstract_expressions = !BiabductionConfig.abs_val >= 1 in
sym_eval ?destructive tenv abstract_expressions exp' sym_eval ?destructive tenv abstract_expressions exp'
@ -1075,7 +1076,7 @@ module Normalize = struct
let exp_normalize_noabs tenv sub exp = let exp_normalize_noabs tenv sub exp =
Config.run_with_abs_val_equal_zero (exp_normalize tenv sub) exp BiabductionConfig.run_with_abs_val_equal_zero (exp_normalize tenv sub) exp
(** Turn an inequality expression into an atom *) (** Turn an inequality expression into an atom *)
@ -1742,7 +1743,7 @@ end
(* End of module Normalize *) (* End of module Normalize *)
let exp_normalize_prop ?destructive tenv prop exp = let exp_normalize_prop ?destructive tenv prop exp =
Config.run_with_abs_val_equal_zero BiabductionConfig.run_with_abs_val_equal_zero
(Normalize.exp_normalize ?destructive tenv (`Exp prop.sub)) (Normalize.exp_normalize ?destructive tenv (`Exp prop.sub))
exp exp
@ -1761,11 +1762,15 @@ let lexp_normalize_prop tenv p lexp =
let atom_normalize_prop tenv prop atom = let atom_normalize_prop tenv prop atom =
Config.run_with_abs_val_equal_zero (Normalize.atom_normalize tenv (`Exp prop.sub)) atom BiabductionConfig.run_with_abs_val_equal_zero
(Normalize.atom_normalize tenv (`Exp prop.sub))
atom
let sigma_normalize_prop tenv prop sigma = let sigma_normalize_prop tenv prop sigma =
Config.run_with_abs_val_equal_zero (Normalize.sigma_normalize tenv (`Exp prop.sub)) sigma BiabductionConfig.run_with_abs_val_equal_zero
(Normalize.sigma_normalize tenv (`Exp prop.sub))
sigma
let sigma_replace_exp tenv epairs sigma = let sigma_replace_exp tenv epairs sigma =
@ -1775,7 +1780,7 @@ let sigma_replace_exp tenv epairs sigma =
(** Construct an atom. *) (** Construct an atom. *)
let mk_atom tenv atom = let mk_atom tenv atom =
Config.run_with_abs_val_equal_zero BiabductionConfig.run_with_abs_val_equal_zero
(fun () -> Normalize.atom_normalize tenv Sil.sub_empty atom) (fun () -> Normalize.atom_normalize tenv Sil.sub_empty atom)
() ()
@ -2023,7 +2028,7 @@ let apply_reindexing tenv (exp_subst : Sil.exp_subst) prop =
let prop_rename_array_indices tenv prop = let prop_rename_array_indices tenv prop =
if !Config.footprint then prop if !BiabductionConfig.footprint then prop
else else
let indices = sigma_get_array_indices prop.sigma in let indices = sigma_get_array_indices prop.sigma in
let not_same_base_lt_offsets (e1 : Exp.t) (e2 : Exp.t) = let not_same_base_lt_offsets (e1 : Exp.t) (e2 : Exp.t) =
@ -2308,7 +2313,7 @@ type 'a prop_iter =
{ pit_sub: Sil.exp_subst (** substitution for equalities *) { pit_sub: Sil.exp_subst (** substitution for equalities *)
; pit_pi: pi (** pure part *) ; pit_pi: pi (** pure part *)
; pit_newpi: (bool * Sil.atom) list (** newly added atoms. *) ; pit_newpi: (bool * Sil.atom) list (** newly added atoms. *)
; (* The first records !Config.footprint. *) ; (* The first records !BiabductionConfig.footprint. *)
pit_old: sigma (** sigma already visited *) pit_old: sigma (** sigma already visited *)
; pit_curr: Sil.hpred (** current element *) ; pit_curr: Sil.hpred (** current element *)
; pit_state: 'a (** state of current element *) ; pit_state: 'a (** state of current element *)

8
infer/src/biabduction/Prover.ml
Unescape View File

@ -1473,7 +1473,7 @@ let path_to_id path =
assert false assert false
(* None *) (* None *)
in in
if !Config.footprint then Ident.create_fresh Ident.kfootprint if !BiabductionConfig.footprint then Ident.create_fresh Ident.kfootprint
else else
match f path with None -> Ident.create_fresh Ident.kfootprint | Some s -> Ident.create_path s match f path with None -> Ident.create_fresh Ident.kfootprint | Some s -> Ident.create_path s
@ -1533,7 +1533,7 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 :
if index_frame <> [] then Some (Sil.Earray (len1, index_frame, inst1)) else None if index_frame <> [] then Some (Sil.Earray (len1, index_frame, inst1)) else None
in in
let index_missing_opt = let index_missing_opt =
if index_missing <> [] && !Config.footprint then if index_missing <> [] && !BiabductionConfig.footprint then
Some (Sil.Earray (len1, index_missing, inst1)) Some (Sil.Earray (len1, index_missing, inst1))
else None else None
in in
@ -2053,7 +2053,7 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
| _ -> | _ ->
() ()
in in
if is_callee && !Config.footprint then add_subtype () if is_callee && !BiabductionConfig.footprint then add_subtype ()
let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 : let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 :
@ -2664,7 +2664,7 @@ let check_implication pname tenv p1 p2 =
in in
check p1 p2 check p1 p2
&& &&
if !Config.footprint then if !BiabductionConfig.footprint then
check (Prop.normalize tenv (Prop.extract_footprint p1)) (Prop.extract_footprint p2) check (Prop.normalize tenv (Prop.extract_footprint p1)) (Prop.extract_footprint p2)
else true else true

53
infer/src/biabduction/Rearrange.ml
Unescape View File

@ -127,7 +127,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let atoms', se', res_t' = let atoms', se', res_t' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp t off' inst create_struct_values pname tenv orig_prop footprint_part kind max_stamp t off' inst
in in
let e' = Sil.array_clean_new_index footprint_part e in let e' = Absarray.array_clean_new_index footprint_part e in
let len = Exp.Var (new_id ()) in let len = Exp.Var (new_id ()) in
let se = Sil.Earray (len, [(e', se')], inst) in let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = Typ.mk_array res_t' in let res_t = Typ.mk_array res_t' in
@ -144,7 +144,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let atoms', se', res_t' = let atoms', se', res_t' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst
in in
let e' = Sil.array_clean_new_index footprint_part e in let e' = Absarray.array_clean_new_index footprint_part e in
let se = Sil.Earray (len, [(e', se')], inst) in let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = Typ.mk_array ~default:t res_t' ?length ?stride in let res_t = Typ.mk_array ~default:t res_t' ?length ?stride in
(Sil.Aeq (e, e') :: atoms', se, res_t) (Sil.Aeq (e, e') :: atoms', se, res_t)
@ -166,7 +166,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let atoms', se', res_t' = let atoms', se', res_t' =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst
in in
let e' = Sil.array_clean_new_index footprint_part e in let e' = Absarray.array_clean_new_index footprint_part e in
let se = Sil.Earray (len, [(e', se')], inst) in let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = mk_typ_f (Tarray {elt= res_t'; length= None; stride= None}) in let res_t = mk_typ_f (Tarray {elt= res_t'; length= None; stride= None}) in
(Sil.Aeq (e, e') :: atoms', se, res_t) (Sil.Aeq (e, e') :: atoms', se, res_t)
@ -314,7 +314,7 @@ and array_case_analysis_index pname tenv orig_prop footprint_part kind max_stamp
let array_default = Sil.Earray (array_len, array_cont, inst_arr) in let array_default = Sil.Earray (array_len, array_cont, inst_arr) in
let typ_default = Typ.mk_array ~default:typ_array typ_cont ?length:typ_array_len in let typ_default = Typ.mk_array ~default:typ_array typ_cont ?length:typ_array_len in
[([], array_default, typ_default)] [([], array_default, typ_default)]
else if !Config.footprint then ( else if !BiabductionConfig.footprint then (
let atoms, elem_se, elem_typ = let atoms, elem_se, elem_typ =
create_struct_values pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst create_struct_values pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst
in in
@ -447,7 +447,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
if if
(* in angelic mode, purposely ignore dangling pointer warnings during the footprint phase -- we (* in angelic mode, purposely ignore dangling pointer warnings during the footprint phase -- we
* will fix them during the re - execution phase *) * will fix them during the re - execution phase *)
not !Config.footprint not !BiabductionConfig.footprint
then ( then (
L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ; L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ;
let deref_str = Localise.deref_str_dangling None in let deref_str = Localise.deref_str_dangling None in
@ -576,7 +576,9 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
assert false assert false
in in
let atoms_se_te_to_iter e (atoms, se, te) = let atoms_se_te_to_iter e (atoms, se, te) =
let iter' = List.fold ~f:(Prop.prop_iter_add_atom !Config.footprint) ~init:iter atoms in let iter' =
List.fold ~f:(Prop.prop_iter_add_atom !BiabductionConfig.footprint) ~init:iter atoms
in
Prop.prop_iter_update_current iter' (Sil.Hpointsto (e, se, te)) Prop.prop_iter_update_current iter' (Sil.Hpointsto (e, se, te))
in in
let do_extend e se te = let do_extend e se te =
@ -646,7 +648,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
List.map List.map
~f:(fun (iter, (atoms, fp_sigma)) -> ~f:(fun (iter, (atoms, fp_sigma)) ->
let iter' = let iter' =
List.fold ~f:(Prop.prop_iter_add_atom !Config.footprint) ~init:iter atoms List.fold ~f:(Prop.prop_iter_add_atom !BiabductionConfig.footprint) ~init:iter atoms
in in
Prop.prop_iter_replace_footprint_sigma iter' fp_sigma ) Prop.prop_iter_replace_footprint_sigma iter' fp_sigma )
iter_atoms_fp_sigma_list iter_atoms_fp_sigma_list
@ -694,7 +696,9 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
let nsigma_fp = Prop.sigma_normalize_prop tenv Prop.prop_emp sigma_fp in let nsigma_fp = Prop.sigma_normalize_prop tenv Prop.prop_emp sigma_fp in
let prop' = Prop.normalize tenv (Prop.set eprop ~sigma_fp:nsigma_fp) in let prop' = Prop.normalize tenv (Prop.set eprop ~sigma_fp:nsigma_fp) in
let prop_new = let prop_new =
List.fold ~f:(Prop.prop_atom_and tenv ~footprint:!Config.footprint) ~init:prop' atoms List.fold
~f:(Prop.prop_atom_and tenv ~footprint:!BiabductionConfig.footprint)
~init:prop' atoms
in in
let iter = let iter =
match Prop.prop_iter_create prop_new with match Prop.prop_iter_create prop_new with
@ -1061,7 +1065,7 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
let sigma_fp = ptsto_foot :: Prop.prop_iter_get_footprint_sigma iter in let sigma_fp = ptsto_foot :: Prop.prop_iter_get_footprint_sigma iter in
let iter_foot = Prop.prop_iter_prev_then_insert iter ptsto in let iter_foot = Prop.prop_iter_prev_then_insert iter ptsto in
let iter_foot_atoms = let iter_foot_atoms =
List.fold ~f:(Prop.prop_iter_add_atom !Config.footprint) ~init:iter_foot atoms List.fold ~f:(Prop.prop_iter_add_atom !BiabductionConfig.footprint) ~init:iter_foot atoms
in in
let iter' = Prop.prop_iter_replace_footprint_sigma iter_foot_atoms sigma_fp in let iter' = Prop.prop_iter_replace_footprint_sigma iter_foot_atoms sigma_fp in
let offsets_default = Sil.exp_get_offsets lexp in let offsets_default = Sil.exp_get_offsets lexp in
@ -1124,7 +1128,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
raise (Exceptions.Missing_fld (fld, __POS__)) raise (Exceptions.Missing_fld (fld, __POS__))
in in
let res = let res =
if !Config.footprint then prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst if !BiabductionConfig.footprint then prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst
else ( else (
check_field_splitting () ; check_field_splitting () ;
match Prop.prop_iter_current tenv iter with match Prop.prop_iter_current tenv iter with
@ -1136,7 +1140,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
in in
let handle_case (atoms', se', te') = let handle_case (atoms', se', te') =
let iter' = let iter' =
List.fold ~f:(Prop.prop_iter_add_atom !Config.footprint) ~init:iter atoms' List.fold ~f:(Prop.prop_iter_add_atom !BiabductionConfig.footprint) ~init:iter atoms'
in in
Prop.prop_iter_update_current iter' (Sil.Hpointsto (e, se', te')) Prop.prop_iter_update_current iter' (Sil.Hpointsto (e, se', te'))
in in
@ -1195,7 +1199,7 @@ let iter_rearrange_ne_dllseg_first tenv recurse_on_iters iter para_dll e1 e2 e3
let _, para_dll_inst = Sil.hpara_dll_instantiate para_dll e1 e2 e3 elist in let _, para_dll_inst = Sil.hpara_dll_instantiate para_dll e1 e2 e3 elist in
let iter' = Prop.prop_iter_update_current_by_list iter para_dll_inst in let iter' = Prop.prop_iter_update_current_by_list iter para_dll_inst in
let prop' = Prop.prop_iter_to_prop tenv iter' in let prop' = Prop.prop_iter_to_prop tenv iter' in
let prop'' = Prop.conjoin_eq tenv ~footprint:!Config.footprint e1 e4 prop' in let prop'' = Prop.conjoin_eq tenv ~footprint:!BiabductionConfig.footprint e1 e4 prop' in
match Prop.prop_iter_create prop'' with None -> assert false | Some iter' -> iter' match Prop.prop_iter_create prop'' with None -> assert false | Some iter' -> iter'
in in
recurse_on_iters [iter_inductive_case; iter_base_case] recurse_on_iters [iter_inductive_case; iter_base_case]
@ -1215,7 +1219,7 @@ let iter_rearrange_ne_dllseg_last tenv recurse_on_iters iter para_dll e1 e2 e3 e
let _, para_dll_inst = Sil.hpara_dll_instantiate para_dll e4 e2 e3 elist in let _, para_dll_inst = Sil.hpara_dll_instantiate para_dll e4 e2 e3 elist in
let iter' = Prop.prop_iter_update_current_by_list iter para_dll_inst in let iter' = Prop.prop_iter_update_current_by_list iter para_dll_inst in
let prop' = Prop.prop_iter_to_prop tenv iter' in let prop' = Prop.prop_iter_to_prop tenv iter' in
let prop'' = Prop.conjoin_eq tenv ~footprint:!Config.footprint e1 e4 prop' in let prop'' = Prop.conjoin_eq tenv ~footprint:!BiabductionConfig.footprint e1 e4 prop' in
match Prop.prop_iter_create prop'' with None -> assert false | Some iter' -> iter' match Prop.prop_iter_create prop'' with None -> assert false | Some iter' -> iter'
in in
recurse_on_iters [iter_inductive_case; iter_base_case] recurse_on_iters [iter_inductive_case; iter_base_case]
@ -1231,7 +1235,7 @@ let iter_rearrange_pe_lseg tenv recurse_on_iters default_case_iter iter para e1
in in
let iter_subcases = let iter_subcases =
let removed_prop = Prop.prop_iter_remove_curr_then_to_prop tenv iter in let removed_prop = Prop.prop_iter_remove_curr_then_to_prop tenv iter in
let prop' = Prop.conjoin_eq tenv ~footprint:!Config.footprint e1 e2 removed_prop in let prop' = Prop.conjoin_eq tenv ~footprint:!BiabductionConfig.footprint e1 e2 removed_prop in
match Prop.prop_iter_create prop' with match Prop.prop_iter_create prop' with
| None -> | None ->
let iter' = default_case_iter (Prop.prop_iter_set_state iter ()) in let iter' = default_case_iter (Prop.prop_iter_set_state iter ()) in
@ -1255,8 +1259,8 @@ let iter_rearrange_pe_dllseg_first tenv recurse_on_iters default_case_iter iter
in in
let iter_subcases = let iter_subcases =
let removed_prop = Prop.prop_iter_remove_curr_then_to_prop tenv iter in let removed_prop = Prop.prop_iter_remove_curr_then_to_prop tenv iter in
let prop' = Prop.conjoin_eq tenv ~footprint:!Config.footprint e1 e3 removed_prop in let prop' = Prop.conjoin_eq tenv ~footprint:!BiabductionConfig.footprint e1 e3 removed_prop in
let prop'' = Prop.conjoin_eq tenv ~footprint:!Config.footprint e2 e4 prop' in let prop'' = Prop.conjoin_eq tenv ~footprint:!BiabductionConfig.footprint e2 e4 prop' in
match Prop.prop_iter_create prop'' with match Prop.prop_iter_create prop'' with
| None -> | None ->
let iter' = default_case_iter (Prop.prop_iter_set_state iter ()) in let iter' = default_case_iter (Prop.prop_iter_set_state iter ()) in
@ -1280,8 +1284,8 @@ let iter_rearrange_pe_dllseg_last tenv recurse_on_iters default_case_iter iter p
in in
let iter_subcases = let iter_subcases =
let removed_prop = Prop.prop_iter_remove_curr_then_to_prop tenv iter in let removed_prop = Prop.prop_iter_remove_curr_then_to_prop tenv iter in
let prop' = Prop.conjoin_eq tenv ~footprint:!Config.footprint e1 e3 removed_prop in let prop' = Prop.conjoin_eq tenv ~footprint:!BiabductionConfig.footprint e1 e3 removed_prop in
let prop'' = Prop.conjoin_eq tenv ~footprint:!Config.footprint e2 e4 prop' in let prop'' = Prop.conjoin_eq tenv ~footprint:!BiabductionConfig.footprint e2 e4 prop' in
match Prop.prop_iter_create prop'' with match Prop.prop_iter_create prop'' with
| None -> | None ->
let iter' = default_case_iter (Prop.prop_iter_set_state iter ()) in let iter' = default_case_iter (Prop.prop_iter_set_state iter ()) in
@ -1401,12 +1405,13 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
L.d_ln () ) ; L.d_ln () ) ;
let default_case_iter (iter' : unit Prop.prop_iter) = let default_case_iter (iter' : unit Prop.prop_iter) =
if Config.trace_rearrange then L.d_strln "entering default_case_iter" ; if Config.trace_rearrange then L.d_strln "entering default_case_iter" ;
if !Config.footprint then prop_iter_add_hpred_footprint pname tenv prop iter' (lexp, typ) inst if !BiabductionConfig.footprint then
else if Config.array_level >= 1 && (not !Config.footprint) && Exp.pointer_arith lexp then prop_iter_add_hpred_footprint pname tenv prop iter' (lexp, typ) inst
rearrange_arith tenv lexp prop else if Config.array_level >= 1 && (not !BiabductionConfig.footprint) && Exp.pointer_arith lexp
then rearrange_arith tenv lexp prop
else ( else (
pp_rearrangement_error "cannot find predicate with root" prop lexp ; pp_rearrangement_error "cannot find predicate with root" prop lexp ;
if not !Config.footprint then Printer.force_delayed_prints () ; if not !BiabductionConfig.footprint then Printer.force_delayed_prints () ;
raise (Exceptions.Symexec_memory_error __POS__) ) raise (Exceptions.Symexec_memory_error __POS__) )
in in
let recurse_on_iters iters = let recurse_on_iters iters =
@ -1768,7 +1773,7 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
let prop' = let prop' =
match pname with match pname with
| Typ.Procname.Java java_pname | Typ.Procname.Java java_pname
when Config.csl_analysis && !Config.footprint when Config.csl_analysis && !BiabductionConfig.footprint
&& not && not
( Typ.Procname.is_constructor pname ( Typ.Procname.is_constructor pname
|| Typ.Procname.Java.is_class_initializer java_pname ) -> || Typ.Procname.Java.is_class_initializer java_pname ) ->
@ -1778,7 +1783,7 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
in in
match Prop.prop_iter_create prop' with match Prop.prop_iter_create prop' with
| None -> | None ->
if !Config.footprint then if !BiabductionConfig.footprint then
[prop_iter_add_hpred_footprint_to_prop pname tenv prop' (nlexp, typ) inst] [prop_iter_add_hpred_footprint_to_prop pname tenv prop' (nlexp, typ) inst]
else ( else (
pp_rearrangement_error "sigma is empty" prop nlexp ; pp_rearrangement_error "sigma is empty" prop nlexp ;

25
infer/src/biabduction/SymExec.ml
Unescape View File

@ -247,7 +247,7 @@ let prune_ne tenv ~positive e1 e2 prop =
if is_inconsistent then Propset.empty if is_inconsistent then Propset.empty
else else
let conjoin = if positive then Prop.conjoin_neq else Prop.conjoin_eq in let conjoin = if positive then Prop.conjoin_neq else Prop.conjoin_eq in
let new_prop = conjoin tenv ~footprint:!Config.footprint e1 e2 prop in let new_prop = conjoin tenv ~footprint:!BiabductionConfig.footprint e1 e2 prop in
if Prover.check_inconsistency tenv new_prop then Propset.empty if Prover.check_inconsistency tenv new_prop then Propset.empty
else Propset.singleton tenv new_prop else Propset.singleton tenv new_prop
@ -277,7 +277,7 @@ let prune_ineq tenv ~is_strict ~positive prop e1 e2 =
let is_inconsistent = Prover.check_atom tenv prop (Prop.mk_inequality tenv not_prune_cond) in let is_inconsistent = Prover.check_atom tenv prop (Prop.mk_inequality tenv not_prune_cond) in
if is_inconsistent then Propset.empty if is_inconsistent then Propset.empty
else else
let footprint = !Config.footprint in let footprint = !BiabductionConfig.footprint in
let prop_with_ineq = Prop.conjoin_eq tenv ~footprint prune_cond Exp.one prop in let prop_with_ineq = Prop.conjoin_eq tenv ~footprint prune_cond Exp.one prop in
Propset.singleton tenv prop_with_ineq Propset.singleton tenv prop_with_ineq
@ -796,7 +796,7 @@ let force_objc_init_return_nil pdesc callee_pname tenv ret_id pre path receiver
let current_pname = Procdesc.get_proc_name pdesc in let current_pname = Procdesc.get_proc_name pdesc in
if if
Typ.Procname.is_constructor callee_pname Typ.Procname.is_constructor callee_pname
&& receiver_self receiver pre && !Config.footprint && receiver_self receiver pre && !BiabductionConfig.footprint
&& Typ.Procname.is_constructor current_pname && Typ.Procname.is_constructor current_pname
then then
let propset = prune_ne tenv ~positive:false (Exp.Var ret_id) Exp.zero pre in let propset = prune_ne tenv ~positive:false (Exp.Var ret_id) Exp.zero pre in
@ -859,7 +859,7 @@ let handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_
match force_objc_init_return_nil pdesc callee_pname tenv ret_id pre path receiver with match force_objc_init_return_nil pdesc callee_pname tenv ret_id pre path receiver with
| [] -> | [] ->
if if
!Config.footprint !BiabductionConfig.footprint
&& Option.is_none (Attribute.get_undef tenv pre receiver) && Option.is_none (Attribute.get_undef tenv pre receiver)
&& not (Rearrange.is_only_pt_by_fld_or_param_nonnull pdesc tenv pre receiver) && not (Rearrange.is_only_pt_by_fld_or_param_nonnull pdesc tenv pre receiver)
then then
@ -970,7 +970,7 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nonnull_annot typ cal
let loc = if Typ.Procname.is_java callee_pname then Location.dummy else callee_loc in let loc = if Typ.Procname.is_java callee_pname then Location.dummy else callee_loc in
Pvar.mk_abduced_ret callee_pname loc Pvar.mk_abduced_ret callee_pname loc
in in
if !Config.footprint then if !BiabductionConfig.footprint then
match lookup_abduced_expression prop abduced_ret_pv with match lookup_abduced_expression prop abduced_ret_pv with
| None -> | None ->
let p, fp_var = add_to_footprint tenv abduced_ret_pv typ prop in let p, fp_var = add_to_footprint tenv abduced_ret_pv typ prop in
@ -1044,7 +1044,7 @@ let execute_load ?(report_deref_errors = true) pname pdesc tenv id rhs_exp typ l
with Exceptions.Symexec_memory_error _ -> with Exceptions.Symexec_memory_error _ ->
(* This should normally be a real alarm and should not be caught but currently happens (* This should normally be a real alarm and should not be caught but currently happens
when the normalization drops hpreds of the form ident |-> footprint var. *) when the normalization drops hpreds of the form ident |-> footprint var. *)
let undef = Exp.get_undefined !Config.footprint in let undef = Exp.get_undefined !BiabductionConfig.footprint in
[Prop.conjoin_eq tenv (Exp.Var id) undef prop] ) [Prop.conjoin_eq tenv (Exp.Var id) undef prop] )
with Rearrange.ARRAY_ACCESS -> with Rearrange.ARRAY_ACCESS ->
if Int.equal Config.array_level 0 then assert false if Int.equal Config.array_level 0 then assert false
@ -1195,8 +1195,9 @@ let declare_locals_and_ret tenv pdesc (prop_ : Prop.normal Prop.t) =
in in
sigma_ret :: sigma_locals sigma_ret :: sigma_locals
in in
Config.run_in_re_execution_mode (* no footprint vars for locals *) BiabductionConfig.run_in_re_execution_mode
sigma_locals_and_ret () (* no footprint vars for locals *)
sigma_locals_and_ret ()
in in
let sigma' = prop_.Prop.sigma @ sigma_locals_and_ret in let sigma' = prop_.Prop.sigma @ sigma_locals_and_ret in
let prop' = Prop.normalize tenv (Prop.set prop_ ~sigma:sigma') in let prop' = Prop.normalize tenv (Prop.set prop_ ~sigma:sigma') in
@ -1583,7 +1584,7 @@ and add_constraints_on_actuals_by_ref tenv caller_pdesc prop actuals_by_ref call
in in
(* prevent introducing multiple abduced retvals for a single call site in a loop *) (* prevent introducing multiple abduced retvals for a single call site in a loop *)
if already_has_abduced_retval prop || is_rec_call callee_pname caller_pdesc then prop if already_has_abduced_retval prop || is_rec_call callee_pname caller_pdesc then prop
else if !Config.footprint then else if !BiabductionConfig.footprint then
let prop', abduced_strexp = let prop', abduced_strexp =
match actual_typ.Typ.desc with match actual_typ.Typ.desc with
| Typ.Tptr (({desc= Tstruct _} as typ), _) -> | Typ.Tptr (({desc= Tstruct _} as typ), _) ->
@ -1955,7 +1956,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
State.set_path path None ; State.set_path path None ;
(* Check for retain cycles after assignments and method calls *) (* Check for retain cycles after assignments and method calls *)
( match instr with ( match instr with
| (Sil.Store _ | Sil.Call _) when !Config.footprint -> | (Sil.Store _ | Sil.Call _) when !BiabductionConfig.footprint ->
RetainCycles.report_cycle tenv summary p RetainCycles.report_cycle tenv summary p
| _ -> | _ ->
() ) ; () ) ;
@ -1977,7 +1978,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
L.d_ln () ; L.d_ln () ;
let prop', fav_normal = pre_process_prop prop in let prop', fav_normal = pre_process_prop prop in
let res_list = let res_list =
Config.run_with_abs_val_equal_zero BiabductionConfig.run_with_abs_val_equal_zero
(* no exp abstraction during sym exe *) (* no exp abstraction during sym exe *)
(fun () -> (fun () ->
sym_exec exe_env tenv (ProcCfg.Exceptional.proc_desc proc_cfg) instr prop' path ) sym_exec exe_env tenv (ProcCfg.Exceptional.proc_desc proc_cfg) instr prop' path )
@ -1998,7 +1999,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
Paths.PathSet.from_renamed_list results Paths.PathSet.from_renamed_list results
with exn -> with exn ->
IExn.reraise_if exn ~f:(fun () -> IExn.reraise_if exn ~f:(fun () ->
(not !Config.footprint) || not (Exceptions.handle_exception exn) ) ; (not !BiabductionConfig.footprint) || not (Exceptions.handle_exception exn) ) ;
handle_exn exn ; handle_exn exn ;
(* calls State.mark_instr_fail *) (* calls State.mark_instr_fail *)
Paths.PathSet.empty Paths.PathSet.empty

12
infer/src/biabduction/Tabulation.ml
Unescape View File

@ -82,7 +82,7 @@ let print_results tenv actual_pre results =
let log_call_trace ~caller_name ~callee_name ?callee_attributes ?reason ?dynamic_dispatch loc res = let log_call_trace ~caller_name ~callee_name ?callee_attributes ?reason ?dynamic_dispatch loc res =
if !Config.footprint then if !BiabductionConfig.footprint then
let get_valid_source_file loc = let get_valid_source_file loc =
let file = loc.Location.file in let file = loc.Location.file in
if SourceFile.is_invalid file then None else Some file if SourceFile.is_invalid file then None else Some file
@ -850,7 +850,7 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat
let caller_pname = Procdesc.get_proc_name caller_pdesc in let caller_pname = Procdesc.get_proc_name caller_pdesc in
let instantiated_post = let instantiated_post =
let posts' = let posts' =
if !Config.footprint && List.is_empty posts then if !BiabductionConfig.footprint && List.is_empty posts then
(* in case of divergence, produce a prop *) (* in case of divergence, produce a prop *)
(* with updated footprint and inconsistent current *) (* with updated footprint and inconsistent current *)
[(Prop.set Prop.prop_emp ~pi:[Sil.Aneq (Exp.zero, Exp.zero)], path_pre)] [(Prop.set Prop.prop_emp ~pi:[Sil.Aneq (Exp.zero, Exp.zero)], path_pre)]
@ -959,7 +959,7 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat
assert false ) ) assert false ) )
in in
let post_p4 = let post_p4 =
if !Config.footprint then if !BiabductionConfig.footprint then
prop_footprint_add_pi_sigma_starfld_sigma tenv post_p3 split.missing_pi split.missing_sigma prop_footprint_add_pi_sigma_starfld_sigma tenv post_p3 split.missing_pi split.missing_sigma
split.missing_fld split.missing_typ split.missing_fld split.missing_typ
else Some post_p3 else Some post_p3
@ -1247,10 +1247,10 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
Invalid_res (Dereference_error (deref_error, desc, pjoin)) Invalid_res (Dereference_error (deref_error, desc, pjoin))
| None -> | None ->
let split = do_split () in let split = do_split () in
if (not !Config.footprint) && split.missing_sigma <> [] then ( if (not !BiabductionConfig.footprint) && split.missing_sigma <> [] then (
L.d_strln "Implication error: missing_sigma not empty in re-execution" ; L.d_strln "Implication error: missing_sigma not empty in re-execution" ;
Invalid_res Missing_sigma_not_empty ) Invalid_res Missing_sigma_not_empty )
else if (not !Config.footprint) && missing_fld_not_objc_class <> [] then ( else if (not !BiabductionConfig.footprint) && missing_fld_not_objc_class <> [] then (
L.d_strln "Implication error: missing_fld not empty in re-execution" ; L.d_strln "Implication error: missing_fld not empty in re-execution" ;
Invalid_res Missing_fld_not_empty ) Invalid_res Missing_fld_not_empty )
else report_valid_res split ) else report_valid_res split )
@ -1319,7 +1319,7 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re
let print_pi pi = L.d_str "pi: " ; Prop.d_pi pi ; L.d_ln () in let print_pi pi = L.d_str "pi: " ; Prop.d_pi pi ; L.d_ln () in
let call_desc kind_opt = Localise.desc_precondition_not_met kind_opt callee_pname loc in let call_desc kind_opt = Localise.desc_precondition_not_met kind_opt callee_pname loc in
let res_with_path_idents = let res_with_path_idents =
if !Config.footprint then if !BiabductionConfig.footprint then
if List.is_empty valid_res_cons_pre_missing then ( if List.is_empty valid_res_cons_pre_missing then (
(* no valid results where actual pre and missing are consistent *) (* no valid results where actual pre and missing are consistent *)
match deref_errors with match deref_errors with

41
infer/src/biabduction/interproc.ml
Unescape View File

@ -50,7 +50,7 @@ module NodeVisitSet = Caml.Set.Make (struct
let compare x1 x2 = let compare x1 x2 =
if !Config.footprint then if !BiabductionConfig.footprint then
match Config.worklist_mode with match Config.worklist_mode with
| 0 -> | 0 ->
compare_ids x1.node x2.node compare_ids x1.node x2.node
@ -169,7 +169,8 @@ let path_set_checkout_todo (wl : Worklist.t) (node : Procdesc.Node.t) : Paths.Pa
(* =============== END of the edge_set object =============== *) (* =============== END of the edge_set object =============== *)
let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t = let collect_do_abstract_pre pname tenv (pset : Propset.t) : Propset.t =
if !Config.footprint then Config.run_in_re_execution_mode (Abs.lifted_abstract pname tenv) pset if !BiabductionConfig.footprint then
BiabductionConfig.run_in_re_execution_mode (Abs.lifted_abstract pname tenv) pset
else Abs.lifted_abstract pname tenv pset else Abs.lifted_abstract pname tenv pset
@ -177,8 +178,8 @@ let collect_do_abstract_post pname tenv (pathset : Paths.PathSet.t) : Paths.Path
let abs_option p = let abs_option p =
if Prover.check_inconsistency tenv p then None else Some (Abs.abstract pname tenv p) if Prover.check_inconsistency tenv p then None else Some (Abs.abstract pname tenv p)
in in
if !Config.footprint then if !BiabductionConfig.footprint then
Config.run_in_re_execution_mode (Paths.PathSet.map_option abs_option) pathset BiabductionConfig.run_in_re_execution_mode (Paths.PathSet.map_option abs_option) pathset
else Paths.PathSet.map_option abs_option pathset else Paths.PathSet.map_option abs_option pathset
@ -199,7 +200,8 @@ let do_meet_pre tenv pset =
let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t list = let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t list =
let proc_name = Summary.get_proc_name summary in let proc_name = Summary.get_proc_name summary in
let collect_do_abstract_one tenv prop = let collect_do_abstract_one tenv prop =
if !Config.footprint then Config.run_in_re_execution_mode (Abs.abstract_no_symop tenv) prop if !BiabductionConfig.footprint then
BiabductionConfig.run_in_re_execution_mode (Abs.abstract_no_symop tenv) prop
else Abs.abstract_no_symop tenv prop else Abs.abstract_no_symop tenv prop
in in
let pres = let pres =
@ -282,7 +284,10 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P
curr_node (wl : Worklist.t) = curr_node (wl : Worklist.t) =
let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in
if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then ( if
!BiabductionConfig.footprint
&& not (Paths.PathSet.is_empty (State.get_diverging_states_node ()))
then (
Errdesc.warning_err (State.get_loc_exn ()) "Propagating Divergence@." ; Errdesc.warning_err (State.get_loc_exn ()) "Propagating Divergence@." ;
let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in
let diverging_states = State.get_diverging_states_node () in let diverging_states = State.get_diverging_states_node () in
@ -398,7 +403,7 @@ let do_symbolic_execution exe_env summary proc_cfg handle_exn tenv
let mark_visited summary node = let mark_visited summary node =
let node_id = (Procdesc.Node.get_id node :> int) in let node_id = (Procdesc.Node.get_id node :> int) in
let stats = summary.Summary.stats in let stats = summary.Summary.stats in
if !Config.footprint then Summary.Stats.add_visited_fp stats node_id if !BiabductionConfig.footprint then Summary.Stats.add_visited_fp stats node_id
else Summary.Stats.add_visited_re stats node_id else Summary.Stats.add_visited_re stats node_id
@ -464,7 +469,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
L.d_ln () L.d_ln ()
with exn -> with exn ->
IExn.reraise_if exn ~f:(fun () -> IExn.reraise_if exn ~f:(fun () ->
(not !Config.footprint) || not (Exceptions.handle_exception exn) ) ; (not !BiabductionConfig.footprint) || not (Exceptions.handle_exception exn) ) ;
handle_exn exn ; handle_exn exn ;
L.d_decrease_indent 1 ; L.d_decrease_indent 1 ;
L.d_ln () L.d_ln ()
@ -498,7 +503,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
handle_exn_node curr_node exn ; handle_exn_node curr_node exn ;
Printer.force_delayed_prints () ; Printer.force_delayed_prints () ;
do_after_node curr_node ; do_after_node curr_node ;
if not !Config.footprint then raise RE_EXE_ERROR if not !BiabductionConfig.footprint then raise RE_EXE_ERROR
in in
while not (Worklist.is_empty wl) do while not (Worklist.is_empty wl) do
let curr_node = Worklist.remove wl in let curr_node = Worklist.remove wl in
@ -738,7 +743,7 @@ let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop.prop_emp t
(** Construct an initial prop from an existing pre with formals *) (** Construct an initial prop from an existing pre with formals *)
let initial_prop_from_pre tenv curr_f pre = let initial_prop_from_pre tenv curr_f pre =
if !Config.footprint then if !BiabductionConfig.footprint then
let vars = Prop.free_vars pre |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in let vars = Prop.free_vars pre |> Ident.hashqueue_of_sequence |> Ident.HashQueue.keys in
let sub_list = let sub_list =
List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.kfootprint))) vars List.map ~f:(fun id -> (id, Exp.Var (Ident.create_fresh Ident.kfootprint))) vars
@ -922,7 +927,7 @@ let set_current_language proc_desc =
(** reset global values before analysing a procedure *) (** reset global values before analysing a procedure *)
let reset_global_values proc_desc = let reset_global_values proc_desc =
Config.reset_abs_val () ; BiabductionConfig.reset_abs_val () ;
Ident.NameGenerator.reset () ; Ident.NameGenerator.reset () ;
SymOp.reset_total () ; SymOp.reset_total () ;
reset_prop_metrics () ; reset_prop_metrics () ;
@ -1196,7 +1201,7 @@ let perform_transition proc_cfg tenv proc_name summary =
let transition summary = let transition summary =
(* disable exceptions for leaks and protect against any other errors *) (* disable exceptions for leaks and protect against any other errors *)
let joined_pres = let joined_pres =
let allow_leak = !Config.allow_leak in let allow_leak = !BiabductionConfig.allow_leak in
(* apply the start node to f, and do nothing in case of exception *) (* apply the start node to f, and do nothing in case of exception *)
let apply_start_node f = let apply_start_node f =
try f (ProcCfg.Exceptional.start_node proc_cfg) try f (ProcCfg.Exceptional.start_node proc_cfg)
@ -1204,14 +1209,14 @@ let perform_transition proc_cfg tenv proc_name summary =
in in
apply_start_node (do_before_node 0) ; apply_start_node (do_before_node 0) ;
try try
Config.allow_leak := true ; BiabductionConfig.allow_leak := true ;
let res = collect_preconditions tenv summary in let res = collect_preconditions tenv summary in
Config.allow_leak := allow_leak ; BiabductionConfig.allow_leak := allow_leak ;
apply_start_node do_after_node ; apply_start_node do_after_node ;
res res
with exn when SymOp.exn_not_failure exn -> with exn when SymOp.exn_not_failure exn ->
apply_start_node do_after_node ; apply_start_node do_after_node ;
Config.allow_leak := allow_leak ; BiabductionConfig.allow_leak := allow_leak ;
L.(debug Analysis Medium) L.(debug Analysis Medium)
"Error in collect_preconditions for %a@." Typ.Procname.pp proc_name ; "Error in collect_preconditions for %a@." Typ.Procname.pp proc_name ;
let error = Exceptions.recognize_exception exn in let error = Exceptions.recognize_exception exn in
@ -1233,10 +1238,12 @@ let analyze_procedure_aux summary exe_env tenv proc_desc : Summary.t =
let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in let proc_cfg = ProcCfg.Exceptional.from_pdesc proc_desc in
Preanal.do_preanalysis proc_desc tenv ; Preanal.do_preanalysis proc_desc tenv ;
let summaryfp = let summaryfp =
Config.run_in_footprint_mode (analyze_proc summary exe_env tenv) proc_cfg BiabductionConfig.run_in_footprint_mode (analyze_proc summary exe_env tenv) proc_cfg
|> perform_transition proc_cfg tenv proc_name |> perform_transition proc_cfg tenv proc_name
in in
let summaryre = Config.run_in_re_execution_mode (analyze_proc summaryfp exe_env tenv) proc_cfg in let summaryre =
BiabductionConfig.run_in_re_execution_mode (analyze_proc summaryfp exe_env tenv) proc_cfg
in
let summary_compact = let summary_compact =
match summaryre.Summary.payloads.biabduction with match summaryre.Summary.payloads.biabduction with
| Some BiabductionSummary.({preposts} as biabduction) when Config.save_compact_summaries -> | Some BiabductionSummary.({preposts} as biabduction) when Config.save_compact_summaries ->

Write Preview
Loading…
Cancel
Save