diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 13a6e265714a9c2c28b8b8977a32699613169d52..cac999676f65a89e8938639c4120039094b8d4eb 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -144,7 +144,7 @@ module Make (Abstract: Abstractions.Eva) = struct
module Computer =
Partitioned_dataflow.Computer
- (Abstract.Dom) (PowersetDomain) (Transfer) (Init) (Logic) (Spec)
+ (Abstract) (PowersetDomain) (Transfer) (Init) (Logic) (Spec)
let initial_state = Init.initial_state
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index a1825d939edc2ceb6b605f688cb95bea744aa54d..6c5c152d4d366e960953ad8997d6afada1f9f061 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Bottom.Type
+
(* --- Split monitors --- *)
type split_monitor = {
@@ -147,24 +149,11 @@ type action =
exception InvalidAction
-
(* --- Flows --- *)
-module type InputDomain =
-sig
- type t
-
- exception Operation_failed
-
- val join : t -> t -> t
- val split : monitor:split_monitor ->
- t -> Cil_types.exp -> (Integer.t * t) list
- val eval_exp_to_int : t -> Cil_types.exp -> int
-end
-
-module MakeFlow (Domain : InputDomain) =
+module MakeFlow (Abstract: Abstractions.Eva) =
struct
- type state = Domain.t
+ type state = Abstract.Dom.t
type t = (key * state) list
let empty = []
@@ -183,7 +172,7 @@ struct
(* Join states with the same key *)
let x' =
try
- Domain.join (KMap.find k p) x
+ Abstract.Dom.join (KMap.find k p) x
with Not_found -> x
in
KMap.add k x' p
@@ -199,6 +188,113 @@ struct
let union (p1 : t) (p2 : t) : t =
p1 @ p2
+ (* --- Evalution and split functions -------------------------------------- *)
+
+ (* Domains transfer functions. *)
+ module TF = Abstract.Dom.Transfer (Abstract.Eval.Valuation)
+
+ exception Operation_failed
+
+ let fail ~exp message =
+ let source = fst exp.Cil_types.eloc in
+ let warn_and_raise message =
+ Value_parameters.warning ~source ~once:true "%s" message;
+ raise Operation_failed
+ in
+ Pretty_utils.ksfprintf warn_and_raise message
+
+ let evaluate_exp_to_ival ?valuation state exp =
+ (* Evaluate the expression *)
+ let valuation, value =
+ match Abstract.Eval.evaluate ?valuation ~reduction:false state exp with
+ | `Value (valuation, value), alarms when Alarmset.is_empty alarms ->
+ valuation, value
+ | _ ->
+ fail ~exp "this partitioning parameter cannot be evaluated safely on \
+ all states"
+ in
+ (* Get the cvalue *)
+ let cvalue = match Abstract.Val.get Main_values.cvalue_key with
+ | Some get_cvalue -> get_cvalue value
+ | None -> fail ~exp "partitioning is disabled when the CValue domain is \
+ not active"
+ in
+ (* Extract the ival *)
+ let ival =
+ try
+ Cvalue.V.project_ival cvalue
+ with Cvalue.V.Not_based_on_null ->
+ fail ~exp "this partitioning parameter must evaluate to an integer"
+ in
+ valuation, ival
+
+ exception Split_limit of Integer.t option
+
+ let split_by_value ~monitor state exp =
+ let module SplitValues = Datatype.Integer.Set in
+ let valuation, ival = evaluate_exp_to_ival state exp in
+ (* Build a state with the lvalue set to a singleton *)
+ let build i acc =
+ let value = Abstract.Val.inject_int (Cil.typeOf exp) i in
+ let state =
+ Abstract.Eval.assume ~valuation state exp value >>- fun valuation ->
+ (* Check the reduction *)
+ TF.update valuation state
+ in
+ match state with
+ | `Value state ->
+ let _,new_ival = evaluate_exp_to_ival state exp in
+ if not (Ival.is_singleton_int new_ival) then
+ fail ~exp "failing to learn perfectly from split" ;
+ monitor.split_values <-
+ SplitValues.add i monitor.split_values;
+ (i, state) :: acc
+ | `Bottom -> (* This value cannot be set in the state ; the evaluation of
+ expr was unprecise *)
+ acc
+ in
+ try
+ (* Check the size of the ival *)
+ begin match Ival.cardinal ival with
+ | None -> raise (Split_limit None)
+ | Some c as count ->
+ if Integer.(gt c (of_int monitor.split_limit)) then
+ raise (Split_limit count)
+ end;
+ (* For each integer of the ival, build a new state *)
+ try
+ let result = Ival.fold_int build ival [] in
+ let c = SplitValues.cardinal monitor.split_values in
+ if c > monitor.split_limit then
+ raise (Split_limit (Some (Integer.of_int c)));
+ result
+ with Abstract_interp.Error_Top -> (* The ival is float *)
+ raise (Split_limit None)
+ with
+ | Split_limit count ->
+ let pp_count fmt =
+ match count with
+ | None -> ()
+ | Some c -> Format.fprintf fmt " (%a)" (Integer.pretty ~hexa:false) c
+ in
+ fail ~exp "split on more than %d values%t prevented ; try to improve \
+ the analysis precision or look at the option -eva-split-limit \
+ to increase this limit."
+ monitor.split_limit pp_count
+
+
+ let eval_exp_to_int state exp =
+ let _valuation, ival = evaluate_exp_to_ival state exp in
+ try
+ Integer.to_int (Ival.project_int ival)
+ with
+ | Ival.Not_Singleton_Int ->
+ fail ~exp "this partitioning parameter must evaluate to a singleton"
+ | Failure _ ->
+ fail ~exp "this partitioning parameter is too big"
+
+ (* --- Applying partitioning actions onto flows --------------------------- *)
+
let split_state ~monitor ~(static : bool) (exp : Cil_types.exp)
(key : key) (state : state) : (key * state) list =
try
@@ -212,8 +308,8 @@ struct
in
(k,x)
in
- List.map update_key (Domain.split ~monitor state exp)
- with Domain.Operation_failed ->
+ List.map update_key (split_by_value ~monitor state exp)
+ with Operation_failed ->
[(key,state)]
let split ~monitor ~(static : bool) (p : t) (exp : Cil_types.exp) =
@@ -260,10 +356,10 @@ struct
| Enter_loop limit_kind -> fun k x ->
let limit = try match limit_kind with
- | ExpLimit exp -> Domain.eval_exp_to_int x exp
+ | ExpLimit exp -> eval_exp_to_int x exp
| IntLimit i -> i
with
- | Domain.Operation_failed -> 0
+ | Operation_failed -> 0
in
{ k with loops = (0,limit) :: k.loops }
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index 9d2c65e8a9e655fd7a56e1db7943648adfda005c..7c8ed9e5a812f5744096ed664b27a56ab2ff7c95 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -126,21 +126,9 @@ exception InvalidAction
(* Flows *)
-module type InputDomain =
+module MakeFlow (Abstract: Abstractions.Eva) :
sig
- type t
-
- exception Operation_failed
-
- val join : t -> t -> t
- val split : monitor:split_monitor ->
- t -> Cil_types.exp -> (Integer.t * t) list
- val eval_exp_to_int : t -> Cil_types.exp -> int
-end
-
-module MakeFlow (Domain : InputDomain) :
-sig
- type state = Domain.t
+ type state = Abstract.Dom.t
type t
val empty : t
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 3f03b79168e15b99e716e1d7b458d3fd0afcc24c..b22c6f12e9f4e828c71980ed072f00ee33f5af0d 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -46,21 +46,25 @@ let blocks_share_locals b1 b2 =
| _, _ -> false
module Make_Dataflow
- (Domain : Abstract_domain.External)
- (States : Powerset.S with type state = Domain.t)
- (Transfer : Transfer_stmt.S with type state = Domain.t)
- (Init: Initialization.S with type state := Domain.t)
- (Logic : Transfer_logic.S with type state = Domain.t
+ (Abstract : Abstractions.Eva)
+ (States : Powerset.S with type state = Abstract.Dom.t)
+ (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
+ (Init: Initialization.S with type state := Abstract.Dom.t)
+ (Logic : Transfer_logic.S with type state = Abstract.Dom.t
and type states = States.t)
- (Spec: sig val treat_statement_assigns: assigns -> Domain.t -> Domain.t end)
+ (Spec: sig
+ val treat_statement_assigns: assigns -> Abstract.Dom.t -> Abstract.Dom.t
+ end)
(AnalysisParam : sig
val kf: kernel_function
val call_kinstr: kinstr
- val initial_state : Domain.t
+ val initial_state : Abstract.Dom.t
end)
()
= struct
+ module Domain = Abstract.Dom
+
(* --- Analysis parameters --- *)
let kf = AnalysisParam.kf
@@ -97,7 +101,7 @@ module Make_Dataflow
(* --- Abstract values storage --- *)
- module Partition = Trace_partitioning.Make (Domain) (Transfer) (AnalysisParam)
+ module Partition = Trace_partitioning.Make (Abstract) (Transfer) (AnalysisParam)
type store = Partition.store
type flow = Partition.flow
@@ -770,20 +774,21 @@ end
module Computer
- (Domain : Abstract_domain.External)
- (States : Powerset.S with type state = Domain.t)
- (Transfer : Transfer_stmt.S with type state = Domain.t
- and type value = Domain.value)
- (Init: Initialization.S with type state := Domain.state)
- (Logic : Transfer_logic.S with type state = Domain.t
+ (Abstract : Abstractions.Eva)
+ (States : Powerset.S with type state = Abstract.Dom.t)
+ (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
+ (Init: Initialization.S with type state := Abstract.Dom.t)
+ (Logic : Transfer_logic.S with type state = Abstract.Dom.t
and type states = States.t)
- (Spec: sig val treat_statement_assigns: assigns -> Domain.t -> Domain.t end)
+ (Spec: sig
+ val treat_statement_assigns: assigns -> Abstract.Dom.t -> Abstract.Dom.t
+ end)
= struct
let compute kf call_kinstr state =
let module Dataflow =
Make_Dataflow
- (Domain) (States) (Transfer) (Init) (Logic) (Spec)
+ (Abstract) (States) (Transfer) (Init) (Logic) (Spec)
(struct
let kf = kf
let call_kinstr = call_kinstr
diff --git a/src/plugins/value/engine/partitioned_dataflow.mli b/src/plugins/value/engine/partitioned_dataflow.mli
index e65f83e2d4f777f2173a8969d034145da641fb28..d76886b509242d78e9177225f43be81872151646 100644
--- a/src/plugins/value/engine/partitioned_dataflow.mli
+++ b/src/plugins/value/engine/partitioned_dataflow.mli
@@ -27,24 +27,26 @@ open Eval
val signal_abort: unit -> unit
module Computer
- (* Abstract domain with partitioning. *)
- (Domain: Abstract_domain.External)
+ (* Abstractions with the evaluator. *)
+ (Abstract: Abstractions.Eva)
(* Set of states of abstract domain. *)
- (States : Powerset.S with type state = Domain.t)
+ (States : Powerset.S with type state = Abstract.Dom.t)
(* Transfer functions for statement on the abstract domain. *)
- (Transfer : Transfer_stmt.S with type state = Domain.t
- and type value = Domain.value)
+ (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t
+ and type value = Abstract.Val.t)
(* Initialization of local variables. *)
- (Init: Initialization.S with type state := Domain.state)
+ (Init: Initialization.S with type state := Abstract.Dom.t)
(* Transfer functions for the logic on the abstract domain. *)
- (Logic : Transfer_logic.S with type state = Domain.t
+ (Logic : Transfer_logic.S with type state = Abstract.Dom.t
and type states = States.t)
- (Spec: sig val treat_statement_assigns: assigns -> Domain.t -> Domain.t end)
+ (Spec: sig
+ val treat_statement_assigns: assigns -> Abstract.Dom.t -> Abstract.Dom.t
+ end)
: sig
val compute:
- kernel_function -> kinstr -> Domain.t ->
- Domain.t list or_bottom * Value_types.cacheable
+ kernel_function -> kinstr -> Abstract.Dom.t ->
+ Abstract.Dom.t list or_bottom * Value_types.cacheable
end
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index f143d2671be67a837951c4ddbbe4efcccb2e1b23..fdaaec4ff3138fa7dfd776b1051485c795a1581f 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -138,7 +138,7 @@ end
module type Domain = Partitioning.Domain
module type Partitioning = functor
- (Domain : Abstract_domain.External)
- (Transfer : Transfer_stmt.S with type state = Domain.t)
+ (Abstract : Abstractions.Eva)
+ (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
(Kf : Kf) ->
- Partition with type state = Domain.t
+ Partition with type state = Abstract.Dom.t
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
index 2411f49ce999889fe0f011682c2fec93835da2ea..9a86cf94ddc109b0351ef72d647744a601e07282 100644
--- a/src/plugins/value/engine/trace_partitioning.ml
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -27,8 +27,8 @@ open Partition
module Make
- (Domain : Abstract_domain.External)
- (Transfer : Transfer_stmt.S with type state = Domain.t)
+ (Abstract: Abstractions.Eva)
+ (Transfer : Transfer_stmt.S with type state = Abstract.Dom.t)
(Kf : Kf) =
struct
module Parameters = Partitioning_parameters.Make (Kf)
@@ -36,22 +36,14 @@ struct
open Kf
open Parameters
- (* Add the split function to the domain *)
- module Domain =
- struct
- exception Operation_failed = Transfer.Operation_failed
- let split = Transfer.split_by_value
- let eval_exp_to_int = Transfer.eval_exp_to_int
+ module Domain = Abstract.Dom
- include Domain
-
- let smash = function
- | [] -> []
- | v1 :: l -> [ List.fold_left join v1 l ]
- end
+ let smash_states = function
+ | [] -> []
+ | v1 :: l -> [ List.fold_left Domain.join v1 l ]
module Index = Partitioning.Make (Domain)
- module Flow = Partition.MakeFlow (Domain)
+ module Flow = Partition.MakeFlow (Abstract)
type state = Domain.t
@@ -133,7 +125,7 @@ struct
Partition.to_list s.store_partition
let smashed (s : store) : state or_bottom =
- Bottom.of_list (Domain.smash (expanded s))
+ Bottom.of_list (smash_states (expanded s))
let contents (f : flow) : state list =
Flow.to_list f.flow_states
@@ -179,11 +171,11 @@ struct
begin match return_exp with
| Some return_exp ->
let states = Transfer.split_final_states kf return_exp i states in
- List.flatten (List.map Domain.smash states)
+ List.flatten (List.map smash_states states)
| None ->
- Domain.smash states
+ smash_states states
end
- | Split_strategy.NoSplit -> Domain.smash states
+ | Split_strategy.NoSplit -> smash_states states
| Split_strategy.FullSplit -> states
(* Last case not possible : already transformed into SplitEqList *)
| Split_strategy.SplitAuto -> assert false
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 1f193393075333ca12341dac6de0e13acd4ea716..c81a78f0133f0029845b9030799c81ae1e9a700e 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -40,10 +40,6 @@ module type S = sig
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
unit or_bottom
val enter_scope: kernel_function -> varinfo list -> state -> state
- exception Operation_failed
- val split_by_value: monitor:Partition.split_monitor ->
- state -> exp -> (Integer.t * state) list
- val eval_exp_to_int: state -> exp -> int
type call_result = {
states: state list or_bottom;
cacheable: Value_types.cacheable;
@@ -875,110 +871,6 @@ module Make (Abstract: Abstractions.Eva) = struct
Domain.initialize_variable lval location ~initialized init_value state
in
List.fold_left initialize_volatile state vars
-
-
- (* ------------------------------------------------------------------------ *)
- (* Partitioning *)
- (* ------------------------------------------------------------------------ *)
-
- exception Operation_failed
-
- let fail ~exp message =
- let warn_and_raise message =
- Value_parameters.warning ~source:(fst exp.eloc) ~once:true "%s" message;
- raise Operation_failed
- in
- Pretty_utils.ksfprintf warn_and_raise message
-
- let evaluate_exp_to_ival ?valuation state exp =
- (* Evaluate the expression *)
- let valuation, value =
- match Eval.evaluate ?valuation ~reduction:false state exp with
- | `Value (valuation, value), alarms when Alarmset.is_empty alarms ->
- valuation, value
- | _ ->
- fail ~exp "this partitioning parameter cannot be evaluated safely on \
- all states"
- in
- (* Get the cvalue *)
- let cvalue = match Value.get Main_values.cvalue_key with
- | Some get_cvalue -> get_cvalue value
- | None -> fail ~exp "partitioning is disabled when the CValue domain is \
- not active"
- in
- (* Extract the ival *)
- let ival =
- try
- Cvalue.V.project_ival cvalue
- with Cvalue.V.Not_based_on_null ->
- fail ~exp "this partitioning parameter must evaluate to an integer"
- in
- valuation, ival
-
- exception Split_limit of Integer.t option
-
- let split_by_value ~monitor state exp =
- let module SplitValues = Datatype.Integer.Set in
- let valuation, ival = evaluate_exp_to_ival state exp in
- (* Build a state with the lvalue set to a singleton *)
- let build i acc =
- let value = Value.inject_int (Cil.typeOf exp) i in
- let state =
- Eval.assume ~valuation state exp value >>- fun valuation ->
- (* Check the reduction *)
- TF.update valuation state
- in
- match state with
- | `Value state ->
- let _,new_ival = evaluate_exp_to_ival state exp in
- if not (Ival.is_singleton_int new_ival) then
- fail ~exp "failing to learn perfectly from split" ;
- monitor.Partition.split_values <-
- SplitValues.add i monitor.Partition.split_values;
- (i, state) :: acc
- | `Bottom -> (* This value cannot be set in the state ; the evaluation of
- expr was unprecise *)
- acc
- in
- try
- (* Check the size of the ival *)
- begin match Ival.cardinal ival with
- | None -> raise (Split_limit None)
- | Some c as count ->
- if Integer.(gt c (of_int monitor.Partition.split_limit)) then
- raise (Split_limit count)
- end;
- (* For each integer of the ival, build a new state *)
- try
- let result = Ival.fold_int build ival [] in
- let c = SplitValues.cardinal monitor.Partition.split_values in
- if c > monitor.Partition.split_limit then
- raise (Split_limit (Some (Integer.of_int c)));
- result
- with Abstract_interp.Error_Top -> (* The ival is float *)
- raise (Split_limit None)
- with
- | Split_limit count ->
- let pp_count fmt =
- match count with
- | None -> ()
- | Some c -> Format.fprintf fmt " (%a)" (Integer.pretty ~hexa:false) c
- in
- fail ~exp "split on more than %d values%t prevented ; try to improve \
- the analysis precision or look at the option -eva-split-limit \
- to increase this limit."
- monitor.Partition.split_limit pp_count
-
-
- let eval_exp_to_int state exp =
- let _valuation, ival = evaluate_exp_to_ival state exp in
- try
- Integer.to_int (Ival.project_int ival)
- with
- | Ival.Not_Singleton_Int ->
- fail ~exp "this partitioning parameter must evaluate to a singleton"
- | Failure _ ->
- fail ~exp "this partitioning parameter is too big"
end
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index 76bb4c92be00fa8da208ef09d39701066da63cd8..a2e64699a2e1578efb3311a99281ce2f326b69a3 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -51,12 +51,6 @@ module type S = sig
val enter_scope: kernel_function -> varinfo list -> state -> state
- exception Operation_failed
-
- val split_by_value: monitor:Partition.split_monitor ->
- state -> exp -> (Integer.t * state) list
- val eval_exp_to_int: state -> exp -> int
-
type call_result = {
states: state list or_bottom;
cacheable: Value_types.cacheable;