diff --git a/ivette/src/dome/renderer/graph/diagram.tsx b/ivette/src/dome/renderer/graph/diagram.tsx
index d594f647ca21f1aa19bdea0b29be528c7f48262b..5764a97e7313d3a15cc929d6405e1d16c253f900 100644
--- a/ivette/src/dome/renderer/graph/diagram.tsx
+++ b/ivette/src/dome/renderer/graph/diagram.tsx
@@ -349,7 +349,7 @@ class Builder {
// --- Edge
edge(e: Edge): void {
const { line = 'solid', head = 'arrow', tail = 'none' } = e;
- const tooltip = e.title ?? e.label ?? `${e.source} -> ${e.target}`;
+ const tooltip = e.title ?? e.label;
if (e.aligned === true)
this
.print('{ rank=same; ')
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
index 2b38fe1acbe532113a27f458bb0a43fe2a30c023..e04a8e56bf3380f062b9c63dd04b982b406fd7e4 100644
--- a/ivette/src/frama-c/plugins/region/memory.tsx
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -54,7 +54,7 @@ function makeRecord(
cells.push({ label, port });
});
if (offset !== sizeof)
- cells.push(`#${sizeof-offset}b`);
+ cells.push(`#${sizeof - offset}b`);
return cells;
}
@@ -70,30 +70,29 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
const id = `n${r.node}`;
// --- Color
const color =
- r.bytes ? 'red' :
- r.pointed !== undefined
- ? (r.writes ? 'orange' : 'yellow')
- : (r.writes && r.reads) ? 'green' :
- r.writes ? 'pink' : r.reads ? 'grey' : 'white';
+ (!r.writes && !r.reads) ? undefined :
+ !r.typed ? 'red' :
+ r.pointed !== undefined
+ ? (r.writes ? 'orange' : 'yellow')
+ : (r.writes && r.reads) ? 'green' :
+ r.writes ? 'pink' : 'grey';
// --- Shape
const font = r.ranges.length > 0 ? 'mono' : 'sans';
const cells = makeRecord(edges, id, r.sizeof, r.ranges);
const shape = cells.length > 0 ? cells : undefined;
nodes.push({ id, font, color, label: r.label, title: r.title, shape });
// --- Labels
- const L: Dot.Node =
- { id: '', shape: 'note', font: 'mono' };
+ const L: Dot.Node = { id: '', shape: 'note', font: 'mono' };
r.labels.forEach(a => {
const lid = `L${a}`;
nodes.push({ ...L, id: lid, label: `${a}:` });
edges.push({
source: lid, target: id, aligned: true,
- headAnchor: 'n', head: 'none', color: 'grey'
+ headAnchor: 's', head: 'none', color: 'grey'
});
});
// --- Roots
- const R: Dot.Node =
- { id: '', shape: 'cds', font: 'mono' };
+ const R: Dot.Node = { id: '', shape: 'cds', font: 'mono' };
r.roots.forEach(x => {
const xid = `X${x}`;
nodes.push({ ...R, id: xid, label: x });
diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index c440b8e4965381bed61e9c1ad95cd270d5780593..7a88530125422d7b9bd618f1e9c4b2b762d4442d 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -24,10 +24,31 @@
(* --- Region Analysis API --- *)
(* -------------------------------------------------------------------------- *)
-let get_map kf = (Code.domain kf).map
-let get_id m n = Memory.id @@ Memory.node m n
-let get_node m id = Memory.node m @@ Memory.forge id
-
-include Memory
-
-let iter = Memory.iter_node
+type map = Memory.map
+type node = Memory.node
+let map kf = (Analysis.get kf).map
+let id n = Memory.id n
+let uid m n = Memory.id @@ Memory.node m n
+let iter = Memory.iter
+let find m id = Memory.node m @@ Memory.forge id
+let node = Memory.node
+let nodes = Memory.nodes
+let equal = Memory.equal
+let included = Memory.included
+let separated = Memory.separated
+let singleton = Memory.singleton
+let size = Memory.size
+let roots = Memory.roots
+let labels = Memory.labels
+let reads = Memory.reads
+let writes = Memory.writes
+let shifts = Memory.shifts
+let typed = Memory.typed
+let parents m n = Memory.nodes m @@ Memory.parents m n
+let points_to m n = Option.map (Memory.node m) @@ Memory.points_to m n
+let pointed_by m n = Memory.nodes m @@ Memory.pointed_by m n
+let lval m l = Memory.node m @@ Memory.lval m l
+let exp m e = Option.map (Memory.node m) @@ Memory.exp m e
+let cvar = Memory.cvar
+let field = Memory.field
+let index = Memory.index
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index 68c04c93ee0a56e85db49f7521231c011df0da71..46e3997e0d8e2c8d3e72a5c19dcfbfafa1c6fb85 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-(** Interface for the Region plug-in.
+(** {1 Interface for the Region plug-in}
Each function is assigned a region map. Areas in the map represents l-values
or, more generally, class of nodes. Regions are classes equivalences of
@@ -29,7 +29,7 @@
Regions can be subdivided into sub-regions. Hence, given two regions, either
one is included into the other, or they are separated. Hence, given two
l-values, if their associated regions are separated, then they can {i not}
- be aliased.
+ be aliased.
Nodes are elementary elements of a region map. Variables maps to nodes, and
one can move to one node to another by struct or union field or array
@@ -38,44 +38,101 @@
a region.
*)
-
open Cil_types
+(** {2 Memory Maps and Nodes} *)
+
type map
type node
-val get_map : kernel_function -> map
-val get_id : map -> node -> int
-val get_node : map -> int -> node
+val map : kernel_function -> map
+
+(** Not normalized.
+ Two nodes in the same equivalence class may have different identifiers. *)
+val id : node -> int
+
+(** Unique id of normalized node.
+ This can be considered the unique identifier of the region equivalence
+ class. *)
+val uid : map -> node -> int
+
+(** Returns a normalized node.
+ @raises Not_found if not a valid node identifier. *)
+val find : map -> int -> node
-(** Normalize node *)
+(** Normalized node.
+ The returned node is the representative of the region equivalence class.
+ There is one unique representative per equivalence class. *)
val node : map -> node -> node
-(** Normalize set of nodes *)
+(** Normalized list of nodes (normalized, uniques, sorted by id) *)
val nodes : map -> node list -> node list
-(** Nodes are in the same region *)
+(** {2 Region Properties}
+
+ All functions in this section provide normalized nodes
+ and shall never raise exception. *)
+
+val points_to : map -> node -> node option
+val pointed_by : map -> node -> node list
+
+val size : map -> node -> int
+val parents : map -> node -> node list
+val roots : map -> node -> varinfo list
+val labels: map -> node -> string list
+val reads : map -> node -> typ list
+val writes : map -> node -> typ list
+val shifts : map -> node -> typ list
+
+val typed : map -> node -> typ option
+(** Full-sized cells with unique type access *)
+
+val iter : map -> (node -> unit) -> unit
+
+(** {2 Alias Analysis} *)
+
+(** [equal m a b] checks if nodes [a] and [b] are in the same region. *)
val equal : map -> node -> node -> bool
-(** First belongs to last *)
+(** [include m a b] checks if region [a] is a sub-region of [b] in map [m]. *)
val included : map -> node -> node -> bool
-(** Nodes can not be aliased *)
+(** [separated m a b] checks if region [a] and region [b] are disjoint.
+ Disjoints regions [a] and [b] have the following properties:
+ - [a] is {i not} a sub-region of [b];
+ - [b] is {i not} a sub-region of [a];
+ - two l-values respectively localized in [a] and [b]
+ can {i never} be aliased.
+*)
val separated : map -> node -> node -> bool
-val cvar : map -> varinfo -> node
-val field : map -> node -> fieldinfo -> node
-val index : map -> node -> typ -> node
+(** [singleton m a] returns [true] when node [a] is guaranteed to have only
+ one single address in its equivalence class. *)
+val singleton : map -> node -> bool
+
+(** [lval m lv] is region where the address of [l] lives in.
+ The returned region is normalized.
+ @raises Not_found if the l-value is not localized in the map *)
val lval : map -> lval -> node
+
+(** [exp m e] is the domain of values that can computed by expression [e].
+ The domain is [Some r] is [e] has a pointer type and any pointer computed by
+ [e] lives in region [r]. The domain is [None] if [e] has a non-pointer
+ scalar or compound type.
+ @raises Not_found if the l-value is not localized in the map
+*)
val exp : map -> exp -> node option
-val points_to : map -> node -> node option
-val pointed_by : map -> node -> node list
-val parents : map -> node -> node list
-val roots : map -> node -> varinfo list
+(** {2 Low-level Navigation through Memory Maps}
-val iter : map -> (node -> unit) -> unit (** Iter over all regions *)
+ For optimized access, all the fonctions in this section return
+ unnormalized nodes and may raise [Not_found] for not localized routes. *)
-val reads : map -> node -> typ list
-val writes : map -> node -> typ list
-val shifts : map -> node -> typ list
+(** Unormalized. @raises Not_found *)
+val cvar : map -> varinfo -> node
+
+(** Unormalized. @raises Not_found *)
+val field : map -> node -> fieldinfo -> node
+
+(** Unormalized. @raises Not_found *)
+val index : map -> node -> typ -> node
diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
index b64c6571bc83fbfa648159d1701a12bf6e597a33..8fd275216e39e9ae08e3a0db8463fb1056fbf4e6 100644
--- a/src/plugins/region/analysis.ml
+++ b/src/plugins/region/analysis.ml
@@ -56,15 +56,6 @@ let get kf =
Options.feedback ~ontty:`Transient "Function %a…" Kernel_function.pretty kf ;
let domain = Code.domain kf in
STATE.add kf domain ;
- Options.result "@[<v 2>Function %a:%t@]@."
- Kernel_function.pretty kf
- begin fun fmt ->
- Memory.iter domain.map
- begin fun r ->
- Format.pp_print_newline fmt () ;
- Memory.pp_region fmt r ;
- end
- end ;
domain
let compute kf = ignore @@ get kf
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index 858b1a02cda82c4aa449c73ace700e7289e2da88..478264d7ca534fdce3033c5e537688096de89dcc 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -51,9 +51,8 @@ and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
| Field(fd,ofs) ->
add_loffset m s (add_field m r fd) fd.ftype ofs
| Index(_,ofs) ->
- let elt,size = Cil.typeOf_array_elem_size ty in
- let n = Z.to_int @@ Option.get size in
- add_loffset m s (add_index m r elt n) elt ofs
+ let elt = Cil.typeOf_array_elem ty in
+ add_loffset m s (add_index m r elt) elt ofs
and add_value m s e = ignore (add_exp m s e)
@@ -66,14 +65,14 @@ and add_exp (m: map) (s:stmt) (e:exp) : scalar =
| Lval lv ->
let rv = add_lval m s lv in
- Memory.read m rv (Lval(s,lv)) ;
+ Memory.add_read m rv (Lval(s,lv)) ;
let ptr = Memory.add_value m rv @@ Cil.typeOfLval lv in
{ from = Some rv ; ptr }
| BinOp((PlusPI|MinusPI),p,k,_) ->
add_value m s k ;
let v = add_exp m s p in
- Option.iter (fun r -> Memory.shift m r (Exp(s,e))) v.from ; v
+ Option.iter (fun r -> Memory.add_shift m r (Exp(s,e))) v.from ; v
| UnOp(_,e,_) ->
add_value m s e ; integral
@@ -102,7 +101,7 @@ let rec add_init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
| SingleInit e ->
let r = add_lval m s lv in
- Memory.write m r acs ;
+ Memory.add_write m r acs ;
Option.iter (Memory.add_points_to m r) (add_exp m s e).ptr
| CompoundInit(_,fvs) ->
@@ -123,14 +122,14 @@ let add_instr (m:map) (s:stmt) (instr:instr) =
| Set(lv, { enode = Lval exp }, _) ->
let l = add_lval m s lv in
let r = add_lval m s exp in
- Memory.read m r (Lval(s,exp)) ;
- Memory.write m l (Lval(s,lv)) ;
+ Memory.add_read m r (Lval(s,exp)) ;
+ Memory.add_write m l (Lval(s,lv)) ;
Memory.merge_copy m ~l ~r
| Set(lv,e,_) ->
let r = add_lval m s lv in
let v = add_exp m s e in
- Memory.write m r (Lval(s,lv)) ;
+ Memory.add_write m r (Lval(s,lv)) ;
Option.iter (Memory.add_points_to m r) v.ptr
| Local_init(x,AssignInit iv,_) ->
@@ -143,7 +142,7 @@ let add_instr (m:map) (s:stmt) (instr:instr) =
Option.iter
(fun lv ->
let r = add_lval m s lv in
- Memory.write m r (Lval(s,lv))
+ Memory.add_write m r (Lval(s,lv))
) lr ;
Options.warning ~source:(fst @@ Stmt.loc s) "Incomplete call analysis"
diff --git a/src/plugins/region/logic.ml b/src/plugins/region/logic.ml
index df43142c587fe4fae7664f149f2545712005c2b0..8c79655d0306b0987692e4d4426f4564caf97d0d 100644
--- a/src/plugins/region/logic.ml
+++ b/src/plugins/region/logic.ml
@@ -27,7 +27,7 @@ let rec add_lval (m:map) (p:path): node =
match p.step with
| Var x -> add_root m x
| Field(lv,fd) -> Memory.add_field m (add_lval m lv) fd
- | Index(lv,n) -> Memory.add_index m (add_lval m lv) lv.typ n
+ | Index(lv,_) -> Memory.add_index m (add_lval m lv) lv.typ
| Star e | Cast(_,e) -> add_pointer m e
| Shift _ | AddrOf _ ->
Options.error ~source:(fst p.loc)
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 2e500375c1477b1120217c34329a90e3a89e4960..df25c23811dbaa1f276f571d3571172fefdb3c06 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -40,6 +40,7 @@ and layout =
| Blob
| Cell of int * node option
| Compound of int * Fields.domain * node Ranges.t
+ (* must only contain strict sub-ranges *)
and chunk = {
cparents: node list ;
@@ -66,11 +67,11 @@ type map = {
(* -------------------------------------------------------------------------- *)
let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_,_) -> s
-let ranges = function Blob | Cell _ -> [] | Compound(_,_,R rs) -> rs
-let fields = function Blob | Cell _ -> Fields.empty | Compound(_,fds,_) -> fds
-let pointed = function Blob | Compound _ -> None | Cell(_,p) -> p
+let cranges = function Blob | Cell _ -> [] | Compound(_,_,R rs) -> rs
+let cfields = function Blob | Cell _ -> Fields.empty | Compound(_,fds,_) -> fds
+let cpointed = function Blob | Compound _ -> None | Cell(_,p) -> p
-let types (m : chunk) : typ list =
+let ctypes (m : chunk) : typ list =
let pool = ref Typ.Set.empty in
let add acs =
pool := Typ.Set.add (Cil.unrollType @@ Access.typeof acs) !pool in
@@ -79,7 +80,7 @@ let types (m : chunk) : typ list =
Typ.Set.elements !pool
let failwith_locked m fn =
- if m.locked then raise (Invalid_argument fn)
+ if m.locked then raise (Invalid_argument (fn ^ ": locked"))
let lock m = m.locked <- true
let unlock m = m.locked <- false
@@ -111,7 +112,7 @@ let pp_chunk fmt (n: node) (m: chunk) =
let acs r s = if Access.Set.is_empty s then '-' else r in
Format.fprintf fmt "@[<hov 2>%a: %c%c%c" pp_node n
(acs 'R' m.creads) (acs 'W' m.cwrites) (acs 'A' m.cshifts) ;
- List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (types m) ;
+ List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (ctypes m) ;
Lset.iter (Format.fprintf fmt "@ %s:") m.clabels ;
Vset.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.croots ;
if Options.debug_atleast 1 then
@@ -179,29 +180,17 @@ let update (m: map) (n: node) (f: chunk -> chunk) =
(* --- Chunk Constructors --- *)
(* -------------------------------------------------------------------------- *)
-let new_chunk (m: map) ?(size=0) ?ptr ?pointed () =
+let new_chunk (m: map) ?parent ?(size=0) ?ptr ?pointed () =
failwith_locked m "Region.Memory.new_chunk" ;
let clayout =
match ptr with
| None -> if size = 0 then Blob else Cell(size,None)
- | Some _ -> Cell(Ranges.gcd size (Cil.bitsSizeOf Cil_const.voidPtrType), ptr)
+ | Some _ ->
+ Cell(Ranges.gcd size (Cil.bitsSizeOf Cil_const.voidPtrType), ptr)
in
- let cpointed =
- match pointed with
- | None -> []
- | Some ptr -> [ptr]
- in
- Ufind.make m.store { empty with clayout ; cpointed }
-
-let new_range (m: map) ?(fields=Fields.empty) ~size ~offset ~length data : node =
- failwith_locked m "Region.Memory.new_range" ;
- let last = offset + length in
- if not (0 <= offset && offset < last && last <= size) then
- raise (Invalid_argument "Region.Memory.add_range") ;
- let ranges = Ranges.singleton { offset ; length ; data } in
- let clayout = Compound(size, fields, ranges) in
- let n = Ufind.make m.store { empty with clayout } in
- update m data (fun r -> { r with cparents = nodes m @@ n :: r.cparents }) ; n
+ let cparents = match parent with None -> [] | Some root -> [root] in
+ let cpointed = match pointed with None -> [] | Some ptr -> [ptr] in
+ Ufind.make m.store { empty with clayout ; cpointed ; cparents }
let add_root (m: map) v =
try Vmap.find v m.roots with Not_found ->
@@ -221,173 +210,49 @@ let add_label (m: map) a =
(* --- Iterator --- *)
(* -------------------------------------------------------------------------- *)
-type range = {
- label: string ; (* pretty printed fields *)
- offset: int ;
- length: int ;
- cells: int ;
- data: node ;
-}
-
-type region = {
- node: node ;
- parents: node list ;
- roots: varinfo list ;
- labels: string list ;
- types: typ list ;
- fields: Fields.domain ;
- reads: Access.acs list ;
- writes: Access.acs list ;
- shifts: Access.acs list ;
- sizeof: int ;
- ranges: range list ;
- pointed: node option ;
-}
-
-let pp_cells fmt = function
- | 1 -> ()
- | 0 -> Format.fprintf fmt "[…]"
- | n -> Format.fprintf fmt "[%d]" n
-
-type slice =
- | Padding of int
- | Range of range
-
-let pad p q s =
- let n = q - p in
- if n > 0 then Padding n :: s else s
-
-let rec span k s = function
- | [] -> pad k s []
- | r::rs -> pad k r.offset @@ Range r :: span (r.offset + r.length) s rs
-
-let pp_slice fields fmt = function
- | Padding n ->
- Format.fprintf fmt "@ %a;" Fields.pp_bits n
- | Range r ->
- Format.fprintf fmt "@ %t: %a%a;"
- (Fields.pslice ~fields ~offset:r.offset ~length:r.length)
- pp_node r.data
- pp_cells r.cells
-
-let pp_range fmt (r: range) =
- Format.fprintf fmt "@ %d..%d: %a%a;"
- r.offset (r.offset + r.length) pp_node r.data pp_cells r.cells
-
-let pp_region fmt (m: region) =
- begin
- let acs r s = if s = [] then '-' else r in
- Format.fprintf fmt "@[<hov 2>%a: %c%c%c"
- pp_node m.node
- (acs 'R' m.reads) (acs 'W' m.writes) (acs 'A' m.shifts) ;
- List.iter (Format.fprintf fmt "@ %s:") m.labels ;
- List.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.roots ;
- List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) m.types ;
- Format.fprintf fmt "@ %db" m.sizeof ;
- Option.iter (Format.fprintf fmt "@ (*%a)" pp_node) m.pointed ;
- if m.ranges <> [] then
- begin
- Format.fprintf fmt "@ @[<hv 0>@[<hv 2>{" ;
- if Options.debug_atleast 1 then
- List.iter (pp_range fmt) m.ranges
- else
- List.iter (pp_slice m.fields fmt) (span 0 m.sizeof m.ranges) ;
- Format.fprintf fmt "@]@ }@]" ;
- end ;
- if Options.debug_atleast 1 then
- begin
- List.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.reads ;
- List.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.writes ;
- List.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.shifts ;
- end ;
- Format.fprintf fmt " ;@]" ;
- end
-
-let make_range (m: map) fields Ranges.{ length ; offset ; data } : range =
- let s = sizeof (get m data).clayout in
- let p = Fields.pslice ~fields ~offset ~length in
- {
- label = Format.asprintf "%t" p ;
- offset ; length ;
- cells = if s = 0 then 0 else length / s ;
- data = node m data ;
- }
-
-let make_region (m: map) (n: node) (r: chunk) : region =
- let fields = fields r.clayout in
- {
- node = n ;
- parents = nodes m r.cparents ;
- roots = Vset.elements r.croots ;
- labels = Lset.elements r.clabels ;
- reads = Access.Set.elements r.creads ;
- writes = Access.Set.elements r.cwrites ;
- shifts = Access.Set.elements r.cshifts ;
- types = types r ;
- sizeof = sizeof r.clayout ;
- fields ; ranges = List.map (make_range m fields) @@ ranges r.clayout ;
- pointed = Option.map (node m) (pointed r.clayout) ;
- }
-
-let region map n = make_region map n (get map n)
-
-let rec walk h m f n =
+let rec walk h m (f: node -> unit) n =
let n = Ufind.find m.store n in
let id = Store.id n in
try Hashtbl.find h id with Not_found ->
Hashtbl.add h id () ;
+ f n ;
let r = Ufind.get m.store n in
- f (make_region m n r) ;
match r.clayout with
| Blob -> ()
| Cell(_,p) -> Option.iter (walk h m f) p
| Compound(_,_,rg) -> Ranges.iter (walk h m f) rg
-let iter (m:map) (f: region -> unit) =
+let iter (m:map) (f: node -> unit) =
let h = Hashtbl.create 0 in
Vmap.iter (fun _x n -> walk h m f n) m.roots
-let rec walk_node h m (f: node -> unit) n =
- let n = Ufind.find m.store n in
- let id = Store.id n in
- try Hashtbl.find h id with Not_found ->
- Hashtbl.add h id () ;
- f n ;
- let r = Ufind.get m.store n in
- match r.clayout with
- | Blob -> ()
- | Cell(_,p) -> Option.iter (walk_node h m f) p
- | Compound(_,_,rg) -> Ranges.iter (walk_node h m f) rg
-
-let iter_node (m:map) (f: node -> unit) =
- let h = Hashtbl.create 0 in
- Vmap.iter (fun _x n -> walk_node h m f n) m.roots
-
-let regions map =
- let pool = ref [] in
- iter map (fun r -> pool := r :: !pool) ;
- List.rev !pool
-
+let size (m: map) (r: node) =
+ sizeof (Ufind.get m.store r).clayout
let parents (m: map) (r: node) =
- let chunk = Ufind.get m.store r in
- nodes m chunk.cparents
+ nodes m (Ufind.get m.store r).cparents
let roots (m: map) (r: node) =
- let chunk = Ufind.get m.store r in Vset.elements chunk.croots
+ Vset.elements (Ufind.get m.store r).croots
+
+let labels (m: map) (r: node) =
+ Lset.elements (Ufind.get m.store r).clabels
(* -------------------------------------------------------------------------- *)
(* --- Merge --- *)
(* -------------------------------------------------------------------------- *)
type queue = (node * node) Queue.t
+type cell = { mutable size : int ; mutable ptr : node option }
+let new_cell ?(size=0) ?ptr () = { size ; ptr }
+let cell_layout { size ; ptr } =
+ if size = 0 && ptr = None then Blob else Cell(size,ptr)
-let singleton ~size = function
- | None -> Ranges.empty
- | Some r -> Ranges.range ~length:size r
+let merge_push (m: map) (q: queue) (a: node) (b: node) : unit =
+ if not @@ Ufind.eq m.store a b then Queue.push (a,b) q
let merge_node (m: map) (q: queue) (a: node) (b: node) : node =
- if not @@ Ufind.eq m.store a b then Queue.push (a,b) q ;
+ merge_push m q a b ;
Ufind.find m.store (min a b)
let merge_opt (m: map) (q: queue)
@@ -396,6 +261,16 @@ let merge_opt (m: map) (q: queue)
| None, p | p, None -> p
| Some pa, Some pb -> Some (merge_node m q pa pb)
+let merge_cell (m:map) (q:queue) cell root r =
+ let node = Ufind.get m.store r in
+ let s = sizeof node.clayout in
+ let p = cpointed node.clayout in
+ begin
+ merge_push m q root r ;
+ cell.size <- Ranges.gcd cell.size s ;
+ cell.ptr <- merge_opt m q cell.ptr p ;
+ end
+
let merge_range (m: map) (q: queue) (ra : rg) (rb : rg) : node =
let na = ra.data in
let nb = rb.data in
@@ -410,41 +285,42 @@ let merge_range (m: map) (q: queue) (ra : rg) (rb : rg) : node =
if size = sa && size = sb then data else
merge_node m q (new_chunk m ~size ()) data
-let merge_ranges (m: map) (q: queue)
+let merge_ranges (m: map) (q: queue) (root: node)
(sa : int) (fa : Fields.domain) (wa : node Ranges.t)
(sb : int) (fb : Fields.domain) (wb : node Ranges.t)
: layout =
- let fields = Fields.union fa fb in
if sa = sb then
- Compound(sa, fields, Ranges.merge (merge_range m q) wa wb)
+ match Ranges.merge (merge_range m q) wa wb with
+ | R [{ offset = 0 ; length ; data }] when length = sa ->
+ merge_push m q root data ; Cell(sa,None)
+ | ranges ->
+ let fields = Fields.union fa fb in
+ Compound(sa, fields, ranges)
else
let size = Ranges.gcd sa sb in
- let ra = Ranges.squash (merge_node m q) wa in
- let rb = Ranges.squash (merge_node m q) wb in
- Compound(size, fields, singleton ~size @@ merge_opt m q ra rb)
+ let cell = new_cell ~size () in
+ Ranges.iter (merge_cell m q cell root) wa ;
+ Ranges.iter (merge_cell m q cell root) wb ;
+ cell_layout cell
-let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout =
+let merge_layout (m:map) (q:queue) (root:node) (a:layout) (b:layout) : layout =
match a, b with
| Blob, c | c, Blob -> c
| Cell(sa,pa) , Cell(sb,pb) -> Cell(Ranges.gcd sa sb, merge_opt m q pa pb)
| Compound(sa,fa,wa), Compound(sb,fb,wb) ->
- merge_ranges m q sa fa wa sb fb wb
+ merge_ranges m q root sa fa wa sb fb wb
- | Compound(sr,fr,wr), Cell(sx,None)
- | Cell(sx,None), Compound(sr,fr,wr) ->
+ | Compound(sr,_,wr), Cell(sx,ptr)
+ | Cell(sx,ptr), Compound(sr,_,wr) ->
let size = Ranges.gcd sx sr in
- Compound(size, fr, singleton ~size @@ Ranges.squash (merge_node m q) wr)
-
- | Compound(sr,fr,wr), Cell(sx,Some ptr)
- | Cell(sx,Some ptr), Compound(sr,fr,wr) ->
- let rp = new_chunk m ~size:sx ~ptr () in
- let fx = Fields.empty in
- let wx = Ranges.range ~length:sx rp in
- merge_ranges m q sx fx wx sr fr wr
+ let cell = new_cell ~size ?ptr () in
+ Ranges.iter (merge_cell m q cell root) wr ;
+ cell_layout cell
-let merge_region (m: map) (q: queue) (a : chunk) (b : chunk) : chunk = {
+let merge_chunk (m: map) (q:queue) (root:node)
+ (a : chunk) (b : chunk) : chunk = {
cparents = nodes m @@ Store.bag a.cparents b.cparents ;
cpointed = nodes m @@ Store.bag a.cpointed b.cpointed ;
clabels = Lset.union a.clabels b.clabels ;
@@ -452,16 +328,16 @@ let merge_region (m: map) (q: queue) (a : chunk) (b : chunk) : chunk = {
creads = Access.Set.union a.creads b.creads ;
cwrites = Access.Set.union a.cwrites b.cwrites ;
cshifts = Access.Set.union a.cshifts b.cshifts ;
- clayout = merge_layout m q a.clayout b.clayout ;
+ clayout = merge_layout m q root a.clayout b.clayout ;
}
let do_merge (m: map) (q: queue) (a: node) (b: node): unit =
begin
- let ra = Ufind.get m.store a in
- let rb = Ufind.get m.store b in
- let rx = Ufind.union m.store a b in
- let rc = merge_region m q ra rb in
- Ufind.set m.store rx rc ;
+ let ca = Ufind.get m.store a in
+ let cb = Ufind.get m.store b in
+ let rt = Ufind.union m.store a b in
+ let ck = merge_chunk m q rt ca cb in
+ Ufind.set m.store rt ck ;
end
let merge_all (m:map) = function
@@ -488,26 +364,27 @@ let merge_copy (m: map) ~(l: node) ~(r: node) : unit =
let add_field (m:map) (r:node) (fd:fieldinfo) : node =
let ci = fd.fcomp in
- if ci.cstruct then
+ if not ci.cstruct then r else
let size = Cil.bitsSizeOf (TComp(ci,[])) in
let offset, length = Cil.fieldBitsOffset fd in
- let rf = new_chunk m () in
- let fields = Fields.singleton fd in
- let rc = new_range m ~fields ~size ~offset ~length rf in
- ignore @@ merge m r rc ; rf
- else r
-
-let add_index (m:map) (r:node) (ty:typ) (n:int) : node =
- let s = Cil.bitsSizeOf ty * n in
- let re = new_chunk m () in
- let rc = new_range m ~size:s ~offset:0 ~length:s re in
- ignore @@ merge m r rc ; re
+ if offset = 0 && size = length then r else
+ let data = new_chunk m ~parent:r () in
+ let ranges = Ranges.singleton { offset ; length ; data } in
+ let fields = Fields.singleton fd in
+ let clayout = Compound(size,fields,ranges) in
+ let nc = Ufind.make m.store { empty with clayout } in
+ merge m r nc ; data
+
+let add_index (m:map) (r:node) (ty:typ) : node =
+ let size = Cil.bitsSizeOf ty in
+ let re = new_chunk m ~size () in
+ merge m r re ; re
let add_points_to (m: map) (a: node) (b : node) =
begin
failwith_locked m "Region.Memory.points_to" ;
- ignore @@ merge m a @@ new_chunk m ~ptr:b () ;
- ignore @@ merge m b @@ new_chunk m ~pointed:a () ;
+ merge m a @@ new_chunk m ~ptr:b () ;
+ merge m b @@ new_chunk m ~pointed:a () ;
end
let add_value (m:map) (rv:node) (ty:typ) : node option =
@@ -515,7 +392,7 @@ let add_value (m:map) (rv:node) (ty:typ) : node option =
begin
failwith_locked m "Region.Memory.add_value" ;
let rp = new_chunk m ~pointed:rv () in
- ignore @@ merge m rv @@ new_chunk m ~ptr:rp () ;
+ merge m rv @@ new_chunk m ~ptr:rp () ;
Some rp
end
else
@@ -530,23 +407,23 @@ let sized (m:map) (a:node) (ty: typ) =
let size = Ranges.gcd sr (Cil.bitsSizeOf ty) in
if sr <> size then ignore (merge m a (new_chunk m ~size ()))
-let read (m: map) (a: node) from =
+let add_read (m: map) (a: node) acs =
failwith_locked m "Region.Memory.read" ;
let r = get m a in
- Ufind.set m.store a { r with creads = Access.Set.add from r.creads } ;
- sized m a (Access.typeof from)
+ Ufind.set m.store a { r with creads = Access.Set.add acs r.creads } ;
+ sized m a (Access.typeof acs)
-let write (m: map) (a: node) from =
+let add_write (m: map) (a: node) acs =
failwith_locked m "Region.Memory.write" ;
let r = get m a in
- Ufind.set m.store a { r with cwrites = Access.Set.add from r.cwrites } ;
- sized m a (Access.typeof from)
+ Ufind.set m.store a { r with cwrites = Access.Set.add acs r.cwrites } ;
+ sized m a (Access.typeof acs)
-let shift (m: map) (a: node) from =
+let add_shift (m: map) (a: node) acs =
failwith_locked m "Region.Memory.shift" ;
let r = get m a in
- Ufind.set m.store a { r with cshifts = Access.Set.add from r.cshifts } ;
- sized m a (Access.typeof from)
+ Ufind.set m.store a { r with cshifts = Access.Set.add acs r.cshifts } ;
+ sized m a (Access.typeof acs)
(* -------------------------------------------------------------------------- *)
(* --- Lookup ---- *)
@@ -574,9 +451,11 @@ let rec move (m: map) (r: node) (p: int) (s: int) =
move m rg.data (p - rg.offset) s
let field (m: map) (r: node) (fd: fieldinfo) : node =
- let s = Cil.bitsSizeOf fd.ftype in
- let (p,_) = Cil.fieldBitsOffset fd in
- move m r p s
+ if fd.fcomp.cstruct then
+ let s = Cil.bitsSizeOf fd.ftype in
+ let (p,_) = Cil.fieldBitsOffset fd in
+ move m r p s
+ else r
let index (m : map) (r: node) (ty:typ) : node =
move m r 0 (Cil.bitsSizeOf ty)
@@ -641,16 +520,190 @@ let included map source target : bool =
let separated map r1 r2 =
not (included map r1 r2) && not (included map r2 r1)
+let single_path m r0 r s =
+ match (Ufind.get m.store r0).clayout with
+ | Blob -> true
+ | Cell(s0,_) -> s = s0
+ | Compound(_,_,R rgs) ->
+ List.for_all
+ (fun (rg : node Ranges.range) ->
+ not (Ufind.eq m.store r rg.data) || rg.length = s
+ ) rgs
+
+let rec singleton m r =
+ let node = Ufind.get m.store r in
+ (* normalized parents *)
+ match nodes m node.cparents with
+ | [] -> Vset.cardinal node.croots = 1
+ | [r0] ->
+ Vset.is_empty node.croots &&
+ single_path m r0 r (sizeof node.clayout) &&
+ singleton m r0
+ | _ -> false
+
(* -------------------------------------------------------------------------- *)
-let reads (m : map) (r:node) =
+let reads (m:map) (r:node) =
let node = Ufind.get m.store r in
List.map Access.typeof @@ Access.Set.elements node.creads
-let writes (m : map) (r:node) =
+let writes (m:map) (r:node) =
let node = Ufind.get m.store r in
List.map Access.typeof @@ Access.Set.elements node.cwrites
-let shifts (m : map) (r:node) =
+let shifts (m:map) (r:node) =
let node = Ufind.get m.store r in
List.map Access.typeof @@ Access.Set.elements node.cshifts
+
+let types (m:map) (r:node) = ctypes @@ Ufind.get m.store r
+
+let typed (m:map) (r:node) =
+ let types = ref None in
+ let node = Ufind.get m.store r in
+ let size = sizeof node.clayout in
+ try
+ let check acs =
+ let t = Access.typeof acs in
+ if Cil.bitsSizeOf t > size then raise Exit ;
+ match !types with
+ | None -> types := Some t
+ | Some t0 -> if not @@ Cil_datatype.Typ.equal t0 t then raise Exit
+ in
+ Access.Set.iter check node.creads ;
+ Access.Set.iter check node.cwrites ;
+ Access.Set.iter check node.cshifts ;
+ !types
+ with Exit -> None
+
+(* -------------------------------------------------------------------------- *)
+(* --- High-Level API --- *)
+(* -------------------------------------------------------------------------- *)
+
+type range = {
+ label: string ; (* pretty printed fields *)
+ offset: int ;
+ length: int ;
+ cells: int ;
+ data: node ;
+}
+
+type region = {
+ node: node ;
+ parents: node list ;
+ roots: varinfo list ;
+ labels: string list ;
+ types: typ list ;
+ typed : typ option ;
+ fields: Fields.domain ;
+ reads: Access.acs list ;
+ writes: Access.acs list ;
+ shifts: Access.acs list ;
+ sizeof: int ;
+ singleton : bool ;
+ ranges: range list ;
+ pointed: node option ;
+}
+
+let make_range (m: map) fields Ranges.{ length ; offset ; data } : range =
+ let s = sizeof (get m data).clayout in
+ let p = Fields.pslice ~fields ~offset ~length in
+ {
+ label = Format.asprintf "%t" p ;
+ offset ; length ;
+ cells = if s = 0 then 0 else length / s ;
+ data = node m data ;
+ }
+
+let ranges (m:map) (r:node) =
+ let node = Ufind.get m.store r in
+ let fields = cfields node.clayout in
+ List.map (make_range m fields) (cranges node.clayout)
+
+let make_region (m: map) (n: node) (r: chunk) : region =
+ let types = ctypes r in
+ let typed = typed m n in
+ let sizeof = sizeof r.clayout in
+ let fields = cfields r.clayout in
+ let singleton = singleton m n in
+ {
+ node = n ;
+ parents = nodes m r.cparents ;
+ roots = Vset.elements r.croots ;
+ labels = Lset.elements r.clabels ;
+ reads = Access.Set.elements r.creads ;
+ writes = Access.Set.elements r.cwrites ;
+ shifts = Access.Set.elements r.cshifts ;
+ ranges = List.map (make_range m fields) (cranges r.clayout) ;
+ pointed = Option.map (node m) (cpointed r.clayout) ;
+ types ; typed ; singleton ; sizeof ; fields ;
+ }
+
+let region map n = make_region map n (get map n)
+
+let regions map =
+ let pool = ref [] in
+ iter map (fun r -> pool := region map r :: !pool) ;
+ List.rev !pool
+
+(* -------------------------------------------------------------------------- *)
+(* --- Pretty Printers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let pp_cells fmt = function
+ | 1 -> ()
+ | 0 -> Format.fprintf fmt "[…]"
+ | n -> Format.fprintf fmt "[%d]" n
+
+type slice =
+ | Padding of int
+ | Range of range
+
+let pad p q s =
+ let n = q - p in
+ if n > 0 then Padding n :: s else s
+
+let rec span k s = function
+ | [] -> pad k s []
+ | r::rs -> pad k r.offset @@ Range r :: span (r.offset + r.length) s rs
+
+let pp_slice fields fmt = function
+ | Padding n ->
+ Format.fprintf fmt "@ %a;" Fields.pp_bits n
+ | Range r ->
+ Format.fprintf fmt "@ %t: %a%a;"
+ (Fields.pslice ~fields ~offset:r.offset ~length:r.length)
+ pp_node r.data
+ pp_cells r.cells
+
+let pp_range fmt (r: range) =
+ Format.fprintf fmt "@ %d..%d: %a%a;"
+ r.offset (r.offset + r.length) pp_node r.data pp_cells r.cells
+
+let pp_region fmt (m: region) =
+ begin
+ let acs r s = if s = [] then '-' else r in
+ Format.fprintf fmt "@[<hov 2>%a: %c%c%c"
+ pp_node m.node
+ (acs 'R' m.reads) (acs 'W' m.writes) (acs 'A' m.shifts) ;
+ List.iter (Format.fprintf fmt "@ %s:") m.labels ;
+ List.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.roots ;
+ List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) m.types ;
+ Format.fprintf fmt "@ %db" m.sizeof ;
+ Option.iter (Format.fprintf fmt "@ (*%a)" pp_node) m.pointed ;
+ if m.ranges <> [] then
+ begin
+ Format.fprintf fmt "@ @[<hv 0>@[<hv 2>{" ;
+ if Options.debug_atleast 1 then
+ List.iter (pp_range fmt) m.ranges
+ else
+ List.iter (pp_slice m.fields fmt) (span 0 m.sizeof m.ranges) ;
+ Format.fprintf fmt "@]@ }@]" ;
+ end ;
+ if Options.debug_atleast 1 then
+ begin
+ List.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.reads ;
+ List.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.writes ;
+ List.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.shifts ;
+ end ;
+ Format.fprintf fmt " ;@]" ;
+ end
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index af3cd23eb708edc8f8bc11a89ee58c3abaea3ab3..5e2affc0faa29d338dff62c646b30d086c656332 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -38,11 +38,13 @@ type region = {
roots: varinfo list ;
labels: string list ;
types: typ list ;
+ typed : typ option ;
fields: Fields.domain ;
reads: Access.acs list ;
writes: Access.acs list ;
shifts: Access.acs list ;
sizeof: int ;
+ singleton : bool ;
ranges: range list ;
pointed: node option ;
}
@@ -70,24 +72,28 @@ val equal : map -> node -> node -> bool
val node : map -> node -> node
val nodes : map -> node list -> node list
-val iter : map -> (region -> unit) -> unit
-val iter_node : map -> (node -> unit) -> unit
-val region : map -> node -> region
-val regions : map -> region list
+val size : map -> node -> int
val parents : map -> node -> node list
val roots : map -> node -> varinfo list
+val labels : map -> node -> string list
+val region : map -> node -> region
+val regions : map -> region list
+val iter : map -> (node -> unit) -> unit
+
+val new_chunk : map ->
+ ?parent:node -> ?size:int -> ?ptr:node -> ?pointed:node ->
+ unit -> node
-val new_chunk : map -> ?size:int -> ?ptr:node -> ?pointed:node -> unit -> node
val add_root : map -> Cil_types.varinfo -> node
val add_label : map -> string -> node
val add_field : map -> node -> fieldinfo -> node
-val add_index : map -> node -> typ -> int -> node
+val add_index : map -> node -> typ -> node
val add_points_to : map -> node -> node -> unit
val add_value : map -> node -> typ -> node option
-val read : map -> node -> Access.acs -> unit
-val write : map -> node -> Access.acs -> unit
-val shift : map -> node -> Access.acs -> unit
+val add_read : map -> node -> Access.acs -> unit
+val add_write : map -> node -> Access.acs -> unit
+val add_shift : map -> node -> Access.acs -> unit
val merge : map -> node -> node -> unit
val merge_all : map -> node list -> unit
@@ -99,12 +105,16 @@ val index : map -> node -> typ -> node
val lval : map -> lval -> node
val exp : map -> exp -> node option
+val ranges : map -> node -> range list
val points_to : map -> node -> node option
val pointed_by : map -> node -> node list
val included : map -> node -> node -> bool
val separated : map -> node -> node -> bool
+val singleton : map -> node -> bool
val reads : map -> node -> typ list
val writes : map -> node -> typ list
val shifts : map -> node -> typ list
+val types : map -> node -> typ list
+val typed : map -> node -> typ option
diff --git a/src/plugins/region/ranges.ml b/src/plugins/region/ranges.ml
index 54e7cc2c43fc0d8864f4332f1de80d8006c647f3..f8a6e0d3e9ddfd4ec6762bda129cbeeeb962e32c 100644
--- a/src/plugins/region/ranges.ml
+++ b/src/plugins/region/ranges.ml
@@ -57,7 +57,7 @@ let range ?(offset=0) ?(length=1) data = singleton { offset ; length ; data }
let rec find (k: int) = function
| [] -> raise Not_found
| ({ offset ; length } as r) :: rs ->
- if offset <= k && k <= offset + length then r else find k rs
+ if offset <= k && k < offset + length then r else find k rs
let find k (R rs) = find k rs
@@ -70,7 +70,7 @@ let rec merge f ra rb =
if a' <= b.offset then
a :: merge f wa rb
else
- if b' < a.offset then
+ if b' <= a.offset then
b :: merge f ra wb
else
let offset = min a.offset b.offset in
@@ -83,12 +83,11 @@ let rec merge f ra rb =
let merge f (R x) (R y) = R (merge f x y)
-let squash f = function
- | R [] -> None
- | R (x::xs) -> Some (List.fold_left (fun w r -> f w r.data) x.data xs)
-
let iteri f (R xs) = List.iter f xs
+let foldi f w (R xs) = List.fold_left f w xs
let iter f (R xs) = List.iter (fun r -> f r.data) xs
+let fold f w (R xs) = List.fold_left (fun w r -> f w r.data) w xs
+let mapi f (R xs) = R (List.map f xs)
let map f (R xs) = R (List.map (fun r -> { r with data = f r.data }) xs)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/ranges.mli b/src/plugins/region/ranges.mli
index b04c273feb06930e56c6d996efe8688f8519dd86..7149b1cd7b3b7da4ce5be8cc8ff8de8c55f92cb6 100644
--- a/src/plugins/region/ranges.mli
+++ b/src/plugins/region/ranges.mli
@@ -36,9 +36,12 @@ val empty : 'a t
val singleton : 'a range -> 'a t
val range : ?offset:int -> ?length:int -> 'a -> 'a t
val merge : ('a range -> 'a range -> 'a) -> 'a t -> 'a t -> 'a t
-val squash : ('a -> 'a -> 'a) -> 'a t -> 'a option
val find : int -> 'a t -> 'a range
+
val map : ('a -> 'b) -> 'a t -> 'b t
+val mapi : ('a range -> 'b range) -> 'a t -> 'b t
val iter : ('a -> unit) -> 'a t -> unit
val iteri : ('a range -> unit) -> 'a t -> unit
+val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
+val foldi : ('b -> 'a range -> 'b) -> 'b -> 'a t -> 'b
diff --git a/src/plugins/region/register.ml b/src/plugins/region/register.ml
index 54cd5cdd62b1d0f0a2e294a2b7ebce49a6390fca..0d904f9fd3ef8e01ccde1980924a745a6a43e312 100644
--- a/src/plugins/region/register.ml
+++ b/src/plugins/region/register.ml
@@ -31,7 +31,20 @@ let main () =
begin
Ast.compute () ;
R.feedback "Analyzing regions" ;
- Globals.Functions.iter Analysis.compute ;
+ Globals.Functions.iter
+ begin fun kf ->
+ let domain = Analysis.get kf in
+ Options.result "@[<v 2>Function %a:%t@]@."
+ Kernel_function.pretty kf
+ begin fun fmt ->
+ List.iter
+ begin fun r ->
+ Format.pp_print_newline fmt () ;
+ Memory.pp_region fmt r ;
+ end @@
+ Memory.regions domain.map
+ end
+ end
end
let () = Boot.Main.extend main
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 243f1975703242f4c9a0158b96c5467f842d8fcd..e5f6ebffe1192ec4dd5ac1b6df0e924eb198b78b 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -114,6 +114,7 @@ struct
let label (m: Memory.region) =
let buffer = Buffer.create 4 in
+ if m.singleton then Buffer.add_string buffer "!" ;
if m.reads <> [] then Buffer.add_char buffer 'R' ;
if m.writes <> [] then Buffer.add_char buffer 'W' ;
if m.pointed <> None then Buffer.add_char buffer '*'
@@ -133,7 +134,7 @@ struct
Typ.pretty fmt ty
let title (m: Memory.region) =
- Format.asprintf "%t (%db)"
+ Format.asprintf "%t (%db)%t"
begin fun fmt ->
match m.types with
| [] -> Format.pp_print_string fmt "Compound"
@@ -141,7 +142,11 @@ struct
| ty::ts ->
pp_typ_layout 0 fmt ty ;
List.iter (Format.fprintf fmt ", %a" (pp_typ_layout 0)) ts ;
- end m.sizeof
+ end
+ m.sizeof
+ begin fun fmt ->
+ if m.singleton then Format.pp_print_string fmt " (singleton)"
+ end
let jtype = Data.declare ~package ~name:"region" @@
Jrecord [
@@ -154,7 +159,8 @@ struct
"pointed", NodeOpt.jtype ;
"reads", Jboolean ;
"writes", Jboolean ;
- "bytes", Jboolean ;
+ "typed", Jboolean ;
+ "singleton", Jboolean ;
"label", Jstring ;
"title", Jstring ;
]
@@ -170,7 +176,8 @@ struct
"pointed", NodeOpt.to_json @@ m.pointed ;
"reads", Json.of_bool (m.reads <> []) ;
"writes", Json.of_bool (m.writes <> []) ;
- "bytes", Json.of_bool (List.length m.types > 1) ;
+ "typed", Json.of_bool (m.typed <> None) ;
+ "singleton", Json.of_bool m.singleton ;
"label", Json.of_string @@ label m ;
"title", Json.of_string @@ title m ;
]
diff --git a/src/plugins/region/tests/region/comp.c b/src/plugins/region/tests/region/comp.i
similarity index 100%
rename from src/plugins/region/tests/region/comp.c
rename to src/plugins/region/tests/region/comp.i
diff --git a/src/plugins/region/tests/region/oracle/blob.res.oracle b/src/plugins/region/tests/region/oracle/blob.res.oracle
index f18edf72e524a8a5f91a20925399ee9dd6ddbfb7..2a12e2190c3bbbd534539bcdd62d45b5967050f4 100644
--- a/src/plugins/region/tests/region/oracle/blob.res.oracle
+++ b/src/plugins/region/tests/region/oracle/blob.res.oracle
@@ -1,9 +1,8 @@
[kernel] Parsing blob.i (no preprocessing)
[region] Analyzing regions
[region] Function array_blob:
- R0003: --- arr 96b { #96b: R0004[…]; } ;
- R0004: --- 0b ;
- R0001: -W- p (int *) 64b (*R0004) ;
+ R0003: --- arr 32b ;
+ R0001: -W- p (int *) 64b (*R0003) ;
[region] Function struct_blob:
R0003: --- y 64b { .f: R0004[…]; #32b; } ;
R0004: --- 0b ;
diff --git a/src/plugins/region/tests/region/oracle/comp.res.oracle b/src/plugins/region/tests/region/oracle/comp.res.oracle
index d444b5dc68c66f3c4e63bbbbd876679a76495ab0..31059b7aa9c15096b4dca29bebf767c897783b6f 100644
--- a/src/plugins/region/tests/region/oracle/comp.res.oracle
+++ b/src/plugins/region/tests/region/oracle/comp.res.oracle
@@ -1,9 +1,8 @@
-[kernel] Parsing comp.c (with preprocessing)
+[kernel] Parsing comp.i (no preprocessing)
[region] Analyzing regions
[region] Function f:
- R0003: --- s 192b { .x: R0004; #32b; .z: R0008; .arr: R000d; } ;
+ R0003: --- s 192b { .x: R0004; #32b; .z: R0008; .arr: R000d[4]; } ;
R0004: -W- (int) 32b ;
R0008: -W- (int *) 64b (*R0001) ;
R0001: RW- a (int) 32b ;
- R000d: --- 64b { #64b: R000f[4]; } ;
- R000f: -W- (short) 16b ;
+ R000d: -W- (short) 16b ;
diff --git a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
index 4de3c9517dbac676e8443d7aea783f55c9355fd5..586a487686d61159339da6487b2fd94f5dc0b18f 100644
--- a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
+++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
@@ -4,14 +4,19 @@
R0003: R-- fb (FB *) 64b (*R0005) ;
R0005: --- 704b
{
- .prm.inp1: R0007[2];
+ .prm: R002e;
+ .inp1: R0007;
#128b;
.out1: R000f;
.out2: R006a;
- .out3.idx1: R0017[2];
+ .out3: R0074;
+ .idx1: R0017;
#128b;
.sum: R0057;
} ;
+ R002e: R-- (struct N *) 64b (*R0031) ;
+ R0031: --- 128b { .v: R0033; #64b; } ;
+ R0033: R-- (double) 64b ;
R0007: R-- (struct N *) 64b (*R0027) ;
R0027: --- 128b { .v: R0029; .s: R0049; #32b; } ;
R0029: R-- (double) 64b ;
@@ -23,13 +28,17 @@
R006a: R-- (struct N *) 64b (*R006d) ;
R006d: --- 128b { .v: R006f; #64b; } ;
R006f: R-- (double) 64b ;
- R0017: R-- (struct N *) (struct L *) 64b (*R0041) ;
- R0041: --- 64b { .v.s: R0043[2]; } ;
- R0043: RW- (int) (double) 32b ;
+ R0074: R-- (struct N *) 64b (*R0077) ;
+ R0077: --- 128b { .v: R0079; #64b; } ;
+ R0079: R-- (double) 64b ;
+ R0017: R-- (struct L *) 64b (*R0041) ;
+ R0041: --- 64b { .v: R0043; .s: R0052; } ;
+ R0043: -W- (int) 32b ;
+ R0052: -W- (int) 32b ;
R0057: R-- (struct N *) 64b (*R005a) ;
- R005a: --- 128b { .v: R005c; .s: R0083; #32b; } ;
+ R005a: --- 128b { .v: R005c; .s: R0084; #32b; } ;
R005c: -W- (double) 64b ;
- R0083: -W- (int) 32b ;
+ R0084: -W- (int) 32b ;
R0001: RWA inp (SN *) 64b (*R0007) ;
R000b: RWA out (SN *) 64b (*R000f) ;
R0013: RWA idx (SL *) 64b (*R0017) ;
diff --git a/src/plugins/region/tests/region/oracle/union.res.oracle b/src/plugins/region/tests/region/oracle/union.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1f2cf922dfa5937551f43671c258ed47f0f24022
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/union.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing union.i (no preprocessing)
+[region] Analyzing regions
+[region] Function f:
+ R0001: R-- p (union U *) 64b (*R0003) ;
+ R0003: RW- (int) (short) 16b ;
diff --git a/src/plugins/region/tests/region/union.i b/src/plugins/region/tests/region/union.i
new file mode 100644
index 0000000000000000000000000000000000000000..85507b96692f3df1944db26f4f146c2f4243547b
--- /dev/null
+++ b/src/plugins/region/tests/region/union.i
@@ -0,0 +1,10 @@
+union U {
+ short s[2];
+ int i;
+};
+
+void f (union U *p) {
+ p->i++;
+ p->s[0]++;
+ p->s[1]++;
+}
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index f173e8b2e0bb0dda307e02dd515d13002bb160bd..22804c75a399e29cf3fe5f7ab7986c5d461d9ef5 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes
+type mheap = Hoare | ZeroAlias | Eva | Bytes | Region | Typed of MemTyped.pointer
type mvar = Raw | Var | Ref | Caveat
type setup = {
@@ -69,6 +69,7 @@ let descr_mheap d = function
| Typed p -> main d "typed" ; descr_mtyped d p
| Eva -> main d "eva"
| Bytes -> main d "bytes"
+ | Region -> main d "region"
let descr_mvar d = function
| Var -> ()
@@ -192,6 +193,10 @@ struct
let iter = refusage_iter
end
+module Static = MemVar.Static
+module MemRegion = MemRegion.Make(RegionAnalysis)(MemBytes)
+module MemEva = MemVal.Make(MemVal.Eva)
+
(* -------------------------------------------------------------------------- *)
(* --- Generator & Model --- *)
(* -------------------------------------------------------------------------- *)
@@ -199,18 +204,17 @@ end
(* Each model must be instanciated statically because of registered memory
models identifiers and Frama-C states *)
-module Register(V : MemVar.VarUsage)(M : Sigs.Model)
+module MakeVar(V : MemVar.VarUsage)(M : Sigs.Model)
= MemVar.Make(MakeVarUsage(V))(M)
-module Model_Hoare_Raw = Register(MemVar.Raw)(MemEmpty)
-module Model_Hoare_Ref = Register(Ref)(MemEmpty)
-module Model_Typed_Var = Register(Var)(MemTyped)
-module Model_Typed_Ref = Register(Ref)(MemTyped)
-module Model_Bytes_Var = Register(Var)(MemBytes)
-module Model_Bytes_Ref = Register(Ref)(MemBytes)
-module Model_Caveat = Register(Caveat)(MemTyped)
-
-module MemVal = MemVal.Make(MemVal.Eva)
+module Model_Hoare_Raw = MakeVar(MemVar.Raw)(MemEmpty)
+module Model_Hoare_Ref = MakeVar(Ref)(MemEmpty)
+module Model_Typed_Var = MakeVar(Var)(MemTyped)
+module Model_Typed_Ref = MakeVar(Ref)(MemTyped)
+module Model_Bytes_Var = MakeVar(Var)(MemBytes)
+module Model_Bytes_Ref = MakeVar(Ref)(MemBytes)
+module Model_Caveat = MakeVar(Caveat)(MemTyped)
+module Model_Region = MakeVar(Static)(MemRegion)
module MakeCompiler(M:Sigs.Model) =
struct
@@ -228,15 +232,12 @@ module Comp_Hoare_Ref = MakeCompiler(Model_Hoare_Ref)
module Comp_MemTyped = MakeCompiler(MemTyped)
module Comp_Typed_Var = MakeCompiler(Model_Typed_Var)
module Comp_Typed_Ref = MakeCompiler(Model_Typed_Ref)
-
module Comp_Caveat = MakeCompiler(Model_Caveat)
-
module Comp_MemBytes = MakeCompiler(MemBytes)
module Comp_Bytes_Var = MakeCompiler(Model_Bytes_Var)
module Comp_Bytes_Ref = MakeCompiler(Model_Bytes_Ref)
-
-module Comp_MemVal = MakeCompiler(MemVal)
-
+module Comp_Region = MakeCompiler(Model_Region)
+module Comp_MemEva = MakeCompiler(MemEva)
let compiler mheap mvar : (module Sigs.Compiler) =
match mheap , mvar with
@@ -247,11 +248,11 @@ let compiler mheap mvar : (module Sigs.Compiler) =
| Typed _ , Raw -> (module Comp_MemTyped)
| Typed _ , Var -> (module Comp_Typed_Var)
| Typed _ , Ref -> (module Comp_Typed_Ref)
- | Eva, _ -> (module Comp_MemVal)
+ | Eva, _ -> (module Comp_MemEva)
| Bytes, Raw -> (module Comp_MemBytes)
| Bytes, Var -> (module Comp_Bytes_Var)
| Bytes, Ref -> (module Comp_Bytes_Ref)
-
+ | Region, _ -> (module Comp_Region)
(* -------------------------------------------------------------------------- *)
(* --- Tuning --- *)
@@ -260,7 +261,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
let configure_mheap = function
| Hoare -> MemEmpty.configure ()
| ZeroAlias -> MemZeroAlias.configure ()
- | Eva -> MemVal.configure ()
+ | Eva -> MemEva.configure ()
| Bytes -> MemBytes.configure ()
| Typed p ->
let rollback_memtyped = MemTyped.configure () in
@@ -270,6 +271,7 @@ let configure_mheap = function
Context.pop MemTyped.pointer orig_memtyped_pointer
in
rollback
+ | Region -> MemBytes.configure ()
let configure_driver setup driver () =
let rollback_mheap = configure_mheap setup.mheap in
@@ -345,6 +347,7 @@ let update_config ~warning m s = function
| "TYPED" -> { s with mheap = Typed MemTyped.Fits }
| "CAST" -> { s with mheap = Typed MemTyped.Unsafe }
| "NOCAST" -> { s with mheap = Typed MemTyped.NoCast }
+ | "REGION" -> { s with mheap = Region }
| "EVA" -> { s with mheap = Eva }
| "BYTES" -> { s with mheap = Bytes }
| "CAVEAT" -> { s with mvar = Caveat }
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 1b9ac3843c252292249ffcc1f491024aefad20b4..741faf0c4268a07813bdf8ebbad13505b133cca2 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva | Bytes
+type mheap = Hoare | ZeroAlias | Eva | Bytes | Region | Typed of MemTyped.pointer
type mvar = Raw | Var | Ref | Caveat
type setup = {
diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index b3d3dad054fceb0e5f459852e480ce16873a2473..795aec9adeab33b0bbfbbc0c589149d4ccecb7b3 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -28,7 +28,8 @@ module Logic = Qed.Logic
(* Why3 symbols *)
-module Why3 = struct
+module Why3 =
+struct
let library = "membytes"
let t_vblock = Qed.Logic.Array (Qed.Logic.Int, Qed.Logic.Int)
@@ -197,13 +198,9 @@ type sigma = Sigma.t
type domain = Sigma.domain
type segment = loc rloc
-let comp_cluster () =
- Definitions.cluster ~id:"Compound" ~title:"Memory Compound Loader" ()
-
let shift_cluster () =
Definitions.cluster ~id:"Shifts" ~title:"Shifts Definitions" ()
-
(* ********************************************************************** *)
(* SIZE *)
(* ********************************************************************** *)
@@ -676,9 +673,6 @@ module Model = struct
Why3.havoc fresh current loc n
else fresh
- let eqmem obj loc _chunk m1 m2 =
- Why3.eqmem m1 m2 loc @@ sizeof obj
-
let eqmem_forall obj loc _chunk m1 m2 =
let xp = Lang.freshvar ~basename:"p" MemAddr.t_addr in
let p = e_var xp in
@@ -1130,3 +1124,17 @@ let scope seq scope xs =
in e_set m (BASE.get x) size)
(Sigma.value seq.pre Alloc) xs in
[ p_equal (Sigma.value seq.post Alloc) alloc ]
+
+(* ********************************************************************** *)
+(* API with Region *)
+(* ********************************************************************** *)
+
+let sizeof = protected_sizeof_object
+let last = Model.last
+let frames = Model.frames
+let eqmem_forall = Model.eqmem_forall
+let set_init = Model.set_init
+let is_init_range = Model.is_init_range
+let value_footprint = Model.value_footprint
+let init_footprint = Model.init_footprint
+let havoc = Model.havoc
diff --git a/src/plugins/wp/MemBytes.mli b/src/plugins/wp/MemBytes.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ddb5ce41037e817691479951fd8e66cb96de2a34
--- /dev/null
+++ b/src/plugins/wp/MemBytes.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include MemRegion.ModelWithLoader
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index bf2d6b187cd68dbe8e27c7b9a1b1d5bfa3f092fe..a94374e98ba0114944c99af67840d35ed99ab71d 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -82,7 +82,6 @@ sig
val set_init_atom : Sigma.t -> c_object -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
- (* val monotonic_init : Sigma.t -> Sigma.t -> pred *)
end
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 46d62359db33e62fbf0df3d723f02ffe00d4f24c..4e73e424b9802157c98f0a73b38324232500bc20 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -78,7 +78,6 @@ sig
val set_init_atom : Sigma.t -> c_object -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
- (* val monotonic_init : Sigma.t -> Sigma.t -> pred *)
end
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
new file mode 100644
index 0000000000000000000000000000000000000000..06b0704d0da1a99ca9d576d4d7515433f9f08770
--- /dev/null
+++ b/src/plugins/wp/MemRegion.ml
@@ -0,0 +1,718 @@
+(*************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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 Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+open Cil_types
+open Ctypes
+open Lang.F
+open Sigs
+open MemMemory
+
+type primitive = Int of c_int | Float of c_float | Ptr
+type kind = Single of primitive | Many of primitive | Garbled
+
+let pp_prim fmt = function
+ | Int i -> Ctypes.pp_int fmt i
+ | Float f -> Ctypes.pp_float fmt f
+ | Ptr -> Format.pp_print_string fmt "ptr"
+
+let pp_kind fmt = function
+ | Single p -> pp_prim fmt p
+ | Many p -> Format.fprintf fmt "[%a]" pp_prim p
+ | Garbled -> Format.pp_print_string fmt "[bytes]"
+
+let tau_of_prim = function
+ | Int _ -> Qed.Logic.Int
+ | Float f -> Cfloat.tau_of_float f
+ | Ptr -> MemAddr.t_addr
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Analysis Proxy --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type RegionProxy =
+sig
+ type region
+ module Type : Sigs.Type with type t = region
+ val id : region -> int
+ val of_id : int -> region option
+ val kind : region -> kind
+ val name : region -> string option
+ val cvar : varinfo -> region option
+ val field : region -> fieldinfo -> region option
+ val shift : region -> c_object -> region option
+ val points_to : region -> region option
+ val literal : eid:int -> Cstring.cst -> region option
+ val separated : region -> region -> bool
+ val included : region -> region -> bool
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Underlying Model (Handles Addresses & Garbled) --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type ModelWithLoader = sig
+ include Sigs.Model
+ include Sigs.Model
+ val sizeof : c_object -> term
+
+ val last : sigma -> c_object -> loc -> term
+ val frames : c_object -> loc -> chunk -> frame list
+
+ val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term
+
+ val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
+
+ val load_int : sigma -> c_int -> loc -> term
+ val load_float : sigma -> c_float -> loc -> term
+ val load_pointer : sigma -> typ -> loc -> loc
+
+ val store_int : sigma -> c_int -> loc -> term -> chunk * term
+ val store_float : sigma -> c_float -> loc -> term -> chunk * term
+ val store_pointer : sigma -> typ -> loc -> term -> chunk * term
+
+ val set_init_atom : sigma -> c_object -> loc -> term -> chunk * term
+ val set_init : c_object -> loc -> length:term -> chunk -> current:term -> term
+ val is_init_atom : sigma -> c_object -> loc -> term
+ val is_init_range : sigma -> c_object -> loc -> term -> pred
+
+ val value_footprint : c_object -> loc -> domain
+ val init_footprint : c_object -> loc -> domain
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Make (R:RegionProxy) (M:ModelWithLoader) (*: Sigs.Model*) =
+struct
+
+ type region = R.region
+ let datatype = "MemRegion.Make"
+ (* For projectification. Must be unique among models. *)
+
+ let configure = M.configure
+ let configure_ia = M.configure_ia
+ let hypotheses = M.hypotheses
+
+ module MChunk = M.Chunk
+ module RChunk =
+ struct
+ let self = "MemRegion.RChunk"
+
+ type mu = Value of primitive | Array of primitive | ValInit | ArrInit
+ type t = { mu : mu ; region : R.region }
+
+ let pp_mu fmt = function
+ | Value p -> Format.fprintf fmt "µ%a" pp_prim p
+ | Array p -> Format.fprintf fmt "µ%a[]" pp_prim p
+ | ValInit -> Format.pp_print_string fmt "µinit"
+ | ArrInit -> Format.pp_print_string fmt "µinit[]"
+
+ let hash { mu ; region } = Hashtbl.hash (mu, R.Type.hash region)
+ let equal a b = Stdlib.(=) a.mu b.mu && R.Type.equal a.region b.region
+ let compare a b =
+ let cmp = Stdlib.compare a.mu b.mu in
+ if cmp <> 0 then cmp else R.Type.compare a.region b.region
+
+ let pretty fmt { mu ; region } =
+ Format.fprintf fmt "%a@%03d" pp_mu mu (R.id region)
+
+ let tau_of_chunk { mu } =
+ match mu with
+ | Value p -> tau_of_prim p
+ | ValInit -> Qed.Logic.Bool
+ | Array p -> Qed.Logic.Array(MemAddr.t_addr,tau_of_prim p)
+ | ArrInit -> Qed.Logic.Array(MemAddr.t_addr,Qed.Logic.Bool)
+
+ let basename_of_chunk { mu ; region } =
+ match mu with
+ | ValInit -> "Vinit"
+ | ArrInit -> "Minit"
+ | Array p -> Format.asprintf "M%a" pp_prim p
+ | Value p ->
+ match R.name region with
+ | Some a -> a
+ | None -> Format.asprintf "V%a" pp_prim p
+
+ let is_framed _ = false
+
+ end
+
+ module MHeap = M.Heap
+ module MSigma = M.Sigma
+
+ module RHeap = Qed.Collection.Make(RChunk)
+ module RSigma = Sigma.Make(RChunk)(RHeap)
+
+ type chunk =
+ | M of MChunk.t
+ | R of RChunk.t
+
+ let cmap f g (m,r) = (f m, g r)
+ let cmap2 f g (m1,r1) (m2,r2) = (f m1 m2, g r1 r2)
+ let capply f g (m,r) = function M c -> f m c, r | R c -> m, g r c
+ let cmerge f g (m,r) = function M c -> f m c | R c -> g r c
+ let mseq { pre ; post } = { pre = fst pre ; post = fst post }
+ let rseq { pre ; post } = { pre = snd pre ; post = snd post }
+
+ module Chunk : Sigs.Chunk with type t = chunk =
+ struct
+ type t = chunk
+ let self = "Wp.MemRegion.Self"
+ let hash = function
+ | M c -> 3 * MChunk.hash c
+ | R c -> 5 * RChunk.hash c
+
+ let equal ca cb = match ca, cb with
+ | M c1, M c2 -> MChunk.equal c1 c2
+ | R c1, R c2 -> RChunk.equal c1 c2
+ | M _, R _ | R _, M _ -> false
+
+ let compare c1 c2 =
+ match c1, c2 with
+ | M m1, M m2 -> MChunk.compare m1 m2
+ | R r1, R r2 -> RChunk.compare r1 r2
+ | M _, R _ -> (-1)
+ | R _, M _ -> (+1)
+
+ let pretty fmt = function
+ | M c -> MChunk.pretty fmt c
+ | R c -> RChunk.pretty fmt c
+
+ let tau_of_chunk = function
+ | M c -> MChunk.tau_of_chunk c
+ | R c -> RChunk.tau_of_chunk c
+
+ let basename_of_chunk = function
+ | M c -> MChunk.basename_of_chunk c
+ | R c -> RChunk.basename_of_chunk c
+
+ let is_framed = function
+ | M c -> MChunk.is_framed c
+ | R c -> RChunk.is_framed c
+
+ end
+
+ module Heap = Qed.Collection.Make(Chunk)
+ module Domain = Heap.Set
+
+ type sigma = MSigma.t * RSigma.t
+ type domain = Domain.t
+
+ module Sigma =
+ struct
+
+ type t = sigma
+ type chunk = Chunk.t
+ module Chunk = Heap
+
+ type domain = Domain.t
+
+ let create () : t = (MSigma.create (), RSigma.create ())
+
+ let pretty fmt (m,r) =
+ Format.fprintf fmt "@[<hv 0>{@[<hv 2>@ %a;@ %a;@]@ }@]"
+ MSigma.pretty m
+ RSigma.pretty r
+
+ let empty : domain = Domain.empty
+ let union = Domain.union
+ let mem = cmerge MSigma.mem RSigma.mem
+ let get = cmerge MSigma.get RSigma.get
+ let value = cmerge MSigma.value RSigma.value
+ let copy = cmap MSigma.copy RSigma.copy
+ let choose = cmap2 MSigma.choose RSigma.choose
+ let havoc_chunk = capply MSigma.havoc_chunk RSigma.havoc_chunk
+ let havoc_any ~call = cmap (MSigma.havoc_any ~call) (RSigma.havoc_any ~call)
+
+ let merge (m1,r1) (m2,r2) =
+ let m,p1,p2 = MSigma.merge m1 m2 in
+ let r,q1,q2 = RSigma.merge r1 r2 in
+ (m,r), Passive.union p1 q1, Passive.union p2 q2
+
+ let merge_list l =
+ let m,p = MSigma.merge_list @@ List.map fst l in
+ let r,q = RSigma.merge_list @@ List.map snd l in
+ (m,r), List.map2 Passive.union p q
+
+ let join (m1,r1) (m2,r2) =
+ Passive.union (MSigma.join m1 m2) (RSigma.join r1 r2)
+
+ let iter f (m,r) =
+ begin
+ MSigma.iter (fun c -> f (M c)) m ;
+ RSigma.iter (fun c -> f (R c)) r ;
+ end
+
+ let iter2 f (m1,r1) (m2,r2) =
+ begin
+ MSigma.iter2 (fun c -> f (M c)) m1 m2 ;
+ RSigma.iter2 (fun c -> f (R c)) r1 r2 ;
+ end
+
+ let mdomain d =
+ MHeap.Set.fold (fun c s -> Domain.add (M c) s) d Domain.empty
+ let rdomain d =
+ RHeap.Set.fold (fun c s -> Domain.add (R c) s) d Domain.empty
+
+ let dsplit d =
+ let m = ref MHeap.Set.empty in
+ let r = ref RHeap.Set.empty in
+ Domain.iter
+ (function
+ | M c -> m := MHeap.Set.add c !m
+ | R c -> r := RHeap.Set.add c !r
+ ) d ;
+ !m, !r
+
+ let assigned ~pre:(m1,r1) ~post:(m2,r2) d =
+ let m,r = dsplit d in
+ let hm = MSigma.assigned ~pre:m1 ~post:m2 m in
+ let hr = RSigma.assigned ~pre:r1 ~post:r2 r in
+ Bag.concat hm hr
+
+ let havoc (m,r) d =
+ let dm,dr = dsplit d in
+ MSigma.havoc m dm, RSigma.havoc r dr
+
+ let remove_chunks (m,r) d =
+ let dm,dr = dsplit d in
+ MSigma.remove_chunks m dm, RSigma.remove_chunks r dr
+
+ let domain (m,r) =
+ union (mdomain @@ MSigma.domain m) (rdomain @@ RSigma.domain r)
+
+ let writes (s : sigma sequence) =
+ union
+ (mdomain @@ MSigma.writes @@ mseq s)
+ (rdomain @@ RSigma.writes @@ rseq s)
+
+ end
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Region Loader --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ module Loader =
+ struct
+ let name = "MemRegion.Loader"
+
+ module Chunk = Chunk
+ module Sigma = Sigma
+
+ type loc =
+ | Null
+ | Raw of M.loc
+ | Loc of M.loc * region
+
+ let make a = function None -> Raw a | Some r -> Loc(a,r)
+ let loc = function Null -> M.null | Raw a | Loc(a,_) -> a
+ let reg = function Null | Raw _ -> None | Loc(_,r) -> Some r
+ let kind = function Null | Raw _ -> Garbled | Loc(_,r) -> R.kind r
+ let rfold f = function Null | Raw _ -> None | Loc(_,r) -> f r
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Utilities on locations --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let last sigma ty l = M.last (fst sigma) ty (loc l)
+
+ let to_addr l = M.pointer_val (loc l)
+
+ let sizeof ty = M.sizeof ty
+
+ let field l fd =
+ make (M.field (loc l) fd) (rfold (fun r -> R.field r fd) l)
+
+ let shift l obj ofs =
+ make (M.shift (loc l) obj ofs) (rfold (fun r -> R.shift r obj) l)
+
+ let frames ty l c =
+ match kind l with
+ | Single Ptr | Many Ptr | Garbled ->
+ let offset = M.sizeof ty in
+ let sizeof = Lang.F.e_one in
+ let tau = Chunk.tau_of_chunk c in
+ let basename = Chunk.basename_of_chunk c in
+ MemMemory.frames ~addr:(to_addr l) ~offset ~sizeof ~basename tau
+ | _ -> []
+
+ let havoc ty l ~length chunk ~fresh ~current =
+ match chunk with
+ | M c -> M.havoc ty (loc l) ~length c ~fresh ~current
+ | R c ->
+ match c.mu with
+ | Value _ | ValInit -> fresh
+ | Array _ | ArrInit -> e_fun f_havoc [fresh;current;to_addr l;length]
+
+ let eqmem_forall ty l chunk m1 m2 =
+ match chunk with
+ | M c -> M.eqmem_forall ty (loc l) c m1 m2
+ | R c ->
+ match c.mu with
+ | Value _ | ValInit -> [], p_true, p_equal m1 m2
+ | Array _ | ArrInit ->
+ let xp = Lang.freshvar ~basename:"b" MemAddr.t_addr in
+ let p = e_var xp in
+ let n = M.sizeof ty in
+ let separated =
+ p_call MemAddr.p_separated [p;e_one;to_addr l;n] in
+ let equal = p_equal (e_get m1 p) (e_get m2 p) in
+ [xp],separated,equal
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Load --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let localized action = function
+ | Null ->
+ Warning.error ~source:"MemRegion"
+ "Attempt to %s at NULL" action
+ | Raw a ->
+ Warning.error ~source:"MemRegion"
+ "Attempt to %s without region (%a)" action M.pretty a
+ | Loc(l,r) -> l,r
+
+ let to_region_pointer l =
+ let l,r = localized "loader" l in R.id r, M.pointer_val l
+
+ let of_region_pointer r _ t =
+ make (M.pointer_loc t) (R.of_id r)
+
+ let check_access action (p:primitive) (q:primitive) =
+ if Stdlib.(<>) p q then
+ Warning.error ~source:"MemRegion"
+ "Inconsistent %s (%a <> %a)"
+ action pp_prim p pp_prim q
+
+ let load_int sigma iota loc : term =
+ let l,r = localized "load int" loc in
+ match R.kind r with
+ | Garbled -> M.load_int (fst sigma) iota l
+ | Single p ->
+ check_access "load" p (Int iota) ;
+ RSigma.value (snd sigma) { mu = Value p ; region = r }
+ | Many p ->
+ check_access "load" p (Int iota) ;
+ e_get
+ (RSigma.value (snd sigma) { mu = Array p ; region = r})
+ (M.pointer_val l)
+
+ let load_float sigma flt loc : term =
+ let l,r = localized "load float" loc in
+ match R.kind r with
+ | Garbled -> M.load_float (fst sigma) flt l
+ | Single p ->
+ check_access "load" p (Float flt) ;
+ RSigma.value (snd sigma) { mu = Value p ; region = r }
+ | Many p ->
+ check_access "load" p (Float flt) ;
+ e_get
+ (RSigma.value (snd sigma) { mu = Array p ; region = r})
+ (M.pointer_val l)
+
+ let load_pointer sigma ty loc : loc =
+ let l,r = localized "load pointer" loc in
+ match R.points_to r with
+ | None ->
+ Warning.error ~source:"MemRegion"
+ "Attempt to load pointer without points-to@\n\
+ (addr %a, region %a)"
+ M.pretty l R.Type.pretty r
+ | Some _ as rp ->
+ let loc =
+ match R.kind r with
+ | Garbled -> M.load_pointer (fst sigma) ty l
+ | Single p ->
+ check_access "load" p Ptr ;
+ M.pointer_loc @@
+ RSigma.value (snd sigma) { mu = Value p ; region = r }
+ | Many p ->
+ check_access "load" p Ptr ;
+ M.pointer_loc @@
+ e_get
+ (RSigma.value (snd sigma) { mu = Array p ; region = r})
+ (M.pointer_val l)
+ in make loc rp
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Store --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let store_int sigma iota loc v : Chunk.t * term =
+ let l,r = localized "store int" loc in
+ match R.kind r with
+ | Garbled ->
+ let c, m = M.store_int (fst sigma) iota l v in M c, m
+ | Single p ->
+ check_access "store" p (Int iota) ;
+ R { mu = Value p ; region = r }, v
+ | Many p ->
+ check_access "store" p (Int iota) ;
+ let rc = RChunk.{ mu = Array p ; region = r } in
+ R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
+
+ let store_float sigma flt loc v : Chunk.t * term =
+ let l,r = localized "store float" loc in
+ match R.kind r with
+ | Garbled ->
+ let c,m = M.store_float (fst sigma) flt l v in M c, m
+ | Single p ->
+ check_access "store" p (Float flt) ;
+ R { mu = Value p ; region = r }, v
+ | Many p ->
+ check_access "store" p (Float flt) ;
+ let rc = RChunk.{ mu = Array p ; region = r } in
+ R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
+
+ let store_pointer sigma ty loc v : Chunk.t * term =
+ let l,r = localized "store pointer" loc in
+ match R.kind r with
+ | Garbled ->
+ let c,m = M.store_pointer (fst sigma) ty l v in M c, m
+ | Single p ->
+ check_access "store" p Ptr ;
+ R { mu = Value p ; region = r }, v
+ | Many p ->
+ check_access "store" p Ptr ;
+ let rc = RChunk.{ mu = Array p ; region = r } in
+ R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Init --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let is_init_atom sigma ty loc : term =
+ let l,r = localized "init atom" loc in
+ match R.kind r with
+ | Garbled -> M.is_init_atom (fst sigma) ty l
+ | Single _-> RSigma.value (snd sigma) { mu = ValInit ; region = r }
+ | Many _ ->
+ e_get
+ (RSigma.value (snd sigma) { mu = ArrInit ; region = r })
+ (M.pointer_val l)
+
+ let set_init_atom sigma ty loc v : Chunk.t * term =
+ let l,r = localized "init atom" loc in
+ match R.kind r with
+ | Garbled ->
+ let c,m = M.set_init_atom (fst sigma) ty l v in M c, m
+ | Single _-> R { mu = ValInit ; region = r }, v
+ | Many _ ->
+ let rc = RChunk.{ mu = ArrInit ; region = r } in
+ R rc, e_set (RSigma.value (snd sigma) rc) (M.pointer_val l) v
+
+ let is_init_range sigma ty loc length : pred =
+ let l,r = localized "init atom" loc in
+ match R.kind r with
+ | Garbled -> M.is_init_range (fst sigma) ty l length
+ | Single _ ->
+ Lang.F.p_bool @@ RSigma.value (snd sigma) { mu = ValInit ; region = r }
+ | Many _ ->
+ let map = RSigma.value (snd sigma) { mu = ArrInit ; region = r } in
+ let size = e_mul (M.sizeof ty) length in
+ p_call p_is_init_r [map;M.pointer_val l;size]
+
+
+ let set_init ty loc ~length chunk ~current : term =
+ let l,r = localized "init atom" loc in
+ match R.kind r, chunk with
+ | Garbled, M c -> M.set_init ty l ~length c ~current
+ | Garbled, R _ -> assert false
+ | Single _, _ -> e_true
+ | Many _ , _ ->
+ let size = e_mul (M.sizeof ty) length in
+ e_fun f_set_init [current;M.pointer_val l;size]
+
+ (* ---------------------------------------------------------------------- *)
+ (* --- Footprints --- *)
+ (* ---------------------------------------------------------------------- *)
+
+ let mfootprint ~value obj l =
+ if value
+ then M.value_footprint obj l
+ else M.init_footprint obj l
+
+ let rec footprint ~value obj loc = match loc with
+ | Null -> Sigma.mdomain @@ mfootprint ~value obj M.null
+ | Raw l -> Sigma.mdomain @@ mfootprint ~value obj l
+ | Loc(l,r) ->
+ match obj with
+ | C_comp { cfields = None} -> Domain.empty
+ | C_comp { cfields = Some fds } ->
+ List.fold_left
+ (fun dom fd ->
+ let obj = Ctypes.object_of fd.ftype in
+ let loc = field loc fd in
+ Domain.union dom (footprint ~value obj loc)
+ ) Domain.empty fds
+ | C_array { arr_element = elt } ->
+ let obj = object_of elt in
+ footprint ~value obj (shift loc obj e_zero)
+ | C_int _ | C_float _ | C_pointer _ ->
+ match R.kind r with
+ | Garbled ->
+ Sigma.mdomain @@ mfootprint ~value obj l
+ | Single p ->
+ let mu = if value then RChunk.Value p else ValInit in
+ Sigma.rdomain @@ RHeap.Set.singleton { mu ; region = r }
+ | Many p ->
+ let mu = if value then RChunk.Array p else ArrInit in
+ Sigma.rdomain @@ RHeap.Set.singleton { mu ; region = r }
+
+ let value_footprint = footprint ~value:true
+ let init_footprint = footprint ~value:false
+
+ end
+
+ type loc = Loader.loc
+ type segment = loc rloc
+
+ open Loader
+ module LOADER = MemLoader.Make(Loader)
+
+ let load = LOADER.load
+ let load_init = LOADER.load_init
+ let stored = LOADER.stored
+ let stored_init = LOADER.stored_init
+ let copied = LOADER.copied
+ let copied_init = LOADER.copied_init
+ let initialized = LOADER.initialized
+ let domain = LOADER.domain
+ let assigned = LOADER.assigned
+
+ (* {2 Reversing the Model} *)
+
+ type state = M.state
+
+ let state sigma = M.state (fst sigma)
+
+ let lookup s e = M.lookup s e
+
+ let updates = M.updates
+
+ let apply = M.apply
+
+ let iter = M.iter
+
+ let pretty fmt (l: loc) =
+ match l with
+ | Null -> M.pretty fmt M.null
+ | Raw l -> M.pretty fmt l
+ | Loc (l,r) -> Format.fprintf fmt "%a@%a" M.pretty l R.Type.pretty r
+
+ (* {2 Memory Model API} *)
+
+ let vars l = M.vars @@ loc l
+ let occurs x l = M.occurs x @@ loc l
+ let null = Null
+
+ let literal ~eid:eid str = make (M.literal ~eid str) (R.literal ~eid str)
+
+ let cvar v = make (M.cvar v) (R.cvar v)
+ let field = field
+ let shift = shift
+
+ let pointer_loc t = Raw (M.pointer_loc t)
+ let pointer_val l = M.pointer_val @@ loc l
+ let base_addr l = Raw (M.base_addr @@ loc l)
+ let base_offset l = M.base_offset @@ loc l
+ let block_length sigma obj l = M.block_length (fst sigma) obj @@ loc l
+ let is_null = function Null -> p_true | Raw l | Loc(l,_) -> M.is_null l
+ let loc_of_int obj t = Raw (M.loc_of_int obj t)
+ let int_of_loc iota l = M.int_of_loc iota @@ loc l
+
+ let cast conv l =
+ let l0 = loc l in
+ let r0 = reg l in
+ make (M.cast conv l0) r0
+
+ let loc_eq a b = M.loc_eq (loc a) (loc b)
+ let loc_lt a b = M.loc_lt (loc a) (loc b)
+ let loc_neq a b = M.loc_neq (loc a) (loc b)
+ let loc_leq a b = M.loc_leq (loc a) (loc b)
+ let loc_diff obj a b = M.loc_diff obj (loc a) (loc b)
+
+ let rloc = function
+ | Rloc(obj, l) -> Rloc (obj, loc l)
+ | Rrange(l, obj, inf, sup) -> Rrange(loc l, obj, inf, sup)
+
+ let rloc_region = function Rloc(_,l) | Rrange(l,_,_,_) -> reg l
+
+ let valid sigma acs r = M.valid (fst sigma) acs @@ rloc r
+ let invalid sigma r = M.invalid (fst sigma) (rloc r)
+
+ let included (a : segment) (b : segment) =
+ match rloc_region a, rloc_region b with
+ | Some ra, Some rb when R.separated ra rb -> p_false
+ | _ -> M.included (rloc a) (rloc b)
+
+ let separated (a : segment) (b : segment) =
+ match rloc_region a, rloc_region b with
+ | Some ra, Some rb when R.separated ra rb -> p_true
+ | _ -> M.separated (rloc a) (rloc b)
+
+ let alloc sigma vars =
+ if vars = [] then sigma else
+ let m,r = sigma in M.alloc m vars, r
+
+ let scope seq scope vars = M.scope (mseq seq) scope vars
+
+ let global sigma p = M.global (fst sigma) p
+
+ let frame sigma =
+ let pool = ref @@ M.frame (fst sigma) in
+ let assume p = pool := p :: !pool in
+ RSigma.iter
+ (fun c m ->
+ let open RChunk in
+ match c.mu with
+ | ValInit -> ()
+ | ArrInit -> assume @@ MemMemory.cinits (e_var m)
+ | Value Ptr -> assume @@ global sigma (e_var m)
+ | Array Ptr -> assume @@ MemMemory.framed (e_var m)
+ | Value (Int _ | Float _) | Array (Int _ | Float _) -> ()
+ ) (snd sigma) ;
+ !pool
+
+ let is_well_formed sigma =
+ let pool = ref @@ [M.is_well_formed (fst sigma)] in
+ let assume p = pool := p :: !pool in
+ RSigma.iter
+ (fun c m ->
+ let open RChunk in
+ match c.mu with
+ | ValInit | ArrInit -> ()
+ | Value (Int iota) -> assume @@ Cint.range iota (e_var m)
+ | Array (Int iota) ->
+ let a = Lang.freshvar ~basename:"p" @@ Lang.t_addr () in
+ let b = e_get (e_var m) (e_var a) in
+ assume @@ p_forall [a] (Cint.range iota b)
+ | Value (Float _ | Ptr) | Array (Float _ | Ptr) -> ()
+ ) (snd sigma) ;
+ p_conj !pool
+
+end
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
new file mode 100644
index 0000000000000000000000000000000000000000..545e03ac004fff4c80fce87a0cb2b1ad1e9066eb
--- /dev/null
+++ b/src/plugins/wp/MemRegion.mli
@@ -0,0 +1,82 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Ctypes
+open Lang.F
+open Sigs
+
+type primitive = | Int of c_int | Float of c_float | Ptr
+type kind = Single of primitive | Many of primitive | Garbled
+val pp_kind : Format.formatter -> kind -> unit
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type RegionProxy =
+sig
+ type region
+ module Type : Sigs.Type with type t = region
+ val id : region -> int
+ val of_id : int -> region option
+ val kind : region -> kind
+ val name : region -> string option
+ val cvar : varinfo -> region option
+ val field : region -> fieldinfo -> region option
+ val shift : region -> c_object -> region option
+ val points_to : region -> region option
+ val literal : eid:int -> Cstring.cst -> region option
+ val separated : region -> region -> bool
+ val included : region -> region -> bool
+end
+
+module type ModelWithLoader =
+sig
+ include Sigs.Model
+ val sizeof : c_object -> term
+
+ val last : sigma -> c_object -> loc -> term
+ val frames : c_object -> loc -> chunk -> frame list
+
+ val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term
+
+ val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
+
+ val load_int : sigma -> c_int -> loc -> term
+ val load_float : sigma -> c_float -> loc -> term
+ val load_pointer : sigma -> typ -> loc -> loc
+
+ val store_int : sigma -> c_int -> loc -> term -> chunk * term
+ val store_float : sigma -> c_float -> loc -> term -> chunk * term
+ val store_pointer : sigma -> typ -> loc -> term -> chunk * term
+
+ val set_init_atom : sigma -> c_object -> loc -> term -> chunk * term
+ val set_init : c_object -> loc -> length:term -> chunk -> current:term -> term
+ val is_init_atom : sigma -> c_object -> loc -> term
+ val is_init_range : sigma -> c_object -> loc -> term -> pred
+
+ val value_footprint : c_object -> loc -> domain
+ val init_footprint : c_object -> loc -> domain
+end
+
+module Make : RegionProxy -> ModelWithLoader -> Sigs.Model
diff --git a/src/plugins/wp/MemTyped.mli b/src/plugins/wp/MemTyped.mli
index ccdbfbd0b9786393e0819d561a77ce899b49aecc..05488e25a7020525b67f8ac8c9f1e14d9364a19a 100644
--- a/src/plugins/wp/MemTyped.mli
+++ b/src/plugins/wp/MemTyped.mli
@@ -24,7 +24,7 @@
(* --- Typed Memory Model --- *)
(* -------------------------------------------------------------------------- *)
-include Sigs.Model
-
type pointer = NoCast | Fits | Unsafe
val pointer : pointer Context.value
+
+include Sigs.Model
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
new file mode 100644
index 0000000000000000000000000000000000000000..008824f22d3745c7d4ae35baaa1d7967ffbd2892
--- /dev/null
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -0,0 +1,104 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Proxy to Region Analysis for Region Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+type region = Region.node
+
+let get_map () =
+ match WpContext.get_scope () with
+ | Kf kf -> Region.map kf
+ | Global -> Wp_parameters.not_yet_implemented "[region] logic context"
+
+let id region = Region.uid (get_map ()) region
+
+let of_id id =
+ try Some (Region.find (get_map ()) id)
+ with Not_found -> None
+
+module Type =
+struct
+ type t = region
+ let hash = Region.id
+ let equal r1 r2 = (Region.id r1 = Region.id r2)
+ let compare r1 r2 = Int.compare (Region.id r1) (Region.id r2)
+ let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
+end
+
+(* Keeping track of the decision to apply which memory model to each region *)
+module Kind = WpContext.Generator(Type)
+ (struct
+ open MemRegion
+ let name = "Wp.RegionAnalysis.Kind"
+ type key = region
+ type data = kind
+ let kind map r p = if Region.singleton map r then Single p else Many p
+ let compile r =
+ let map = get_map () in
+ match Region.typed map r with
+ | Some ty ->
+ begin
+ match Ctypes.object_of ty with
+ | C_int i -> kind map r (Int i)
+ | C_float f -> kind map r (Float f)
+ | C_pointer _ -> kind map r Ptr
+ | _ -> Garbled
+ end
+ | None -> Garbled
+ end)
+
+module Name = WpContext.Generator(Type)
+ (struct
+ let name = "Wp.RegionAnalysis.Name"
+ type key = region
+ type data = string option
+ let compile r =
+ let map = get_map () in
+ match Region.labels map r with
+ | label::_ -> Some label
+ | [] ->
+ match Region.roots map r with
+ | v::_ -> Some v.vorig_name
+ | _ -> None
+ end)
+
+let kind = Kind.get
+let name = Name.get
+let points_to region = Region.points_to (get_map ()) region
+let separated r1 r2 = Region.separated (get_map ()) r1 r2
+let included r1 r2 = Region.included (get_map ()) r1 r2
+
+let cvar var =
+ try Some (Region.cvar (get_map ()) var)
+ with Not_found -> None
+
+let field r fd =
+ try Some (Region.field (get_map ()) r fd)
+ with Not_found -> None
+
+let shift r obj =
+ try Some (Region.index (get_map ()) r (Ctypes.object_to obj))
+ with Not_found -> None
+
+let literal ~eid _ = ignore eid ; None
diff --git a/src/plugins/wp/RegionAnalysis.mli b/src/plugins/wp/RegionAnalysis.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ebce9717a1d73bcdd4abc795a6b4ba355da31d92
--- /dev/null
+++ b/src/plugins/wp/RegionAnalysis.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* 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 Analysis API for Region Memory Model --- *)
+(* -------------------------------------------------------------------------- *)
+
+include MemRegion.RegionProxy
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 1fa08a3da0a8c43ab4271d1bffa0065883883c18..c5d734ab9ab8d2f3d72efe26e281f241f087e79d 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -129,6 +129,15 @@ type update = Mstore of s_lval * term
(** {1 Memory Models} *)
(* -------------------------------------------------------------------------- *)
+module type Type =
+sig
+ type t
+ val hash : t -> int
+ val equal : t -> t -> bool
+ val compare : t -> t -> int
+ val pretty : Format.formatter -> t -> unit
+end
+
(** Memory Chunks.
The concrete memory is partionned into a vector of abstract data.
@@ -148,10 +157,7 @@ sig
val self : string
(** Chunk names, for pretty-printing. *)
- val hash : t -> int
- val equal : t -> t -> bool
- val compare : t -> t -> int
- val pretty : Format.formatter -> t -> unit
+ include Type with type t := t
val tau_of_chunk : t -> tau
(** The type of data hold in a chunk. *)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index eba61ce0010a6e6c23e66022e3ac36c98d1a7fbe..71ece40c6ca4d674f5dff4adf6bcdebbe6895073 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -384,6 +384,35 @@ let () =
cmp := compare ;
end
+(* -------------------------------------------------------------------------- *)
+(* --- Revert c_object to typ --- *)
+(* -------------------------------------------------------------------------- *)
+
+let ikinds = [
+ IBool;IChar;
+ ISChar;IUChar;
+ IInt;IUInt;
+ IShort;IUShort;
+ ILong;IULong;
+ ILongLong;IULongLong
+]
+let fkinds = [FFloat;FDouble;FLongDouble]
+
+let to_ikind iota =
+ List.find (fun ik -> c_int ik = iota) ikinds
+
+let to_fkind flt =
+ List.find (fun fk -> c_float fk = flt) fkinds
+
+let object_to = function
+ | C_int i -> TInt(to_ikind i,[])
+ | C_float f -> TFloat(to_fkind f,[])
+ | C_pointer typ -> TPtr(typ,[])
+ | C_comp comp -> TComp(comp,[])
+ | C_array { arr_element = elt ; arr_flat = None } -> TArray(elt,None,[])
+ | C_array { arr_element = elt ; arr_flat = Some { arr_size = size } } ->
+ TArray(elt,Some (Cil.integer ~loc:Location.unknown size),[])
+
(* -------------------------------------------------------------------------- *)
(* --- Accessor Utilities --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index f38d4d05826751e7eef0f5ff6ad06028eefb6764..060c3e9ffa0199e75a5102e3538b08d306dd6295 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -97,7 +97,14 @@ val c_int : ikind -> c_int
val c_float : fkind -> c_float
(** Conforms to {!Machine.theMachine} *)
+val to_ikind : c_int -> ikind
+(** @raises Not_found *)
+
+val to_fkind : c_float -> fkind
+(** @raises Not_found *)
+
val object_of : typ -> c_object
+val object_to : c_object -> typ
val is_pointer : c_object -> bool
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index b46cbeb373eb6214a4aa1d096431328d18678263..44dfa7418530fdc02756c3d23ecd077f5f3cd0c2 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -40,6 +40,7 @@
frama-c.kernel
frama-c-rtegen.core
frama-c-server.core
+ frama-c-region.core
qed why3 zarith ocamlgraph
(select wp_eva.ml from
(frama-c-eva.core -> wp_eva.enabled.ml)
diff --git a/src/plugins/wp/gui/GuiPanel.ml b/src/plugins/wp/gui/GuiPanel.ml
index 4b25d1880a95c901a759b5d4830e83c42a2b67cb..69de6705145de3f9286844b9e5312675ac3d687d 100644
--- a/src/plugins/wp/gui/GuiPanel.ml
+++ b/src/plugins/wp/gui/GuiPanel.ml
@@ -99,7 +99,7 @@ let run_and_prove
(* --- Model Panel --- *)
(* ------------------------------------------------------------------------ *)
-type memory = TREE | HOARE | TYPED | EVA | BYTES
+type memory = TREE | HOARE | TYPED | EVA | BYTES | REGION
class model_selector (main : Design.main_window_extension_points) =
let dialog = new Wpane.dialog
@@ -152,6 +152,7 @@ class model_selector (main : Design.main_window_extension_points) =
| Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
| Eva -> memory#set EVA
| Bytes -> memory#set BYTES
+ | Region -> memory#set REGION
) ;
c_byref#set (s.mvar = Ref) ;
c_ctxt#set (s.mvar = Caveat) ;
@@ -167,6 +168,7 @@ class model_selector (main : Design.main_window_extension_points) =
(if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
| EVA -> Eva
| BYTES -> Bytes
+ | REGION -> Region
in {
mheap = m ;
mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;
diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config
index 9ea351239b8b70f111befdca7dd03aebaf071a90..b70003f3d7cc939ab94a76c82cddc31ce8b727e5 100644
--- a/src/plugins/wp/tests/ptests_config
+++ b/src/plugins/wp/tests/ptests_config
@@ -1,8 +1,12 @@
-DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
-DEFAULT_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
+## General Purpose
+DEFAULT_SUITES= wp wp_manual wp_usage wp_plugin wp_gallery wp_tip wp_bts
+qualif_SUITES= wp wp_manual wp_usage wp_plugin wp_gallery wp_tip wp_bts
-qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
-qualif_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
-qualif_SUITES= why3
+## Memory Models
+DEFAULT_SUITES= wp_acsl wp_hoare wp_store wp_typed wp_bytes wp_region
+qualif_SUITES= wp_acsl wp_hoare wp_store wp_typed wp_bytes wp_region
-ce_SUITES= wp_ce
+## Specific Objectives
+qualif_SUITES= why3
+DEFAULT_SUITES= wp_ce
+ce_SUITES= wp_ce
diff --git a/src/plugins/wp/tests/wp_region/affectations.c b/src/plugins/wp/tests/wp_region/affectations.c
new file mode 100644
index 0000000000000000000000000000000000000000..601aa47036e6badcfe4b339ce47cc1141c8ecc9f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/affectations.c
@@ -0,0 +1,22 @@
+/*@ predicate pointed(int *p, int* q) = p==q || \separated(p,q);
+*/
+
+/*@
+ requires \valid(p);
+ requires \valid(q);
+ requires pointed(p,q);
+ assigns *p, *q;
+ region PQ: *p, *q;
+ behavior EQ:
+ assumes p == q;
+ ensures P: *p == \old(*p);
+ ensures Q: *q == \old(*q);
+ behavior SEP:
+ assumes p != q;
+ ensures Q: *p == \old(*p)+1;
+ ensures Q: *q == \old(*q)-1;
+*/
+void f(int* p, int* q) {
+ (*p)++;
+ (*q)--;
+}
diff --git a/src/plugins/wp/tests/wp_region/array.c b/src/plugins/wp/tests/wp_region/array.c
new file mode 100644
index 0000000000000000000000000000000000000000..825ceb18aebbc8a3421fe4e49f9b25b92c2d2051
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/array.c
@@ -0,0 +1,23 @@
+struct S {
+ int len;
+ int content[10];
+};
+/*@ predicate pointed(struct S *p, struct S * q) = p==q || \separated(p,q);
+*/
+
+
+/*@
+ requires pointed(a, b);
+ region AB: *a, *b;
+ ensures a!=b ==> a->content[2] == \old(a->content[2]) + b->content[2];
+ ensures a==b ==> a->content[2] == 2*\old(a->content[2]);
+ ensures a->content[2] == \old(a->content[2] + b->content[2]);
+ ensures a->content[4] == \old(a->content[4]);
+*/
+void add_first4(struct S * a , struct S * b )
+{
+ a->content[0] += b->content[0];
+ a->content[1] += b->content[1];
+ a->content[2] += b->content[2];
+ a->content[3] += b->content[3];
+}
diff --git a/src/plugins/wp/tests/wp_region/copy_array.c b/src/plugins/wp/tests/wp_region/copy_array.c
new file mode 100644
index 0000000000000000000000000000000000000000..4084930a6721494ad12a67b7ed940b1b9cde3112
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/copy_array.c
@@ -0,0 +1,21 @@
+
+/*@ requires n>=0 ;
+ requires \separated( a+ (0..n-1) , b + (0..n-1) );
+ ensures \forall integer k ; 0 <= k < n ==> a[k] == b[k] ;
+ assigns a[0..n-1] ;
+ region AB: a[..], b[..];
+ */
+void copy( int * a , int * b , int n )
+{
+ /*@ loop invariant Range: 0 <= i <= n ;
+ loop invariant Copy: \forall integer k ; 0 <= k < i ==> a[k] == b[k] ;
+ loop assigns i , a[0..n-1] ;
+ loop variant n - i;
+ */
+ for (int i = 0 ; i < n ; i++) {
+ L:
+ a[i] = b[i] ;
+ /*@ assert A: \forall integer k ; 0 <= k < i ==> a[k] == \at(a[k],L); */
+ /*@ assert B: \forall integer k ; 0 <= k < i ==> b[k] == \at(b[k],L); */
+ }
+}
diff --git a/src/plugins/wp/tests/wp_region/heterogenous_cast.c b/src/plugins/wp/tests/wp_region/heterogenous_cast.c
new file mode 100644
index 0000000000000000000000000000000000000000..ef9c1c52cfb71e9dc96f179ee7a16596c2b3557d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/heterogenous_cast.c
@@ -0,0 +1,10 @@
+/*@
+ assigns *p;
+@*/
+void g (int *p) {
+ *p = 42;
+ short *q = (short*) p;
+ q[0] = -1;
+ q[1] = -1;
+ //@ assert *p == -1;
+}
diff --git a/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle b/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..90b845e92270d85fecec252c6d7b263039d4c3f6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle
@@ -0,0 +1,86 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (1/2):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (2/2):
+Effect at line 21
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior EQ
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'P' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'Q' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior SEP
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = 1 + x.
+Let m = Msint32_0[p <- x_1].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Let x_4 = m[q <- x_3][p].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(Msint32_0[q]) /\ is_sint32(x_2) /\
+ is_sint32(x_3) /\ is_sint32(x_4).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, p, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, q, 4).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Pre-condition for 'SEP' *)
+ Have: q != p.
+}
+Prove: x_4 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = Msint32_0[q].
+Let m = Msint32_0[p <- 1 + x].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+ is_sint32(m[q <- x_3][p]).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, p, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, q, 4).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Pre-condition for 'SEP' *)
+ Have: q != p.
+}
+Prove: x_2 = x_1.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5872636534506a3deb2ac371e6e23d96731f49a6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
@@ -0,0 +1,91 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function add_first4
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 12) in 'add_first4':
+Let a_1 = shiftfield_F1_S_content(a).
+Let a_2 = shift_sint32(a_1, 0).
+Let x = Msint32_0[a_2].
+Let a_3 = shift_sint32(a_1, 1).
+Let x_1 = Msint32_0[a_3].
+Let a_4 = shift_sint32(a_1, 2).
+Let x_2 = Msint32_0[a_4].
+Let a_5 = shift_sint32(a_1, 3).
+Let x_3 = Msint32_0[a_5].
+Let a_6 = shiftfield_F1_S_content(b).
+Let x_4 = Msint32_0[shift_sint32(a_6, 0)].
+Let a_7 = shift_sint32(a_6, 2).
+Let m = Msint32_0[a_2 <- x + x_4].
+Let x_5 = m[shift_sint32(a_6, 1)].
+Let m_1 = m[a_3 <- x_1 + x_5].
+Let x_6 = m_1[a_7].
+Let x_7 = x_2 + x_6.
+Let m_2 = m_1[a_4 <- x_7].
+Let x_8 = m_2[shift_sint32(a_6, 3)].
+Let x_9 = m_2[a_5 <- x_3 + x_8][a_7].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_4) /\
+ is_sint32(Msint32_0[a_7]) /\ is_sint32(x_5) /\ is_sint32(x_6) /\
+ is_sint32(x_7) /\ is_sint32(x_8) /\ is_sint32(x_9).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: b != a.
+ (* Pre-condition *)
+ Have: P_pointed(a, b).
+}
+Prove: x_9 = x_6.
+
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 13) in 'add_first4':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 14) in 'add_first4':
+Let a_1 = shiftfield_F1_S_content(a).
+Let a_2 = shift_sint32(a_1, 0).
+Let x = Msint32_0[a_2].
+Let a_3 = shift_sint32(a_1, 1).
+Let x_1 = Msint32_0[a_3].
+Let a_4 = shift_sint32(a_1, 2).
+Let x_2 = Msint32_0[a_4].
+Let a_5 = shift_sint32(a_1, 3).
+Let x_3 = Msint32_0[a_5].
+Let a_6 = shiftfield_F1_S_content(b).
+Let x_4 = Msint32_0[shift_sint32(a_6, 0)].
+Let a_7 = shift_sint32(a_6, 2).
+Let x_5 = Msint32_0[a_7].
+Let m = Msint32_0[a_2 <- x + x_4].
+Let x_6 = m[shift_sint32(a_6, 1)].
+Let m_1 = m[a_3 <- x_1 + x_6].
+Let x_7 = m_1[a_7].
+Let x_8 = x_2 + x_7.
+Let m_2 = m_1[a_4 <- x_8].
+Let x_9 = m_2[shift_sint32(a_6, 3)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_4) /\
+ is_sint32(x_5) /\ is_sint32(x_6) /\ is_sint32(x_7) /\ is_sint32(x_8) /\
+ is_sint32(x_9) /\ is_sint32(m_2[a_5 <- x_3 + x_9][a_7]).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Pre-condition *)
+ Have: P_pointed(a, b).
+}
+Prove: x_7 = x_5.
+
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 15) in 'add_first4':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..75bce10e9805bbf6ad133de1cd99b97755d66e1d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
@@ -0,0 +1,213 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing copy_array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal copy_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal copy_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function copy
+------------------------------------------------------------
+
+Goal Post-condition (file copy_array.c, line 4) in 'copy':
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let x = 4 * n.
+Let a_3 = havoc(Msint32_undef_0, Msint32_0, a_1, i).
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < n).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Else *)
+ Have: n <= i.
+}
+Prove: a_3[shift_sint32(b, i_1)] = a_3[shift_sint32(a, i_1)].
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Copy' (file copy_array.c, line 11):
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
+Let x = 4 * n.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (i_1 <= i) /\ (0 <= i_1).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Then *)
+ Have: i < n.
+ (* Assertion 'A' *)
+ Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+ ((i_2 < i) -> (a_3[a_4] = a_2[a_4]))).
+ (* Assertion 'B' *)
+ Have: forall i_2 : Z. let a_4 = shift_sint32(b, i_2) in ((0 <= i_2) ->
+ ((i_2 < i) -> (a_3[a_4] = a_2[a_4]))).
+ (* Invariant 'Range' *)
+ Have: (-1) <= i.
+}
+Prove: a_3[shift_sint32(b, i_1)] = a_3[shift_sint32(a, i_1)].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Copy' (file copy_array.c, line 11):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file copy_array.c, line 10):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file copy_array.c, line 10):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'A' (file copy_array.c, line 18):
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let x = 4 * n.
+Let a_3 = shift_sint32(a, i_1).
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Then *)
+ Have: i < n.
+}
+Prove: a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]][a_3] = a_2[a_3].
+
+------------------------------------------------------------
+
+Goal Assertion 'B' (file copy_array.c, line 19):
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
+Let x = 4 * n.
+Let a_4 = shift_sint32(b, i_1).
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Then *)
+ Have: i < n.
+ (* Assertion 'A' *)
+ Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+ ((i_2 < i) -> (a_3[a_5] = a_2[a_5]))).
+}
+Prove: a_3[a_4] = a_2[a_4].
+
+------------------------------------------------------------
+
+Goal Loop assigns (file copy_array.c, line 12) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file copy_array.c, line 12) (2/3):
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file copy_array.c, line 12) (3/3):
+Effect at line 17
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let x = i - 1.
+Let a_3 = shift_sint32(a, x).
+Let a_4 = a_2[a_3 <- a_2[shift_sint32(b, x)]].
+Let x_1 = 4 * n.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0) /\ linked(alloc_0).
+ (* Goal *)
+ When: !invalid(alloc_0[P_a_24 <- 8][P_b_25 <- 8], a_3, 4).
+ (* Pre-condition *)
+ Have: separated(a_1, x_1, shift_sint32(b, 0), x_1).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 < i) /\ (i <= (1 + n)).
+ (* Invariant 'Copy' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> (((2 + i_1) <= i) ->
+ (a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
+ (* Then *)
+ Have: i <= n.
+ (* Assertion 'A' *)
+ Have: forall i_1 : Z. let a_5 = shift_sint32(a, i_1) in ((0 <= i_1) ->
+ (((2 + i_1) <= i) -> (a_4[a_5] = a_2[a_5]))).
+ (* Assertion 'B' *)
+ Have: forall i_1 : Z. let a_5 = shift_sint32(b, i_1) in ((0 <= i_1) ->
+ (((2 + i_1) <= i) -> (a_4[a_5] = a_2[a_5]))).
+ (* Invariant 'Copy' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ (a_4[shift_sint32(b, i_1)] = a_4[shift_sint32(a, i_1)]))).
+}
+Prove: included(a_3, 4, a_1, x_1).
+
+------------------------------------------------------------
+
+Goal Assigns (file copy_array.c, line 5) in 'copy':
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file copy_array.c, line 15):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file copy_array.c, line 15):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a6a8f41e11a888e1a6f98cda200b495d786522d4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
@@ -0,0 +1,41 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function g
+------------------------------------------------------------
+
+Goal Assertion (file heterogenous_cast.c, line 9):
+Let x = read_sint32(write_sint16(write_sint16(write_sint32(mem_0, p, 42),
+ shift_sint16(p, 0), -1),
+ shift_sint16(p, 1), -1), p).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (1/3):
+Effect at line 5
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (2/3):
+Effect at line 7
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (3/3):
+Effect at line 8
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..721829172e9de5998570491c9e65070ce79fac74
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/record.res.oracle
@@ -0,0 +1,76 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing record.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] record.c:22: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Post-condition (file record.c, line 12) in 'f':
+Let a = shiftfield_F1_S_g(q).
+Let a_1 = shiftfield_F1_S_f(p).
+Let x = Msint32_0[a_1].
+Let x_1 = 1 + x.
+Let m = Msint32_0[a_1 <- x_1].
+Let a_2 = shiftfield_F1_S_f(q).
+Let x_2 = m[a_2].
+Let x_3 = m[a_2 <- x_2 - 1][a_1].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_3).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ framed(mem_0) /\
+ sconst(mem_0).
+ (* Goal *)
+ When: q != p.
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Assertion *)
+ Have: read_sint32(write_sint16(write_sint16(mem_0, shift_sint16(a, 0), -1),
+ shift_sint16(a, 1), -1), a) = (-1).
+}
+Prove: x_3 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition (file record.c, line 13) in 'f':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file record.c, line 14) in 'f':
+Let a = shiftfield_F1_S_g(q).
+Let m = write_sint16(write_sint16(mem_0, shift_sint16(a, 0), -1),
+ shift_sint16(a, 1), -1).
+Let x = read_sint32(write_sint32(m, a, 0), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ framed(mem_0) /\
+ sconst(mem_0).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Assertion *)
+ Have: read_sint32(m, a) = (-1).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Assertion (file record.c, line 22):
+Let a = shiftfield_F1_S_g(q).
+Let x = read_sint32(write_sint16(write_sint16(mem_0, shift_sint16(a, 0), -1),
+ shift_sint16(a, 1), -1), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ framed(mem_0) /\
+ sconst(mem_0).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9e615df719c8f1a9aeee600b0d66b123215e5393
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
@@ -0,0 +1,70 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing swap.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal swap_aliased_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_aliased_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal swap_separated_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_separated_terminates (Cfg) (Trivial)
+------------------------------------------------------------
+ Function swap_aliased
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 20) in 'swap_aliased':
+Let x = Msint32_0[a].
+Let x_1 = Msint32_0[b].
+Let x_2 = Msint32_0[a <- x_1][b <- x][a].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0) /\ linked(alloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, a, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, b, 4).
+}
+Prove: x_2 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 21) in 'swap_aliased':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 22) in 'swap_aliased' (1/2):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 22) in 'swap_aliased' (2/2):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function swap_separated
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 5) in 'swap_separated':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 6) in 'swap_separated':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 7) in 'swap_separated' (1/2):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 7) in 'swap_separated' (2/2):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7023fcc52f23930b494cefea0d98c9ca702accf0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
@@ -0,0 +1,66 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing union.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] union.i:14: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Post-condition (file union.i, line 8) in 'f':
+Let a = shiftfield_F1_U_i(p).
+Let a_1 = shiftfield_F1_U_s(p).
+Let m = write_sint16(write_sint16(write_sint32(mem_0, a, 42),
+ shift_sint16(a_1, 0), -1), shift_sint16(a_1, 1), -1).
+Let x = read_sint32(write_sint32(m, a, 0), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+ (* Assertion *)
+ Have: read_sint32(m, a) = (-1).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Assertion (file union.i, line 14):
+Let a = shiftfield_F1_U_i(p).
+Let a_1 = shiftfield_F1_U_s(p).
+Let x = read_sint32(write_sint16(write_sint16(write_sint32(mem_0, a, 42),
+ shift_sint16(a_1, 0), -1),
+ shift_sint16(a_1, 1), -1), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (1/4):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (2/4):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (3/4):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (4/4):
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3679fc28e57abf2c942f179a5ce6933da56953e9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Valid] region_f_assigns_part1 (Qed)
+[wp] [Valid] region_f_assigns_part2 (Qed)
+[wp] [Valid] region_f_EQ_ensures_P (Qed)
+[wp] [Valid] region_f_EQ_ensures_Q (Qed)
+[wp] [Valid] region_f_SEP_ensures_Q (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_SEP_ensures_Q_2 (Alt-Ergo) (Cached)
+[wp] Proved goals: 8 / 8
+ Terminating: 1
+ Unreachable: 1
+ Qed: 4
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f 4 2 6 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8111c5b2622ed02f7378a3d8ccbf7c4e68fdbdf5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Valid] region_add_first4_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_add_first4_ensures_2 (Qed)
+[wp] [Valid] region_add_first4_ensures_3 (Alt-Ergo) (Cached)
+[wp] [Valid] region_add_first4_ensures_4 (Qed)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Qed: 2
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ add_first4 2 2 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..87119772a2ea41da0a911917fa0dd40913588d9c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
@@ -0,0 +1,32 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing copy_array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal copy_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal copy_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[wp] 13 goals scheduled
+[wp] [Valid] region_copy_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_loop_invariant_Copy_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_loop_invariant_Copy_established (Qed)
+[wp] [Valid] region_copy_loop_invariant_Range_preserved (Qed)
+[wp] [Valid] region_copy_loop_invariant_Range_established (Qed)
+[wp] [Valid] region_copy_assert_A (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_assert_B (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_loop_assigns_part1 (Qed)
+[wp] [Valid] region_copy_loop_assigns_part2 (Qed)
+[wp] [Valid] region_copy_loop_assigns_part3 (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_assigns (Qed)
+[wp] [Valid] region_copy_loop_variant_decrease (Qed)
+[wp] [Valid] region_copy_loop_variant_positive (Qed)
+[wp] Proved goals: 15 / 15
+ Terminating: 1
+ Unreachable: 1
+ Qed: 8
+ Alt-Ergo: 5
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ copy 8 5 13 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cc19d2134ab95a9f647e807f4b7d9d8d8e377ccf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[wp] 4 goals scheduled
+[wp] [Valid] region_g_assert (Alt-Ergo) (Cached)
+[wp] [Valid] region_g_assigns_part1 (Qed)
+[wp] [Valid] region_g_assigns_part2 (Qed)
+[wp] [Valid] region_g_assigns_part3 (Qed)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Qed: 3
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ g 3 1 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..166e787cf3e5c5feb8bc5d0eaf440e4162ba7ea7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/record.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing record.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] record.c:22: Warning: Annotations not analyzed
+[wp] 4 goals scheduled
+[wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_ensures_2 (Qed)
+[wp] [Valid] region_f_ensures_3 (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_assert (Alt-Ergo) (Cached)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Qed: 1
+ Alt-Ergo: 3
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f 1 3 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3f2fc25aafc08726123f2af753e77aeeb7334270
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
@@ -0,0 +1,27 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing swap.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal swap_aliased_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_aliased_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal swap_separated_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_separated_terminates (Cfg) (Trivial)
+[wp] 8 goals scheduled
+[wp] [Valid] region_swap_separated_ensures (Qed)
+[wp] [Valid] region_swap_separated_ensures_2 (Qed)
+[wp] [Valid] region_swap_separated_assigns_part1 (Qed)
+[wp] [Valid] region_swap_separated_assigns_part2 (Qed)
+[wp] [Valid] region_swap_aliased_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_swap_aliased_ensures_2 (Qed)
+[wp] [Valid] region_swap_aliased_assigns_part1 (Qed)
+[wp] [Valid] region_swap_aliased_assigns_part2 (Qed)
+[wp] Proved goals: 12 / 12
+ Terminating: 2
+ Unreachable: 2
+ Qed: 7
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ swap_separated 4 - 4 100%
+ swap_aliased 3 1 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8ac57f31244c3cae6924ce5daae5907e69300be5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
@@ -0,0 +1,23 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing union.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] union.i:14: Warning: Annotations not analyzed
+[wp] 6 goals scheduled
+[wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_assert (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_assigns_part1 (Qed)
+[wp] [Valid] region_f_assigns_part2 (Qed)
+[wp] [Valid] region_f_assigns_part3 (Qed)
+[wp] [Valid] region_f_assigns_part4 (Qed)
+[wp] Proved goals: 8 / 8
+ Terminating: 1
+ Unreachable: 1
+ Qed: 4
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f 4 2 6 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/record.c b/src/plugins/wp/tests/wp_region/record.c
new file mode 100644
index 0000000000000000000000000000000000000000..10da25acbd0baf51c500b5a055a0d77daa214ead
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/record.c
@@ -0,0 +1,24 @@
+struct S {
+ int f;
+ int g;
+};
+
+/*@ predicate pointed(struct S *p, struct S * q) = p==q || \separated(p,q);
+*/
+
+
+/*@ requires pointed(p,q);
+ region PQf: p->f, q->f;
+ ensures p != q ==> p->f == \old(p->f) + 1;
+ ensures p == q ==> p->f == \old(p->f);
+ ensures q->g == 0;
+@*/
+void f (struct S *p, struct S *q) {
+ (p->f)++;
+ (q->f)--;
+ short *r = &(q->g);
+ r[0] = -1;
+ r[1] = -1;
+ //@ assert q->g == -1;
+ (q->g)++;
+}
diff --git a/src/plugins/wp/tests/wp_region/swap.i b/src/plugins/wp/tests/wp_region/swap.i
new file mode 100644
index 0000000000000000000000000000000000000000..04816ea5fd84319d9dad1009e3cbdb643cea9272
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/swap.i
@@ -0,0 +1,29 @@
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region A: *a, B: *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_separated(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
+
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region R: *a, *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_aliased(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..87e39087d8a41ddbc3e6ef2a3acb8dd436efb5c0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -0,0 +1 @@
+OPT: -wp-model region
diff --git a/src/plugins/wp/tests/wp_region/test_config_qualif b/src/plugins/wp/tests/wp_region/test_config_qualif
new file mode 100644
index 0000000000000000000000000000000000000000..87e39087d8a41ddbc3e6ef2a3acb8dd436efb5c0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/test_config_qualif
@@ -0,0 +1 @@
+OPT: -wp-model region
diff --git a/src/plugins/wp/tests/wp_region/union.i b/src/plugins/wp/tests/wp_region/union.i
new file mode 100644
index 0000000000000000000000000000000000000000..edc24141817bd90b9d349ba38f7810d8506ee736
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/union.i
@@ -0,0 +1,16 @@
+union U {
+ short s[2];
+ int i;
+};
+
+/*@
+ assigns *p;
+ ensures p->i == 0;
+@*/
+void f (union U *p) {
+ p->i = 42;
+ p->s[0] = -1;
+ p->s[1] = -1;
+ //@ assert p->i == -1;
+ (p->i)++;
+}