Memory accesses & direct array accesses make no assumptions on alignment

jasmin-lang · Mar 13, 2024 · aedf820 · aedf820
1 parent 48fa75b
commit aedf820
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 10 deletions.
diff --git a/compiler/safety/fail/bad_align.jazz b/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;
 }
diff --git a/compiler/src/pretyping.ml b/compiler/src/pretyping.ml
@@ -951,9 +951,12 @@ let ensure_int loc i ty =
   | _ -> rs_tyerror ~loc (TypeMismatch (ty, P.tint))
 
 (* -------------------------------------------------------------------- *)
-let tt_al = function
-  | Some `Unaligned -> Memory_model.Unaligned
-  | Some `Aligned | None -> Memory_model.Aligned
+let tt_al aa =
+  let open Memory_model in
+  function
+  | None -> (match aa with Warray_.AAdirect -> Unaligned | AAscale -> Aligned)
+  | Some `Unaligned -> Unaligned
+  | Some `Aligned -> Aligned
 
 (* -------------------------------------------------------------------- *)
 let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
@@ -978,7 +981,7 @@ 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 al 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
@@ -1084,7 +1087,7 @@ and tt_mem_access pd ?(mode=`AllVar) (env : 'asm Env.env)
       | `Add -> e
       | `Sub -> Papp1(E.Oneg (E.Op_w pd), e) in
   let ct = ct |> Option.map_default tt_ws pd in
-  let al = tt_al al in
+  let al = tt_al AAdirect al in
   (ct,L.mk_loc xlc x,e, al)
 
 (* -------------------------------------------------------------------- *)
@@ -1156,7 +1159,7 @@ let tt_lvalue pd (env : 'asm Env.env) { L.pl_desc = pl; L.pl_loc = loc; } =
   | S.PLArray (al, aa, ws, ({ pl_loc = xlc } as x), pi, olen) ->
     let x  = tt_var `NoParam env x in
     reject_constant_pointers xlc x ;
-    let al = tt_al al in
+    let al = tt_al aa al in
     let ty,_ = tt_as_array (xlc, x.P.v_ty) in
     let ws = Option.map_default tt_ws (P.ws_of_ty ty) ws in
     let ty = P.tu ws in

diff --git a/compiler/src/printCommon.ml b/compiler/src/printCommon.ml
@@ -16,7 +16,8 @@ let pp_wsize fmt sz = fprintf fmt "%a" pp_string0 (string_of_wsize sz)
 
 let pp_aligned fmt =
   function
-  | Memory_model.Aligned -> ()
+  | Memory_model.Aligned ->
+     Format.fprintf fmt "#aligned "
   | Unaligned ->
      Format.fprintf fmt "#unaligned "
 

diff --git a/compiler/tests/success/x86-64/vector.jazz b/compiler/tests/success/x86-64/vector.jazz
@@ -10,8 +10,8 @@ export
 fn test_vmovdqa(reg u64 p) {
 reg u128 r;
 
-r = #VMOVDQA_128((u128)[p + 16 * 0]);
-(u128)[p + 16 * 1] = #VMOVDQA_128(r);
+r = #VMOVDQA_128((u128)[#aligned p + 16 * 0]);
+(u128)[#aligned p + 16 * 1] = #VMOVDQA_128(r);
 }
 
 export