[WIP] [Eva] Enable descending sequences

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 \

src/plugins/value/partitioning/join_cache.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/value/partitioning/join_cache.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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

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 =

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