Removing the constraint on overwriteable instructions

herd/AArch64Sem.ml

@@ -2692,61 +2692,57 @@ module Make
       let check_self test ii =
         let module InstrSet = AArch64.V.Cst.Instr.Set in
         let inst = ii.A.inst in
-        if not (AArch64Base.is_overwritable inst) then
-          do_build_semantics test inst ii
-        else
-          let lbls = get_exported_labels test in
-          let is_exported =
-            Label.Set.exists
-              (fun lbl ->
-                Label.Full.Set.exists
-                  (fun (_,lbl0) -> Misc.string_eq lbl lbl0)
-                  lbls)
-              ii.A.labels in
-          if is_exported then
-            match Label.norm ii.A.labels with
-            | None -> assert false
-            | Some hd ->
-                let insts =
-                  InstrSet.of_list
-                    (get_overwriting_instrs lbls test) in
-                let insts =
-                  InstrSet.add inst
-                    (InstrSet.filter AArch64.can_overwrite insts) in
-                if false then
-                  Printf.eprintf "%s: {%s}\n%!"
-                    (Label.pp hd)
-                    (String.concat ","
-                       (List.map AArch64.V.Cst.Instr.pp
-                          (InstrSet.elements insts))) ;
-                (* Shadow default control sequencing operator *)
-                let(>>*=) = M.bind_control_set_data_input_first in
-                let a_v = make_label_value ii.A.fetch_proc hd in
-                let a = (* Normalised address of instruction *)
-                  A.Location_global a_v in
-                read_loc_instr a ii
-                  >>= fun actual_val ->
-                    InstrSet.fold
-                      (fun inst k ->
-                        M.op Op.Eq actual_val (V.instructionToV inst) >>==
-                        fun cond -> M.choiceT cond
-                            (commit_pred ii >>*=
-                             fun () -> do_build_semantics test inst ii)
-                            k)
-                      insts
-                      begin
-(* Anything else than a legit instruction is a failure *)
-                        let (>>!) = M.(>>!) in
-                        let m_fault =
-                          mk_fault
-                            None Dir.R AArch64.N ii
-                            (Some FaultType.AArch64.UndefinedInstruction)
-                            (Some "Invalid") in
-                        commit_pred ii
-                          >>*= fun () -> m_fault >>| set_elr_el1 ii
-                            >>! B.Fault Dir.R
-                      end
-          else do_build_semantics test inst ii
+        let lbls = get_exported_labels test in
+        let is_exported =
+          Label.Set.exists
+            (fun lbl ->
+              Label.Full.Set.exists
+                (fun (_,lbl0) -> Misc.string_eq lbl lbl0)
+                lbls)
+            ii.A.labels in
+        if is_exported then
+          match Label.norm ii.A.labels with
+          | None -> assert false
+          | Some hd ->
+              let insts =
+                InstrSet.of_list
+                  (get_overwriting_instrs lbls test) in
+              let insts =
+                InstrSet.add inst (InstrSet.filter AArch64.can_overwrite insts) in
+              if false then
+                Printf.eprintf "%s: {%s}\n%!"
+                  (Label.pp hd)
+                  (String.concat ","
+                      (List.map AArch64.V.Cst.Instr.pp
+                        (InstrSet.elements insts))) ;
+              (* Shadow default control sequencing operator *)
+              let(>>*=) = M.bind_control_set_data_input_first in
+              let a_v = make_label_value ii.A.fetch_proc hd in
+              let a = (* Normalised address of instruction *)
+                A.Location_global a_v in
+              read_loc_instr a ii
+                >>= fun actual_val ->
+                  InstrSet.fold
+                    (fun inst k ->
+                      M.op Op.Eq actual_val (V.instructionToV inst) >>==
+                      fun cond -> M.choiceT cond
+                          (commit_pred ii >>*=
+                            fun () -> do_build_semantics test inst ii)
+                          k)
+                    insts
+                    begin
+  (* Anything else than a legit instruction is a failure *)
+                      let (>>!) = M.(>>!) in
+                      let m_fault =
+                        mk_fault
+                          None Dir.R AArch64.N ii
+                          (Some FaultType.AArch64.UndefinedInstruction)
+                          (Some "Invalid") in
+                      commit_pred ii
+                        >>*= fun () -> m_fault >>| set_elr_el1 ii
+                          >>! B.Fault Dir.R
+                    end
+        else do_build_semantics test inst ii
 
       let build_semantics test ii =
         M.addT (A.next_po_index ii.A.program_order_index)

