From 5b1e64e84b3c039d418668ef17d9f30ae35e9b95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 28 Mar 2019 17:37:26 +0100
Subject: [PATCH] [Eva] New module type Abstractions.Eva: all abstractions and
the evaluator.
This module type simplifies the signature of functors using evaluation
functions.
---
Makefile | 4 +-
src/plugins/value/engine/abstractions.ml | 8 ++-
src/plugins/value/engine/abstractions.mli | 12 +++-
src/plugins/value/engine/analysis.ml | 10 ++--
src/plugins/value/engine/compute_functions.ml | 52 +++++-----------
.../value/engine/compute_functions.mli | 7 +--
.../value/engine/transfer_specification.ml | 12 ++--
.../value/engine/transfer_specification.mli | 16 ++---
src/plugins/value/engine/transfer_stmt.ml | 60 +++++++++----------
src/plugins/value/engine/transfer_stmt.mli | 16 ++---
10 files changed, 87 insertions(+), 110 deletions(-)
diff --git a/Makefile b/Makefile
index f517edfe058..08279956546 100644
--- a/Makefile
+++ b/Makefile
@@ -913,12 +913,12 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
domains/cvalue/cvalue_specification \
domains/cvalue/cvalue_domain \
- engine/subdivided_evaluation engine/evaluation \
+ engine/subdivided_evaluation engine/evaluation engine/abstractions \
engine/recursion engine/transfer_stmt engine/transfer_specification \
engine/partitioning engine/mem_exec \
engine/legacy_partitioning engine/basic_partitioning \
engine/loop_partitioning engine/partitioned_dataflow \
- engine/initialization engine/abstractions \
+ engine/initialization \
engine/compute_functions engine/analysis register
PLUGIN_CMI:= values/abstract_value values/abstract_location \
engine/state_partitioning \
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index a15c6bb25a6..117b2a5e4fe 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -83,11 +83,17 @@ end
module type S = sig
module Val : Value
module Loc : Abstract_location.External with type value = Val.t
- and type location = Precise_locs.precise_location
module Dom : Abstract_domain.External with type value = Val.t
and type location = Loc.location
end
+module type Eva = sig
+ include S
+ module Eval: Evaluation.S with type state = Dom.t
+ and type value = Val.t
+ and type loc = Loc.location
+ and type origin = Dom.origin
+end
(* -------------------------------------------------------------------------- *)
(* Value Abstraction *)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 499cb28161d..9b3a1fb81ed 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -61,11 +61,21 @@ end
module type S = sig
module Val : Value
module Loc : Abstract_location.External with type value = Val.t
- and type location = Precise_locs.precise_location
module Dom : Abstract_domain.External with type value = Val.t
and type location = Loc.location
end
+(** Module gathering:
+ - the analysis abstractions: value, location and state abstractions;
+ - the evaluation functions for these abstractions. *)
+module type Eva = sig
+ include S
+ module Eval: Evaluation.S with type state = Dom.t
+ and type value = Val.t
+ and type loc = Loc.location
+ and type origin = Dom.origin
+end
+
(** Type of abstractions that use the builtin types for values and locations *)
module type Standard_abstraction = Abstract_domain.Internal
with type value = Cvalue.V.t
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index d11f2ec4640..402aea1875c 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -59,11 +59,13 @@ end
module Make (Abstract: Abstractions.S) = struct
- include Abstract
-
- module Eval = Evaluation.Make (Abstract.Val) (Abstract.Loc) (Abstract.Dom)
+ module Abstract = struct
+ include Abstract
+ module Eval = Evaluation.Make (Abstract.Val) (Abstract.Loc) (Abstract.Dom)
+ end
- include Compute_functions.Make (Abstract) (Eval)
+ include Abstract
+ include Compute_functions.Make (Abstract)
let get_stmt_state stmt =
let fundec = Kernel_function.(get_definition (find_englobing_kf stmt)) in
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 8d30fe87260..409a3b2a285 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -132,44 +132,24 @@ let () =
| Sys.Signal_handle f -> prev := f
with Invalid_argument _ -> () (* Ignore: SIGURSR1 is not available on Windows,
and possibly on other platforms. *)
-module Make
- (Abstract: Abstractions.S)
- (Eva: Evaluation.S with type value = Abstract.Val.t
- and type origin = Abstract.Dom.origin
- and type loc = Abstract.Loc.location
- and type state = Abstract.Dom.t)
-= struct
-
- module Domain = struct
- include Abstract.Dom
- let enter_scope kf vars state = match vars with
- | [] -> state
- | _ -> enter_scope kf vars state
- let leave_scope kf vars state = match vars with
- | [] -> state
- | _ -> leave_scope kf vars state
- end
- module PowersetDomain = Powerset.Make (Domain)
-
- module Transfer =
- Transfer_stmt.Make (Abstract.Val) (Abstract.Loc) (Domain) (Eva)
- module Logic = Transfer_logic.Make (Domain) (PowersetDomain)
+module Make (Abstract: Abstractions.Eva) = struct
- module Spec =
- Transfer_specification.Make
- (Abstract.Val) (Abstract.Loc) (Domain) (PowersetDomain) (Logic)
+ module PowersetDomain = Powerset.Make (Abstract.Dom)
- module Init = Initialization.Make (Abstract.Dom) (Eva) (Transfer)
+ module Transfer = Transfer_stmt.Make (Abstract)
+ module Logic = Transfer_logic.Make (Abstract.Dom) (PowersetDomain)
+ module Spec = Transfer_specification.Make (Abstract) (PowersetDomain) (Logic)
+ module Init = Initialization.Make (Abstract.Dom) (Abstract.Eval) (Transfer)
module Computer =
Partitioned_dataflow.Computer
- (Domain) (PowersetDomain) (Transfer) (Init) (Logic) (Spec)
+ (Abstract.Dom) (PowersetDomain) (Transfer) (Init) (Logic) (Spec)
let initial_state = Init.initial_state
let get_cvalue =
- match Domain.get Cvalue_domain.key with
+ match Abstract.Dom.get Cvalue_domain.key with
| None -> fun _ -> Cvalue.Model.top
| Some get -> fun state -> get state
@@ -237,7 +217,7 @@ module Make
(* Mem Exec *)
- module MemExec = Mem_exec.Make (Abstract.Val) (Domain)
+ module MemExec = Mem_exec.Make (Abstract.Val) (Abstract.Dom)
let compute_and_cache_call stmt call init_state =
let default () = compute_using_spec_or_body (Kstmt stmt) call init_state in
@@ -299,7 +279,7 @@ module Make
let join_states = function
| [] -> `Bottom
| [state] -> `Value state
- | s :: l -> `Value (List.fold_left Domain.join s l)
+ | s :: l -> `Value (List.fold_left Abstract.Dom.join s l)
let compute_call_or_builtin stmt call state =
match Builtins.find_builtin_override call.kf with
@@ -333,14 +313,14 @@ module Make
Builtins.apply_builtin builtin cvalue_call cvalue_state
in
let insert (cvalue_state, clobbered_set) =
- Domain.set Locals_scoping.key clobbered_set
- (Domain.set Cvalue_domain.key cvalue_state final_state)
+ Abstract.Dom.set Locals_scoping.key clobbered_set
+ (Abstract.Dom.set Cvalue_domain.key cvalue_state final_state)
in
let states = Bottom.bot_of_list (List.map insert cvalue_states) in
Transfer.{states; cacheable; builtin=true}
let compute_call =
- if Domain.mem Cvalue_domain.key
+ if Abstract.Dom.mem Cvalue_domain.key
&& Abstract.Val.mem Main_values.cvalue_key
&& Abstract.Loc.mem Main_locations.ploc_key
then compute_call_or_builtin
@@ -349,7 +329,7 @@ module Make
let () = Transfer.compute_call_ref := compute_call
let store_initial_state kf init_state =
- Domain.Store.register_initial_state (Value_util.call_stack ()) init_state;
+ Abstract.Dom.Store.register_initial_state (Value_util.call_stack ()) init_state;
let cvalue_state = get_cvalue init_state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
@@ -366,7 +346,7 @@ module Make
Value_util.pop_call_stack ();
Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
post_analysis ();
- Domain.post_analysis final_state;
+ Abstract.Dom.post_analysis final_state;
with
| Db.Value.Aborted ->
post_analysis_cleanup ~aborted:true;
@@ -398,7 +378,7 @@ module Make
let compute_from_init_state kf init_state =
pre_analysis ();
- Domain.Store.register_global_state (`Value init_state);
+ Abstract.Dom.Store.register_global_state (`Value init_state);
compute kf init_state
end
diff --git a/src/plugins/value/engine/compute_functions.mli b/src/plugins/value/engine/compute_functions.mli
index 2e04b81105c..3e1db0817b9 100644
--- a/src/plugins/value/engine/compute_functions.mli
+++ b/src/plugins/value/engine/compute_functions.mli
@@ -25,12 +25,7 @@
open Cil_types
open Eval
-module Make
- (Abstract: Abstractions.S)
- (Eva: Evaluation.S with type value = Abstract.Val.t
- and type origin = Abstract.Dom.origin
- and type loc = Abstract.Loc.location
- and type state = Abstract.Dom.t)
+module Make (Abstract: Abstractions.Eva)
: sig
(** Compute a call to the main function. *)
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index dc968ee3006..5515e44a3b8 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -165,15 +165,15 @@ let precise_loc_of_assign env assign_or_allocation =
module Make
- (Value: Abstract_value.External)
- (Location: Abstract_location.External)
- (Domain: Abstract_domain.External with type value = Value.t
- and type location = Location.location)
- (States: Powerset.S with type state = Domain.t)
- (Logic : Transfer_logic.S with type state = Domain.t
+ (Abstract: Abstractions.S)
+ (States: Powerset.S with type state = Abstract.Dom.t)
+ (Logic : Transfer_logic.S with type state = Abstract.Dom.t
and type states = States.t)
= struct
+ module Domain = Abstract.Dom
+ module Location = Abstract.Loc
+
(* Most transfer functions about logic return a set of states instead of a
single state, and States.empty instead of bottom. We thus use this monad
to turn `Bottom into States.empty in the following for consistency. *)
diff --git a/src/plugins/value/engine/transfer_specification.mli b/src/plugins/value/engine/transfer_specification.mli
index 056587e6cbb..dfb86ee93c2 100644
--- a/src/plugins/value/engine/transfer_specification.mli
+++ b/src/plugins/value/engine/transfer_specification.mli
@@ -24,21 +24,17 @@ open Cil_types
open Eval
module Make
- (Value: Abstract_value.External)
- (Location: Abstract_location.External)
- (Domain: Abstract_domain.External with type value = Value.t
- and type location = Location.location)
- (States: Powerset.S with type state = Domain.t)
- (Logic : Transfer_logic.S with type state = Domain.t
+ (Abstract: Abstractions.S)
+ (States: Powerset.S with type state = Abstract.Dom.t)
+ (Logic : Transfer_logic.S with type state = Abstract.Dom.t
and type states = States.t)
: sig
-
- val treat_statement_assigns: assigns -> Domain.t -> Domain.t
+ val treat_statement_assigns: assigns -> Abstract.Dom.t -> Abstract.Dom.t
val compute_using_specification:
warn:bool ->
- kinstr -> (Location.location, Value.t) call -> spec ->
- Domain.t -> Domain.t list or_bottom
+ kinstr -> (Abstract.Loc.location, Abstract.Val.t) call -> spec ->
+ Abstract.Dom.t -> Abstract.Dom.t list or_bottom
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 2a2ac4ca72b..dedb9086728 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -101,23 +101,19 @@ module DumpFileCounters =
let name = "Transfer_stmt.DumpFileCounters"
end)
-module Make
- (Value: Abstract_value.External)
- (Location: Abstract_location.External)
- (Domain: Abstract_domain.External with type value = Value.t
- and type location = Location.location)
- (Eva: Evaluation.S with type state = Domain.state
- and type value = Domain.value
- and type loc = Domain.location
- and type origin = Domain.origin)
-= struct
-
- type state = Domain.state
- type value = Domain.value
- type location = Domain.location
+module Make (Abstract: Abstractions.Eva) = struct
+
+ module Value = Abstract.Val
+ module Location = Abstract.Loc
+ module Domain = Abstract.Dom
+ module Eval = Abstract.Eval
+
+ type state = Domain.t
+ type value = Value.t
+ type location = Location.location
(* Transfer functions. *)
- module TF = Domain.Transfer (Eva.Valuation)
+ module TF = Domain.Transfer (Eval.Valuation)
(* When using a product of domains, a product of states may have no
concretization (if the domains have inferred incompatible properties)
@@ -157,17 +153,17 @@ module Make
if they lead to bottom without alarms. *)
let evaluate_and_check ?valuation state expr =
- let res = Eva.evaluate ?valuation state expr in
+ let res = Eval.evaluate ?valuation state expr in
report_unreachability state res "the expression %a" Printer.pp_exp expr;
res
let lvaluate_and_check ~for_writing ?valuation state lval =
- let res = Eva.lvaluate ~for_writing ?valuation state lval in
+ let res = Eval.lvaluate ~for_writing ?valuation state lval in
report_unreachability state res "the lvalue %a" Printer.pp_lval lval;
res
let copy_lvalue_and_check ?valuation state lval =
- let res = Eva.copy_lvalue ?valuation state lval in
+ let res = Eval.copy_lvalue ?valuation state lval in
report_unreachability state res "the copy of %a" Printer.pp_lval lval;
res
@@ -217,7 +213,7 @@ module Make
then
let truth = Location.assume_no_overlap ~partial:true loc right_loc in
let alarm () = Alarms.Overlap (lval, right_lval) in
- Eva.interpret_truth ~alarm (loc, right_loc) truth
+ Eval.interpret_truth ~alarm (loc, right_loc) truth
else `Value (loc, right_loc), Alarmset.none
(* Checks the compatibility between the left and right locations of a copy. *)
@@ -273,7 +269,7 @@ module Make
(* Assumption. *)
let assume state stmt expr positive =
- let eval, alarms = Eva.reduce state expr positive in
+ let eval, alarms = Eval.reduce state expr positive in
(* TODO: check not comparable. *)
Alarmset.emit (Kstmt stmt) alarms;
eval >>- fun valuation ->
@@ -345,7 +341,7 @@ module Make
| None -> default valuation expr
| Some inout ->
let find_loc lval =
- match Eva.Valuation.find_loc valuation lval with
+ match Eval.Valuation.find_loc valuation lval with
| `Top -> Precise_locs.loc_top
| `Value record -> get record.loc
in
@@ -378,7 +374,7 @@ module Make
reduced, and their new (more precise) value. *)
let gather_reduced_arguments call valuation state =
let safe_arguments = filter_safe_arguments valuation call in
- let empty = Eva.Valuation.empty in
+ let empty = Eval.Valuation.empty in
let reduce_one_argument acc argument =
acc >>- fun acc ->
let pre_value = match argument.avalue with
@@ -393,7 +389,7 @@ module Make
If the call has copied the argument, it may be uninitialized. Thus,
we also avoid the backward propagation if the formal is uninitialized
here. This should not happen in the Assign case above. *)
- fst (Eva.copy_lvalue ~valuation:empty state lval)
+ fst (Eval.copy_lvalue ~valuation:empty state lval)
>>- fun (_valuation, post_value) ->
if
Bottom.is_included Value.is_included pre_value post_value.v
@@ -407,10 +403,10 @@ module Make
This function reduces the [state] by assuming [expr = value] for each pair
(expr, value) of [reductions]. *)
let reduce_arguments reductions state =
- let valuation = `Value Eva.Valuation.empty in
+ let valuation = `Value Eval.Valuation.empty in
let reduce_one_argument valuation (argument, post_value) =
valuation >>- fun valuation ->
- Eva.assume ~valuation state argument.concrete post_value
+ Eval.assume ~valuation state argument.concrete post_value
in
List.fold_left reduce_one_argument valuation reductions >>-: fun valuation ->
TF.update valuation state
@@ -602,7 +598,7 @@ module Make
let domain_show_each name arguments state =
let pretty fmt expr =
let pp fmt =
- match fst (Eva.evaluate state expr) with
+ match fst (Eval.evaluate state expr) with
| `Bottom -> Format.fprintf fmt "%s" (Unicode.bottom_string ())
| `Value (valuation, _value) -> show_expr valuation state fmt expr
in
@@ -625,7 +621,7 @@ module Make
begin
try
let offsm =
- fst (Eva.lvaluate ~for_writing:false state lval)
+ fst (Eval.lvaluate ~for_writing:false state lval)
>>- fun (_, loc, _) ->
let ploc = get_ploc loc
and cvalue_state = get_cvalue state in
@@ -644,7 +640,7 @@ module Make
| None -> fun fmt _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cval ->
fun fmt expr state ->
- let value = fst (Eva.evaluate state expr) >>-: snd >>-: get_cval in
+ let value = fst (Eval.evaluate state expr) >>-: snd >>-: get_cval in
(Bottom.pretty Cvalue.V.pretty) fmt value
let pretty_arguments state arguments =
@@ -734,7 +730,7 @@ module Make
let cacheable = ref Value_types.Cacheable in
let eval =
(* Resolve [funcexp] into the called kernel functions. *)
- let functions, alarms = Eva.eval_function_exp funcexp ~args state in
+ let functions, alarms = Eval.eval_function_exp funcexp ~args state in
Alarmset.emit ki_call alarms;
functions >>- fun functions ->
let current_kf = Value_util.current_kf () in
@@ -781,7 +777,7 @@ module Make
if Cil.isIntegralOrPointerType varinfo.vtype
then
let matched, tail =
- Eva.split_by_evaluation return_expr expected_values states
+ Eval.split_by_evaluation return_expr expected_values states
in
let process (i, states, mess) =
if mess then
@@ -809,14 +805,14 @@ module Make
let check_non_overlapping state lvs1 lvs2 =
let eval_loc (acc, valuation) lval =
- match fst (Eva.lvaluate ~valuation ~for_writing:false state lval) with
+ match fst (Eval.lvaluate ~valuation ~for_writing:false state lval) with
| `Bottom -> acc, valuation
| `Value (valuation, loc, _) -> (lval, loc) :: acc, valuation
in
let eval_list valuation lvs =
List.fold_left eval_loc ([], valuation) lvs
in
- let list1, valuation = eval_list Eva.Valuation.empty lvs1 in
+ let list1, valuation = eval_list Eval.Valuation.empty lvs1 in
let list2, _ = eval_list valuation lvs2 in
let check acc (lval1, loc1) (lval2, loc2) =
let truth = Location.assume_no_overlap ~partial:false loc1 loc2 in
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index 3fb197fdbc0..a2e64699a2e 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -61,18 +61,10 @@ module type S = sig
(stmt -> (location, value) call -> state -> call_result) ref
end
-module Make
- (Value: Abstract_value.External)
- (Location: Abstract_location.External)
- (Domain: Abstract_domain.External with type value = Value.t
- and type location = Location.location)
- (Eva: Evaluation.S with type state = Domain.state
- and type value = Domain.value
- and type loc = Domain.location
- and type origin = Domain.origin)
- : S with type state = Domain.state
- and type value = Domain.value
- and type location = Domain.location
+module Make (Abstract: Abstractions.Eva)
+ : S with type state = Abstract.Dom.t
+ and type value = Abstract.Val.t
+ and type location = Abstract.Loc.location
(*
Local Variables:
--
GitLab