Future-proofing: keep signature information in IA32 and PowerPC Asm, just like we already do in ARM Asm.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 67 insertions, 63 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 78c4c3b..7bd1755 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -181,13 +181,13 @@ Inductive instruction: Type :=
   | Pxorpd_f (rd: freg)	              (**r [xor] with self = set to zero *)
   (** Branches and calls *)
   | Pjmp_l (l: label)
-  | Pjmp_s (symb: ident)
-  | Pjmp_r (r: ireg)
+  | Pjmp_s (symb: ident) (sg: signature)
+  | Pjmp_r (r: ireg) (sg: signature)
   | Pjcc (c: testcond)(l: label)
   | Pjcc2 (c1 c2: testcond)(l: label)   (**r pseudo *)
   | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *)
-  | Pcall_s (symb: ident)
-  | Pcall_r (r: ireg)
+  | Pcall_s (symb: ident) (sg: signature)
+  | Pcall_r (r: ireg) (sg: signature)
   | Pret
   (** Pseudo-instructions *)
   | Plabel(l: label)
@@ -201,9 +201,8 @@ with annot_param : Type :=
   | APstack: memory_chunk -> Z -> annot_param.
 
 Definition code := list instruction.
-Definition function := code.
-Definition fn_code (f: function) : code := f.
-Definition fundef := AST.fundef code.
+Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
+Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
 
 (** * Operational semantics *)
@@ -423,8 +422,8 @@ Definition nextinstr (rs: regset) :=
 Definition nextinstr_nf (rs: regset) : regset :=
   nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs).
 
-Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) :=
-  match label_pos lbl 0 c with
+Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
+  match label_pos lbl 0 (fn_code f) with
   | None => Stuck
   | Some pos =>
       match rs#PC with
@@ -469,7 +468,7 @@ Definition exec_store (chunk: memory_chunk) (m: mem)
     but we do not need to model this precisely.
 *)
 
-Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome :=
+Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
   (** Moves *)
   | Pmov_rr rd r1 =>
@@ -627,20 +626,20 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m
   (** Branches and calls *)
   | Pjmp_l lbl =>
-      goto_label c lbl rs m
-  | Pjmp_s id =>
+      goto_label f lbl rs m
+  | Pjmp_s id sg =>
       Next (rs#PC <- (symbol_offset id Int.zero)) m
-  | Pjmp_r r =>
+  | Pjmp_r r sg =>
       Next (rs#PC <- (rs r)) m
   | Pjcc cond lbl =>
       match eval_testcond cond rs with
-      | Some true => goto_label c lbl rs m
+      | Some true => goto_label f lbl rs m
       | Some false => Next (nextinstr rs) m
       | None => Stuck
       end
   | Pjcc2 cond1 cond2 lbl =>
       match eval_testcond cond1 rs, eval_testcond cond2 rs with
-      | Some true, Some true => goto_label c lbl rs m
+      | Some true, Some true => goto_label f lbl rs m
       | Some _, Some _ => Next (nextinstr rs) m
       | _, _ => Stuck
       end
@@ -649,13 +648,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       | Vint n => 
           match list_nth_z tbl (Int.unsigned n) with
           | None => Stuck
-          | Some lbl => goto_label c lbl rs m
+          | Some lbl => goto_label f lbl rs m
           end
       | _ => Stuck
       end
-  | Pcall_s id =>
+  | Pcall_s id sg =>
       Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m
-  | Pcall_r r =>
+  | Pcall_r r sg =>
       Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (rs r)) m
   | Pret =>
       Next (rs#PC <- (rs#RA)) m
@@ -760,27 +759,27 @@ Inductive state: Type :=
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
-      forall b ofs c i rs m rs' m',
+      forall b ofs f i rs m rs' m',
       rs PC = Vptr b ofs ->
-      Genv.find_funct_ptr ge b = Some (Internal c) ->
-      find_instr (Int.unsigned ofs) c = Some i ->
-      exec_instr c i rs m = Next rs' m' ->
+      Genv.find_funct_ptr ge b = Some (Internal f) ->
+      find_instr (Int.unsigned ofs) f.(fn_code) = Some i ->
+      exec_instr f i rs m = Next rs' m' ->
       step (State rs m) E0 (State rs' m')
   | exec_step_builtin:
-      forall b ofs c ef args res rs m t vl rs' m',
+      forall b ofs f ef args res rs m t vl rs' m',
       rs PC = Vptr b ofs ->
-      Genv.find_funct_ptr ge b = Some (Internal c) ->
-      find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) ->
+      Genv.find_funct_ptr ge b = Some (Internal f) ->
+      find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
       external_call' ef ge (map rs args) m t vl m' ->
       rs' = nextinstr_nf 
              (set_regs res vl
                (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
       step (State rs m) t (State rs' m')
   | exec_step_annot:
-      forall b ofs c ef args rs m vargs t v m',
+      forall b ofs f ef args rs m vargs t v m',
       rs PC = Vptr b ofs ->
-      Genv.find_funct_ptr ge b = Some (Internal c) ->
-      find_instr (Int.unsigned ofs) c = Some (Pannot ef args) ->
+      Genv.find_funct_ptr ge b = Some (Internal f) ->
+      find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) ->
       annot_arguments rs m args vargs ->
       external_call' ef ge vargs m t v m' ->
       step (State rs m) t
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 0410057..740dff8 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -496,16 +496,16 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mstore chunk addr args src =>
       transl_store chunk addr args src k
   | Mcall sig (inl reg) =>
-      do r <- ireg_of reg; OK (Pcall_r r :: k)
+      do r <- ireg_of reg; OK (Pcall_r r sig :: k)
   | Mcall sig (inr symb) =>
-      OK (Pcall_s symb :: k)
+      OK (Pcall_s symb sig :: k)
   | Mtailcall sig (inl reg) =>
       do r <- ireg_of reg; 
       OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
-          Pjmp_r r :: k)
+          Pjmp_r r sig :: k)
   | Mtailcall sig (inr symb) =>
       OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
