Add the fault check functionality related to pte value.

- add `check_fault` and `check_value` fields in `node` structure in `cycle.ml`,
,with default values being `None` for irrelevance. `check_fault` carries a boolean
and a string, that is, if the event should fault and a label for the instruction.
While `check_value` carries a boolean for if any memory effect check, i.e. read event,
should be check. This two new variables enable generating fault and value check when
there is previous change to pte or plain values respectively.
- Introduce `can_fault` function in `Pteval`, which currently check if `valid` is set,
i.e., being 1, in AArch64, while always returns `true` for other platform.
- Introduce FaultSet of element of an optional label string and a variable string.
This replace the StringSet used in the `final.ml` for printing the fault-related post-
condition such as `fault(P1:L02,y)`.
- Modify `AArch64Compile_gen.ml` for printing the label on load and store instruction,
when a fault check is needed.

Minor improvement:

- Merge the accumulators `cell` and `pte_cell` into CoSt `st` in cycle (`cycle.ml`) building,
functions `do_set_write_v` and `do_set_read_v`.
- Replace a few manual list foldings with a `List.fold_left`.
- Add some explanatory comments on some single-latter variables.

Author: ShaleXIONG

gen/AArch64Arch_gen.ml

@@ -588,6 +588,11 @@ let overwrite_value v ao w = match ao with
       match a with
       | Pte f,None -> do_setpteval a f p
       | _ -> Warn.user_error "Atom %s is not a pteval write" (pp_atom a)
+
+    let can_fault pte_val = 
+      let open AArch64PteVal in
+      pte_val.valid = 0
+
   end
 
 (* Wide accesses *)

gen/AArch64Compile_gen.ml

@@ -1725,6 +1725,19 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
 
     let get_tagged_loc e = add_tag (as_data e.C.loc) e.C.tag
 
+    let add_label_to_instructions e cs =
+      match e.C.check_fault with
+      | Some (label_name, _) -> 
+        (* Always label the last instruction,
+           which should be the actual load or store. *)
+        let length = List.length cs in
+        List.mapi 
+        ( fun index instr ->
+            if index = (length - 1) then
+                Label(label_name, instr)
+            else instr ) cs
+      | None -> cs 
+
     let emit_access  st p init e = match e.C.dir,e.C.loc with
     | None,_ -> Warn.fatal "AArchCompile.emit_access"
     | Some d,Code lab ->
@@ -1756,12 +1769,18 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
             assert (Misc.is_none m) ;
             Some (a,Some (MachSize.S128,0))
           | _ -> Some (a,m) end in
-        begin match d,atom with
+        (* Compile the node.
+           - `regs`, registers
+           - `inits`, initial values
+           - `cs`, instructions
+           - `st`, states
+        *)
+        let regs,inits,cs,st = begin match d,atom with
         | R,None ->
             let r,init,cs,st = LDR.emit_load st p init loc in
             Some r,init,cs,st
         | R,Some (Acq _,None) ->
-            let r,init,cs,st = LDAR.emit_load st p init loc  in
+            let r,init,cs,st = LDAR.emit_load st p init loc in
             Some r,init,cs,st
         | R,Some (Acq a,Some (sz,o)) ->
             let module L =
@@ -1777,7 +1796,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
             let cs2 = emit_ldr_addon a r in
             Some r,init,cs@pseudo cs2,st
         | R,Some (AcqPc _,None) ->
-            let r,init,cs,st = LDAPR.emit_load st p init loc  in
+            let r,init,cs,st = LDAPR.emit_load st p init loc in
             Some r,init,cs,st
         | R,Some (AcqPc a,Some (sz,o)) ->
             let module L =
@@ -1926,7 +1945,11 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
            let init,cs,st = emit_store st p init loc e.C.v in
            None,init,cs,st
         | W,Some (Neon _,Some _) -> assert false
-        end
+        end in
+        (* Add a label to instructions `cs`, when a fault check is required. *)
+        let cs = add_label_to_instructions e cs in
+        regs,inits,cs,st
+    (* END of emit_access *)
 
     let same_sz sz1 sz2 = match sz1,sz2 with
       | None,None -> true

gen/FaultSetElm.ml

