diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-09 16:48:53 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-09 16:48:53 +0100 |
| commit | cd386c6943576049412760c0a72ff90e034a43d2 (patch) | |
| tree | f68db5dbb9ca03cfd7f36f6afb51afd2ace4730f /aarch64/Asmblock.v | |
| parent | 86d2b0555ee09d648c8d7373b0a9a4acdcb344e0 (diff) | |
| download | compcert-kvx-cd386c6943576049412760c0a72ff90e034a43d2.tar.gz compcert-kvx-cd386c6943576049412760c0a72ff90e034a43d2.zip | |
First version of the oracle checker, does not compile yet
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 9 |
1 files changed, 9 insertions, 0 deletions
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'. |