diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-08-18 11:23:05 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-08-18 11:23:05 +0200 |
commit | f66711dc06c73adf3dd715c564cb6d27b51c5199 (patch) | |
tree | e68a132caa6df4bc3215b638dfe83ddf9db7a506 /arm/Asmgenproof1.v | |
parent | ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee (diff) | |
parent | fc1b2bfea598354a3e939de35d270376c880e1b0 (diff) | |
download | compcert-f66711dc06c73adf3dd715c564cb6d27b51c5199.tar.gz compcert-f66711dc06c73adf3dd715c564cb6d27b51c5199.zip |
Merge pull request #22 from AbsIntPrivate/arm_large_offsets
Issue #P18: handle large offsets when accessing return address and back link in the stack frame
Diffstat (limited to 'arm/Asmgenproof1.v')
-rw-r--r-- | arm/Asmgenproof1.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index eec531dc..7084336e 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -616,6 +616,37 @@ Proof. intros; Simpl. Qed. +(** Saving the link register *) + +Lemma save_lr_correct: + forall ofs k (rs: regset) m m', + Mem.storev Mint32 m (Val.offset_ptr rs#IR13 ofs) (rs#IR14) = Some m' -> + exists rs', + exec_straight ge fn (save_lr ofs k) rs m k rs' m' + /\ (forall r, if_preg r = true -> r <> IR12 -> rs'#r = rs#r) + /\ (save_lr_preserves_R12 ofs = true -> rs'#IR12 = rs#IR12). +Proof. + intros; unfold save_lr, save_lr_preserves_R12. + set (n := Ptrofs.to_int ofs). set (n1 := mk_immed_mem_word n). + assert (EQ: Val.offset_ptr rs#IR13 ofs = Val.add rs#IR13 (Vint n)). + { destruct rs#IR13; try discriminate. simpl. f_equal; f_equal. unfold n; symmetry; auto with ptrofs. } + destruct (Int.eq n n1). +- econstructor; split. apply exec_straight_one. simpl; unfold exec_store. rewrite <- EQ, H; reflexivity. auto. + split. intros; Simpl. intros; Simpl. +- destruct (addimm_correct IR12 IR13 (Int.sub n n1) (Pstr IR14 IR12 (SOimm n1) :: k) rs m) + as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl; unfold exec_store. + rewrite B. rewrite Val.add_assoc. simpl. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg n1)). + rewrite Int.add_neg_zero. rewrite Int.add_zero. + rewrite <- EQ. rewrite C by eauto with asmgen. rewrite H. reflexivity. + auto. + split. intros; Simpl. congruence. +Qed. + (** Translation of shift immediates *) Lemma transl_shift_correct: |