diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-20 12:32:11 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-20 12:32:11 +0100 |
| commit | 61b41b4f2e46ecd4a023ce72e72f697b5f1e2637 (patch) | |
| tree | 2ecbe0f2fe023c47576475885c3a0ffcaca5b44b /aarch64/Asmblockprops.v | |
| parent | 169764e1873c6c04ed8027eec7e016365d6b5434 (diff) | |
| download | compcert-kvx-61b41b4f2e46ecd4a023ce72e72f697b5f1e2637.tar.gz compcert-kvx-61b41b4f2e46ecd4a023ce72e72f697b5f1e2637.zip | |
draft of the exec_bblock Asmblockdeps proof
Diffstat (limited to 'aarch64/Asmblockprops.v')
| -rw-r--r-- | aarch64/Asmblockprops.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/aarch64/Asmblockprops.v b/aarch64/Asmblockprops.v index 782d8aee..d1015ea9 100644 --- a/aarch64/Asmblockprops.v +++ b/aarch64/Asmblockprops.v @@ -25,8 +25,13 @@ Require Import Axioms. Definition bblock_simu (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := forall rs m rs' m' t, - exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk ge f bb rs m t rs' m'. + exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk ge f bb' rs m t rs' m'. +Definition bblock_simu_aux (lk: aarch64_linker) (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) := + forall rs m, + bbstep lk ge f bb rs m <> Stuck -> + bbstep lk ge f bb rs m = bbstep lk ge f bb' rs m. + Hint Extern 2 (_ <> _) => congruence: asmgen. Lemma preg_of_data: |