[herd] Use "static" po indices when rendering execution graphs

herd/AArch64Sem.ml

@@ -4758,7 +4758,7 @@ Arguments:
                 let base = Label.Map.find lbl test.Test_herd.program in
                 let cand_a = base + offset in
                 let cand_i = match IntMap.find cand_a test.Test_herd.code_segment with
-                | (_,(_,i)::_) -> i
+                | (_,(_,i)::_) -> i.A.CodeInstr.instr
                 (* 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 *)

herd/Pretty.ml

@@ -827,7 +827,7 @@ module Make (S:SemExtra.S) : S with module S = S  = struct
   | E.IdSome ii ->
       fprintf chan "proc:%s poi:%i\\l"
         (Proc.pp ii.A.proc)
-        ii.A.program_order_index
+        ii.A.static_poi
 
 (*
   This complex function is not meant to be used directly,

herd/archExtra_herd.ml

@@ -74,8 +74,12 @@ module type S = sig
    the test, such as its name (cf. Test.mli) *)
 
 
+  module CodeInstr : sig
+    type t = { instr: instr; static_poi: int }
+  end
+
   (* Code memory is a mapping from labels to sequences of instructions, too far from actual machine, maybe *)
-  type code = (int * instr) list
+  type code = (int * CodeInstr.t) list
 
   (* Program loaded in memory *)
   type program = int Label.Map.t
@@ -105,6 +109,7 @@ module type S = sig
       fetch_proc : proc; (* Fetching source *)
       proc       : proc; (* Current thread *)
       program_order_index   : program_order_index;
+      static_poi : program_order_index;
       inst : instr;
       labels : Label.Set.t; lbl2addr:program;
       addr : int;
@@ -335,8 +340,12 @@ module Make(C:Config) (I:I) : S with module I = I
       (* Components of test structures *)
       (*********************************)
 
+      module CodeInstr = struct
+        type t = { instr: instr; static_poi: int }
+      end
+
       (* Code memory is a mapping from globals locs, to instructions *)
-      type code = (int * instr) list
+      type code = (int * CodeInstr.t) list
 
       (* Programm loaded in memory *)
       type program = int Label.Map.t
@@ -364,6 +373,7 @@ module Make(C:Config) (I:I) : S with module I = I
           fetch_proc : proc;
           proc       : proc;
           program_order_index   : program_order_index;
+          static_poi : program_order_index;
           inst : instr;
           labels : Label.Set.t; lbl2addr : program;
           addr : int ;

herd/event.ml

@@ -69,6 +69,7 @@ val same_instance : event -> event -> bool
   val same_proc     : event -> event -> bool
   val same_proc_not_init : event -> event -> bool
   val progorder_of  : event -> A.program_order_index option
+  val static_poi  : event -> A.program_order_index option
 
 (* Is e1 before e2 w.r.t. prog order ? Nothing assumed on e1 and e2 *)
   val po_strict : event -> event -> bool
@@ -643,6 +644,10 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
     | IdSome i -> Some i.A.program_order_index
     | IdInit|IdSpurious -> None
 
+    let static_poi e =
+      match e.iiid with
+      | IdSome i -> Some i.A.static_poi
+      | IdInit | IdSpurious -> None
 
 (************************)
 (* Predicates on events *)

herd/loader.ml

@@ -86,29 +86,30 @@ struct
     | Offset _ as x -> x in
     A.map_labels_base labelmap instr
 
-  let rec load_code proc addr mem = function
+  let rec load_code ~proc ~addr ~static_poi mem = function
     | [] -> []
-    | ins::code -> load_ins proc addr mem code ins
+    | ins::code -> load_ins ~proc ~addr ~static_poi mem code ins
 
-  and load_ins proc addr mem code = function
+  and load_ins ~proc ~addr ~static_poi mem code = function
     | A.Nop ->
-       load_code proc addr mem code
+       load_code ~proc ~addr ~static_poi mem code
     | A.Instruction ins ->
         let start =
-          load_code proc (addr+A.size_of_ins ins) mem code in
+          load_code ~proc ~addr:(addr+A.size_of_ins ins) ~static_poi:(static_poi+1) mem code in
         let new_ins =
           convert_lbl_to_offset proc addr mem ins in
-        (addr,new_ins)::start
+        let code_ins = A.CodeInstr.{ instr = new_ins; static_poi; } in
+        (addr,code_ins)::start
     | A.Label (_,A.Nop) ->
-        load_code proc addr mem code
+        load_code ~proc ~addr ~static_poi mem code
     | A.Label (_,_) -> assert false (* Expected to have been normalised already! *)
     | A.Symbolic _
     | A.Macro (_,_) -> assert false
     | A.Pagealign ->
       assert false
     | A.Skip n ->
       let new_addr = addr + n in
-      load_code proc new_addr mem code
+      load_code ~proc ~addr:new_addr ~static_poi mem code
 
   let make_padding old_addr new_addr =
     let offset = new_addr - old_addr in
@@ -170,7 +171,7 @@ struct
     | [] ->
       IntMap.add addr (proc,[]) rets
     | (addr, ins)::start_tl ->
-      let ins_sz = A.size_of_ins ins in
+      let ins_sz = A.size_of_ins ins.A.CodeInstr.instr in
       let new_rets = IntMap.add addr (proc,start) rets in
       mk_rets_from_starts proc (addr+ins_sz) new_rets start_tl
 
@@ -183,7 +184,7 @@ struct
       | ((proc,_,func),code)::pseudo_prog_tl ->
          let starts,rets = load_iter pseudo_prog_tl in
          let addr = func_start_addr proc func in
