cheri_perms_and accepts morello mask

coq/CheriMemory/CheriMorelloMemory.v

@@ -3250,12 +3250,14 @@ Module Type CheriMemoryImpl
               mem_state_with_funptrmap funptrmap st))
         ;;
         match mask_val with
-        | MVinteger (CoqIntegerType.Size_t as ity) (IV n_value)
+        | MVinteger (CoqIntegerType.Size_t as ity) (IV z_value)
           =>
             iss <- option2memM "is_signed_ity failed" (is_signed_ity DEFAULT_FUEL ity) ;;
             sz <- serr2InternalErr (sizeof DEFAULT_FUEL None (CoqCtype.Ctype [](CoqCtype.Basic (CoqCtype.Integer ity)))) ;;
-            bytes_value <- serr2InternalErr (bytes_of_Z iss sz n_value) ;;
-            let bits := bool_bits_of_bytes bytes_value in
+            bytes_value <- serr2InternalErr (bytes_of_Z iss sz z_value) ;;
+            let bits := List.rev (bool_bits_of_bytes bytes_value) in
+            let bits := list.take (BinNat.N.to_nat Permissions.len) bits in
+            let bits := List.map negb bits in
             match Permissions.of_list bits with
             | None =>
                 fail loc

coq/Common/Utils.v

@@ -175,7 +175,7 @@ Definition bool_bits_of_bytes (bytes : list ascii): list bool
     | Ascii a0 a1 a2 a3 a4 a5 a6 a7 => [a7; a6; a5; a4; a3; a2; a1; a0]
     end
   in
-  List.fold_left (fun l a => List.app l (ascii_to_bits a)) bytes [].
+  List.fold_left (fun l a => List.app (ascii_to_bits a) l) bytes [].
 
 (* size is in bytes *)
 Definition bytes_of_Z (is_signed: bool) (size: nat) (i: Z): serr (list ascii)

frontend/model/translation_aux.lem

@@ -445,10 +445,11 @@ let conv_arith stdlib ty_src ty_dst pe =
   memop(cheri_perms_and, ptr, mask)
 *)
 let cheri_readonly_perms ptr_ty ptr_pe =
-  (* TODO: the mask should be ~(BIT(16)|BIT(13)|BIT(12)) but there is
-      currently a mismatch in the Coq memory model between the mask u64 and
-      the Permission.t value. -- FIXME when the coq is updated *)
-  (* let mask_pe = Caux.mk_integer_pe 0xfffffffffffecfff in *)
-  let mask_pe = Caux.mk_integer_pe 0xffffffffff7fffff in
+  (* C equivalent:
+     size_t mask = ~(CHERI_PERM_STORE|CHERI_PERM_STORE_CAP|CHERI_PERM_STORE_LOCAL_CAP);
+
+     for Morello, `mask` is 64-bit unsigned integer.
+   *)
+  let mask_pe = Caux.mk_integer_pe 0xfffffffffffecfff in
   Caux.mk_memop_e (Mem_common.CHERI_intrinsic "cheri_perms_and" (ptr_ty, [ptr_ty; size_t]))
     [ ptr_pe; mask_pe ]