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,7 +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 emit_access st p init e = 
+    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 rec do_rec = function
+          | [] -> assert false (* the `cs` should not be empty *)
+          | [instr] -> [Label(label_name, instr)]
+          | instr::rem -> instr::do_rec rem in
+        do_rec cs
+      | None -> cs
+
+    let emit_access st p init e =
     (* collapse the value `v` in event `e` to integer *)
     let value = Code.value_to_int e.C.v in
     match e.C.dir,e.C.loc with
@@ -1759,12 +1771,12 @@ 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
+        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 =
@@ -1780,7 +1792,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 =
@@ -1929,7 +1941,10 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
            let init,cs,st = emit_store st p init loc value 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

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
 
 
 (***********************)
@@ -181,7 +182,7 @@ 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)