From ca39f059d00a22d1e95b75cca48fd36861fc3468 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 12 Jun 2024 08:54:26 +0200
Subject: [PATCH] [region] aliasing annotations & region labels
---
.../src/frama-c/plugins/region/api/index.ts | 20 +--
ivette/src/frama-c/plugins/region/memory.tsx | 17 ++-
src/plugins/region/annot.ml | 128 +++++++++---------
src/plugins/region/annot.mli | 32 ++---
src/plugins/region/code.ml | 71 ++++++----
src/plugins/region/logic.ml | 55 ++++++++
src/plugins/region/logic.mli | 27 ++++
src/plugins/region/memory.ml | 125 ++++++++++++-----
src/plugins/region/memory.mli | 19 ++-
src/plugins/region/services.ml | 5 +
10 files changed, 333 insertions(+), 166 deletions(-)
create mode 100644 src/plugins/region/logic.ml
create mode 100644 src/plugins/region/logic.mli
diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
index 122c71d9f67..8d4530d2f54 100644
--- a/ivette/src/frama-c/plugins/region/api/index.ts
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -92,15 +92,16 @@ export const rangeDefault: range =
{ offset: 0, length: 0, cells: 0, data: nodeDefault };
export type region =
- { node: node, roots: string[], parents: node[], sizeof: number,
- ranges: range[], pointed?: node, reads: boolean, writes: boolean,
- bytes: boolean, label: string, title: string };
+ { node: node, roots: string[], labels: string[], parents: node[],
+ sizeof: number, ranges: range[], pointed?: node, reads: boolean,
+ writes: boolean, bytes: boolean, label: string, title: string };
/** Decoder for `region` */
export const jRegion: Json.Decoder<region> =
Json.jObject({
node: jNode,
roots: Json.jArray(Json.jString),
+ labels: Json.jArray(Json.jString),
parents: Json.jArray(jNode),
sizeof: Json.jNumber,
ranges: Json.jArray(jRange),
@@ -115,11 +116,12 @@ export const jRegion: Json.Decoder<region> =
/** Natural order for `region` */
export const byRegion: Compare.Order<region> =
Compare.byFields
- <{ node: node, roots: string[], parents: node[], sizeof: number,
- ranges: range[], pointed?: node, reads: boolean, writes: boolean,
- bytes: boolean, label: string, title: string }>({
+ <{ node: node, roots: string[], labels: string[], parents: node[],
+ sizeof: number, ranges: range[], pointed?: node, reads: boolean,
+ writes: boolean, bytes: boolean, label: string, title: string }>({
node: byNode,
roots: Compare.array(Compare.alpha),
+ labels: Compare.array(Compare.alpha),
parents: Compare.array(byNode),
sizeof: Compare.number,
ranges: Compare.array(byRange),
@@ -133,9 +135,9 @@ export const byRegion: Compare.Order<region> =
/** Default value for `region` */
export const regionDefault: region =
- { node: nodeDefault, roots: [], parents: [], sizeof: 0, ranges: [],
- pointed: undefined, reads: false, writes: false, bytes: false, label: '',
- title: '' };
+ { node: nodeDefault, roots: [], labels: [], parents: [], sizeof: 0,
+ ranges: [], pointed: undefined, reads: false, writes: false,
+ bytes: false, label: '', title: '' };
/** Region Analysis Updated */
export const updated: Server.Signal = {
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
index 4e011695b5d..29c9b5a6341 100644
--- a/ivette/src/frama-c/plugins/region/memory.tsx
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -55,8 +55,8 @@ function makeRecord(
}
interface Diagram {
- nodes: Dot.Node[] ;
- edges: Dot.Edge[] ;
+ nodes: Dot.Node[];
+ edges: Dot.Edge[];
}
function makeDiagram(regions: readonly Region.region[]): Diagram {
@@ -76,8 +76,17 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
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' };
+ r.labels.forEach(a => {
+ const lid = `L${a}`;
+ nodes.push({ ...L, id: lid, label: `${a}:` });
+ edges.push({ source: lid, target: id });
+ });
// --- Roots
- const R: Dot.Node = { id: '', shape: 'cds', font: 'mono', color: 'blue' };
+ const R: Dot.Node =
+ { id: '', shape: 'cds', font: 'mono' };
r.roots.forEach(x => {
const xid = `X${x}`;
nodes.push({ ...R, id: xid, label: x });
@@ -106,7 +115,7 @@ export interface MemoryViewProps {
}
export function MemoryView(props: MemoryViewProps): JSX.Element {
- const { regions=[], label, node } = props;
+ const { regions = [], label, node } = props;
const diagram = React.useMemo(() => makeDiagram(regions), [regions]);
if (label && node) addSelected(diagram, label, node);
return <Dot.Diagram {...diagram} />;
diff --git a/src/plugins/region/annot.ml b/src/plugins/region/annot.ml
index fb873e3ee84..746ebcffad8 100644
--- a/src/plugins/region/annot.ml
+++ b/src/plugins/region/annot.ml
@@ -28,25 +28,25 @@ open Cil_datatype
(* --- Region Specifications --- *)
(* -------------------------------------------------------------------------- *)
-type lpath = {
+type path = {
loc : location ;
- ltype : typ ;
- lnode : lnode ;
+ typ : typ ;
+ step: step ;
}
-and lnode =
- | L_var of varinfo
- | L_region of string
- | L_addr of lpath
- | L_star of lpath
- | L_index of lpath
- | L_shift of lpath
- | L_field of lpath * fieldinfo
- | L_cast of typ * lpath
+and step =
+ | Var of varinfo
+ | Region of string
+ | AddrOf of path
+ | Star of path
+ | Index of path
+ | Shift of path
+ | Field of path * fieldinfo
+ | Cast of typ * path
type region = {
rname: string option ;
- rpath: lpath list ;
+ rpath: path list ;
}
(* -------------------------------------------------------------------------- *)
@@ -54,29 +54,29 @@ type region = {
(* -------------------------------------------------------------------------- *)
let atomic = function
- | L_var _ | L_region _ | L_addr _ | L_star _ | L_index _ | L_field _ -> true
- | L_shift _ | L_cast _ -> false
-
-let rec pp_lnode fmt = function
- | L_var x -> Varinfo.pretty fmt x
- | L_region a -> Format.pp_print_string fmt a
- | L_field(p,f) -> pfield p f fmt
- | L_index a -> Format.fprintf fmt "%a[..]" pp_latom a
- | L_shift a -> Format.fprintf fmt "%a+(..)" pp_latom a
- | L_star a -> Format.fprintf fmt "*%a" pp_latom a
- | L_addr a -> Format.fprintf fmt "&%a" pp_latom a
- | L_cast(t,a) -> Format.fprintf fmt "(%a)@,%a" Typ.pretty t pp_latom a
+ | Var _ | Region _ | AddrOf _ | Star _ | Index _ | Field _ -> true
+ | Shift _ | Cast _ -> false
+
+let rec pp_step fmt = function
+ | Var x -> Varinfo.pretty fmt x
+ | Region a -> Format.pp_print_string fmt a
+ | Field(p,f) -> pfield p f fmt
+ | Index a -> Format.fprintf fmt "%a[..]" pp_atom a
+ | Shift a -> Format.fprintf fmt "%a+(..)" pp_atom a
+ | Star a -> Format.fprintf fmt "*%a" pp_atom a
+ | AddrOf a -> Format.fprintf fmt "&%a" pp_atom a
+ | Cast(t,a) -> Format.fprintf fmt "(%a)@,%a" Typ.pretty t pp_atom a
and pfield p fd fmt =
- match p.lnode with
- | L_star p -> Format.fprintf fmt "%a->%a" pp_latom p Fieldinfo.pretty fd
- | _ -> Format.fprintf fmt "%a.%a" pp_latom p Fieldinfo.pretty fd
+ match p.step with
+ | Star p -> Format.fprintf fmt "%a->%a" pp_atom p Fieldinfo.pretty fd
+ | _ -> Format.fprintf fmt "%a.%a" pp_atom p Fieldinfo.pretty fd
-and pp_latom fmt a =
- if atomic a.lnode then pp_lnode fmt a.lnode
- else Format.fprintf fmt "@[<hov 2>(%a)@]" pp_lnode a.lnode
+and pp_atom fmt a =
+ if atomic a.step then pp_step fmt a.step
+ else Format.fprintf fmt "@[<hov 2>(%a)@]" pp_step a.step
-and pp_lpath fmt a = pp_lnode fmt a.lnode
+and pp_path fmt a = pp_step fmt a.step
let pp_named fmt = function None -> () | Some a -> Format.fprintf fmt "%s: " a
@@ -85,10 +85,10 @@ let pp_region fmt r =
| [] -> Format.pp_print_string fmt "\null"
| p::ps ->
begin
- Format.fprintf fmt "@[<hov 2>]" ;
+ Format.fprintf fmt "@[<hov 2>" ;
pp_named fmt r.rname ;
- pp_lpath fmt p ;
- List.iter (Format.fprintf fmt ",@ %a" pp_lpath) ps ;
+ pp_path fmt p ;
+ List.iter (Format.fprintf fmt ",@ %a" pp_path) ps ;
Format.fprintf fmt "@]" ;
end
@@ -96,7 +96,7 @@ let pp_regions fmt = function
| [] -> Format.pp_print_string fmt "\null"
| r::rs ->
begin
- Format.fprintf fmt "@[<hv 0>]" ;
+ Format.fprintf fmt "@[<hv 0>" ;
pp_region fmt r ;
List.iter (Format.fprintf fmt ",@ %a" pp_region) rs ;
Format.fprintf fmt "@]" ;
@@ -109,7 +109,7 @@ let pp_regions fmt = function
type env = {
context: Logic_typing.typing_context ;
mutable named: string option ;
- mutable paths: lpath list ;
+ mutable paths: path list ;
mutable specs: region list ;
}
@@ -123,9 +123,9 @@ let getCompoundType env ~loc typ =
let parse_name (env:env) ~loc x =
try
match env.context.find_var x with
- | { lv_origin = Some v } -> { loc ; ltype = v.vtype ; lnode = L_var v }
+ | { lv_origin = Some v } -> { loc ; typ = v.vtype ; step = Var v }
| _ -> error env ~loc "Variable '%s' is not a C-variable" x
- with Not_found -> { loc ; ltype = TVoid [] ; lnode = L_region x }
+ with Not_found -> { loc ; typ = TVoid [] ; step = Region x }
let parse_field env ~loc comp f =
try List.find (fun fd -> fd.fname = f) (Option.value ~default:[] comp.cfields)
@@ -138,7 +138,7 @@ let parse_lrange (env: env) (e : lexpr) =
| _ ->
error env ~loc:e.lexpr_loc "Unexpected index (use unspecified range only)"
-let parse_ltype env ~loc t =
+let parse_typ env ~loc t =
let open Logic_typing in
let g = env.context in
let t = g.logic_type g loc g.pre_state t in
@@ -152,52 +152,52 @@ let rec parse_lpath (env:env) (e: lexpr) =
| PLvar x -> parse_name env ~loc x
| PLunop( Ustar , p ) ->
let lv = parse_lpath env p in
- if Cil.isPointerType lv.ltype then
- let te = Cil.typeOf_pointed lv.ltype in
- { loc ; lnode = L_star lv ; ltype = te }
+ if Cil.isPointerType lv.typ then
+ let te = Cil.typeOf_pointed lv.typ in
+ { loc ; step = Star lv ; typ = te }
else
error env ~loc "Pointer-type expected for operator '&'"
| PLunop( Uamp , p ) ->
let lv = parse_lpath env p in
- let ltype = TPtr( lv.ltype , [] ) in
- { loc ; lnode = L_addr lv ; ltype }
+ let typ = TPtr( lv.typ , [] ) in
+ { loc ; step = AddrOf lv ; typ }
| PLbinop( p , Badd , rg ) ->
parse_lrange env rg ;
- let { ltype } as lv = parse_lpath env p in
- if Cil.isPointerType ltype then
- { loc ; lnode = L_shift lv ; ltype = ltype }
+ let { typ } as lv = parse_lpath env p in
+ if Cil.isPointerType typ then
+ { loc ; step = Shift lv ; typ = typ }
else
- if Cil.isArrayType ltype then
- let te = Cil.typeOf_array_elem ltype in
- { loc ; lnode = L_shift lv ; ltype = TPtr(te,[]) }
+ if Cil.isArrayType typ then
+ let te = Cil.typeOf_array_elem typ in
+ { loc ; step = Shift lv ; typ = TPtr(te,[]) }
else
error env ~loc "Pointer-type expected for operator '+'"
| PLdot( p , f ) ->
let lv = parse_lpath env p in
- let comp = getCompoundType env ~loc:lv.loc lv.ltype in
+ let comp = getCompoundType env ~loc:lv.loc lv.typ in
let fd = parse_field env ~loc comp f in
- { loc ; lnode = L_field(lv,fd) ; ltype = fd.ftype }
+ { loc ; step = Field(lv,fd) ; typ = fd.ftype }
| PLarrow( p , f ) ->
let sp = { lexpr_loc = loc ; lexpr_node = PLunop(Ustar,p) } in
let pf = { lexpr_loc = loc ; lexpr_node = PLdot(sp,f) } in
parse_lpath env pf
| PLarrget( p , rg ) ->
parse_lrange env rg ;
- let { ltype } as lv = parse_lpath env p in
- if Cil.isPointerType ltype then
- let pointed = Cil.typeOf_pointed ltype in
- let ls = { loc ; lnode = L_shift lv ; ltype } in
- { loc ; lnode = L_star ls ; ltype = pointed }
+ let { typ } as lv = parse_lpath env p in
+ if Cil.isPointerType typ then
+ let pointed = Cil.typeOf_pointed typ in
+ let ls = { loc ; step = Shift lv ; typ } in
+ { loc ; step = Star ls ; typ = pointed }
else
- if Cil.isArrayType ltype then
- let elt = Cil.typeOf_array_elem ltype in
- { loc ; lnode = L_index lv ; ltype = elt }
+ if Cil.isArrayType typ then
+ let elt = Cil.typeOf_array_elem typ in
+ { loc ; step = Index lv ; typ = elt }
else
error env ~loc:lv.loc "Pointer or array type expected"
| PLcast( t , a ) ->
let lv = parse_lpath env a in
- let ty = parse_ltype env ~loc t in
- { loc ; lnode = L_cast(ty,lv) ; ltype = ty }
+ let ty = parse_typ env ~loc t in
+ { loc ; step = Cast(ty,lv) ; typ = ty }
| _ ->
error env ~loc "Unexpected expression for region spec"
@@ -255,7 +255,7 @@ let () =
Acsl_extension.register_behavior
~plugin:"region" "region" typecheck ~printer false ;
Acsl_extension.register_code_annot
- ~plugin:"region" "region" typecheck ~printer false ;
+ ~plugin:"region" "alias" typecheck ~printer false ;
end
diff --git a/src/plugins/region/annot.mli b/src/plugins/region/annot.mli
index e460c86cb14..d820c8a741d 100644
--- a/src/plugins/region/annot.mli
+++ b/src/plugins/region/annot.mli
@@ -22,30 +22,30 @@
open Cil_types
-type lpath = {
+type path = {
loc : location ;
- ltype : typ ;
- lnode : lnode ;
+ typ : typ ;
+ step: step ;
}
-and lnode =
- | L_var of varinfo
- | L_region of string
- | L_addr of lpath
- | L_star of lpath
- | L_index of lpath
- | L_shift of lpath
- | L_field of lpath * fieldinfo
- | L_cast of typ * lpath
+and step =
+ | Var of varinfo
+ | Region of string
+ | AddrOf of path
+ | Star of path
+ | Index of path
+ | Shift of path
+ | Field of path * fieldinfo
+ | Cast of typ * path
type region = {
rname: string option ;
- rpath: lpath list ;
+ rpath: path list ;
}
-val pp_lnode : Format.formatter -> lnode -> unit
-val pp_latom : Format.formatter -> lpath -> unit
-val pp_lpath : Format.formatter -> lpath -> unit
+val pp_step : Format.formatter -> step -> unit
+val pp_atom : Format.formatter -> path -> unit
+val pp_path : Format.formatter -> path -> unit
val pp_region : Format.formatter -> region -> unit
val pp_regions : Format.formatter -> region list -> unit
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index b0231ead15f..26a8e0de778 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -24,11 +24,6 @@ open Cil_types
open Cil_datatype
open Memory
-let typeof_array_elt ty =
- match Cil.unrollType ty with
- | TArray(te,_,_) -> te
- | _ -> Cil.voidType
-
(* -------------------------------------------------------------------------- *)
(* --- L-Values & Expressions --- *)
(* -------------------------------------------------------------------------- *)
@@ -38,25 +33,17 @@ let rec lval (m:map) (s:stmt) (lv:lval) : node =
loffset m s (lhost m s h) (Cil.typeOfLhost h) (snd lv)
and lhost (m:map) (s:stmt) = function
- | Var x -> Memory.root m x
+ | Var x -> Memory.add_root m x
| Mem e -> pointer m s e
and loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
| NoOffset -> r
| Field(fd,ofs) ->
- let size = Cil.bitsSizeOf ty in
- let offset, length = Cil.fieldBitsOffset fd in
- let data = Memory.cell m () in
- let rc = Memory.range m ~size ~offset ~length ~data in
- ignore @@ Memory.merge m r rc ; loffset m s data fd.ftype ofs
+ loffset m s (add_field m r fd) fd.ftype ofs
| Index(_,ofs) ->
- let size = Cil.bitsSizeOf ty in
- let te = typeof_array_elt ty in
- let data = Memory.cell m () in
- let rc = Memory.range m ~size ~offset:0 ~length:size ~data in
- ignore @@ Memory.merge m r rc ; loffset m s data te ofs
+ loffset m s (add_index m r ty) (Cil.typeOf_array_elem ty) ofs
-and pointer m s e = match exp m s e with None -> cell m () | Some r -> r
+and pointer m s e = match exp m s e with None -> add_cell m () | Some r -> r
and value m s e = ignore (exp m s e)
@@ -70,12 +57,7 @@ and exp (m: map) (s:stmt) (e:exp) : node option =
| Lval lv ->
let rv = lval m s lv in
Memory.read m rv (Lval(s,lv)) ;
- if Cil.isPointerType @@ Cil.typeOfLval lv then
- let rp = cell m () in
- Memory.points_to m rv rp ;
- Some rp
- else
- None
+ Memory.add_value m rv @@ Cil.typeOfLval lv
| UnOp(_,e,_) ->
value m s e ; None
@@ -84,7 +66,7 @@ and exp (m: map) (s:stmt) (e:exp) : node option =
value m s k ;
let r = pointer m s p in
(*TODO: move the 'A' access on the source of the pointed region *)
- Memory.shift m r (Exp(s,p)) ;
+ (*Memory.shift m r (Exp(s,p)) ;*)
Some r
| BinOp(_,a,b,_) ->
@@ -96,7 +78,7 @@ and exp (m: map) (s:stmt) (e:exp) : node option =
if Cil.isPointerType ty then
Some (pointer m s p)
else
- (value m s e ; None)
+ (value m s p ; None)
| Const _
| SizeOf _ | SizeOfE _ | SizeOfStr _
@@ -113,7 +95,7 @@ let rec init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
| SingleInit e ->
let r = lval m s lv in
Memory.write m r acs ;
- Option.iter (Memory.points_to m r) (exp m s e)
+ Option.iter (Memory.add_points_to m r) (exp m s e)
| CompoundInit(_,fvs) ->
List.iter
@@ -134,7 +116,7 @@ let instr (m:map) (s:stmt) (instr:instr) =
let r = lval m s lv in
let v = exp m s e in
Memory.write m r (Lval(s,lv)) ;
- Option.iter (Memory.points_to m r) v
+ Option.iter (Memory.add_points_to m r) v
| Local_init(x,AssignInit iv,_) ->
let acs = Access.Init(s,x) in
@@ -173,7 +155,7 @@ let rec stmt (r:rmap) (m:map) (s:stmt) =
"Annotations not analyzed" ;
match s.skind with
| Instr ki -> instr m s ki ; store r m s
- | Return(Some e,_) -> value m s e ; store r m s
+ | Return(Some e,_) -> value m s e ; store r m s
| Goto _ | Break _ | Continue _ | Return(None,_) -> store r m s
| If(e,st,se,_) ->
value m s e ;
@@ -207,6 +189,27 @@ and catch (r:rmap) (m:map) (c:catch_binder) =
and block (r:rmap) (m:map) (b:block) =
List.iter (stmt r m) b.bstmts
+(* -------------------------------------------------------------------------- *)
+(* --- Behavior --- *)
+(* -------------------------------------------------------------------------- *)
+
+type imap = Memory.map Property.Map.t ref
+
+let istore imap m ip =
+ imap := Property.Map.add ip (Memory.copy ~locked:true m) !imap
+
+let bhv ~kf (s:imap) (m:map) (bhv:behavior) =
+ List.iter
+ (fun e ->
+ let rs = Annot.of_extension e in
+ if rs <> [] then
+ begin
+ List.iter (Logic.add_region m) rs ;
+ let ip = Property.ip_of_extended (ELContract kf) e in
+ istore s m ip ;
+ end
+ ) bhv.b_extended
+
(* -------------------------------------------------------------------------- *)
(* --- Function --- *)
(* -------------------------------------------------------------------------- *)
@@ -220,15 +223,23 @@ type domain = {
let domain ?global kf =
let m = match global with Some g -> g | None -> Memory.create () in
let r = ref Stmt.Map.empty in
+ let s = ref Property.Map.empty in
+ begin
+ try
+ let funspec = Annotations.funspec kf in
+ List.iter (bhv ~kf s m) funspec.spec_behavior ;
+ with Annotations.No_funspec _ -> ()
+ end ;
begin
try
let fundec = Kernel_function.get_definition kf in
block r m fundec.sbody ;
with Kernel_function.No_Definition -> ()
- end ; {
+ end ;
+ {
map = Memory.copy ~locked:true m ;
body = !r ;
- spec = Property.Map.empty ;
+ spec = !s ;
}
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/logic.ml b/src/plugins/region/logic.ml
new file mode 100644
index 00000000000..e46702c622e
--- /dev/null
+++ b/src/plugins/region/logic.ml
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Annot
+open Memory
+
+let rec add_lval (m:map) (p:path): node =
+ match p.step with
+ | Var x -> add_root m x
+ | Region a -> add_label m a
+ | Field(lv,fd) -> Memory.add_field m (add_lval m lv) fd
+ | 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)
+ "Unexpected expression (l-value expected)" ;
+ Memory.add_cell m ()
+and add_pointer (m:map) (p:path): Memory.node =
+ match add_exp m p with
+ | None -> add_cell m ()
+ | Some r -> r
+
+and add_exp (m:map) (p:path): Memory.node option =
+ match p.step with
+ | (Var _ | Field _ | Index _ | Star _ | Cast _ | Region _) ->
+ let r = add_lval m p in
+ add_value m r p.typ
+ | AddrOf p -> Some (add_lval m p)
+ | Shift p -> add_exp m p
+
+let add_region (m: map) (r : Annot.region) =
+ let rs = List.map (add_lval m) r.rpath in
+ merge_all m @@
+ match r.rname with
+ | None -> rs
+ | Some a -> add_label m a :: rs
diff --git a/src/plugins/region/logic.mli b/src/plugins/region/logic.mli
new file mode 100644
index 00000000000..e5fb991d29a
--- /dev/null
+++ b/src/plugins/region/logic.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Memory
+
+val add_lval : map -> Annot.path -> node
+val add_exp : map -> Annot.path -> node option
+val add_region : map -> Annot.region -> unit
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 8ac0519149b..9bf73e527ba 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -24,6 +24,9 @@ open Cil_types
open Cil_datatype
module Ufind = UnionFind.Make(Store)
module Vmap = Varinfo.Map
+module Vset = Varinfo.Set
+module Lmap = Map.Make(String)
+module Lset = Set.Make(String)
(* -------------------------------------------------------------------------- *)
(* --- Region Maps --- *)
@@ -40,7 +43,8 @@ and layout =
and chunk = {
cparents: node list ;
- croots: varinfo list ;
+ croots: Vset.t ;
+ clabels: Lset.t ;
creads: Access.Set.t ;
cwrites: Access.Set.t ;
cshifts: Access.Set.t ;
@@ -52,7 +56,8 @@ type rg = node Ranges.range
type map = {
store: chunk Ufind.store ;
mutable locked: bool ;
- mutable index: node Vmap.t ;
+ mutable roots: node Vmap.t ;
+ mutable labels: node Lmap.t ;
}
(* -------------------------------------------------------------------------- *)
@@ -101,7 +106,8 @@ let pp_chunk fmt (n: node) (m: chunk) =
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" Varinfo.pretty) m.croots ;
+ Lset.iter (Format.fprintf fmt "@ %s:") m.clabels ;
+ Vset.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.croots ;
if Options.debug_atleast 1 then
begin
Access.Set.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.creads ;
@@ -119,18 +125,21 @@ let pp_chunk fmt (n: node) (m: chunk) =
let create () = {
locked = false ;
store = Ufind.new_store () ;
- index = Vmap.empty ;
+ roots = Vmap.empty ;
+ labels = Lmap.empty ;
}
let copy ?locked m = {
locked = (match locked with None -> m.locked | Some l -> l) ;
store = Ufind.copy m.store ;
- index = m.index ;
+ roots = m.roots ;
+ labels = m.labels ;
}
let empty = {
cparents = [] ;
- croots = [] ;
+ croots = Vset.empty ;
+ clabels = Lset.empty ;
creads = Access.Set.empty ;
cwrites = Access.Set.empty ;
cshifts = Access.Set.empty ;
@@ -158,33 +167,40 @@ let get map node =
(* --- Chunk Constructors --- *)
(* -------------------------------------------------------------------------- *)
-let cell (m: map) ?size ?ptr ?root () =
- failwith_locked m "Region.Memory.cell" ;
+let add_cell (m: map) ?size ?ptr ?root ?label () =
+ failwith_locked m "Region.Memory.add_cell" ;
let clayout = match size, ptr with
| None, None -> Blob
| None, Some _ -> Cell(Cil.bitsSizeOf Cil.voidPtrType,ptr)
| Some s, _ -> Cell(s,ptr) in
- let croots = match root with None -> [] | Some v -> [v] in
- Ufind.make m.store { empty with clayout ; croots }
+ let croots = Vset.(match root with None -> empty | Some v -> singleton v) in
+ let clabels = Lset.(match label with None -> empty | Some a -> singleton a) in
+ Ufind.make m.store { empty with clayout ; croots ; clabels }
let update (m: map) (n: node) (f: chunk -> chunk) =
let r = get m n in
Ufind.set m.store n (f r)
-let range (m: map) ~size ~offset ~length ~data : node =
- failwith_locked m "Region.Memory.range" ;
+let add_range (m: map) ~size ~offset ~length ~data : node =
+ failwith_locked m "Region.Memory.add_range" ;
let last = offset + length in
if not (0 <= offset && offset < last && last <= size) then
- raise (Invalid_argument "Region.Memory.range") ;
+ raise (Invalid_argument "Region.Memory.add_range") ;
let clayout = Compound(size, Ranges.singleton { offset ; length ; data }) 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 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
+let add_root (m: map) v =
+ try Vmap.find v m.roots with Not_found ->
+ failwith_locked m "Region.Memory.add_root" ;
+ let n = add_cell m ~root:v () in
+ m.roots <- Vmap.add v n m.roots ; n
+
+let add_label (m: map) a =
+ try Lmap.find a m.labels with Not_found ->
+ failwith_locked m "Region.Memory.add_label" ;
+ let n = add_cell m ~label:a () in
+ m.labels <- Lmap.add a n m.labels ; n
(* -------------------------------------------------------------------------- *)
(* --- Iterator --- *)
@@ -201,6 +217,7 @@ type region = {
node: node ;
parents: node list ;
roots: varinfo list ;
+ labels: string list ;
types: typ list ;
reads: Access.acs list ;
writes: Access.acs list ;
@@ -220,11 +237,12 @@ let pp_region fmt (m: region) =
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 "@ (%a)" Typ.pretty) m.types ;
+ 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 ;
- Format.fprintf fmt "@[<hv 0>]" ;
+ Format.fprintf fmt "@[<hv 0>" ;
List.iter (Format.fprintf fmt "@ %a" pp_range) m.ranges ;
Format.fprintf fmt "@]" ;
if Options.debug_atleast 1 then
@@ -246,7 +264,8 @@ let make_range (m: map) (rg: rg) : range = {
let make_region (m: map) (n: node) (r: chunk) : region = {
node = n ;
parents = nodes m r.cparents ;
- roots = r.croots ;
+ 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 ;
@@ -272,7 +291,7 @@ let rec walk h m f n =
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
+ Vmap.iter (fun _x n -> walk h m f n) m.roots
let regions map =
let pool = ref [] in
@@ -311,7 +330,7 @@ let merge_range (m: map) (q: queue) (ra : rg) (rb : rg) : node =
let size = Ranges.(sa %. sb %. dp %. dq) in
let data = merge_node m q na nb in
if size = sa && size = sb then data else
- merge_node m q (cell m ~size ()) data
+ merge_node m q (add_cell m ~size ()) data
let merge_ranges (m: map) (q: queue)
(sa : int) (wa : node Ranges.t)
@@ -338,13 +357,14 @@ let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout =
Compound(size, singleton ~size @@ Ranges.squash (merge_node m q) wr)
| Compound(sr,wr), Cell(sx,Some ptr) | Cell(sx,Some ptr), Compound(sr,wr) ->
- let rp = cell m ~size:sx ~ptr () in
+ let rp = add_cell m ~size:sx ~ptr () in
let wx = Ranges.range ~length:sx rp in
merge_ranges m q sx wx sr wr
let merge_region (m: map) (q: queue) (a : chunk) (b : chunk) : chunk = {
cparents = nodes m @@ Store.bag a.cparents b.cparents ;
- croots = List.sort_uniq Varinfo.compare @@ Store.bag a.croots b.croots ;
+ clabels = Lset.union a.clabels b.clabels ;
+ croots = Vset.union a.croots b.croots ;
creads = Access.Set.union a.creads b.creads ;
cwrites = Access.Set.union a.cwrites b.cwrites ;
cshifts = Access.Set.union a.cshifts b.cshifts ;
@@ -360,16 +380,51 @@ let do_merge (m: map) (q: queue) (a: node) (b: node): unit =
Ufind.set m.store rx rc ;
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 merge_all (m:map) = function
+ | [] -> ()
+ | r::rs ->
let q = Queue.create () in
- do_merge m q a b ;
+ List.iter (fun r' -> ignore @@ merge_node m q r r') rs ;
while not @@ Queue.is_empty q do
let a,b = Queue.pop q in
do_merge m q a b ;
- done ;
- Ufind.find m.store a
+ done
+
+let merge (m: map) (a: node) (b: node) : node =
+ failwith_locked m "Region.Memory.merge" ;
+ merge_all m [a;b] ; Ufind.find m.store (min a b)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Offset --- *)
+(* -------------------------------------------------------------------------- *)
+
+let add_field (m:map) (r:node) (fd:fieldinfo) : node =
+ let ci = fd.fcomp in
+ if ci.cstruct then
+ let size = Cil.bitsSizeOf (TComp(ci,[])) in
+ let offset, length = Cil.fieldBitsOffset fd in
+ let data = add_cell m () in
+ let rc = add_range m ~size ~offset ~length ~data in
+ ignore @@ merge m r rc ; data
+ else r
+
+let add_index (m:map) (r:node) (ty:typ) : node =
+ let size = Cil.bitsSizeOf ty in
+ let data = add_cell m () in
+ let rc = add_range m ~size ~offset:0 ~length:size ~data in
+ ignore @@ merge m r rc ; data
+
+let add_points_to (m: map) (a: node) (b : node) =
+ failwith_locked m "Region.Memory.points_to" ;
+ ignore @@ merge m a @@ add_cell m ~ptr:b ()
+
+let add_value (m:map) (rv:node) (ty:typ) : node option =
+ if Cil.isPointerType ty then
+ let rp = add_cell m () in
+ add_points_to m rv rp ;
+ Some rp
+ else
+ None
(* -------------------------------------------------------------------------- *)
(* --- Access --- *)
@@ -378,11 +433,7 @@ let merge (m: map) (a: node) (b: node) : node =
let access (m:map) (a:node) (ty: typ) =
let sr = sizeof (get m a).clayout in
let size = Ranges.gcd sr (Cil.bitsSizeOf ty) in
- 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 ()
+ if sr <> size then ignore (merge m a (add_cell m ~size ()))
let read (m: map) (a: node) from =
failwith_locked m "Region.Memory.read" ;
@@ -424,7 +475,7 @@ let rec lval (m: map) (lv: lval) : node =
and host (m: map) (h: lhost) : node =
match h with
- | Var x -> Ufind.find m.store @@ Vmap.find x m.index
+ | Var x -> Ufind.find m.store @@ Vmap.find x m.roots
| Mem e ->
match exp m e with
| None -> raise Not_found
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index d31f9bcfa71..79a0543ef0d 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -35,6 +35,7 @@ type region = {
node: node ;
parents: node list ;
roots: varinfo list ;
+ labels: string list ;
types: typ list ;
reads: Access.acs list ;
writes: Access.acs list ;
@@ -62,10 +63,6 @@ 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
-val range : map -> size:int -> offset:int -> length:int -> data:node -> node
-
val id : node -> int
val forge : int -> node
val node : map -> node -> node
@@ -75,11 +72,21 @@ val iter : map -> (region -> unit) -> unit
val region : map -> node -> region
val regions : map -> region list
-val merge : map -> node -> node -> node
+val add_root : map -> Cil_types.varinfo -> node
+val add_label : map -> string -> node
+val add_cell : map -> ?size:int -> ?ptr:node -> ?root:varinfo -> ?label:string -> unit -> node
+val add_range : map -> size:int -> offset:int -> length:int -> data:node -> node
+val add_field : map -> node -> fieldinfo -> 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 points_to : map -> node -> node -> unit
+
+val merge : map -> node -> node -> node
+val merge_all : map -> node list -> unit
(** @raise Not_found *)
val lval : map -> lval -> node
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 72d94683a11..0b5ab56eeec 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -71,6 +71,9 @@ struct
let open Cil_types in
Json.of_list @@ List.map (fun v -> Json.of_string v.vname) vs
+ let labels_to_json ls =
+ Json.of_list @@ List.map Json.of_string ls
+
let ikind_to_char (ikind : Cil_types.ikind) =
match ikind with
| IBool | IUChar -> 'b'
@@ -141,6 +144,7 @@ struct
Jrecord [
"node", Node.jtype ;
"roots", Jarray Jalpha ;
+ "labels", Jarray Jalpha ;
"parents", NodeList.jtype ;
"sizeof", Jnumber ;
"ranges", Ranges.jtype ;
@@ -156,6 +160,7 @@ struct
Json.of_fields [
"node", Node.to_json m.node ;
"roots", roots_to_json m.roots ;
+ "labels", labels_to_json m.labels ;
"parents", NodeList.to_json m.parents ;
"sizeof", Json.of_int @@ m.sizeof ;
"ranges", Ranges.to_json @@ m.ranges ;
--
GitLab