diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-08-02 14:26:16 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2017-08-02 14:26:16 +0200 |
| commit | 9f6e2aac73ca1f863d236f86f446b0894c8ebcef (patch) | |
| tree | d87b9b562eb83f7ea36b7deb97289839f59b2331 /arm/Asmgenproof.v | |
| parent | 0aa08f5d521401644b5c839239de97f587e0a217 (diff) | |
| download | compcert-kvx-9f6e2aac73ca1f863d236f86f446b0894c8ebcef.tar.gz compcert-kvx-9f6e2aac73ca1f863d236f86f446b0894c8ebcef.zip | |
Improve stack offset addressing
Functions which require large amounts of stack for spilling and/or arguments for function calls lead to stackframe offsets that exceed the 12bit limit of immediate constants in ARM instructions. This patch fixes the stack-offsets in the function prolog/epilog.
Diffstat (limited to 'arm/Asmgenproof.v')
| -rw-r--r-- | arm/Asmgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 09c20d5c..f306f43a 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -854,7 +854,7 @@ Opaque loadind. generalize EQ; intros EQ'. monadInv EQ'. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. subst x0. monadInv EQ0. - set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x0) in *. + set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Psavelr (fn_retaddr_ofs f) :: x0) in *. set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. @@ -877,7 +877,7 @@ Opaque loadind. simpl. auto. simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). rewrite Ptrofs.add_zero_l. simpl. unfold Tptr, chunk_of_type, Archi.ptr64 in P. simpl in P. - rewrite Ptrofs.add_zero_l in P. rewrite ATLR. rewrite Ptrofs.of_int_to_int by auto. + rewrite Ptrofs.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto. left; exists (State rs3 m3'); split. eapply exec_straight_steps_1; eauto. omega. constructor. |