Add alloc to create/kill checking

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

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))
 
 
 

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