[wp/region] upgrading region analysis to potassium

headers/header_spec.txt

@@ -1384,6 +1384,8 @@ src/plugins/wp/GuiSource.ml: CEA_WP
 src/plugins/wp/GuiSource.mli: CEA_WP
 src/plugins/wp/GuiTactic.ml: CEA_WP
 src/plugins/wp/GuiTactic.mli: CEA_WP
+src/plugins/wp/Layout.ml: CEA_WP
+src/plugins/wp/Layout.mli: CEA_WP
 src/plugins/wp/Lang.ml: CEA_WP
 src/plugins/wp/Lang.mli: CEA_WP
 src/plugins/wp/Letify.ml: CEA_WP
@@ -1457,6 +1459,14 @@ src/plugins/wp/RefUsage.ml: CEA_WP
 src/plugins/wp/RefUsage.mli: CEA_WP
 src/plugins/wp/Region.ml: CEA_WP
 src/plugins/wp/Region.mli: CEA_WP
+src/plugins/wp/RegionAccess.ml: CEA_WP
+src/plugins/wp/RegionAccess.mli: CEA_WP
+src/plugins/wp/RegionAnalysis.ml: CEA_WP
+src/plugins/wp/RegionAnalysis.mli: CEA_WP
+src/plugins/wp/RegionAnnot.ml: CEA_WP
+src/plugins/wp/RegionAnnot.mli: CEA_WP
+src/plugins/wp/RegionDump.ml: CEA_WP
+src/plugins/wp/RegionDump.mli: CEA_WP
 src/plugins/wp/Repr.ml: CEA_WP
 src/plugins/wp/Repr.mli: CEA_WP
 src/plugins/wp/Sigma.ml: CEA_WP

src/plugins/qed/listmap.ml

@@ -43,6 +43,7 @@ struct
   let equal eq = Hcons.equal_list (fun (i,x) (j,y) -> K.equal i j && eq x y)
 
   let empty = []
+  let is_empty = function [] -> true | _ -> false
 
   (* used for better sharing between a list and a modified list *)
   let rev_append_until i l1 l2 =

src/plugins/qed/listmap.mli

@@ -42,6 +42,8 @@ sig
   val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 
   val empty : 'a t
+  val is_empty : 'a t -> bool
+
   val add : key -> 'a -> 'a t -> 'a t
   val mem : key -> 'a t -> bool
   val find : key -> 'a t -> 'a

src/plugins/qed/listset.ml

@@ -42,6 +42,7 @@ struct
   let equal = Hcons.equal_list E.equal
 
   let empty = []
+  let is_empty = function [] -> true | _ -> false
 
   (* used for better sharing between a list and a modified list *)
   let rev_append_until i l1 l2 =

src/plugins/qed/listset.mli

@@ -41,6 +41,7 @@ sig
   val compare : t -> t -> int
 
   val empty : t
+  val is_empty : t -> bool
 
   (* good sharing *)
   val add : elt -> t -> t

src/plugins/wp/Cint.ml

@@ -244,8 +244,8 @@ let match_power2_extraction = match_list_extraction match_power2
 (* to_iota(e) where e = to_iota'(e'), only ranges for iota *)
 let simplify_range_comp f iota e conv e' =
   let iota' = to_cint conv in
