Add interference for indirect calls.

Avoids problems with overwritting the registe containing the
function address.
Bug 19779

5 files changed, 22 insertions, 6 deletions

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
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 0013d91a..b91bad27 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -657,9 +657,12 @@ let add_interfs_instr g instr live =
   | Xstore(chunk, addr, args, src) ->
       add_interfs_destroyed g live (destroyed_by_store chunk addr)
   | Xcall(sg, vos, args, res) ->
+      begin match vos with
+      | Coq_inl v ->  List.iter (fun r -> IRC.add_interf g (vmreg r) v) destroyed_at_indirect_call
+      | _ -> () end;
       add_interfs_destroyed g (vset_removelist res live) destroyed_at_call
   | Xtailcall(sg, Coq_inl v, args) ->
-      List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs
+      List.iter (fun r -> IRC.add_interf g (vmreg r) v) (int_callee_save_regs @ destroyed_at_indirect_call)
   | Xtailcall(sg, Coq_inr id, args) ->
       ()
   | Xbuiltin(ef, args, res) ->
diff --git a/extraction/extraction.v b/extraction/extraction.v
index e7f2e2fc..aecc07a5 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -159,12 +159,13 @@ Separate Extraction
    Ctyping.typecheck_program
    Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr
    Ctypes.make_program
-   Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs 
-   Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs 
+   Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs
+   Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs
    Conventions1.dummy_int_reg Conventions1.dummy_float_reg
    RTL.instr_defs RTL.instr_uses
    Machregs.mregs_for_operation Machregs.mregs_for_builtin
    Machregs.two_address_op Machregs.is_stack_reg
+   Machregs.destroyed_at_indirect_call
    AST.signature_main
    Floats.Float32.from_parsed Floats.Float.from_parsed
    Globalenvs.Senv.invert_symbol
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index fb80a1fd..3a6ae674 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -55,7 +55,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
@@ -166,6 +166,9 @@ Definition destroyed_at_function_entry: list mreg :=
   (* must include [destroyed_by_setstack ty] *)
   DX :: FP0 :: nil.
 
+Definition destroyed_at_indirect_call: list mreg :=
+  nil.
+
 Definition destroyed_by_setstack (ty: typ): list mreg :=
   match ty with
   | Tfloat | Tsingle => FP0 :: nil
@@ -210,6 +213,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store
     destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
+    destroyed_at_indirect_call
     destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame
     mregs_for_operation mregs_for_builtin.
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 24065254..ce9c3542 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -76,7 +76,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
@@ -210,6 +210,9 @@ Definition destroyed_by_setstack (ty: typ): list mreg :=
 Definition destroyed_at_function_entry: list mreg :=
   nil.
 
+Definition destroyed_at_indirect_call: list mreg :=
+  nil.
+
 Definition temp_for_parent_frame: mreg :=
   R11.
 
@@ -230,6 +233,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store
     destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
+    destroyed_at_indirect_call
     destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame
     mregs_for_operation mregs_for_builtin.