review

compiler/src/latex_printer.ml

@@ -121,8 +121,8 @@ let pp_attribute_key fmt s =
 
 let pp_aligned fmt = function
   | None -> ()
-  | Some `Aligned -> F.fprintf fmt "%aaligned" sharp ()
-  | Some `Unaligned -> F.fprintf fmt "%aunaligned" sharp ()
+  | Some `Aligned -> F.fprintf fmt "%aaligned " sharp ()
+  | Some `Unaligned -> F.fprintf fmt "%aunaligned " sharp ()
 
 let rec pp_simple_attribute fmt a = 
   match L.unloc a with 
@@ -178,7 +178,7 @@ let rec pp_expr_rec prio fmt pe =
     F.fprintf fmt "%a ? %a : %a" (pp_expr_rec p) e1 (pp_expr_rec p) e2 (pp_expr_rec p) e3;
     optparent fmt prio p ")"
 
-and pp_mem_access fmt (ty,x,e, al) =
+and pp_mem_access fmt (al, ty,x,e) =
   let pp_e fmt e = 
     match e with
     | None -> ()

compiler/src/parser.mly

@@ -235,7 +235,7 @@ prim:
 
 %inline mem_access:
 | ct=parens(utype)? LBRACKET al=unaligned? v=var e=mem_ofs? RBRACKET
-  { ct, v, e, al }
+  { al, ct, v, e }
 
 arr_access_len: 
 | COLON e=pexpr { e }

compiler/src/pretyping.ml

@@ -964,14 +964,18 @@ let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
   | S.PEGet (al, aa, ws, ({ L.pl_loc = xlc } as x), pi, olen) ->
     let x, ty = tt_var_global mode env x in
     let ty, _ = tt_as_array (xlc, ty) in
-    let al = tt_al aa al in
     let ws = Option.map_default tt_ws (P.ws_of_ty ty) ws in
     let ty = P.tu ws in
     let i,ity  = tt_expr ~mode pd env pi in
     let i = ensure_int (L.loc pi) i ity in
     begin match olen with
-    | None -> P.Pget (al, aa, ws, x, i), ty
+    | None ->
+       let al = tt_al aa al in
+       P.Pget (al, aa, ws, x, i), ty
     | Some plen ->
