From 823d1fc8407f25fb3a03461b628d897178b2ef0c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 10 Jun 2024 16:37:20 +0200
Subject: [PATCH] [region] localize l-values and expressions
---
.../src/frama-c/plugins/region/api/index.ts | 26 +++++-
src/plugins/region/code.ml | 9 +--
src/plugins/region/code.mli | 4 +-
src/plugins/region/memory.ml | 79 ++++++++++++++++++-
src/plugins/region/memory.mli | 21 ++++-
src/plugins/region/services.ml | 49 ++++++++----
src/plugins/region/services.mli | 3 -
7 files changed, 161 insertions(+), 30 deletions(-)
diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
index 942053971ed..a0b2fef8928 100644
--- a/ivette/src/frama-c/plugins/region/api/index.ts
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -162,14 +162,32 @@ const regions_internal: Server.GetRequest<decl,region[]> = {
/** Compute regions for the given declaration */
export const regions: Server.GetRequest<decl,region[]>= regions_internal;
-const regionsAt_internal: Server.GetRequest<marker,region[]> = {
+const regionsAt_internal: Server.GetRequest<[ marker, boolean ],region[]> = {
kind: Server.RqKind.GET,
name: 'plugins.region.regionsAt',
- input: jMarker,
+ input: Json.jPair( jMarker, Json.jBoolean,),
output: Json.jArray(jRegion),
signals: [ { name: 'plugins.region.updated' } ],
};
-/** Compute regions at the given marker position */
-export const regionsAt: Server.GetRequest<marker,region[]>= regionsAt_internal;
+/** Compute regions at the given marker */
+export const regionsAt: Server.GetRequest<[ marker, boolean ],region[]>= regionsAt_internal;
+
+const localize_internal: Server.GetRequest<
+ [ marker, boolean ],
+ node |
+ undefined
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.region.localize',
+ input: Json.jPair( jMarker, Json.jBoolean,),
+ output: Json.jOption(jNode),
+ signals: [ { name: 'plugins.region.updated' } ],
+};
+/** Localize in the local (true) or global map (false) */
+export const localize: Server.GetRequest<
+ [ marker, boolean ],
+ node |
+ undefined
+ >= localize_internal;
/* ------------------------------------- */
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index c7f3e43ccf4..b0231ead15f 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -164,10 +164,9 @@ let instr (m:map) (s:stmt) (instr:instr) =
type rmap = Memory.map Stmt.Map.t ref
let store rmap m s =
- rmap := Stmt.Map.add s (Memory.copy m) !rmap
+ rmap := Stmt.Map.add s (Memory.copy ~locked:true m) !rmap
let rec stmt (r:rmap) (m:map) (s:stmt) =
-
let annots = Annotations.code_annot s in
if annots <> [] then
Options.warning ~source:(fst @@ Stmt.loc s)
@@ -218,8 +217,8 @@ type domain = {
spec : map Property.Map.t ;
}
-let domain kf =
- let m = Memory.create () in
+let domain ?global kf =
+ let m = match global with Some g -> g | None -> Memory.create () in
let r = ref Stmt.Map.empty in
begin
try
@@ -227,7 +226,7 @@ let domain kf =
block r m fundec.sbody ;
with Kernel_function.No_Definition -> ()
end ; {
- map = m ;
+ map = Memory.copy ~locked:true m ;
body = !r ;
spec = Property.Map.empty ;
}
diff --git a/src/plugins/region/code.mli b/src/plugins/region/code.mli
index 1ae6e52fc2c..fb4df16f1af 100644
--- a/src/plugins/region/code.mli
+++ b/src/plugins/region/code.mli
@@ -29,10 +29,12 @@ val exp : map -> stmt -> exp -> node option
val instr : map -> stmt -> instr -> unit
val stmt : map Stmt.Map.t ref -> map -> stmt -> unit
+(** All the provided maps are locked. *)
type domain = {
map : map ;
body : map Stmt.Map.t ;
spec : map Property.Map.t ;
}
-val domain : kernel_function -> domain
+(** The global map, if provided, is used as an accumulator. *)
+val domain : ?global:map -> kernel_function -> domain
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 2ac7d0d25ef..8ac0519149b 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -51,6 +51,7 @@ type rg = node Ranges.range
type map = {
store: chunk Ufind.store ;
+ mutable locked: bool ;
mutable index: node Vmap.t ;
}
@@ -70,6 +71,12 @@ let types (m : chunk) : typ list =
Access.Set.iter add m.cwrites ;
Typ.Set.elements !pool
+let failwith_locked m fn =
+ if m.locked then raise (Invalid_argument fn)
+
+let lock m = m.locked <- true
+let unlock m = m.locked <- false
+
(* -------------------------------------------------------------------------- *)
(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
@@ -110,11 +117,13 @@ let pp_chunk fmt (n: node) (m: chunk) =
(* -------------------------------------------------------------------------- *)
let create () = {
+ locked = false ;
store = Ufind.new_store () ;
index = Vmap.empty ;
}
-let copy m = {
+let copy ?locked m = {
+ locked = (match locked with None -> m.locked | Some l -> l) ;
store = Ufind.copy m.store ;
index = m.index ;
}
@@ -150,6 +159,7 @@ let get map node =
(* -------------------------------------------------------------------------- *)
let cell (m: map) ?size ?ptr ?root () =
+ failwith_locked m "Region.Memory.cell" ;
let clayout = match size, ptr with
| None, None -> Blob
| None, Some _ -> Cell(Cil.bitsSizeOf Cil.voidPtrType,ptr)
@@ -162,6 +172,7 @@ let update (m: map) (n: node) (f: chunk -> chunk) =
Ufind.set m.store n (f r)
let range (m: map) ~size ~offset ~length ~data : node =
+ failwith_locked m "Region.Memory.range" ;
let last = offset + length in
if not (0 <= offset && offset < last && last <= size) then
raise (Invalid_argument "Region.Memory.range") ;
@@ -171,6 +182,7 @@ let range (m: map) ~size ~offset ~length ~data : node =
let root (m: map) v =
try Vmap.find v m.index with Not_found ->
+ failwith_locked m "Region.Memory.root" ;
let n = cell m ~root:v () in
m.index <- Vmap.add v n m.index ; n
@@ -262,6 +274,11 @@ let iter (m:map) (f: region -> unit) =
let h = Hashtbl.create 0 in
Vmap.iter (fun _x n -> walk h m f n) m.index
+let regions map =
+ let pool = ref [] in
+ iter map (fun r -> pool := r :: !pool) ;
+ List.rev !pool
+
(* -------------------------------------------------------------------------- *)
(* --- Merge --- *)
(* -------------------------------------------------------------------------- *)
@@ -344,6 +361,7 @@ let do_merge (m: map) (q: queue) (a: node) (b: node): unit =
end
let merge (m: map) (a: node) (b: node) : node =
+ failwith_locked m "Region.Memory.merge" ;
if Ufind.eq m.store a b then Ufind.find m.store a else
let q = Queue.create () in
do_merge m q a b ;
@@ -363,21 +381,80 @@ let access (m:map) (a:node) (ty: typ) =
if sr <> size then ignore (merge m a (cell m ~size ()))
let points_to (m: map) (a: node) (b : node) =
+ failwith_locked m "Region.Memory.points_to" ;
ignore @@ merge m a @@ cell m ~ptr:b ()
let read (m: map) (a: node) from =
+ 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 } ;
access m a (Access.typeof from)
let write (m: map) (a: node) from =
+ 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 } ;
access m a (Access.typeof from)
let shift (m: map) (a: node) from =
+ 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 }
(* no access *)
(* -------------------------------------------------------------------------- *)
+(* --- Lookup ---- *)
+(* -------------------------------------------------------------------------- *)
+
+let cranges m r =
+ let rg = Ufind.get m.store r in
+ match rg.clayout with
+ | Blob | Cell _ -> raise Not_found
+ | Compound(s,rgs) -> s, rgs
+
+let cpointed m r =
+ let rg = Ufind.get m.store r in
+ match rg.clayout with
+ | Blob | Compound _ | Cell(_,None) -> None
+ | Cell(_,Some r) -> Some (Ufind.find m.store r)
+
+let rec lval (m: map) (lv: lval) : node =
+ let h = host m (fst lv) in
+ offset m h (snd lv)
+
+and host (m: map) (h: lhost) : node =
+ match h with
+ | Var x -> Ufind.find m.store @@ Vmap.find x m.index
+ | Mem e ->
+ match exp m e with
+ | None -> raise Not_found
+ | Some r -> r
+
+and offset (m: map) (r: node) (ofs: offset) : node =
+ match ofs with
+ | NoOffset -> Ufind.find m.store r
+ | Field (fd, ofs) ->
+ let _, rgs = cranges m r in
+ let (p,w) = Cil.fieldBitsOffset fd in
+ let rg = Ranges.find p rgs in
+ if rg.offset <= p && p+w <= rg.offset + rg.length then
+ offset m rg.data ofs
+ else raise Not_found
+ | Index (_, ofs) ->
+ let s, rgs = cranges m r in
+ match rgs with
+ | R [rg] when rg.offset = 0 && rg.length = s ->
+ offset m rg.data ofs
+ | _ -> raise Not_found
+
+and exp (m: map) (e: exp) : node option =
+ match e.enode with
+ | Const _
+ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> None
+ | Lval lv -> cpointed m @@ lval m lv
+ | AddrOf lv | StartOf lv -> Some (lval m lv)
+ | CastE(_, e) -> exp m e
+ | BinOp((PlusPI|MinusPI),p,_,_) -> exp m p
+ | UnOp (_, _, _) | BinOp (_, _, _, _) -> None
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index f1a3bc95e8c..d31f9bcfa71 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -50,8 +50,17 @@ val pp_node : Format.formatter -> node -> unit
val pp_range : Format.formatter -> range -> unit
val pp_region : Format.formatter -> region -> unit
+(** Initially unlocked. *)
val create : unit -> map
-val copy : map -> map
+
+(** Default locked status is inherited from the copied map. *)
+val copy : ?locked:bool -> map -> map
+
+(** Lock the map. No more access nor merge can be added into the map. *)
+val lock : map -> unit
+
+(** Unlock the map. *)
+val unlock : map -> unit
val root : map -> Cil_types.varinfo -> node
val cell : map -> ?size:int -> ?ptr:node -> ?root:varinfo -> unit -> node
@@ -61,11 +70,19 @@ val id : node -> int
val forge : int -> node
val node : map -> node -> node
val nodes : map -> node list -> node list
-val region : map -> node -> region
+
val iter : map -> (region -> unit) -> unit
+val region : map -> node -> region
+val regions : map -> region list
val merge : map -> node -> node -> node
val read : map -> node -> Access.acs -> unit
val write : map -> node -> Access.acs -> unit
val shift : map -> node -> Access.acs -> unit
val points_to : map -> node -> node -> unit
+
+(** @raise Not_found *)
+val lval : map -> lval -> node
+
+(** @raise Not_found *)
+val exp : map -> exp -> node option
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 38550cc6615..d92e5850987 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -176,20 +176,27 @@ module Regions = Data.Jlist(Region)
(* --- Server API --- *)
(* -------------------------------------------------------------------------- *)
-let regions map =
- let pool = ref [] in
- Memory.iter map (fun r -> pool := r :: !pool) ;
- List.rev !pool
-
-let map_of_localizable (loc : Printer_tag.localizable) =
+let map_of_localizable ~local (loc : Printer_tag.localizable) =
let open Printer_tag in
match kf_of_localizable loc with
| None -> raise Not_found
| Some kf ->
let domain = Analysis.find kf in
- match ki_of_localizable loc with
- | Kglobal -> domain.map
- | Kstmt s -> Stmt.Map.find s domain.body
+ if local then
+ match ki_of_localizable loc with
+ | Kglobal -> domain.map
+ | Kstmt s -> Stmt.Map.find s domain.body
+ else domain.map
+
+let region_of_localizable (m: Memory.map) (loc: Printer_tag.localizable) =
+ try
+ match loc with
+ | PExp(_,_,e) -> Memory.exp m e
+ | PLval(_,_,lv) -> Some (Memory.lval m lv)
+ | PVDecl(_,_,x) -> Some (Memory.lval m (Var x,NoOffset))
+ | PStmt _ | PStmtStart _
+ | PTermLval _ | PGlobal _ | PIP _ | PType _ -> None
+ with Not_found -> None
let map_of_declaration (decl : Printer_tag.declaration) =
match decl with
@@ -217,20 +224,34 @@ let () =
~output:(module Regions)
~signals:[signal]
begin fun decl ->
- try regions @@ map_of_declaration decl
+ try Memory.regions @@ map_of_declaration decl
with Not_found -> []
end
let () =
Request.register
~package ~kind:`GET ~name:"regionsAt"
- ~descr:(Md.plain "Compute regions at the given marker position")
- ~input:(module Kernel_ast.Marker)
+ ~descr:(Md.plain "Compute regions at the given marker")
+ ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
~output:(module Regions)
~signals:[signal]
- begin fun loc ->
- try regions @@ map_of_localizable loc
+ begin fun (loc,local) ->
+ try Memory.regions @@ map_of_localizable ~local loc
with Not_found -> []
end
+let () =
+ Request.register
+ ~package ~kind:`GET ~name:"localize"
+ ~descr:(Md.plain "Localize in the local (true) or global map (false)")
+ ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+ ~output:(module NodeOpt)
+ ~signals:[signal]
+ begin fun (loc,local) ->
+ try
+ let map = map_of_localizable ~local loc in
+ region_of_localizable map loc
+ with Not_found -> None
+ end
+
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/services.mli b/src/plugins/region/services.mli
index d694a69647e..2507b13f97d 100644
--- a/src/plugins/region/services.mli
+++ b/src/plugins/region/services.mli
@@ -28,6 +28,3 @@ val package : Package.package
module Node : Data.S with type t = Memory.node
module Range : Output with type t = Memory.range
module Region : Output with type t = Memory.region
-
-(** @raises Not_found *)
-val map_of_localizable : Printer_tag.localizable -> Memory.map
--
GitLab