From d1bb7e5ea8861236cca73cbbb47b31d75d859f8a Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc_mak@outlook.com>
Date: Wed, 16 Aug 2023 20:17:18 +0100
Subject: [PATCH] Add alloc to create/kill checking

---
 backend/cn/check.ml          | 5 +++++
 backend/cn/compile.ml        | 7 +++++++
 backend/cn/core_to_mucore.ml | 5 +++--
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/backend/cn/check.ml b/backend/cn/check.ml
index f105d65f5..0dda66fd1 100644
--- a/backend/cn/check.ml
+++ b/backend/cn/check.ml
@@ -1185,6 +1185,8 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr)
                }, 
              O (default_ (BT.of_sct act.ct)))
         in
+        let@ () =
+          add_r loc (P (Global.mk_alloc ret), O IT.unit_) in
         k ret)
      | M_CreateReadOnly (sym1, ct, sym2, _prefix) -> 
         Cerb_debug.error "todo: CreateReadOnly"
@@ -1203,6 +1205,9 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr)
             iargs = [];
           }, None)
         in
+        let@ _ =
+          RI.Special.predicate_request loc (Access Kill) (Global.mk_alloc arg, None)
+        in
         k unit_)
      | M_Store (_is_locking, act, p_pe, v_pe, mo) -> 
         let@ () = WellTyped.ensure_base_type loc ~expect Unit in
diff --git a/backend/cn/compile.ml b/backend/cn/compile.ml
index c9f7d3213..657891092 100644
--- a/backend/cn/compile.ml
+++ b/backend/cn/compile.ml
@@ -1037,6 +1037,13 @@ let ownership (loc, (addr_s, ct)) env =
   let value = IT.sym_ (name, oa_bt) in
   return (name, ((pt_ret, oa_bt), lcs), value)
 
+let allocation_token loc addr_s =
+  let name = match Sym.description addr_s with
+    | SD_ObjectAddress obj_name ->
+       Sym.fresh_make_uniq ("A_"^obj_name)
+    | _ -> assert false in
+  let alloc_ret = Global.mk_alloc (IT.sym_ (addr_s, BT.Loc)) in
+  ((name, (ResourceTypes.P alloc_ret, BT.Unit)), (loc, None))
 
 
 
diff --git a/backend/cn/core_to_mucore.ml b/backend/cn/core_to_mucore.ml
index ce302303f..1177910d3 100644
--- a/backend/cn/core_to_mucore.ml
+++ b/backend/cn/core_to_mucore.ml
@@ -928,9 +928,10 @@ let make_label_args f_i loc env st args (accesses, inv) =
        let@ (oa_name, ((pt_ret, oa_bt), lcs), value) = C.ownership (loc, (s, ct)) env in
        let env = C.add_logical oa_name oa_bt env in
        let st = C.LocalState.add_c_variable_state s (CVS_Pointer_pointing_to value) st in
-       let resource = ((oa_name, (pt_ret, SBT.to_basetype oa_bt)), (loc, None)) in
+       let owned_res = ((oa_name, (pt_ret, SBT.to_basetype oa_bt)), (loc, None)) in
+       let alloc_res = C.allocation_token loc s in
        let@ at = 
-         aux (resources @ [resource], 
+         aux (resources @ [alloc_res; owned_res],
               good_lcs @ good_pointer_lc :: lcs) 
            env st rest 
        in