-  let size' = Ctypes.range iota' in
-  let size = Ctypes.range iota in
+  let size' = Ctypes.i_bits iota' in
+  let size = Ctypes.i_bits iota in
   if size <= size'
   then e_fun f [e']
   (* rule B:
@@ -275,7 +275,7 @@ let configure_to_int iota =
     begin
       try match F.repr e with
         | Logic.Kint value ->
-            let size = Integer.of_int (Ctypes.range iota) in
+            let size = Integer.of_int (Ctypes.i_bits iota) in
             let signed = Ctypes.signed iota in
             F.e_zint (Integer.cast ~size ~signed ~value)
         | Logic.Fun( fland , es )
@@ -495,7 +495,7 @@ let smp_bitk_positive = function
             F.e_not (bitk_positive k a)
         | Logic.Fun( conv , [a] ) (* when is_to_c_int conv *) ->
             let iota = to_cint conv in
-            let range = Ctypes.range iota in
+            let range = Ctypes.i_bits iota in
             let signed = Ctypes.signed iota in
             if signed then (* beware of sign-bit *)
               begin match is_leq k (e_int (range-2)) with

src/plugins/wp/Generator.ml

@@ -86,63 +86,42 @@ let compute_ip cc ip =
 (* --- Annotations Entry Point                                            --- *)
 (* -------------------------------------------------------------------------- *)
 
-type functions =
-  | F_All
-  | F_List of Cil_datatype.Kf.Set.t
-  | F_Skip of Cil_datatype.Kf.Set.t
-
-let iter_kf phi = function
-  | None -> Globals.Functions.iter phi
-  | Some kf -> phi kf
-
-let iter_fct phi = function
-  | F_All -> Globals.Functions.iter phi
-  | F_Skip fs ->
-      Globals.Functions.iter
-        (fun kf -> if not (Cil_datatype.Kf.Set.mem kf fs) then phi kf)
-  | F_List fs -> Cil_datatype.Kf.Set.iter phi fs
-
 let add_kf cc ?bhv ?prop kf =
   let model = cc#model in
   let assigns = WpAnnot.WithAssigns in
   List.iter cc#add_strategy
     (WpAnnot.get_function_strategies ~model ~assigns ?bhv ?prop kf)
 
+let add_lemmas cc = function
+  | None | Some[] ->
+      LogicUsage.iter_lemmas
+        (fun lem ->
+           let idp = WpPropId.mk_lemma_id lem in
+           if WpAnnot.filter_status idp then cc#add_lemma lem)
+  | Some ps ->
+      if List.mem "-@lemmas" ps then ()
+      else LogicUsage.iter_lemmas
+          (fun lem ->
+             let idp = WpPropId.mk_lemma_id lem in
+             if WpAnnot.filter_status idp && WpPropId.select_by_name ps idp
+             then cc#add_lemma lem)
+
 let compute_kf cc ?kf ?bhv ?prop () =
   begin
-    iter_kf (add_kf cc ?bhv ?prop) kf ;
+    Extlib.may (add_kf cc ?bhv ?prop) kf ;
     cc#compute
   end
 
-let do_lemmas = function F_All | F_Skip _ -> true | F_List _ -> false
-
-let compute_selection cc ?(fct=F_All) ?bhv ?prop () =
+let compute_selection cc ?(fct=Wp_parameters.Fct_all) ?bhv ?prop () =
   begin
-    if do_lemmas fct then
-      begin
-        match prop with
-        | None | Some[] ->
-            LogicUsage.iter_lemmas
-              (fun lem ->
-                 let idp = WpPropId.mk_lemma_id lem in
-                 if WpAnnot.filter_status idp then cc#add_lemma lem)
-        | Some ps ->
-            if List.mem "-@lemmas" ps then ()
-            else LogicUsage.iter_lemmas
-                (fun lem ->
-                   let idp = WpPropId.mk_lemma_id lem in
-                   if WpAnnot.filter_status idp && WpPropId.select_by_name ps idp
-                   then cc#add_lemma lem)
-      end ;
-    iter_fct (add_kf cc ?bhv ?prop) fct ;
+    add_lemmas cc prop ;
+    Wp_parameters.iter_fct (add_kf cc ?bhv ?prop) fct ;
     cc#compute
   end
 
-(* -------------------------------------------------------------------------- *)
-(* --- Calls Entry Point                                                  --- *)
-(* -------------------------------------------------------------------------- *)
-
 let compute_call cc stmt =
   let model = cc#model in
   List.iter cc#add_strategy (WpAnnot.get_call_pre_strategies ~model stmt) ;
   cc#compute
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/Generator.mli

@@ -33,18 +33,17 @@ class type computer =
     method compute : Wpo.t Bag.t
   end
 
-type functions =
-  | F_All
-  | F_List of Cil_datatype.Kf.Set.t
-  | F_Skip of Cil_datatype.Kf.Set.t
+open Wp_parameters
 
 val compute_ip : computer -> Property.t -> Wpo.t Bag.t
 val compute_call : computer -> Cil_types.stmt -> Wpo.t Bag.t
+
 val compute_kf : computer ->
   ?kf:Kernel_function.t ->
   ?bhv:string list ->
   ?prop:string list ->
   unit -> Wpo.t Bag.t
+
 val compute_selection : computer ->
   ?fct:functions ->
   ?bhv:string list ->

src/plugins/wp/Layout.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2019                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Region Utilities *)
+
+open Pretty_utils
+open Cil_types
+
+module type Data =
+sig
+  type t
+  val equal : t -> t -> bool
+  val compare : t -> t -> int
+  val pretty : t formatter
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 L-Path} *)
+(* -------------------------------------------------------------------------- *)
+
+type offset =
+  | Field of fieldinfo
+  | Index of typ * int
+
+type lvalue = (** Generalized l-values *)
+  | Eval of exp
+  | Tval of term
+  | Assigned of stmt
+
+module Offset :
+sig
+  include Data with type t = offset
+  val index : typ -> offset
+  val field : fieldinfo -> offset
+  val typeof : offset -> typ
+  val typeof_chain : typ -> offset list -> typ
+  val pp_chain : typ -> offset list formatter
+
+  type cache
+  val cache : unit -> cache
+  val field_offset : cache -> fieldinfo -> int * int (* in bits *)
+  val range : cache -> offset -> (int * int) * int (* in bits *)
+  val sizeof : offset -> int (* in bits *)
+end
+
+module Lvalue : Data with type t = lvalue
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Access} *)
+(* -------------------------------------------------------------------------- *)
+
+type alias = NotUsed | NotAliased | Aliased
+type usage = Value | Deref | Array
+type deref = usage * typ
+
+module Alias :
+sig
+  val use : alias -> alias
+  val merge : alias -> alias -> alias
+  val alias : alias -> alias -> alias
+  val is_aliased : alias -> bool
+  val pretty : alias formatter
+end
+
+module Usage :
+sig
+  val pretty : usage formatter
+  val merge : usage -> usage -> usage
+  val is_shifted : usage -> bool
+  val is_aliased : usage -> bool
+end
+
+module Deref : Data with type t = deref
+
+(* -------------------------------------------------------------------------- *)
+(** {2 R-Values} *)
+(* -------------------------------------------------------------------------- *)
+
+type 'a value =
+  | Int of Ctypes.c_int
+  | Float of Ctypes.c_float
+  | Pointer of 'a
+
+module Value :
+sig
+
+  val compare : ('a -> 'a -> int) -> 'a value -> 'a value -> int
+  val equal : ('a -> 'a -> bool) -> 'a value -> 'a value -> bool
+  val pretty : 'a formatter -> 'a value formatter
+
+  val sizeof : 'a value -> int
+  val pointed : 'a value -> 'a option
+
+  val merge : ('a -> 'a -> 'a) -> 'a value -> 'a value -> 'a value option
+
+end
+
+module Matrix :
+sig
+
+  val gcd : int -> int -> int
+  val pretty : int list formatter
+  val sizeof : int -> int list -> int
+  val merge : int list -> int list -> int list
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Overlays} *)
+(* -------------------------------------------------------------------------- *)
+
+type dim = Raw of int | Dim of int * int list
+
+type 'a range = private {
+  ofs : int ; (* in bits, start from 0 *)
+  len : int ;
+  reg : 'a ;
+  dim : dim ;
+}
+
+type 'a overlay = 'a range list
+
+type 'a merger = raw:bool -> 'a -> 'a -> 'a
+
+module Range :
+sig
+
+  val pretty : 'a formatter -> 'a range formatter
+  val overlap : 'a formatter -> 'a merger -> 'a range -> 'a range -> 'a range
+  val included : int -> int -> 'a range -> bool
+
+end
+
+module Overlay :
+sig
+
+  val pretty : ?title:(Format.formatter -> unit) ->
+    'a formatter -> 'a overlay formatter
+  val merge : 'a formatter ->
+    'a merger -> 'a overlay -> 'a overlay -> 'a overlay
+
+  val once : 'a -> 'a overlay -> bool
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Compound Layout} *)
+(* -------------------------------------------------------------------------- *)
+
+type 'a layout = {
+  sizeof : int ;
+  layout : 'a overlay ;
+}
+
+module Compound :
+sig
+
+  val garbled : Offset.cache -> offset -> 'a -> 'a layout
+  val reshape : eq:('a -> 'a -> bool) -> flat:bool -> pack:bool ->
+    'a layout -> 'a layout
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Clustering} *)
+(* -------------------------------------------------------------------------- *)
+
+type 'a cluster =
+  | Empty
+  | Garbled
+  | Chunk of 'a value
+  | Layout of 'a layout
+
+module Cluster :
+sig
+
+  val pretty : 'a formatter -> 'a cluster formatter
+  val deref : pointed:'a Lazy.t -> deref -> 'a cluster
+  val shift : Offset.cache -> 'a formatter ->
+    offset -> 'a -> inline:bool -> 'a cluster -> 'a layout
+  val merge : 'a formatter -> 'a merger -> 'a cluster -> 'a cluster -> 'a cluster
+  val is_empty : 'a cluster -> bool
+  val is_garbled : 'a cluster -> bool
+  val reshape : eq:('a -> 'a -> bool) -> flat:bool -> pack:bool ->
+    'a cluster -> 'a cluster
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Roots} *)
+(* -------------------------------------------------------------------------- *)
+
+type 'a from =
+  | Fvar of varinfo
+  | Ffield of 'a * int
+  | Findex of 'a
+  | Fderef of 'a
+  | Farray of 'a
+
+type root =
+  | Rnone
+  | Rfield of varinfo * int (* static offset *)
+  | Rindex of varinfo (* any offset rooted at var *)
+  | Rtop
+
+module Root :
+sig
+
+  val pretty : root formatter
+  val from : root:('a -> root) -> 'a from -> root
+  val merge : root -> root -> root
+  val indexed : root -> bool
+  val framed : root -> bool
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Chunks} *)
+(* -------------------------------------------------------------------------- *)
+
+type chunks = Qed.Intset.t
+
+type 'a chunk =
+  | Mref of 'a (** Constant pointers to region *)
+  | Mmem of root * 'a value (** Aliased values *)
+  | Mraw of root * 'a option (** Bits that may points-to *)
+  | Mcomp of chunks * 'a overlay (** Aliased chunks & overlay *)
+
+module Chunk :
+sig
+  val empty : chunks
+  val singleton : int -> chunks
+  val union : chunks -> chunks -> chunks
+  val disjoint : chunks -> chunks -> bool
+  val union_map : ('a -> chunks) -> 'a list -> chunks
+  val mem : int -> chunks -> bool
+  val pretty : int formatter -> chunks formatter
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Options} *)
+(* -------------------------------------------------------------------------- *)
+
+(** Read-Write access *)
+module RW :
+sig
+  val default : unit -> bool
+  val merge : bool -> bool -> bool
+end
+
+(** Flatten arrays *)
+module Flat :
+sig
+  val default : unit -> bool
+  val merge : bool -> bool -> bool
+end
+
+(** Pack fields *)
+module Pack :
+sig
+  val default : unit -> bool
+  val merge : bool -> bool -> bool
+end
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/Makefile.in

