Initial import of compcert

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

1 files changed, 295 insertions, 0 deletions

diff --git a/backend/Mach.v b/backend/Mach.v
new file mode 100644
index 00000000..f9537985
--- /dev/null
+++ b/backend/Mach.v
@@ -0,0 +1,295 @@
+(** The Mach intermediate language: abstract syntax and semantics.
+
+  Mach is the last intermediate language before generation of assembly
+  code.
+*)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Mem.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Locations.
+
+(** * Abstract syntax *)
+
+(** Like Linear, the Mach language is organized as lists of instructions
+  operating over machine registers, with default fall-through behaviour
+  and explicit labels and branch instructions.  
+
+  The main difference with Linear lies in the instructions used to
+  access the activation record.  Mach has three such instructions:
+  [Mgetstack] and [Msetstack] to read and write within the activation
+  record for the current function, at a given word offset and with a
+  given type; and [Mgetparam], to read within the activation record of
+  the caller.
+
+  These instructions implement a more concrete view of the activation
+  record than the the [Bgetstack] and [Bsetstack] instructions of
+  Linear: actual offsets are used instead of abstract stack slots; the
+  distinction between the caller's frame and the callee's frame is
+  made explicit. *)
+
+Definition label := positive.
+
+Inductive instruction: Set :=
+  | Mgetstack: int -> typ -> mreg -> instruction
+  | Msetstack: mreg -> int -> typ -> instruction
+  | Mgetparam: int -> typ -> mreg -> instruction
+  | Mop: operation -> list mreg -> mreg -> instruction
+  | Mload: memory_chunk -> addressing -> list mreg -> mreg -> instruction
+  | Mstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction
+  | Mcall: signature -> mreg + ident -> instruction
+  | Mlabel: label -> instruction
+  | Mgoto: label -> instruction
+  | Mcond: condition -> list mreg -> label -> instruction
+  | Mreturn: instruction.
+
+Definition code := list instruction.
+
+Record function: Set := mkfunction
+  { fn_sig: signature;
+    fn_code: code;
+    fn_stacksize: Z;
+    fn_framesize: Z }.
+
+Definition program := AST.program function.
+
+Definition genv := Genv.t function.
+
+(** * Dynamic semantics *)
+
+Module RegEq.
+  Definition t := mreg.
+  Definition eq := mreg_eq.
+End RegEq.
+
+Module Regmap := EMap(RegEq).
+
+Definition regset := Regmap.t val.
+
+Notation "a ## b" := (List.map a b) (at level 1).
+Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level).
+
+Definition is_label (lbl: label) (instr: instruction) : bool :=
+  match instr with
+  | Mlabel lbl' => if peq lbl lbl' then true else false
+  | _ => false
+  end.
+
+Lemma is_label_correct:
+  forall lbl instr,
+  if is_label lbl instr then instr = Mlabel lbl else instr <> Mlabel lbl.
+Proof.
+  intros.  destruct instr; simpl; try discriminate.
+  case (peq lbl l); intro; congruence.
+Qed.
+
+Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
+  match c with
+  | nil => None
+  | i1 :: il => if is_label lbl i1 then Some il else find_label lbl il
+  end.
+
+(** The three stack-related Mach instructions are interpreted as
+  memory accesses relative to the stack pointer.  More precisely:
+- [Mgetstack ofs ty r] is a memory load at offset [ofs * 4] relative
+  to the stack pointer.
+- [Msetstack r ofs ty] is a memory store at offset [ofs * 4] relative
+  to the stack pointer.
+- [Mgetparam ofs ty r] is a memory load at offset [ofs * 4]
+  relative to the pointer found at offset 0 from the stack pointer.
+  The semantics maintain a linked structure of activation records,
+  with the current record containing a pointer to the record of the
+  caller function at offset 0. *)
+
+Definition chunk_of_type (ty: typ) :=
+  match ty with Tint => Mint32 | Tfloat => Mfloat64 end.
+
+Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) :=
+  Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)).
+
+Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) :=
+  Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v.
+
+Definition align_16_top (lo hi: Z) :=
+  Zmax 0 (((hi - lo + 15) / 16) * 16 + lo).
+
+Section RELSEM.
+
+Variable ge: genv.
+
+Definition find_function (ros: mreg + ident) (rs: regset) : option function :=
+  match ros with
+  | inl r => Genv.find_funct ge (rs r)
+  | inr symb =>
+      match Genv.find_symbol ge symb with
+      | None => None
+      | Some b => Genv.find_funct_ptr ge b
+      end
+  end.
+
+(** [exec_instr ge f sp c rs m c' rs' m'] reflects the execution of
+  the first instruction in the current instruction sequence [c].  
+  [c'] is the current instruction sequence after this execution.
+  [rs] and [rs'] map machine registers to values, respectively
+  before and after instruction execution.  [m] and [m'] are the
+  memory states before and after. *)
+
+Inductive exec_instr:
+      function -> val ->
+      code -> regset -> mem ->
+      code -> regset -> mem -> Prop :=
+  | exec_Mlabel:
+      forall f sp lbl c rs m,
+      exec_instr f sp
+                 (Mlabel lbl :: c) rs m
+                 c rs m
+  | exec_Mgetstack:
+      forall f sp ofs ty dst c rs m v,
+      load_stack m sp ty ofs = Some v ->
+      exec_instr f sp
+                 (Mgetstack ofs ty dst :: c) rs m
+                 c (rs#dst <- v) m
+  | exec_Msetstack:
+      forall f sp src ofs ty c rs m m',
+      store_stack m sp ty ofs (rs src) = Some m' ->
+      exec_instr f sp
+                 (Msetstack src ofs ty :: c) rs m
+                 c rs m'
+  | exec_Mgetparam:
+      forall f sp parent ofs ty dst c rs m v,
+      load_stack m sp Tint (Int.repr 0) = Some parent ->
+      load_stack m parent ty ofs = Some v ->
+      exec_instr f sp
+                 (Mgetparam ofs ty dst :: c) rs m
+                 c (rs#dst <- v) m
+  | exec_Mop:
+      forall f sp op args res c rs m v,
+      eval_operation ge sp op rs##args = Some v ->
+      exec_instr f sp
+                 (Mop op args res :: c) rs m
+                 c (rs#res <- v) m
+  | exec_Mload:
+      forall f sp chunk addr args dst c rs m a v,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.loadv chunk m a = Some v ->
+      exec_instr f sp 
+                 (Mload chunk addr args dst :: c) rs m
+                 c (rs#dst <- v) m
+  | exec_Mstore:
+      forall f sp chunk addr args src c rs m m' a,
+      eval_addressing ge sp addr rs##args = Some a ->
+      Mem.storev chunk m a (rs src) = Some m' ->
+      exec_instr f sp
+                 (Mstore chunk addr args src :: c) rs m
+                 c rs m'
+  | exec_Mcall:
+      forall f sp sig ros c rs m f' rs' m',
+      find_function ros rs = Some f' ->
+      exec_function f' sp rs m rs' m' ->
+      exec_instr f sp
+                 (Mcall sig ros :: c) rs m
+                 c rs' m'
+  | exec_Mgoto:
+      forall f sp lbl c rs m c',
+      find_label lbl f.(fn_code) = Some c' ->
+      exec_instr f sp
+                 (Mgoto lbl :: c) rs m
+                 c' rs m
+  | exec_Mcond_true:
+      forall f sp cond args lbl c rs m c',
+      eval_condition cond rs##args = Some true ->
+      find_label lbl f.(fn_code) = Some c' ->
+      exec_instr f sp
+                 (Mcond cond args lbl :: c) rs m
+                 c' rs m
+  | exec_Mcond_false:
+      forall f sp cond args lbl c rs m,
+      eval_condition cond rs##args = Some false ->
+      exec_instr f sp
+                 (Mcond cond args lbl :: c) rs m
+                 c rs m
+
+with exec_instrs:
+      function -> val ->
+      code -> regset -> mem ->
+      code -> regset -> mem -> Prop :=
+  | exec_refl:
+      forall f sp c rs m,
+      exec_instrs f sp  c rs m  c rs m
+  | exec_one:
+      forall f sp c rs m c' rs' m',
+      exec_instr f sp c rs m  c' rs' m' ->
+      exec_instrs f sp c rs m  c' rs' m'
+  | exec_trans:
+      forall f sp c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
+      exec_instrs f sp  c1 rs1 m1  c2 rs2 m2 ->
+      exec_instrs f sp  c2 rs2 m2  c3 rs3 m3 ->
+      exec_instrs f sp  c1 rs1 m1  c3 rs3 m3
+
+(** In addition to reserving the word at offset 0 in the activation 
+  record for maintaining the linking of activation records,
+  we need to reserve the word at offset 4 to store the return address
+  into the caller.  However, the return address (a pointer within
+  the code of the caller) is not precisely known at this point:
+  it will be determined only after the final translation to PowerPC
+  assembly code.  Therefore, we simply reserve that word in the strongest
+  sense of the word ``reserve'': we make sure that whatever pointer
+  is stored there at function entry keeps the same value until the
+  final return instruction, and that the return value and final memory
+  state are the same regardless of the return address.  
+  This is captured in the evaluation rule [exec_function]
+  that quantifies universally over all possible values of the return
+  address, and pass this value to [exec_function_body].  In other
+  terms, the inference rule [exec_function] has an infinity of
+  premises, one for each possible return address.  Such infinitely
+  branching inference rules are uncommon in operational semantics,
+  but cause no difficulties in Coq. *)
+
+with exec_function_body:
+      function -> val -> val ->
+      regset -> mem -> regset -> mem -> Prop :=
+  | exec_funct_body:
+      forall f parent ra rs m rs' m1 m2 m3 m4 stk c,
+      Mem.alloc m (- f.(fn_framesize))
+                  (align_16_top (- f.(fn_framesize)) f.(fn_stacksize))
+                                                        = (m1, stk) ->
+      let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in
+      store_stack m1 sp Tint (Int.repr 0) parent = Some m2 ->
+      store_stack m2 sp Tint (Int.repr 4) ra = Some m3 ->
+      exec_instrs f sp
+                  f.(fn_code) rs m3
+                 (Mreturn :: c) rs' m4 ->
+      load_stack m4 sp Tint (Int.repr 0) = Some parent ->
+      load_stack m4 sp Tint (Int.repr 4) = Some ra ->
+      exec_function_body f parent ra rs m rs' (Mem.free m4 stk)
+
+with exec_function:
+      function -> val -> regset -> mem -> regset -> mem -> Prop :=
+  | exec_funct:
+      forall f parent rs m rs' m',
+      (forall ra,
+         Val.has_type ra Tint ->
+         exec_function_body f parent ra rs m rs' m') ->
+      exec_function f parent rs m rs' m'.
+
+Scheme exec_instr_ind4 := Minimality for exec_instr Sort Prop
+  with exec_instrs_ind4 := Minimality for exec_instrs Sort Prop
+  with exec_function_body_ind4 := Minimality for exec_function_body Sort Prop
+  with exec_function_ind4 := Minimality for exec_function Sort Prop.
+
+End RELSEM.
+
+Definition exec_program (p: program) (r: val) : Prop :=
+  let ge := Genv.globalenv p in
+  let m0 := Genv.init_mem p in
+  exists b, exists f, exists rs, exists m,
+  Genv.find_symbol ge p.(prog_main) = Some b /\
+  Genv.find_funct_ptr ge b = Some f /\
+  exec_function ge f (Vptr Mem.nullptr Int.zero) (Regmap.init Vundef) m0 rs m /\
+  rs R3 = r.
+