Merge pull request #1744 from HadrienRenaud/fix-ambiguous-po-regs

[herd,asl] Fix ambiguous PC writes

This PR cherry picks a commit from #1735 that introduces some checks on the coherence of writes, and fixes the problems highlighted from those checks.

## PC handling in ASL+herd

The aarch64 handwritten semantics in herd handle the program counter differently from the ASL code: the ASL code has an explicit PC register, whereas the handwritten semantics rely on po and BCC branching events.

We had introduced in #711 an AArch64 PC register in ASL to support the ASL code that uses it.
This implementation wrote 2 times to the PC:
1. First at the beginning of the instruction to correctly initialize the PC value
2. Secondly when the branching is committed and we actually increments the PC

This poses a few problems, mainly because the current herd algorithm does not handle multiple writes at the same register in a single instruction.

We thus remove the translation of the PC accesses, replaced here by a BCC commit event in case of a write. This leaves implicit the PC reads.

## Intra-Instruction Dependencies starting from a register write

The PC handling described above had a strange graph, where a `iico_data` was starting at a register write. This is because this register write was read-from in the same instruction.

(Precisely, the first write to PC was read from to query the current PC and then increment it, resulting in a graph like [the one](https://github.com/user-attachments/files/25799596/A.pdf) shown by Luc in [a comment](#1735 (comment)) on #1704).

We simply add guards on the Intra-Instruction Data dependencies to force them to start at a register read or at a memory read.

Author: HadrienRenaud

herd/AArch64ASLSem.ml

@@ -215,9 +215,6 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
       let open Asllib.AST in
       let with_pos desc = Asllib.ASTUtils.add_dummy_annotation ~version:V0 desc in
       let ( ^= ) x e = S_Decl (LDK_Let, LDI_Var x, None, Some e) |> with_pos in
-      let ( ^^= ) x e =
-        let le_x = LE_Var x |> with_pos in
-        S_Assign (le_x, e) |> with_pos in
       let lit v = E_Literal v |> with_pos in
       let liti i = lit (L_Int (Z.of_int i)) in
       let litb b = lit (L_Bool b) in
@@ -249,7 +246,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
                stmt
                  [
                    "offset" ^= litbv 64 off;
-                   "_PC" ^^= litbv 64 ii.A.addr; ])
+                   ])
       | I_CBZ (v,rt,lab)
       | I_CBNZ (v,rt,lab) as i
         ->
@@ -266,7 +263,6 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
                 "t" ^= reg rt;
                 "datasize" ^= variant v;
                 "offset" ^= litbv 64 off;
-                "_PC" ^^= litbv 64 ii.A.addr;
               ])
       | I_BC (c,lab)
         ->
@@ -277,7 +273,6 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
               [
                 "offset" ^= litbv 64 off;
                 "condition" ^= cond c;
-                "_PC" ^^= litbv 64 ii.A.addr;
               ])
       | I_TBZ (v, rt, k, lab)
       | I_TBNZ (v, rt, k, lab) ->
@@ -296,7 +291,6 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
                 "offset" ^= litbv 64 offset;
                 "bit_pos" ^= liti k;
                 "datasize" ^= variant v;
-                "_PC" ^^= litbv 64 ii.A.addr;
               ])
 
       (* Atomic instructions *)
@@ -1126,9 +1120,13 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
         not is_vmsa ||
         List.exists (Proc.equal ii.A.proc) TopConf.procs_user in
       let pstate_val, eqs = build_pstate_val is_el0 ii in
+      let pc_val =
+        ASLS.A.V.scalarToV (ASLScalar.bv_of_int_sized 64 ii.A.addr)
+      in
       let st =
         ASLS.A.state_empty
         |> state_add (global_loc "PSTATE") pstate_val
+        |> state_add (global_loc "_PC") pc_val
         |> List.fold_right add_arch_reg_if_present ASLBase.gregs
         |> add_reg_if_present AArch64Base.ResAddr (global_loc "RESADDR")
         |> add_reg_if_present AArch64Base.SP (global_loc "_SP_EL0")
@@ -1341,6 +1339,15 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
             Printf.eprintf "tr_action %s\n%!"
               (ASLS.Act.pp_action act) in
         match act with
