Module Mach



The Mach intermediate language: abstract syntax. Mach is the last intermediate language before generation of assembly code. This file defines the abstract syntax for Mach; two dynamic semantics are given in modules Machabstr and Machconcr.

Require Import Coqlib.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Pointers.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Conventions.

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 Lgetstack and Lsetstack instructions of Linear: actual offsets are used instead of abstract stack slots, and the distinction between the caller's frame and the callee's frame is made explicit.

Definition label := positive.

Inductive instruction: Type :=
  | 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
  | Mthreadcreate: instruction
  | Matomic: atomic_statement -> list mreg -> mreg -> instruction
  | Mfence: instruction.

Definition code := list instruction.

Record function: Type := mkfunction
  { fn_sig: signature;
    fn_code: code;
    fn_paddedstacksize : Z;
    fn_stacksize: int ;
    fn_framesize: Z
  }.

Definition fundef := Ast.fundef function.

Definition program := Ast.program fundef unit.

Definition funsig (fd: fundef) :=
  match fd with
  | Internal f => f.(fn_sig)
  | External ef => ef.(ef_sig)
  end.

Definition genv := Genv.t fundef.

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 mreg _ a b) (at level 1).
Notation "a # b <- c" := (Regmap.set (b : mreg) c a) (at level 1, b at next level).

Fixpoint undef_regs (rl: list mreg) (rs: regset) {struct rl} : regset :=
  match rl with
  | nil => rs
  | r1 :: rl' => undef_regs rl' (Regmap.set r1 Vundef rs)
  end.

Definition undef_temps (rs: regset) :=
  undef_regs (int_temporaries ++ float_temporaries) rs.

Definition undef_op (op: operation) (rs: regset) :=
  match op with
  | Omove => rs
  | _ => undef_temps rs
  end.

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.

Lemma find_label_incl:
  forall lbl c c', find_label lbl c = Some c' -> incl c' c.
Proof.
  induction c; simpl; intros. discriminate.
  destruct (is_label lbl a). inv H. auto with coqlib. eauto with coqlib.
Qed.

Definition find_function_ptr
        (ge: genv) (ros: mreg + ident) (rs: regset) : option pointer :=
  match ros with
  | inl r =>
      match rs r with
      | Vptr p => Some p
      | _ => None
      end
  | inr symb =>
      Genv.find_symbol ge symb
  end.
Generated by coq2html