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 checks if `valid` is set,
  i.e., being 1, in AArch64, while always returns `true` for other platform.
- In `final.ml` Use the FaultSet in `/lib` to track and rendering the `Fault`, which
  replace the existing `StringSet` solutions. In particular, there are
  two `FaultSet` that track postive and negative cases, i.e.
  `Fault(...)` and `~Fault(...)`.
- Modify `AArch64Compile_gen.ml` for printing the label on load and store instruction,
  when a fault check is needed.

The test for postive fault is a variant of `LB.litmus`. That is
```
diyone7 -arch AArch64 -variant kvm PodRW PteVA Rfe PodRW PteVA Rfe
```
This will generate a test:
```
AArch64 A
"PodRWPPteVA RfePteVAP PodRWPPteVA RfePteVAP"
Generator=diyone7 (version 7.58+1)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
Com=Rf Rf
Orig=PodRWPPteVA RfePteVAP PodRWPPteVA RfePteVAP
{ int y=0; int x=4;
0:X0=x; 0:X2=PTE(y); 0:X3=(oa:PA(y), valid:0);
1:X1=y; 1:X5=PTE(x); 1:X6=(oa:PA(x), valid:0);
}
 P0          | P1          ;
 L01:        | L00:        ;
 LDR W1,[X0] | LDR W4,[X1] ;
 STR X3,[X2] | STR X6,[X5] ;
exists (Fault(P0:L01,x) /\ Fault(P1:L00,y))
```
that checks if both labelled-`LDR` triggers fault. This is in the same spirit of
`catalogue/aarch64/tests/LB.litmus` that both `LDR` observe
the the value written by `STR`.

Regarding the test for much more common negetive fault, i.e. no fault.
```
diyone7 -arch AArch64 -variant kvm -oneloc PteVA TLBI-sync.ISHsWR Fri
```
This will generate a test:
```
AArch64 A
"TLBI-sync.ISHsWRPteVAP FriPPteVA"
Generator=diyone7 (version 7.58+1)
Com=Fr
Orig=TLBI-sync.ISHsWRPteVAP FriPPteVA
{ int x=0;
0:X0=PTE(x); 0:X1=(oa:PA(x), valid:0); 0:X2=x;
}
 P0              ;
 STR X1,[X0]     ;
 LSR X4,X2,herd#12   ;
 DSB ISH         ;
 TLBI VAAE1IS,X4 ;
 DSB ISH         ;
 L00:            ;
 LDR W3,[X2]     ;
exists (~Fault(P0:L00,x))
```
which check if the labelled-`LDR` triggers no fault because does not
observe the previous `STR` on the PTE value of variable `x`.

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.

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>
Signed-off-by: Shale Xiong <shale.xiong@arm.com,xiongshale@gmail.com>

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

@@ -229,6 +229,12 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
     let cbz r1 lbl = I_CBZ (vloc,r1,BranchTarget.Lbl lbl)
     let do_cbnz v r1 lbl = I_CBNZ (v,r1,BranchTarget.Lbl lbl)
     let cbnz = do_cbnz vloc
+    let is_branch l = match l with
+      | Instruction ins -> begin match ins with
+        | I_CBZ _|I_CBNZ _|I_TBNZ _|I_TBZ _|I_BR _|I_BLR _|I_RET _ -> true
+        | _ -> false
+      end
+      | _ -> false
 
     let do_cmpi v r i = op3i v SUBS ZR r i
     let cmpi r i = do_cmpi vloc r i
@@ -1723,7 +1729,35 @@ 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_last_instructions e cs =
+      match e.C.check_fault with
+      | Some (label_name, _) ->
+        let rec do_rec = function
+          | [] -> assert false (* the `cs` should not be empty *)
+          | [instr] -> [Label(label_name, instr)]
+          | [instr;branch_instr] when is_branch branch_instr ->
+              [Label(label_name, instr);branch_instr]
+          | instr::rem -> instr::do_rec rem in
+        do_rec cs
+      | None -> cs
+
+    (* If there is a fault label in `e`, add the `index`-th label
+       to the first instruction in `cs` *)
+    let add_label_to_first_instructions e cs =
+      match e.C.check_fault with
+      | Some (label_name, _) ->
+        (* find the first non-label instruction *)
+        let rec do_rec cs = match cs with
+          | [] -> assert false (* the `cs` should not be empty *)
+          | instr::rem -> begin match instr with
+            (* skip label or instruction that is already labelled *)
+            | Label(_) -> instr::do_rec rem
+            |_ -> Label(label_name, instr)::rem
+        end 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
@@ -1733,7 +1767,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
         | R,Some (Instr, None) ->
             let r,init,cs,st = LDR.emit_fetch st p init lab in
             Some r,init,cs,st