+        | ASLS.Act.Access
+            ( d,
+              ASLS.A.Location_reg (_proc, ASLBase.ArchReg AArch64Base.PC),
+              v,
+              _,
+              _ ) -> (
+            match d with
+            | Dir.W -> Some (Act.Commit (Act.Bcc, Some (V.pp true (tr_v v))))
+            | Dir.R -> None)
         | ASLS.Act.Access (dir, loc, v, sz, (a, exp, acc)) -> (
             match tr_loc ii loc with
             | None -> None
@@ -1542,35 +1549,22 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           let bds = List.fold_left one_event [] event_list in
           let finals = get_cat_show  Misc.identity "AArch64_Finals" in
           let pc =
-            let n_pc = (* Count writes to PC *)
-              List.fold_left
-                (fun c (r,_) ->
-                  match r with
-                  | AArch64Base.PC -> c+1
-                  | _ -> c)
-                0 bds in
-            (* Branching instructions all generate one, initial,
-             * PC assignement and a second PC assignement
-             * that gives the branch target. This applies even
-             * for  non-taken conditional branches where
-             * the second assignment is to the next instruction.
-             * This second write event is the final write to PC.
-             * Non-branching instructions neither read nor
-             * write the PC, cf. case [None] below.
-             *)
-            if n_pc <= 1 then None
-            else
-              ESet.fold
-                (fun e r ->
-                  match e.ASLE.action with
-                  | ASLS.Act.Access
-                    (Dir.W,
-                     ASLS.A.Location_reg
-                       (_,
-                        ASLBase.ArchReg AArch64Base.PC), v, _, _) ->
-                     Some (tr_v v)
-                  | _ -> r)
-                finals None in
+            ESet.fold
+              (fun e r ->
+                match e.ASLE.action with
+                | ASLS.Act.Access
+                    ( Dir.W,
+                      ASLS.A.Location_reg (_, ASLBase.ArchReg AArch64Base.PC),
+                      v,
+                      _,
+                      _ ) ->
+                    if Option.is_some r then
+                      Warn.fatal
+                        "There are 2 direct writes to PC in this instruction.";
+                    Some (tr_v v)
+                | _ -> r)
+              finals None
+          in
           match Misc.seq_opt A.V.as_int pc with
           | Some v -> B.Jump (B.Addr v,bds)
           | None ->

herd/libdir/asl.cat

@@ -50,7 +50,7 @@ let asl_ctrl_deps = [B]; (asl_data | asl_iico_ctrl)+; [AArch64]
 (**********************************)
 
 (* Intra-instruction Data dependencies *)
-let aarch64_iico_data = [AArch64 \ B]; asl_deps; [AArch64]
+let aarch64_iico_data = [AArch64 & (R | Rreg)]; asl_deps; [AArch64]
 
 (* Intra-instruction Control dependencies *)
 let aarch64_iico_ctrl = [B]; asl_ctrl_deps; [AArch64]

herd/mem.ml

@@ -864,27 +864,71 @@ and get_written e = match E.written_of e with
 (* Compute rfmap for registers *)
 (*******************************)
 
+module EvtSetByPo (I : sig
+  val es : S.event_structure
+end) =
+struct
+  let is_before_strict = U.is_before_strict I.es
+
+  let ambiguous_po e1 e2 =
+    Warn.fatal "Ambiguous po for register %s: %s and %s are not ordered.\n%!"
+      (A.pp_location (get_loc e1))
+      (E.debug_event_str e1) (E.debug_event_str e2)
+
+  include Set.Make (struct
+    type t = E.event
+
+    let compare e1 e2 =
+      if is_before_strict e1 e2 then -1
+      else if is_before_strict e2 e1 then 1
+      else ambiguous_po e1 e2
+  end)
+
+  let find_last_before e set =
+    find_last_opt (fun e' -> is_before_strict e' e) set
+
+  let find_first_after e set =
+    find_first_opt (fun e' -> is_before_strict e e') set
+  [@@warning "-32"]
+
+  (* We have to check that the order is total because none of the set
+     construction methods perform enough comparison to ensure that all
+     consecutive elements will be compared.
+
+     Checking that all consecutive elements are comparable is enough to prove
+     totality if the relation is transitive. Here, we believe that
+     [is_before_strict] is transitive by construction.
+
+     See this gist:
+       https://gist.github.com/HadrienRenaud/245295e0950fb3b58c23e43937248c9c
+  *)
+
+  let check_total set =
+    if not (is_empty set) then
+      fold
+        (fun e pred_opt ->
+          match pred_opt with
+          | Some pred ->
+              if not (is_before_strict pred e) then ambiguous_po e pred;
+              Some e
+          | None -> Some e)
+        set None
+      |> ignore
+
+  let of_list li =
+    let set = of_list li in
+    let () = check_total set in
+    set
+end
+
 let map_loc_find loc m =
   try U.LocEnv.find loc m
   with Not_found -> []
 
 let match_reg_events add_eq es csn =
   let loc_loads_stores = U.collect_reg_loads_stores es in
-  let is_before_strict = U.is_before_strict es in
-  let compare e1 e2 =
-    if is_before_strict e1 e2 then -1
-    else if is_before_strict e2 e1 then 1
-    else
-      let () =
-        Printf.eprintf "Not ordered stores %a and %a\n" E.debug_event e1
-          E.debug_event e2
-      in
-      assert false
-  in
-  let module StoreSet = Set.Make (struct
-    type t = E.event
-
-    let compare = compare
+  let module StoreSet = EvtSetByPo (struct
+    let es = es
   end) in
   let add wt rf (rfm, csn) = (S.RFMap.add wt rf rfm, add_eq rfm wt rf csn) in
   (* For all loads find the right store, the one "just before" the load *)
@@ -901,9 +945,8 @@ let match_reg_events add_eq es csn =
       (* Add the corresponding store for each load *)
       List.fold_left
         (fun k load ->
-          let f e = is_before_strict e load in
           let rf =
-            match StoreSet.find_last_opt f stores with
+            match StoreSet.find_last_before load stores with
             | Some store -> S.Store store
             | None -> S.Init
           in

lib/ASLScalar.ml

@@ -393,6 +393,7 @@ let zeros_size_one = S_BitVector (BV.zeros 1)
 let bv_of_bool b =  S_BitVector (if b then BV.one else BV.zero)
 
 let bv_of_int x = S_BitVector (BV.of_int x)
+let bv_of_int_sized n x = S_BitVector (BV.of_int_sized n x)
 
 let do_bv_of_bit = function
   | 0 -> BV.zero