Split large memory accesses in stack alloc

compiler/config/tests.config

@@ -40,18 +40,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
 
 [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]
@@ -71,12 +71,11 @@ 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
+kodirs  = tests/fail/**/arm-m4 test/success/arm-m4/large_memory_immediates

compiler/src/compile.ml

@@ -183,10 +183,22 @@ 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 ->
+          let msg =
+            "This memory immediate does not fit in one instruction, several \
+             instructions were issued."
+          in
+          Some (SplitMemoryAccess, msg)
+    in
+    let loc, _ = ii in
+    Option.may (fun (w, msg) -> warning w loc "%s" msg) o;
     ii
   in
 

compiler/src/printer.ml

@@ -405,9 +405,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/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

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

compiler/src/utils.mli

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

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

@@ -0,0 +1,18 @@
+// 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];
+
+    return r;
+}

proofs/compiler/arm_decl.v

@@ -381,6 +381,12 @@ Definition is_expandable_or_shift (n : Z) : bool :=
    | EI_byte | EI_pattern | EI_shift => true
    | EI_none => false
   end.
-
-Definition is_w12_encoding (z : Z) : bool := (z <? Z.pow 2 12)%Z.
-Definition is_w16_encoding (z : Z) : bool := (z <? Z.pow 2 16)%Z.
+
+Definition is_w12_encoding (z : Z) : bool := [&& 0 <=? z & z <? Z.pow 2 12 ]%Z.
+Definition is_w16_encoding (z : Z) : bool := [&& 0 <=? z & z <? Z.pow 2 16 ]%Z.
+
+(* The LDR/STR families can take 12-bit unsigned immediates or 8-bit signed
+   immediates. *)
+Definition is_mem_immediate (z : Z) : bool :=
+  let u := (if z <? 0 then z + wbase reg_size else z)%Z in
+  is_w12_encoding u || [&& -256 <? z & z <? 256 ]%Z.

proofs/compiler/arm_params.v

@@ -77,11 +77,46 @@ Definition arm_immediate (x: var_i) z :=
 Definition arm_swap t (x y z w : var_i) :=
   Copn [:: Lvar x; Lvar y] t (Oasm (ExtOp (Oarm_swap reg_size))) [:: Plvar z; Plvar w].
 
+(* Build the the immediate [eoff] if it does not fit in a single LDR/STR
+   instruction. *)
+Definition lower_mem_off (tmp : var_i) (eoff : pexpr) : seq copn_args * pexpr :=
+  if expr.is_wconst reg_size eoff is Some woff
+  then ARMCopn.load_mem_imm tmp woff
+  else ([::], eoff).
+
+Definition split_mem_opn_match_lvs lvs :=
+  if lvs is [:: Lmem ws vbase eoff ] then Some (ws, vbase, eoff) else None.
+
+Definition split_mem_opn_match_es es :=
+  if es is [:: Pload ws vbase eoff ] then Some (ws, vbase, eoff) else None.
+
+(* Call [lower_mem_off] on memory accesses. *)
+Definition split_mem_opn
+  (tmp : var_i)
+  (lvs : seq lval)
+  (op : sopn)
+  (es : seq pexpr) :
+  cexec (seq copn_args) :=
+  if split_mem_opn_match_lvs lvs is Some (ws, vbase, eoff)
+  then
+    (* STR *)
+    let '(pre, eoff) := lower_mem_off tmp eoff in
+    ok (rcons pre ([:: Lmem ws vbase eoff ], op, es))
+  else
+    if split_mem_opn_match_es es is Some (ws, vbase, eoff)
+    then
+      (* LDR *)
+      let '(pre, eoff) := lower_mem_off tmp eoff in
+      ok (rcons pre (lvs, op, [:: Pload ws vbase eoff ]))
+    else
+      ok [:: (lvs, op, es) ].
+
 Definition arm_saparams : stack_alloc_params :=
   {|
     sap_mov_ofs := arm_mov_ofs;
     sap_immediate := arm_immediate;
     sap_swap := arm_swap;
+    sap_split_mem_opn := split_mem_opn;
   |}.
 
 (* ------------------------------------------------------------------------ *)

proofs/compiler/arm_params_common.v

@@ -84,6 +84,12 @@ Module ARMOpn (Args : OpnArgs).
      Precondition: if [imm] is large, [x <> tmp]. *)
   Definition smart_subi_tmp x tmp imm := map to_opn (Core.smart_subi_tmp x tmp imm).
 
