diff --git a/Makefile b/Makefile
index 5d51fd0d81a053bf22fff6c62c7071d0c83a2a08..411ebb702e9700c539ebd8b0abf82366a00a6e93 100644
--- a/Makefile
+++ b/Makefile
@@ -877,7 +877,7 @@ PLUGIN_DISTRIB_EXTERNAL+= \
PLUGIN_CMO:= slevel/split_strategy value_parameters \
utils/value_perf utils/value_util utils/red_statuses \
utils/mark_noresults \
- utils/widen_hints_ext utils/widen utils/unroll_annots \
+ utils/widen_hints_ext utils/widen utils/partitioning_annots \
engine/split_return \
slevel/per_stmt_slevel \
utils/library_functions \
@@ -918,8 +918,8 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
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/partition engine/partitioning_parameters engine/trace_partitioning \
+ engine/partitioned_dataflow \
engine/initialization \
engine/compute_functions engine/analysis register
PLUGIN_CMI:= values/abstract_value values/abstract_location \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7a59f56fa0af6966a004d87d2a7ee43768bc23cb..e94bb4bef29fba47a4d4011839b7e546957bd5b1 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1170,24 +1170,22 @@ src/plugins/value/engine/abstractions.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/abstractions.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/analysis.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/analysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/basic_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/basic_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/compute_functions.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/compute_functions.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/evaluation.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/evaluation.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/initialization.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/initialization.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/legacy_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/legacy_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/loop_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/engine/loop_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/mem_exec.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/mem_exec.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/partitioned_dataflow.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/partitioned_dataflow.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/engine/partition.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/engine/partition.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/partitioning.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/partitioning.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/engine/partitioning_parameters.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/engine/partitioning_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/recursion.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/recursion.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/split_return.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1195,6 +1193,8 @@ src/plugins/value/engine/split_return.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/state_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/subdivided_evaluation.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/subdivided_evaluation.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/engine/trace_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/engine/trace_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_logic.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_logic.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_specification.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1239,9 +1239,9 @@ src/plugins/value/utils/red_statuses.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/red_statuses.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/library_functions.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/library_functions.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/unroll_annots.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/unroll_annots.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/mark_noresults.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/partitioning_annots.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/partitioning_annots.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/state_import.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/state_import.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/engine/basic_partitioning.ml b/src/plugins/value/engine/basic_partitioning.ml
deleted file mode 100644
index 4a790f63214cb4110f506432f5b5a23262b78576..0000000000000000000000000000000000000000
--- a/src/plugins/value/engine/basic_partitioning.ml
+++ /dev/null
@@ -1,313 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Bottom.Type
-open State_partitioning
-
-
-module Make (Domain : Domain) (Param : Param) =
-struct
- include Param
- module Partition = Partitioning.Make (Domain)
-
- type state = Domain.t
-
- (** Stores contains what have been already computed at a fixed control
- point.
- Propagation contrains what have changed since last iteration and needs
- to be propagated.
- Widening records previous states used in widening operations and keep
- tracks of the number of iterations remaining before next widening.
-
- How states are stored:
- - Eternal states are states which, once propagated, we are sure they
- will stay until the end of the analysis. This means they have not
- been widened, and thus cannot descend or disapear.
- - When states have been widened and/or joined due to the lack of
- slevel, they are put in the ultimate state.
- - Eternal states that can't be propagated due to the lack of slevel
- are doomed to wander into the limbo state. It is a join of all those
- states.
- With these rules, the ultimate state at one point is the join of the
- limbo state and the ultimate states of the predecessors.
- The field [size] store a value compatible with the legacy way of
- counting the number of eternal states in the store. *)
- type store = {
- size_limit : int;
- merge : bool;
- mutable eternal_states : Partition.t;
- mutable ultimate_state : state or_bottom;
- mutable limbo_state : state or_bottom;
- mutable size : int;
- }
-
- type propagation = {
- mutable eternal_propagation : state list;
- mutable ultimate_propagation : state or_bottom option;
- mutable widening_depth : int;
- mutable current_depth : int;
- }
-
- type shadow = {
- mutable transfered_eternals : int;
- mutable shadowed_ultimate : state or_bottom;
- }
-
- type widening = {
- stmt : stmt;
- mutable widened_state : state or_bottom;
- mutable previous_state : state or_bottom;
- mutable widening_counter : int;
- }
-
- (* Constructors *)
-
- let empty_store ~(stmt : stmt option) : store =
- let size_limit, merge = match stmt with
- | None -> max_int, false
- | Some stmt -> slevel stmt, merge stmt
- in
- {
- size_limit; merge;
- eternal_states = Partition.empty ();
- ultimate_state = `Bottom;
- limbo_state = `Bottom;
- size = 0;
- }
-
- let empty_propagation () : propagation =
- {
- eternal_propagation = [];
- ultimate_propagation = None;
- widening_depth = max_int;
- current_depth = 0;
- }
-
- let empty_shadow () : shadow =
- {
- transfered_eternals = 0;
- shadowed_ultimate = `Bottom;
- }
-
- let empty_widening ~(stmt : stmt option) : widening =
- {
- stmt = Extlib.opt_conv Cil.invalidStmt stmt;
- widened_state = `Bottom;
- previous_state = `Bottom;
- widening_counter = widening_delay;
- }
-
- let initial_propagation (states : state list) =
- let empty = empty_propagation () in
- { empty with eternal_propagation = states }
-
- (* Pretty printing *)
-
- let pretty_eternal (fmt : Format.formatter) (v : Domain.t) : unit =
- Format.fprintf fmt "eternal state %a@\n" Domain.pretty v
-
- let pretty_ultimate (fmt : Format.formatter) (v : Domain.t) : unit =
- Format.fprintf fmt "ultimate state %a@\n" Domain.pretty v
-
- let pretty_store (fmt : Format.formatter) (s : store) : unit =
- List.iter (pretty_eternal fmt) (Partition.to_list s.eternal_states);
- if not (Bottom.is_bottom s.ultimate_state) then
- pretty_ultimate fmt (Bottom.non_bottom s.ultimate_state)
-
- let pretty_propagation (fmt : Format.formatter) (p : propagation) =
- List.iter (pretty_eternal fmt) p.eternal_propagation;
- Extlib.may (Bottom.pretty pretty_ultimate fmt) p.ultimate_propagation
-
- (* Accessors *)
-
- let expanded (s : store) : state list =
- Bottom.add_to_list s.ultimate_state (Partition.to_list s.eternal_states)
-
- let smashed (s : store) : state or_bottom =
- let l = expanded s in
- Domain.join_list l
-
- let is_empty_store (s : store) : bool =
- s.size = 0 && Bottom.is_bottom s.ultimate_state
-
- let is_empty_propagation (p : propagation) : bool =
- p.eternal_propagation = [] && not (Extlib.has_some p.ultimate_propagation)
-
- let is_empty_shadow (s : shadow) : bool =
- s.transfered_eternals = 0 && Bottom.is_bottom s.shadowed_ultimate
-
- let store_size (s : store) : int =
- s.size
-
- let propagation_size (p : propagation) : int =
- List.length p.eternal_propagation +
- match p.ultimate_propagation with
- | None | Some `Bottom -> 0
- | Some (`Value _) -> 1
-
- (* Reset state (for hierchical convergence) *)
-
- let reset_store (s : store) : unit =
- s.ultimate_state <- `Bottom
-
- let reset_propagation (p : propagation) : unit =
- p.ultimate_propagation <- None;
- p.widening_depth <- max_int
-
- let reset_shadow (s : shadow) : unit =
- s.shadowed_ultimate <- `Bottom
-
- let reset_widening (w : widening) : unit =
- w.widened_state <- `Bottom;
- w.previous_state <- `Bottom;
- w.widening_counter <- widening_delay
-
- let reset_widening_counter (w : widening) : unit =
- w.widening_counter <- max w.widening_counter (widening_period - 1)
-
- (* Operators *)
-
- let clear_propagation (p : propagation) : unit =
- p.eternal_propagation <- [];
- p.ultimate_propagation <- None;
- p.widening_depth <- max_int;
- p.current_depth <- 0
-
- let transfer (f : state list -> state list) (p : propagation) : unit =
- let transfer_ultimate state' =
- state' >>- fun x -> Domain.join_list (f [x])
- in
- if p.eternal_propagation <> [] then
- p.eternal_propagation <- f p.eternal_propagation;
- p.ultimate_propagation <-
- Extlib.opt_map transfer_ultimate p.ultimate_propagation
-
- let merge ~(into : propagation) (source : propagation) : unit =
- if Extlib.has_some source.ultimate_propagation then
- into.ultimate_propagation <- source.ultimate_propagation;
- into.eternal_propagation <-
- source.eternal_propagation @ into.eternal_propagation;
- into.widening_depth <- source.widening_depth;
- into.current_depth <- source.current_depth
-
- let join (sources : (propagation*shadow) list) (dest : store): propagation =
- let ultimates_changed = ref false in
- (* Update source shadow with source propagation *)
- let update (eternals,ultimates) (p,s) =
- begin match p.ultimate_propagation with
- | None -> ()
- | Some state' ->
- if not (Bottom.equal Domain.equal state' s.shadowed_ultimate) then
- ultimates_changed := true;
- s.shadowed_ultimate <- state'
- end;
- s.transfered_eternals <- s.transfered_eternals +
- List.length p.eternal_propagation;
- p.eternal_propagation @ eternals,
- Bottom.add_to_list s.shadowed_ultimate ultimates
- in
- let eternals, ultimates = List.fold_left update ([],[]) sources in
- (* Create a new propagation *)
- let p = empty_propagation () in
- let current_depth acc (p,_s) = max p.current_depth acc
- and widening_depth acc (p,_s) = min p.widening_depth acc in
- p.current_depth <- List.fold_left current_depth 0 sources;
- p.widening_depth <- List.fold_left widening_depth max_int sources;
- (* Add all eternal states *)
- dest.size <- dest.size + List.length eternals;
- let states = Partition.merge_set_return_new eternals dest.eternal_states in
- (* Merge / Merge after loop : join eternal states being propagated *)
- let states =
- if dest.merge
- then Bottom.to_list (Domain.join_list states)
- else states
- in
- (* Do we have too many eternal states ? *)
- if dest.size > dest.size_limit then
- begin
- (* Send excess states into limbo *)
- dest.limbo_state <- Domain.join_list ~into:dest.limbo_state states;
- ultimates_changed := true
- end else
- p.eternal_propagation <- states;
- (* Join ultimate states *)
- if !ultimates_changed then
- begin
- let inputs = Bottom.add_to_list dest.limbo_state ultimates in
- let state' = Domain.join_list inputs in
- if not (Bottom.equal Domain.equal state' dest.ultimate_state) then
- p.ultimate_propagation <- Some state';
- dest.ultimate_state <- state'
- end;
- p
-
- let widen (_s : store) (w : widening) (p : propagation) : bool =
- let ultimate_stable =
- match p.ultimate_propagation with
- | None -> true
- | Some current_state ->
- let previous_state = w.previous_state in
- w.previous_state <- current_state;
- w.widening_counter <- w.widening_counter - 1;
- match previous_state, current_state with
- | _, `Bottom -> true
- | `Bottom, `Value _ -> false
- | `Value prev, `Value curr ->
- if Domain.is_included curr prev then
- true
- else if w.widening_counter >= 0 then
- false
- else begin
- Value_parameters.feedback ~level:1 ~once:true ~current:true
- ~dkey:Value_parameters.dkey_widening
- "applying a widening at this point";
- let prev = match w.widened_state with
- | `Value v -> Domain.join prev v
- | `Bottom -> prev
- in
- let next = Domain.widen kf w.stmt prev (Domain.join prev curr) in
- p.ultimate_propagation <- Some (`Value next);
- p.widening_depth <- min p.widening_depth p.current_depth;
- w.previous_state <- `Value next;
- w.widened_state <- `Value next;
- w.widening_counter <- widening_period - 1;
- false
- end
- in
- ultimate_stable && p.eternal_propagation = []
-
- let enter_loop (p : propagation) (_ : loop) =
- p.current_depth <- p.current_depth + 1
-
- let leave_loop (p : propagation) (_ : loop) =
- p.current_depth <- p.current_depth - 1;
- match p.ultimate_propagation with
- (* We leave the loop where the ultimate have been widened.
- It becomes eternal again. *)
- | Some state' when p.current_depth < p.widening_depth ->
- p.ultimate_propagation <- None;
- p.eternal_propagation <- Bottom.add_to_list state' p.eternal_propagation
- | _ -> ()
-
- let next_loop_iteration (_p : propagation) (_ : loop) = ()
-end
diff --git a/src/plugins/value/engine/legacy_partitioning.ml b/src/plugins/value/engine/legacy_partitioning.ml
deleted file mode 100644
index bb2b4660552bdd4cb95ac52621f595d414375e5b..0000000000000000000000000000000000000000
--- a/src/plugins/value/engine/legacy_partitioning.ml
+++ /dev/null
@@ -1,217 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-
-open Cil_types
-open Bottom.Type
-open State_partitioning
-
-module Make (Domain : Domain) (Param : Param) =
-struct
- include Param
- module Partition = Partitioning.Make (Domain)
-
- type state = Domain.t
-
- type store = {
- size_limit : int;
- merge : bool;
- mutable eternal_states : Partition.t;
- mutable ultimate_state : state or_bottom;
- mutable size : int;
- }
-
- type propagation = {
- mutable states : state list;
- }
-
- type shadow = {
- mutable transfered_states : int;
- }
-
- type widening = {
- stmt : stmt;
- mutable widened_state : state or_bottom;
- mutable previous_state : state or_bottom;
- mutable widening_counter : int;
- }
-
- (* Constructors *)
-
- let empty_store ~(stmt : stmt option) : store =
- let size_limit, merge = match stmt with
- | None -> max_int, false
- | Some stmt -> slevel stmt, merge stmt
- in
- {
- size_limit; merge;
- eternal_states = Partition.empty ();
- ultimate_state = `Bottom;
- size = 0;
- }
-
- let empty_propagation () : propagation =
- { states = [] }
-
- let empty_shadow () : shadow =
- { transfered_states = 0 }
-
- let empty_widening ~(stmt : stmt option) : widening =
- {
- stmt = Extlib.opt_conv Cil.invalidStmt stmt;
- widened_state = `Bottom;
- previous_state = `Bottom;
- widening_counter = widening_delay;
- }
-
- let initial_propagation (states : state list) : propagation =
- { states }
-
- (* Pretty printing *)
-
- let pretty_eternal (fmt : Format.formatter) (v : Domain.t) : unit =
- Format.fprintf fmt "eternal state %a@\n" Domain.pretty v
-
- let pretty_ultimate (fmt : Format.formatter) (v : Domain.t) : unit =
- Format.fprintf fmt "ultimate state %a@\n" Domain.pretty v
-
- let pretty_store (fmt : Format.formatter) (s : store) : unit =
- List.iter (pretty_eternal fmt) (Partition.to_list s.eternal_states);
- if not (Bottom.is_bottom s.ultimate_state) then
- pretty_ultimate fmt (Bottom.non_bottom s.ultimate_state)
-
- let pretty_propagation (fmt : Format.formatter) (p : propagation) =
- List.iter (pretty_eternal fmt) p.states
-
- (* Accessors *)
-
- let expanded (s : store) : state list =
- Bottom.add_to_list s.ultimate_state (Partition.to_list s.eternal_states)
-
- let smashed (s : store) : state or_bottom =
- let l = expanded s in
- Domain.join_list l
-
- let is_empty_store (s : store) : bool =
- s.size = 0 && Bottom.is_bottom s.ultimate_state
-
- let is_empty_propagation (p : propagation) : bool =
- p.states = []
-
- let is_empty_shadow (s : shadow) : bool =
- s.transfered_states = 0
-
- let store_size (s : store) : int =
- s.size
-
- let propagation_size (p : propagation) : int =
- List.length p.states
-
- (* Reset state (for hierchical convergence) *)
-
- let reset_store (s : store) : unit =
- s.ultimate_state <- `Bottom
-
- let reset_propagation (p : propagation) : unit =
- p.states <- []
-
- let reset_shadow (_s : shadow) : unit = ()
-
- let reset_widening (w : widening) : unit =
- w.widened_state <- `Bottom;
- w.previous_state <- `Bottom;
- w.widening_counter <- widening_delay
-
- let reset_widening_counter w =
- w.widening_counter <- max w.widening_counter (widening_period - 1)
-
- (* Operators *)
-
- let clear_propagation (p : propagation) : unit =
- p.states <- []
-
- let transfer (f : state list -> state list) (p : propagation) : unit =
- if p.states <> [] then
- p.states <- f p.states
-
- let merge ~(into : propagation) (source : propagation) : unit =
- into.states <- source.states @ into.states
-
- let join (sources : (propagation*shadow) list) (dest : store) : propagation =
- (* Update source stores with source propagation *)
- let update acc (p,s) =
- let size = List.length p.states in
- s.transfered_states <- s.transfered_states + size;
- dest.size <- dest.size + size;
- Partition.merge_set_return_new p.states dest.eternal_states @ acc
- in
- let new_states = List.fold_left update [] sources in
- (* Create a new propagation *)
- let p = { states = new_states } in
- (* Merge / Merge after loop : join eternal states being propagated *)
- if dest.merge then
- p.states <- Bottom.to_list (Domain.join_list p.states);
- (* Do we have too many eternal states ? *)
- if dest.size > dest.size_limit then
- begin
- let state' = Domain.join_list ~into:dest.ultimate_state p.states in
- if Bottom.is_included Domain.is_included state' dest.ultimate_state then
- p.states <- []
- else begin
- dest.ultimate_state <- state';
- p.states <- Bottom.to_list state'
- end
- end;
- p
-
- let widen (s : store) (w : widening) (p : propagation) : bool =
- let current_state = s.ultimate_state
- and previous_state = w.previous_state in
- if not (Bottom.is_bottom current_state) then begin
- w.previous_state <- current_state;
- w.widening_counter <- w.widening_counter - 1;
- match previous_state, current_state with
- | _, `Bottom | `Bottom, _ -> ()
- | `Value prev, `Value curr ->
- if Domain.is_included curr prev then
- p.states <- []
- else if w.widening_counter < 0 then begin
- Value_parameters.feedback ~level:1 ~once:true ~current:true
- ~dkey:Value_parameters.dkey_widening
- "applying a widening at this point";
- let prev = match w.widened_state with
- | `Value v -> Domain.join prev v
- | `Bottom -> prev
- in
- let next = Domain.widen kf w.stmt prev (Domain.join prev curr) in
- p.states <- [next];
- w.previous_state <- `Value next;
- w.widened_state <- `Value next;
- w.widening_counter <- widening_period - 1
- end
- end;
- p.states = []
-
- let enter_loop (_p : propagation) (_ : loop) = ()
- let leave_loop (_p : propagation) (_ : loop) = ()
- let next_loop_iteration (_p : propagation) (_ : loop) = ()
-end
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
new file mode 100644
index 0000000000000000000000000000000000000000..44642d2a166d24d00e1823f992ae18f9ce5aa221
--- /dev/null
+++ b/src/plugins/value/engine/partition.ml
@@ -0,0 +1,325 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Utility function on options *)
+let opt_flatten (type a) (o : a option option) : a option =
+ Extlib.opt_conv None o
+
+module LvalMap = Cil_datatype.LvalStructEq.Map
+module IList = Datatype.List (Datatype.Int)
+
+type branch = int
+
+type key = {
+ ration_stamp : int option;
+ transfer_stamp : int option;
+ branches : branch list;
+ loops : int list;
+ static_split : Integer.t LvalMap.t;
+ dynamic_split : Integer.t LvalMap.t;
+}
+
+module Key =
+struct
+ type t = key
+
+ let compare k1 k2 =
+ let (<?>) c (cmp,x,y) =
+ if c = 0 then cmp x y else c
+ in
+ Extlib.opt_compare (-) k1.ration_stamp k2.ration_stamp
+ <?> (Extlib.opt_compare (-), k1.transfer_stamp, k2.transfer_stamp)
+ <?> (IList.compare, k1.loops, k2.loops)
+ <?> (LvalMap.compare Integer.compare, k1.static_split, k2.static_split)
+ <?> (LvalMap.compare Integer.compare, k1.dynamic_split, k2.dynamic_split)
+ <?> (IList.compare, k1.branches, k2.branches)
+end
+
+module KMap = Map.Make (Key)
+
+
+type 'a partition = 'a KMap.t
+
+type action =
+ | Enter_loop
+ | Leave_loop
+ | Incr_loop of int
+ | Branch of branch * int
+ | Ration of int
+ | Ration_merge of int option
+ | Transfer_merge
+ | Static_split of Cil_types.lval
+ | Dynamic_split of Cil_types.lval
+ | Static_merge of Cil_types.lval
+ | Dynamic_merge of Cil_types.lval
+ | Update_dynamic_splits
+
+exception InvalidAction
+
+
+module type InputDomain =
+sig
+ type t
+
+ exception Cant_split
+
+ val join : t -> t -> t
+ val split : t -> Cil_types.lval -> (Integer.t * t) list
+end
+
+
+module Make (Domain : InputDomain) =
+struct
+ type t = Domain.t partition
+ type state = Domain.t
+
+ let empty : 'a partition =
+ KMap.empty
+
+ let empty_key : key = {
+ ration_stamp = None;
+ transfer_stamp = None;
+ branches = [];
+ loops = [];
+ static_split = LvalMap.empty;
+ dynamic_split = LvalMap.empty;
+ }
+
+ let is_empty (p : 'a partition) : bool =
+ KMap.is_empty p
+
+ let initial (l : 'a list) : 'a partition =
+ let stamp = ref 0 in
+ let add p state =
+ let k = { empty_key with ration_stamp = Some !stamp } in
+ incr stamp;
+ KMap.add k state p
+ in
+ List.fold_left add KMap.empty l
+
+ let add (p : t) (k : key) (x : state) : t =
+ (* Join states with the same key *)
+ let x =
+ try
+ Domain.join (KMap.find k p) x
+ with Not_found -> x
+ in
+ KMap.add k x p
+
+ let add_list (p : t) (l : (key * state) list) : t =
+ List.fold_left (fun p (k,x) -> add p k x) p l
+
+ let split_state ~(static : bool) (lval : Cil_types.lval)
+ (key : key) (state : state) : (key * state) list =
+ try
+ let update_key (v,x) =
+ let k =
+ if static then
+ { key with static_split = LvalMap.add lval v key.static_split }
+ else
+ { key with dynamic_split = LvalMap.add lval v key.dynamic_split }
+ in
+ (k,x)
+ in
+ List.map update_key (Domain.split state lval)
+ with Domain.Cant_split ->
+ [(key,state)]
+
+ let split ~(static : bool) (p : t) (lval : Cil_types.lval) =
+ let add_split key state p =
+ add_list p (split_state ~static lval key state)
+ in
+ KMap.fold add_split p KMap.empty
+
+ let update_dynamic_splits p =
+ (* Update one state *)
+ let update_state key state p =
+ (* Split the states in the list l for the given lval *)
+ let update_lval lval _ l =
+ let static = false in
+ List.fold_left (fun l (k,s) -> split_state ~static lval k s @ l) [] l
+ in
+ (* Foreach lval in original state: split *)
+ let l = LvalMap.fold update_lval key.dynamic_split [(key,state)] in
+ add_list p l
+ in
+ KMap.fold update_state p KMap.empty
+
+ let map_keys (f : key -> key) (p : t) =
+ KMap.fold (fun k x acc -> add acc (f k) x) p empty
+
+ let transfer_keys p = function
+ | Static_split lval ->
+ split ~static:true p lval
+
+ | Dynamic_split lval ->
+ split ~static:false p lval
+
+ | Update_dynamic_splits ->
+ update_dynamic_splits p
+
+ | action -> (* Simple map transfer functions *)
+ let transfer = match action with
+ | Static_split _ | Dynamic_split _ | Update_dynamic_splits ->
+ assert false (* Handled above *)
+
+ | Enter_loop -> fun k ->
+ { k with loops = 0 :: k.loops }
+
+ | Leave_loop -> fun k ->
+ begin match k.loops with
+ | [] -> raise InvalidAction
+ | _ :: tl -> { k with loops = tl }
+ end
+
+ | Incr_loop limit -> fun k ->
+ begin match k.loops with
+ | [] -> raise InvalidAction
+ | h :: tl ->
+ if h >= limit then
+ k
+ else
+ { k with loops = h + 1 :: tl }
+ end
+
+ | Branch (b,max) -> fun k ->
+ let list_start l i =
+ let rec aux acc i = function
+ | [] -> acc
+ | _ when i <= 0 -> List.rev acc
+ | x :: l -> aux (x :: acc) (i - 1) l
+ in
+ aux [] i l
+ in
+ if max > 0 then
+ { k with branches = b :: list_start k.branches (max - 1) }
+ else if k.branches <> [] then
+ { k with branches = [] }
+ else
+ k
+
+ | Ration (min) ->
+ let r = ref min in
+ fun k ->
+ let ration_stamp = Some !r in
+ incr r;
+ { k with ration_stamp }
+
+ | Ration_merge ration_stamp -> fun k ->
+ { k with ration_stamp }
+
+ | Transfer_merge -> fun k ->
+ { k with transfer_stamp = None }
+
+ | Static_merge lval -> fun k ->
+ { k with static_split = LvalMap.remove lval k.static_split }
+
+ | Dynamic_merge lval -> fun k ->
+ { k with dynamic_split = LvalMap.remove lval k.dynamic_split }
+ in
+ map_keys transfer p
+
+ let map_states (f : 'a -> 'a) (p : 'a partition) : 'a partition =
+ KMap.map f p
+
+ let transfer_states (f : 'a -> 'a list) (p : 'a partition) : 'a partition =
+ let transfer_one k x p =
+ let t = ref 0 in
+ let add p y =
+ let k' = { k with transfer_stamp = Some !t } in
+ incr t;
+ KMap.add k' y p
+ in
+ match f x with
+ | [y] -> KMap.add k y p
+ | l -> List.fold_left add p l
+ in
+ KMap.fold transfer_one p KMap.empty
+
+ (*
+ let legacy_transfer_states (f : 'a list -> 'a list) (p : 'a partition)
+ : 'a partition =
+ (* Group the states in buckets, where each bucket is a list of states
+ with the same key except for the ration stamp *)
+ let fill_buckets k x buckets =
+ (* Ignore the ration stamp *)
+ let k = { k with ration_stamp = None } in
+ (* Find the bucket *)
+ let contents =
+ try KMap.find k buckets
+ with Not_found -> []
+ in
+ (* Add the state to the bucket *)
+ KMap.add k (x :: contents) buckets
+ in
+ let buckets = KMap.fold fill_buckets p KMap.empty in
+ (* Apply the transfer function to each bucket *)
+ let result = KMap.map f buckets in
+ (* Rebuild a partition by rationing out all the states *)
+ let r = ref 0 in
+ let ration_bucket k bucket acc =
+ let ration_one acc x =
+ let k' = { k with ration_stamp = Some !r } in
+ incr r;
+ KMap.add k' x acc
+ in
+ List.fold_left ration_one acc bucket
+ in
+ KMap.fold ration_bucket result KMap.empty *)
+
+ let find = KMap.find
+ let replace = KMap.add
+
+ let to_list (p : 'a partition) : 'a list =
+ KMap.fold (fun _k x l -> x :: l) p []
+
+ let size (p : 'a partition) : int =
+ KMap.fold (fun _k _x n -> n + 1) p 0
+
+
+ let merge (f : 'a option -> 'b option -> 'c option) (p1 : 'a partition)
+ (p2 : 'b partition) : 'c partition =
+ KMap.merge (fun _k o1 o2 -> f o1 o2) p1 p2
+
+ (* Almost like Map.union of Ocaml 4.03.0 *)
+ let union (f : 'a -> 'a -> 'a) (p1 : 'a partition)
+ (p2 : 'a partition) : 'a partition =
+ let g _k o1 o2 =
+ match o1 with
+ | None -> o2
+ | Some x1 ->
+ match o2 with
+ | None -> o1
+ | Some x2 -> Some (f x1 x2)
+ in
+ KMap.merge g p1 p2
+
+ let iter (f : 'a -> unit) (p : 'a partition) : unit =
+ KMap.iter (fun _k x -> f x) p
+
+ let filter_keys (f : key -> bool) (p : 'a partition) : 'a partition =
+ KMap.filter (fun k _x -> f k) p
+
+ let map_filter (f : key -> 'a -> 'b option) (p : 'a partition)
+ : 'b partition =
+ KMap.merge (fun k o _ -> opt_flatten (Extlib.opt_map (f k) o)) p KMap.empty
+end
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
new file mode 100644
index 0000000000000000000000000000000000000000..161b95ca6ba604b2f9ce9d1ef315a319bb2f6eea
--- /dev/null
+++ b/src/plugins/value/engine/partition.mli
@@ -0,0 +1,119 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* A state partition is a collection of states, each of which is identified
+ by a unique key. The key identifies the reason for which we want to keep
+ the state separate from the others. The partitioning method will involve
+ updating the key. If at some point two states share the same key, it means
+ that the partitioning method decided to not consider those states separately
+ anymore and that they should be joined together.
+
+ The key have several fields, one for each kind of partitioning.
+
+ - Ration stamps: These modelize the legacy slevel. Each state is given
+ a ration stamp (represented by an integer) until there is no slevel left.
+ It is an option type, when there is no more ration stamp, this field is
+ set to None; each new state will not be distinguished by this field.
+ - Branches: This field enumerate the last branches taken to reach this
+ state. The partitioning may chose how the branches are identified, but it
+ is a First-In-First-Out set.
+ - Loops: This field stores the loop iterations needed to reach this state
+ for each loop we are currently in. It is stored in reverse order
+ (innermost loop first)
+ - Static/Dynamic splits:
+
+ Note on implementation. These partitions are implemented as map from keys
+ to states. We chose to have the same partition for stores, propagation and
+ widenings so the combination of propagation + store or propagation +
+ widening can be done as a map2 operation. However, this involve some tricks
+ to make keys be always distinguished in propagation, like giving them new
+ ration stamps. It may have been more natural to consider that propagations
+ are lists, allowing states to have the same key.
+*)
+
+type branch = int
+
+module LvalMap = Cil_datatype.LvalStructEq.Map
+
+type key = private {
+ ration_stamp : int option;
+ transfer_stamp : int option;
+ branches : branch list;
+ loops : int list;
+ static_split : Integer.t LvalMap.t;
+ dynamic_split : Integer.t LvalMap.t;
+}
+
+type 'a partition
+
+type action =
+ | Enter_loop
+ | Leave_loop
+ | Incr_loop of int (* the parameter is the unroll limit *)
+ | Branch of branch * int (* branch taken, max branches in history *)
+ | Ration of int (* starting ration stamp *)
+ | Ration_merge of int option (* new ration stamp for the merge state *)
+ | Transfer_merge
+ | Static_split of Cil_types.lval
+ | Dynamic_split of Cil_types.lval
+ | Static_merge of Cil_types.lval
+ | Dynamic_merge of Cil_types.lval
+ | Update_dynamic_splits
+
+exception InvalidAction
+
+
+module type InputDomain =
+sig
+ type t
+
+ exception Cant_split
+
+ val join : t -> t -> t
+ val split : t -> Cil_types.lval -> (Integer.t * t) list
+end
+
+
+module Make (Domain : InputDomain) :
+sig
+ type t = Domain.t partition
+ type state = Domain.t
+
+ val empty : 'a partition
+ val is_empty : 'a partition -> bool
+ val initial : 'a list -> 'a partition
+ val size : 'a partition -> int
+ val to_list : 'a partition -> 'a list
+
+ val find : key -> 'a partition -> 'a
+ val replace : key -> 'a -> 'a partition -> 'a partition
+ val merge : ('a option -> 'b option -> 'c option) -> 'a partition
+ -> 'b partition -> 'c partition
+ val union : ('a -> 'a -> 'a) -> 'a partition -> 'a partition -> 'a partition
+
+ val iter : ('a -> unit) -> 'a partition -> unit
+ val transfer_keys : t -> action -> t
+ val filter_keys : (key -> bool) -> 'a partition -> 'a partition
+ val map_states : ('a -> 'a) -> 'a partition -> 'a partition
+ val transfer_states : ('a -> 'a list) -> 'a partition -> 'a partition
+ val map_filter : (key -> 'a -> 'b option) -> 'a partition -> 'b partition
+end
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 8621a85292a90e77ee6d6e6620d39659ec65aca6..e3d842a247fe0282e8e30d59a7a9b84d902d3133 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -39,9 +39,6 @@ let check_signals, signal_abort =
let dkey = Value_parameters.dkey_iterator
let dkey_callbacks = Value_parameters.dkey_callbacks
-let is_return s = match s.skind with Return _ -> true | _ -> false
-let is_loop s = match s.skind with Loop _ -> true | _ -> false
-
let blocks_share_locals b1 b2 =
match b1.blocals, b2.blocals with
| [], [] -> true
@@ -88,108 +85,27 @@ module Make_Dataflow
let interpreter_mode =
Value_parameters.InterpreterMode.get ()
- let slevel (stmt : stmt) : int =
- if is_return stmt || interpreter_mode then
- max_int
- else match Per_stmt_slevel.local kf with
- | Per_stmt_slevel.Global i -> i
- | Per_stmt_slevel.PerStmt f -> f stmt
-
- let merge_after_loop : bool =
- Kernel_function.Set.mem kf
- (Value_parameters.SlevelMergeAfterLoop.get ())
-
- let merge (stmt : stmt) : bool =
- is_loop stmt && merge_after_loop
- ||
- match Per_stmt_slevel.merge kf with
- | Per_stmt_slevel.NoMerge -> false
- | Per_stmt_slevel.Merge f -> f stmt
-
- let default_loop_unroll : int = Value_parameters.MinLoopUnroll.get ()
-
- let unroll (stmt : stmt) : int =
- let local_unroll = match Unroll_annots.get_unroll_terms stmt with
- | [] ->
- let is_attribute a = Cil.hasAttribute a stmt.sattr in
- begin
- match List.filter is_attribute ["for" ; "while" ; "dowhile"] with
- | [] -> ()
- | loop_kind :: _ ->
- let wkey =
- if loop_kind = "for"
- then Value_parameters.wkey_missing_loop_unroll_for
- else Value_parameters.wkey_missing_loop_unroll
- in
- Value_parameters.warning
- ~wkey ~source:(fst (Cil_datatype.Stmt.loc stmt)) ~once:true
- "%s loop without unroll annotation" loop_kind
- end;
- None
- | [t] ->
- (* Inlines the value of const variables in [t]. *)
- let global_init vi =
- try (Globals.Vars.find vi).init with Not_found -> None
- in
- let t =
- Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
- in
- begin match Logic_utils.constFoldTermToInt t with
- | Some n -> Some (Integer.to_int n)
- | None ->
- Kernel.warning ~once:true ~current:true
- "invalid term, not integer: %a"
- Printer.pp_term t;
- None
- end
- | _ ->
- Kernel.warning ~once:true ~current:true
- "ignoring invalid unroll annotation";
- None
- in match local_unroll with
- | Some n -> n
- | None -> default_loop_unroll
-
let slevel_display_step : int =
Value_parameters.ShowSlevel.get ()
+ (* Ideally, the slevel parameter should not be used anymore in this file
+ but it is still required for logic interpretation *)
+ let slevel =
+ let module P = Partitioning_parameters.Make (AnalysisParam) in
+ P.slevel
- (* --- Abstract values storage --- *)
-
- module Domain = struct
- include Domain
- let join_list ?(into : t or_bottom = `Bottom) (l : t list) : t or_bottom =
- List.fold_left
- (fun acc v -> Bottom.join join acc (`Value v))
- into l
- end
-
- module PartitioningParam = struct
- type loop = stmt
- let kf = kf
- let widening_delay = Value_parameters.WideningDelay.get ()
- let widening_period = Value_parameters.WideningPeriod.get ()
- let slevel = slevel
- let merge = merge
- let unroll = unroll
- end
-
- module type P =
- State_partitioning.Partition with type state = Domain.t
- and type loop = PartitioningParam.loop
-
- let partition_module =
- if descending_iteration = NoIteration
- then (module Loop_partitioning.Make (Domain) (PartitioningParam) : P)
- else (module Basic_partitioning.Make (Domain) (PartitioningParam) : P)
+ (* --- Abstract values storage --- *)
- module Partition = (val partition_module: P)
+ module Partition = Trace_partitioning.Make (Domain) (AnalysisParam)
type store = Partition.store
type widening = Partition.widening
type propagation = Partition.propagation
- type shadow = Partition.shadow
+
+ type edge_info = {
+ mutable fireable : bool (* Does any states survive the transition ? *)
+ }
(* --- Interpreted automata --- *)
@@ -226,8 +142,8 @@ module Make_Dataflow
| `Value state -> state
let initial_propagation =
- Partition.initial_propagation (States.to_list initial_states),
- Partition.empty_shadow ()
+ -1, (* dummy edge identifier *)
+ Partition.initial_propagation (States.to_list initial_states)
let post_conditions = ref false
@@ -259,7 +175,7 @@ module Make_Dataflow
VertexTable.create control_point_count
let w_table : widening VertexTable.t =
VertexTable.create 7
- let e_table : (propagation * shadow) EdgeTable.t =
+ let e_table : (propagation * edge_info) EdgeTable.t =
EdgeTable.create transition_count
(* Default (Initial) stores on vertex and edges *)
@@ -267,18 +183,21 @@ module Make_Dataflow
Partition.empty_store ~stmt:v.vertex_start_of
let default_vertex_widening (v : vertex) () : widening =
Partition.empty_widening ~stmt:v.vertex_start_of
- let default_edge_store () : propagation * shadow =
- Partition.empty_propagation (), Partition.empty_shadow ()
+ let default_edge_propagation () : propagation * edge_info =
+ Partition.empty_propagation (), { fireable = false }
(* Get the stores associated to a control point or edge *)
let get_vertex_store (v : vertex) : store =
VertexTable.find_or_add v_table v ~default:(default_vertex_store v)
let get_vertex_widening (v : vertex) : widening =
VertexTable.find_or_add w_table v ~default:(default_vertex_widening v)
- let get_edge_propagation (e : vertex edge) : propagation * shadow =
- EdgeTable.find_or_add e_table e ~default:default_edge_store
- let get_pred_propagations (v : vertex) : (propagation * shadow) list =
- List.map (fun (_,e,_) -> get_edge_propagation e) (G.pred_e graph v)
+ let get_edge_propagation (e : vertex edge) : propagation * edge_info =
+ EdgeTable.find_or_add e_table e ~default:default_edge_propagation
+ let get_pred_propagations (v : vertex) : ('branch * propagation) list =
+ let get (_,e,_) =
+ e.edge_key, fst (get_edge_propagation e)
+ in
+ List.map get (G.pred_e graph v)
let get_succ_propagations (v : vertex) : propagation list =
List.map (fun (_,e,_) -> fst (get_edge_propagation e)) (G.succ_e graph v)
@@ -305,6 +224,12 @@ module Make_Dataflow
type state = Domain.t
+ (** Join every state in the list *)
+ let smash (l : state list) : state or_bottom =
+ match l with
+ | [] -> `Bottom
+ | v1 :: l -> `Value (List.fold_left Domain.join v1 l)
+
(* Thse lifting function helps to uniformize the transfer functions to a
common signature *)
@@ -382,10 +307,6 @@ module Make_Dataflow
let transfer_return (stmt : stmt) (return_exp : exp option)
(states : state list) : state list =
- (** Join every state in the list and put the result in a singleton. *)
- let smash (l : state list) : state list =
- Bottom.to_list (Domain.join_list l)
- in
(* Deconstruct return statement *)
let return_var = match return_exp with
| Some {enode = Lval (Var v, NoOffset)} -> Some v
@@ -411,12 +332,12 @@ module Make_Dataflow
begin match return_exp with
| Some return_exp ->
let split_states = Transfer.split_final_states kf return_exp i states in
- let states' = List.map Domain.join_list split_states in
+ let states' = List.map smash split_states in
Bottom.all states'
| None ->
- smash states
+ Bottom.to_list (smash states)
end
- | Split_strategy.NoSplit -> smash states
+ | Split_strategy.NoSplit -> Bottom.to_list (smash states)
| Split_strategy.FullSplit -> states
(* Last case not possible : already transformed into SplitEqList *)
| Split_strategy.SplitAuto -> assert false
@@ -529,13 +450,15 @@ module Make_Dataflow
let process_edge (v1,e,v2 : G.edge) : unit =
let {edge_transition=transition; edge_kinstr=kinstr} = e in
- let propagation,_shadow = get_edge_propagation e in
+ let propagation,edge_info = get_edge_propagation e in
!Db.progress ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
Partition.transfer (transfer_transition transition) propagation;
- process_loop_transitions v1 v2 propagation
+ process_loop_transitions v1 v2 propagation;
+ if not (Partition.is_empty_propagation propagation) then
+ edge_info.fireable <- true
let update_vertex ?(widening : bool = false) (v : vertex) : bool =
(* Set location if possible *)
@@ -586,7 +509,7 @@ module Make_Dataflow
false
in
(* Reset sources *)
- List.iter (fun (p,_) -> Partition.clear_propagation p) sources;
+ List.iter (fun (_,p) -> Partition.clear_propagation p) sources;
(* Dispatch to successors *)
List.iter (fun p2 -> Partition.merge p ~into:p2) (get_succ_propagations v);
(* Return wether the iterator should stop or not *)
@@ -619,21 +542,6 @@ module Make_Dataflow
| _ -> (* Several successors - failure *)
Value_parameters.abort "Do not know which branch to take. Stopping."
- let reset_component (vertex_list : vertex list) : unit =
- let reset_edge (_,e,_) =
- let p,s = get_edge_propagation e in
- Partition.reset_propagation p;
- Partition.reset_shadow s;
- in
- let reset_vertex v =
- let s = get_vertex_store v
- and w = get_vertex_widening v in
- Partition.reset_store s;
- Partition.reset_widening w;
- List.iter reset_edge (G.succ_e graph v)
- in
- List.iter reset_vertex vertex_list
-
let rec iterate_list (l : wto) =
List.iter iterate_element l
and iterate_element = function
@@ -644,7 +552,7 @@ module Make_Dataflow
Otherwise, only resets the widening counter for this component. This
is especially useful for nested loops. *)
if hierachical_convergence
- then reset_component (v :: Wto.flatten w)
+ then () (* reset_component (v :: Wto.flatten w) *)
else Partition.reset_widening_counter (get_vertex_widening v);
(* Iterate until convergence *)
let iteration_count = ref 0 in
@@ -715,12 +623,12 @@ module Make_Dataflow
| Then -> Db.Value.mask_then
| Else -> Db.Value.mask_else
in
- let shadow = snd (get_edge_propagation e) in
+ let edge_info = snd (get_edge_propagation e) in
let old_status =
try StmtTable.find table stmt
with Not_found -> 0
and status =
- if Partition.is_empty_shadow shadow then 0 else mask
+ if edge_info.fireable then mask else 0
in
let new_status = old_status lor status in
StmtTable.replace table stmt new_status;
diff --git a/src/plugins/value/engine/partitioning.ml b/src/plugins/value/engine/partitioning.ml
index 3b6f292b4f6f572cb609f4d6054c7c9b8dd33c84..c40be57a5bc0189d25c7352849313ecfa5ec33ee 100644
--- a/src/plugins/value/engine/partitioning.ml
+++ b/src/plugins/value/engine/partitioning.ml
@@ -33,6 +33,7 @@ module type S = sig
type t
val empty: unit -> t
+ val add : state -> t -> bool
val merge_set_return_new: state list -> t -> state list
val join: t -> state or_bottom
val to_list: t -> state list
diff --git a/src/plugins/value/engine/partitioning.mli b/src/plugins/value/engine/partitioning.mli
index 40bb50a1f25a6f772a4f8980cec36c87c0f883a3..4ecc2ee21ff9444a5913bbe3277499e428ca95c0 100644
--- a/src/plugins/value/engine/partitioning.mli
+++ b/src/plugins/value/engine/partitioning.mli
@@ -34,6 +34,7 @@ module type S = sig
val empty: unit -> t
+ val add : state -> t -> bool
val merge_set_return_new: state list -> t -> state list
val join: t -> state or_bottom
diff --git a/src/plugins/value/engine/partitioning_parameters.ml b/src/plugins/value/engine/partitioning_parameters.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d625a9ef865e0d2bc4f1627a990d0117199734fb
--- /dev/null
+++ b/src/plugins/value/engine/partitioning_parameters.ml
@@ -0,0 +1,129 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open State_partitioning
+open Value_parameters
+open Partitioning_annots
+open Cil_types
+
+let is_return s = match s.skind with Return _ -> true | _ -> false
+let is_loop s = match s.skind with Loop _ -> true | _ -> false
+
+let warn ?(current = true) = Kernel.warning ~once:true ~current
+
+module Make (Kf : Kf) : Parameters =
+struct
+ let kf = Kf.kf
+
+ let widening_delay = WideningDelay.get ()
+ let widening_period = WideningPeriod.get ()
+
+ let interpreter_mode = InterpreterMode.get ()
+
+ let slevel stmt =
+ if is_return stmt || interpreter_mode then
+ max_int
+ else match Per_stmt_slevel.local kf with
+ | Per_stmt_slevel.Global i -> i
+ | Per_stmt_slevel.PerStmt f -> f stmt
+
+ let merge_after_loop = SlevelMergeAfterLoop.mem kf
+
+ let merge stmt =
+ is_loop stmt && merge_after_loop
+ ||
+ match Per_stmt_slevel.merge kf with
+ | Per_stmt_slevel.NoMerge -> false
+ | Per_stmt_slevel.Merge f -> f stmt
+
+ let default_loop_unroll = MinLoopUnroll.get ()
+
+ let unroll stmt =
+ let local_unroll = match get_unroll_annot stmt with
+ | [] ->
+ let is_attribute a = Cil.hasAttribute a stmt.sattr in
+ begin
+ match List.filter is_attribute ["for" ; "while" ; "dowhile"] with
+ | [] -> ()
+ | loop_kind :: _ ->
+ let wkey =
+ if loop_kind = "for"
+ then Value_parameters.wkey_missing_loop_unroll_for
+ else Value_parameters.wkey_missing_loop_unroll
+ in
+ Value_parameters.warning
+ ~wkey ~source:(fst (Cil_datatype.Stmt.loc stmt)) ~once:true
+ "%s loop without unroll annotation" loop_kind
+ end;
+ None
+ | [t] ->
+ (* Inlines the value of const variables in [t]. *)
+ let global_init vi =
+ try (Globals.Vars.find vi).init with Not_found -> None
+ in
+ let t =
+ Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
+ in
+ begin match Logic_utils.constFoldTermToInt t with
+ | Some n -> Some (Integer.to_int n)
+ | None ->
+ warn "invalid term, not integer: %a" Printer.pp_term t;
+ None
+ end
+ | _ ->
+ warn "ignoring invalid unroll annotation";
+ None
+ in match local_unroll with
+ | Some n -> n
+ | None -> default_loop_unroll
+
+ let history_size = HistoryPartitioning.get ()
+
+ let universal_splits =
+ let add name l =
+ try
+ let vi = Globals.Vars.find_from_astinfo name VGlobal in
+ Cil.var vi :: l
+ with Not_found ->
+ warn ~current:false "cannot find the global variable %s for value \
+ partitioning" name;
+ l
+ in
+ ValuePartitioning.fold add []
+
+ let flow_actions stmt =
+ let term_to_lval = function
+ | {term_node = TLval tlv} ->
+ !Db.Properties.Interp.term_lval_to_lval ~result:None tlv
+ | _ ->
+ warn "split/merge expressions must be lvalues";
+ raise Exit
+ in
+ let map_annot acc t =
+ try
+ match t with
+ | FlowSplit t -> Partition.Static_split (term_to_lval t) :: acc
+ | FlowMerge t -> Partition.Static_merge (term_to_lval t) :: acc
+ with Exit -> acc (* Impossible to convert term to lval *)
+ in
+ List.fold_left map_annot [] (get_flow_annot stmt)
+end
diff --git a/src/plugins/value/engine/legacy_partitioning.mli b/src/plugins/value/engine/partitioning_parameters.mli
similarity index 95%
rename from src/plugins/value/engine/legacy_partitioning.mli
rename to src/plugins/value/engine/partitioning_parameters.mli
index 9006e977b10eb7d8b3f6c62af203180b23055a08..177cb8752a1eb4fa0d01a2140217c15fd045dbe1 100644
--- a/src/plugins/value/engine/legacy_partitioning.mli
+++ b/src/plugins/value/engine/partitioning_parameters.mli
@@ -20,4 +20,5 @@
(* *)
(**************************************************************************)
-module Make : State_partitioning.Partitioning
+module Make (Kf : State_partitioning.Kf) : State_partitioning.Parameters
+
diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli
index b9958356da1a916830c3c1d4bcce6a9164e61f50..7395634a2c1c848b59d1beb9f2fccdf51bccfd72 100644
--- a/src/plugins/value/engine/state_partitioning.mli
+++ b/src/plugins/value/engine/state_partitioning.mli
@@ -22,34 +22,32 @@
open Bottom.Type
-module type Param =
+type branch = Partition.branch
+type loop = Cil_types.stmt
+
+module type Kf =
+sig
+ val kf : Cil_types.kernel_function
+end
+
+module type Parameters =
sig
- type loop
- val kf : Cil_types.kernel_function
val widening_delay : int
val widening_period : int
val slevel : Cil_types.stmt -> int
val merge : Cil_types.stmt -> bool
val unroll : loop -> int
-end
-
-module type Domain =
-sig
- include Partitioning.Domain
- val join_list : ?into:t or_bottom -> t list -> t or_bottom
+ val history_size : int
+ val universal_splits : Cil_types.lval list
+ val flow_actions : Cil_types.stmt -> Partition.action list
end
module type Partition =
sig
- type loop (** Loops identifiers *)
type state (** The states being partitioned *)
type store (** The storage of a partition *)
type propagation (** Only contains states which needs to be propagated, i.e.
states which have not been propagated yet *)
- type shadow (** The shadow of a propagation remembers all the previous
- propagations ; shadows are useful before joins during
- descending sequences or to find if a transition is
- fireable *)
type widening (** Widening informations *)
@@ -57,7 +55,6 @@ sig
val empty_store : stmt:Cil_types.stmt option -> store
val empty_propagation : unit -> propagation
- val empty_shadow : unit -> shadow
val empty_widening : stmt:Cil_types.stmt option -> widening
(** Build the initial propagation for the entry point of a function. *)
@@ -76,7 +73,6 @@ sig
val smashed : store -> state or_bottom
val is_empty_store : store -> bool
val is_empty_propagation : propagation -> bool
- val is_empty_shadow : shadow -> bool
val store_size : store -> int
val propagation_size : propagation -> int
@@ -88,7 +84,6 @@ sig
val reset_store : store -> unit
val reset_propagation : propagation -> unit
- val reset_shadow : shadow -> unit
val reset_widening : widening -> unit
(** Resets (or just delays) the widening counter. Used on nested loops, to
@@ -120,10 +115,8 @@ sig
together inside the propagation is allowed. *)
val merge : into:propagation -> propagation -> unit
- (** Join all incoming propagations into the given store. Each propagation is
- paired with a shadow of the previous propagations on the same edge. This
- function returns a set of states which still need to be propagated past
- the store.
+ (** Join all incoming propagations into the given store. This function returns
+ a set of states which still need to be propagated past the store.
If a state from the propagations is included in another state which has
already been propagated, it may be removed from the output propagation.
@@ -134,7 +127,7 @@ sig
This function also interprets partitioning annotations at the store
vertex (slevel, splits, merges, ...) which will generally change the
current partitioning. *)
- val join : (propagation * shadow) list -> store -> propagation
+ val join : (branch * propagation) list -> store -> propagation
(** Widen a propagation at the position of the given store. The widening
object keeps track of the previous widenings to ensure termination. The
@@ -148,7 +141,8 @@ sig
end
+module type Domain = Partitioning.Domain
+
module type Partitioning =
- functor (Domain : Domain) (Param : Param) ->
+ functor (Domain : Domain) (Kf : Kf) ->
Partition with type state = Domain.t
- and type loop = Param.loop
diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml
new file mode 100644
index 0000000000000000000000000000000000000000..081851332d43db8f067848956479c918bed8c98f
--- /dev/null
+++ b/src/plugins/value/engine/trace_partitioning.ml
@@ -0,0 +1,386 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Bottom.Type
+open State_partitioning
+open Partition
+
+
+module Make (Domain : Domain) (Kf : Kf) =
+struct
+ module Parameters = Partitioning_parameters.Make (Kf)
+
+ open Kf
+ open Parameters
+
+ (* Add the split function to the domain *)
+ module Domain =
+ struct
+ include Domain
+
+ module Val = struct
+ include Main_values.CVal
+ include Structure.Open (Structure.Key_Value) (Main_values.CVal)
+ let reduce t = t
+ end
+
+ module Eva =
+ Evaluation.Make
+ (Val)
+ (Main_locations.PLoc)
+ (Cvalue_domain.State)
+
+ exception Cant_split
+
+ (* TODO: size of split limit *)
+ let split state lval =
+ (* Whenever the split fail, warn the user and exit with an exception *)
+ let fail message =
+ Value_parameters.warning ~once:true message;
+ raise Cant_split
+ in
+ (* Get the cvalue *)
+ let cvalue = match get Cvalue_domain.key with
+ | Some get_cvalue -> get_cvalue state
+ | None -> fail "cannot partition by value when the CValue domain is not\
+ active"
+ in
+ (* Retrieve the location of the lval *)
+ let cstate = Cvalue_domain.inject cvalue in
+ let location = match Eva.lvaluate ~for_writing:true cstate lval with
+ | `Value (_valuation, loc, _typ), _alarmset ->
+ Precise_locs.imprecise_location loc
+ | `Bottom, _alarmset ->
+ fail "cannot partition by value on an imprecise lvalue"
+ in
+ (* Extract the ival *)
+ let ival =
+ try
+ let v = Cvalue.Model.find cvalue location in
+ Cvalue.V.project_ival v
+ with Cvalue.V.Not_based_on_null ->
+ fail "cannot partition by value on pointers"
+ in
+ (* Build a state with the lvalue set to a singleton *)
+ let build i acc =
+ let v = Cvalue.V.inject_int i in
+ let cvalue = Cvalue.Model.add_binding ~exact:true cvalue location v in
+ let new_state = set Cvalue_domain.key cvalue state in
+ (i,new_state) :: acc
+ in
+ (* For each integer of the ival, build a new state *)
+ try
+ Ival.fold_int build ival []
+ with Abstract_interp.Error_Top ->
+ fail "too many values to partition by value on"
+ end
+
+ module Index = Partitioning.Make (Domain)
+ module Partition = Partition.Make (Domain)
+
+ type state = Domain.t
+
+ type store = {
+ size_limit : int;
+ merge : bool;
+ flow_actions : action list;
+ store_stmt : stmt option;
+ store_index : Index.t;
+ mutable store_partition : state partition;
+ mutable store_size : int;
+ }
+
+ type propagation = {
+ mutable partition : state partition;
+ }
+
+ type widening_state = {
+ widened_state : state option;
+ previous_state : state;
+ widening_counter : int;
+ }
+
+ type widening = {
+ widening_stmt : stmt;
+ mutable widening_partition : widening_state partition;
+ }
+
+ (* Constructors *)
+
+ let empty_store ~(stmt : stmt option) : store =
+ let size_limit, merge, flow_actions = match stmt with
+ | None -> max_int, false, []
+ | Some stmt -> slevel stmt, merge stmt, flow_actions stmt
+ in
+ {
+ size_limit; merge; flow_actions;
+ store_stmt = stmt;
+ store_index = Index.empty ();
+ store_partition = Partition.empty;
+ store_size = 0;
+ }
+
+ let empty_propagation () : propagation =
+ { partition = Partition.empty }
+
+ let empty_widening ~(stmt : stmt option) : widening =
+ {
+ widening_stmt = Extlib.opt_conv Cil.invalidStmt stmt;
+ widening_partition = Partition.empty;
+ }
+
+ let initial_propagation (states : state list) : propagation =
+ let partition = Partition.initial states in
+ (* Split the initial partition according to the global split seetings *)
+ let split partition lval =
+ Partition.transfer_keys partition (Dynamic_split lval)
+ in
+ let partition = List.fold_left split partition universal_splits in
+ { partition }
+
+
+ (* Pretty printing *)
+
+ let pretty_store (fmt : Format.formatter) (s : store) : unit =
+ Partition.iter (Domain.pretty fmt) s.store_partition
+
+ let pretty_propagation (fmt : Format.formatter) (p : propagation) =
+ Partition.iter (Domain.pretty fmt) p.partition
+
+
+ (* Accessors *)
+
+ let expanded (s : store) : state list =
+ Partition.to_list s.store_partition
+
+ let smashed (s : store) : state or_bottom =
+ match expanded s with
+ | [] -> `Bottom
+ | v1 :: l -> `Value (List.fold_left Domain.join v1 l)
+
+ let is_empty_store (s : store) : bool =
+ Partition.is_empty s.store_partition
+
+ let is_empty_propagation (p : propagation) : bool =
+ Partition.is_empty p.partition
+
+ let store_size (s : store) : int =
+ s.store_size
+
+ let propagation_size (p : propagation) : int =
+ Partition.size p.partition
+
+
+ (* Partition transfer functions *)
+
+ let enter_loop (p : propagation) (_i : loop) =
+ p.partition <- Partition.transfer_keys p.partition Enter_loop
+
+ let leave_loop (p : propagation) (_i : loop) =
+ p.partition <- Partition.transfer_keys p.partition Leave_loop
+
+ let next_loop_iteration (p : propagation) (i : loop) =
+ let limit = unroll i in
+ p.partition <- Partition.transfer_keys p.partition (Incr_loop limit)
+
+
+ (* Reset state (for hierchical convergence) *)
+
+ let reset_store (s : store) : unit =
+ let is_eternal key =
+ key.ration_stamp <> None
+ in
+ s.store_partition <- Partition.filter_keys is_eternal s.store_partition
+
+ let reset_propagation (p : propagation) : unit =
+ p.partition <- Partition.empty
+
+ let reset_widening (w : widening) : unit =
+ w.widening_partition <- Partition.empty
+
+ let reset_widening_counter (w : widening) : unit =
+ let reset w =
+ { w with widening_counter = max w.widening_counter (widening_period - 1) }
+ in
+ w.widening_partition <- Partition.map_states reset w.widening_partition
+
+
+ (* Operators *)
+
+ let clear_propagation (p : propagation) : unit =
+ p.partition <- Partition.empty
+
+ let transfer (f : state list -> state list) (p : propagation) : unit =
+ p.partition <- Partition.transfer_states (fun s -> f [s]) p.partition
+
+ let merge ~(into : propagation) (source : propagation) : unit =
+ (* TODO: state the precondition for this to be correct *)
+ let merge_two dest src = (* Erase the destination *)
+ if Extlib.has_some src
+ then src
+ else dest
+ in
+ into.partition <- Partition.merge merge_two into.partition source.partition
+
+ let join (sources : (branch*propagation) list) (dest : store)
+ : propagation =
+ let is_loop_head =
+ match dest.store_stmt with
+ | Some {skind=Cil_types.Loop _} -> true
+ | _ -> false
+ in
+ let current_ration = ref dest.store_size in
+ (* Update states counters *)
+ let count acc (_b,p) =
+ acc + Partition.size p.partition
+ in
+ dest.store_size <- List.fold_left count dest.store_size sources;
+ (* Get every source propagation *)
+ let source_partitions =
+ match sources with
+ | [(_,p)] -> [p.partition]
+ | sources ->
+ (* Several branches ; partition according to the incoming branch *)
+ let get (b,p) =
+ Partition.transfer_keys p.partition (Branch (b,history_size))
+ in
+ List.map get sources
+ in
+ (* Handle ration stamps *)
+ let slevel_exceeded = dest.store_size > dest.size_limit in
+ let rationing =
+ if slevel_exceeded then
+ (* No more slevel, no more ration tickets *)
+ fun p -> Partition.transfer_keys p (Ration_merge None)
+ else if dest.merge then
+ (* Merge / Merge after loop : a unique ration stamp for all *)
+ fun p -> Partition.transfer_keys p (Ration_merge (Some !current_ration))
+ else begin fun p ->
+ (* Attribute a ration stamp to each individual state *)
+ let p = Partition.transfer_keys p (Ration !current_ration) in
+ current_ration := !current_ration + Partition.size p;
+ p
+ end
+ in
+ let source_partitions = List.map rationing source_partitions in
+ (* Handle Split / Merge operations *)
+ let do_flow_actions partition =
+ let actions =
+ dest.flow_actions @ [Update_dynamic_splits ; Transfer_merge]
+ in
+ List.fold_left Partition.transfer_keys partition actions
+ in
+ let source_partitions = List.map do_flow_actions source_partitions in
+ (* Merge incomming propagations *)
+ let union = Partition.union Domain.join in
+ let partition = List.fold_left union Partition.empty source_partitions in
+ (* Add states to the store but filter out already propagated states *)
+ let update key current_state =
+ (* Inclusion test *)
+ let state =
+ try
+ let previous_state = Partition.find key dest.store_partition in
+ if Domain.is_included current_state previous_state then
+ (* The current state is included in the previous; stop *)
+ None
+ else begin
+ (* Propagate the join of the two states *)
+ if is_loop_head then
+ Value_parameters.feedback ~level:1 ~once:true ~current:true
+ "starting to merge loop iterations";
+ Some (Domain.join previous_state current_state)
+ end
+ with
+ (* There is no previous state, propagate normally *)
+ Not_found -> Some current_state
+ in
+ (* Add the propagated state to the store *)
+ let add s =
+ dest.store_partition <- Partition.replace key s dest.store_partition;
+ in
+ Extlib.may add state;
+ (* Filter out already propagated states *)
+ Extlib.opt_filter (fun s -> Index.add s dest.store_index) state
+ in
+ let partition = Partition.map_filter update partition in
+ { partition }
+
+
+ let widen (_s : store) (w : widening) (p : propagation) : bool =
+ let stmt = w.widening_stmt in
+ (* Auxiliary function to update the result *)
+ let update key widening_state =
+ w.widening_partition <-
+ Partition.replace key widening_state w.widening_partition
+ in
+ (* Apply widening to each leaf *)
+ let widen_one key curr =
+ try
+ (* Search for an already existing widening state *)
+ let wstate = Partition.find key w.widening_partition in
+ (* Update the widening state *)
+ update key {
+ wstate with
+ previous_state = curr;
+ widening_counter = wstate.widening_counter - 1
+ };
+ (* Propagated state decreases, stop to propagate *)
+ if Domain.is_included curr wstate.previous_state then
+ None
+ (* Widening is delayed *)
+ else if wstate.widening_counter > 0 then begin
+ Some curr
+ (* Apply widening *)
+ end else begin
+ Value_parameters.feedback ~level:1 ~once:true ~current:true
+ ~dkey:Value_parameters.dkey_widening
+ "applying a widening at this point";
+ (* We join the previous widening state with the previous iteration
+ state so as to allow the intermediate(s) iteration(s) (between
+ two widenings) to stabilize at least a part of the state. *)
+ let prev = match wstate.widened_state with
+ | Some v -> Domain.join wstate.previous_state v
+ | None -> wstate.previous_state
+ in
+ let next = Domain.widen kf stmt prev (Domain.join prev curr) in
+ update key {
+ previous_state = next;
+ widened_state = Some next;
+ widening_counter = widening_period - 1;
+ };
+ Some next
+ end
+ with Not_found ->
+ (* The key is not in the widening state; add it if slevel is not
+ exceeded *)
+ if key.ration_stamp = None then
+ update key {
+ widened_state = None;
+ previous_state = curr;
+ widening_counter = widening_delay - 1;
+ };
+ Some curr
+ in
+ p.partition <- Partition.map_filter widen_one p.partition;
+ Partition.is_empty p.partition
+end
diff --git a/src/plugins/value/engine/basic_partitioning.mli b/src/plugins/value/engine/trace_partitioning.mli
similarity index 99%
rename from src/plugins/value/engine/basic_partitioning.mli
rename to src/plugins/value/engine/trace_partitioning.mli
index 9006e977b10eb7d8b3f6c62af203180b23055a08..07d509e4b5c203ebba676300dda6930ee5f22c12 100644
--- a/src/plugins/value/engine/basic_partitioning.mli
+++ b/src/plugins/value/engine/trace_partitioning.mli
@@ -21,3 +21,4 @@
(**************************************************************************)
module Make : State_partitioning.Partitioning
+
diff --git a/src/plugins/value/slevel/per_stmt_slevel.ml b/src/plugins/value/slevel/per_stmt_slevel.ml
index 4c9b5b4fe09d3e4dcc77cf0f66ada2aecad65cda..ca504df3baeb37c32d6aa5048117373d27e3afb6 100644
--- a/src/plugins/value/slevel/per_stmt_slevel.ml
+++ b/src/plugins/value/slevel/per_stmt_slevel.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Partitioning_annots
module G = struct
type t = kernel_function
@@ -39,54 +40,6 @@ end
module Dfs = Graph.Traverse.Dfs(G)
-(* We use the following encoding to store the directives in the AST: *)
-type local_slevel =
- | LMerge (* encoded as '"merge"' *)
- | LDefault (* encoded as '"default"' *)
- | LLocal of int (* encoded as 'Const i' *)
-
-let retrieve_annot lt =
- match lt with
- | [{term_node = TConst (Integer (i, _))}] ->
- LLocal (Integer.to_int i)
- | [{term_node = TConst (LStr "default")}] -> LDefault
- | [{term_node = TConst (LStr "merge")}] -> LMerge
- | _ -> LDefault (* be kind. Someone is bound to write a visitor that will
- simplify our term into something unrecognizable... *)
-
-let () = Logic_typing.register_code_annot_next_stmt_extension "slevel" false
- (fun ~typing_context:_ ~loc args ->
- let abort () =
- Value_parameters.abort ~source:(fst loc) "Invalid slevel directive"
- in
- let open Logic_ptree in
- let p = match args with
- | [{lexpr_node = PLvar ("default" | "merge" as s)}] ->
- Logic_const.tstring s
- | [{lexpr_node = PLconstant (IntConstant i)}] ->
- begin
- try
- let i = int_of_string i in
- if i < 0 then abort ();
- Logic_const.tinteger i
- with Failure _ -> abort ()
- end
- | _ -> abort ()
- in
- Ext_terms [p]
- )
-
-let () = Cil_printer.register_code_annot_extension "slevel"
- (fun _pp fmt lp ->
- match lp with
- | Ext_id _ | Ext_preds _ -> assert false
- | Ext_terms lt ->
- match retrieve_annot lt with
- | LDefault -> Format.pp_print_string fmt "default"
- | LMerge -> Format.pp_print_string fmt "merge"
- | LLocal i -> Format.pp_print_int fmt i
- )
-
type slevel =
| Global of int
| PerStmt of (stmt -> int)
@@ -111,19 +64,9 @@ module DatatypeMerge = Datatype.Make(struct
let mem_project = Datatype.never_any_project
end)
-let extract_slevel_directive s =
- let rec find_one l =
- match l with
- | [] -> None
- | {annot_content = AExtended(_,_,(_,"slevel", _, _,Ext_terms lp))} :: _ ->
- Some (retrieve_annot lp)
- | _ :: q -> find_one q
- in
- find_one (Annotations.code_annot s)
-
let kf_contains_slevel_directive kf =
List.exists
- (fun stmt -> extract_slevel_directive stmt <> None)
+ (fun stmt -> get_slevel_annot stmt <> None)
(Kernel_function.get_definition kf).sallstmts
let compute kf =
@@ -139,15 +82,15 @@ let compute kf =
(* Before visiting the successors of the statement: push or pop according
to directive *)
let pre s =
- match extract_slevel_directive s with
- | None | Some LMerge as d ->
+ match get_slevel_annot s with
+ | None | Some SlevelMerge as d ->
Cil_datatype.Stmt.Hashtbl.add h_local s (Stack.top local_slevel);
if d <> None then Cil_datatype.Stmt.Hashtbl.add h_merge s ();
- | Some (LLocal i) ->
+ | Some (SlevelLocal i) ->
if debug then Format.printf "Vising split %d, pushing %d@." s.sid i;
Cil_datatype.Stmt.Hashtbl.add h_local s i;
Stack.push i local_slevel;
- | Some LDefault ->
+ | Some SlevelDefault ->
let top = Stack.pop local_slevel in
if debug then
Format.printf "Visiting merge %d, poping (prev %d)@." s.sid top;
@@ -157,12 +100,12 @@ let compute kf =
(* after the visit of a statement and its successors. Do the converse
operation of pre *)
and post s =
- match extract_slevel_directive s with
- | None | Some LMerge -> ()
- | Some (LLocal _) ->
+ match get_slevel_annot s with
+ | None | Some SlevelMerge -> ()
+ | Some (SlevelLocal _) ->
if debug then Format.printf "Leaving split %d, poping@." s.sid;
ignore (Stack.pop local_slevel);
- | Some LDefault ->
+ | Some SlevelDefault ->
(* slevel on nodes above s *)
let above = Cil_datatype.Stmt.Hashtbl.find h_local s in
(* slevel on s and on the nodes below *)
diff --git a/src/plugins/value/utils/partitioning_annots.ml b/src/plugins/value/utils/partitioning_annots.ml
new file mode 100644
index 0000000000000000000000000000000000000000..55908660a051c0b6b1d48ed6fd073f040d643f21
--- /dev/null
+++ b/src/plugins/value/utils/partitioning_annots.ml
@@ -0,0 +1,175 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Logic_ptree
+
+[@@@ warning "-42"]
+
+type slevel_annotation =
+ | SlevelMerge
+ | SlevelDefault
+ | SlevelLocal of int
+
+type unroll_annotation = term
+
+type flow_annotation =
+ | FlowSplit of term
+ | FlowMerge of term
+
+
+exception Parse_error
+
+module type Annotation =
+sig
+ type t
+
+ val name : string
+ val is_loop_annot : bool
+ val parse : typing_context:Logic_typing.typing_context -> lexpr list -> t
+ val export : t -> acsl_extension_kind
+ val import : acsl_extension_kind -> t
+ val print : Format.formatter -> t -> unit
+end
+
+module Register (M : Annotation) =
+struct
+ include M
+
+ let typing_ext ~typing_context ~loc args =
+ try export (parse ~typing_context args)
+ with Parse_error ->
+ typing_context.Logic_typing.error loc "Invalid %s directive" name
+
+ let printer_ext _pp fmt lp =
+ print fmt (import lp)
+
+ let () =
+ if is_loop_annot then begin
+ Logic_typing.register_code_annot_next_loop_extension name false typing_ext;
+ Cil_printer.register_loop_annot_extension name printer_ext
+ end else begin
+ Logic_typing.register_code_annot_next_stmt_extension name false typing_ext;
+ Cil_printer.register_code_annot_extension name printer_ext
+ end
+
+ let get stmt =
+ let filter_add _emitter annot acc =
+ match annot.annot_content with
+ | Cil_types.AExtended (_, is_loop_annot', (_,name',_,_,data))
+ when name' = name && is_loop_annot' = is_loop_annot ->
+ import data :: acc
+ | _ -> acc
+ in
+ List.rev (Annotations.fold_code_annot filter_add stmt [])
+end
+
+
+module Slevel = Register (struct
+ type t = slevel_annotation
+
+ let name = "slevel"
+ let is_loop_annot = false
+
+ let parse ~typing_context:_ = function
+ | [{lexpr_node = PLvar "default"}] -> SlevelDefault
+ | [{lexpr_node = PLvar "merge"}] -> SlevelMerge
+ | [{lexpr_node = PLconstant (IntConstant i)}] ->
+ let i =
+ try int_of_string i
+ with Failure _ -> raise Parse_error
+ in
+ if i < 0 then raise Parse_error;
+ SlevelLocal i
+ | _ -> raise Parse_error
+
+ let export = function
+ | SlevelDefault -> Ext_terms [Logic_const.tstring "default"]
+ | SlevelMerge -> Ext_terms [Logic_const.tstring "merge"]
+ | SlevelLocal i -> Ext_terms [Logic_const.tinteger i]
+
+ let import = function
+ | Ext_terms [{term_node}] ->
+ begin match term_node with
+ | TConst (LStr "default") -> SlevelDefault
+ | TConst (LStr "merge") -> SlevelMerge
+ | TConst (Integer (i, _)) -> SlevelLocal (Integer.to_int i)
+ | _ -> SlevelDefault (* be kind. Someone is bound to write a visitor that
+ will simplify our term into something
+ unrecognizable... *)
+ end
+ | _ -> assert false
+
+ let print fmt = function
+ | SlevelDefault -> Format.pp_print_string fmt "default"
+ | SlevelMerge -> Format.pp_print_string fmt "merge"
+ | SlevelLocal i -> Format.pp_print_int fmt i
+ end)
+
+module SimpleTermAnnotation =
+struct
+ type t = term
+
+ let parse ~typing_context = function
+ | [t] ->
+ let open Logic_typing in
+ typing_context.type_term typing_context typing_context.pre_state t
+ | _ -> raise Parse_error
+
+ let export t =
+ Ext_terms [t]
+
+ let import = function
+ | Ext_terms [t] -> t
+ | _ -> assert false
+
+ let print = Printer.pp_term
+end
+
+module Unroll = Register (struct
+ include SimpleTermAnnotation
+ let name = "unroll"
+ let is_loop_annot = true
+ end)
+
+module Split = Register (struct
+ include SimpleTermAnnotation
+ let name = "split"
+ let is_loop_annot = false
+ end)
+
+module Merge = Register (struct
+ include SimpleTermAnnotation
+ let name = "merge"
+ let is_loop_annot = false
+ end)
+
+
+let get_slevel_annot stmt =
+ try Some (List.hd (Slevel.get stmt))
+ with Failure _ -> None
+
+let get_unroll_annot stmt = Unroll.get stmt
+
+let get_flow_annot stmt =
+ List.map (fun a -> FlowSplit a) (Split.get stmt) @
+ List.map (fun a -> FlowMerge a) (Merge.get stmt)
diff --git a/src/plugins/value/utils/unroll_annots.mli b/src/plugins/value/utils/partitioning_annots.mli
similarity index 80%
rename from src/plugins/value/utils/unroll_annots.mli
rename to src/plugins/value/utils/partitioning_annots.mli
index f47d4f9ea36ca3fc749f09f85f500c0e6db00255..264cd94a5f0f25e3f3e82dfed7108f8bc89cd2b7 100644
--- a/src/plugins/value/utils/unroll_annots.mli
+++ b/src/plugins/value/utils/partitioning_annots.mli
@@ -20,8 +20,17 @@
(* *)
(**************************************************************************)
-(** Syntax extension for unrolling annotations, used by Eva. *)
+type slevel_annotation =
+ | SlevelMerge
+ | SlevelDefault
+ | SlevelLocal of int
-open Cil_types
+type unroll_annotation = Cil_types.term
-val get_unroll_terms : stmt -> term list
+type flow_annotation =
+ | FlowSplit of Cil_types.term
+ | FlowMerge of Cil_types.term
+
+val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
+val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
+val get_flow_annot : Cil_types.stmt -> flow_annotation list
diff --git a/src/plugins/value/utils/unroll_annots.ml b/src/plugins/value/utils/unroll_annots.ml
deleted file mode 100644
index 3c2ae1c955ca2d81332b6c8ccd7ae388f5dd7b2e..0000000000000000000000000000000000000000
--- a/src/plugins/value/utils/unroll_annots.ml
+++ /dev/null
@@ -1,54 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-exception Parse_error of string option
-
-let parse_error ?msg () = raise (Parse_error msg)
-
-let () = Logic_typing.register_code_annot_next_loop_extension "unroll" false
- begin fun ~typing_context ~loc:_ args ->
- match args with
- | [arg] ->
- let open Logic_typing in
- Ext_terms
- [typing_context.type_term typing_context typing_context.pre_state arg]
- | _ -> parse_error ~msg:"must be a single term" ()
- end
-
-let () = Cil_printer.register_behavior_extension "unroll"
- begin fun _pp fmt lp ->
- match lp with
- | Ext_terms [t] -> Printer.pp_term fmt t
- | Ext_id _ | Ext_preds _ | Ext_terms _ -> assert false
- end
-
-let get_unroll_terms stmt =
- Annotations.fold_code_annot
- (fun _emitter annot acc ->
- match annot with
- | {annot_content =
- AExtended (_, true, (_, "unroll", _,_,Ext_terms [term]))} ->
- term :: acc
- | _ -> acc
- ) stmt []
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 7b0254eb4854e6efd6d47df74d0e7ef0ed107de7..051104b6512fc80a9bc51ba83d09febea2a4d41c 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -589,6 +589,8 @@ let () = InitializationPaddingGlobals.add_aliases ["-val-initialization-padding-
(* --- Tuning --- *)
(* ------------------------------------------------------------------------- *)
+(* --- Iteration strategy --- *)
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.is_invisible ()
module DescendingIteration =
@@ -645,22 +647,7 @@ module WideningPeriod =
let () = WideningDelay.set_range ~min:1 ~max:max_int
let () = add_precision_dep WideningPeriod.parameter
-let () = Parameter_customize.set_group precision_tuning
-module ILevel =
- Int
- (struct
- let option_name = "-eva-ilevel"
- let default = 8
- let arg_name = "n"
- let help =
- "Sets of integers are represented as sets up to <n> elements. \
- Above, intervals with congruence information are used \
- (defaults to 8, must be between 4 and 128)"
- end)
-let () = add_precision_dep ILevel.parameter
-let () = ILevel.add_aliases ["-val-ilevel"]
-let () = ILevel.add_update_hook (fun _ i -> Ival.set_small_cardinal i)
-let () = ILevel.set_range 4 256
+(* --- Partitioning --- *)
let () = Parameter_customize.set_group precision_tuning
module SemanticUnrollingLevel =
@@ -727,6 +714,31 @@ module MinLoopUnroll =
let () = add_precision_dep MinLoopUnroll.parameter
let () = MinLoopUnroll.set_range 0 max_int
+let () = Parameter_customize.set_group precision_tuning
+module HistoryPartitioning =
+ Int
+ (struct
+ let option_name = "-eva-partition-history"
+ let arg_name = "n"
+ let default = 0
+ let help =
+ "keep states distincts as long as the <n> last branching in their\
+ traces are also distinct. (A value of 0 deactivate this feature)"
+ end)
+let () = add_precision_dep HistoryPartitioning.parameter
+let () = HistoryPartitioning.set_range 0 max_int
+
+let () = Parameter_customize.set_group precision_tuning
+module ValuePartitioning =
+ String_set
+ (struct
+ let option_name = "-eva-partition-value"
+ let help = "partition the space of reachable states according to the \
+ possible values of the global(s) variable(s) V."
+ let arg_name = "V"
+ end)
+let () = add_precision_dep ValuePartitioning.parameter
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
module SplitReturnFunction =
@@ -780,6 +792,25 @@ let () =
let () = add_precision_dep SplitReturn.parameter
let () = SplitReturn.add_aliases ["-val-split-return"]
+(* --- Misc --- *)
+
+let () = Parameter_customize.set_group precision_tuning
+module ILevel =
+ Int
+ (struct
+ let option_name = "-eva-ilevel"
+ let default = 8
+ let arg_name = "n"
+ let help =
+ "Sets of integers are represented as sets up to <n> elements. \
+ Above, intervals with congruence information are used \
+ (defaults to 8, must be between 4 and 128)"
+ end)
+let () = add_precision_dep ILevel.parameter
+let () = ILevel.add_aliases ["-val-ilevel"]
+let () = ILevel.add_update_hook (fun _ i -> Ival.set_small_cardinal i)
+let () = ILevel.set_range 4 256
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
module BuiltinsOverrides =
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index c6a81aa6e935db912cd109fdec2d1c5f6ea3c6cf..c6891422da333e93705ee8f140834f7398e232db 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -72,6 +72,11 @@ module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set
module IgnoreRecursiveCalls: Parameter_sig.Bool
+module DescendingIteration: Parameter_sig.String
+module HierarchicalConvergence: Parameter_sig.Bool
+module WideningDelay: Parameter_sig.Int
+module WideningPeriod: Parameter_sig.Int
+
module SemanticUnrollingLevel: Parameter_sig.Int
module SlevelFunction:
Parameter_sig.Map with type key = Cil_types.kernel_function
@@ -80,11 +85,9 @@ module SlevelFunction:
module SlevelMergeAfterLoop: Parameter_sig.Kernel_function_set
module MinLoopUnroll : Parameter_sig.Int
+module HistoryPartitioning : Parameter_sig.Int
+module ValuePartitioning : Parameter_sig.String_set
-module DescendingIteration: Parameter_sig.String
-module HierarchicalConvergence: Parameter_sig.Bool
-module WideningDelay: Parameter_sig.Int
-module WideningPeriod: Parameter_sig.Int
module ArrayPrecisionLevel: Parameter_sig.Int
module AllocatedContextValid: Parameter_sig.Bool
diff --git a/tests/misc/unroll_annots.c b/tests/misc/unroll_annots.c
deleted file mode 100644
index 9154b42da50951e4ded83202de0eacb935147d7f..0000000000000000000000000000000000000000
--- a/tests/misc/unroll_annots.c
+++ /dev/null
@@ -1,22 +0,0 @@
-#define N 10
-int a[N], b[N];
-
-int main() {
- //@ loop unroll N;
- for (int i = 0; i < N; i++) {
- //@ loop unroll 1;
- for (int j = 0; j < N; j++) {
- a[i] = 42;
- }
- }
-
- //@ loop unroll 1;
- for (int i = 0; i < N; i++) {
- //@ loop unroll N;
- for (int j = 0; j < N; j++) {
- b[j] = 42;
- }
- }
-
- return 0;
-}
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..75f64a73b09ab27c502e61cbf524958617be1403
--- /dev/null
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -0,0 +1,26 @@
+[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_unroll
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ k ∈ {0}
+[eva] tests/value/partitioning-annots.c:25: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:33: starting to merge loop iterations
+[eva] tests/value/partitioning-annots.c:35: starting to merge loop iterations
+[eva] Recording results for test_unroll
+[eva] done for function test_unroll
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_unroll:
+ a[0..9] ∈ {42}
+ b[0..9] ∈ {42}
+[from] Computing for function test_unroll
+[from] Done for function test_unroll
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function test_unroll:
+ NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_unroll:
+ a[0..9]; b[0..9]; i; j; i_0; j_0
+[inout] Inputs for function test_unroll:
+ \nothing
diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8778196f4add115ff01d5d80a512da5ab26ba11f
--- /dev/null
+++ b/tests/value/oracle/partitioning-annots.1.res.oracle
@@ -0,0 +1,68 @@
+[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_split
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ k ∈ {0}
+[eva] computing for function Frama_C_interval <- test_split.
+ Called from tests/value/partitioning-annots.c:47.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:47:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_split.
+ Called from tests/value/partitioning-annots.c:48.
+[eva] tests/value/partitioning-annots.c:48:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:54:
+ Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:57:
+ Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:57:
+ Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {0}, {0}, {0}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {0}, {2}, {0}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {1}, {0}, {1}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {1}, {1}, {1}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {1}, {2}, {1}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1}
+[eva] tests/value/partitioning-annots.c:63:
+ Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1}
+[eva] Recording results for test_split
+[eva] done for function test_split
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_split:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ {0; 1}
+ i ∈ {0; 1}
+ j ∈ {0; 1; 2}
+[from] Computing for function test_split
+[from] Computing for function Frama_C_interval <-test_split
+[from] Done for function Frama_C_interval
+[from] Done for function test_split
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function test_split:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ k FROM Frama_C_entropy_source
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_split:
+ Frama_C_entropy_source; k; i; j
+[inout] Inputs for function test_split:
+ Frama_C_entropy_source; k
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c41cff4e89944fac83d636b9c12be7c77acab2cf
--- /dev/null
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -0,0 +1,76 @@
+[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_split
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ k ∈ {0}
+[eva] computing for function Frama_C_interval <- test_split.
+ Called from tests/value/partitioning-annots.c:47.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:47:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_split.
+ Called from tests/value/partitioning-annots.c:48.
+[eva] tests/value/partitioning-annots.c:48:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:54:
+ Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:57:
+ Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:57:
+ Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {0}, {0}, {0}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {0}, {2}, {0}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {1}, {0}, {1}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {1}, {1}, {1}
+[eva] tests/value/partitioning-annots.c:59:
+ Frama_C_show_each_before_first_merge: {1}, {2}, {1}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {0}, {0}, {0}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {1}, {0}, {1}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {0}, {1}, {0}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {1}, {1}, {1}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {0}, {2}, {0}
+[eva] tests/value/partitioning-annots.c:61:
+ Frama_C_show_each_before_second_merge: {1}, {2}, {1}
+[eva] tests/value/partitioning-annots.c:63:
+ Frama_C_show_each_end: {0}, {0; 1; 2}, {0}
+[eva] tests/value/partitioning-annots.c:63:
+ Frama_C_show_each_end: {1}, {0; 1; 2}, {1}
+[eva] Recording results for test_split
+[eva] done for function test_split
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_split:
+ Frama_C_entropy_source ∈ [--..--]
+ k ∈ {0; 1}
+ i ∈ {0; 1}
+ j ∈ {0; 1; 2}
+[from] Computing for function test_split
+[from] Computing for function Frama_C_interval <-test_split
+[from] Done for function Frama_C_interval
+[from] Done for function test_split
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function test_split:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ k FROM Frama_C_entropy_source
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_split:
+ Frama_C_entropy_source; k; i; j
+[inout] Inputs for function test_split:
+ Frama_C_entropy_source; k
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..276bbc7d39325158489c457f78d399d100539768
--- /dev/null
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -0,0 +1,67 @@
+[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_loop_split
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ k ∈ {0}
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:81.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:81:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:81.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:79: starting to merge loop iterations
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:81.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:81.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:81.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+ Called from tests/value/partitioning-annots.c:81.
+[eva] Done for function Frama_C_interval
+[eva:alarm] tests/value/partitioning-annots.c:88: Warning:
+ accessing uninitialized left-value. assert \initialized(&A[i]);
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {0}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {1}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {2}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {3}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {4}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {5}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {6}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {7}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {8}, {42}
+[eva] tests/value/partitioning-annots.c:93: Frama_C_show_each: {9}, {42}
+[eva] tests/value/partitioning-annots.c:94: assertion got status valid.
+[eva] tests/value/partitioning-annots.c:97:
+ Frama_C_show_each: {{ "Value 42 not found" }}
+[eva] Recording results for test_loop_split
+[eva] done for function test_loop_split
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_loop_split:
+ Frama_C_entropy_source ∈ [--..--]
+ A[0] ∈ [0..100]
+ [1..9] ∈ [0..100] or UNINITIALIZED
+ i ∈ [0..10]
+[from] Computing for function test_loop_split
+[from] Computing for function Frama_C_interval <-test_loop_split
+[from] Done for function Frama_C_interval
+[from] Done for function test_loop_split
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function test_loop_split:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_loop_split:
+ Frama_C_entropy_source; A[0..9]; i
+[inout] Inputs for function test_loop_split:
+ Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a2c98fb07a7bc198ce0425de2a4edbfd9082503c
--- /dev/null
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -0,0 +1,39 @@
+[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_history
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ k ∈ {0}
+[eva] computing for function Frama_C_interval <- test_history.
+ Called from tests/value/partitioning-annots.c:103.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:103:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:109: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] tests/value/partitioning-annots.c:112: Warning:
+ division by zero. assert j ≢ 0;
+[eva] Recording results for test_history
+[eva] done for function test_history
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_history:
+ Frama_C_entropy_source ∈ [--..--]
+ i ∈ {0; 1}
+ j ∈ {0; 1}
+ k_0 ∈ {1}
+[from] Computing for function test_history
+[from] Computing for function Frama_C_interval <-test_history
+[from] Done for function Frama_C_interval
+[from] Done for function test_history
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function test_history:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_history:
+ Frama_C_entropy_source; i; j; k_0
+[inout] Inputs for function test_history:
+ Frama_C_entropy_source
diff --git a/tests/value/oracle/partitioning-annots.5.res.oracle b/tests/value/oracle/partitioning-annots.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d0d38833a469d604f5c41b04875eba90472e49ad
--- /dev/null
+++ b/tests/value/oracle/partitioning-annots.5.res.oracle
@@ -0,0 +1,38 @@
+[kernel] Parsing tests/value/partitioning-annots.c (with preprocessing)
+[eva] Analyzing a complete application starting at test_history
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ k ∈ {0}
+[eva] computing for function Frama_C_interval <- test_history.
+ Called from tests/value/partitioning-annots.c:103.
+[eva] using specification for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:103:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/partitioning-annots.c:109: Frama_C_show_each: {1}, {1}
+[eva] tests/value/partitioning-annots.c:109: Frama_C_show_each: {0}, {0}
+[eva] Recording results for test_history
+[eva] done for function test_history
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_history:
+ Frama_C_entropy_source ∈ [--..--]
+ i ∈ {0; 1}
+ j ∈ {0; 1}
+ k_0 ∈ {1}
+[from] Computing for function test_history
+[from] Computing for function Frama_C_interval <-test_history
+[from] Done for function Frama_C_interval
+[from] Done for function test_history
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function test_history:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function test_history:
+ Frama_C_entropy_source; i; j; k_0
+[inout] Inputs for function test_history:
+ Frama_C_entropy_source
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
new file mode 100644
index 0000000000000000000000000000000000000000..0e22c9b32f025b5a053945e9c9b2653e407b15a9
--- /dev/null
+++ b/tests/value/partitioning-annots.c
@@ -0,0 +1,121 @@
+/* run.config*
+ GCC:
+ STDOPT: #"-main test_unroll"
+ STDOPT: #"-main test_split"
+ STDOPT: +"-main test_split -eva-partition-value k"
+ STDOPT: #"-main test_loop_split -eva-partition-history 1"
+ STDOPT: #"-main test_history -eva-partition-history 0"
+ STDOPT: #"-main test_history -eva-partition-history 1"
+ */
+
+#include "__fc_builtin.h"
+
+#define N 10
+
+void test_unroll()
+{
+ int a[N], b[N];
+
+ // The inner loop needs to be unrolled to allow strong updates
+ // The outer loops doesn't need to be unrolled
+
+ //@ loop unroll N;
+ for (int i = 0; i < N; i++) {
+ //@ loop unroll 1;
+ for (int j = 0; j < N; j++) {
+ a[i] = 42;
+ }
+ }
+
+ // This time the outer loop needs unrolling but not the inner loop
+
+ //@ loop unroll 1;
+ for (int i = 0; i < N; i++) {
+ //@ loop unroll N;
+ for (int j = 0; j < N; j++) {
+ b[j] = 42;
+ }
+ }
+
+ // At the end, we must have both arrays a and b to be fully initialized at 42
+}
+
+int k;
+
+void test_split()
+{
+ int i = Frama_C_interval(0,1);
+ int j = Frama_C_interval(0,2);
+
+ // The splits are done on i and j and undone in the same order
+ // If global dynamic split is done on k, since it is equaly to i, merge i will
+ // have no effects.
+
+ Frama_C_show_each_before_first_split(i,j,k);
+ //@ split i;
+ k = i;
+ Frama_C_show_each_before_second_split(i,j,k);
+ //@ split j;
+ Frama_C_show_each_before_first_merge(i,j,k);
+ //@ merge i;
+ Frama_C_show_each_before_second_merge(i,j,k);
+ //@ merge j;
+ Frama_C_show_each_end(i,j,k);
+}
+
+void test_loop_split()
+{
+ int A[N];
+ int i;
+
+ // In this example we can split on the value of the loop index in order to
+ // keep the relation between i and the value A[i] found in the array to be
+ // equal to 42.
+ // However, since the split is not dynamic, an history partitioning must be
+ // added to distinguish between the two states that share i = 9 : those who
+ // left the loop at the break point and those who left after the loop test.
+
+ // Init a random array
+ for (i = 0 ; i < N ; i ++)
+ {
+ A[i] = Frama_C_interval(0,100);
+ }
+
+ // Search for some value
+ for (i = 0 ; i < N ; i++)
+ {
+ //@ split i;
+ if (A[i] == 42)
+ break;
+ }
+
+ if (i < N) {
+ Frama_C_show_each(i, A[i]);
+ //@ assert A[i] == 42;
+ }
+ else {
+ Frama_C_show_each("Value 42 not found");
+ }
+}
+
+void test_history()
+{
+ int i = Frama_C_interval(0,1);
+ int j = 0, k = 1;
+
+ if (i)
+ j = 1;
+
+ Frama_C_show_each(i, j);
+
+ if (i)
+ k = k / j;
+}
+
+void main(void)
+{
+ test_unroll();
+ test_split();
+ test_loop_split();
+}
+