What a nice syntactic choice

compiler/src/latex_printer.ml

@@ -120,8 +120,8 @@ let pp_attribute_key fmt s =
   else F.fprintf fmt "%S" s
 
 let pp_aligned fmt = function
-  | None -> ()
-  | Some `Unaligned -> F.fprintf fmt "߸"
+  | None | Some `Aligned -> ()
+  | Some `Unaligned -> F.fprintf fmt "%aunaligned" sharp ()
 
 let rec pp_simple_attribute fmt a = 
   match L.unloc a with 
@@ -183,7 +183,7 @@ and pp_mem_access fmt (ty,x,e, al) =
     | None -> ()
     | Some (`Add, e) -> Format.fprintf fmt " + %a" pp_expr e 
     | Some (`Sub, e) -> Format.fprintf fmt " - %a" pp_expr e in
-  F.fprintf fmt "%a[%a%a%a]" (pp_opt (pp_paren pp_ws)) ty pp_var x pp_e e pp_aligned al
+  F.fprintf fmt "%a[%a%a%a]" (pp_opt (pp_paren pp_ws)) ty pp_aligned al pp_var x pp_e e
 
 and pp_type fmt ty =
   match L.unloc ty with
@@ -203,8 +203,8 @@ and pp_arr_access fmt al aa ws x e len=
  F.fprintf fmt "%a%s[%a%a%a%a%a]"
     pp_var x
     (if aa = Warray_.AAdirect then "." else "")
-    (pp_opt pp_ws) ws (pp_opt pp_space) ws pp_expr e pp_olen len
     pp_aligned al
+    (pp_opt pp_ws) ws (pp_opt pp_space) ws pp_expr e pp_olen len
 
 let pp_writable = function
   | Some `Constant -> " const"

compiler/src/lexer.mll

@@ -181,7 +181,8 @@ rule main = parse
   | "="  { EQ       }
   | "==" { EQEQ     }
   | "!=" { BANGEQ   }
-  | "߸" { UNALIGNED   }
+  | "#unaligned" { UNALIGNED   }
+  | "#aligned" { ALIGNED   }
 
   | _ as c  { invalid_char (L.of_lexbuf lexbuf) c }
   | eof     { EOF }

compiler/src/parser.mly

@@ -23,6 +23,7 @@
 %token T_U8 T_U16 T_U32 T_U64 T_U128 T_U256 T_INT 
 
 %token SHARP
+%token ALIGNED
 %token AMP
 %token AMPAMP
 %token BANG
@@ -229,17 +230,18 @@ prim:
 | MINUS e=pexpr { `Sub, e }
 
 %inline unaligned:
+| ALIGNED { `Aligned }
 | UNALIGNED { `Unaligned }
 
 %inline mem_access:
-| ct=parens(utype)? LBRACKET v=var e=mem_ofs? al=unaligned? RBRACKET
+| ct=parens(utype)? LBRACKET al=unaligned? v=var e=mem_ofs? RBRACKET
   { ct, v, e, al }
 
 arr_access_len: 
 | COLON e=pexpr { e }
 
 arr_access_i:
-| ws=utype? e=pexpr len=arr_access_len? al=unaligned? {ws, e, len, al }
+| al=unaligned? ws=utype? e=pexpr len=arr_access_len? {ws, e, len, al }
 
 arr_access:
  | s=DOT?  i=brackets(arr_access_i) {

compiler/src/pretyping.ml

@@ -953,7 +953,7 @@ let ensure_int loc i ty =
 (* -------------------------------------------------------------------- *)
 let tt_al = function
   | Some `Unaligned -> Memory_model.Unaligned
-  | None -> Memory_model.Aligned
+  | Some `Aligned | None -> Memory_model.Aligned
 
 (* -------------------------------------------------------------------- *)
 let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =

compiler/src/printCommon.ml

@@ -18,7 +18,7 @@ let pp_aligned fmt =
   function
   | Memory_model.Aligned -> ()
   | Unaligned ->
-     Format.fprintf fmt " ߸"
+     Format.fprintf fmt "#unaligned "
 
 (* -------------------------------------------------------------------- *)
 
@@ -132,8 +132,8 @@ let pp_arr_access pp_gvar pp_expr pp_len fmt al aa ws x e olen =
   in
   fprintf fmt "%a%s[%a %a %a%a]" pp_gvar x
     (if aa = Warray_.AAdirect then "." else "")
-    pp_btype (U ws) pp_expr e pp_len olen
     pp_aligned al
+    pp_btype (U ws) pp_expr e pp_len olen
 
 (* -------------------------------------------------------------------- *)
 let pp_len fmt len = fprintf fmt "%i" len

compiler/src/syntax.ml

@@ -149,7 +149,7 @@ module W = Wsize
 type pexpr_r =
   | PEParens of pexpr
   | PEVar    of pident
-  | PEGet    of [`Unaligned] option * arr_access * wsize option * pident * pexpr * pexpr option
+  | PEGet    of [`Aligned|`Unaligned] option * arr_access * wsize option * pident * pexpr * pexpr option
   | PEFetch  of mem_access
   | PEpack   of svsize * pexpr list
   | PEBool   of bool
@@ -163,7 +163,7 @@ type pexpr_r =
 
 and pexpr = pexpr_r L.located
 
-and mem_access = wsize option * pident * ([`Add | `Sub] * pexpr) option * [`Unaligned] option
+and mem_access = wsize option * pident * ([`Add | `Sub] * pexpr) option * [`Aligned|`Unaligned] option
 
 (* -------------------------------------------------------------------- *)
 and ptype_r = TBool | TInt | TWord of wsize | TArray of wsize * pexpr
@@ -181,7 +181,7 @@ type annot_pstotype = annotations * pstotype
 type plvalue_r =
   | PLIgnore
   | PLVar   of pident
-  | PLArray of [`Unaligned] option * arr_access * wsize option * pident * pexpr * pexpr option
+  | PLArray of [`Aligned|`Unaligned] option * arr_access * wsize option * pident * pexpr * pexpr option
   | PLMem   of mem_access 
 
 type plvalue = plvalue_r L.located

compiler/tests/success/common/unaligned.jazz

@@ -3,6 +3,6 @@ fn main(reg u32 x) -> reg u32 {
   stack u32[2] a;
   a[0] = x;
   a[1] = x;
-  x = a.[2߸];
+  x = a.[#unaligned 2];
   return x;
 }

compiler/tests/success/x86-64/unaligned.jazz

@@ -8,7 +8,7 @@ fn main(reg u64 x) -> reg u128 {
   }
   ?{}, r = #set0_128();
   for i = 0 to 3 {
-    r ^= a.[i * 8߸];
+    r ^= a.[#unaligned i * 8];
   }
   return r;
 }
@@ -18,7 +18,7 @@ fn sopndest() -> reg u64 {
   stack u128[2] a;
   reg u128 x;
   x = #set0_128();
-  a.[8߸] = x;
+  a.[#unaligned 8] = x;
   reg u64 r;
   r = a.[u64 8];
   return r;
@@ -29,8 +29,8 @@ fn add_in_mem(reg u64 x y) -> reg u64 {
   stack u64[2] s;
   s[0] = 0;
   s[1] = 0;
-  s.[4߸] = x;
-  s.[4߸] += y;
+  s.[#unaligned 4] = x;
+  s.[#unaligned 4] += y;
   x = s[0];
   return x;
 }

proofs/compiler/x86_params_proof.v

@@ -415,7 +415,7 @@ Qed.
 Lemma check_sopn_args_xmm rip ii oargs es ads cond n k ws:
   check_sopn_args x86_agparams rip ii oargs es ads ->
   check_i_args_kinds [::cond] oargs ->
-  nth (E 0, sword8) ads n = (E k, sword ws) ->
+  nth (Eu 0, sword8) ads n = (Eu k, sword ws) ->
   nth xmm cond k = xmm ->
   n < size es ->
   exists (r: xreg_t),
@@ -424,7 +424,7 @@ Lemma check_sopn_args_xmm rip ii oargs es ads cond n k ws:
     oseq.onth oargs k = Some (XReg r).
 Proof.
   rewrite /= orbF => hca hc hE hxmm hn.
-  have /(_ n):= all2_nth (Rexpr (Fconst 0)) (E 0, sword8) _ hca.
+  have /(_ n):= all2_nth (Rexpr (Fconst 0)) (Eu 0, sword8) _ hca.
   rewrite hn => /(_ erefl) ha.
   assert (hcIaux := check_sopn_argP ha).
   move: hcIaux; rewrite hE => h; inversion_clear h.
@@ -443,10 +443,10 @@ Proof.
     eauto.
 Qed.
 
-Lemma check_sopn_dests_xmm rip ii oargs xs ads cond n k ws:
+Lemma check_sopn_dests_xmm rip ii oargs xs ads cond n al k ws:
   check_sopn_dests x86_agparams rip ii oargs xs ads ->
   check_i_args_kinds [::cond] oargs ->
-  nth (E 0, sword8) ads n = (E k, sword ws) ->
+  nth (Ea 0, sword8) ads n = (ADExplicit (AK_mem al) k None, sword ws) ->
   nth xmm cond k = xmm ->
   n < size xs ->
   exists (r: xreg_t),
@@ -456,7 +456,7 @@ Lemma check_sopn_dests_xmm rip ii oargs xs ads cond n k ws:
     oseq.onth oargs k = Some (XReg r).
 Proof.
   rewrite /= orbF => hca hc hE hxmm hn.
-  have /(_ n):= all2_nth (Rexpr (Fconst 0)) (E 0, sword8) _ hca.
+  have /(_ n):= all2_nth (Rexpr (Fconst 0)) (Ea 0, sword8) _ hca.
   rewrite size_map hn => /(_ erefl).
   rewrite (nth_map (LLvar (mk_var_i rip))) //.
   set e := nth (LLvar _) _ _.
@@ -498,7 +498,7 @@ Proof.
   have [yr [vi /= ? hyr]] := check_sopn_dests_xmm (n:=0) hcd hidc erefl erefl erefl; subst y ops ops'.
   have [s' hwm hlow'] :=
     compile_lvals (asm_e:=x86_extra)
-     (id_out := [:: E 0]) (id_tout := [:: sword256]) MSB_CLEAR refl_equal hwr hlow hcd refl_equal.
+     (id_out := [:: Eu 0]) (id_tout := [:: sword256]) MSB_CLEAR refl_equal hwr hlow hcd refl_equal.
   exists s'; last done.
   move: hca; rewrite /check_sopn_args /= => /and4P [] _ hE2 hE3 _.
   have [vh' hev2 /= hvh']:= check_sopn_arg_sem_eval eval_assemble_cond hlow hE2 hvh hwh.