[region] use smallest fields

src/plugins/region/fields.ml

@@ -32,11 +32,11 @@ let union = Domain.union
 let empty = Domain.empty
 let singleton (fd : fieldinfo) = Domain.singleton fd.fcomp
 
-(* minimal offset first, then maximal length, then largest struct *)
+(* minimal offset first, then minimal length, then largest struct *)
 let compare (a : field) (b : field) =
   let cmp = a.offset - b.offset in
   if cmp <> 0 then cmp else
-    let cmp = b.length - a.length in
+    let cmp = a.length - b.length in
     if cmp <> 0 then cmp else
       let sa = Cil.bitsSizeOf (TComp(a.data.fcomp,[])) in
       let sb = Cil.bitsSizeOf (TComp(b.data.fcomp,[])) in
@@ -64,20 +64,6 @@ let find fields rg =
 
 type slice = Bits of int | Field of fieldinfo
 
-let delta (a : _ range) (b : _ range) =
-  let p = a.offset + a.length in
-  let q = b.offset in
-  if p < q then [Bits (q - p)] else []
-
-let span fields rg =
-  match find_all fields rg with
-  | [] -> [Bits rg.length]
-  | fr :: frs ->
-    delta rg fr @ [Field fr.data] @
-    match List.rev frs with
-    | [] -> delta fr rg
-    | lr :: _ -> delta fr lr @ [Field lr.data] @ delta lr rg
-
 let pp_bits fmt n =
   if n <> 0 then Format.fprintf fmt "#%db" n
 
@@ -85,6 +71,25 @@ let pp_slice fmt = function
   | Bits n -> pp_bits fmt n
   | Field fd -> Format.fprintf fmt ".%s" fd.fname
 
+let pad p q s =
+  let n = q - p in
+  if n > 0 then Bits n :: s else s
+
+let last (rg : _ range) = rg.offset + rg.length
+
+let span fields rg =
+  match find_all fields rg with
+  | [] -> [Bits rg.length]
+  | fr :: frs ->
+    pad rg.offset fr.offset @@
+    Field fr.data ::
+    let p = last fr in
+    let q = last rg in
+    match List.rev @@ List.filter (fun r -> p <= r.offset) frs with
+    | [] -> pad p q []
+    | lr :: _ ->
+      pad p lr.offset @@ Field lr.data :: pad (last lr) q []
+
 let pretty fields fmt rg =
   List.iter (pp_slice fmt) @@ span fields rg
 

src/plugins/region/memory.ml

@@ -236,19 +236,21 @@ type region = {
 }
 
 let pp_cells fmt = function
-| 1 -> ()
-| 0 -> Format.fprintf fmt "[…]"
-| n -> Format.fprintf fmt "[%d]" n
+  | 1 -> ()
+  | 0 -> Format.fprintf fmt "[…]"
+  | n -> Format.fprintf fmt "[%d]" n
 
 type slice =
   | Padding of int
   | Range of range
 
-let pad n s = if n > 0 then Padding n :: s else s
+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 (s-k) []
-  | r::rs -> pad (r.offset - k) @@ Range r :: span (r.offset + r.length) s rs
+  | [] -> 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 ->
@@ -259,6 +261,10 @@ let pp_slice fields fmt = function
       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
@@ -273,7 +279,10 @@ let pp_region fmt (m: region) =
     if m.ranges <> [] then
       begin
         Format.fprintf fmt "@ @[<hv 0>@[<hv 2>{" ;
-        List.iter (pp_slice m.fields fmt) (span 0 m.sizeof m.ranges) ;
+        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