Unaligned accesses & sub-arrays

Co-authored-by: Benjamin Grēgoire <[email protected]>

compiler/src/stackAlloc.ml

@@ -121,7 +121,7 @@ let memory_analysis pp_err ~debug up =
       Stack_alloc.({
         pp_ptr = Conv.cvar_of_var pi.pi_ptr;
         pp_writable = pi.pi_writable;
-        pp_align    = pi.pi_align;
+        pp_align    = pi.pi_align.ac_strict;
       }) in
     let conv_sub (i:Interval.t) = 
       Stack_alloc.{ z_ofs = Conv.cz_of_int i.min; 

compiler/src/varalloc.ml

@@ -1,5 +1,6 @@
 open Utils
 open Wsize
+open Memory_model
 open Prog
 
 module Live = Liveness
@@ -10,10 +11,17 @@ let hierror = hierror ~kind:"compilation error" ~sub_kind:"variable allocation"
 type liverange = G.graph Mint.t
 
 (* --------------------------------------------------- *)
-type param_info = { 
+(** Invariant: heuristic is always higher than the strict constraint *)
+type alignment_constraint =
+  { ac_strict: wsize
+  ; ac_heuristic: wsize }
+
+let no_alignment_constraint = { ac_strict = U8; ac_heuristic = U8 }
+
+type param_info = {
   pi_ptr      : var;
   pi_writable : bool;
-  pi_align    : wsize;
+  pi_align    : alignment_constraint;
 }
 
 type ptr_kind = 
@@ -117,33 +125,38 @@ let check_class f_name f_loc ptr_classes args x s =
     hierror ~loc:(Lone f_loc) ~funname:f_name "cannot put a reg ptr argument into the local stack"
 
 (* --------------------------------------------------- *)
+let max_align al ws ac =
+  let max_align ws' = if wsize_lt ws' ws then ws else ws' in
+  match al with
+  | Aligned -> { ac_strict = max_align ac.ac_strict; ac_heuristic = max_align ac.ac_heuristic }
+  | Unaligned -> { ac with ac_heuristic = max_align ac.ac_heuristic }
 
-type alignment = wsize Hv.t
+type alignment = alignment_constraint Hv.t
 
-let classes_alignment (onfun : funname -> param_info option list) (gtbl: alignment) alias c =
+let classes_alignment (onfun : funname -> param_info option list) (gtbl: alignment) alias c : alignment * Sf.t =
   let ltbl = Hv.create 117 in
   let calls = ref Sf.empty in
 
-  let set x scope ws = 
+  let set al x scope ws =
     let tbl = if scope = E.Sglob then gtbl else ltbl in
-    Hv.modify_def U8 x (fun ws' -> if wsize_lt ws' ws then ws else ws') tbl in
+    Hv.modify_def no_alignment_constraint x (max_align al ws) tbl in
 
-  let add_ggvar x ws i =
+  let add_ggvar al x ws i =
     let x' = L.unloc x.gv in
     if is_gkvar x then
       begin
         let c = Alias.normalize_var alias x' in
-        set c.in_var c.scope ws;
-        if (fst c.range + i) land (size_of_ws ws - 1) <> 0 then
+        set al c.in_var c.scope ws;
+        if al == Aligned && (fst c.range + i) land (size_of_ws ws - 1) <> 0 then
             hierror ~loc:(Lone (L.loc x.gv)) "bad range alignment for %a[%d]/%s in %a"
               (Printer.pp_var ~debug:true) x' i (string_of_ws ws)
               Alias.pp_slice c
       end
-    else set x' E.Sglob ws in
+    else set al x' E.Sglob ws in
 
   let rec add_e = function
     | Pconst _ | Pbool _ | Parr_init _  | Pvar _ -> ()
-    | Pget (_, _, ws, x, e) -> add_ggvar x ws 0; add_e e
+    | Pget (al, _, ws, x, e) -> add_ggvar al x ws 0; add_e e
     | Psub (_,_,_,_,e) | Pload (_, _, _, e) | Papp1 (_, e) -> add_e e
     | Papp2 (_, e1,e2) -> add_e e1; add_e e2
     | PappN (_, es) -> add_es es 
@@ -153,22 +166,25 @@ let classes_alignment (onfun : funname -> param_info option list) (gtbl: alignme
   let add_lv = function
     | Lnone _ | Lvar _ -> ()
     | Lmem (_, _, _, e) | Lasub (_,_,_,_,e) -> add_e e
-    | Laset(_, _, ws,x,e) -> add_ggvar (gkvar x) ws 0; add_e e in
+    | Laset(al, _, ws,x,e) -> add_ggvar al (gkvar x) ws 0; add_e e in
 
   let add_lvs = List.iter add_lv in
 
   let add_p opi e = 
     match opi, e with
     | None, _ -> add_e e
-    | Some pi, Pvar x ->  add_ggvar x pi.pi_align 0
+    | Some pi, Pvar x ->
+       add_ggvar Aligned x pi.pi_align.ac_strict 0;
+       add_ggvar Unaligned x pi.pi_align.ac_heuristic 0
     | Some pi, Psub(aa,ws,_, x, e) ->
       let i = 
         match get_ofs aa ws e with
         | None ->
           (* this error is probably always caught before by the similar code in alias.ml *)
           hierror ~loc:(Lone (L.loc x.gv)) "Cannot compile sub-array %a that has a non-constant start index" (Printer.pp_var ~debug:true) (L.unloc x.gv)
         | Some i -> i in
-      add_ggvar x pi.pi_align i
+      add_ggvar Aligned x pi.pi_align.ac_strict i;
+      add_ggvar Unaligned x pi.pi_align.ac_heuristic i
     | _, _ -> assert false in
 
   let rec add_ir i_desc =
@@ -246,9 +262,11 @@ let init_slots pd stack_pointers alias coloring fv =
   !slots, lalloc
 
 (* --------------------------------------------------- *)
-let all_alignment pd ctbl alias ret params lalloc =
+let all_alignment pd (ctbl: alignment) alias ret params lalloc : param_info option list * wsize Hv.t =
 
-  let get_align c = try Hv.find ctbl c.Alias.in_var with Not_found -> U8 in
+  let get_align c =
+    try Hv.find ctbl c.Alias.in_var
+    with Not_found -> no_alignment_constraint in
   let doparam i x =
     match x.v_kind with
     | Reg (_, Direct) -> None
@@ -260,8 +278,8 @@ let all_alignment pd ctbl alias ret params lalloc =
         | RegPtr p -> p
         | _ | exception Not_found -> assert false in
       let pi_writable = List.mem (Some i) ret in
-      let pi_align = get_align c in 
-      Some { pi_ptr; pi_writable; pi_align } 
+      let pi_align = get_align c in
+      Some { pi_ptr; pi_writable; pi_align }
     | _ -> assert false in
   let params = List.mapi doparam params in
 
@@ -274,7 +292,7 @@ let all_alignment pd ctbl alias ret params lalloc =
     | Direct (slot, _, E.Slocal) ->
       let ws = 
         match x.v_ty with
-        | Arr _ -> get_align (Alias.normalize_var alias x)
+        | Arr _ -> (get_align (Alias.normalize_var alias x)).ac_heuristic
         | Bty (U ws) -> ws
         | _ -> assert false in
       set slot ws
@@ -293,7 +311,7 @@ let round_ws ws sz =
 let alloc_local_stack size slots atbl =
   let do1 x = 
     let ws = 
-      try Hv.find atbl x 
+      try Hv.find atbl x
       with Not_found -> 
         match x.v_ty with
         | Arr _ -> U8
@@ -423,7 +441,7 @@ let alloc_stack_fd callstyle pd get_info gtbl fd =
   } in
   sao
 
-let alloc_mem gtbl globs =
+let alloc_mem (gtbl: wsize Hv.t) globs =
   let gao_align, gao_slots, gao_size = alloc_local_stack 0 (List.map fst globs) gtbl in
   let t = Array.make gao_size (Word0.wrepr U8 (Conv.cz_of_int 0)) in
   let get x = 
@@ -457,7 +475,7 @@ let alloc_stack_prog callstyle pd (globs, fds) =
     let sao = alloc_stack_fd callstyle pd get_info gtbl fd in
     set_info fd.f_name sao in
   List.iter doit (List.rev fds);
-  let gao =  alloc_mem gtbl globs in
+  let gao =  alloc_mem (Hv.map (fun _ x -> x.ac_heuristic) gtbl) globs in
   gao, ftbl 
 
 let extend_sao sao extra =

compiler/src/varalloc.mli

@@ -1,11 +1,15 @@
 open Wsize
 open Prog
 
-type param_info = { 
-  pi_ptr      : var;
-  pi_writable : bool;
-  pi_align    : wsize;
-}
+type alignment_constraint =
+  { ac_strict: wsize
+  ; ac_heuristic: wsize }
+
+type param_info = {
+    pi_ptr      : var;
+    pi_writable : bool;
+    pi_align    : alignment_constraint;
+  }
 
 type ptr_kind = 
   | Direct   of var * Interval.interval * Expr.v_scope

compiler/tests/success/common/unaligned_subarray.jazz

@@ -0,0 +1,55 @@
+export
+fn main() -> reg u32 {
+  stack u32[2] s;
+  reg ptr u32[1] p;
+  reg u32 z;
+  z = 0;
+
+  s[0] = z;
+  s[1] = z;
+
+  p = s[u8 1:4];
+
+  reg u32 r;
+  r = p[#unaligned 0];
+
+  return r;
+}
+
+fn load(reg ptr u32[1] a) -> reg u32 {
+  reg u32 v;
+  v = a[#unaligned 0];
+  return v;
+}
+
+export
+fn deref_unaligned() -> reg u32 {
+  stack u32[2] s; // s mod u32 = -1
+  reg u32 z;
+  z = 0;
+  inline int i;
+  for i = 0 to 8 {
+    s[u8 i] = z;
+  }
+
+  reg u32 r;
+  r = load(s.[1:1]);
+
+  return r;
+}
+
+export
+fn deref_aligned() -> reg u32 {
+  stack u32[1] s;
+  reg u32 z;
+  z = 0;
+  inline int i;
+  for i = 0 to 4 {
+    s[u8 i] = z;
+  }
+
+  reg u32 r;
+  r = load(s.[0:1]);
+
+  return r;
+}

proofs/compiler/stack_alloc.v

@@ -176,10 +176,10 @@ Record pos_map := {
 
 (* TODO: Z.land or is_align ?
    Could be just is_align (sub_region_addr sr) ws ? *)
-Definition check_align x (sr:sub_region) ws :=
-  Let _ := assert (ws <= sr.(sr_region).(r_align))%CMP
+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? *)
                   (stk_ierror_basic x "unaligned offset") in
-  assert (Z.land sr.(sr_zone).(z_ofs) (wsize_size ws - 1) == 0)%Z
+  assert ((al == Unaligned) || (Z.land sr.(sr_zone).(z_ofs) (wsize_size ws - 1) == 0)%Z)
          (stk_ierror_basic x "unaligned sub offset").
 
 Definition writable (x:var_i) (r:region) :=
@@ -313,7 +313,7 @@ End WITH_POINTER_DATA.
 
 (* Precondition size_of x = ws && length sr.sr_zone = wsize_size ws *)
 Definition set_word rmap (x:var_i) sr ws :=
-  Let _ := check_align x sr ws in
+  Let _ := check_align Aligned x sr ws in
   set_sub_region rmap x sr (Some 0)%Z (size_slot x).
 
 (* If we write to array [x] at offset [ofs], we invalidate the corresponding
@@ -324,9 +324,9 @@ Definition set_word rmap (x:var_i) sr ws :=
    approximation.
 *)
 (* [set_word], [set_stack_ptr] and [set_arr_word] could be factorized? -> think more about it *)
-Definition set_arr_word (rmap:region_map) (x:var_i) ofs ws :=
+Definition set_arr_word (rmap:region_map) al (x:var_i) ofs ws :=
   Let sr := get_sub_region rmap x in
-  Let _ := check_align x sr ws in
+  Let _ := check_align al x sr ws in
   set_sub_region rmap x sr ofs (wsize_size ws).
 
 Definition set_arr_call rmap x sr := set_sub_region rmap x sr (Some 0)%Z (size_slot x).
@@ -584,9 +584,9 @@ Definition check_vpk rmap (x:var_i) vpk ofs len :=
     ok sr'.
 *)
 
-Definition check_vpk_word rmap x vpk ofs ws :=
+Definition check_vpk_word rmap al x vpk ofs ws :=
   Let srs := check_vpk rmap x vpk ofs (wsize_size ws) in
-  check_align x srs.1 ws.
+  check_align al x srs.1 ws.
 
 Fixpoint alloc_e (e:pexpr) :=
   match e with
@@ -598,7 +598,7 @@ Fixpoint alloc_e (e:pexpr) :=
     | None => Let _ := check_diff xv in ok e
     | Some vpk =>
       if is_word_type (vtype xv) is Some ws then
-        Let _ := check_vpk_word rmap xv vpk (Some 0%Z) ws in
+        Let _ := check_vpk_word rmap Aligned xv vpk (Some 0%Z) ws in
         Let pofs := mk_addr xv AAdirect ws vpk (Pconst 0) in
         ok (Pload Aligned ws pofs.1 pofs.2)
       else Error (stk_ierror_basic xv "not a word variable in expression")
@@ -612,7 +612,7 @@ Fixpoint alloc_e (e:pexpr) :=
     | None => Let _ := check_diff xv in ok (Pget al aa ws x e1)
     | Some vpk =>
       let ofs := mk_ofsi aa ws e1 in
-      Let _ := check_vpk_word rmap xv vpk ofs ws in
+      Let _ := check_vpk_word rmap al xv vpk ofs ws in
       Let pofs := mk_addr xv aa ws vpk e1 in
       ok (Pload al ws pofs.1 pofs.2)
     end
@@ -690,7 +690,7 @@ Definition alloc_lval (rmap: region_map) (r:lval) (ty:stype) :=
     | None => Let _ := check_diff x in ok (rmap, Laset al aa ws x e1)
     | Some pk =>
       let ofs := mk_ofsi aa ws e1 in
-      Let rmap := set_arr_word rmap x ofs ws in
+      Let rmap := set_arr_word rmap al x ofs ws in
       Let pofs := mk_addr_ptr x aa ws pk e1 in
       let r := Lmem al ws pofs.1 pofs.2 in
       ok (rmap, r)
@@ -1048,7 +1048,7 @@ Definition alloc_call_arg_aux rmap0 rmap (sao_param: option param_info) (e:pexpr
     Let srs := Region.check_valid rmap0 xv (Some 0%Z) (size_slot xv) in
     let sr := srs.1 in
     Let rmap := if pi.(pp_writable) then set_clear rmap xv sr (Some 0%Z) (size_slot xv) else ok rmap in
-    Let _  := check_align xv sr pi.(pp_align) in
+    Let _  := check_align Aligned xv sr pi.(pp_align) in
     ok (rmap, (Some (pi.(pp_writable),sr), Pvar (mk_lvar (with_var xv p))))
   | Some _, _ => Error (stk_ierror_basic xv "the argument should be a reg ptr")
   end.