diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-21 17:21:56 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-21 17:21:56 +0200 |
| commit | e342ebbfe9751639e6e0d87a69029661376060b0 (patch) | |
| tree | ce69fd271542f15447afff261eafc19ea35a4b51 /aarch64/Asmblock.v | |
| parent | 58083528c9dec31cbc1405a236fc6e3dc7779438 (diff) | |
| download | compcert-kvx-e342ebbfe9751639e6e0d87a69029661376060b0.tar.gz compcert-kvx-e342ebbfe9751639e6e0d87a69029661376060b0.zip | |
Adding buitin_args lemmas
There was an issue with the register PC in the eval_BA constructor for builtin : we were not able to prove that the concerned reg was different from PC.
This commit modify the definitions in Asmgen and Asmblock to support this, by replacing the parameter with a dreg instead of a preg.
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 950e28e9..67ad2aa5 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -217,7 +217,7 @@ Inductive control: Type := | PCtlFlow (i: cf_instruction) (** Pseudo-instructions *) | Pbuiltin (ef: external_function) - (args: list (builtin_arg preg)) (res: builtin_res preg) (**r built-in function (pseudo) *) + (args: list (builtin_arg dreg)) (res: builtin_res dreg) (**r built-in function (pseudo) *) . Coercion PCtlFlow: cf_instruction >-> control. @@ -1900,7 +1900,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out [X30] is used for the return address, and can also be used as temporary. [X16] can be used as temporary. *) -Definition preg_of (r: mreg) : preg := +Definition dreg_of (r: mreg) : dreg := match r with | R0 => X0 | R1 => X1 | R2 => X2 | R3 => X3 | R4 => X4 | R5 => X5 | R6 => X6 | R7 => X7 @@ -1920,6 +1920,9 @@ Definition preg_of (r: mreg) : preg := | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31 end. +Definition preg_of (r: mreg) : preg := + dreg_of r. + (** Undefine all registers except SP and callee-save registers *) Definition undef_caller_save_regs (rs: regset) : regset := @@ -1979,10 +1982,10 @@ Inductive exec_exit (f: function) size_b (rs: regset) (m: mem): (option control) exec_cfi f cfi (incrPC size_b rs) m = Next rs' m' -> exec_exit f size_b rs m (Some (PCtlFlow cfi)) E0 rs' m' | builtin_step ef args res vargs t vres rs' m': - eval_builtin_args ge rs rs#SP m args vargs -> + eval_builtin_args ge (fun (r: dreg) => rs r) rs#SP m args vargs -> external_call ef ge vargs m t vres m' -> rs' = incrPC size_b - (set_res res vres + (set_res (map_builtin_res DR res) vres (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> exec_exit f size_b rs m (Some (Pbuiltin ef args res)) t rs' m' . |