CLI: Parse isla's section part

Author: febyeji

cli/lib/isla/converter.ml

@@ -154,9 +154,21 @@ let build_data_memory syms sym addr init_value =
   }
 
 let to_testrepr (ir : Ir.t) : Testrepr.t =
+  (* Assemble sections first and reserve their address ranges *)
+  let assembled_sections =
+    List.map
+      (fun (sec : Ir.section) ->
+        let enc = Assembler.assemble sec.code in
+        (sec, enc))
+      ir.sections
+  in
   let syms = Symbols.empty () in
+  List.iter
+    (fun (sec, enc) ->
+      Symbols.reserve syms sec.Ir.address (Bytes.length enc))
+    assembled_sections;
   List.iter (Symbols.alloc_sym syms) ir.symbolic;
-  let encoded_threads =
+  let assembled_threads =
     List.map
       (fun (thread : Ir.thread) ->
         let enc = Assembler.assemble thread.code in
@@ -169,12 +181,17 @@ let to_testrepr (ir : Ir.t) : Testrepr.t =
     List.map
       (fun (thread, _, code_addr) ->
         build_registers syms ~arch:ir.arch code_addr thread)
-      encoded_threads
+      assembled_threads
   in
   let code_memory =
     List.map
       (fun (_, enc, code_addr) -> build_code_memory ~step:code_step code_addr enc)
-      encoded_threads
+      assembled_threads
+  in
+  let section_memory =
+    List.map
+      (fun (sec, enc) -> build_code_memory ~step:code_step sec.Ir.address enc)
+      assembled_sections
   in
   let data_memory =
     List.map (fun sym ->
@@ -202,7 +219,7 @@ let to_testrepr (ir : Ir.t) : Testrepr.t =
       (fun (_, enc, code_addr) ->
         let end_pc = Z.of_int (code_addr + Bytes.length enc) in
         [(pc, RegValGen.Number end_pc)])
-      encoded_threads
+      assembled_threads
   in
   let finals =
     to_final_conds
@@ -215,7 +232,7 @@ let to_testrepr (ir : Ir.t) : Testrepr.t =
     arch = Litmus.Arch_id.to_string ir.arch;
     name = ir.name;
     registers;
-    memory = code_memory @ data_memory;
+    memory = code_memory @ section_memory @ data_memory;
     term_cond;
     finals;
   }

cli/lib/isla/ir.ml

@@ -12,6 +12,12 @@ type thread = {
   init : (string * value) list;
 }
 
+type section = {
+  sec_name : string;
+  address : int;
+  code : string;
+}
+
 type expect =
   | Sat
   | Unsat
@@ -20,6 +26,7 @@ type t = {
   arch : Litmus.Arch_id.t;
   name : string;
   threads : thread list;
+  sections : section list;
   symbolic : string list;
   locations : (string * value) list;
   expect : expect;
@@ -53,6 +60,27 @@ let parse_threads toml =
   let table = Otoml.get_table toml in
   List.sort (fun a b -> compare a.tid b.tid) (List.map parse_thread table)
 
+let parse_address = function
+  | Otoml.TomlInteger i -> i
+  | Otoml.TomlString s ->
+    (try Z.to_int (Z.of_string s)
+     with Invalid_argument _ ->
+       raise (Otoml.Type_error ("invalid address: " ^ s)))
+  | v ->
+    raise (Otoml.Type_error
+      ("address must be integer or hex string, got: " ^
+       Otoml.Printer.to_string v))
+
+let parse_section (name, table) =
+  let _ = Otoml.get_table table in
+  let address = Otoml.find table parse_address ["address"] in
+  let code = Otoml.find table Otoml.get_string ["code"] |> String.trim in
+  { sec_name = name; address; code }
+
+let parse_sections toml =
+  let table = Otoml.get_table toml in
+  List.map parse_section table
+
 let parse_expect toml =
   match Otoml.get_string toml with
   | "sat" -> Sat
@@ -85,6 +113,8 @@ let of_toml toml =
     arch = Otoml.find toml parse_arch ["arch"];
     name = Otoml.find_or ~default:"unknown" toml Otoml.get_string ["name"];
     threads = Otoml.find toml parse_threads ["thread"];
+    sections =
+      Otoml.find_or ~default:[] toml parse_sections ["section"];
     symbolic =
       Otoml.find_or ~default:[] toml (Otoml.get_array Otoml.get_string) ["symbolic"];
     locations = Otoml.find_or ~default:[] toml (Otoml.get_table_values parse_value) ["locations"];

cli/lib/isla/symbols.ml

@@ -3,6 +3,7 @@
 type t = {
   mutable next_addr : int;
   mutable table : (string * int) list;
+  mutable reserved : (int * int) list;  (** (addr, size) pairs for reserved ranges *)
 }
 
 let resolve_opt t name = List.assoc_opt name t.table
@@ -26,12 +27,25 @@ let base_addr () =
 let empty () = {
   next_addr = base_addr ();
   table = [];
+  reserved = [];
 }
 
+let overlaps addr size (r_addr, r_size) =
+  addr < r_addr + r_size && r_addr < addr + size
+
+let reserve t addr size =
+  t.reserved <- (addr, size) :: t.reserved
+
 let alloc_page t =
   let page_size = page_size () in
-  let addr = t.next_addr in
-  t.next_addr <- (addr + page_size);
+  let rec find_free addr =
+    if List.exists (overlaps addr page_size) t.reserved then
+      find_free (addr + page_size)
+    else
+      addr
+  in
+  let addr = find_free t.next_addr in
+  t.next_addr <- addr + page_size;
   addr
 
 let alloc_sym t name =

cli/tests/unit/isla/converter_test.ml

@@ -135,6 +135,27 @@ let tests =
         }
       in
       assert_equal expected (convert mp_toml));
