From f6f295cc5353c8cc2f6523bcc62474ee24a3f385 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 28 May 2024 20:16:49 +0200
Subject: [PATCH] [region] expr, term, init, instr
---
src/plugins/region/access.ml | 32 ++++++++-
src/plugins/region/access.mli | 10 ++-
src/plugins/region/insert.ml | 122 ++++++++++++++++++++++++++++++++--
src/plugins/region/insert.mli | 8 +++
src/plugins/region/memory.ml | 12 +++-
5 files changed, 171 insertions(+), 13 deletions(-)
diff --git a/src/plugins/region/access.ml b/src/plugins/region/access.ml
index 10768c98f64..5baa3096b5d 100644
--- a/src/plugins/region/access.ml
+++ b/src/plugins/region/access.ml
@@ -24,19 +24,34 @@ open Cil_types
open Cil_datatype
type acs =
+ | Exp of Stmt.t * exp
| Lval of Stmt.t * lval
+ | Init of Stmt.t * varinfo
| Term of Property.t * term_lval
let compare (a : acs) (b : acs) : int =
match a, b with
+ | Init(sa,xa), Init(sb,xb) ->
+ let cmp = Stmt.compare sa sb in
+ if cmp <> 0 then cmp else Varinfo.compare xa xb
+ | Init _ , _ -> (-1)
+ | _ , Init _ -> (+1)
+
| Lval(sa,la), Lval(sb,lb) ->
let cmp = Stmt.compare sa sb in
if cmp <> 0 then cmp else Lval.compare la lb
+ | Lval _ , _ -> (-1)
+ | _ , Lval _ -> (+1)
+
+ | Exp(sa,ea), Exp(sb,eb) ->
+ let cmp = Stmt.compare sa sb in
+ if cmp <> 0 then cmp else Exp.compare ea eb
+ | Exp _ , _ -> (-1)
+ | _ , Exp _ -> (+1)
+
| Term(sa,ta), Term(sb,tb) ->
let cmp = Property.compare sa sb in
if cmp <> 0 then cmp else Term_lval.compare ta tb
- | Lval _ , Term _ -> (-1)
- | Term _ , Lval _ -> (+1)
let pstmt fmt (s : stmt) =
match s.labels with
@@ -46,10 +61,23 @@ let pstmt fmt (s : stmt) =
Format.fprintf fmt "L%d" loc.pos_lnum
let pretty fmt = function
+ | Init(s,x) ->
+ Format.fprintf fmt "%a@%a" Varinfo.pretty x pstmt s
+ | Exp(s,e) ->
+ Format.fprintf fmt "%a@%a" Exp.pretty e pstmt s
| Lval(s,l) ->
Format.fprintf fmt "%a@%a" Lval.pretty l pstmt s
| Term(s,l) ->
Format.fprintf fmt "%a@%s" Term_lval.pretty l
(Property.Names.get_prop_name_id s)
+let typeof = function
+ | Init(_,x) -> x.vtype
+ | Lval(_,lv) -> Cil.typeOfLval lv
+ | Exp(_,e) -> Cil.typeOf e
+ | Term(_,lt) ->
+ match Cil.typeOfTermLval lt with
+ | Ctype ty -> ty
+ | _ -> Cil.voidType
+
module Set = Set.Make(struct type t = acs let compare = compare end)
diff --git a/src/plugins/region/access.mli b/src/plugins/region/access.mli
index b36604e1bdf..cadb24bc098 100644
--- a/src/plugins/region/access.mli
+++ b/src/plugins/region/access.mli
@@ -20,11 +20,17 @@
(* *)
(**************************************************************************)
+open Cil_types
+
type acs =
- | Lval of Cil_types.stmt * Cil_types.lval
- | Term of Property.t * Cil_types.term_lval
+ | Exp of stmt * exp
+ | Lval of stmt * lval
+ | Init of stmt * varinfo
+ | Term of Property.t * term_lval
val compare : acs -> acs -> int
val pretty : Format.formatter -> acs -> unit
+val typeof : acs -> typ
+
module Set : Set.S with type elt = acs
diff --git a/src/plugins/region/insert.ml b/src/plugins/region/insert.ml
index 0da88f88ec9..721feee97b2 100644
--- a/src/plugins/region/insert.ml
+++ b/src/plugins/region/insert.ml
@@ -23,20 +23,128 @@
open Cil_types
open Memory
-[@@@ warning "-a"]
+let typeof_array_elt ty =
+ match Cil.unrollType ty with
+ | TArray(te,_,_) -> te
+ | _ -> Cil.voidType
-let rec lval (m: map) (lv : lval) : node =
+(* -------------------------------------------------------------------------- *)
+(* --- L-Values & Expressions --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec lval (m:map) (s:stmt) (lv:lval) : node =
let h = fst lv in
- offset m (host m h) (Cil.typeOfLhost h) (snd lv)
+ loffset m s (lhost m s h) (Cil.typeOfLhost h) (snd lv)
-and host (m: map) = function
+and lhost (m:map) (s:stmt) = function
| Var x -> Memory.root m x
- | Mem e -> assert false
+ | Mem e -> ptr m s e
-and offset (m: map) (r: node) (ty: typ)= function
+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
+ | 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
+
+and ptr m s e =
+ match exp m s e with None -> cell m () | Some r -> r
+
+and exp (m: map) (s:stmt) (e:exp) : node option =
+ match e.enode with
+
+ | AddrOf lv | StartOf lv ->
+ let rv = lval m s lv in
+ Some rv
+
+ | 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
+
+ | UnOp(_,e,_) ->
+ ignore (exp m s e) ; None
+
+ | BinOp((PlusPI|MinusPI),p,k,_) ->
+ ignore (exp m s k) ;
+ let r = ptr m s p in
+ Memory.shift m r (Exp(s,e)) ;
+ Some r
+
+ | BinOp(_,a,b,_) ->
+ ignore (exp m s a) ;
+ ignore (exp m s b) ;
+ None
+
+ | CastE(ty,p) ->
+ if Cil.isPointerType ty then
+ Some (ptr m s p)
+ else
+ (ignore (exp m s e) ; None)
+
+ | Const _
+ | SizeOf _ | SizeOfE _ | SizeOfStr _
+ | AlignOf _ | AlignOfE _
+ -> None
+
+(* -------------------------------------------------------------------------- *)
+(* --- Initializers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
+ match iv with
+
+ | 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)
+
+ | CompoundInit(_,fvs) ->
+ List.iter
+ (fun (ofs,iv) ->
+ let lv = Cil.addOffsetLval ofs lv in
+ init m s acs lv iv
+ ) fvs
+
+(* -------------------------------------------------------------------------- *)
+(* --- Instructions --- *)
+(* -------------------------------------------------------------------------- *)
+
+let instr (m:map) (s:stmt) (instr:instr) =
+ match instr with
+ | Skip _ | Code_annot _ -> ()
+
+ | Set(lv,e,_) ->
+ 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
+
+ | Local_init(x,AssignInit iv,_) ->
+ let acs = Access.Init(s,x) in
+ init m s acs (Var x,NoOffset) iv
+
+ | Call _ ->
assert false
- | Index(exp,ofs) -> assert false
+
+ | Local_init(_,ConsInit _,_) ->
+ Options.warning ~source:(fst @@ Cil_datatype.Stmt.loc s)
+ "Constructor init not yet implemented"
+ | Asm _ ->
+ Options.warning ~source:(fst @@ Cil_datatype.Stmt.loc s)
+ "Inline assembly not supported (ignored)"
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/insert.mli b/src/plugins/region/insert.mli
index 664d5d2b3c7..9016f2094c9 100644
--- a/src/plugins/region/insert.mli
+++ b/src/plugins/region/insert.mli
@@ -19,3 +19,11 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+
+open Cil_types
+open Memory
+
+val lval : map -> stmt -> lval -> node
+val ptr : map -> stmt -> exp -> node
+val exp : map -> stmt -> exp -> node option
+val instr : map -> stmt -> instr -> unit
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 5287fb031c7..98b06b38d6a 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -220,19 +220,27 @@ let merge (m: map) (a: node) (b: node) : node =
(* --- Access --- *)
(* -------------------------------------------------------------------------- *)
+let access (m:map) (a:node) (ty: typ) =
+ let sr = sizeof (region m a).layout 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) =
ignore @@ merge m a @@ cell m ~ptr:b ()
let read (m: map) (a: node) from =
let r = region m a in
- Ufind.set m.store a { r with reads = Access.Set.add from r.reads }
+ Ufind.set m.store a { r with reads = Access.Set.add from r.reads } ;
+ access m a (Access.typeof from)
let write (m: map) (a: node) from =
let r = region m a in
- Ufind.set m.store a { r with writes = Access.Set.add from r.writes }
+ Ufind.set m.store a { r with writes = Access.Set.add from r.writes } ;
+ access m a (Access.typeof from)
let shift (m: map) (a: node) from =
let r = region m a in
Ufind.set m.store a { r with shifts = Access.Set.add from r.shifts }
+(* no access *)
(* -------------------------------------------------------------------------- *)
--
GitLab