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

[region] clarify internal api

parent e4cf78c8
No related branches found
No related tags found
No related merge requests found
...@@ -66,14 +66,14 @@ and add_exp (m: map) (s:stmt) (e:exp) : scalar = ...@@ -66,14 +66,14 @@ and add_exp (m: map) (s:stmt) (e:exp) : scalar =
| Lval lv -> | Lval lv ->
let rv = add_lval m s lv in let rv = add_lval m s lv in
Memory.read m rv (Lval(s,lv)) ; Memory.add_read m rv (Lval(s,lv)) ;
let ptr = Memory.add_value m rv @@ Cil.typeOfLval lv in let ptr = Memory.add_value m rv @@ Cil.typeOfLval lv in
{ from = Some rv ; ptr } { from = Some rv ; ptr }
| BinOp((PlusPI|MinusPI),p,k,_) -> | BinOp((PlusPI|MinusPI),p,k,_) ->
add_value m s k ; add_value m s k ;
let v = add_exp m s p in let v = add_exp m s p in
Option.iter (fun r -> Memory.shift m r (Exp(s,e))) v.from ; v Option.iter (fun r -> Memory.add_shift m r (Exp(s,e))) v.from ; v
| UnOp(_,e,_) -> | UnOp(_,e,_) ->
add_value m s e ; integral add_value m s e ; integral
...@@ -102,7 +102,7 @@ let rec add_init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) = ...@@ -102,7 +102,7 @@ let rec add_init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
| SingleInit e -> | SingleInit e ->
let r = add_lval m s lv in let r = add_lval m s lv in
Memory.write m r acs ; Memory.add_write m r acs ;
Option.iter (Memory.add_points_to m r) (add_exp m s e).ptr Option.iter (Memory.add_points_to m r) (add_exp m s e).ptr
| CompoundInit(_,fvs) -> | CompoundInit(_,fvs) ->
...@@ -123,14 +123,14 @@ let add_instr (m:map) (s:stmt) (instr:instr) = ...@@ -123,14 +123,14 @@ let add_instr (m:map) (s:stmt) (instr:instr) =
| Set(lv, { enode = Lval exp }, _) -> | Set(lv, { enode = Lval exp }, _) ->
let l = add_lval m s lv in let l = add_lval m s lv in
let r = add_lval m s exp in let r = add_lval m s exp in
Memory.read m r (Lval(s,exp)) ; Memory.add_read m r (Lval(s,exp)) ;
Memory.write m l (Lval(s,lv)) ; Memory.add_write m l (Lval(s,lv)) ;
Memory.merge_copy m ~l ~r Memory.merge_copy m ~l ~r
| Set(lv,e,_) -> | Set(lv,e,_) ->
let r = add_lval m s lv in let r = add_lval m s lv in
let v = add_exp m s e in let v = add_exp m s e in
Memory.write m r (Lval(s,lv)) ; Memory.add_write m r (Lval(s,lv)) ;
Option.iter (Memory.add_points_to m r) v.ptr Option.iter (Memory.add_points_to m r) v.ptr
| Local_init(x,AssignInit iv,_) -> | Local_init(x,AssignInit iv,_) ->
...@@ -143,7 +143,7 @@ let add_instr (m:map) (s:stmt) (instr:instr) = ...@@ -143,7 +143,7 @@ let add_instr (m:map) (s:stmt) (instr:instr) =
Option.iter Option.iter
(fun lv -> (fun lv ->
let r = add_lval m s lv in let r = add_lval m s lv in
Memory.write m r (Lval(s,lv)) Memory.add_write m r (Lval(s,lv))
) lr ; ) lr ;
Options.warning ~source:(fst @@ Stmt.loc s) "Incomplete call analysis" Options.warning ~source:(fst @@ Stmt.loc s) "Incomplete call analysis"
......
...@@ -367,20 +367,20 @@ let add_field (m:map) (r:node) (fd:fieldinfo) : node = ...@@ -367,20 +367,20 @@ let add_field (m:map) (r:node) (fd:fieldinfo) : node =
let rf = new_chunk m () in let rf = new_chunk m () in
let fields = Fields.singleton fd in let fields = Fields.singleton fd in
let rc = new_range m ~fields ~size ~offset ~length rf in let rc = new_range m ~fields ~size ~offset ~length rf in
ignore @@ merge m r rc ; rf merge m r rc ; rf
else r else r
let add_index (m:map) (r:node) (ty:typ) (n:int) : node = let add_index (m:map) (r:node) (ty:typ) (n:int) : node =
let s = Cil.bitsSizeOf ty * n in let s = Cil.bitsSizeOf ty * n in
let re = new_chunk m () in let re = new_chunk m () in
let rc = new_range m ~size:s ~offset:0 ~length:s re in let rc = new_range m ~size:s ~offset:0 ~length:s re in
ignore @@ merge m r rc ; re merge m r rc ; re
let add_points_to (m: map) (a: node) (b : node) = let add_points_to (m: map) (a: node) (b : node) =
begin begin
failwith_locked m "Region.Memory.points_to" ; failwith_locked m "Region.Memory.points_to" ;
ignore @@ merge m a @@ new_chunk m ~ptr:b () ; merge m a @@ new_chunk m ~ptr:b () ;
ignore @@ merge m b @@ new_chunk m ~pointed:a () ; merge m b @@ new_chunk m ~pointed:a () ;
end end
let add_value (m:map) (rv:node) (ty:typ) : node option = let add_value (m:map) (rv:node) (ty:typ) : node option =
...@@ -388,7 +388,7 @@ let add_value (m:map) (rv:node) (ty:typ) : node option = ...@@ -388,7 +388,7 @@ let add_value (m:map) (rv:node) (ty:typ) : node option =
begin begin
failwith_locked m "Region.Memory.add_value" ; failwith_locked m "Region.Memory.add_value" ;
let rp = new_chunk m ~pointed:rv () in let rp = new_chunk m ~pointed:rv () in
ignore @@ merge m rv @@ new_chunk m ~ptr:rp () ; merge m rv @@ new_chunk m ~ptr:rp () ;
Some rp Some rp
end end
else else
...@@ -403,23 +403,23 @@ let sized (m:map) (a:node) (ty: typ) = ...@@ -403,23 +403,23 @@ let sized (m:map) (a:node) (ty: typ) =
let size = Ranges.gcd sr (Cil.bitsSizeOf ty) in let size = Ranges.gcd sr (Cil.bitsSizeOf ty) in
if sr <> size then ignore (merge m a (new_chunk m ~size ())) if sr <> size then ignore (merge m a (new_chunk m ~size ()))
let read (m: map) (a: node) from = let add_read (m: map) (a: node) acs =
failwith_locked m "Region.Memory.read" ; failwith_locked m "Region.Memory.read" ;
let r = get m a in let r = get m a in
Ufind.set m.store a { r with creads = Access.Set.add from r.creads } ; Ufind.set m.store a { r with creads = Access.Set.add acs r.creads } ;
sized m a (Access.typeof from) sized m a (Access.typeof acs)
let write (m: map) (a: node) from = let add_write (m: map) (a: node) acs =
failwith_locked m "Region.Memory.write" ; failwith_locked m "Region.Memory.write" ;
let r = get m a in let r = get m a in
Ufind.set m.store a { r with cwrites = Access.Set.add from r.cwrites } ; Ufind.set m.store a { r with cwrites = Access.Set.add acs r.cwrites } ;
sized m a (Access.typeof from) sized m a (Access.typeof acs)
let shift (m: map) (a: node) from = let add_shift (m: map) (a: node) acs =
failwith_locked m "Region.Memory.shift" ; failwith_locked m "Region.Memory.shift" ;
let r = get m a in let r = get m a in
Ufind.set m.store a { r with cshifts = Access.Set.add from r.cshifts } ; Ufind.set m.store a { r with cshifts = Access.Set.add acs r.cshifts } ;
sized m a (Access.typeof from) sized m a (Access.typeof acs)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* --- Lookup ---- *) (* --- Lookup ---- *)
......
...@@ -88,9 +88,9 @@ val add_index : map -> node -> typ -> int -> node ...@@ -88,9 +88,9 @@ val add_index : map -> node -> typ -> int -> node
val add_points_to : map -> node -> node -> unit val add_points_to : map -> node -> node -> unit
val add_value : map -> node -> typ -> node option val add_value : map -> node -> typ -> node option
val read : map -> node -> Access.acs -> unit val add_read : map -> node -> Access.acs -> unit
val write : map -> node -> Access.acs -> unit val add_write : map -> node -> Access.acs -> unit
val shift : map -> node -> Access.acs -> unit val add_shift : map -> node -> Access.acs -> unit
val merge : map -> node -> node -> unit val merge : map -> node -> node -> unit
val merge_all : map -> node list -> unit val merge_all : map -> node list -> unit
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment