diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml index 6cc448f5e198eafc7450826c8673007d657ec4dc..c440b8e4965381bed61e9c1ad95cd270d5780593 100644 --- a/src/plugins/region/Region.ml +++ b/src/plugins/region/Region.ml @@ -24,241 +24,10 @@ (* --- Region Analysis API --- *) (* -------------------------------------------------------------------------- *) +let get_map kf = (Code.domain kf).map +let get_id m n = Memory.id @@ Memory.node m n +let get_node m id = Memory.node m @@ Memory.forge id -open Cil_types +include Memory - -module Node = struct - - type node = Memory.node - type map = Code.domain - - - - (* API GETTERS *) - let get_map (f:kernel_function) : map = Code.domain f - - - let get_id map node = Memory.id (Memory.node map.Code.map node) - let get_node map id = Memory.node map.Code.map @@ Memory.forge id - - - - let cvar (map:map) (var:varinfo) = - Memory.node map.Code.map (Memory.lval map.Code.map ((Var var), NoOffset)) - - let field (map:map) (node:node) (field:fieldinfo) = - Memory.node map.Code.map - @@ Memory.offset map.Code.map node (Field (field, NoOffset)) - - let shift (_map:map) node (_ty:typ) = (* TODO *) node - let index (map:map) node = Memory.index map.Code.map node - - let literal _map ~eid:_eid (_cst : Base.cstring) = raise Not_found - let logical_node _map = raise Not_found - let of_int_node _map = raise Not_found - - - let base_addr _map node = (* TODO *) node - - - - (* API POINTERS *) - let points_to (map:map) (node:node) : node option = - Option.map (Memory.node map.Code.map) - @@ Memory.cpointed map.map node - - let pointed_by (map:map) (node:node) : node list = - List.map (Memory.node map.Code.map) - @@ Memory.cpointed_by map.Code.map node - - - (* COMPARATOR *) - let equal map r1 r2 = Memory.eq_node map.Code.map r1 r2 - - - module Reachable = struct - - module Imap = Map.Make(Int) - - let is_reachable map source target : bool = - let q = Queue.create () in - let exception Reached in - try - let push r = - if equal map target r then raise Reached else Queue.push r q - in - push source ; - let visited = ref Imap.empty in - while true do (*not !accessible && not @@ Queue.is_empty q do *) - let node = Queue.pop q in - if equal map target node then raise Exit else - if not @@ Imap.mem (get_id map node) !visited then begin - visited := Imap.add (get_id map node) node !visited ; - List.iter push (Memory.parents map.Code.map node) - end - done ; - false - with - | Queue.Empty -> false - | Reached -> true - - end - - let included map r1 r2 : bool = Reachable.is_reachable map r1 r2 - - - let separated map r1 r2 = - not (Reachable.is_reachable map r1 r2) - && not (Reachable.is_reachable map r2 r1) - - - - (* API ITERATOR *) - let iter (map:map) (f:node -> unit) : unit = - Memory.iter_node map.map f - - - (* API PRINTER *) - let pp_node fmt node : unit = Memory.pp_node fmt node - - - - - (* API ACCESS *) - type acs = { - acs_read : typ list; - acs_write : typ list; - acs_shift : typ list; - } - let empty_acs = { - acs_read = []; - acs_write = []; - acs_shift = []; - } - - let accesses (m: map) (r:node) : acs = - let acs_read, acs_write, acs_shift = Memory.accesses m.Code.map r in - { acs_read ; acs_write ; acs_shift } -end - - -module Region = struct - type region = Memory.region - - - type map = Code.domain - - - - (* API GETTERS *) - let get_map (f:kernel_function) : map = Code.domain f - - - - let get_id map region = Node.get_id map region.Memory.node - let get_region map id = - try Some (Memory.region map.Code.map @@ Node.get_node map id) - with Not_found -> None - - - - let cvar (map:map) (var:varinfo) = - try Some (Memory.region map.Code.map @@ Node.cvar map var) - with Not_found -> None - - let field (map:map) (region:region) (field:fieldinfo) = - try Some (Memory.region map.Code.map @@ Node.field map region.Memory.node field) - with Not_found -> None - - let shift (map:map) region (ty:typ) = (* TODO *) - try Some (Memory.region map.Code.map @@ Node.shift map region.Memory.node ty) - with Not_found -> None - - - - let base_addr _map region = (* TODO *) region - - - - (* API POINTERS *) - let points_to (map:map) (region:region) : region option = - Option.map (Memory.region map.Code.map) - @@ Memory.cpointed map.map region.Memory.node - - let pointed_by (map:map) (region:region) : region list = - List.map (Memory.region map.Code.map) - @@ Memory.cpointed_by map.Code.map region.Memory.node - - - (* COMPARATOR *) - let equal map r1 r2 = Node.equal map r1.Memory.node r2.Memory.node - - - module Reachable = struct - - module Imap = Map.Make(Int) - - let is_reachable map source target : bool = - let q = Queue.create () in - let exception Reached in - try - let push r = - if equal map target r then raise Reached else Queue.push r q - in - push source ; - let visited = ref Imap.empty in - while true do (*not !accessible && not @@ Queue.is_empty q do *) - let region = Queue.pop q in - if equal map target region then raise Exit else - if not @@ Imap.mem (get_id map region) !visited then begin - visited := Imap.add (get_id map region) region !visited ; - List.iter (fun r -> push (Memory.region map.Code.map r)) region.Memory.parents - end - done ; - false - with - | Queue.Empty -> false - | Reached -> true - - end - - let included map r1 r2 : bool = Reachable.is_reachable map r1 r2 - - - let separated map r1 r2 = - not (Reachable.is_reachable map r1 r2) - && not (Reachable.is_reachable map r2 r1) - - - - (* API ITERATOR *) - let iter (map:map) (f:region -> unit) : unit = - Memory.iter map.map f - - - (* API PRINTER *) - let pp_region fmt region : unit = Memory.pp_region fmt region - - - - - (* API ACCESS *) - type acs = { - acs_read : typ list; - acs_write : typ list; - acs_shift : typ list; - } - let empty_acs = { - acs_read = []; - acs_write = []; - acs_shift = []; - } - - let accesses (region:region) : acs = - { - acs_read = List.map Access.typeof region.Memory.reads ; - acs_write = List.map Access.typeof region.Memory.writes ; - acs_shift = List.map Access.typeof region.Memory.shifts ; - } -end +let iter = Memory.iter_node diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli index 4fb00f9a4f1ba3a505e5d9eda289cbad97dab455..e54782c9d8da43e61b74efe2449db39b03849a03 100644 --- a/src/plugins/region/Region.mli +++ b/src/plugins/region/Region.mli @@ -25,106 +25,31 @@ open Cil_types +type node +type map -(* Lower level API - more efficient *) -module Node : sig - (* General type *) - type node - type map +val get_map : kernel_function -> map +val get_id : map -> node -> int +val get_node : map -> int -> node - (* API GETTERS *) - val get_map : kernel_function -> map +val node : map -> node -> node +val nodes : map -> node list -> node list - val get_id : map -> node -> int - val get_node : map -> int -> node +val cvar : map -> varinfo -> node +val field : map -> node -> fieldinfo -> node +val index : map -> node -> typ -> node - val cvar : map -> varinfo -> node - val field : map -> node -> fieldinfo -> node - val shift : map -> node -> typ -> node - val index : map -> node -> node +val points_to : map -> node -> node option +val pointed_by : map -> node -> node list - val base_addr : map -> node -> node +val equal : map -> node -> node -> bool +val separated : map -> node -> node -> bool +val included : map -> node -> node -> bool - val literal : map -> eid:int -> Base.cstring -> node - val logical_node : map -> node - val of_int_node : map -> node +val iter : map -> (node -> unit) -> unit +val reads : map -> node -> typ list +val writes : map -> node -> typ list +val shifts : map -> node -> typ list - - (* API POINTERS *) - val points_to : map -> node -> node option - val pointed_by : map -> node -> node list - - - (* COMPARATOR *) - val separated : map -> node -> node -> bool - val included : map -> node -> node -> bool - val equal : map -> node -> node -> bool - - (* API ITERATOR *) - val iter : map -> (node -> unit) -> unit - - - (* API PRINTER *) - val pp_node : Format.formatter -> node -> unit - - - (* API ACCESS *) - type acs = { - acs_read : typ list; - acs_write : typ list; - acs_shift : typ list; - } - val empty_acs : acs - val accesses : map -> node -> acs -end - - - - -(* High level API *) -module Region : sig - (* General type *) - type region - type map - - (* API GETTERS *) - val get_map : kernel_function -> map - - val get_id : map -> region -> int - val get_region : map -> int -> region option - - val cvar : map -> varinfo -> region option - val field : map -> region -> fieldinfo -> region option - val shift : map -> region -> typ -> region option - - val base_addr : map -> region -> region - - - (* API POINTERS *) - val points_to : map -> region -> region option - val pointed_by : map -> region -> region list - - - (* COMPARATOR *) - val separated : map -> region -> region -> bool - val included : map -> region -> region -> bool - val equal : map -> region -> region -> bool - - (* API ITERATOR *) - val iter : map -> (region -> unit) -> unit - - - (* API PRINTER *) - val pp_region : Format.formatter -> region -> unit - - - (* API ACCESS *) - type acs = { - acs_read : typ list; - acs_write : typ list; - acs_shift : typ list; - } - val empty_acs : acs - val accesses : region -> acs -end +val pp_node : Format.formatter -> node -> unit diff --git a/src/plugins/region/dune b/src/plugins/region/dune index e091122472a6428e81683f0796a916d9de12458c..f4f00f77e3abbaac66d5fb72b9b59018d629a236 100644 --- a/src/plugins/region/dune +++ b/src/plugins/region/dune @@ -37,7 +37,7 @@ (name Region) (public_name frama-c-region.core) (flags -open Frama_c_kernel :standard -w -9) - (libraries qed frama-c.kernel frama-c-server.core unionFind) + (libraries frama-c.kernel frama-c-server.core unionFind) (instrumentation (backend landmarks)) (instrumentation (backend bisect_ppx))) diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index 1f24461b1ef181344fb415669e4e0c95a216fddb..5e6f6c6e262c424bb3342390e8a1592edaaad1b5 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -43,13 +43,13 @@ and layout = and chunk = { cparents: node list ; + cpointed: node list ; croots: Vset.t ; clabels: Lset.t ; creads: Access.Set.t ; cwrites: Access.Set.t ; cshifts: Access.Set.t ; clayout: layout ; - cpointed_by : node list; } type rg = node Ranges.range @@ -144,13 +144,13 @@ let copy ?locked m = { let empty = { cparents = [] ; + cpointed = [] ; croots = Vset.empty ; clabels = Lset.empty ; creads = Access.Set.empty ; cwrites = Access.Set.empty ; cshifts = Access.Set.empty ; clayout = Blob ; - cpointed_by = [] ; } (* -------------------------------------------------------------------------- *) @@ -159,6 +159,7 @@ let empty = { let id = Store.id let forge = Store.forge +let equal (m: map) = Ufind.eq m.store let node map node = try Ufind.find map.store node @@ -178,17 +179,19 @@ let update (m: map) (n: node) (f: chunk -> chunk) = (* --- Chunk Constructors --- *) (* -------------------------------------------------------------------------- *) -let new_chunk (m: map) ?(size=0) ?ptr ?ptrby () = +let new_chunk (m: map) ?(size=0) ?ptr ?pointed () = failwith_locked m "Region.Memory.new_chunk" ; let clayout = match ptr with | None -> if size = 0 then Blob else Cell(size,None) | Some _ -> Cell(Ranges.gcd size (Cil.bitsSizeOf Cil_const.voidPtrType), ptr) - in let cpointed_by = - match ptrby with - | None -> [] - | Some ptr -> [ptr] - in Ufind.make m.store { empty with clayout ; cpointed_by } + in + let cpointed = + match pointed with + | None -> [] + | Some ptr -> [ptr] + in + Ufind.make m.store { empty with clayout ; cpointed } let new_range (m: map) ?(fields=Fields.empty) ~size ~offset ~length data : node = failwith_locked m "Region.Memory.new_range" ; @@ -440,13 +443,13 @@ let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout = let merge_region (m: map) (q: queue) (a : chunk) (b : chunk) : chunk = { cparents = nodes m @@ Store.bag a.cparents b.cparents ; + cpointed = nodes m @@ Store.bag a.cpointed b.cpointed ; 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 ; clayout = merge_layout m q a.clayout b.clayout ; - cpointed_by = List.append a.cpointed_by b.cpointed_by ; } let do_merge (m: map) (q: queue) (a: node) (b: node): unit = @@ -498,14 +501,20 @@ let add_index (m:map) (r:node) (ty:typ) (n:int) : node = ignore @@ merge m r rc ; re let add_points_to (m: map) (a: node) (b : node) = - failwith_locked m "Region.Memory.points_to" ; - ignore @@ merge m a @@ new_chunk m ~ptr:b ~ptrby:a () + begin + failwith_locked m "Region.Memory.points_to" ; + ignore @@ merge m a @@ new_chunk m ~ptr:b () ; + ignore @@ merge m b @@ new_chunk m ~pointed:a () ; + end let add_value (m:map) (rv:node) (ty:typ) : node option = if Cil.isPointerType ty then - let rp = new_chunk m () in - add_points_to m rv rp ; - Some rp + begin + failwith_locked m "Region.Memory.add_value" ; + let rp = new_chunk m ~pointed:rv () in + ignore @@ merge m rv @@ new_chunk m ~ptr:rp () ; + Some rp + end else None @@ -540,66 +549,60 @@ let shift (m: map) (a: node) from = (* --- Lookup ---- *) (* -------------------------------------------------------------------------- *) -let cranges m r = - let rg = Ufind.get m.store r in - match rg.clayout with - | Blob | Cell _ -> raise Not_found - | Compound(s,_,rgs) -> s, rgs - -let cpointed m r = +let points_to m (r : node) : node option = let rg = Ufind.get m.store r in match rg.clayout with | Blob | Compound _ | Cell(_,None) -> None | Cell(_,Some r) -> Some (Ufind.find m.store r) -let cpointed_by m r = - let rg = Ufind.get m.store r in - rg.cpointed_by +let pointed_by m (r : node) = + let rg = Ufind.get m.store r in rg.cpointed let cvar (m: map) (v: varinfo) : node = Ufind.find m.store @@ Vmap.find v m.roots +let rec move (m: map) (r: node) (p: int) (s: int) = + let c = Ufind.get m.store r in + match c.clayout with + | Blob | Cell _ -> r + | Compound(s0,_,rgs) -> + if s0 <= s then r else + let rg = Ranges.find p rgs in + move m rg.data (p - rg.offset) s + let field (m: map) (r: node) (fd: fieldinfo) : node = - 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 - Ufind.find m.store rg.data - else raise Not_found - else r + let s = Cil.bitsSizeOf fd.ftype in + let (p,_) = Cil.fieldBitsOffset fd in + move m r p s -let index (m : map) (r: node) : node = - let s, rgs = cranges m r in - match rgs with - | R [rg] when rg.offset = 0 && rg.length = s -> rg.data - | _ -> raise Not_found +let index (m : map) (r: node) (ty:typ) : node = + move m r 0 (Cil.bitsSizeOf ty) -let rec lval (m: map) (lv: lval) : node = - let h = host m (fst lv) in - offset m h (snd lv) +let rec lval (m: map) (h,ofs) : node = + offset m (lhost m h) (Cil.typeOfLhost h) ofs -and host (m: map) (h: lhost) : node = +and lhost (m: map) (h: lhost) : node = match h with | Var x -> cvar m x | Mem e -> match exp m e with - | None -> raise Not_found | Some r -> r + | None -> raise Not_found -and offset (m: map) (r: node) (ofs: offset) : node = +and offset (m: map) (r: node) (ty: typ) (ofs: offset) : node = match ofs with | NoOffset -> Ufind.find m.store r | Field (fd, ofs) -> - if fd.fcomp.cstruct then offset m (field m r fd) ofs - else r - | Index (_, ofs) -> offset m (index m r) ofs + offset m (field m r fd) fd.ftype ofs + | Index (_, ofs) -> + let te = Cil.typeOf_array_elem ty in + offset m (index m r te) te ofs and exp (m: map) (e: exp) : node option = match e.enode with | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> None - | Lval lv -> cpointed m @@ lval m lv + | Lval lv -> points_to m @@ lval m lv | AddrOf lv | StartOf lv -> Some (lval m lv) | CastE(_, e) -> exp m e | BinOp((PlusPI|MinusPI),p,_,_) -> exp m p @@ -607,11 +610,44 @@ and exp (m: map) (e: exp) : node option = (* -------------------------------------------------------------------------- *) +let included map source target : bool = + let exception Reached in + try + let q = Queue.create () in (* only marked nodes *) + let push r = + let r = node map r in + if equal map target r then raise Reached else Queue.push r q + in + push source ; + let visited = Hashtbl.create 0 in + while true do + let node = Queue.pop q in + if equal map target node then raise Exit else + let id = id node in + if not @@ Hashtbl.mem visited id then + begin + Hashtbl.add visited id () ; + List.iter push (parents map node) ; + end + done ; + assert false + with + | Queue.Empty -> false + | Reached -> true + +let separated map r1 r2 = + not (included map r1 r2) && not (included map r2 r1) + +(* -------------------------------------------------------------------------- *) -let eq_node (m: map) = Ufind.eq m.store +let reads (m : map) (r:node) = + let node = Ufind.get m.store r in + List.map Access.typeof @@ Access.Set.elements node.creads + +let writes (m : map) (r:node) = + let node = Ufind.get m.store r in + List.map Access.typeof @@ Access.Set.elements node.cwrites -let accesses (m : map) (r:node) = +let shifts (m : map) (r:node) = let node = Ufind.get m.store r in - List.map Access.typeof @@ Access.Set.elements node.creads, - List.map Access.typeof @@ Access.Set.elements node.cwrites, List.map Access.typeof @@ Access.Set.elements node.cshifts diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli index a5d11505e0e6029a50046c3425bc3351560a26f9..cdd2ae7c65a10412209c06fbac7be8f736ffb30d 100644 --- a/src/plugins/region/memory.mli +++ b/src/plugins/region/memory.mli @@ -66,6 +66,7 @@ val unlock : map -> unit val id : node -> int val forge : int -> node +val equal : map -> node -> node -> bool val node : map -> node -> node val nodes : map -> node list -> node list @@ -75,7 +76,7 @@ val region : map -> node -> region val regions : map -> region list val parents : map -> node -> node list -val new_chunk : map -> ?size:int -> ?ptr:node -> ?ptrby:node -> unit -> node +val new_chunk : map -> ?size:int -> ?ptr:node -> ?pointed:node -> unit -> node val add_root : map -> Cil_types.varinfo -> node val add_label : map -> string -> node val add_field : map -> node -> fieldinfo -> node @@ -91,20 +92,18 @@ val merge : map -> node -> node -> unit val merge_all : map -> node list -> unit val merge_copy : map -> l:node -> r:node -> unit -(** @raise Not_found *) +val cvar : map -> varinfo -> node +val field : map -> node -> fieldinfo -> node +val index : map -> node -> typ -> node val lval : map -> lval -> node -val offset : map -> node -> offset -> node -val index : map -> node -> node -val cpointed : map -> node -> node option -val cpointed_by : map -> node -> node list - -(** @raise Not_found *) val exp : map -> exp -> node option -(** @raise Not_found *) -val field : map -> node -> fieldinfo -> node -val cvar : map -> varinfo -> node +val points_to : map -> node -> node option +val pointed_by : map -> node -> node list -val eq_node : map -> node -> node -> bool +val included : map -> node -> node -> bool +val separated : map -> node -> node -> bool -val accesses : map -> node -> typ list * typ list * typ list +val reads : map -> node -> typ list +val writes : map -> node -> typ list +val shifts : map -> node -> typ list diff --git a/src/plugins/region/tests/region/oracle/comp.res.oracle b/src/plugins/region/tests/region/oracle/comp.res.oracle index f73256e38a6e7ec99715ae0edf5f6e15e2bb1da0..d444b5dc68c66f3c4e63bbbbd876679a76495ab0 100644 --- a/src/plugins/region/tests/region/oracle/comp.res.oracle +++ b/src/plugins/region/tests/region/oracle/comp.res.oracle @@ -1,9 +1,9 @@ [kernel] Parsing comp.c (with preprocessing) [region] Analyzing regions [region] Function f: - R0003: --- s 192b { .x: R0004; #32b; .z: R0008; .arr: R000c; } ; + R0003: --- s 192b { .x: R0004; #32b; .z: R0008; .arr: R000d; } ; R0004: -W- (int) 32b ; R0008: -W- (int *) 64b (*R0001) ; R0001: RW- a (int) 32b ; - R000c: --- 64b { #64b: R000e[4]; } ; - R000e: -W- (short) 16b ; + R000d: --- 64b { #64b: R000f[4]; } ; + R000f: -W- (short) 16b ; diff --git a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle index db2191393f4788d8cdd0d304779db01b93806d44..4de3c9517dbac676e8443d7aea783f55c9355fd5 100644 --- a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle +++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle @@ -6,31 +6,31 @@ { .prm.inp1: R0007[2]; #128b; - .out1: R000e; - .out2: R0067; - .out3.idx1: R0015[2]; + .out1: R000f; + .out2: R006a; + .out3.idx1: R0017[2]; #128b; - .sum: R0054; + .sum: R0057; } ; - R0007: R-- (struct N *) 64b (*R0024) ; - R0024: --- 128b { .v: R0026; .s: R0046; #32b; } ; - R0026: R-- (double) 64b ; - R0046: R-- (int) 32b ; - R000e: R-- (struct N *) 64b (*R001d) ; - R001d: --- 128b { .v: R001f; .s: R0038; #32b; } ; - R001f: RW- (double) 64b ; - R0038: -W- (int) 32b ; - R0067: R-- (struct N *) 64b (*R006a) ; - R006a: --- 128b { .v: R006c; #64b; } ; - R006c: R-- (double) 64b ; - R0015: R-- (struct N *) (struct L *) 64b (*R003e) ; - R003e: --- 64b { .v.s: R0040[2]; } ; - R0040: RW- (int) (double) 32b ; - R0054: R-- (struct N *) 64b (*R0057) ; - R0057: --- 128b { .v: R0059; .s: R0080; #32b; } ; - R0059: -W- (double) 64b ; - R0080: -W- (int) 32b ; + R0007: R-- (struct N *) 64b (*R0027) ; + R0027: --- 128b { .v: R0029; .s: R0049; #32b; } ; + R0029: R-- (double) 64b ; + R0049: R-- (int) 32b ; + R000f: R-- (struct N *) 64b (*R0020) ; + R0020: --- 128b { .v: R0022; .s: R003b; #32b; } ; + R0022: RW- (double) 64b ; + R003b: -W- (int) 32b ; + R006a: R-- (struct N *) 64b (*R006d) ; + R006d: --- 128b { .v: R006f; #64b; } ; + R006f: R-- (double) 64b ; + R0017: R-- (struct N *) (struct L *) 64b (*R0041) ; + R0041: --- 64b { .v.s: R0043[2]; } ; + R0043: RW- (int) (double) 32b ; + R0057: R-- (struct N *) 64b (*R005a) ; + R005a: --- 128b { .v: R005c; .s: R0083; #32b; } ; + R005c: -W- (double) 64b ; + R0083: -W- (int) 32b ; R0001: RWA inp (SN *) 64b (*R0007) ; - R000a: RWA out (SN *) 64b (*R000e) ; - R0011: RWA idx (SL *) 64b (*R0015) ; - R0018: RW- i (int) 32b ; + R000b: RWA out (SN *) 64b (*R000f) ; + R0013: RWA idx (SL *) 64b (*R0017) ; + R001b: RW- i (int) 32b ;