@@ -0,0 +1,27 @@
+(****************************************************************************)
+(*                           The diy toolsuite                              *)
+(*                                                                          *)
+(* Jade Alglave, University College London, UK.                             *)
+(* Luc Maranget, INRIA Paris-Rocquencourt, France.                          *)
+(*                                                                          *)
+(* Copyright 2025-present Institut National de Recherche en Informatique et *)
+(* en Automatique, ARM Ltd and the authors. All rights reserved.            *)
+(*                                                                          *)
+(* This software is governed by the CeCILL-B license under French law and   *)
+(* abiding by the rules of distribution of free software. You can use,      *)
+(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
+(* license as circulated by CEA, CNRS and INRIA at the following URL        *)
+(* "http://www.cecill.info". We also give a copy in LICENSE.txt.            *)
+(****************************************************************************)
+
+type t = string option * bool option * string
+
+let compare (lhs_label, lhs_bool, lhs_var) (rhs_label, rhs_bool, rhs_var) = 
+    let label = 
+        Option.compare String.compare lhs_label rhs_label in
+    let boolean =
+        Option.compare Bool.compare lhs_bool rhs_bool in
+    match label, boolean with
+    | 0, 0 -> String.compare lhs_var rhs_var
+    | 0, boolean -> boolean
+    | label, _ -> label

gen/PPCCompile_gen.ml

@@ -450,7 +450,7 @@ module Make(O:Config)(C:sig val eieio : bool end) : XXXCompile_gen.S =
           let emit = match e.atom with
           | None -> emit_load
           | Some (PPC.Mixed (sz,o)) -> emit_load_mixed sz o
-          | Some PPC.Reserve ->emit_lwarx
+          | Some PPC.Reserve -> emit_lwarx
           | Some PPC.Atomic -> emit_lda in
           let r,init,cs,st = emit st p init loc in
           Some r,init,(if isync then insert_isync c cs else c@cs),st

gen/RISCVCompile_gen.ml

@@ -221,7 +221,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S  =
 
 (* For export *)
     let emit_load_one = LOAD.emit_load_one AV.Rlx
-    let emit_load = LOAD.emit_load  AV.Rlx
+    let emit_load = LOAD.emit_load AV.Rlx
     let emit_obs _ = OBS.emit_load AV.Rlx
     let emit_obs_not_value = OBS.emit_load_not_value AV.Rlx
     let emit_obs_not_eq = OBS.emit_load_not_eq AV.Rlx

gen/X86_64Compile_gen.ml

@@ -324,7 +324,7 @@ module Make(Cfg:CompileCommon.Config) : XXXCompile_gen.S =
             | R ->
                begin match e.C.atom with
                | None|Some (Plain,None) ->
-                  let r,init,cs,st = emit_load st _p init loc  in
+                  let r,init,cs,st = emit_load st _p init loc in
                   Some r,init, cs,st
                | Some (Atomic,_) ->
                   Warn.fatal "No atomic load for X86_64"

gen/archExtra_gen.ml

@@ -62,6 +62,7 @@ module type S = sig
 
 (* complete init with necessary information *)
   val complete_init : bool (* hexa *) -> Code.env -> init -> init
+  val pp_env: init -> string
 
 
 (***********************)
@@ -150,6 +151,8 @@ and type special3 = I.special3
   let of_loc loc = Loc (Code.as_data loc)
   let of_reg p r = Reg (p,r)
 
+  (* - S of a plain value, a pte_* address or a phy_* address 
+     - P of a PteVal *)
   type initval = S of string | P of AArch64PteVal.t
   let pp_initval = function
     | S v ->  pp_symbol v
@@ -162,11 +165,15 @@ and type special3 = I.special3
 
   type init = (location * initval option) list
 
+  (* convert to `Some`, if input `s`
+     is not a pteval nor a number *)
   let as_virtual s = match Misc.tr_pte s with
   | Some _ -> None
   | None ->
       if LexScan.is_num s then None else Some s
 
+  (* convert to `Some`, if input `s` 
+     is neither a pteval or a physical location *)
   let refers_virtual s = match Misc.tr_pte s with
   | Some _ as r -> r
   | None -> match Misc.tr_physical s with
@@ -181,21 +188,25 @@ and type special3 = I.special3
     | None -> "-"
     | Some v -> pp_initval v
 
-  let _pp_env env =
+  let pp_env env =
     String.concat ", "
        (List.map (fun (loc,v) -> pp_location loc ^ "->" ^ ppo v) env)
 
   let complete_init hexa iv i =
     let i =
+      (* Add the locs `loc` and values `v` inside `iv` to `i` *)
       List.fold_left
         (fun env (loc,v) -> (Loc loc,Some (S (Code.pp_v ~hexa:hexa v)))::env) i iv in
     let already_here =
       List.fold_left
         (fun k (loc,v) ->
           let k = match loc with
+          (* Add Loc `s` into `k` if `s` is not a pte address nor a number *)
           | Loc s -> add_some (as_virtual s) k
+          (* No process on register *)
           | Reg _  -> k in
           let k = match v with
+          (* Add value `s` into `k` if `s` is not a pte nor a number *)
           | Some (S s) -> add_some (as_virtual s) k
           | _ -> k in
           k)
@@ -204,16 +215,22 @@ and type special3 = I.special3
       List.fold_left
         (fun k (loc,v) ->
           let k = match loc with
+          (* Add Loc `s` into `k` if `s` is a pte or physical address *)
           | Loc s -> add_some (refers_virtual s) k
+          (* No process on register *)
           | Reg _ -> k in
           let k = match v with
+          (* Add value `s` into `k` if `s` is a pte or physical address *)
           | Some (S s) -> add_some (refers_virtual s) k
+          (* Add the associated physical address in a pteval `p` into `k` *)
           | Some (P p) ->
              add_some
                (OutputAddress.refers_virtual p.AArch64PteVal.oa) k
           | None -> k in
           k)
         StringSet.empty i in
+    (* If a `refer` exist but there is no entry, 
+       then add it into init state `i` *)
     let i =
       StringSet.fold
         (fun x i -> (Loc x,None)::i)