From 96e77350201cfb75d14b6da7412b496efe1ab084 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 7 Oct 2024 17:09:25 +0200
Subject: [PATCH] [wp/region] check size for single type
---
src/plugins/region/Region.ml | 1 +
src/plugins/region/Region.mli | 2 ++
src/plugins/region/memory.ml | 5 ++++-
src/plugins/region/memory.mli | 7 ++++---
src/plugins/wp/RegionAnalysis.ml | 10 +++++-----
5 files changed, 16 insertions(+), 9 deletions(-)
diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index 4c912d7a61b..f236171a302 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -36,6 +36,7 @@ let nodes = Memory.nodes
let equal = Memory.equal
let included = Memory.included
let separated = Memory.separated
+let size = Memory.size
let roots = Memory.roots
let labels = Memory.labels
let reads = Memory.reads
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index baedc6b4030..c17d49d5319 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -74,6 +74,8 @@ val nodes : map -> node list -> node list
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
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 048e7ed6ee1..bc2916eaa1e 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -353,7 +353,10 @@ let regions map =
iter map (fun r -> pool := region map r :: !pool) ;
List.rev !pool
-let parents (m: map) (r: node) =
+let size (m: map) (r: node) =
+ sizeof (Ufind.get m.store r).clayout
+
+ let parents (m: map) (r: node) =
nodes m (Ufind.get m.store r).cparents
let roots (m: map) (r: node) =
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 4e8f5c4da4b..5485a5c974f 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -70,12 +70,13 @@ val equal : map -> node -> node -> bool
val node : map -> node -> node
val nodes : map -> node list -> node list
-val iter : 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 -> ?size:int -> ?ptr:node -> ?pointed:node -> unit -> node
val add_root : map -> Cil_types.varinfo -> node
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index 53cbfdca051..ec894b8dfe1 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -46,11 +46,10 @@ struct
let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
end
-let types r =
+let types map r =
let module Tset = Cil_datatype.Typ.Set in
let pool = ref Tset.empty in
let add ty = pool := Tset.add ty !pool in
- let map = get_map () in
List.iter add @@ Region.reads map r ;
List.iter add @@ Region.writes map r ;
List.iter add @@ Region.shifts map r ;
@@ -63,10 +62,11 @@ module Kind = WpContext.Generator(Type)
type key = region
type data = MemRegion.kind
let name = "Wp.RegionAnalysis.R"
- let compile region =
+ let compile r =
let open MemRegion in
- match types region with
- | [ty] ->
+ let map = get_map () in
+ match types map r with
+ | [ty] when Cil.bitsSizeOf ty >= Region.size map r ->
begin
match Ctypes.object_of ty with
| C_int i -> Many (Int i)
--
GitLab