-          Pjmp_s symb :: k)
+          Pjmp_s symb sig :: k)
   | Mlabel lbl =>
       OK(Plabel lbl :: k)
   | Mgoto lbl =>
@@ -563,11 +563,16 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo
   otherwise the offset part of the [PC] code pointer could wrap
   around, leading to incorrect executions. *)
 
-Definition transf_function (f: Mach.function) : res Asm.code :=
+Definition transl_function (f: Mach.function) :=
   do c <- transl_code' f f.(Mach.fn_code) true;
-  if zlt (list_length_z c) Int.max_unsigned 
-  then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)
-  else Error (msg "code size exceeded").
+  OK (mkfunction f.(Mach.fn_sig)
+        (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)).
+
+Definition transf_function (f: Mach.function) : res Asm.function :=
+  do tf <- transl_function f;
+  if zlt Int.max_unsigned (list_length_z tf.(fn_code))
+  then Error (msg "code size exceeded")
+  else OK tf.
 
 Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
   transf_partial_fundef transf_function f.
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index df09ca7..fa8ce6c 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -77,10 +77,10 @@ Qed.
 
 Lemma transf_function_no_overflow:
   forall f tf,
-  transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned.
+  transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned.
 Proof.
-  intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0.
-  rewrite list_length_z_cons. omega. 
+  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); monadInv EQ0.
+  omega. 
 Qed.
 
 Lemma exec_straight_exec:
@@ -299,12 +299,12 @@ Lemma transl_find_label:
   forall lbl f tf,
   transf_function f = OK tf ->
   match Mach.find_label lbl f.(Mach.fn_code) with
-  | None => find_label lbl tf = None
-  | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc
+  | None => find_label lbl tf.(fn_code) = None
+  | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc
   end.
 Proof.
-  intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0.
-  simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ; eauto. 
+  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0.
+  monadInv EQ. simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ0; eauto. 
 Qed.
 
 End TRANSL_LABEL.
@@ -346,8 +346,8 @@ Proof.
 - intros. exploit transl_instr_label; eauto. 
   destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
 - intros. monadInv H0. 
-  destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0.
-  rewrite transl_code'_transl_code in EQ.
+  destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0.
+  monadInv EQ. rewrite transl_code'_transl_code in EQ0.
   exists x; exists true; split; auto. unfold fn_code. repeat constructor.
 - exact transf_function_no_overflow.
 Qed.
@@ -583,7 +583,7 @@ Opaque loadind.
 - (* Mcall *)
   assert (f0 = f) by congruence.  subst f0.
   inv AT. 
-  assert (NOOV: list_length_z tf <= Int.max_unsigned).
+  assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   destruct ros as [rf|fid]; simpl in H; monadInv H5.
 + (* Indirect call *)
@@ -623,7 +623,7 @@ Opaque loadind.
 - (* Mtailcall *)
   assert (f0 = f) by congruence.  subst f0.
   inv AT. 
-  assert (NOOV: list_length_z tf <= Int.max_unsigned).
+  assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
   exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
@@ -820,7 +820,7 @@ Transparent destroyed_by_jumptable.
 - (* Mreturn *)
   assert (f0 = f) by congruence. subst f0.
   inv AT. 
