From 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 9 Feb 2006 14:55:48 +0000 Subject: Initial import of compcert git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Mach.v | 295 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 295 insertions(+) create mode 100644 backend/Mach.v (limited to 'backend/Mach.v') 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. + -- cgit