CN VIP: Use record for base and size in Alloc

backend/cn/lib/alloc.ml

@@ -27,10 +27,16 @@ module History = struct
     IndexTerms.(map_get_ (it loc') (allocId_ ptr loc') loc')
 
 
-  let get_base_size ptr loc' =
+  type value =
+    { base : IndexTerms.t;
+      size : IndexTerms.t
+    }
+
+  let split value loc' =
     IndexTerms.
-      ( recordMember_ ~member_bt:base_bt (ptr, base_id) loc',
-        recordMember_ ~member_bt:size_bt (ptr, size_id) loc' )
+      { base = recordMember_ ~member_bt:base_bt (value, base_id) loc';
+        size = recordMember_ ~member_bt:size_bt (value, size_id) loc'
+      }
 
 
   let sbt = BaseTypes.Surface.inj bt

backend/cn/lib/alloc.mli

@@ -21,7 +21,12 @@ module History : sig
 
   val lookup_ptr : IndexTerms.t -> Locations.t -> IndexTerms.t
 
-  val get_base_size : IndexTerms.t -> Cerb_location.t -> IndexTerms.t * IndexTerms.t
+  type value =
+    { base : IndexTerms.t;
+      size : IndexTerms.t
+    }
+
+  val split : IndexTerms.t -> Cerb_location.t -> value
 
   val sbt : BaseTypes.Surface.t
 end

backend/cn/lib/check.ml

@@ -437,8 +437,8 @@ let check_has_alloc_id loc ptr ub_unspec =
 let check_alloc_bounds loc ~ptr ub_unspec =
   if !use_vip then (
     let here = Locations.other __FUNCTION__ in
-    let base_size = Alloc.History.lookup_ptr ptr here in
-    let base, size = Alloc.History.get_base_size base_size here in
+    let module H = Alloc.History in
+    let H.{ base; size } = H.(split (lookup_ptr ptr here) here) in
     let addr = addr_ ptr here in
     let lower = le_ (base, addr) here in
     let upper = le_ (addr, add_ (base, size) here) here in
@@ -476,7 +476,7 @@ let check_both_eq_alloc loc arg1 arg2 ub =
 let check_live_alloc_bounds reason loc arg ub term constr =
   let@ base_size = RI.Special.get_live_alloc reason loc arg in
   let here = Locations.other __FUNCTION__ in
-  let base, size = Alloc.History.get_base_size base_size here in
+  let Alloc.History.{ base; size } = Alloc.History.split base_size here in
   if !use_vip then (
     let constr = constr ~base ~size in
     let@ provable = provable loc in
@@ -2298,9 +2298,9 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m =
         let ptr = sym_ (sym, bt, here) in
         let@ () = add_c here (LC.T (IT.hasAllocId_ ptr here)) in
         let@ () =
-          if !IT.use_vip then (
-            let base_size = Alloc.History.lookup_ptr ptr here in
-            let base, size = Alloc.History.get_base_size base_size here in
+          if !IT.use_vip then
+            let module H = Alloc.History in
+            let H.{ base; size } = H.(split (lookup_ptr ptr here) here) in
             let addr = addr_ ptr here in
             let upper = Resources.upper_bound addr ct here in
             let bounds =
@@ -2311,7 +2311,7 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m =
                 ]
                 here
             in
-            add_c here (LC.T bounds))
+            add_c here (LC.T bounds)
           else
             return ()
         in

backend/cn/lib/resources.ml

@@ -44,17 +44,18 @@ let derived_lc1 (resource, O oarg) =
     let addr = IT.addr_ pointer here in
     let upper = upper_bound addr ct here in
     let alloc_bounds =
-      if !IT.use_vip then (
-        let lookup = Alloc.History.lookup_ptr pointer here in
-        let base, size = Alloc.History.get_base_size lookup here in
-        [ IT.(le_ (base, addr) here); IT.(le_ (upper, add_ (base, size) here) here) ])
+      if !IT.use_vip then
+        let module H = Alloc.History in
+        let H.{ base; size } = H.(split (lookup_ptr pointer here) here) in
+        [ IT.(le_ (base, addr) here); IT.(le_ (upper, add_ (base, size) here) here) ]
       else
         []
     in
     [ IT.hasAllocId_ pointer here; IT.(le_ (addr, upper) here) ] @ alloc_bounds
   | P { name; pointer; iargs = [] } when !IT.use_vip && equal_predicate_name name alloc ->
-    let lookup = Alloc.History.lookup_ptr pointer here in
-    let base, size = Alloc.History.get_base_size lookup here in
+    let module H = Alloc.History in
+    let lookup = H.lookup_ptr pointer here in
+    let H.{ base; size } = H.split lookup here in
     [ IT.(eq_ (lookup, oarg) here); IT.(le_ (base, add_ (base, size) here) here) ]
   | Q { name = Owned _; pointer; _ } -> [ IT.hasAllocId_ pointer here ]
   | P { name = PName _; pointer = _; iargs = _ } | Q { name = PName _; _ } -> []