Relaxed alignment constraints for memory and array accesses

CHANGELOG.md

@@ -86,6 +86,9 @@
 - Register allocation can print liveness information (enable with `-pliveness`)
   ([PR #749](https://github.com/jasmin-lang/jasmin/pull/749)).
 
+- Relaxed alignment constraints for memory and array accesses
+  ([PR #748](https://github.com/jasmin-lang/jasmin/pull/748)).
+
 ## Bug fixes
 
 - Type-checking rejects invalid variants of primitive operators

compiler/safety/fail/bad_align.jazz

@@ -3,7 +3,7 @@ fn main(reg u64 pt) -> reg u64 {
   reg u64 tmp;
 
   tmp = (u64)[pt + 0];
-  tmp = (u64)[pt + 1];
+  tmp = (u64)[#aligned pt + 1];
 
   return tmp;
 }

compiler/safetylib/safetyAbsExpr.ml

@@ -416,7 +416,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
 
       | Pvar x -> mvar_of_var x :: acc
 
-      | Pget(access,ws,x,ei) ->
+      | Pget(_, access,ws,x,ei) ->
         abs_sub_arr_range abs (L.unloc x.gv,x.gs) access ws 1   ei @ acc
       | Psub (access, ws, len, x, ei) -> 
         abs_sub_arr_range abs (L.unloc x.gv,x.gs) access ws len ei @ acc
@@ -606,7 +606,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
         | _ -> raise (Binop_not_supported op2)
       end
 
-    | Pget(access,ws,x,ei) ->
+    | Pget(_, access,ws,x,ei) ->
       begin
         match abs_sub_arr_range abs (L.unloc x.gv,x.gs) access ws 1 ei with
         | [] -> assert false
@@ -641,17 +641,17 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
 
     | Pconst _  | Pbool _ | Parr_init _ | Pvar _  -> None
 
-    | Pget(acc,ws,x,e1) ->
+    | Pget(al,acc,ws,x,e1) ->
       remove_if_expr_aux e1
-      |> map_f (fun ex -> Pget(acc,ws,x,ex))
+      |> map_f (fun ex -> Pget(al,acc,ws,x,ex))
 
     | Psub(acc,ws,x,len,e1) ->
       remove_if_expr_aux e1
       |> map_f (fun ex -> Psub(acc,ws,x,len,ex))
 
-    | Pload (sz, x, e1) ->
+    | Pload (al, sz, x, e1) ->
       remove_if_expr_aux e1
-      |> map_f (fun ex -> Pload (sz,x,ex))
+      |> map_f (fun ex -> Pload (al,sz,x,ex))
 
     | Papp1 (op1, e1) ->
       remove_if_expr_aux e1
@@ -1012,7 +1012,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
         | _, Bty _ -> MLvar (loc, Mlocal (Avar ux))
         | _, Arr _ -> MLvar (loc, Mlocal (Aarray ux)) end
 
-    | Laset (acc, ws, x, ei) ->
+    | Laset (_, acc, ws, x, ei) ->
       begin
         match abs_sub_arr_range abs (L.unloc x,Expr.Slocal) acc ws 1 ei with
         | [] -> assert false

compiler/safetylib/safetyInterpreter.ml

@@ -277,20 +277,26 @@ let safe_var x = match (L.unloc x).v_ty with
 let safe_gvar x = match x.gs with
   | Expr.Sglob  -> []
   | Expr.Slocal -> safe_var x.gv
-
+
+let optional_alignment_check al ws x e acc =
+  match al with
+  | Memory_model.Unaligned -> acc
+  | _ -> AlignedPtr (ws, x, e) :: acc
+
 let rec safe_e_rec safe = function
   | Pconst _ | Pbool _ | Parr_init _ -> safe
   | Pvar x -> safe_gvar x @ safe
 
-  | Pload (ws,x,e) ->
-    Valid      (ws, L.unloc x, e) ::
-    AlignedPtr (ws, L.unloc x, e) ::
-    safe_e_rec safe e
+  | Pload (al, ws,x,e) ->
+     let x = L.unloc x in
+    Valid (ws, x, e) ::
+    optional_alignment_check al ws x e
+    (safe_e_rec safe e)
 
-  | Pget (access, ws, x, e) ->
+  | Pget (al, access, ws, x, e) ->
     in_bound    x.gv access ws e 1 @
     init_get    x access ws e 1 @
-    arr_aligned (* x.gv *) access ws e @
+    (if al = Aligned then arr_aligned (* x.gv *) access ws e else []) @
     safe
 
   | Psub (access, ws, len, x, e) ->
@@ -317,14 +323,15 @@ let safe_es = List.fold_left safe_e_rec []
 let safe_lval = function
   | Lnone _ | Lvar _ -> []
 
-  | Lmem(ws, x, e) ->
-    Valid (ws, L.unloc x, e) ::
-    AlignedPtr (ws, L.unloc x, e) ::
-    safe_e_rec [] e
+  | Lmem(al, ws, x, e) ->
+    let x = L.unloc x in
+    Valid (ws, x, e) ::
+    optional_alignment_check al ws x e
+    (safe_e_rec [] e)
 
-  | Laset(access,ws, x,e) ->
+  | Laset(al, access,ws, x,e) ->
     in_bound x access ws e 1 @
-    arr_aligned (* x *) access ws e @
+    (if al = Aligned then arr_aligned (* x *) access ws e else []) @
     safe_e_rec [] e
 
   | Lasub(access,ws,len,x,e) ->
@@ -1499,7 +1506,7 @@ end = struct
 
     and nm_e vs_for = function
       | Pconst _ | Pbool _ | Parr_init _ | Pvar _ -> true
-      | Pget (_,_,_,    e) 
+      | Pget (_,_,_,_,  e)
       | Psub (_,_,_, _, e) -> know_offset vs_for e && nm_e vs_for e
       | Pload _            -> false
       | Papp1 (_, e)       -> nm_e vs_for e
@@ -1511,7 +1518,7 @@ end = struct
 
     and nm_lv vs_for = function
       | Lnone _ | Lvar _ -> true
-      | Laset (_,_,_,e) | Lasub (_,_,_,_,e) -> know_offset vs_for e
+      | Laset (_,_,_,_,e) | Lasub (_,_,_,_,e) -> know_offset vs_for e
       | Lmem _ -> false
 
     and nm_lvs vs_for lvs = List.for_all (nm_lv vs_for) lvs 

compiler/safetylib/safetyPreanalysis.ml

@@ -64,8 +64,8 @@ end = struct
   and mk_lval fn lv = match lv with
     | Lnone _ -> lv
     | Lvar v -> Lvar (mk_v_loc fn v)
-    | Lmem (ws,ty,e) -> Lmem (ws, mk_v_loc fn ty, mk_expr fn e)
-    | Laset (acc,ws,v,e) -> Laset (acc,ws, mk_v_loc fn v, mk_expr fn e)
+    | Lmem (al, ws,ty,e) -> Lmem (al, ws, mk_v_loc fn ty, mk_expr fn e)
+    | Laset (al,acc,ws,v,e) -> Laset (al,acc,ws, mk_v_loc fn v, mk_expr fn e)
     | Lasub (acc,ws,len,v,e) -> Lasub (acc,ws,len, mk_v_loc fn v, mk_expr fn e)
 
   and mk_range fn (dir, e1, e2) = (dir, mk_expr fn e1, mk_expr fn e2)
@@ -99,10 +99,10 @@ end = struct
   and mk_expr fn expr = match expr with
     | Pconst _ | Pbool _ | Parr_init _ -> expr
     | Pvar v -> Pvar (mk_gvar fn v)
-    | Pget (acc, ws, v, e) -> Pget (acc, ws, mk_gvar fn v, mk_expr fn e)
+    | Pget (al, acc, ws, v, e) -> Pget (al, acc, ws, mk_gvar fn v, mk_expr fn e)
     | Psub (acc, ws, len, v, e) ->
       Psub (acc, ws, len, mk_gvar fn v, mk_expr fn e)
-    | Pload (ws, v, e) -> Pload (ws, mk_v_loc fn v, mk_expr fn e)
+    | Pload (al, ws, v, e) -> Pload (al, ws, mk_v_loc fn v, mk_expr fn e)
     | Papp1 (op, e) -> Papp1 (op, mk_expr fn e)
     | Papp2 (op, e1, e2) -> Papp2 (op, mk_expr fn e1, mk_expr fn e2)
     | PappN (op,es) -> PappN (op, List.map (mk_expr fn) es)
@@ -186,7 +186,7 @@ end = struct
     | Psub _ -> dp  (* We ignore sub-array copies  *)
 
     (* We ignore loads for v, but we compute dependencies of v' in ei *)
-    | Pload (_,v',ei) -> app_expr dp (L.unloc v') ei ct
+    | Pload (_, _,v',ei) -> app_expr dp (L.unloc v') ei ct
 
     | Papp1 (_,e1) -> app_expr dp v e1 ct
     | Papp2  (_,e1,e2) -> app_expr (app_expr dp v e1 ct) v e2 ct
@@ -223,7 +223,7 @@ end = struct
         end
 
       (* We ignore loads for v, but we compute dependencies of v' in ei *)
-      | Pload (_,v',ei) ->
+      | Pload (_, _,v',ei) ->
         let dp = app_expr st.dp (L.unloc v') ei st.ct in
         acc, { st with dp = dp }
 
@@ -249,7 +249,7 @@ end = struct
 
       | Pvar v' -> aux_gv acc v'
       (* We ignore loads for v, but we compute dependencies of v' in ei *)
-      | Pload (_,v',ei) -> aux (aux_v acc v') ei
+      | Pload (_, _,v',ei) -> aux (aux_v acc v') ei
 
       | Papp1 (_,e1) -> aux acc e1
       | Papp2  (_,e1,e2) -> aux (aux acc e1) e2
@@ -285,7 +285,7 @@ end = struct
     | Lvar v -> pa_expr st (L.unloc v) e
 
     (* For memory stores, we are only interested in v and ei *)
-    | Lmem (_, v, ei) -> pa_expr st (L.unloc v) ei
+    | Lmem (_, _, v, ei) -> pa_expr st (L.unloc v) ei
 
 
   let rec flag_mem_lvs v = function
@@ -484,9 +484,9 @@ end = struct
         | Expr.Sglob -> sv
         | Expr.Slocal -> Sv.add (L.unloc v.gv) sv
       end
-    | Pget (_,_, v, e)   -> collect_vars_e (Sv.add (L.unloc v.gv) sv) e
+    | Pget (_,_, _, v, e)   -> collect_vars_e (Sv.add (L.unloc v.gv) sv) e
     | Psub (_,_,_, v, e) -> collect_vars_e (Sv.add (L.unloc v.gv) sv) e
-    | Pload (_, v, e) -> collect_vars_e (Sv.add (L.unloc v) sv) e
+    | Pload (_, _, v, e) -> collect_vars_e (Sv.add (L.unloc v) sv) e
     | Papp1 (_,e) -> collect_vars_e sv e
     | Papp2 (_,e1,e2) -> collect_vars_es sv [e1;e2]
     | PappN (_, el)  -> collect_vars_es sv el
@@ -496,7 +496,7 @@ end = struct
   let collect_vars_lv sv = function
     | Lnone _ -> sv
     | Lvar v -> Sv.add (L.unloc v) sv
-    | Laset (_,_, v, e) | Lasub (_,_,_, v, e) | Lmem (_, v, e) ->
+    | Laset (_,_,_, v, e) | Lasub (_,_,_, v, e) | Lmem (_, _, v, e) ->
       collect_vars_e (Sv.add (L.unloc v) sv) e
 
   let collect_vars_lvs sv = List.fold_left collect_vars_lv sv

compiler/src/conv.ml

@@ -79,10 +79,10 @@ let rec cexpr_of_expr = function
   | Pbool  b          -> C.Pbool  b
   | Parr_init n       -> C.Parr_init (pos_of_int n)
   | Pvar x            -> C.Pvar (cgvari_of_gvari x)
-  | Pget (aa,ws, x,e) -> C.Pget (aa, ws, cgvari_of_gvari x, cexpr_of_expr e)
+  | Pget (al, aa,ws, x,e) -> C.Pget (al, aa, ws, cgvari_of_gvari x, cexpr_of_expr e)
   | Psub (aa,ws,len, x,e) -> 
     C.Psub (aa, ws, pos_of_int len, cgvari_of_gvari x, cexpr_of_expr e)
-  | Pload (ws, x, e)  -> C.Pload(ws, cvari_of_vari x, cexpr_of_expr e)
+  | Pload (al, ws, x, e)  -> C.Pload(al, ws, cvari_of_vari x, cexpr_of_expr e)
   | Papp1 (o, e)      -> C.Papp1(o, cexpr_of_expr e)
   | Papp2 (o, e1, e2) -> C.Papp2(o, cexpr_of_expr e1, cexpr_of_expr e2)
   | PappN (o, es) -> C.PappN (o, List.map (cexpr_of_expr) es)
@@ -96,9 +96,9 @@ let rec expr_of_cexpr = function
   | C.Pbool  b          -> Pbool  b
   | C.Parr_init n       -> Parr_init (int_of_pos n)
   | C.Pvar x            -> Pvar (gvari_of_cgvari x)
-  | C.Pget (aa,ws, x,e) -> Pget (aa, ws, gvari_of_cgvari x, expr_of_cexpr e)
+  | C.Pget (al, aa,ws, x,e) -> Pget (al, aa, ws, gvari_of_cgvari x, expr_of_cexpr e)
   | C.Psub (aa,ws,len,x,e) -> Psub (aa, ws, int_of_pos len, gvari_of_cgvari x, expr_of_cexpr e)
-  | C.Pload (ws, x, e)  -> Pload(ws, vari_of_cvari x, expr_of_cexpr e)
+  | C.Pload (al, ws, x, e)  -> Pload(al, ws, vari_of_cvari x, expr_of_cexpr e)
   | C.Papp1 (o, e)      -> Papp1(o, expr_of_cexpr e)
   | C.Papp2 (o, e1, e2) -> Papp2(o, expr_of_cexpr e1, expr_of_cexpr e2)
   | C.PappN (o, es) -> PappN (o, List.map (expr_of_cexpr) es)
@@ -112,16 +112,16 @@ let rec expr_of_cexpr = function
 let clval_of_lval = function
   | Lnone(loc, ty)  -> C.Lnone (loc, cty_of_ty ty)
   | Lvar x          -> C.Lvar  (cvari_of_vari x)
-  | Lmem (ws, x, e) -> C.Lmem (ws, cvari_of_vari x, cexpr_of_expr e)
-  | Laset(aa,ws,x,e)-> C.Laset (aa, ws, cvari_of_vari x, cexpr_of_expr e)
+  | Lmem (al, ws, x, e) -> C.Lmem (al, ws, cvari_of_vari x, cexpr_of_expr e)
+  | Laset(al, aa,ws,x,e)-> C.Laset (al, aa, ws, cvari_of_vari x, cexpr_of_expr e)
   | Lasub(aa,ws,len,x,e)-> 
     C.Lasub (aa, ws, pos_of_int len, cvari_of_vari x, cexpr_of_expr e)
 
 let lval_of_clval = function
   | C.Lnone(p, ty)  -> Lnone (p, ty_of_cty ty)
   | C.Lvar x        -> Lvar (vari_of_cvari x)
-  | C.Lmem(ws,x,e)  -> Lmem (ws, vari_of_cvari x, expr_of_cexpr e)
-  | C.Laset(aa,ws,x,e) -> Laset (aa,ws, vari_of_cvari x, expr_of_cexpr e)
+  | C.Lmem(al,ws,x,e)  -> Lmem (al, ws, vari_of_cvari x, expr_of_cexpr e)
+  | C.Laset(al, aa,ws,x,e) -> Laset (al, aa,ws, vari_of_cvari x, expr_of_cexpr e)
   | C.Lasub(aa,ws,len,x,e) -> 
     Lasub (aa,ws, int_of_pos len, vari_of_cvari x, expr_of_cexpr e)
 
@@ -282,7 +282,7 @@ let prog_of_csprog p =
 let to_array ty p t = 
   let ws, n = array_kind ty in
   let get i = 
-    match Warray_.WArray.get p Warray_.AAscale ws t (cz_of_int i) with
+    match Warray_.WArray.get p Aligned Warray_.AAscale ws t (cz_of_int i) with
     | Utils0.Ok w -> z_of_word ws w
     | _    -> assert false in
   ws, Array.init n get

compiler/src/ct_checker_forward.ml

@@ -380,12 +380,12 @@ let rec ty_expr ~(public:bool) env (e:expr) =
 
   | Pvar x -> Env.gget ~public env x
 
-  | Pget (_, _, x, i) | Psub (_, _, _, x, i) ->
+  | Pget (_, _, _, x, i) | Psub (_, _, _, x, i) ->
     let env, ty = Env.gget ~public env x in
     let env, _  = ty_expr ~public:true env i in
     env, ty
 
-  | Pload (_, x, i) ->
+  | Pload (_, _, x, i) ->
     let env, _ = Env.get ~public:true env x in
     let env, _ = ty_expr ~public:true env i in
     env, Secret
@@ -413,11 +413,11 @@ let ty_lval env x lvl =
   match x with
   | Lnone _ -> env
   | Lvar x -> Env.set env x lvl
-  | Lmem(_, x, i) ->
+  | Lmem(_, _, x, i) ->
     let env, _ = Env.get ~public:true env x in
     let env, _ = ty_expr ~public:true env i in
     env
-  | Laset(_, _, x, i) | Lasub(_, _, _, x, i) ->
+  | Laset(_, _, _, x, i) | Lasub(_, _, _, x, i) ->
     (* x[i] = e is x = x[i <- e] *)
     let env, xlvl = Env.get ~public:false env x in
     let env, _    = ty_expr ~public:true env i in

compiler/src/evaluator.ml

@@ -206,10 +206,10 @@ let pp_val fmt v =
     Format.fprintf fmt "@[[";
     for i = 0 to ip-2 do
       let i = Conv.cz_of_int i in
-      Format.fprintf fmt "%a;@ " pp_res (WArray.get p AAscale U8 t i);
+      Format.fprintf fmt "%a;@ " pp_res (WArray.get p Aligned AAscale U8 t i);
     done;
     if 0 < ip then 
-      pp_res fmt (WArray.get p AAscale U8 t (Conv.cz_of_int (ip-1)));
+      pp_res fmt (WArray.get p Aligned AAscale U8 t (Conv.cz_of_int (ip-1)));
     Format.fprintf fmt "]@]";
   | Vword(ws, w) -> pp_word fmt ws w
   | Vundef ty -> pp_undef fmt ty

compiler/src/latex_printer.ml

@@ -119,6 +119,11 @@ let pp_attribute_key fmt s =
   then F.fprintf fmt "%s" s
   else F.fprintf fmt "%S" s
 
+let pp_aligned fmt = function
+  | None -> ()
+  | 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 
   | Aint i -> Z.pp_print fmt i
@@ -146,9 +151,9 @@ let rec pp_expr_rec prio fmt pe =
   match L.unloc pe with
   | PEParens e -> pp_expr_rec prio fmt e
   | PEVar x -> pp_var fmt x
-  | PEGet (aa, ws, x, e, len) -> 
-    pp_arr_access fmt aa ws x e len
-  | PEFetch me -> pp_mem_access fmt me 
+  | PEGet (al, aa, ws, x, e, len) ->
+    pp_arr_access fmt al aa ws x e len
+  | PEFetch me -> pp_mem_access fmt me
   | PEpack (vs,es) ->
     F.fprintf fmt "(%a)[@[%a@]]" pp_svsize vs (pp_list ",@ " pp_expr) es
   | PEBool b -> F.fprintf fmt "%s" (if b then "true" else "false")
@@ -173,13 +178,13 @@ 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) = 
+and pp_mem_access fmt (ty,x,e, al) =
   let pp_e fmt e = 
     match e with
     | 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]" (pp_opt (pp_paren pp_ws)) ty pp_var x pp_e e
+  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
@@ -191,14 +196,15 @@ and pp_type fmt ty =
 and pp_ws fmt w = F.fprintf fmt "%a" ptype (string_of_wsize w)
 and pp_expr fmt e = pp_expr_rec Pmin fmt e
 
-and pp_arr_access fmt aa ws x e len= 
+and pp_arr_access fmt al aa ws x e len=
  let pp_olen fmt len = 
    match len with
    | None -> ()
    | Some len -> Format.fprintf fmt " : %a" pp_expr len in
- F.fprintf fmt "%a%s[%a%a%a%a]" 
-    pp_var x 
+ F.fprintf fmt "%a%s[%a%a%a%a%a]"
+    pp_var x
     (if aa = Warray_.AAdirect then "." else "")
+    pp_aligned al
     (pp_opt pp_ws) ws (pp_opt pp_space) ws pp_expr e pp_olen len
 
 let pp_writable = function
@@ -248,7 +254,7 @@ let pp_lv fmt x =
   match L.unloc x with
   | PLIgnore -> F.fprintf fmt "_"
   | PLVar x -> pp_var fmt x
-  | PLArray (aa, ws, x, e, len) -> pp_arr_access fmt aa ws x e len
+  | PLArray (al, aa, ws, x, e, len) -> pp_arr_access fmt al aa ws x e len
   | PLMem me -> pp_mem_access fmt me 
 
 let pp_eqop fmt op =

compiler/src/lexer.mll

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