-         let start = load_code proc addr mem code in
+         let start = load_code ~proc ~addr ~static_poi:0 mem code in
          let fin_rets = mk_rets_from_starts proc addr rets start in
          (proc,func,start)::starts,fin_rets in
     let starts,code_segments = load_iter pseudo_prog in

herd/mem.ml

@@ -164,6 +164,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
     module VC = EM.VC
     module U = MemUtils.Make(S)
     module W = Warn.Make(C)
+    module I = A.CodeInstr
 
     let dbg = C.debug.Debug_herd.mem
     let morello = C.variant Variant.Morello
@@ -302,14 +303,14 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
               | Some fh_code -> code@fh_code
               | None -> code in
             List.fold_left
-              (fun locs (_,ins) ->
+              (fun locs (_, (i : I.t)) ->
                 A.fold_addrs
                   (fun x ->
                     let loc = A.maybev_to_location x in
                     match loc with
                     | A.Location_global _ -> A.LocSet.add loc
                     | _ -> fun locs -> locs)
-                  locs ins)
+                  locs i.I.instr)
               locs code)
           locs
           test.Test_herd.start_points in
@@ -353,7 +354,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
 
       (* Creates a mapping:
        * - from an integer of a herd7-internal representation for an address,
-       * - to a VA page_label+offset, where page_label is the label at the 
+       * - to a VA page_label+offset, where page_label is the label at the
        *   beginning of page the address is on
        *)
       let a2ra =
@@ -513,7 +514,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
                     match addr2va addr with
                     | Some va when (is_on_exported_page (addr2va addr)) -> begin
                         let loc = A.Location_global va in
-                        let v = A.V.instructionToV i in
+                        let v = A.V.instructionToV i.I.instr in
                         A.state_add env loc v
                       end
                     | Some _ | None -> env
@@ -533,7 +534,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
                 | Some lbl ->
                     let symb = Constant.mk_sym_virtual_label proc lbl in
                     let loc = A.Location_global (A.V.cstToV symb)
-                    and v = A.V.instructionToV i in
+                    and v = A.V.instructionToV i.I.instr in
                     A.state_add env loc v)
               init_state lbls2i in
         { test with init_state; } in
@@ -615,10 +616,13 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
                 | e -> raise e in
 
 (* Call instruction semantics proper *)
-        let wrap re_exec fetch_proc proc inst addr env m poi =
+        let wrap re_exec fetch_proc proc (code_instr : I.t) addr env m poi =
           profile "build semantics" @@ fun () ->
+        let static_poi = code_instr.I.static_poi in
+        let inst = code_instr.I.instr in
         let ii =
            { A.program_order_index = poi;
+             static_poi;
              proc = proc; fetch_proc; inst = inst;
              labels = labels_of_instr addr;
              lbl2addr = prog;
@@ -639,8 +643,9 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
         m ii in
 
       let  sem_instr =  SM.build_semantics test in
-      let rec add_next_instr re_exec fetch_proc proc env seen addr inst nexts =
-        wrap re_exec fetch_proc proc inst addr env sem_instr >>> fun branch ->
+      let rec add_next_instr re_exec fetch_proc proc env seen addr (code_instr : I.t) nexts =
+        wrap re_exec fetch_proc proc code_instr addr env sem_instr >>> fun branch ->
+          let inst = code_instr.I.instr in
           let { A.regs=env; lx_sz=szo; fh_code } = env in
           let env = A.kill_regs (A.killed inst) env
           and szo =
@@ -658,7 +663,7 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
                   bds env
             | _ -> env in
           next_instr
-            re_exec inst fetch_proc proc { A.regs=env; lx_sz=szo; fh_code}
+            re_exec code_instr fetch_proc proc { A.regs=env; lx_sz=szo; fh_code}
             seen addr nexts branch
 
       and add_code re_exec fetch_proc proc env seen nexts = match nexts with
@@ -712,15 +717,15 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
                else (* execute  again the same instruction *)
                  add_next_instr true fetch_proc proc env seen addr inst nexts
 
-      and next_instr re_exec inst fetch_proc proc env seen addr nexts b =
+      and next_instr re_exec (code_instr : I.t) fetch_proc proc env seen addr nexts b =
         match b with
       | S.B.Exit -> EM.unitcodeT true
       | S.B.Next _ ->
           add_code re_exec fetch_proc proc env seen nexts
       | S.B.Jump (tgt,_) ->
           add_tgt re_exec true proc env seen addr tgt
       | S.B.Fault (syscall,_) ->
-          add_fault re_exec inst fetch_proc proc env seen addr syscall nexts
+          add_fault re_exec code_instr fetch_proc proc env seen addr syscall nexts
       | S.B.FaultRet tgt ->
           add_tgt false true proc env seen addr tgt
       | S.B.CondJump (v,tgt) ->
@@ -2305,7 +2310,7 @@ let get_rf_value test read =
                    Warn.user_error
                      "Instruction %s:%s cannot be overwritten"
                      (Label.pp lbl)
-                     (A.dump_instruction i)
+                     (A.dump_instruction i.I.instr)
               with
               | Not_found ->
                  Warn.user_error

herd/prettyUtils.ml

@@ -23,7 +23,7 @@ module Make(S : SemExtra.S) = struct
     let by_po =
       E.EventSet.fold
         (fun e k ->
-          match E.progorder_of e with
+          match E.static_poi e with
             | None -> k
             | Some poi ->
                let es_poi = IntMap.safe_find []  poi k in