@@ -67,10 +67,12 @@ PLUGIN_CMO:= \
 	dyncall ctypes clabels \
 	MemoryContext \
 	LogicUsage RefUsage \
+	Layout Region \
+	RegionAnnot RegionAccess RegionDump RegionAnalysis \
 	cil2cfg normAtLabels wpPropId mcfg \
 	Context Warning Model Lang Repr Matrix Passive Splitter \
 	LogicBuiltins Definitions \
-	Cmath Cint Cfloat Vset Vlist Region Cstring Cvalues \
+	Cmath Cint Cfloat Vset Vlist Cstring Cvalues \
 	Letify Cleaning \
 	Sigs Mstate Conditions \
 	Filtering \

src/plugins/wp/Region.mli

@@ -20,43 +20,86 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* -------------------------------------------------------------------------- *)
-(* --- Logic Path and Regions                                             --- *)
-(* -------------------------------------------------------------------------- *)
+open Cil_types
+open Layout
 
-open Lang
-open Lang.F
-open Vset
+type region
+type map
 
-(** {2 Paths} *)
+module R : Layout.Data with type t = region
+module Map : Qed.Idxmap.S with type key = region
+module Set : Qed.Idxset.S with type elt = region
 
-type path = offset list
-and offset =
-  | Oindex of term
-  | Ofield of field
+val create : unit -> map
+val is_empty : map -> bool
+val iter : map -> (region -> unit) -> unit
 
