From 890d33fc7d7813fffcfbf724e20ba0c42fe536a6 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 11 Mar 2020 15:25:41 +0100
Subject: [PATCH] Revert "[WIP] [Eva] Enable descending sequences"
This reverts commit e9c60779e79c220fa924dd67b6b5081983fcf894
---
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, 1 insertion(+), 167 deletions(-)
delete mode 100644 src/plugins/value/partitioning/join_cache.ml
delete mode 100644 src/plugins/value/partitioning/join_cache.mli
diff --git a/Makefile b/Makefile
index 9a30035ad52..d23384d9cc8 100644
--- a/Makefile
+++ b/Makefile
@@ -905,7 +905,6 @@ 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
deleted file mode 100644
index 6b8c9aaa929..00000000000
--- a/src/plugins/value/partitioning/join_cache.ml
+++ /dev/null
@@ -1,95 +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). *)
-(* *)
-(**************************************************************************)
-
-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
deleted file mode 100644
index a1de53720ab..00000000000
--- a/src/plugins/value/partitioning/join_cache.mli
+++ /dev/null
@@ -1,47 +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 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 f1921f3d359..977dce271f2 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -22,24 +22,6 @@
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 = {
@@ -98,17 +80,13 @@ 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.
- 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. *)
+ whereas dynamic splits are reevaluated regularly. *)
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 f0f91e0a50c..aa261fbfb89 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -37,7 +37,6 @@ 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