Support far global variable accesses in ARM

CHANGELOG.md

@@ -22,6 +22,13 @@
 - Add support for the MMX instruction `POR`
   ([PR #917](https://github.com/jasmin-lang/jasmin/pull/917)).
 
+- The compiler now introduces labels for each byte of the data section
+  ([PR#921](https://github.com/jasmin-lang/jasmin/pull/921)).
+
+- ARM now emits two instructions instead of `ADR` to load the low and high
+  parts of global addresses
+  ([PR#921](https://github.com/jasmin-lang/jasmin/pull/921)).
+
 ## Bug fixes
 
 - Easycrypt extraction for CT : fix decreasing for loops

compiler/src/pp_arm_m4.ml

@@ -42,8 +42,8 @@ let pp_reg_address_aux base disp off scal =
 
 let global_datas = "glob_data"
 
-let pp_rip_address (p : Ssralg.GRing.ComRing.sort) : string =
-  Format.asprintf "%s+%a" global_datas Z.pp_print (Conv.z_of_int32 p)
+let pp_rip_address (p : Ssralg.GRing.ComRing.sort) =
+  byte_label global_datas (Conv.z_of_int32 p)
 
 (* -------------------------------------------------------------------- *)
 (* TODO_ARM: This is architecture-independent. *)
@@ -223,6 +223,26 @@ end = struct
     | _ -> ""
 end
 
+(* We assume that [ADR] instructions are only generated for accessing the data
+   section (i.e., global variables). *)
+let pp_ADR pp opts args =
+  let name_lo = pp_mnemonic_ext (ARM_op(MOV, opts)) "w" args in
+  let name_hi = pp_mnemonic_ext (ARM_op(MOVT, opts)) "" args in
+  let args =
+    List.filter_map (fun (_, a) -> pp_asm_arg a) pp.pp_aop_args
+  in
+  let args_lo =
+    match args with
+    | dst :: addr :: rest -> dst :: ("#:lower16:" ^ addr) :: rest
+    | _ -> assert false
+  in
+  let args_hi =
+    match args with
+    | dst :: addr :: rest -> dst :: ("#:upper16:" ^ addr) :: rest
+    | _ -> assert false
+  in
+  [ LInstr(name_lo, args_lo); LInstr(name_hi, args_hi) ]
+
 let pp_instr fn i =
   match i with
   | ALIGN ->
@@ -265,12 +285,18 @@ let pp_instr fn i =
   | AsmOp (op, args) ->
       let id = instr_desc arm_decl arm_op_decl (None, op) in
       let pp = id.id_pp_asm args in
+      (* We need to perform the check even if we don't use the suffix, for
+         instance for [LDR] or [STR]. *)
       let suff = ArgChecker.check_args op pp.pp_aop_args in
-      let name = pp_mnemonic_ext op suff args in
-      let args = List.filter_map (fun (_, a) -> pp_asm_arg a) pp.pp_aop_args in
-      let args = pp_shift op args in
-      get_IT i @ [ LInstr (name, args) ]
-
+      match op with
+      | ARM_op(ADR, opts) -> pp_ADR pp opts args
+      | _ ->
+          let name = pp_mnemonic_ext op suff args in
+          let args =
+            List.filter_map (fun (_, a) -> pp_asm_arg a) pp.pp_aop_args
+          in
+          let args = pp_shift op args in
+          get_IT i @ [ LInstr (name, args) ]
 
 (* -------------------------------------------------------------------- *)
 
@@ -314,7 +340,7 @@ let pp_data globs names =
   if not (List.is_empty globs) then
     LInstr (".p2align", ["5"]) ::
     LLabel global_datas ::
-    format_glob_data globs names
+    format_glob_data global_datas globs names
   else []
 
 let pp_prog p =

compiler/src/ppasm.ml

@@ -201,7 +201,7 @@ let pp_glob_data fmt gd names =
             `Instr (".p2align", [pp_align U256]);
             `Label m;
             `Label n]);
-      format_glob_data gd names |> print_asm_lines fmt
+      format_glob_data global_datas gd names |> print_asm_lines fmt
     end
 
 let pp_instr_wsize (ws : W.wsize) =

compiler/src/printASM.ml

@@ -32,19 +32,31 @@ let string_of_glob occurrences x =
   let suffix = if count > 0 then Format.asprintf "$%d" count else "" in
   Format.asprintf "G$%s%s" (escape x.v_name) suffix
 
+let byte_label global_datas i =
+  Format.asprintf "%s_%a" global_datas Z.pp_print i
 
 (* -------------------------------------------------------------------- *)
-let format_glob_data globs names =
+let format_glob_data_entry global_datas i olabel b =
+  let lbl =
+    match olabel with
+    | Some x -> [ LLabel x ]
+    | None -> []
+  in
+  lbl @ [ LLabel(byte_label global_datas (Z.of_int i)); LByte(b) ]
+
+let format_glob_data global_datas globs names =
   (* Creating a Hashtable to count occurrences of a label name*)
   let occurrences = Hash.create 42 in
   let names =
     List.map (fun ((x, _), p) -> (Conv.var_of_cvar x, Conv.z_of_cz p)) names
   in
-  List.flatten
-    (List.mapi
-       (fun i b ->
-         let b = LByte (Z.to_string (Conv.z_of_int8 b)) in
-         match List.find (fun (_, p) -> Z.equal (Z.of_int i) p) names with
-         | exception Not_found -> [ b ]
-         | x, _ -> [ LLabel (string_of_glob occurrences x); b ])
-       globs)
+  let doit i b =
+    let olabel =
+      match List.find (fun (_, p) -> Z.equal p (Z.of_int i)) names with
+      | x, _ -> Some (string_of_glob occurrences x)
+      | exception Not_found -> None
+    in
+    let b = Conv.z_of_int8 b |> Z.to_string in
+    format_glob_data_entry global_datas i olabel b
+  in
+  List.flatten (List.mapi doit globs)

compiler/src/printASM.mli

@@ -5,7 +5,12 @@ type asm_line =
 
 val print_asm_lines : Format.formatter -> asm_line list -> unit
 
+val byte_label : string -> Z.t -> string
+
 val format_glob_data :
-  Obj.t list -> ((Var0.Var.var * 'a) * BinNums.coq_Z) list -> asm_line list
+  string ->
+  Obj.t list ->
+  ((Var0.Var.var * 'a) * BinNums.coq_Z) list ->
+  asm_line list
 
 val string_of_label : string -> Label.label -> string

compiler/tests/success/arm-m4/far_global_access.jazz

@@ -0,0 +1,21 @@
+param int L = 2042;
+
+u32[2] a = { 1, 2 };
+
+export
+fn main() -> reg u32 {
+    reg ptr u32[2] p = a;
+    reg u32 t = p[0];
+    reg u32 tmp = p[1];
+    t += tmp;
+
+    reg ptr u32[1] q = a[1:1];
+    reg u32 tmp = q[0];
+    t += tmp;
+
+    reg u32 v = 0;
+    inline int i;
+    for i = 0 to L { v += t; }
+
+    return v;
+}

proofs/compiler/arm_params.v

@@ -37,6 +37,8 @@ Context {atoI : arch_toIdent}.
 Definition is_load e :=
   if e is Pload _ _ _ _ then true else false.
 
+(* It is important that we generate the [ADR] instruction *only* for accesses to
+   the data section, since the symbols get split to perform far accesses. *)
 Definition arm_mov_ofs
   (x : lval) (tag : assgn_tag) (vpk : vptr_kind) (y : pexpr) (ofs : Z) :
   option instr_r :=