-  assert (NOOV: list_length_z tf <= Int.max_unsigned).
+  assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
   exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. 
@@ -844,8 +844,9 @@ Transparent destroyed_by_jumptable.
 
 - (* internal function *)
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
-  generalize EQ; intros EQ'. monadInv EQ'. rewrite transl_code'_transl_code in EQ0.
-  destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1.
+  generalize EQ; intros EQ'. monadInv EQ'.
+  destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inv EQ1.
+  monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
   unfold store_stack in *. 
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
   intros [m1' [C D]].
@@ -855,14 +856,13 @@ Transparent destroyed_by_jumptable.
   intros [m3' [P Q]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto. 
-  subst x; simpl.
-  rewrite Int.unsigned_zero. simpl. eauto.
+  simpl. rewrite Int.unsigned_zero. simpl. eauto.
   simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F.
   simpl in P. rewrite ATLR. rewrite P. eauto.
   econstructor; eauto.
   unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. 
   rewrite ATPC. simpl. constructor; eauto.
-  subst x. unfold fn_code. eapply code_tail_next_int. rewrite list_length_z_cons. omega. 
+  unfold fn_code. eapply code_tail_next_int. simpl in g. omega. 
   constructor. 
   apply agree_nextinstr. eapply agree_change_sp; eauto.
 Transparent destroyed_at_function_entry.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 9ddc463..5d3df67 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -97,7 +97,7 @@ Ltac Simplifs := repeat Simplif.
 Section CONSTRUCTORS.
 
 Variable ge: genv.
-Variable fn: code.
+Variable fn: function.
 
 (** Smart constructor for moves. *)
 
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 4480f91..3badbfc 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -681,9 +681,9 @@ let print_instruction oc = function
   (** Branches and calls *)
   | Pjmp_l(l) ->
       fprintf oc "	jmp	%a\n" label (transl_label l)
-  | Pjmp_s(f) ->
+  | Pjmp_s(f, sg) ->
       fprintf oc "	jmp	%a\n" symbol f
-  | Pjmp_r(r) ->
+  | Pjmp_r(r, sg) ->
       fprintf oc "	jmp	*%a\n" ireg r
   | Pjcc(c, l) ->
       let l = transl_label l in
@@ -698,9 +698,9 @@ let print_instruction oc = function
       let l = new_label() in
       fprintf oc "	jmp	*%a(, %a, 4)\n" label l ireg r;
       jumptables := (l, tbl) :: !jumptables
-  | Pcall_s(f) ->
+  | Pcall_s(f, sg) ->
       fprintf oc "	call	%a\n" symbol f
-  | Pcall_r(r) ->
+  | Pcall_r(r, sg) ->
       fprintf oc "	call	*%a\n" ireg r
   | Pret ->
       fprintf oc "	ret\n"
@@ -758,7 +758,7 @@ let print_jumptable oc (lbl, tbl) =
     (fun l -> fprintf oc "	.long	%a\n" label (transl_label l))
     tbl
 
-let print_function oc name code =
+let print_function oc name fn =
   Hashtbl.clear current_function_labels;
   float_literals := [];
   jumptables := [];
@@ -775,7 +775,7 @@ let print_function oc name code =
   fprintf oc "%a:\n" symbol name;
   print_location oc (C2C.atom_location name);
   cfi_startproc oc;
-  List.iter (print_instruction oc) code;
+  List.iter (print_instruction oc) fn.fn_code;
   cfi_endproc oc;
   if target = ELF then begin
     fprintf oc "	.type	%a, @function\n" symbol name;
diff --git a/ia32/Unusedglob1.ml b/ia32/Unusedglob1.ml
index fe962e2..8332a30 100644
--- a/ia32/Unusedglob1.ml
+++ b/ia32/Unusedglob1.ml
@@ -35,10 +35,10 @@ let referenced_instr = function
   | Pmovzb_rm (_, a) | Pmovsb_rm (_, a)
   | Pmovzw_rm (_, a) | Pmovsw_rm (_, a)
   | Pcvtss2sd_fm (_, a) | Pcvtsd2ss_mf (a, _) | Plea (_, a) -> referenced_addr a
-  | Pjmp_s s -> [s]
-  | Pcall_s s -> [s]
+  | Pjmp_s(s, _) -> [s]
+  | Pcall_s(s, _) -> [s]
   | Pbuiltin(ef, args, res) -> referenced_builtin ef
   | _ -> []
 
-let code_of_function f = f
+let code_of_function f = f.fn_code