diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-25 00:25:05 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-25 00:25:05 +0100 |
| commit | 0e42b14d8e3c1a87a0242468bb5ace8ec8f9ef9a (patch) | |
| tree | f890a86aca25be3686dad57fcae4b2486d3e165b /aarch64 | |
| parent | ef9c9d4eb1e6e4ed1db4b57d647d60b0491e63ca (diff) | |
| download | compcert-kvx-0e42b14d8e3c1a87a0242468bb5ace8ec8f9ef9a.tar.gz compcert-kvx-0e42b14d8e3c1a87a0242468bb5ace8ec8f9ef9a.zip | |
proof forward
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 0b863162..e7b13cc9 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -893,20 +893,25 @@ Local Transparent destroyed_by_op. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_opt_steps_goto; eauto. intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C). + exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). exists jmp; exists k; exists rs'. split. eexact A. split. apply agree_exten with rs0; auto with asmgen. - exact B. + split. + exact B. + rewrite D. exact LEAF. - (* Mcond false *) exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps; eauto. intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C). + exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto. split. apply agree_exten with rs0; auto. intros. Simpl. + split. simpl; congruence. + Simpl. rewrite D. + exact LEAF. - (* Mjumptable *) assert (f0 = f) by congruence. subst f0. @@ -928,6 +933,10 @@ Local Transparent destroyed_by_op. simpl. intros. rewrite C; auto with asmgen. Simpl. congruence. + rewrite C by congruence. + repeat rewrite Pregmap.gso by congruence. + assumption. + - (* Mreturn *) assert (f0 = f) by congruence. subst f0. inversion AT; subst. simpl in H6; monadInv H6. @@ -970,7 +979,7 @@ Local Transparent destroyed_by_op. simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. change (rs2 X2) with sp. eexact P. simpl; congruence. congruence. - intros (rs3 & U & V). + intros (rs3 & U & V & W). assert (EXEC_PROLOGUE: exec_straight tge tf tf.(fn_code) rs0 m' @@ -996,7 +1005,8 @@ Local Transparent destroyed_at_function_entry. simpl. simpl; intros; Simpl. unfold sp; congruence. intros. rewrite V by auto with asmgen. reflexivity. - + intro IS_LEAF. + - (* external function *) exploit functions_translated; eauto. intros [tf [A B]]. simpl in B. inv B. |