CHERI: _Alignas handling

rems-project · Aug 18, 2024 · a93fb23 · a93fb23
1 parent bbe0233
commit a93fb23
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 14 deletions.
diff --git a/coq/CheriMemory/CheriMorelloMemory.v b/coq/CheriMemory/CheriMorelloMemory.v
@@ -541,7 +541,7 @@ Module Type CheriMemoryImpl
         (* mprint_msg ("Alloc: " ++ String.hex_str addr ++ " (" ++ String.dec_str size ++ ")" ) ;; *)
         ret (alloc_id, (AddressValue.of_Z addr)).
 
-  Definition alignof
+  Fixpoint alignof
     (fuel: nat)
     (maybe_tagDefs : option (SymMap.t CoqCtype.tag_definition))
     (ty: CoqCtype.ctype): serr nat
@@ -583,8 +583,12 @@ Module Type CheriMemoryImpl
                         alignof_ fuel (CoqCtype.Ctype [] (CoqCtype.Array elem_ty None))
                     end ;;
                   monadic_fold_left
-                    (fun acc '(_, (_, _, _, ty)) =>
-                       al <- alignof_ fuel ty ;;
+                    (fun acc '(_, (_, align_opt, _, ty)) =>
+                       al <- match align_opt with
+                            | None => alignof fuel (Some tagDefs) ty
+                            | Some (CoqCtype.AlignInteger al_n) => ret (Z.to_nat al_n)
+                            | Some (CoqCtype.AlignType al_ty) => alignof fuel (Some tagDefs) al_ty
+                            end ;;
                        ret (Nat.max al acc)
                     )
                     membrs
@@ -597,8 +601,12 @@ Module Type CheriMemoryImpl
                   raise "no alignment for union with struct tag"
               | Some (CoqCtype.UnionDef membrs) =>
                   monadic_fold_left
-                    (fun acc '(_, (_, _, ty)) =>
-                       al <- alignof_ fuel ty ;;
+                    (fun acc '(_, (_, align_opt, _, ty)) =>
+                       al <- match align_opt with
+                            | None => alignof fuel (Some tagDefs) ty
+                            | Some (CoqCtype.AlignInteger al_n) => ret (Z.to_nat al_n)
+                            | Some (CoqCtype.AlignType al_ty) => alignof fuel (Some tagDefs) al_ty
+                            end ;;
                        ret (Nat.max al acc)
                     )
                     membrs
@@ -629,9 +637,14 @@ Module Type CheriMemoryImpl
             in
             '(xs, maxoffset) <-
               monadic_fold_left
-                (fun '(xs, last_offset) '(membr, (_, _, _, ty))  =>
+                (fun '(xs, last_offset) '(membr, (_, align_opt, _, ty))  =>
                    size  <- sizeof fuel (Some tagDefs) ty ;;
-                   align <- alignof fuel (Some tagDefs) ty ;;
+                   align <-
+                     match align_opt with
+                     | None => alignof fuel (Some tagDefs) ty
+                     | Some (CoqCtype.AlignInteger al_n) => ret (Z.to_nat al_n)
+                     | Some (CoqCtype.AlignType al_ty) => alignof fuel (Some tagDefs) al_ty
+                     end ;;
                    let x_value := Nat.modulo last_offset align in
                    let pad :=
                      if Nat.eqb x_value O
@@ -690,9 +703,13 @@ Module Type CheriMemoryImpl
                        sassert (Nat.ltb 0 (List.length members)) "Empty union encountered" ;;
                        '(max_size, max_align) <-
                          monadic_fold_left
-                           (fun '(acc_size, acc_align) '(_, (_, _, ty)) =>
+                           (fun '(acc_size, acc_align) '(_, (_, align_opt, _, ty)) =>
                               sz <- sizeof fuel (Some tagDefs) ty ;;
-                              al <- alignof fuel (Some tagDefs) ty ;;
+                              al <- match align_opt with
+                              | None => alignof fuel (Some tagDefs) ty
+                              | Some (CoqCtype.AlignInteger al_n) => ret (Z.to_nat al_n)
+                              | Some (CoqCtype.AlignType al_ty) => alignof fuel (Some tagDefs) al_ty
+                              end ;;
                               ret (Nat.max acc_size sz, Nat.max acc_align al)
                            )
                            members (0%nat, 0%nat) ;;

diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -5266,10 +5266,16 @@ Module CheriMemoryImplWithProofs
               state_inv_steps.
               apply IHfuel in H0.
               clear - H0 H2.
-              remember (fun '(acc_size, acc_align) '(_, (_, _, ty)) =>
+
+              remember (fun '(acc_size, acc_align) '(_, (_, align_opt, _, ty)) =>
                           sz <- sizeof fuel' (Some t) ty;;
-                          al <- alignof fuel' (Some t) ty;; ret (Nat.max acc_size sz, Nat.max acc_align al))
-                         as f.
+                          al <-
+                            match align_opt with
+                            | Some (CoqCtype.AlignInteger al_n) => ret (Z.to_nat al_n)
+                            | Some (CoqCtype.AlignType al_ty) => alignof fuel' (Some t) al_ty
+                            | None => alignof fuel' (Some t) ty
+                            end;; ret (Nat.max acc_size sz, Nat.max acc_align al))
+                as f.
               assert (f_mon : forall sz sz' al al' a,
                          f (sz, al) a = inr (sz', al') ->
                          (sz <= sz')%nat).
@@ -5288,7 +5294,7 @@ Module CheriMemoryImplWithProofs
               }
               clear Heqf.
               generalize dependent sz.
-              generalize dependent al.
+              generalize dependent (Z.to_nat z).
               induction l; intros; cbn in H2.
               **
                 now invc H2.
@@ -5299,6 +5305,10 @@ Module CheriMemoryImplWithProofs
                 easy.
                 apply f_mon in FA.
                 lia.
+              **
+                admit. (* TODO: zoick *)
+              **
+                admit. (* TODO: zoick *)
     -
       clear offsetof_struct_max_offset_pos.
       intros fuel t s l max_offset OF.
@@ -5375,7 +5385,7 @@ Module CheriMemoryImplWithProofs
         easy.
         apply f_mon in F1.
         lia.
-  Qed.
+  Admitted.
 
   Fact amap_add_list_not_at
     {T: Type}