From fe0d215679e74c10db758eefdd5e2211e1d00f0d Mon Sep 17 00:00:00 2001
From: Yeji Han <yeji.han@sf.snu.ac.kr>
Date: Thu, 27 Aug 2026 17:32:28 +0900
Subject: [PATCH] feat(Isla): Support bounded address allocation

Add an optional exclusive limit to the existing linear allocator so callers can partition independently allocated arenas without changing unbounded allocation behavior.
---
 cli/lib/isla/allocator.ml  | 21 +++++++++++++++++----
 cli/lib/isla/allocator.mli |  6 +++---
 2 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/cli/lib/isla/allocator.ml b/cli/lib/isla/allocator.ml
index afb95301..c45461d2 100644
--- a/cli/lib/isla/allocator.ml
+++ b/cli/lib/isla/allocator.ml
@@ -40,7 +40,10 @@
 
 (** Page-oriented address allocator. *)
 
-type t = {mutable current : int}
+type t =
+  { mutable current : int;
+    limit : int option
+  }
 
 let default_base = 0x1000
 
@@ -56,17 +59,27 @@ let align_up addr alignment =
 
 let page_after addr = align_up (addr + 1) page_size
 
-let make ?(base = default_base) ?(reserved = []) () =
+let make ?(base = default_base) ?limit ?(reserved = []) () =
   let current =
     List.fold_left
       (fun current addr -> max current (page_after addr))
       base reserved
   in
-  {current}
+  ( match limit with
+  | Some limit when current > limit ->
+      Litmus.Error.failwith "allocator: initial address exceeds limit"
+  | _ -> ()
+  );
+  {current; limit}
 
 let alloc_aligned allocator ~size ~alignment =
   let addr = align_up allocator.current alignment in
-  allocator.current <- addr + size;
+  let next = addr + size in
+  ( match allocator.limit with
+  | Some limit when next > limit ->
+      Litmus.Error.failwith "allocator: limit exceeded"
+  | _ -> allocator.current <- next
+  );
   addr
 
 let alloc_page allocator =
diff --git a/cli/lib/isla/allocator.mli b/cli/lib/isla/allocator.mli
index c9214ccd..819124df 100644
--- a/cli/lib/isla/allocator.mli
+++ b/cli/lib/isla/allocator.mli
@@ -48,9 +48,9 @@ val page_size : int
 (** Size of one block (2MB) allocated by [alloc_big]. *)
 val big_size : int
 
-(** Make an allocator, optionally with reserved addresses. Each reserved
-    address blocks the page containing it. *)
-val make : ?base:int -> ?reserved:int list -> unit -> t
+(** Make an allocator, optionally with an exclusive upper limit and reserved
+    addresses. Each reserved address blocks the page containing it. *)
+val make : ?base:int -> ?limit:int -> ?reserved:int list -> unit -> t
 
 (** Allocate [size] bytes at an address aligned to [alignment]. *)
 val alloc_aligned : t -> size:int -> alignment:int -> int