Skip to content
Snippets Groups Projects
Commit 3eb276f8 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[region] add-code

parent b03f3586
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/region/code.ml
+ 56
− 56
View file @ 3eb276f8
......@@ -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 ;
{
......
src/plugins/region/code.mli
+ 0
− 5
View file @ 3eb276f8
......@@ -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 ;
......
src/plugins/region/memory.ml
+ 8
− 6
View file @ 3eb276f8
......@@ -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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment