Take asm clobbers into account for determining callee-save registers used.

9 files changed, 37 insertions, 4 deletions

diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index 5486c4b4..3f7d0693 100644
--- a/arm/Machregsaux.ml
+++ b/arm/Machregsaux.ml
@@ -41,3 +41,10 @@ let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
 
+let mregs_of_clobber idl =
+  List.fold_left
+    (fun l c ->
+      match register_by_name (Camlcoq.extern_atom c) with
+      | Some r -> r :: l
+      | None -> l)
+    [] idl
diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli
index 400c5abb..90343b5b 100644
--- a/arm/Machregsaux.mli
+++ b/arm/Machregsaux.mli
@@ -15,3 +15,4 @@
 val register_by_name: string -> Machregs.mreg option
 val can_reserve_register: Machregs.mreg -> bool
 val name_of_register: Machregs.mreg -> string option
+val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 249ff796..7528b66e 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -87,6 +87,8 @@ Section BOUNDS.
 
 Variable f: function.
 
+Parameter mregs_of_clobber: list ident -> list mreg.
+
 (** In the proof of the [Stacking] pass, we only need to bound the
   registers written by an instruction.  Therefore, this function
   returns these registers, ignoring registers used only as
@@ -101,6 +103,7 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lstore chunk addr args src => nil
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
+  | Lbuiltin (EF_inline_asm txt typs clob) args res => res ++ mregs_of_clobber clob
   | Lbuiltin ef args res => res ++ destroyed_by_builtin ef
   | Lannot ef args => nil
   | Llabel lbl => nil
@@ -351,7 +354,9 @@ Proof.
 (* call *)
   eapply size_arguments_bound; eauto.
 (* builtin *)
-  apply H1. apply in_or_app; auto. 
+  apply H1. destruct e; apply in_or_app; auto.
+  change (destroyed_by_builtin (EF_inline_asm text sg clobbers)) with (@nil mreg) in H2.
+  simpl in H2; tauto.
 (* annot *)
   apply H0. rewrite slots_of_locs_charact; auto. 
 Qed.
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 1db52ef3..4c400036 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -22,6 +22,7 @@ Require Inlining.
 Require ValueDomain.
 Require Tailcall.
 Require Allocation.
+Require Bounds.
 Require Ctypes.
 Require Csyntax.
 Require Ctyping.
@@ -76,6 +77,9 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc".
 (* Linearize *)
 Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 
+(* Bounds *)
+Extract Constant Bounds.mregs_of_clobber => "Machregsaux.mregs_of_clobber".
+
 (* SimplExpr *)
 Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident".
 Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2.
diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml
index 3083cf3e..75fd588a 100644
--- a/ia32/Machregsaux.ml
+++ b/ia32/Machregsaux.ml
@@ -38,3 +38,10 @@ let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
 
+let mregs_of_clobber idl =
+  List.fold_left
+    (fun l c ->
+      match register_by_name (Camlcoq.extern_atom c) with
+      | Some r -> r :: l
+      | None -> l)
+    [] idl
diff --git a/ia32/Machregsaux.mli b/ia32/Machregsaux.mli
index 4cd79024..f09ebddb 100644
--- a/ia32/Machregsaux.mli
+++ b/ia32/Machregsaux.mli
@@ -15,3 +15,4 @@
 val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val can_reserve_register: Machregs.mreg -> bool
+val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index b8d7c97f..f8253ca4 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -49,3 +49,10 @@ let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
 
+let mregs_of_clobber idl =
+  List.fold_left
+    (fun l c ->
+      match register_by_name (Camlcoq.extern_atom c) with
+      | Some r -> r :: l
+      | None -> l)
+    [] idl
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index 400c5abb..90343b5b 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -15,3 +15,4 @@
 val register_by_name: string -> Machregs.mreg option
 val can_reserve_register: Machregs.mreg -> bool
 val name_of_register: Machregs.mreg -> string option
+val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list
diff --git a/test/regression/extasm.c b/test/regression/extasm.c
index a69b3e79..4925392e 100644
--- a/test/regression/extasm.c
+++ b/test/regression/extasm.c
@@ -6,11 +6,11 @@ int clobbers(int x)
   int y;
   asm("TEST0 out:%0 in:%1" : "=r"(y) : "r"(x) : "cc"
 #if defined(__i386__)
-      , "eax", "edx", "ecx"
+      , "eax", "edx", "ebx"
 #elif defined(__arm__)
-      , "r0", "r1", "r2"
+      , "r0", "r1", "r4"
 #elif defined(__PPC__)
-      , "r3", "r4", "r5"
+      , "r3", "r4", "r31"
 #endif
 );
   return y;