review

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,29 @@ 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;
 }
+
+export
+fn sopndest() -> reg u64 {
+  stack u128[2] a;
+  reg u128 x;
+  x = #set0_128();
+  a.[#unaligned 8] = x;
+  reg u64 r;
+  r = a.[u64 8];
+  return r;
+}
+
+export
+fn add_in_mem(reg u64 x y) -> reg u64 {
+  stack u64[2] s;
+  s[0] = 0;
+  s[1] = 0;
+  s.[#unaligned 4] = x;
+  s.[#unaligned 4] += y;
+  x = s[0];
+  return x;
+}

proofs/arch/arch_decl.v

@@ -260,10 +260,10 @@ Variant arg_desc :=
 
 Definition F  f   := ADImplicit (IArflag f).
 Definition R  r   := ADImplicit (IAreg   r).
-Definition E  n   := ADExplicit (AK_mem Aligned) n None. (* TODO: alignment *)
-Definition Eu n   := ADExplicit (AK_mem Unaligned) n None. (* TODO: alignment *)
+Definition Ea n   := ADExplicit (AK_mem Aligned) n None.
+Definition Eu n   := ADExplicit (AK_mem Unaligned) n None.
 Definition Ec n   := ADExplicit AK_compute n None.
-Definition Ef n r := ADExplicit (AK_mem Aligned) n (Some  r). (* TODO: alignment *)
+Definition Ef n r := ADExplicit (AK_mem Aligned) n (Some  r).
 
 Definition check_oreg or ai :=
   match or, ai with

proofs/arch/arch_sem.v

@@ -333,7 +333,7 @@ Definition mem_write_word (f:msb_flag) (s:asmmem) (args:asm_args) (ad:arg_desc)
   match ad with
   | ADImplicit (IAreg r)   => ok (mem_write_reg f r w s)
   | ADImplicit (IArflag f) => type_error
-  | ADExplicit _ i or    =>
+  | ADExplicit k i or    =>
     match onth args i with
     | None => type_error
     | Some a =>
@@ -342,7 +342,10 @@ Definition mem_write_word (f:msb_flag) (s:asmmem) (args:asm_args) (ad:arg_desc)
       | Reg r   => ok (mem_write_reg  f r w s)
       | Regx r  => ok (mem_write_regx  f r w s)
       | XReg x  => ok (mem_write_xreg f x w s)
-      | Addr addr => mem_write_mem Aligned (decode_addr s addr) w s (* TODO: alignement *)
+      | Addr addr =>
+          if k is AK_mem al
+          then mem_write_mem al (decode_addr s addr) w s
+          else type_error
       | _       => type_error
       end
     end
@@ -392,13 +395,13 @@ Definition eval_op o args m :=
 (* -------------------------------------------------------------------- *)
 Definition eval_POP (s: asm_state) : exec (asm_state * wreg) :=
   Let sp := truncate_word Uptr (s.(asm_m).(asm_reg) ad_rsp) in
-  Let v := read s.(asm_m).(asm_mem) Aligned sp reg_size in (* TODO: alignment *)
+  Let v := read s.(asm_m).(asm_mem) Aligned sp reg_size in
   let m := mem_write_reg MSB_CLEAR ad_rsp (sp + wrepr Uptr (wsize_size Uptr))%R s.(asm_m) in
   ok ({| asm_m := m ; asm_f := s.(asm_f) ; asm_c := s.(asm_c) ; asm_ip := s.(asm_ip).+1 |}, v).
 
 Definition eval_PUSH (w: wreg) (s: asm_state) : exec asm_state :=
   Let sp := truncate_word Uptr (s.(asm_m).(asm_reg) ad_rsp) in
-  Let m := mem_write_mem Aligned (sp - wrepr Uptr (wsize_size Uptr))%R w s.(asm_m) in (* TODO: alignment *)
+  Let m := mem_write_mem Aligned (sp - wrepr Uptr (wsize_size Uptr))%R w s.(asm_m) in
   let m := mem_write_reg MSB_CLEAR ad_rsp (sp - wrepr Uptr (wsize_size Uptr))%R m in
   ok {| asm_m := m ; asm_f := s.(asm_f) ; asm_c := s.(asm_c) ; asm_ip := s.(asm_ip).+1 |}.
 
@@ -516,10 +519,11 @@ Proof.
   - by move => ? _; case: d.1 => // - [] // ? /ok_inj <-.
   move => ? ? _; case: d.1 => [ [] | ] //=.
   - by move => ? /ok_inj <-.
-  move => _ ? ?; case: onth => //; t_xrbindP => - [] // ? _.
+  move => k ? ?; case: onth => //; t_xrbindP => - [] // ? _.
   - by move=> /ok_inj <-.
   - by move=> /ok_inj <-.
-  - by exact: mem_write_mem_invariant.
+  - case: k => // al.
+    by exact: mem_write_mem_invariant.
   by move => /ok_inj <-.
 Qed.
 

proofs/arch/asm_gen.v

@@ -228,10 +228,6 @@ Definition xreg_of_var ii (x: var_i) : cexec asm_arg :=
   else if to_regx x is Some r then ok (Regx r)
   else Error (E.verror false "Not a (x)register" ii x).
 
-(* TODO: move *)
-Definition aligned_le (x y: aligned) : bool :=
-  (x == Unaligned) || (y == Aligned).
-
 Definition assemble_word_load rip ii al (sz: wsize) (e: rexpr) :=
   match e with
   | Rexpr (Fapp1 (Oword_of_int sz') (Fconst z)) =>
@@ -343,10 +339,12 @@ Definition check_sopn_arg rip ii (loargs : seq asm_arg) (x : rexpr) (adt : arg_d
 Definition check_sopn_dest rip ii (loargs : seq asm_arg) (x : rexpr) (adt : arg_desc * stype) :=
   match adt.1 with
   | ADImplicit i => is_implicit i x
-  | ADExplicit _ n o =>
+  | ADExplicit k n o =>
     match onth loargs n with
     | Some a =>
-      if arg_of_rexpr (AK_mem Aligned) rip ii adt.2 x is Ok a' then (a == a') && check_oreg o a
+      if k is AK_mem al then
+      if arg_of_rexpr (AK_mem al) rip ii adt.2 x is Ok a' then (a == a') && check_oreg o a
+      else false
       else false
     | None => false
     end

proofs/arch/asm_gen_proof.v

@@ -359,19 +359,6 @@ Definition assemble_cond_spec :=
 Context
   (eval_assemble_cond : assemble_cond_spec).
 
-(* TODO: move *)
-Lemma aligned_leP al al' p sz :
-  aligned_le al al' →
-  is_aligned_if al' p sz →
-  is_aligned_if al p sz.
-Proof. by case: al => // /eqP ->. Qed.
-
-Lemma read_relax_aligned m p sz v al al' :
-  aligned_le al al' →
-  read m al' p sz = ok v →
-  read m al p sz = ok v.
-Proof. by rewrite /read; t_xrbindP => h /(aligned_leP h) -> ? -> /= ->. Qed.
-
 Lemma check_sopn_arg_sem_eval rip m s ii args e ad ty v vt :
   lom_eqv rip m s
   -> check_sopn_arg agparams rip ii args e (ad,ty)
@@ -408,7 +395,7 @@ Proof.
     move: hcomp; rewrite /compat_imm orbF => /eqP <-.
     move=> w1 wp vp hget htop wp' vp' hp hp' wr hwr <- /= htr.
     have -> := addr_of_xpexprP eqm hr hget htop hp hp'.
-    by case: eqm => ? <- ??????; rewrite (read_relax_aligned ok_al' hwr) /=; eauto.
+    by case: eqm => ? <- ??????; rewrite (aligned_le_read ok_al' hwr) /=; eauto.
   case => //.
   + move=> x al.
     move=> /xreg_of_varI; case: a' hcomp => // r;
@@ -571,6 +558,7 @@ Proof.
     have /(_ r erefl) := lom_eqv_write_var msb_flag hlom hw.
     rewrite /mem_write_val /= truncate_word_u /=; eauto.
   case heq1: onth => [a | //].
+  case heq3: k => [ // | al ].
   case heq2: arg_of_rexpr => [ a' | //] hty hw he1 /andP[] /eqP ? hc; subst a'.
   rewrite /mem_write_val /mem_write_ty.
   case: lv1 hw he1 heq2=> //=; cycle 1.
@@ -612,15 +600,15 @@ Proof.
       + by apply word_uincl_word_extend => //; apply cmp_lt_le.
       by rewrite word_extend_big //;apply /negP.
     by move=> f; rewrite Vm.setP_neq.
-  move=> al sz [x xii] /= e; t_xrbindP.
+  move=> al' sz [x xii] /= e; t_xrbindP.
   move=> wp vp hget hp wofs vofs he hofs w hw m1 hm1 ??; subst m' e1.
   case: ty hty vt hw => //= sz' _ vt hw.
-  t_xrbindP => /eqP ? /eqP ?; subst sz' al.
+  t_xrbindP => /eqP ? hal; subst sz'.
   move: hw; rewrite truncate_word_u => -[?]; subst vt.
   move => adr hadr ?; subst a => /=.
   rewrite /= heq1 hc /= /mem_write_mem -h1.
   have -> := addr_of_xpexprP hlom hadr hget hp he hofs.
-  rewrite hm1 /=; eexists; split; first by reflexivity.
+  rewrite (aligned_le_write hal hm1) /=; eexists; split; first by reflexivity.
   by constructor.
 Qed.
 
@@ -1270,7 +1258,7 @@ Proof.
     exact: (ofgetxreg eqm ok_r ok_v).
   move => al' sz' ? ? _ /=; t_xrbindP => /eqP <-{sz'} ok_al' d ok_d <- ptr w ok_w ok_ptr uptr u ok_u ok_uptr ? ok_rd ?; subst v => /=.
   case: (eqm) => _ eqmem _ _ _ _ _.
-  rewrite (addr_of_xpexprP eqm ok_d ok_w ok_ptr ok_u ok_uptr) -eqmem (read_relax_aligned ok_al' ok_rd).
+  rewrite (addr_of_xpexprP eqm ok_d ok_w ok_ptr ok_u ok_uptr) -eqmem (aligned_le_read ok_al' ok_rd).
   eexists; first reflexivity.
   exact: word_uincl_refl.
 Qed.