+    "section: assembled at explicit address" >:: (fun _ ->
+      Test_utils.setup ();
+      let toml = Otoml.Parser.from_string {|
+arch = "AArch64"
+name = "WithSection"
+symbolic = ["x"]
+
+[thread.0]
+init = { X0 = "x" }
+code = "NOP"
+
+[section.handler]
+address = "0x1400"
+code = "MOV X2, #1"
+|} in
+      let repr = convert toml in
+      let sec_block =
+        List.find (fun (b : Testrepr.memory_block) -> b.addr = 0x1400) repr.memory
+      in
+      assert_equal Testrepr.Code sec_block.kind;
+      assert_equal 4 (Bytes.length sec_block.data));
     "e2e: SimpleStore seq" >:: (fun _ ->
       Test_utils.setup ();
       let result, _msgs =

cli/tests/unit/isla/ir_test.ml

@@ -28,6 +28,13 @@ code = """
   STR W0,[X1]
 """
 
+[section.el1_handler]
+address = "0x1400"
+code = """
+  MOV X2, #1
+  ERET
+"""
+
 [final]
 expect = "sat"
 assertion = "1:X0 = 1 & *y = 1"
@@ -51,6 +58,8 @@ let expected : Isla.Ir.t =
           init = [ ("X1", Isla.Ir.Sym "y"); ("X2", Isla.Ir.Sym "x") ];
         };
       ];
+    sections =
+      [{ sec_name = "el1_handler"; address = 0x1400; code = "MOV X2, #1\n  ERET" }];
     symbolic = [ "x"; "y" ];
     locations = [ ("x", Isla.Ir.Int Z.zero); ("y", Isla.Ir.Int Z.zero) ];
     expect = Isla.Ir.Sat;

cli/tests/unit/isla/normalize_test.ml

@@ -15,6 +15,7 @@ let sample_ir arch : Isla.Ir.t =
           init = [ ("X0", Isla.Ir.Sym "x"); ("W2", Isla.Ir.Int (Z.of_int 3)) ];
         };
       ];
+    sections = [{ sec_name = "handler"; address = 0x1400; code = "MOV X2, #1" }];
     symbolic = [ "x" ];
     locations = [ ("x", Isla.Ir.Int Z.zero) ];
     expect = Isla.Ir.Sat;

cli/tests/unit/isla/symbols_test.ml

@@ -31,6 +31,34 @@ let tests =
       let a1 = Isla.Symbols.resolve_or_alloc s0 "x" in
       let a2 = Isla.Symbols.resolve_or_alloc s0 "x" in
       assert_equal a1 a2);
+    "alloc skips reserved range" >:: (fun _ ->
+      Test_utils.setup ();
+      let s = Isla.Symbols.empty () in
+      Isla.Symbols.reserve s 0x500 4;
+      let addr = Isla.Symbols.resolve_or_alloc s "x" in
+      assert_equal 0x1500 addr);
+    "alloc skips multiple reserved ranges" >:: (fun _ ->
+      Test_utils.setup ();
+      let s = Isla.Symbols.empty () in
+      Isla.Symbols.reserve s 0x500 4;
+      Isla.Symbols.reserve s 0x1500 4;
+      let addr = Isla.Symbols.resolve_or_alloc s "x" in
+      assert_equal 0x2500 addr);
+    "alloc skips reserved then continues normally" >:: (fun _ ->
+      Test_utils.setup ();
+      let s = Isla.Symbols.empty () in
+      Isla.Symbols.reserve s 0x500 4;
+      let a1 = Isla.Symbols.resolve_or_alloc s "x" in
+      let a2 = Isla.Symbols.resolve_or_alloc s "y" in
+      assert_equal 0x1500 a1;
+      assert_equal 0x2500 a2);
+    "reserved range overlapping middle of page skips it" >:: (fun _ ->
+      Test_utils.setup ();
+      let s = Isla.Symbols.empty () in
+      (* reserve range that overlaps with the first page [0x500, 0x1500) *)
+      Isla.Symbols.reserve s 0x1000 0x100;
+      let addr = Isla.Symbols.resolve_or_alloc s "x" in
+      assert_equal 0x1500 addr);
   ]
 
 let () = run_test_tt_main tests