From cd386c6943576049412760c0a72ff90e034a43d2 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 9 Nov 2020 16:48:53 +0100 Subject: First version of the oracle checker, does not compile yet --- aarch64/Asmblock.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'aarch64/Asmblock.v') diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 4bc56a05..5da7e20a 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1470,6 +1470,9 @@ 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. + (** 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 := | none_step: @@ -1486,6 +1489,12 @@ 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' + | Stuck => Stuck + end. + Definition exec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (t:trace) (rs':regset) (m':mem): Prop := exists rs1 m1, exec_body (body b) rs m = Next rs1 m1 /\ exec_exit f (Ptrofs.repr (size b)) rs1 m1 (exit b) t rs' m'. -- cgit