From 6f2b5713f8e378e6e074f35a537e86a497c64e35 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Sep 2016 12:32:26 +0200 Subject: Add interference for indirect calls. Avoids problems with overwritting the registe containing the function address. Bug 19779 --- arm/Machregs.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'arm/Machregs.v') diff --git a/arm/Machregs.v b/arm/Machregs.v index b43f9be6..e97df790 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -58,7 +58,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -161,6 +161,9 @@ Definition destroyed_by_setstack (ty: typ): list mreg := nil. Definition destroyed_at_function_entry: list mreg := R12 :: nil. +Definition destroyed_at_indirect_call: list mreg := + R0 :: R1 :: R2 :: R3 :: nil. + Definition temp_for_parent_frame: mreg := R12. @@ -177,6 +180,7 @@ Global Opaque destroyed_by_op destroyed_by_load destroyed_by_store destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame + destroyed_at_indirect_call mregs_for_operation mregs_for_builtin. (** Two-address operations. Return [true] if the first argument and -- cgit