[herd,asl] PTE accesses in ASL+VMSA mode.

Notice that page table are accessed in PTE2 mode. That is,
PTE accesses undergo the vrtual to physical translation,
as the mode that is naturally compatible with existing
ASL code.

herd/AArch64ASLSem.ml

@@ -737,8 +737,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           None
 
     let tr_cst tr =
-      Constant.map tr
-        (fun _ -> Warn.fatal "Cannot translate PTE")
+      Constant.map tr Misc.identity
         (fun _ -> Warn.fatal "Cannot translate instruction")
 
     let aarch64_to_asl_bv = function

herd/AArch64Sem.ml

@@ -38,7 +38,7 @@ module Make
     let neon = C.variant Variant.Neon || sve
     let kvm = C.variant Variant.VMSA
     let is_branching = kvm && not (C.variant Variant.NoPteBranch)
-    let pte2 = kvm && C.variant Variant.PTE2
+    let pte2 = kvm && (C.variant Variant.PTE2 || C.variant Variant.ASL)
     let do_cu = C.variant Variant.ConstrainedUnpredictable
     let self = C.variant Variant.Ifetch
 

herd/ASLSem.ml

@@ -250,6 +250,18 @@ module Make (C : Config) = struct
       in
       an
 
+    let access_to_access acc =
+      let open Access in
+      match v_as_int acc with
+      | 0 -> REG
+      | 1 -> VIR
+      | 2 -> PHY
+      | 3 -> PTE
+      | 4 -> TLB
+      | 5 -> TAG
+      | 6 -> PHY_PTE
+      | i -> Warn.fatal "Bad access code from ASL: %d" i
+
     let wrap_op1_symb_as_var op1 = function
       | V.Val (Constant.Symbolic _) as v ->
           let v' = V.fresh_var () in
@@ -555,7 +567,7 @@ module Make (C : Config) = struct
         (use_ii_with_poi ii poi)
 
     let write_pc (ii,poi) v_m =
-      let* v = v_m >>= to_int_unsigned in
+      let* v = v_m >>= to_aarch64_val in
       write_loc MachSize.Quad (loc_pc ii)
         v aneutral aexp areg (use_ii_with_poi ii poi) >>! []
 
@@ -572,11 +584,10 @@ module Make (C : Config) = struct
       do_read_memory ii (M.unitT addr)  (M.unitT (V.intToV 64))
         aneutral (AArch64Explicit.(NExp Other)) apte
 
-    let vir_or_phy = if is_kvm then Access.PHY else Access.VIR
-
-    let read_memory_gen ii addr_m datasize_m accdesc_m =
-      let* accdesc = accdesc_m in
-      do_read_memory ii addr_m datasize_m (accdesc_to_annot true accdesc) aexp vir_or_phy
+    let read_memory_gen ii addr_m datasize_m accdesc_m access_m =
+      let* accdesc = accdesc_m and* access = access_m in
+      do_read_memory ii addr_m datasize_m (accdesc_to_annot true accdesc)
+        aexp (access_to_access access)
 
     let do_write_memory (ii, poi) addr_m datasize_m value_m an aexp acc =
       let value_m = M.as_data_port value_m in
@@ -589,10 +600,10 @@ module Make (C : Config) = struct
     let write_memory ii addr_m datasize_m value_m =
       do_write_memory ii addr_m datasize_m value_m aneutral aexp avir
 
-    let write_memory_gen ii addr_m datasize_m value_m accdesc_m =
-      let* accdesc = accdesc_m in
+    let write_memory_gen ii addr_m datasize_m value_m accdesc_m access_m =
+      let* accdesc = accdesc_m and* access = access_m in
       do_write_memory ii addr_m datasize_m value_m
-        (accdesc_to_annot false accdesc)  aexp vir_or_phy
+        (accdesc_to_annot false accdesc)  aexp (access_to_access access)
 
     let loc_sp ii = A.Location_reg (ii.A.proc, ASLBase.ArchReg AArch64Base.SP)
 
@@ -601,14 +612,18 @@ module Make (C : Config) = struct
         (use_ii_with_poi ii poi)
 
     let write_sp (ii, poi) v_m =
-      let* v = v_m >>= to_int_signed in
+      let* v = v_m >>= to_aarch64_val in
       write_loc MachSize.Quad (loc_sp ii) v aneutral aexp areg
         (use_ii_with_poi ii poi)
       >>! []
 
     let uint _ bv_m = bv_m >>= to_int_unsigned
     let sint _ bv_m = bv_m >>= to_int_signed
     let processor_id (ii, _poi) () = return (V.intToV ii.A.proc)
+    let is_virtual _ addr_m =
+      addr_m
+      >>= M.op1 Op.IsVirtual
+      >>=  M.op1 (Op.ArchOp1 ASLOp.ToBool)
 
     let can_predict_from _ v_m w_m =
       let diff_case = v_m in
@@ -718,22 +733,22 @@ module Make (C : Config) = struct
       in
       build_primitive ~args:[ arg1; arg2; arg3 ] ?parameters name f
 
