Put ttbr values in TLB

Author: febyeji

ArchSemArm/VMPromising.v

@@ -809,17 +809,38 @@ Module TLB.
   #[export] Typeclasses Transparent Ctxt.t.
 
   Module Entry.
-    Definition t (lvl : Level) := vec val (S lvl).
-    Definition pte {lvl} (tlbe : t lvl) := Vector.last tlbe.
+    Record t (lvl : Level) :=
+      make {
+        val_ttbr : val;
+        ptes : vec val (S lvl);
+      }.
+    Arguments make {_} _ _.
+    Arguments val_ttbr {_}.
+    Arguments ptes {_}.
+
+    #[global] Instance eq_dec lvl : EqDecision (t lvl).
+    Proof. solve_decision. Defined.
+
+    #[global] Instance eqdep_dec : EqDepDecision t.
+    Proof. intros ? ? ? [] []. decide_jmeq. Defined.
+
+    #[global] Instance count lvl : Countable (t lvl).
+    Proof.
+      eapply (inj_countable' (fun ent => (val_ttbr ent, ptes ent))
+                        (fun x => make x.1 x.2)).
+      abstract sauto.
+    Defined.
+
+    Definition pte {lvl} (tlbe : t lvl) := Vector.last tlbe.(ptes).
 
     Program Definition append {lvl clvl : Level}
         (tlbe : t lvl)
         (pte : val)
         (CHILD : lvl + 1 = clvl) : t clvl :=
-      ctrans _ (tlbe +++ [#pte]).
+      make tlbe.(val_ttbr) (ctrans _ (tlbe.(ptes) +++ [#pte])).
     Solve All Obligations with lia.
   End Entry.
-  #[export] Typeclasses Transparent Entry.t.
+  Export (hints) Entry.
 
   (* Full Entry *)
   Module FE.
@@ -949,7 +970,8 @@ Module TLB.
           let asid := bv_extract 48 16 val_ttbr in
           let ndctxt := NDCtxt.make va (Some asid) in
           let ctxt := existT root_lvl ndctxt in
-          let entry : Entry.t (Ctxt.lvl ctxt) := [#memval] in
+          let entry : Entry.t (Ctxt.lvl ctxt) :=
+            Entry.make val_ttbr ([#memval] : vec val (S root_lvl)) in
           (* add the entry to vatlb only when it is not in the original vatlb *)
           if decide (entry ∉ (VATLB.get ctxt vatlb)) then
             Ok (VATLB.add ctxt entry vatlb, true)
@@ -973,8 +995,8 @@ Module TLB.
       (te : Entry.t (Ctxt.lvl ctxt))
       (index : bv 9)
       (ttbr : reg) : result string (VATLB.t * bool) :=
-    guard_or "ASID is not active"
-      $ is_active_asid ts (Ctxt.asid ctxt) ttbr time;;
+    (* guard_or "ASID is not active"
+      $ is_active_asid ts (Ctxt.asid ctxt) ttbr time;; *)
     guard_or "The translation entry is not in the TLB"
       (te ∈ VATLB.get ctxt vatlb);;
 
@@ -1201,7 +1223,7 @@ Module TLB.
                else filter (λ te, is_block (TLB.Entry.pte te)) tes in
     for te in (elements tes) do
       ti ← invalidation_time mem tid trans_time ctxt te;
-      mret ((vec_to_list te), ti)
+      mret ((vec_to_list (Entry.ptes te)), ti)
     end.
 
   (** Get all the TLB entries that could translate the given VA
@@ -1263,7 +1285,7 @@ Module TLB.
             if decide (is_valid memval) then mret None
             else
               ti ← invalidation_time mem tid trans_time ctxt te;
-              mret $ Some ((vec_to_list te) ++ [memval], ti)
+              mret $ Some ((vec_to_list (Entry.ptes te)) ++ [memval], ti)
           else
             mthrow "The PTE is missing"
         end;
@@ -1298,9 +1320,11 @@ Module TLB.
                 (va : bv 64) (asid : bv 16)
                 (ttbr : reg) : result string (list (list val * (option nat))) :=
     candidates_asid ←
-      get_invalid_ptes_with_inv_time_by_lvl_asid ts init mem tid tlb trans_time lvl va (Some asid) ttbr;
+      get_invalid_ptes_with_inv_time_by_lvl_asid
+        ts init mem tid tlb trans_time lvl va (Some asid) ttbr;
     candidates_global ←
-      get_invalid_ptes_with_inv_time_by_lvl_asid ts init mem tid tlb trans_time lvl va None ttbr;
+      get_invalid_ptes_with_inv_time_by_lvl_asid
+        ts init mem tid tlb trans_time lvl va None ttbr;
     mret (candidates_asid ++ candidates_global).
 
   Definition get_invalid_ptes_with_inv_time (ts : TState.t) (init : Memory.initial)
@@ -1741,7 +1765,9 @@ Definition get_invalid_entries_from_snapshots (snapshots : list (TLB.t * nat))
     if decide (is_ets2 ∧ trans_time < ts.(TState.vwr) ⊔ ts.(TState.vrd)) then
       entries
     else
-      candidates ← TLB.get_invalid_ptes_with_inv_time ts init mem tid tlb trans_time va asid ttbr;
+      candidates ←
+        TLB.get_invalid_ptes_with_inv_time
+          ts init mem tid tlb trans_time va asid ttbr;
       prev ←@{result string} entries;
       let new :=
         omap (λ '(path, ti_opt),
@@ -1771,8 +1797,10 @@ Definition run_trans_start (trans_start : TranslationStartInfo)
   trans_res ←
     if decide (va_in_range va) then
       ttbr ← mlift $ ttbr_of_regime va trans_start.(TranslationStartInfo_regime);
-      snapshots ← mlift $ TLB.unique_snapshots_until_timestamp ts init mem vmax_t va ttbr;
-      valid_entries ← mlift $ get_valid_entries_from_snapshots snapshots mem tid va asid;
+      snapshots ← mlift $
+        TLB.unique_snapshots_until_timestamp ts init mem vmax_t va ttbr;
+      valid_entries ← mlift $
+        get_valid_entries_from_snapshots snapshots mem tid va asid;
       invalid_entries ← mlift $
         get_invalid_entries_from_snapshots snapshots ts init mem tid is_ets2 va asid ttbr;
       (* update IIS with either a valid translation result or a fault *)
@@ -1847,8 +1875,8 @@ Definition run_take_exception (fault : exn) (vmax_t : view) :
 
 (** Runs an outcome. *)
 Section RunOutcome.
-  Context (tid : nat) (initmem : memoryMap).
 
+Context (tid : nat) (initmem : memoryMap).
   Equations run_outcome (out : outcome) (mem_update : bool) :
       Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out * option view) :=
   | RegRead reg racc, mem_update =>