herd/mem.ml

@@ -321,15 +321,10 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
               List.fold_left
                 (fun (ps, ls) (addr,i) ->
                   let lbls = labels_of_instr addr in
-                  let is_overwritable = A.V.Cst.Instr.is_overwritable i in
-                  if
-                    Label.Set.exists is_exported_label lbls ||
-                    is_overwritable
+                  if Label.Set.exists is_exported_label lbls
                   then
-                    if Label.Set.is_empty lbls then ps,ls
-                    else
                       (lbls,(proc,i))::ps,
-                      (if is_overwritable then Label.Set.union lbls ls else ls)
+                      Label.Set.union lbls ls
                   else ps,ls)
                 (ps,ls) code)
             ([], Label.Set.empty) starts

herd/tests/instructions/AArch64.self/A007.litmus.expected

@@ -0,0 +1,11 @@
+Test A007 Allowed
+States 2
+0:X2=1;
+0:X2=2;
+Ok
+Witnesses
+Positive: 1 Negative: 1
+Condition exists (0:X2=1)
+Observation A007 Sometimes 1 1
+Hash=77032c0be8690b2b66d8c9f20e2a5363
+

herd/tests/instructions/AArch64.self/A010.litmus.expected

@@ -0,0 +1,11 @@
+Test A010 Allowed
+States 2
+0:X2=1;
+0:X2=2;
+Ok
+Witnesses
+Positive: 1 Negative: 1
+Condition exists (0:X2=1)
+Observation A010 Sometimes 1 1
+Hash=77b235b3243a7010216394415245557e
+

herd/tests/instructions/AArch64.self/S23.litmus.expected

@@ -0,0 +1,11 @@
+Test S23 Required
+States 2
+t={1,3};
+t={3,2};
+Ok
+Witnesses
+Positive: 2 Negative: 0
+Condition forall (true)
+Observation S23 Always 2 0
+Hash=b5828ee8a20d1f9c72c22257755f5515
+

lib/AArch64Base.ml

@@ -2197,13 +2197,6 @@ let loop_idx = Internal 4
 
 let hash_pteval p = AArch64PteVal.pp_hash (AArch64PteVal.tr p)
 
-(* For performance reasons, overwritable sites are limited *)
-let is_overwritable = function
-  |I_NOP| I_B _|I_BC _|I_BL _|I_CBNZ _
-  |I_CBZ _|I_FENCE ISB|I_TBNZ _|I_TBZ _
-   -> true
-  | _ -> false
-
 (*
  * The set of overwriting instruction is more extensive.
  * Only branches to explicit labels are excluded, as their direct
@@ -2283,8 +2276,7 @@ module
     | I_UDF _| I_UNSEAL _
   -> true
 
-  let is_overwritable = is_overwritable
-  and can_overwrite =  can_overwrite
+  let can_overwrite =  can_overwrite
   and get_exported_label = get_exported_label
 
   module Set =

lib/instr.ml

@@ -23,7 +23,6 @@ module type S = sig
   val nop : t option
   val is_nop : t -> bool
   val needs_cmodx : t -> bool
-  val is_overwritable : t -> bool
   val can_overwrite : t -> bool
   val get_exported_label : t -> Label.t option
 
@@ -44,7 +43,6 @@ module No (I:sig type instr end) = struct
   let nop = None
   let is_nop _ = fail "is_nop"
   let needs_cmodx _ = fail "needs_cmodx"
-  let is_overwritable _ = false
   let can_overwrite _ = false
   let get_exported_label _ = None
 
@@ -76,7 +74,7 @@ module
       fail ("litteral instruction " ^ InstrLit.pp i)
     let nop = Some I.nop
     let is_nop i = eq i I.nop
-    let is_overwritable _ = false
+    let needs_cmodx _ = false
     let can_overwrite _ = false
     let get_exported_label _ = None
 

lib/instr.mli

@@ -24,7 +24,6 @@ module type S = sig
   val nop : t option
   val is_nop : t -> bool
   val needs_cmodx : t -> bool
-  val is_overwritable : t -> bool
   val can_overwrite : t -> bool
   val get_exported_label : t -> Label.t option