From e342ebbfe9751639e6e0d87a69029661376060b0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 21 Oct 2020 17:21:56 +0200 Subject: 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. --- aarch64/Asmblock.v | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'aarch64/Asmblock.v') 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' . -- cgit