-    (** Build a primitive with arity 3 and a return value. *)
-    let p3r name arg1 arg2 arg3 ~returns ?parameters f =
+    (** Build a primitive with arity 4 and a return value. *)
+    let p4r name arg1 arg2 arg3 arg4 ~returns ?parameters f =
       let f ii_env = function
-        | [ v1; v2; v3 ] -> return [ f ii_env v1 v2 v3 ]
+        | [ v1; v2; v3; v4; ] -> return [ f ii_env v1 v2 v3 v4 ]
         | _ -> Warn.fatal "Arity error for function %s." name
       in
-      build_primitive ?returns:(Some returns) ~args:[ arg1; arg2; arg3 ]
+      build_primitive ?returns:(Some returns) ~args:[ arg1; arg2; arg3; arg4 ]
         ?parameters name f
 
-    (** Build a primitive with arity 4 and no return value. *)
-    let p4 name arg1 arg2 arg3 arg4 ?parameters f =
+    (** Build a primitive with arity 5 and no return value. *)
+    let p5 name arg1 arg2 arg3 arg4 arg5 ?parameters f =
       let f ii_env = function
-        | [ v1; v2; v3; v4 ] -> f ii_env v1 v2 v3 v4
+        | [ v1; v2; v3; v4; v5; ] -> f ii_env v1 v2 v3 v4 v5
         | _ -> Warn.fatal "Arity error for function %s." name
       in
-      build_primitive ~args:[ arg1; arg2; arg3; arg4 ] ?parameters name f
+      build_primitive ~args:[ arg1; arg2; arg3; arg4; arg5; ] ?parameters name f
 
     (* Primitives *)
     let extra_funcs =
@@ -777,15 +792,16 @@ module Make (C : Config) = struct
         (* Memory *)
         p2r "read_memory" ("addr", bv_64) ("size", integer) ~returns:bv_64
           read_memory;
-        p3r "read_memory_gen" ("addr", bv_64) ("size", integer)
-          ("accdesc", t_named "AccessDescriptor")
+        p4r "read_memory_gen" ("addr", bv_64) ("size", integer)
+          ("accdesc", t_named "AccessDescriptor") ("access", t_named "EventAccess")
           ~returns:bv_64 read_memory_gen;
         p3 "write_memory" ("addr", bv_64) ("size", integer)
           ("data", bv_var "size")
           write_memory;
-        p4 "write_memory_gen" ("addr", bv_64) ("size", integer)
+        p5 "write_memory_gen" ("addr", bv_64) ("size", integer)
           ("data", bv_var "size")
           ("accdesc", t_named "AccessDescriptor")
+          ("access", t_named "EventAccess")
           write_memory_gen;
 (* VMSA *)
         p1r "ComputePtePrimitive"
@@ -808,8 +824,10 @@ module Make (C : Config) = struct
           ~parameters:[ ("N", None) ]
           ("x", bv_var "N")
           ~returns:sint_returns sint;
-        (* Misc *)
+(* Misc *)
         p0r "ProcessorID" ~returns:integer processor_id;
+        p1r "IsVirtual"
+          ("addr",bv_64)  ~returns:boolean is_virtual;
         p2r "CanPredictFrom"
           ~parameters:[ ("N", None) ]
           ("predicted", bv_var "N")

herd/Pretty.ml

@@ -1594,7 +1594,6 @@ module Make (S:SemExtra.S) : S with module S = S  = struct
   module SHOW = Show.Make(PC)
 
   let show_es_rfm test es rfm =
-    prerr_endline "Bingo" ;
     SHOW.show (fun chan -> dump_es_rfm chan test es rfm)
 
   let show_legend test legend conc ?(sets = StringMap.empty) vbs  =

herd/eventsMonad.ml

@@ -1266,6 +1266,9 @@ Monad type:
       let memtag = C.variant Variant.MemTag
       let morello = C.variant Variant.Morello
       let kvm = C.variant Variant.VMSA
+      let is_asl = C.variant Variant.ASL
+      (* Combining the ASL and VMSA variant implies PTE2 mode *)
+      let is_pte2 = kvm && (is_asl || C.variant Variant.PTE2)
 
       module AM = A.Mixed(SZ)
 
@@ -1520,7 +1523,7 @@ Monad type:
                 else (pte_loc s,default_pteval s)::env)
               virt env in
           let env =
