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/Asmblock.v | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 3973abc0..bdcead0b 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1478,8 +1478,12 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := Definition incrPC size_b (rs: regset) := rs#PC <- (Val.offset_ptr rs#PC size_b). -Definition estep (f: function) cfi size_b (rs: regset) (m: mem) := - exec_cfi f cfi (incrPC size_b rs) m. +Definition estep (f: function) oc size_b (rs: regset) (m: mem) := + match oc with + | Some (PCtlFlow cfi) => exec_cfi f cfi (incrPC size_b rs) m + | Some (Pbuiltin ef args res) => None + | None => Next (incrPC size_b rs) m + end. (** execution of the exit instruction of a bblock *) Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) -> trace -> regset -> mem -> Prop := @@ -1497,9 +1501,15 @@ Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m' . -Definition bbstep f cfi size_b bdy rs m := - match exec_body bdy rs m with - | Some (State rs' m') => estep f cfi size_b rs' m' +(*Definition bbstep f cfi size_b bdy rs m :=*) + (*match exec_body bdy rs m with*) + (*| Some (State rs' m') => estep f cfi size_b rs' m'*) + (*| Stuck => Stuck*) + (*end.*) + +Definition bbstep f bb rs m := + match exec_body (body bb) rs m with + | Some (State rs' m') => estep f (exit bb) (Ptrofs.repr (size bb)) rs' m' | Stuck => Stuck end. -- cgit