-        (* Plain read from an instruction label is currently not supported, 
+        (* Plain read from an instruction label is currently not supported,
            but will be implemented in a future patch
         | R, None ->
             let r,init,cs,st = LDR.emit_load st p init lab in
@@ -1757,12 +1791,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 =
@@ -1778,7 +1812,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 +1960,11 @@ 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. *)
+          (* Add a label to instructions `cs`, when a fault check is required. *)
+        let cs = add_label_to_last_instructions e cs in
+        regs,inits,cs,st
     (* END of emit_access *)
 
     let same_sz sz1 sz2 = match sz1,sz2 with
@@ -1945,7 +1983,6 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       check_cu (not (A64.do_cu || same_sz szr szw)) ;
       ar,aw
 
-
     let emit_addr_simple  st p init er =
       let rA,init,st = U.next_init st p init (get_tagged_loc er) in
       rA,init,[],st
@@ -1956,6 +1993,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let rW,init,csi,st = U.emit_mov st p init (Code.value_to_int ew.C.v) in
       let arw = check_arw_lxsx er ew in
       let init,cs,st = XSingle.emit_pair arw p st init rR rW rA ew in
+      let cs = add_label_to_first_instructions er cs in
       rR,init,csi@caddr@cs,st
 
     let emit_exch1 = do_emit_exch1 emit_addr_simple
@@ -1968,6 +2006,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let arw = check_arw_lxsx er ew in
       let init,cs,st =
         XPair.emit_pair arw p st init (rR1,rR2) (rW1,rW2) rA ew in
+      let cs = add_label_to_first_instructions er cs in
       rR1,init,csi@caddr@cs,st
 
     let emit_exch22 = do_emit_exch22 emit_addr_simple
@@ -1980,6 +2019,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let module X = ExclusivePair(XLoadPair)(XStore) in
       let init,cs,st =
         X.emit_pair arw p st init (rR1,rR2) rW rA ew in
+      let cs = add_label_to_first_instructions er cs in
       rR1,init,csi@caddr@cs,st
 
     let emit_exch21 = do_emit_exch21 emit_addr_simple
@@ -1993,6 +2033,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let module X = ExclusivePair(XLoad)(XStorePair) in
       let init,cs,st =
         X.emit_pair arw p st init rR (rW1,rW2) rA ew in
+      let cs = add_label_to_first_instructions er cs in
       rR,init,csi@caddr@cs,st
 
     let emit_exch12 = do_emit_exch12 emit_addr_simple
@@ -2053,8 +2094,9 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Some (sz,o) ->
           let rA,cs,st = sumi_addr st rA o in
           cs@[ins_mixed sz a rW rR rA],st in
+      let cs = add_label_to_last_instructions er (pseudo cs) in
       let cs2 = emit_ldr_addon opt rR in
-      rR,init,csi@csi2@pseudo (cs@cs2),st
+      rR,init,(csi@csi2@cs@pseudo cs2),st
 
     let do_emit_ldop ins ins_mixed st p init er ew =
       let rA,init,st =
@@ -2079,8 +2121,9 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Some (sz,o) ->
           let rA,cs,st = sumi_addr st rA o in
           cs@[cas_mixed sz a rS rT rA],st in
+      let cs = add_label_to_last_instructions er (pseudo cs) in
       let cs2 = emit_ldr_addon opt rS in
-      rS,init,csS@csS2@csT@csT2@pseudo (cs@cs2),st
+      rS,init,csS@csS2@csT@csT2@cs@pseudo cs2,st
 
     let emit_cas  st p init er ew =
       let rA,init,st =
@@ -2103,7 +2146,8 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Some (sz,o) ->
           let rA,cs,st = sumi_addr st rA o in
           cs@[stop_mixed op sz a rW rA],st in
-      None,init,csi@pseudo cs,st
+      let cs = add_label_to_last_instructions er (pseudo cs) in
+      None,init,csi@cs,st
 
     let emit_stop  op st p init er ew =
       let rA,init,st =
@@ -2220,7 +2264,7 @@ 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_idx_var vloc vdep st p init loc r2 in
@@ -2434,8 +2478,10 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
               None,init,pseudo cs0@cs,st
           | W,Some (Neon _,Some _) -> assert false
           | _,Some (Plain _,None) -> assert false
-          end
-      | _,Code _ -> Warn.fatal "No dependency to code location"
+          end in
+          (* Add a label to instructions `cs`, when a fault check is required. *)
+          regs,inits,(add_label_to_last_instructions e cs),st
+        | _,Code _ -> Warn.fatal "No dependency to code location"
       (* END of emit_access_dep_addr *)
 
     let emit_addr_dep csel vdep st p init loc rd =
@@ -2497,7 +2543,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
         | _ -> Some (a,m) end in
       (* 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
+      let regs,inits,cs,st = match e.C.dir,e.C.loc with
       | None,_ -> Warn.fatal "TODO"
       | Some R,_ -> Warn.fatal "data dependency to load"
       | Some W,Data loc ->
@@ -2645,8 +2691,10 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
              None,init,cs2@cs,st
           | Some (Pair _,Some _) -> assert false
           end
-      | _,Code _ -> Warn.fatal "Not Yet (%s,dep_data)" (C.debug_evt e)
-      (* END of emit_access_dep_data *)
+      (* END of `Some W` *)
+      | _,Code _ -> Warn.fatal "Not Yet (%s,dep_data)" (C.debug_evt e) in
+    regs,inits,(add_label_to_last_instructions e cs),st
+    (* END of emit_access_dep_data *)
 
     let is_ctrlisync = function
       | D.CTRLISYNC -> true

gen/CCompile_gen.ml

@@ -826,7 +826,7 @@ module Make(O:Config) : Builder.S
                   F.run evts m
               | Cycle -> F.check f
               | Observe -> F.observe f in
-            (add_args env c,f []),
+            (add_args env c,f (F.FaultSet.empty,F.FaultSet.empty)),
             (U.compile_prefetch_ios (List.length obsc) ios,
              U.compile_coms splitted),
             env

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
 
 
 (***********************)
@@ -189,7 +190,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)