[gen] Fix problems related to physical address change, annotation PteOA.

Makefile

@@ -747,6 +747,29 @@ diy-test-aarch64:
 		$(REGRESSION_TEST_MODE)
 	@ echo "herd7 AArch64 diycross7 tests: OK"
 
+diy-test:: diy-test-vmsa
+diy-test-vmsa:
+	@ echo
+	$(HERD_DIYCROSS_REGRESSION_TEST) \
+		-j $(J) \
+		-herd-path $(HERD) \
+		-diycross-path $(DIYCROSS) \
+		-libdir-path ./herd/libdir \
+		-expected-dir ./gen/tests/AArch64.vmsa \
+		-variant vmsa \
+		-diycross-arg -arch \
+		-diycross-arg AArch64 \
+		-diycross-arg -variant \
+		-diycross-arg vmsa \
+		-diycross-arg -oneloc \
+		-diycross-arg 'PteOA,PteHA,PteHD,P' \
+		-diycross-arg TLBI-sync.ISHsWW \
+		-diycross-arg 'PteV1,PteAF0,P' \
+		-diycross-arg 'PteOA,P' \
+		-diycross-arg PosWR \
+		-diycross-arg Fri \
+		$(REGRESSION_TEST_MODE)
+
 diy-test:: diy-test-mixed
 diy-test-mixed::
 	@ echo

gen/common/AArch64Arch_gen.ml

@@ -380,6 +380,12 @@ module Value = struct
       | Pte f,None -> do_setpteval f p
       | _ -> Warn.user_error "Atom is not a pteval write"
 
+    let get_physical_address p =
+      match AArch64PteVal.as_physical p with
+      | Some loc -> loc
+      | None -> Warn.user_error "No physical address."
+
+
     let can_fault dir pte_val =
       let open AArch64PteVal in
       pte_val.valid = 0 || pte_val.af = 0 || (dir = Code.W && pte_val.db = 0)
@@ -406,6 +412,13 @@ module Value = struct
         when affect_pte_field DB pte -> Dir W
       | _ -> NoDir
 
+    let need_check_value_on_pte atom =
+      let open WPTE in
+      match atom with
+      | Some(Pte (Set(pte_atom_set)|SetRel(pte_atom_set)),None) ->
+          WPTESet.mem OA pte_atom_set
+      |_ -> false
+
     let implicitly_set_pteval dir machine_feature p =
       let open WPTE in
       let open AArch64PteVal in

gen/common/archExtra_gen.ml

@@ -186,25 +186,6 @@ and module Value := I.Value
 
   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
-    | Some _ as r -> r
-    | None -> None
-
-  let add_some x xs = match x with
-  | None -> xs
-  | Some x -> StringSet.add x xs
-
   let ppo = function
     | None -> "-"
     | Some v -> pp_initval v
@@ -214,53 +195,14 @@ and module Value := I.Value
        (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) ->
           if Misc.is_pte loc then (Location.Location_global loc,Some (P (Value.to_pte v)))::env
           (* Do not include if the value is default zero *)
           else if Value.to_int v = 0 then env
           else (Location.Location_global loc,Some (S (Value.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 *)
-          | Location.Location_global s -> add_some (as_virtual s) k
-          (* No process on register *)
-          | Location.Location_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)
-        StringSet.empty i in
-    let refer =
-      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 *)
-          | Location.Location_global s -> add_some (refers_virtual s) k
-          (* No process on register *)
-          | Location.Location_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 (Value.refers_virtual p) 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 -> (Location.Location_global x,None)::i)
-        (StringSet.diff refer already_here)
-        i in
-    i
+          ) i iv
 
   module RegMap =
     MyMap.Make

gen/common/value_gen.ml

@@ -23,6 +23,7 @@ module type PteType = sig
   val init_pte : string -> atom list -> pte
   val pte_compare : pte -> pte -> int
   val set_pteval : atom -> pte -> (unit -> string) -> pte
+  val get_physical_address : pte -> string
   (* Implicitly set pte value. Return indicates fault check and new pte vaule,
      This is for a case where a memory event `Code:dir` to `x` rather than `Pte(x)`,
      when certain machine features present `StringSet.t`, might update
@@ -34,6 +35,10 @@ module type PteType = sig
      Dir W and Dir R for write and read, respectively.
      and Irr for both, NoDir for none *)
   val need_check_fault : atom option -> Code.extr
+  (* check if the pte change by `pte_atom` triggers
+     a value check for further memory access,
+     for example input `PteOA` returns `true`. *)
+  val need_check_value_on_pte : atom option -> bool
 end
 
 module type S = sig
@@ -95,10 +100,12 @@ module NoPte(A:sig type arch_atom end) = struct
     let init_pte s _atom_list = default_pte s
     let pte_compare _ _ = 0
     let set_pteval _ p _ = p
+    let get_physical_address _ = "[nopte]"
     let implicitly_set_pteval _ _ _ = None
     let can_fault _dir _t = false
     let refers_virtual _ = None
     let need_check_fault _ = Code.NoDir
+    let need_check_value_on_pte _ = false
   end)
 
   let from_pte _ = Warn.user_error "Cannot convert from pte"