From e9c60779e79c220fa924dd67b6b5081983fcf894 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 11 Mar 2020 14:51:26 +0100
Subject: [PATCH] [WIP] [Eva] Enable descending sequences
---
Makefile | 1 +
src/plugins/value/partitioning/join_cache.ml | 95 +++++++++++++++++++
src/plugins/value/partitioning/join_cache.mli | 47 +++++++++
src/plugins/value/partitioning/partition.ml | 24 ++++-
.../value/partitioning/trace_partitioning.ml | 1 +
5 files changed, 167 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/value/partitioning/join_cache.ml
create mode 100644 src/plugins/value/partitioning/join_cache.mli
diff --git a/Makefile b/Makefile
index d23384d9cc8..9a30035ad52 100644
--- a/Makefile
+++ b/Makefile
@@ -905,6 +905,7 @@ PLUGIN_CMO:= partitioning/split_strategy value_parameters \
engine/recursion engine/transfer_stmt engine/transfer_specification \
partitioning/auto_loop_unroll \
partitioning/partition partitioning/partitioning_parameters \
+ partitioning/join_cache \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
diff --git a/src/plugins/value/partitioning/join_cache.ml b/src/plugins/value/partitioning/join_cache.ml
new file mode 100644
index 00000000000..6b8c9aaa929
--- /dev/null
+++ b/src/plugins/value/partitioning/join_cache.ml
@@ -0,0 +1,95 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module type Domain =
+sig
+ type t
+ val join : t -> t -> t
+end
+
+module type Tag =
+sig
+ type t
+ val equal : t -> t -> bool
+end
+
+module Make (Domain : Domain) (Tag : Tag) =
+struct
+ type state = Domain.t
+ type tag = Tag.t
+
+ type partial_join = {
+ last_tag: tag;
+ last_state: state;
+ last_join: state;
+ }
+
+ type t = {
+ mutable joined: partial_join list;
+ mutable unjoined: (tag * state) list;
+ }
+
+ let create () = {
+ joined = [];
+ unjoined = []
+ }
+
+ let add tag state cache =
+ cache.unjoined <- (tag, state) :: cache.unjoined
+
+ let remove tag cache =
+ (* Find the elements with tag in the joined list *)
+ (* At all times, collect left right acc l satisfies
+ - acc @ l is the original list with some of the filtered elements removed
+ - acc have all the filtered elements removed
+ - l does not
+ - left, right is a snapshot of acc, l, the last time a filtered element
+ have been encountered, the begining of the iteration if none *)
+ let rec collect left right acc = function
+ | [] -> left, right
+ | pj :: t when Tag.equal pj.last_tag tag -> collect acc t acc t
+ | pj :: t -> collect left right (pj :: acc) t
+ in
+ (* Split the list in two part: at the left and at the righ of the element *)
+ let left, right = collect [] cache.joined [] cache.joined in
+ (* Update the cache *)
+ cache.joined <- right;
+ cache.unjoined <-
+ List.filter (fun (tag',_state) -> Tag.equal tag' tag) cache.unjoined @
+ List.map (fun pj -> pj.last_tag, pj.last_state) left
+
+ let join cache =
+ let append (last_tag,last_state) =
+ let new_element = match cache.joined with
+ | [] ->
+ { last_tag ; last_state ; last_join=last_state }
+ | { last_join } :: _ ->
+ { last_tag ; last_state ; last_join=Domain.join last_join last_state }
+ in
+ cache.joined <- new_element :: cache.joined
+ in
+ List.iter append (List.rev cache.unjoined);
+ cache.unjoined <- [];
+ match cache.joined with
+ | [] -> `Bottom
+ | { last_join } :: _ -> `Value last_join
+end
diff --git a/src/plugins/value/partitioning/join_cache.mli b/src/plugins/value/partitioning/join_cache.mli
new file mode 100644
index 00000000000..a1de53720ab
--- /dev/null
+++ b/src/plugins/value/partitioning/join_cache.mli
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(* *)
+(* 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 Bottom.Type
+
+module type Domain =
+sig
+ type t
+ val join : t -> t -> t
+end
+
+module type Tag =
+sig
+ type t
+ val equal : t -> t -> bool
+end
+
+module Make (Domain : Domain) (Tag : Tag) :
+sig
+ type state = Domain.t
+ type tag = Tag.t
+ type t
+
+ val create : unit -> t
+ val add : tag -> state -> t -> unit
+ val remove : tag -> t -> unit
+ val join : t -> state or_bottom
+end
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index 977dce271f2..f1921f3d359 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -22,6 +22,24 @@
open Bottom.Type
+(* --- Tagging --- *)
+
+(* Tags are stored in keys to track states through the propagation *)
+
+module Tag =
+struct
+ include Datatype.Int64
+
+ let fresh : unit -> t =
+ let last = ref Int64.zero in
+ fun () ->
+ last := Int64.succ !last;
+ !last
+end
+
+type tag = Tag.t
+
+
(* --- Split monitors --- *)
type split_monitor = {
@@ -80,13 +98,17 @@ type branch = int
the split creates states in which the expression evalutates to a
singleton, the values of the map are integers.
Static splits are only evaluated when the annotation is encountered
- whereas dynamic splits are reevaluated regularly. *)
+ whereas dynamic splits are reevaluated regularly.
+ Additionnaly, the key store a tag that is used to track the state it is
+ associated with. This tag is not used during the indexing process and thus
+ cannot differentiate keys. *)
type key = {
ration_stamp : stamp;
branches : branch list;
loops : (int * int) list; (* current iteration / max unrolling *)
static_split : (Integer.t*split_monitor) ExpMap.t; (* exp->value*monitor *)
dynamic_split : (Integer.t*split_monitor) ExpMap.t; (* exp->value*monitor *)
+ tag : tag;
}
module Key =
diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index aa261fbfb89..f0f91e0a50c 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -37,6 +37,7 @@ struct
module Index = Partitioning_index.Make (Domain)
module Flow = Partition.MakeFlow (Abstract)
+ module JoinCache = Join_cache.Make (Domain) (Partition.Tag)
type state = Domain.t
--
GitLab