+       Option.may (fun _al ->
+           warning Always (L.i_loc0 (L.loc plen)) "ignored alignment annotation in array slice"
+         ) al;
       let len,ity  = tt_expr ~mode:`OnlyParam pd env plen in
       check_ty_eq ~loc:(L.loc plen) ~from:ity ~to_:P.tint;
       let ty = P.Arr(ws, len) in
@@ -1058,7 +1062,7 @@ and tt_expr_cast pd ?(mode=`AllVar) (env : 'asm Env.env) pe ty =
   cast (L.loc pe) e ety ty 
 
 and tt_mem_access pd ?(mode=`AllVar) (env : 'asm Env.env)
-           (ct, ({ L.pl_loc = xlc } as x), e, al) =
+           (al, ct, ({ L.pl_loc = xlc } as x), e) =
   let x = tt_var `NoParam env x in
   check_ty_ptr pd ~loc:xlc x.P.v_ty;
   let e = 

compiler/src/printCommon.ml

@@ -131,7 +131,7 @@ let pp_arr_access pp_gvar pp_expr pp_len fmt al aa ws x e olen =
     | None -> ()
     | Some len -> fprintf fmt " : %a" pp_len len
   in
-  fprintf fmt "%a%s[%a %a %a%a]" pp_gvar x
+  fprintf fmt "%a%s[%a%a %a%a]" pp_gvar x
     (if aa = Warray_.AAdirect then "." else "")
     pp_aligned al
     pp_btype (U ws) pp_expr e pp_len olen

compiler/src/printFexpr.ml

@@ -13,9 +13,9 @@ let rec pp_fexpr fmt =
 let pp_rexpr fmt =
   function
   | Rexpr e -> pp_fexpr fmt e
-  | Load (al, sz, x, e) -> Format.fprintf fmt "(u%a)[%a + %a%a]" pp_wsize sz pp_var_i x pp_fexpr e pp_aligned al
+  | Load (al, sz, x, e) -> Format.fprintf fmt "(u%a)[%a%a + %a]" pp_wsize sz pp_aligned al pp_var_i x pp_fexpr e
 
 let pp_lexpr fmt =
   function
   | LLvar x -> pp_var_i fmt x
-  | Store (al, sz, x, e) -> Format.fprintf fmt "(u%a)[%a + %a%a]" pp_wsize sz pp_var_i x pp_fexpr e pp_aligned al
+  | Store (al, sz, x, e) -> Format.fprintf fmt "(u%a)[%a%a + %a]" pp_wsize sz pp_aligned al pp_var_i x pp_fexpr e

compiler/src/syntax.ml

@@ -163,7 +163,7 @@ type pexpr_r =
 
 and pexpr = pexpr_r L.located
 
-and mem_access = wsize option * pident * ([`Add | `Sub] * pexpr) option * [`Aligned|`Unaligned] option
+and mem_access = [ `Aligned | `Unaligned ] option * wsize option * pident * ([`Add | `Sub] * pexpr) option
 
 (* -------------------------------------------------------------------- *)
 and ptype_r = TBool | TInt | TWord of wsize | TArray of wsize * pexpr

compiler/src/toEC.ml

@@ -1085,7 +1085,7 @@ module Leak = struct
         | Arr(ws,n) -> Inita (L.unloc x, arr_size ws n) :: safe
         | _ -> Initv(L.unloc x) :: safe 
       else safe 
-    | Pload (al, ws,x,e) -> (* FIXME: alignment *)
+    | Pload (al, ws,x,e) -> (* TODO: alignment *)
       is_init env x (Valid (ws, snd (add_ptr pd (gkvar x) e)) :: safe_e_rec pd env safe e)
     | Papp1 (_, e) -> safe_e_rec pd env safe e
     | Pget (al, aa, ws, x, e) ->
@@ -1125,7 +1125,7 @@ module Leak = struct
 
   let safe_lval pd env = function
     | Lnone _ | Lvar _ -> []
-    | Lmem(al, ws, x, e) -> (* FIXME: alignment *)
+    | Lmem(al, ws, x, e) -> (* TODO: alignment *)
       is_init env x (Valid (ws, snd (add_ptr pd (gkvar x) e)) :: safe_e_rec pd env [] e)
     | Laset(al, aa, ws, x,e) ->
       assert (aa = Warray_.AAscale); (* NOT IMPLEMENTED *)

proofs/compiler/stack_alloc.v

@@ -177,7 +177,7 @@ Record pos_map := {
 (* TODO: Z.land or is_align ?
    Could be just is_align (sub_region_addr sr) ws ? *)
 Definition check_align al x (sr:sub_region) ws :=
-  Let _ := assert ((al == Unaligned) || (ws <= sr.(sr_region).(r_align))%CMP) (* FIXME: is this check needed? *)
+  Let _ := assert ((al == Unaligned) || (ws <= sr.(sr_region).(r_align))%CMP) (* TODO: is this check needed? *)
                   (stk_ierror_basic x "unaligned offset") in
   assert ((al == Unaligned) || (Z.land sr.(sr_zone).(z_ofs) (wsize_size ws - 1) == 0)%Z)
          (stk_ierror_basic x "unaligned sub offset").

proofs/compiler/stack_alloc_proof.v

@@ -1197,9 +1197,9 @@ Qed.
 
 Lemma eq_sub_region_val_disjoint_range sr bytes ty mem1 mem2 v p sz :
   (forall al p1 ws1,
-      disjoint_range_ovf p sz p1 (wsize_size ws1) ->
+      disjoint_zrange_ovf p sz p1 (wsize_size ws1) ->
       read mem2 al p1 ws1 = read mem1 al p1 ws1) ->
-  disjoint_range_ovf p sz (sub_region_addr sr) (size_of ty) ->
+  disjoint_zrange_ovf p sz (sub_region_addr sr) (size_of ty) ->
   eq_sub_region_val ty mem1 sr bytes v ->
   eq_sub_region_val ty mem2 sr bytes v.
 Proof.
@@ -1218,7 +1218,7 @@ Lemma disjoint_source_word rmap m0 s1 s2 :
   valid_state rmap m0 s1 s2 ->
   forall s al p ws,
     Sv.In s Slots -> validw s1.(emem) al p ws ->
-    disjoint_range_ovf p (wsize_size ws) (Addr s) (size_slot s).
+    disjoint_zrange_ovf p (wsize_size ws) (Addr s) (size_slot s).
 Proof.
   move=> hvs s al p ws hin /validwP [] hal hd i i' /hd.
   rewrite (validw8_alignment Aligned) !addE => hi hi'.
@@ -1762,15 +1762,15 @@ Proof.
         apply: (eq_sub_region_val_disjoint_range hreadeq _ (hval _ _ _ _ hgvalid hgy)).
         have := disjoint_source_word hvs hwfy.(wfr_slot) hvp1.
         have := zbetween_sub_region_addr hwfy.
-        exact: zbetween_disjoint_range_ovf.
+        exact: zbetween_disjoint_zrange_ovf.
       move=> y sry hgy.
       have [pk [hgpk hvpk]] := hptr _ _ hgy; exists pk; split => //.
       case: pk hgpk hvpk => //= s ofs ws' z f hgpk hread /hread <-.
       apply: (writeP_neq _ hmem2).
       assert (hwf' := sub_region_stkptr_wf (wf_locals hgpk)).
       have := disjoint_source_word hvs hwf'.(wfr_slot) hvp1.
       have := zbetween_sub_region_addr hwf'.
-      exact: zbetween_disjoint_range_ovf.
+      exact: zbetween_disjoint_zrange_ovf.
     + move=> p; rewrite (write_validw_eq hmem1) => hv.
       apply: read_write_any_mem hmem1 hmem2.
       by apply heqmem.

proofs/lang/memory_model.v

@@ -386,7 +386,7 @@ Section CoreMem.
     by rewrite (write_read8 hw) (write_read8 hw') /=; case: andP.
  Qed.
 
- Definition disjoint_range_ovf p s p' s' : Prop :=
+ Definition disjoint_zrange_ovf p s p' s' : Prop :=
    ∀ i i' : Z, 0 <= i < s → 0 <= i' < s' → add p i ≠ add p' i'.
 
 End CoreMem.
@@ -614,7 +614,7 @@ Global Opaque Pointer.
 
 Lemma disjoint_zrange_alt a m b n :
   disjoint_zrange a m b n →
-  disjoint_range_ovf a m b n.
+  disjoint_zrange_ovf a m b n.
 Proof.
   case => /ZleP ha /ZleP hb D i j hi hj.
   rewrite !addE => K.
@@ -625,10 +625,10 @@ Proof.
   by rewrite K.
 Qed.
 
-Lemma zbetween_disjoint_range_ovf a b p m n s :
-  zbetween a n b m → disjoint_range_ovf p s a n → disjoint_range_ovf p s b m.
+Lemma zbetween_disjoint_zrange_ovf a b p m n s :
+  zbetween a n b m → disjoint_zrange_ovf p s a n → disjoint_zrange_ovf p s b m.
 Proof.
-  rewrite /zbetween /disjoint_range_ovf !zify => - [] hlo hhi D i i' hi hi' K.
+  rewrite /zbetween /disjoint_zrange_ovf !zify => - [] hlo hhi D i i' hi hi' K.
   set ofs := wunsigned b - wunsigned a.
   have hofs : 0 <= ofs + i' < n by Lia.lia.
   apply: (D _ _ hi hofs).