-val access : term -> path -> term
-val update : term -> path -> term -> term
+val id: region -> int
+val noid: int
 
-(** {2 Regions} *)
+val get_addrof : map -> region -> region
+val add_pointed : map -> region -> region
+val add_offset : map -> region -> offset -> region
+val field_offset : map -> fieldinfo -> int * int
 
-type rpath = roffset list
-and roffset =
-  | Rindex of set
-  | Rfield of field
+val get_froms : map -> region -> region from list
+val get_roots : map -> region -> root
+val has_roots : map -> region -> bool
 
-type region
+val is_garbled : region -> bool
+val has_pointed : region -> bool
+val has_layout : region -> bool
+val has_offset : region -> offset -> bool
+val has_copies : region -> bool
+val has_deref : region -> bool
+val has_names : region -> bool
+val has_return : map -> bool
+
+val get_pointed : map -> region -> region option
+val get_offset : map -> region -> offset -> region option
+val get_copies : map -> region -> region list
+val get_alias : map -> region -> region
+val get_merged : map -> region -> region option
+val eq_alias : map -> region -> region -> bool
+
+val acs_read : region -> lvalue -> unit
+val acs_write : region -> lvalue -> unit
+val acs_shift : region -> lvalue -> unit
+val acs_deref : region -> deref -> unit
+val acs_copy : src:region -> tgt:region -> unit
+
+val is_read : region -> bool
+val is_written : region -> bool
+val is_shifted : region -> bool
+val is_aliased : region -> bool
+
+val iter_read : (lvalue -> unit) -> region -> unit
+val iter_write : (lvalue -> unit) -> region -> unit
+val iter_shift : (lvalue -> unit) -> region -> unit
+val iter_deref : (deref -> unit) -> region -> unit
+val iter_offset : map -> (offset -> region -> unit) -> region -> unit
+val iter_copies : map -> (region -> unit) -> region -> unit
+val iter_vars : map -> (varinfo -> region -> unit) -> unit
+val iter_names : map -> (string -> region -> unit) -> unit
+val iter_strings : map -> (region -> string -> unit) -> unit
+
+val of_null : map -> region
+val of_return : map -> region
+val of_cvar : map -> varinfo -> region
+val of_cstring : map -> eid:int -> cst:string -> region
+val of_name : map -> string -> region
+val of_class : map -> string option -> region
 
-val empty : region
-val full : region
-val path : path -> region (** Empty, but Full for the path *)
-val rpath : rpath -> region (** Empty, but Full for the r-paths *)
-val merge : region -> region -> region
+val region : map -> int -> region
+val cluster : map -> region -> region cluster
+val chunk : map -> region -> region chunk
+val chunks : map -> region -> chunks
 
-val disjoint : region -> region -> pred