From e590d32f230762c0184f4b14dc5bd62eea4dfc01 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 4 Sep 2020 17:26:52 +0200
Subject: [PATCH] [Inout] Completely remove option -inout-callwise, which is
always active.
---
.../plugin_entry_points/db.mli | 3 +-
src/plugins/inout/inout_parameters.ml | 15 --
src/plugins/inout/inout_parameters.mli | 1 -
src/plugins/inout/operational_inputs.ml | 131 ++++++++----------
src/plugins/value/value_parameters.ml | 11 +-
tests/builtins/realloc2.c | 2 +-
6 files changed, 64 insertions(+), 99 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 360b783ab48..30c474f13e5 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1317,8 +1317,7 @@ module Operational_inputs : sig
val get_internal_precise: (?stmt:stmt -> kernel_function -> Inout_type.t) ref
(** More precise version of [get_internal] function. If [stmt] is
specified, and is a possible call to the given kernel_function,
- returns the operational inputs for this call (if option -inout-callwise
- has been set). *)
+ returns the operational inputs for this call. *)
(**/**)
(* Internal use *)
diff --git a/src/plugins/inout/inout_parameters.ml b/src/plugins/inout/inout_parameters.ml
index d40e57102ef..eef83915883 100644
--- a/src/plugins/inout/inout_parameters.ml
+++ b/src/plugins/inout/inout_parameters.ml
@@ -77,21 +77,6 @@ module ForceInout =
let help = "Compute operational inputs, an over-approximation of the set of locations whose initial value is used; and the sure outputs, an under-approximation of the set of the certainly written locations"
end)
-(* Remove in Frama-C Chlorine *)
-let () = Parameter_customize.is_invisible ()
-module ForceCallwiseInout =
- True
- (struct
- let option_name = "-inout-callwise"
- let help = "Compute callsite-wide operational inputs; this results in more precise results for -inout and -out options"
- end)
-let () =
- ForceCallwiseInout.add_update_hook
- (fun _ new_ ->
- if not new_ then
- Kernel.abort "@[option -inout-callwise can no longer be unset.@]")
-
-
module ForceInoutExternalWithFormals =
False
(struct
diff --git a/src/plugins/inout/inout_parameters.mli b/src/plugins/inout/inout_parameters.mli
index 3f5390706a6..d59478b1bb4 100644
--- a/src/plugins/inout/inout_parameters.mli
+++ b/src/plugins/inout/inout_parameters.mli
@@ -28,7 +28,6 @@ module ForceExternalOut: Parameter_sig.Bool
module ForceInput: Parameter_sig.Bool
module ForceInputWithFormals: Parameter_sig.Bool
module ForceInout: Parameter_sig.Bool
-module ForceCallwiseInout: Parameter_sig.Bool
module ForceInoutExternalWithFormals: Parameter_sig.Bool
module ForceDeref: Parameter_sig.Bool
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 777c7ce0892..f1c1fe4aa45 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -215,16 +215,14 @@ module Internals =
module CallsiteHash = Value_types.Callsite.Hashtbl
(* Results of an an entire call, represented by a pair (stmt, kernel_function).
- This table is filled by the [-inout-callwise] option, or for functions for
- which only the specification is used. *)
+*)
module CallwiseResults =
State_builder.Hashtbl
(Value_types.Callsite.Hashtbl)
(Inout_type)
(struct
let size = 17
- let dependencies = [Internals.self;
- Inout_parameters.ForceCallwiseInout.self]
+ let dependencies = [Internals.self]
let name = "Inout.Operational_inputs.CallwiseResults"
end)
@@ -565,10 +563,6 @@ let extract_inout_from_froms froms =
module Callwise = struct
- let compute_callwise () =
- Inout_parameters.ForceCallwiseInout.get () ||
- Dynamic.Parameter.Bool.get "-memexec-all" ()
-
let merge_call_in_local_table call local_table v =
let prev =
try CallsiteHash.find local_table call
@@ -600,41 +594,39 @@ module Callwise = struct
let call_inout_stack = ref []
let call_for_callwise_inout (call_type, state, call_stack) =
- if compute_callwise () then begin
- let (current_function, ki as call_site) = List.hd call_stack in
- let merge_inout inout =
- if ki = Kglobal
- then merge_call_in_global_tables call_site inout
- else
- let _above_function, table =
- try List.hd !call_inout_stack
- with Failure _ -> assert false
- in
- merge_call_in_local_table call_site table inout
- in
- match call_type with
- | `Builtin {Value_types.c_from = Some (froms,sure_out) } ->
- let in_, out_ = extract_inout_from_froms froms in
- let inout = {
- over_inputs_if_termination = in_;
- over_inputs = in_;
- over_logic_inputs = Zone.bottom;
- over_outputs_if_termination = out_ ;
- over_outputs = out_;
- under_outputs_if_termination = sure_out;
- } in
- merge_inout inout
- | `Def | `Memexec ->
- let table_current_function = CallsiteHash.create 7 in
- call_inout_stack :=
- (current_function, table_current_function) :: !call_inout_stack
- | `Spec spec ->
- let inout =compute_using_given_spec_state state spec current_function in
- merge_inout inout
- | `Builtin { Value_types.c_from = None } ->
- let inout = compute_using_prototype_state state current_function in
- merge_inout inout
- end;;
+ let (current_function, ki as call_site) = List.hd call_stack in
+ let merge_inout inout =
+ if ki = Kglobal
+ then merge_call_in_global_tables call_site inout
+ else
+ let _above_function, table =
+ try List.hd !call_inout_stack
+ with Failure _ -> assert false
+ in
+ merge_call_in_local_table call_site table inout
+ in
+ match call_type with
+ | `Builtin {Value_types.c_from = Some (froms,sure_out) } ->
+ let in_, out_ = extract_inout_from_froms froms in
+ let inout = {
+ over_inputs_if_termination = in_;
+ over_inputs = in_;
+ over_logic_inputs = Zone.bottom;
+ over_outputs_if_termination = out_ ;
+ over_outputs = out_;
+ under_outputs_if_termination = sure_out;
+ } in
+ merge_inout inout
+ | `Def | `Memexec ->
+ let table_current_function = CallsiteHash.create 7 in
+ call_inout_stack :=
+ (current_function, table_current_function) :: !call_inout_stack
+ | `Spec spec ->
+ let inout =compute_using_given_spec_state state spec current_function in
+ merge_inout inout
+ | `Builtin { Value_types.c_from = None } ->
+ let inout = compute_using_prototype_state state current_function in
+ merge_inout inout
module MemExec =
@@ -711,31 +703,30 @@ module Callwise = struct
Computer.end_dataflow ()
let record_for_callwise_inout ((call_stack: Db.Value.callstack), value_res) =
- if compute_callwise () then
- let inout = match value_res with
- | Value_types.Normal (states, _after_states)
- | Value_types.NormalStore ((states, _after_states), _) ->
- let kf, _ = List.hd call_stack in
- let inout =
- try
- if !Db.Value.no_results (Kernel_function.get_definition kf) then
- top
- else
- compute_call_from_value_states kf call_stack (Lazy.force states)
- with Kernel_function.No_Definition -> top
- in
- (match value_res with
- | Value_types.NormalStore (_, memexec_counter) ->
- MemExec.replace memexec_counter inout
- | _ -> ());
- inout
-
- | Value_types.Reuse counter ->
- MemExec.find counter
- in
- Db.Operational_inputs.Record_Inout_Callbacks.apply
- (call_stack, inout);
- end_record call_stack inout
+ let inout = match value_res with
+ | Value_types.Normal (states, _after_states)
+ | Value_types.NormalStore ((states, _after_states), _) ->
+ let kf, _ = List.hd call_stack in
+ let inout =
+ try
+ if !Db.Value.no_results (Kernel_function.get_definition kf) then
+ top
+ else
+ compute_call_from_value_states kf call_stack (Lazy.force states)
+ with Kernel_function.No_Definition -> top
+ in
+ (match value_res with
+ | Value_types.NormalStore (_, memexec_counter) ->
+ MemExec.replace memexec_counter inout
+ | _ -> ());
+ inout
+
+ | Value_types.Reuse counter ->
+ MemExec.find counter
+ in
+ Db.Operational_inputs.Record_Inout_Callbacks.apply
+ (call_stack, inout);
+ end_record call_stack inout
(* Register our callbacks inside the value analysis *)
@@ -816,8 +807,8 @@ let get_internal =
Internals.memo
(fun kf ->
!Db.Value.compute ();
- try Internals.find kf (* If [-inout-callwise] is set, the results may
- have been computed by the call to Value.compute *)
+ try Internals.find kf (* The results may have been computed by the call
+ to Value.compute *)
with
| Not_found ->
if!Db.Value.use_spec_instead_of_definition kf then
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 353dd6bb25c..1446dd8d796 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1016,19 +1016,10 @@ module MemExecAll =
(struct
let option_name = "-eva-memexec"
let help = "Speed up analysis by not recomputing functions already \
- analyzed in the same context. Forces -inout-callwise. \
+ analyzed in the same context. \
Callstacks for which the analysis has not been recomputed \
are incorrectly shown as dead in the GUI."
end)
-let () =
- MemExecAll.add_set_hook
- (fun _bold bnew ->
- if bnew then
- try
- Dynamic.Parameter.Bool.set "-inout-callwise" true
- with Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ ->
- abort "Cannot set option -eva-memexec. Is plugin Inout registered?"
- )
let () = Parameter_customize.set_group precision_tuning
module ArrayPrecisionLevel =
diff --git a/tests/builtins/realloc2.c b/tests/builtins/realloc2.c
index 6614f80f06f..3636bd1ea2a 100644
--- a/tests/builtins/realloc2.c
+++ b/tests/builtins/realloc2.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: #"-eva-mlevel 0 -inout-callwise -inout-no-print "
+ STDOPT: #"-eva-mlevel 0 -inout-no-print "
*/
#include <stdlib.h>
--
GitLab