Split large memory accesses in stack alloc

CHANGELOG.md

@@ -70,6 +70,11 @@
   ([PR #955](https://github.com/jasmin-lang/jasmin/pull/955);
   fixes [#950](https://github.com/jasmin-lang/jasmin/issues/950)).
 
+- The compiler now introduces several instructions for memory operations whose
+  offsets are too large for the ARM encoding
+  ([PR #741](https://github.com/jasmin-lang/jasmin/pull/741)). It issues a
+  warning in these cases.
+
 # Jasmin 2024.07.1 — Nancy, 2024-10-03
 
 ## New features

compiler/config/tests.config

@@ -54,18 +54,18 @@ exclude = tests/success/noextract
 
 [test-arm-m4]
 bin = ./scripts/check-arm-m4
-okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common
+okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common tests/success/arm-m4/large_memory_immediates
 kodirs = tests/fail/**/arm-m4 tests/fail/**/common
 
 [test-arm-m4-print]
 bin = ./scripts/parse-print-parse
 args = arm
-okdirs = tests/success/**/arm-m4 tests/success/**/common
+okdirs = tests/success/**/arm-m4 tests/success/**/common tests/success/arm-m4/large_memory_immediates
 
 [test-arm-m4-extraction]
 bin = ./scripts/extract-and-check
 args = arm
-okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common
+okdirs = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/**/common tests/success/arm-m4/large_memory_immediates
 exclude = tests/success/noextract
 
 [test-x86-64-stack-zero-loop]
@@ -85,12 +85,12 @@ exclude = tests/fail/warning
 [test-arm-m4-stack-zero-loop]
 bin     = ./scripts/check-arm-m4
 args    = -stack-zero=loop
-okdirs  = examples/**/arm-m4 tests/success/**/arm-m4
+okdirs  = examples/**/arm-m4 tests/success/**/arm-m4 tests/success/arm-m4/large_memory_immediates
 kodirs  = tests/fail/**/arm-m4
 
 [test-arm-m4-stack-zero-unrolled]
 bin     = ./scripts/check-arm-m4
 args    = -stack-zero=unrolled
 okdirs  = examples/**/arm-m4 tests/success/**/arm-m4
 kodirs  = tests/fail/**/arm-m4
-exclude = tests/success/arm-m4/large_stack
+exclude = tests/success/arm-m4/large_stack tests/success/arm-m4/large_memory_immediates

compiler/src/arm_arch_full.ml

@@ -99,6 +99,8 @@ module Arm_core = struct
     | Oarm_swap _ -> true
     | Oarm_add_large_imm -> true
     | (Osmart_li _ | Osmart_li_cc _) -> true (* emit MOVT *)
+    | Olarge_load _ | Olarge_load_cc _ | Olarge_store _ | Olarge_store_cc _ ->
+        true (* emit MOV, MOVT, STR *)
 
 end
 

compiler/src/compile.ml

@@ -183,10 +183,25 @@ let compile (type reg regx xreg rflag cond asm_op extra_op)
     (fn, f) |> Conv.fdef_of_cufdef |> refresh_i_loc_f |> Conv.cufdef_of_fdef |> snd
   in
 
-  let warning ii msg =
-    (if not !Glob_options.lea then
-     let loc, _ = ii in
-     warning UseLea loc "%a" Printer.pp_warning_msg msg);
+  let warning ii w =
+    let o =
+      match w with
+      | Compiler_util.Use_lea ->
+          if not !Glob_options.lea
+          then Some (UseLea, "LEA instruction is used")
+          else None
+      | Split_memory_access ->
+          if not !Glob_options.split_memory_access
+          then
+            let msg =
+              "This memory immediate does not fit in one instruction, several \
+               instructions were issued."
+            in
+            Some (SplitMemoryAccess, msg)
+          else None
+    in
+    let loc, _ = ii in
+    Option.may (fun (w, msg) -> warning w loc "%s" msg) o;
     ii
   in
 

compiler/src/glob_options.ml

@@ -25,6 +25,7 @@ type color = | Auto | Always | Never
 let color = ref Auto
 
 let lea = ref false
+let split_memory_access = ref false
 let set0 = ref false
 let model = ref Normal
 let print_stack_alloc = ref false
@@ -172,6 +173,9 @@ let options = [
     "-I"       , Arg.String set_idirs  , "[ident:path] Bind ident to path for from ident require ...";
     "-lea"     , Arg.Set lea           , " Use lea as much as possible (default is nolea)";
     "-nolea"   , Arg.Clear lea         , " Try to use add and mul instead of lea";
+    "-split-memory-access"
+      , Arg.Set split_memory_access
+      , " Split large memory accesses in several instructions";
     "-set0"     , Arg.Set set0          , " Use [xor x x] to set x to 0 (default is not)";
     "-noset0"   , Arg.Clear set0        , " Do not use set0 option";
     "-ec"       , Arg.String  set_ec    , "[f] Extract function [f] and its dependencies to an easycrypt file (deprecated)";

compiler/src/pp_arm_m4.ml

@@ -213,6 +213,13 @@ end = struct
   let chk_imm_w16_encoding args n opts =
     chk_imm args n (chk_w16_encoding opts) (chk_w16_encoding opts)
 
+  let chk_mem_immediate args n =
+    match List.at args n with
+    | _, Addr(Areg(addr)) ->
+        let n = Word0.wsigned Wsize.U32 addr.ad_disp in
+        if not (is_mem_immediate n) then exn_imm_too_big n
+    | _, _ -> ()
+
   let check_args (ARM_op (mn, opts)) args =
     match mn with
     | ADC | SBC | RSB -> chk_imm_accept_shift args 2
@@ -221,6 +228,8 @@ end = struct
     | MOV -> chk_imm_w16_encoding args 1 opts
     | AND | BIC | EOR | ORR -> chk_imm_reject_shift args 2
     | MVN | TST -> chk_imm_reject_shift args 1
+    | LDR | LDRB | LDRH -> chk_mem_immediate args 1; "" (* Should not happen. *)
+    | STR | STRB | STRH -> chk_mem_immediate args 1; "" (* Should not happen. *)
     | _ -> ""
 end
 

compiler/src/printer.ml

@@ -409,9 +409,6 @@ let pp_sprog ~debug pd asmOp fmt ((funcs, p_extra):('info, 'asm) Prog.sprog) =
 
 (* ----------------------------------------------------------------------- *)
 
-let pp_warning_msg fmt = function
-  | Compiler_util.Use_lea -> Format.fprintf fmt "LEA instruction is used"
-
 let pp_err ~debug fmt (pp_e : Compiler_util.pp_error) =
   let pp_var fmt v =
     let v = Conv.var_of_cvar v in

compiler/src/printer.mli

@@ -1,6 +1,5 @@
 open Prog
 
-val pp_warning_msg :  Format.formatter -> Compiler_util.warning_msg -> unit
 val pp_err : debug:bool -> Format.formatter -> Compiler_util.pp_error -> unit
 
 val pp_print_X : Format.formatter -> Z.t -> unit

compiler/src/regalloc.ml

@@ -88,19 +88,23 @@ let find_equality_constraints (id: instruction_desc) : arg_position list list =
        | _ -> apl :: res)
     tbl []
 
-let find_var outs ins ap : _ option =
-  let oget = function
-    | Some x -> x
-    | None -> hierror_reg ~loc:Lnone ~internal:true "the instruction description is not correct" in
+let find_var outs ins ap =
+  let err () =
+    hierror_reg
+      ~loc:Lnone ~internal:true "the instruction description is not correct"
+  in
+  let get_lvar = function
+    | Lvar v | Lmem(_, _, v, _) -> Some v
+    | _ -> None
+  in
+  let get_evar = function
+  | Pvar v when is_gkvar v -> Some v.gv
+  | Pload(_, _, v, _) -> Some v
+  | _ -> None
+  in
   match ap with
-  | APout n ->
-     Oseq.onth outs n |> oget |>
-       (function Lvar v -> Some v | _ -> None)
-  | APin n ->
-     Oseq.onth ins n |> oget |>
-       (function
-        | Pvar v -> if is_gkvar v then Some v.gv else None
-        | _ -> None)
+  | APout n -> Oseq.onth outs n |> Option.default_delayed err |> get_lvar
+  | APin n -> Oseq.onth ins n |> Option.default_delayed err |> get_evar
 
 let asm_equality_constraints ~loc pd reg_size asmOp is_move_op (int_of_var: var_i -> int option) (k: int -> int -> unit)
     (k': int -> int -> unit)

compiler/src/stackAlloc.ml

@@ -190,6 +190,7 @@ let memory_analysis pp_err ~debug up =
         gao.gao_data
         cglobs
         get_sao
+        (fun ii _ -> ii)
         up
     with
     | Utils0.Ok sp -> sp 

compiler/src/utils.ml

@@ -420,6 +420,7 @@ type warning =
   | SimplifyVectorSuffix
   | DuplicateVar 
   | UnusedVar 
+  | SplitMemoryAccess
   | SCTchecker
   | Deprecated
   | Experimental

compiler/src/utils.mli

@@ -180,6 +180,7 @@ type warning =
   | SimplifyVectorSuffix
   | DuplicateVar 
   | UnusedVar 
+  | SplitMemoryAccess
   | SCTchecker
   | Deprecated
   | Experimental

compiler/tests/success/arm-m4/large_memory_immediates/basic.jazz

@@ -0,0 +1,21 @@
+export
+fn basic(reg u32 p) -> reg u32 {
+    [p + 4096] = p;
+    (u8)[p + 4096] = p;
+    (u16)[p + 4096] = p;
+    p = [p + 4096];
+    p = (32u)(u8)[p + 4096];
+    p = (32u)(u16)[p + 4096];
+
+    reg bool b;
+    b = p <= 3;
+    [p + 4096] = p if b;
+    (u8)[p + 4096] = p if b;
+    (u16)[p + 4096] = p if b;
+    p = [p + 4096] if b;
+    p = (32u)(u8)[p + 4096] if b;
+    p = (32u)(u16)[p + 4096] if b;
+
+    p = p;
+    return p;
+}

compiler/tests/success/arm-m4/large_memory_immediates/intrinsics.jazz

@@ -0,0 +1,21 @@
+export
+fn intrinsics(reg u32 p) -> reg u32 {
+    [p + 4096] = #STR(p);
+    (u8)[p + 4096] = #STRB(p);
+    (u16)[p + 4096] = #STRH(p);
+    p = #LDR([p + 4096]);
+    p = #LDRB((u8)[p + 4096]);
+    p = #LDRH((u16)[p + 4096]);
+
+    reg bool b;
+    b = p <= 3;
+    [p + 4096] = #STRcc(p, b, [p + 4096]);
+    (u8)[p + 4096] = #STRBcc(p, b, (u8)[p + 4096]);
+    (u16)[p + 4096] = #STRHcc(p, b, (u16)[p + 4096]);
+    p = #LDRcc([p + 4096], b, p);
+    p = #LDRBcc((u8)[p + 4096], b, p);
+    p = #LDRHcc((u16)[p + 4096], b, p);
+
+    p = p;
+    return p;
+}

compiler/tests/success/arm-m4/large_memory_immediates/large_internal_array.jazz

@@ -0,0 +1,23 @@
+// Stack allocation needs to split the array set and get operations into several
+// instructions to that the immediates fit in one instruction.
+
+// The LDR/STR instructions take an immediate of up to 12 bits.
+// Since elements are 4 bytes, we the size limit for an array is 2^12 / 4.
+param int LIMIT = 1024;
+
+export
+fn large_array() -> reg u32 {
+    reg u32 r;
+    stack u32[LIMIT + 1] a;
+
+    r = 0;
+    a[LIMIT] = r;
+    r = a[LIMIT];
+
+    reg bool b;
+    b = r <= 3;
+    a[LIMIT] = r if b;
+    r = a[LIMIT] if b;
+
+    return r;
+}