From 3eb276f8f5969ef4b3f52b9ef3ddab7fd782d873 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 12 Jun 2024 16:05:48 +0200
Subject: [PATCH] [region] add-code
---
src/plugins/region/code.ml | 112 +++++++++++++++++------------------
src/plugins/region/code.mli | 5 --
src/plugins/region/memory.ml | 14 +++--
3 files changed, 64 insertions(+), 67 deletions(-)
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index 26a8e0de778..2e2aa7f154e 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -28,57 +28,57 @@ open Memory
(* --- L-Values & Expressions --- *)
(* -------------------------------------------------------------------------- *)
-let rec lval (m:map) (s:stmt) (lv:lval) : node =
+let rec add_lval (m:map) (s:stmt) (lv:lval) : node =
let h = fst lv in
- loffset m s (lhost m s h) (Cil.typeOfLhost h) (snd lv)
+ add_loffset m s (add_lhost m s h) (Cil.typeOfLhost h) (snd lv)
-and lhost (m:map) (s:stmt) = function
+and add_lhost (m:map) (s:stmt) = function
| Var x -> Memory.add_root m x
- | Mem e -> pointer m s e
+ | Mem e -> add_pointer m s e
-and loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
+and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
| NoOffset -> r
| Field(fd,ofs) ->
- loffset m s (add_field m r fd) fd.ftype ofs
+ add_loffset m s (add_field m r fd) fd.ftype ofs
| Index(_,ofs) ->
- loffset m s (add_index m r ty) (Cil.typeOf_array_elem ty) ofs
+ add_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 -> add_cell m () | Some r -> r
+and add_pointer m s e = match add_exp m s e with None -> add_cell m () | Some r -> r
-and value m s e = ignore (exp m s e)
+and add_value m s e = ignore (add_exp m s e)
-and exp (m: map) (s:stmt) (e:exp) : node option =
+and add_exp (m: map) (s:stmt) (e:exp) : node option =
match e.enode with
| AddrOf lv | StartOf lv ->
- let rv = lval m s lv in
+ let rv = add_lval m s lv in
Some rv
| Lval lv ->
- let rv = lval m s lv in
+ let rv = add_lval m s lv in
Memory.read m rv (Lval(s,lv)) ;
Memory.add_value m rv @@ Cil.typeOfLval lv
| UnOp(_,e,_) ->
- value m s e ; None
+ add_value m s e ; None
| BinOp((PlusPI|MinusPI),p,k,_) ->
- value m s k ;
- let r = pointer m s p in
+ add_value m s k ;
+ let r = add_pointer m s p in
(*TODO: move the 'A' access on the source of the pointed region *)
(*Memory.shift m r (Exp(s,p)) ;*)
Some r
| BinOp(_,a,b,_) ->
- value m s a ;
- value m s b ;
+ add_value m s a ;
+ add_value m s b ;
None
| CastE(ty,p) ->
if Cil.isPointerType ty then
- Some (pointer m s p)
+ Some (add_pointer m s p)
else
- (value m s p ; None)
+ (add_value m s p ; None)
| Const _
| SizeOf _ | SizeOfE _ | SizeOfStr _
@@ -89,45 +89,45 @@ and exp (m: map) (s:stmt) (e:exp) : node option =
(* --- Initializers --- *)
(* -------------------------------------------------------------------------- *)
-let rec init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
+let rec add_init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
match iv with
| SingleInit e ->
- let r = lval m s lv in
+ let r = add_lval m s lv in
Memory.write m r acs ;
- Option.iter (Memory.add_points_to m r) (exp m s e)
+ Option.iter (Memory.add_points_to m r) (add_exp m s e)
| CompoundInit(_,fvs) ->
List.iter
(fun (ofs,iv) ->
let lv = Cil.addOffsetLval ofs lv in
- init m s acs lv iv
+ add_init m s acs lv iv
) fvs
(* -------------------------------------------------------------------------- *)
(* --- Instructions --- *)
(* -------------------------------------------------------------------------- *)
-let instr (m:map) (s:stmt) (instr:instr) =
+let add_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
+ let r = add_lval m s lv in
+ let v = add_exp m s e in
Memory.write m r (Lval(s,lv)) ;
Option.iter (Memory.add_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
+ add_init m s acs (Var x,NoOffset) iv
| Call(lr,e,es,_) ->
- value m s e ;
- List.iter (value m s) es ;
+ add_value m s e ;
+ List.iter (add_value m s) es ;
Option.iter
(fun lv ->
- let r = lval m s lv in
+ let r = add_lval m s lv in
Memory.write m r (Lval(s,lv))
) lr ;
Options.warning ~source:(fst @@ Stmt.loc s) "Incomplete call analysis"
@@ -148,46 +148,46 @@ type rmap = Memory.map Stmt.Map.t ref
let store rmap m s =
rmap := Stmt.Map.add s (Memory.copy ~locked:true m) !rmap
-let rec stmt (r:rmap) (m:map) (s:stmt) =
+let rec add_stmt (r:rmap) (m:map) (s:stmt) =
let annots = Annotations.code_annot s in
if annots <> [] then
Options.warning ~source:(fst @@ Stmt.loc s)
"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
+ | Instr ki -> add_instr m s ki ; store r m s
+ | Return(Some e,_) -> add_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 ;
+ add_value m s e ;
store r m s ;
- block r m st ;
- block r m se ;
+ add_block r m st ;
+ add_block r m se ;
| Switch(e,b,_,_) ->
- value m s e ;
+ add_value m s e ;
store r m s ;
- block r m b ;
- | Block b | Loop(_,b,_,_,_) -> block r m b
- | UnspecifiedSequence s -> block r m @@ Cil.block_from_unspecified_sequence s
- | Throw(exn,_) -> Option.iter (fun (e,_) -> value m s e) exn
+ add_block r m b ;
+ | Block b | Loop(_,b,_,_,_) -> add_block r m b
+ | UnspecifiedSequence s -> add_block r m @@ Cil.block_from_unspecified_sequence s
+ | Throw(exn,_) -> Option.iter (fun (e,_) -> add_value m s e) exn
| TryCatch(b,hs,_) ->
- block r m b ;
- List.iter (fun (c,b) -> catch r m c ; block r m b) hs ;
+ add_block r m b ;
+ List.iter (fun (c,b) -> add_catch r m c ; add_block r m b) hs ;
| TryExcept(a,(ks,e),b,_) ->
- block r m a ;
- List.iter (instr m s) ks ;
- value m s e ;
- block r m b ;
+ add_block r m a ;
+ List.iter (add_instr m s) ks ;
+ add_value m s e ;
+ add_block r m b ;
| TryFinally(a,b,_) ->
- block r m a ;
- block r m b ;
+ add_block r m a ;
+ add_block r m b ;
-and catch (r:rmap) (m:map) (c:catch_binder) =
+and add_catch (r:rmap) (m:map) (c:catch_binder) =
match c with
| Catch_all -> ()
- | Catch_exn(_,xbs) -> List.iter (fun (_,b) -> block r m b) xbs
+ | Catch_exn(_,xbs) -> List.iter (fun (_,b) -> add_block r m b) xbs
-and block (r:rmap) (m:map) (b:block) =
- List.iter (stmt r m) b.bstmts
+and add_block (r:rmap) (m:map) (b:block) =
+ List.iter (add_stmt r m) b.bstmts
(* -------------------------------------------------------------------------- *)
(* --- Behavior --- *)
@@ -198,7 +198,7 @@ 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) =
+let add_bhv ~kf (s:imap) (m:map) (bhv:behavior) =
List.iter
(fun e ->
let rs = Annot.of_extension e in
@@ -227,13 +227,13 @@ let domain ?global kf =
begin
try
let funspec = Annotations.funspec kf in
- List.iter (bhv ~kf s m) funspec.spec_behavior ;
+ List.iter (add_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 ;
+ add_block r m fundec.sbody ;
with Kernel_function.No_Definition -> ()
end ;
{
diff --git a/src/plugins/region/code.mli b/src/plugins/region/code.mli
index fb4df16f1af..46cea3a9d8d 100644
--- a/src/plugins/region/code.mli
+++ b/src/plugins/region/code.mli
@@ -24,11 +24,6 @@ open Cil_types
open Cil_datatype
open Memory
-val lval : map -> stmt -> lval -> node
-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 ;
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 9bf73e527ba..ac29123b225 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -485,12 +485,14 @@ 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
+ if fd.fcomp.cstruct then
+ 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
+ else r
| Index (_, ofs) ->
let s, rgs = cranges m r in
match rgs with
--
GitLab