diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-23 01:53:05 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-23 01:53:05 +0200 |
| commit | 37ad0670e1dc02c47b4987c16602aadb462c44c2 (patch) | |
| tree | 35f538126dc796187c869c9f3e2fd8993ec9e196 /aarch64/Asmgenproof.v | |
| parent | 2ff831f62b8674e41dac82b4738199eaa4fb4011 (diff) | |
| download | compcert-kvx-37ad0670e1dc02c47b4987c16602aadb462c44c2.tar.gz compcert-kvx-37ad0670e1dc02c47b4987c16602aadb462c44c2.zip | |
aarch64 compiles again (but ccomp generates incorrect assembly)
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 0ea37a38..f469e437 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Léo Gourdin UGA, VERIMAG *) (* Justus Fasse UGA, VERIMAG *) (* Xavier Leroy INRIA Paris-Rocquencourt *) (* David Monniaux CNRS, VERIMAG *) @@ -17,7 +18,7 @@ Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. -Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock. +Require Import Op Locations Machblock Conventions PseudoAsmblock Asm Asmblock. Require Machblockgenproof Asmblockgenproof. Require Import Asmgen. Require Import Axioms. @@ -1862,8 +1863,8 @@ Qed. Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m (ATPC : rs PC = Vptr b ofs) (MATCHI : match_internal (size bb - 1) - {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} - {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}), + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}), _rs PC = Vptr b (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))). Proof. intros; inv MATCHI. rewrite <- AGPC; rewrite ATPC; unfold Val.offset_ptr; eauto. @@ -1874,8 +1875,8 @@ Lemma find_instr_ofs_somei: forall ofs bb f tc asmi rs m _rs _m (FIND_INSTR : Asm.find_instr (Ptrofs.unsigned ofs + (size bb - 1)) tc = Some (asmi)) (MATCHI : match_internal (size bb - 1) - {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} - {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}), + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}), Asm.find_instr (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) (Asm.fn_code {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}) = Some (asmi). @@ -1900,8 +1901,8 @@ Qed. Lemma eval_builtin_args_match: forall bb rs m _rs _m args vargs (MATCHI : match_internal (size bb - 1) - {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} - {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}) + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}) (EVAL : eval_builtin_args tge (fun r : dreg => rs r) (rs SP) m args vargs), eval_builtin_args tge _rs (_rs SP) _m (map (map_builtin_arg DR) args) vargs. Proof. @@ -2114,9 +2115,9 @@ Proof. erewrite !set_builtin_map_not_pc. rewrite HPC. eapply set_builtin_res_dont_move_pc_gen; intros. eapply set_buitin_res_sym; eauto. +Qed. - Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) |