+  Definition load_mem_imm
+    {_ : PointerData} (tmp : var_i) (woff : word Uptr) : seq opn_args * rval :=
+    let z := wsigned woff in
+    if is_mem_immediate z
+    then ([::], rconst Uptr z)
+    else (li tmp (wunsigned woff), rvar tmp).
 
   End WITH_PARAMS.
 

proofs/compiler/arm_params_common_proof.v

@@ -45,6 +45,87 @@ Ltac t_arm_op :=
   rewrite ?zero_extend_u ?addn1;
   t_simpl_rewrites.
 
+Module ARMCopnP.
+
+Section WITH_PARAMS.
+
+Context
+  {wsw : WithSubWord}
+  {dc : DirectCall}
+  {syscall_state : Type}
+  {sc_sem : syscall_sem syscall_state}
+  {atoI : arch_toIdent}
+  {pT : progT}
+  {sCP : semCallParams}
+  (p : prog)
+  (evt : extra_val_t)
+.
+
+Let mkv xname vi :=
+  let: x := {| vname := xname; vtype := sword arm_reg_size; |} in
+  let: xi := {| v_var := x; v_info := vi; |} in
+  (xi, x).
+
+Lemma sem_copn_equiv gd args s :
+  ARMCopn_coreP.sem_copn_args gd args s
+  = sem_copn_args gd (ARMCopn.to_opn args) s.
+Proof.
+  rewrite /sem_copn_args /sem_sopn /exec_sopn /=.
+  case: args => -[lvs o] es /=.
+  case: sem_pexprs => //= ?.
+  by case: app_sopn.
+Qed.
+
+Lemma sem_copns_equiv gd args s :
+  ARMCopn_coreP.sem_copns_args gd s args
+  = sem_copns_args gd s (map ARMCopn.to_opn args).
+Proof.
+  elim: args s => //= o os ih s.
+  rewrite sem_copn_equiv.
+  by case: sem_copn_args.
+Qed.
+
+Lemma li_sem gd s xname vi imm :
+  let: (xi, x) := mkv xname vi in
+  let: lcmd := ARMCopn.li xi imm in
+  exists vm',
+    [/\ sem_copns_args gd s lcmd = ok (with_vm s vm')
+      , vm' =[\ Sv.singleton x ] evm s
+      & get_var true vm' x = ok (Vword (wrepr reg_size imm))
+    ].
+Proof.
+  have [vm' []] := ARMCopn_coreP.li_sem_copns_args gd s xname vi imm.
+  rewrite sem_copns_equiv => h1 h2 h3.
+  by exists vm'.
+Qed.
+Opaque ARMCopn.li.
+
+Lemma load_mem_immP pre eimm xname vi imm ii tag s :
+  let: x := {| vname := xname; vtype := sword arm_reg_size; |} in
+  let: xi := {| v_var := x; v_info := vi; |} in
+  let: c := [seq i_of_copn_args ii tag a | a <- pre ] in
+  ARMCopn.load_mem_imm xi imm = (pre, eimm) ->
+  exists vm,
+    let: s' := with_vm s vm in
+    [/\ sem p evt s c s'
+      , vm =[\ Sv.singleton x ] evm s
+      & sem_pexpr true (p_globs p) s' eimm = ok (Vword imm)
+    ].
+Proof.
+  set x := {| vname := _; |}; set xi := {| v_var := _; |}.
+  rewrite /ARMCopn.load_mem_imm.
+  case: is_mem_immediate => -[??]; subst pre eimm.
+  - exists (evm s); split => //. + rewrite with_vm_same /=. by econstructor.
+    by rewrite /= /sem_sop1 /= wrepr_signed.
+  have [vm [hsem hvm hget]] := li_sem (p_globs p) s xname vi (wunsigned imm).
+  exists vm; split=> //; first exact: sem_copns_args_sem.
+  by rewrite /sem_pexpr /= /get_gvar /= hget wrepr_unsigned.
+Qed.
+
+End WITH_PARAMS.
+
+End ARMCopnP.
+
 Module ARMFopnP.
 
 Section WITH_PARAMS.

proofs/compiler/arm_params_core.v

@@ -105,4 +105,5 @@ Module ARMOpn_core (Args : OpnArgs).
 
 End ARMOpn_core.
 
+Module ARMCopn_core := ARMOpn_core(CopnArgs).
 Module ARMFopn_core := ARMOpn_core(FopnArgs).