diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx index 2b38fe1acbe532113a27f458bb0a43fe2a30c023..42e4ac7f8de6f78166ab7d811ca027408e149c09 100644 --- a/ivette/src/frama-c/plugins/region/memory.tsx +++ b/ivette/src/frama-c/plugins/region/memory.tsx @@ -70,7 +70,7 @@ function makeDiagram(regions: readonly Region.region[]): Diagram { const id = `n${r.node}`; // --- Color const color = - r.bytes ? 'red' : + !r.typed ? 'red' : r.pointed !== undefined ? (r.writes ? 'orange' : 'yellow') : (r.writes && r.reads) ? 'green' : @@ -81,19 +81,17 @@ function makeDiagram(regions: readonly Region.region[]): Diagram { const shape = cells.length > 0 ? cells : undefined; nodes.push({ id, font, color, label: r.label, title: r.title, shape }); // --- Labels - const L: Dot.Node = - { id: '', shape: 'note', font: 'mono' }; + const L: Dot.Node = { id: '', shape: 'note', font: 'mono' }; r.labels.forEach(a => { const lid = `L${a}`; nodes.push({ ...L, id: lid, label: `${a}:` }); edges.push({ source: lid, target: id, aligned: true, - headAnchor: 'n', head: 'none', color: 'grey' + headAnchor: 's', head: 'none', color: 'grey' }); }); // --- Roots - const R: Dot.Node = - { id: '', shape: 'cds', font: 'mono' }; + const R: Dot.Node = { id: '', shape: 'cds', font: 'mono' }; r.roots.forEach(x => { const xid = `X${x}`; nodes.push({ ...R, id: xid, label: x }); diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml index c9c75368a2f3d5f72a2cca07cc06b09aa7b230b5..1ad5b12e13bcc7950c181f43c9c38290c4f9010f 100644 --- a/src/plugins/region/memory.ml +++ b/src/plugins/region/memory.ml @@ -66,11 +66,11 @@ type map = { (* -------------------------------------------------------------------------- *) let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_,_) -> s -let ranges = function Blob | Cell _ -> [] | Compound(_,_,R rs) -> rs -let fields = function Blob | Cell _ -> Fields.empty | Compound(_,fds,_) -> fds -let pointed = function Blob | Compound _ -> None | Cell(_,p) -> p +let cranges = function Blob | Cell _ -> [] | Compound(_,_,R rs) -> rs +let cfields = function Blob | Cell _ -> Fields.empty | Compound(_,fds,_) -> fds +let cpointed = function Blob | Compound _ -> None | Cell(_,p) -> p -let types (m : chunk) : typ list = +let ctypes (m : chunk) : typ list = let pool = ref Typ.Set.empty in let add acs = pool := Typ.Set.add (Cil.unrollType @@ Access.typeof acs) !pool in @@ -111,7 +111,7 @@ let pp_chunk fmt (n: node) (m: chunk) = let acs r s = if Access.Set.is_empty s then '-' else r in Format.fprintf fmt "@[<hov 2>%a: %c%c%c" pp_node n (acs 'R' m.creads) (acs 'W' m.cwrites) (acs 'A' m.cshifts) ; - List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (types m) ; + List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (ctypes m) ; Lset.iter (Format.fprintf fmt "@ %s:") m.clabels ; Vset.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.croots ; if Options.debug_atleast 1 then @@ -221,117 +221,6 @@ let add_label (m: map) a = (* --- Iterator --- *) (* -------------------------------------------------------------------------- *) -type range = { - label: string ; (* pretty printed fields *) - offset: int ; - length: int ; - cells: int ; - data: node ; -} - -type region = { - node: node ; - parents: node list ; - roots: varinfo list ; - labels: string list ; - types: typ list ; - fields: Fields.domain ; - reads: Access.acs list ; - writes: Access.acs list ; - shifts: Access.acs list ; - sizeof: int ; - ranges: range list ; - pointed: node option ; -} - -let pp_cells fmt = function - | 1 -> () - | 0 -> Format.fprintf fmt "[…]" - | n -> Format.fprintf fmt "[%d]" n - -type slice = - | Padding of int - | Range of range - -let pad p q s = - let n = q - p in - if n > 0 then Padding n :: s else s - -let rec span k s = function - | [] -> pad k s [] - | r::rs -> pad k r.offset @@ Range r :: span (r.offset + r.length) s rs - -let pp_slice fields fmt = function - | Padding n -> - Format.fprintf fmt "@ %a;" Fields.pp_bits n - | Range r -> - Format.fprintf fmt "@ %t: %a%a;" - (Fields.pslice ~fields ~offset:r.offset ~length:r.length) - pp_node r.data - pp_cells r.cells - -let pp_range fmt (r: range) = - Format.fprintf fmt "@ %d..%d: %a%a;" - r.offset (r.offset + r.length) pp_node r.data pp_cells r.cells - -let pp_region fmt (m: region) = - begin - let acs r s = if s = [] then '-' else r in - Format.fprintf fmt "@[<hov 2>%a: %c%c%c" - pp_node m.node - (acs 'R' m.reads) (acs 'W' m.writes) (acs 'A' m.shifts) ; - List.iter (Format.fprintf fmt "@ %s:") m.labels ; - List.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.roots ; - List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) m.types ; - Format.fprintf fmt "@ %db" m.sizeof ; - Option.iter (Format.fprintf fmt "@ (*%a)" pp_node) m.pointed ; - if m.ranges <> [] then - begin - Format.fprintf fmt "@ @[<hv 0>@[<hv 2>{" ; - if Options.debug_atleast 1 then - List.iter (pp_range fmt) m.ranges - else - List.iter (pp_slice m.fields fmt) (span 0 m.sizeof m.ranges) ; - Format.fprintf fmt "@]@ }@]" ; - end ; - if Options.debug_atleast 1 then - begin - List.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.reads ; - List.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.writes ; - List.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.shifts ; - end ; - Format.fprintf fmt " ;@]" ; - end - -let make_range (m: map) fields Ranges.{ length ; offset ; data } : range = - let s = sizeof (get m data).clayout in - let p = Fields.pslice ~fields ~offset ~length in - { - label = Format.asprintf "%t" p ; - offset ; length ; - cells = if s = 0 then 0 else length / s ; - data = node m data ; - } - -let make_region (m: map) (n: node) (r: chunk) : region = - let types = types r in - let sizeof = sizeof r.clayout in - let fields = fields r.clayout in - { - node = n ; - parents = nodes m r.cparents ; - roots = Vset.elements r.croots ; - labels = Lset.elements r.clabels ; - reads = Access.Set.elements r.creads ; - writes = Access.Set.elements r.cwrites ; - shifts = Access.Set.elements r.cshifts ; - types ; sizeof ; fields ; - ranges = List.map (make_range m fields) (ranges r.clayout) ; - pointed = Option.map (node m) (pointed r.clayout) ; - } - -let region map n = make_region map n (get map n) - let rec walk h m (f: node -> unit) n = let n = Ufind.find m.store n in let id = Store.id n in @@ -348,11 +237,6 @@ let iter (m:map) (f: node -> unit) = let h = Hashtbl.create 0 in Vmap.iter (fun _x n -> walk h m f n) m.roots -let regions map = - let pool = ref [] in - iter map (fun r -> pool := region map r :: !pool) ; - List.rev !pool - let size (m: map) (r: node) = sizeof (Ufind.get m.store r).clayout @@ -665,6 +549,8 @@ let shifts (m:map) (r:node) = let node = Ufind.get m.store r in List.map Access.typeof @@ Access.Set.elements node.cshifts +let types (m:map) (r:node) = ctypes @@ Ufind.get m.store r + let typed (m:map) (r:node) = let types = ref None in let node = Ufind.get m.store r in @@ -682,3 +568,136 @@ let typed (m:map) (r:node) = Access.Set.iter check node.cshifts ; !types with Exit -> None + +(* -------------------------------------------------------------------------- *) +(* --- High-Level API --- *) +(* -------------------------------------------------------------------------- *) + +type range = { + label: string ; (* pretty printed fields *) + offset: int ; + length: int ; + cells: int ; + data: node ; +} + +type region = { + node: node ; + parents: node list ; + roots: varinfo list ; + labels: string list ; + types: typ list ; + typed : typ option ; + fields: Fields.domain ; + reads: Access.acs list ; + writes: Access.acs list ; + shifts: Access.acs list ; + sizeof: int ; + singleton : bool ; + ranges: range list ; + pointed: node option ; +} + +let make_range (m: map) fields Ranges.{ length ; offset ; data } : range = + let s = sizeof (get m data).clayout in + let p = Fields.pslice ~fields ~offset ~length in + { + label = Format.asprintf "%t" p ; + offset ; length ; + cells = if s = 0 then 0 else length / s ; + data = node m data ; + } + +let ranges (m:map) (r:node) = + let node = Ufind.get m.store r in + let fields = cfields node.clayout in + List.map (make_range m fields) (cranges node.clayout) + +let make_region (m: map) (n: node) (r: chunk) : region = + let types = ctypes r in + let typed = typed m n in + let sizeof = sizeof r.clayout in + let fields = cfields r.clayout in + let singleton = singleton m n in + { + node = n ; + parents = nodes m r.cparents ; + roots = Vset.elements r.croots ; + labels = Lset.elements r.clabels ; + reads = Access.Set.elements r.creads ; + writes = Access.Set.elements r.cwrites ; + shifts = Access.Set.elements r.cshifts ; + ranges = List.map (make_range m fields) (cranges r.clayout) ; + pointed = Option.map (node m) (cpointed r.clayout) ; + types ; typed ; singleton ; sizeof ; fields ; + } + +let region map n = make_region map n (get map n) + +let regions map = + let pool = ref [] in + iter map (fun r -> pool := region map r :: !pool) ; + List.rev !pool + +(* -------------------------------------------------------------------------- *) +(* --- Pretty Printers --- *) +(* -------------------------------------------------------------------------- *) + +let pp_cells fmt = function + | 1 -> () + | 0 -> Format.fprintf fmt "[…]" + | n -> Format.fprintf fmt "[%d]" n + +type slice = + | Padding of int + | Range of range + +let pad p q s = + let n = q - p in + if n > 0 then Padding n :: s else s + +let rec span k s = function + | [] -> pad k s [] + | r::rs -> pad k r.offset @@ Range r :: span (r.offset + r.length) s rs + +let pp_slice fields fmt = function + | Padding n -> + Format.fprintf fmt "@ %a;" Fields.pp_bits n + | Range r -> + Format.fprintf fmt "@ %t: %a%a;" + (Fields.pslice ~fields ~offset:r.offset ~length:r.length) + pp_node r.data + pp_cells r.cells + +let pp_range fmt (r: range) = + Format.fprintf fmt "@ %d..%d: %a%a;" + r.offset (r.offset + r.length) pp_node r.data pp_cells r.cells + +let pp_region fmt (m: region) = + begin + let acs r s = if s = [] then '-' else r in + Format.fprintf fmt "@[<hov 2>%a: %c%c%c" + pp_node m.node + (acs 'R' m.reads) (acs 'W' m.writes) (acs 'A' m.shifts) ; + List.iter (Format.fprintf fmt "@ %s:") m.labels ; + List.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.roots ; + List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) m.types ; + Format.fprintf fmt "@ %db" m.sizeof ; + Option.iter (Format.fprintf fmt "@ (*%a)" pp_node) m.pointed ; + if m.ranges <> [] then + begin + Format.fprintf fmt "@ @[<hv 0>@[<hv 2>{" ; + if Options.debug_atleast 1 then + List.iter (pp_range fmt) m.ranges + else + List.iter (pp_slice m.fields fmt) (span 0 m.sizeof m.ranges) ; + Format.fprintf fmt "@]@ }@]" ; + end ; + if Options.debug_atleast 1 then + begin + List.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.reads ; + List.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.writes ; + List.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.shifts ; + end ; + Format.fprintf fmt " ;@]" ; + end diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli index ea7949d6ed68e8dec78a71b7799140cf93534367..35a2b9d2f8568513e67dc22b3f340f1f511b0372 100644 --- a/src/plugins/region/memory.mli +++ b/src/plugins/region/memory.mli @@ -38,11 +38,13 @@ type region = { roots: varinfo list ; labels: string list ; types: typ list ; + typed : typ option ; fields: Fields.domain ; reads: Access.acs list ; writes: Access.acs list ; shifts: Access.acs list ; sizeof: int ; + singleton : bool ; ranges: range list ; pointed: node option ; } @@ -100,6 +102,7 @@ val index : map -> node -> typ -> node val lval : map -> lval -> node val exp : map -> exp -> node option +val ranges : map -> node -> range list val points_to : map -> node -> node option val pointed_by : map -> node -> node list @@ -110,4 +113,5 @@ val singleton : map -> node -> bool val reads : map -> node -> typ list val writes : map -> node -> typ list val shifts : map -> node -> typ list +val types : map -> node -> typ list val typed : map -> node -> typ option diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml index 243f1975703242f4c9a0158b96c5467f842d8fcd..e5f6ebffe1192ec4dd5ac1b6df0e924eb198b78b 100644 --- a/src/plugins/region/services.ml +++ b/src/plugins/region/services.ml @@ -114,6 +114,7 @@ struct let label (m: Memory.region) = let buffer = Buffer.create 4 in + if m.singleton then Buffer.add_string buffer "!" ; if m.reads <> [] then Buffer.add_char buffer 'R' ; if m.writes <> [] then Buffer.add_char buffer 'W' ; if m.pointed <> None then Buffer.add_char buffer '*' @@ -133,7 +134,7 @@ struct Typ.pretty fmt ty let title (m: Memory.region) = - Format.asprintf "%t (%db)" + Format.asprintf "%t (%db)%t" begin fun fmt -> match m.types with | [] -> Format.pp_print_string fmt "Compound" @@ -141,7 +142,11 @@ struct | ty::ts -> pp_typ_layout 0 fmt ty ; List.iter (Format.fprintf fmt ", %a" (pp_typ_layout 0)) ts ; - end m.sizeof + end + m.sizeof + begin fun fmt -> + if m.singleton then Format.pp_print_string fmt " (singleton)" + end let jtype = Data.declare ~package ~name:"region" @@ Jrecord [ @@ -154,7 +159,8 @@ struct "pointed", NodeOpt.jtype ; "reads", Jboolean ; "writes", Jboolean ; - "bytes", Jboolean ; + "typed", Jboolean ; + "singleton", Jboolean ; "label", Jstring ; "title", Jstring ; ] @@ -170,7 +176,8 @@ struct "pointed", NodeOpt.to_json @@ m.pointed ; "reads", Json.of_bool (m.reads <> []) ; "writes", Json.of_bool (m.writes <> []) ; - "bytes", Json.of_bool (List.length m.types > 1) ; + "typed", Json.of_bool (m.typed <> None) ; + "singleton", Json.of_bool m.singleton ; "label", Json.of_string @@ label m ; "title", Json.of_string @@ title m ; ]