draft of the exec_bblock Asmblockdeps proof

1 files changed, 15 insertions, 5 deletions

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.