-            if C.variant Variant.PTE2 then
+            if is_pte2 then
               List.fold_right
                 (fun (loc,_ as bd) env -> match loc with
                 | A.Location_global (V.Val (Symbolic (System (PTE,s))))

herd/libdir/asl-pseudocode/implementations.asl

@@ -607,4 +607,17 @@ end
 func EndOfInstruction()
 begin
   return;
-end
+end
+
+// Type of underlying accesses (same order as lib/access.mli),
+// as recorder un events.
+
+type EventAccess of enumeration {
+     REG,
+     VIR,
+     PHY,
+     PTE,
+     TLB,
+     TAG,
+     PHY_PTE,
+};

herd/libdir/asl-pseudocode/physmem-std.asl

@@ -9,7 +9,7 @@ func PhysMemWrite(
   value::bits(8*size)
 ) => PhysMemRetStatus
 begin
-  write_memory_gen (desc.vaddress, size*8, value,accdesc);
+  write_memory_gen (desc.vaddress, size*8, value,accdesc,VIR);
   return PhysMemRetStatus {
     statuscode = Fault_None,
     extflag = '0',
@@ -27,7 +27,7 @@ func PhysMemRead(
 ) => (PhysMemRetStatus, bits(8*size))
 begin
   let value =
-    read_memory_gen (desc.vaddress,size*8,accdesc)[8*size-1:0];
+    read_memory_gen (desc.vaddress,size*8,accdesc,VIR)[8*size-1:0];
   let ret_status = PhysMemRetStatus {
     statuscode = Fault_None,
     extflag = '0',

herd/libdir/asl-pseudocode/physmem-vmsa.asl

@@ -9,7 +9,18 @@ func PhysMemWrite(
   value::bits(8*size)
 ) => PhysMemRetStatus
 begin
-  write_memory_gen (desc.paddress.address, size*8, value,accdesc);
+// Event level access, there differ for standard (virtual) addresses
+// and PTE's.
+//   We cannot use conditional expresssion,
+// because  write_memory_gen  needs a concrete argument.
+  var eventaccess : EventAccess;
+  if IsVirtual(desc.vaddress) then
+    eventaccess = PHY;
+  else
+    eventaccess = PHY_PTE;
+  end
+// No, we can write, physically.
+  write_memory_gen (desc.paddress.address, size*8, value,accdesc,eventaccess);
   return PhysMemRetStatus {
     statuscode = Fault_None,
     extflag = '0',
@@ -26,8 +37,15 @@ func PhysMemRead(
   accdesc::AccessDescriptor
 ) => (PhysMemRetStatus, bits(8*size))
 begin
+  var eventaccess : EventAccess;
+  if IsVirtual(desc.vaddress) then
+    eventaccess = PHY;
+  else
+    eventaccess = PHY_PTE;
+  end
   let value =
-    read_memory_gen (desc.paddress.address,size*8,accdesc)[8*size-1:0];
+    read_memory_gen
+      (desc.paddress.address,size*8,accdesc,eventaccess)[8*size-1:0];
   let ret_status = PhysMemRetStatus {
     statuscode = Fault_None,
     extflag = '0',

herd/mem.ml

@@ -859,10 +859,12 @@ let match_reg_events es =
 
     let solve_regs test es csn =
       match do_solve_regs test es csn with
-      | Some (es,rfm,_) as r ->
+      | Some (es,rfm,cns) as r ->
           if C.debug.Debug_herd.solver && C.verbose > 0 then begin
             let module PP = Pretty.Make(S) in
             prerr_endline "Reg solved, direct" ;
+            Printf.eprintf "++++ Remaing equations:\n%s\n++++++\n%!"
+              (VC.pp_cnstrnts cns) ;
             PP.show_es_rfm test es rfm
           end ;
           r

lib/ASLOp.ml

@@ -87,6 +87,7 @@ let pp_op1 _hexa = function
   | ToAArch64 -> "ToAArch64"
   | FromAArch64 -> "FromAArch64"
 
+
 let ( let* ) = Option.bind
 let return c = Some c
 let return_concrete s = Constant.Concrete s |> return
@@ -249,6 +250,7 @@ let do_op1 op cst =
               (* Valid *)
                 let valid = pte.AArch64PteVal.valid in
                 Some (Constant.Concrete (ASLScalar.bv_of_bit valid))
+            | _ when  is_address_mask positions -> Some cst
             | _ -> None
           end
       | Constant.Symbolic x ->

lib/ASLScalar.ml

@@ -289,16 +289,13 @@ let convert_to_int_unsigned = function
   | S_Bool true -> S_Int Z.one
   | S_BitVector bv -> S_Int (BV.to_z_unsigned bv)
 
-let as_bool = function
-  | S_Int i -> Some (not (Z.equal i Z.zero))
-  | S_Bool b -> Some b
-  | S_BitVector _ -> None
+let to_caml_bool = function
+  | S_Bool b -> b
+  | S_Int _|S_BitVector _   as sc -> not (is_zero sc)
+
+let as_bool sc = Some (to_caml_bool sc)
+let convert_to_bool sc = S_Bool (to_caml_bool sc)
 
-let convert_to_bool c =
-  match as_bool c with
-  | Some b -> S_Bool b
-  | None ->
-      Warn.fatal "ASLScalar invalid op: to_bool %s" (pp false c)
 
 let convert_to_bv = function
   | S_BitVector _ as bv -> bv

lib/genParser.ml

@@ -225,7 +225,6 @@ module Make
                       | _ -> assert false
                       end
                 in
-                if O.verbose > 0 then prerr_endline "Bingo" ;
                 ConstrGen.map_constr map_atom cond
               with Not_found -> cond in
             { parsed with