[herd] Addressing review comments

Author: artkhyzha

herd/AArch64Sem.ml

@@ -1600,8 +1600,25 @@ module Make
         | None -> false
         | Some rB -> AArch64.reg_compare rA rB=0
 
+(*
+Arguments:
+- rA:         Base address register.
+- dir:        Access direction (Dir.R for reads, Dir.W for writes).
+- updatedb:   If true, update the Dirty Bit in table descriptors.
+- checked:    If true, perform memory tagging checks.
+- mop:        Function defining the memory operation.
+- perms:      Required permissions for Morello.
+- ma:         Virtual address to be accessed, represented as the value within the monad.
+- mv:         Value to be stored (for write operations), represented as the value in the monad.
+- an:         Annotation for the event structure.
+- ii:         Instruction metadata.
+- branch:     Determines control flow after the translated memory access:
+              typically next instruction for data accesses, or no change
+              when translating for instruction fetches. 
+- domain:     Whether the translation is for data or instruction access.
+*)
       let do_lift_memop rA (* Base address register *)
-            dir updatedb checked mop perms ma mv an ii (branch : 'a M.t -> branch M.t) domain =
+            dir updatedb checked mop perms ma mv an ii branch domain =
         if morello then
           lift_morello mop perms ma mv dir an ii branch
         else
@@ -1631,19 +1648,6 @@ module Make
           else
             mop Access.VIR ma |> branch
 
-(*
-Arguments:
-- rA:         Base address register.
-- dir:        Access direction (Dir.R for reads, Dir.W for writes).
-- updatedb:   If true, update the Dirty Bit in table descriptors.
-- checked:    If true, perform memory tagging checks.
-- mop:        Function defining the memory operation.
-- perms:      Required permissions for Morello.
-- ma:         Virtual address to be accessed, represented as the value within the monad.
-- mv:         Value to be stored (for write operations), represented as the value in the monad.
-- an:         Annotation for the event structure.
-- ii:         Instruction metadata.
-*)
       let lift_memop rA (* Base address register *)
             dir updatedb checked mop perms ma mv an ii =
         let domain = DISide.Data in
@@ -4731,7 +4735,10 @@ Arguments:
                 let cand_a = base + offset in
                 let cand_i = match IntMap.find cand_a test.Test_herd.code_segment with
                 | (_,(_,i)::_) -> i
-                  | _ -> Warn.user_error "Instruction not found by the address %d" cand_a (* this case means that we have found a relevant page, but it does not have an instruction -- it may make sense to use NOP here rather than throw an error *)
+                  (* this case means that we have found a relevant page, but it
+                  does not have an instruction -- currently throws an error, but
+                  a convention to assume NOP could be envisioned *)
+                  | _ -> Warn.user_error "Instruction not found by the address %d" cand_a
                 in
                 cand_i)
              |> InstrSet.of_list
@@ -4772,7 +4779,7 @@ Arguments:
               (fun inst k ->
                 M.op Op.Eq actual_val (V.instructionToV inst) >>==
                 fun cond -> M.choiceT cond
-                    (commit_pred ii >>*=
+                    (commit_pred_txt (Some "decode") ii >>*=
                       fun () -> do_build_semantics test inst ii)
                     k)
               cands
@@ -4781,9 +4788,9 @@ Arguments:
                 let (>>!) = M.(>>!) in
                 let m_fault = mk_fault None Dir.R Annot.N ii
                     (Some FaultType.AArch64.UndefinedInstruction)
-                    (Some "Invalid") in
+                    None in
                 let lbl_v = get_instr_label ii.A.proc ii in
-                commit_pred ii
+                commit_pred_txt (Some "decode") ii
                   >>*= fun () -> m_fault >>| set_elr_el1 lbl_v ii
                   >>! B.Fault (false,[AArch64Base.elr_el1, lbl_v])
               end in
@@ -4823,9 +4830,10 @@ Arguments:
                 (get_exported_labels test))
             labels in
 
-        let needs_vmsa_for_ifetch =
+        let needs_vmsa_for_ifetch = (* checks if the logic for VA remapping needed *)
           kvm && self && is_on_exported_page in
-        let needs_ifetch = (lbl_exposed ii.A.addr) && self in
+        let needs_ifetch = (* checks if the logic for instruction overwrite needed *)
+          (lbl_exposed ii.A.addr) && self in
         if needs_ifetch || needs_vmsa_for_ifetch then
           try (
             let mop_fetch = mk_mop_fetch is_on_exported_page lbl_exposed test ii in

herd/loader.ml

@@ -114,7 +114,9 @@ struct
     let offset = new_addr - old_addr in
     let immbranch_v = Option.get (A.mk_imm_branch offset) in
     let immbranch_sz = A.size_of_ins immbranch_v in
-    assert (offset mod 4 = 0); (* FIXME: this check will fail when page alignment is implemented on architectures where instructions are not all 32-bit-sized *)
+    (* NOTE: the following check will fail once page alignment is implemented on
+    architectures where instructions are not all 32-bit-sized *)
+    assert (offset mod 4 = 0);
     if offset == 0 then
       []
     else if offset == immbranch_sz then

herd/mem.ml

@@ -1329,7 +1329,7 @@ let match_reg_events es =
         with
         | Some (V.Var _) -> true
         | Some (V.Val (Symbolic (Virtual {name=n;_}))) when Symbol.is_label n -> true
-        | Some (V.Val (Symbolic (Physical (s,_)))) when (s |> Symbol.of_string |> Symbol.is_label) -> true (* FIXME: this benefits from a proper exposition of a label as a physical address *)
+        | Some (V.Val (Symbolic (Physical (s,_)))) when (s |> Symbol.of_string |> Symbol.is_label) -> true
         | Some _|None -> false
       in
       let is_to_instr_ttd e =

herd/semExtra.ml

@@ -91,8 +91,6 @@ module type S = sig
 (* "Exposed" TTDs of code pages, i.e. TTDs whose addresses are in registers *)
   (* In initial state *)
   val get_exposed_codepages : test -> (A.V.Cst.Scalar.t, A.V.Cst.PteVal.t, A.V.Cst.AddrReg.t, A.instruction) Constant.t list
-(* "Exposed" TTDs, i.e. TTDs whose values are in registers *)
-  val get_exposed_codepage_mappings : test -> (A.V.Cst.Scalar.t, A.V.Cst.PteVal.t, A.V.Cst.AddrReg.t, A.instruction) Constant.t list
 
   type event = E.event
   type event_structure = E.event_structure
@@ -362,25 +360,6 @@ module Make(C:Config) (A:Arch_herd.S) (Act:Action.S with module A = A)
           )
         st []
 
-    let get_exposed_codepage_mappings test =
-      let { Test_herd.init_state=st; _ } = test in
-      A.state_fold
-        (fun _ v k ->
-          match v with
-          | V.Val (Constant.PteVal pte_v) -> begin
-            match V.Cst.PteVal.as_physical pte_v with
-            | Some str -> begin
-              match Misc.str_as_label str with
-                  | Some (proc, lblname) ->
-                    (Constant.mk_sym_virtual_label_with_offset proc lblname 0)::k
-                  | None -> k
-              end
-            | None -> k
-            end
-          | V.Val _ | V.Var _ -> k)
-        st []
-
-
 (**********)
 (* Events *)
 (**********)