additional alignment checks in repr

rems-project · Aug 12, 2024 · efaa7ba · efaa7ba
1 parent 6d711f1
commit efaa7ba
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 15 deletions.
diff --git a/coq/CheriMemory/CheriMorelloMemory.v b/coq/CheriMemory/CheriMorelloMemory.v
@@ -750,19 +750,14 @@ Module Type CheriMemoryImpl
     let align := IMP.get.(alignof_pointer) in
     (AddressValue.to_Z addr) mod (Z.of_nat align) =? 0.
 
-  (** Update [capmeta] dictionary for capability [c] stored at [addr].
-      If address is capability-aligned, then the tag and ghost state
-      is stored. Otherwise capmeta is left unchanged.  *)
+  (** Update [capmeta] dictionary for capability [c] stored at [addr]. *)
   Definition update_capmeta
     (c: C.t)
     (addr: AddressValue.t)
     (capmeta : AMap.M.t (bool*CapGhostState))
     : AMap.M.t (bool*CapGhostState)
     :=
-    if is_pointer_algined addr
-    then AMap.M.add addr (C.cap_is_valid c, C.get_ghost_state c) capmeta
-    else capmeta.
-
+    AMap.M.add addr (C.cap_is_valid c, C.get_ghost_state c) capmeta.
 
   Fixpoint repr
     (fuel: nat)
@@ -797,6 +792,7 @@ Module Type CheriMemoryImpl
             | CoqIntegerType.Unsigned CoqIntegerType.Intptr_t
               =>
                 '(cb, ct) <- option2serr "int encoding error" (C.encode true c_value) ;;
+                sassert (is_pointer_algined addr) "unaligned pointer to cap" ;;
                 let capmeta := update_capmeta c_value addr capmeta in
                 sassert (AddressValue.to_Z addr + (Z.of_nat (length cb)) <=? AddressValue.ADDR_LIMIT) "object does not fit in address space" ;;
                 ret (funptrmap, capmeta, List.map (Some) cb)
@@ -816,11 +812,13 @@ Module Type CheriMemoryImpl
                   fp) =>
                 let '(funptrmap, c_value) := resolve_function_pointer funptrmap fp in
                 '(cb, ct) <- option2serr "valid function pointer encoding error" (C.encode true c_value) ;;
+                sassert (is_pointer_algined addr) "unaligned pointer to cap" ;;
                 let capmeta := update_capmeta c_value addr capmeta in
                 sassert (AddressValue.to_Z addr + (Z.of_nat (length cb)) <=? AddressValue.ADDR_LIMIT) "object does not fit in address space" ;;
                 ret (funptrmap, capmeta, List.map (Some) cb)
             | (PVfunction (FP_invalid c_value) | PVconcrete c_value) =>
                 '(cb, ct) <- option2serr "pointer encoding error" (C.encode true c_value) ;;
+                sassert (is_pointer_algined addr) "unaligned pointer to cap" ;;
                 let capmeta := update_capmeta c_value addr capmeta in
                 sassert (AddressValue.to_Z addr + (Z.of_nat (length cb)) <=? AddressValue.ADDR_LIMIT) "object does not fit in address space" ;;
                 ret (funptrmap, capmeta, List.map (Some) cb)

diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -5826,12 +5826,16 @@ Module CheriMemoryImplWithProofs
       forall (c : Capability_GS.t) (cb : list ascii) (b:bool),
         Capability_GS.encode true c = Some (cb, b) ->
         forall start : AddressValue.t,
+          is_pointer_algined start = true ->
           AddressValue.to_Z start + Z.of_nat (Datatypes.length cb) <= AddressValue.ADDR_LIMIT ->
           forall bs : list (option ascii),
             bs = map Some cb ->
             mem_invariant (mem_state_with_funptrmap_bytemap_capmeta (funptrmap s) (AMap.map_add_list_at (bytemap s) bs start) (update_capmeta c start (capmeta s)) s).
   Proof.
-    intros s Bdead Bnooverlap Bfit Balign Bnextallocid Blastaddr MIcap c cb ct start RSZ bs Heqbs.
+    intros s Bdead Bnooverlap Bfit Balign Bnextallocid Blastaddr MIcap c cb ct E start SA RSZ bs Heqbs.
+
+
+    (* TODO: this proof must be substantionally similar to [mem_state_with_bytes_preserves] *)
   Admitted.
 
   Lemma repr_preserves
@@ -5895,13 +5899,13 @@ Module CheriMemoryImplWithProofs
         repeat break_match_hyp; state_inv_steps.
         *
           generalize dependent (Capability_GS.cap_get_value c); clear c.
-          intros start RSZ IHfuel.
+          intros start R4 RSZ IHfuel.
           bool_to_prop_hyp.
           remember (map Some l) as bs.
           eapply mem_state_with_cap_preserves;eauto.
         *
           generalize dependent (Capability_GS.cap_get_value c); clear c.
-          intros start RSZ IHfuel.
+          intros start R4 RSZ IHfuel.
           bool_to_prop_hyp.
           remember (map Some l) as bs.
           eapply mem_state_with_cap_preserves;eauto.
@@ -5934,23 +5938,25 @@ Module CheriMemoryImplWithProofs
           state_inv_step_quick.
           break_let.
           state_inv_step_quick.
-          apply ret_inr in R5.
-          inversion R5; clear R5.
+          state_inv_step_quick.
+          apply ret_inr in R6.
+          inversion R6; clear R6.
           bool_to_prop_hyp.
           eapply mem_state_with_cap_preserves;eauto.
         *
           state_inv_step_quick.
           break_let.
           state_inv_step_quick.
           state_inv_step_quick.
-          apply ret_inr in R5.
-          inversion R5; clear R5.
+          state_inv_step_quick.
+          apply ret_inr in R6.
+          inversion R6; clear R6.
           bool_to_prop_hyp.
           eapply mem_state_with_cap_preserves;eauto.
       +
         state_inv_steps.
         generalize dependent (Capability_GS.cap_get_value c); clear c.
-        intros start RSZ.
+        intros start R4 RSZ.
         bool_to_prop_hyp.
         remember (map Some l) as bs.
         eapply mem_state_with_cap_preserves;eauto.