From 61b41b4f2e46ecd4a023ce72e72f697b5f1e2637 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 20 Nov 2020 12:32:11 +0100 Subject: draft of the exec_bblock Asmblockdeps proof --- aarch64/Asmblockprops.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'aarch64/Asmblockprops.v') 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: -- cgit