Initial import of compcert

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

1 files changed, 226 insertions, 0 deletions

diff --git a/backend/Stacking.v b/backend/Stacking.v
new file mode 100644
index 00000000..1f0c4542
--- /dev/null
+++ b/backend/Stacking.v
@@ -0,0 +1,226 @@
+(** Layout of activation records; translation from Linear to Mach. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Op.
+Require Import RTL.
+Require Import Locations.
+Require Import Linear.
+Require Import Lineartyping.
+Require Import Mach.
+Require Import Conventions.
+
+(** * Layout of activation records *)
+
+(** The general shape of activation records is as follows,
+  from bottom (lowest offsets) to top:
+- 24 reserved bytes.  The first 4 bytes hold the back pointer to the
+  activation record of the caller.  The next 4 bytes will be used
+  to store the return address.  The remaining 16 bytes are unused
+  but reserved in accordance with the PowerPC application binary interface.
+- Space for outgoing arguments to function calls.
+- Local stack slots of integer type.
+- Saved values of integer callee-save registers used by the function.
+- One word of padding, if necessary to align the following data
+  on a 8-byte boundary.
+- Local stack slots of float type.
+- Saved values of float callee-save registers used by the function.
+- Space for the stack-allocated data declared in Cminor.
+
+To facilitate some of the proofs, the Cminor stack-allocated data
+starts at offset 0; the preceding areas in the activation record
+therefore have negative offsets.  This part (with negative offsets)
+is called the ``frame'' (see the [Machabstr] semantics for the Mach
+language), by opposition with the ``Cminor stack data'' which is the part
+with positive offsets.
+
+The [frame_env] compilation environment records the positions of
+the boundaries between areas in the frame part.
+*)
+
+Record frame_env : Set := mk_frame_env {
+  fe_size: Z;
+  fe_ofs_int_local: Z;
+  fe_ofs_int_callee_save: Z;
+  fe_num_int_callee_save: Z;
+  fe_ofs_float_local: Z;
+  fe_ofs_float_callee_save: Z;
+  fe_num_float_callee_save: Z
+}.
+
+(** Computation of the frame environment from the bounds of the current
+  function. *)
+
+Definition make_env (b: bounds) :=
+  let oil := 4 * b.(bound_outgoing) in              (* integer locals *)
+  let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *)
+  let oendi := oics + 4 * b.(bound_int_callee_save) in
+  let ofl := align oendi 8 in       (* float locals *)
+  let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
+  let sz := ofcs + 8 * b.(bound_float_callee_save) in (* total frame size *)
+  mk_frame_env sz oil oics b.(bound_int_callee_save)
+                  ofl ofcs b.(bound_float_callee_save).
+
+(** Computation the frame offset for the given component of the frame.
+  The component is expressed by the following [frame_index] sum type. *)
+
+Inductive frame_index: Set :=
+  | FI_local: Z -> typ -> frame_index
+  | FI_arg: Z -> typ -> frame_index
+  | FI_saved_int: Z -> frame_index
+  | FI_saved_float: Z -> frame_index.
+
+Definition offset_of_index (fe: frame_env) (idx: frame_index) :=
+  match idx with
+  | FI_local x Tint => fe.(fe_ofs_int_local) + 4 * x
+  | FI_local x Tfloat => fe.(fe_ofs_float_local) + 8 * x
+  | FI_arg x ty => 4 * x
+  | FI_saved_int x => fe.(fe_ofs_int_callee_save) + 4 * x
+  | FI_saved_float x => fe.(fe_ofs_float_callee_save) + 8 * x
+  end.
+
+(** * Saving and restoring callee-save registers *)
+
+(** [save_callee_save fe k] adds before [k] the instructions that
+  store in the frame the values of callee-save registers used by the
+  current function. *)
+
+Definition save_int_callee_save (fe: frame_env) (cs: mreg) (k: Mach.code) :=
+  let i := index_int_callee_save cs in
+  if zlt i fe.(fe_num_int_callee_save)
+  then Msetstack cs (Int.repr (offset_of_index fe (FI_saved_int i))) Tint :: k
+  else k.
+
+Definition save_float_callee_save (fe: frame_env) (cs: mreg) (k: Mach.code) :=
+  let i := index_float_callee_save cs in
+  if zlt i fe.(fe_num_float_callee_save)
+  then Msetstack cs (Int.repr (offset_of_index fe (FI_saved_float i))) Tfloat :: k
+  else k.
+
+Definition save_callee_save (fe: frame_env) (k: Mach.code) :=
+  List.fold_right (save_int_callee_save fe)
+    (List.fold_right (save_float_callee_save fe) k float_callee_save_regs)
+    int_callee_save_regs.
+
+(** [restore_callee_save fe k] adds before [k] the instructions that
+  re-load from the frame the values of callee-save registers used by the
+  current function, restoring these registers to their initial values. *)
+
+Definition restore_int_callee_save (fe: frame_env) (cs: mreg) (k: Mach.code) :=
+  let i := index_int_callee_save cs in
+  if zlt i fe.(fe_num_int_callee_save)
+  then Mgetstack (Int.repr (offset_of_index fe (FI_saved_int i))) Tint cs :: k
+  else k.
+
+Definition restore_float_callee_save (fe: frame_env) (cs: mreg) (k: Mach.code) :=
+  let i := index_float_callee_save cs in
+  if zlt i fe.(fe_num_float_callee_save)
+  then Mgetstack (Int.repr (offset_of_index fe (FI_saved_float i))) Tfloat cs :: k
+  else k.
+
+Definition restore_callee_save (fe: frame_env) (k: Mach.code) :=
+  List.fold_right (restore_int_callee_save fe)
+    (List.fold_right (restore_float_callee_save fe) k float_callee_save_regs)
+    int_callee_save_regs.
+
+(** * Code transformation. *)
+
+(** Translation of operations and addressing mode.
+  In Linear, the stack pointer has offset 0, i.e. points to the
+  beginning of the Cminor stack data block.  In Mach, the stack
+  pointer points to the bottom of the activation record,
+  at offset [- fe.(fe_size)] where [fe] is the frame environment.
+  Operations and addressing mode that are relative to the stack pointer
+  must therefore be offset by [fe.(fe_size)] to preserve their
+  behaviour. *)
+
+Definition transl_op (fe: frame_env) (op: operation) :=
+  match op with
+  | Oaddrstack ofs => Oaddrstack (Int.add (Int.repr fe.(fe_size)) ofs)
+  | _ => op
+  end.
+
+Definition transl_addr (fe: frame_env) (addr: addressing) :=
+  match addr with
+  | Ainstack ofs => Ainstack (Int.add (Int.repr fe.(fe_size)) ofs)
+  | _ => addr
+  end.
+
+(** Translation of a Linear instruction.  Prepends the corresponding
+  Mach instructions to the given list of instructions.
+  [Lgetstack] and [Lsetstack] moves between registers and stack slots
+  are turned into [Mgetstack], [Mgetparent] or [Msetstack] instructions
+  at offsets determined by the frame environment.
+  Instructions and addressing modes are modified as described previously.
+  Code to restore the values of callee-save registers is inserted
+  before the function returns. *)
+
+Definition transl_instr
+    (fe: frame_env) (i: Linear.instruction) (k: Mach.code) : Mach.code :=
+  match i with
+  | Lgetstack s r =>
+      match s with
+      | Local ofs ty =>
+          Mgetstack (Int.repr (offset_of_index fe (FI_local ofs ty))) ty r :: k
+      | Incoming ofs ty =>
+          Mgetparam (Int.repr (offset_of_index fe (FI_arg ofs ty))) ty r :: k
+      | Outgoing ofs ty =>
+          Mgetstack (Int.repr (offset_of_index fe (FI_arg ofs ty))) ty r :: k
+      end
+  | Lsetstack r s =>
+      match s with
+      | Local ofs ty =>
+          Msetstack r (Int.repr (offset_of_index fe (FI_local ofs ty))) ty :: k
+      | Incoming ofs ty =>
+          k (* should not happen *)
+      | Outgoing ofs ty =>
+          Msetstack r (Int.repr (offset_of_index fe (FI_arg ofs ty))) ty :: k
+      end
+  | Lop op args res =>
+      Mop (transl_op fe op) args res :: k
+  | Lload chunk addr args dst =>
+      Mload chunk (transl_addr fe addr) args dst :: k
+  | Lstore chunk addr args src =>
+      Mstore chunk (transl_addr fe addr) args src :: k
+  | Lcall sig ros =>
+      Mcall sig ros :: k
+  | Llabel lbl =>
+      Mlabel lbl :: k
+  | Lgoto lbl =>
+      Mgoto lbl :: k
+  | Lcond cond args lbl =>
+      Mcond cond args lbl :: k
+  | Lreturn =>
+      restore_callee_save fe (Mreturn :: k)
+  end.
+
+(** Translation of a function.  Code that saves the values of used
+  callee-save registers is inserted at function entry, followed
+  by the translation of the function body.
+
+  Subtle point: the compiler must check that the frame is no
+  larger than [- Int.min_signed] bytes, otherwise arithmetic overflows
+  could occur during frame accesses using signed machine integers as
+  offsets. *)
+
+Definition transl_code
+    (fe: frame_env) (il: list Linear.instruction) : Mach.code :=
+  List.fold_right (transl_instr fe) nil il.
+
+Definition transl_body (f: Linear.function) (fe: frame_env) :=
+  save_callee_save fe (transl_code fe f.(Linear.fn_code)).
+
+Definition transf_function (f: Linear.function) : option Mach.function :=
+  let fe := make_env (function_bounds f) in
+  if zlt f.(Linear.fn_stacksize) 0 then None else
+  if zlt (- Int.min_signed) fe.(fe_size) then None else
+  Some (Mach.mkfunction
+         f.(Linear.fn_sig)
+         (transl_body f fe)
+         f.(Linear.fn_stacksize)
+         fe.(fe_size)).
+
+Definition transf_program (p: Linear.program) : option Mach.program :=
+  transform_partial_program transf_function p.