diff options
Diffstat (limited to 'backend/Machconcr.v')
| -rw-r--r-- | backend/Machconcr.v | 250 |
1 files changed, 250 insertions, 0 deletions
diff --git a/backend/Machconcr.v b/backend/Machconcr.v new file mode 100644 index 00000000..fe9a7d90 --- /dev/null +++ b/backend/Machconcr.v @@ -0,0 +1,250 @@ +(** The Mach intermediate language: concrete semantics. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Conventions. +Require Import Mach. +Require PPCgenretaddr. + +(** In the concrete semantics for Mach, 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. + +In addition to this linking of activation records, the concrete +semantics also make provisions for storing a return address +at offset 12 from the stack pointer. This stack location will +be used by the PPC code generated by [PPCgen] to save the return +address into the caller at the beginning of a function, then restore +it and jump to it at the end of a function. The Mach concrete +semantics does not attach any particular meaning to the pointer +stored in this reserved location, but makes sure that it is preserved +during execution of a function. The [return_address_offset] predicate +from module [PPCgenretaddr] is used to guess the value of the return +address that the PPC code generated later will store in the +reserved location. +*) + +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. + +(** Extract the values of the arguments of an external call. *) + +Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := + | extcall_arg_reg: forall rs m sp r, + extcall_arg rs m sp (R r) (rs r) + | extcall_arg_stack: forall rs m sp ofs ty v, + load_stack m sp ty (Int.repr (4 * ofs)) = Some v -> + extcall_arg rs m sp (S (Outgoing ofs ty)) v. + +Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := + | extcall_args_nil: forall rs m sp, + extcall_args rs m sp nil nil + | extcall_args_cons: forall rs m sp l1 ll v1 vl, + extcall_arg rs m sp l1 v1 -> extcall_args rs m sp ll vl -> + extcall_args rs m sp (l1 :: ll) (v1 :: vl). + +Definition extcall_arguments + (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := + extcall_args rs m sp (Conventions.loc_arguments sg) args. + +(** The components of an execution state are: + +- [State cs f sp c rs m]: [f] is the block reference corresponding + to the function currently executing. [sp] is the stack pointer. + [c] is the list of instructions that remain to be executed. + [rs] assigns values to registers. [m] is the memory state. +- [Callstate cs f rs m]: [f] is the block reference corresponding + to the function being called. [rs] is the current values of registers, + and [m] the current memory state. +- [Returnstate cs rs m]: [rs] is the current values of registers, + and [m] the current memory state. + +[cs] is a list of stack frames [Stackframe f sp retaddr c], +where [f] is the block reference for the calling function, +[c] the code within this function that follows the call instruction, +[sp] its stack pointer, and [retaddr] the return address predicted +by [PPCgenretaddr.return_address_offset]. +*) + +Inductive stackframe: Set := + | Stackframe: + forall (f: block) (sp retaddr: val) (c: code), + stackframe. + +Inductive state: Set := + | State: + forall (stack: list stackframe) (f: block) (sp: val) + (c: code) (rs: regset) (m: mem), + state + | Callstate: + forall (stack: list stackframe) (f: block) (rs: regset) (m: mem), + state + | Returnstate: + forall (stack: list stackframe) (rs: regset) (m: mem), + state. + +Definition parent_sp (s: list stackframe) : val := + match s with + | nil => Vptr Mem.nullptr Int.zero + | Stackframe f sp ra c :: s' => sp + end. + +Definition parent_ra (s: list stackframe) : val := + match s with + | nil => Vzero + | Stackframe f sp ra c :: s' => ra + end. + +Section RELSEM. + +Variable ge: genv. + +Inductive step: state -> trace -> state -> Prop := + | exec_Mlabel: + forall s f sp lbl c rs m, + step (State s f sp (Mlabel lbl :: c) rs m) + E0 (State s f sp c rs m) + | exec_Mgetstack: + forall s f sp ofs ty dst c rs m v, + load_stack m sp ty ofs = Some v -> + step (State s f sp (Mgetstack ofs ty dst :: c) rs m) + E0 (State s f sp c (rs#dst <- v) m) + | exec_Msetstack: + forall s f sp src ofs ty c rs m m', + store_stack m sp ty ofs (rs src) = Some m' -> + step (State s f sp (Msetstack src ofs ty :: c) rs m) + E0 (State s f sp c rs m') + | exec_Mgetparam: + forall s 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 -> + step (State s f sp (Mgetparam ofs ty dst :: c) rs m) + E0 (State s f sp c (rs#dst <- v) m) + | exec_Mop: + forall s f sp op args res c rs m v, + eval_operation ge sp op rs##args m = Some v -> + step (State s f sp (Mop op args res :: c) rs m) + E0 (State s f sp c (rs#res <- v) m) + | exec_Mload: + forall s 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 -> + step (State s f sp (Mload chunk addr args dst :: c) rs m) + E0 (State s f sp c (rs#dst <- v) m) + | exec_Mstore: + forall s 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' -> + step (State s f sp (Mstore chunk addr args src :: c) rs m) + E0 (State s f sp c rs m') + | exec_Mcall: + forall s fb sp sig ros c rs m f f' ra, + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + PPCgenretaddr.return_address_offset f c ra -> + step (State s fb sp (Mcall sig ros :: c) rs m) + E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) + f' rs m) + | exec_Mtailcall: + forall s fb stk soff sig ros c rs m f', + find_function_ptr ge ros rs = Some f' -> + load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> + step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) + E0 (Callstate s f' rs (Mem.free m stk)) + | exec_Malloc: + forall s f sp c rs m sz m' blk, + rs (Conventions.loc_alloc_argument) = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', blk) -> + step (State s f sp (Malloc :: c) rs m) + E0 (State s f sp c + (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero)) + m') + | exec_Mgoto: + forall s fb f sp lbl c rs m c', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + step (State s fb sp (Mgoto lbl :: c) rs m) + E0 (State s fb sp c' rs m) + | exec_Mcond_true: + forall s fb f sp cond args lbl c rs m c', + eval_condition cond rs##args m = Some true -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + step (State s fb sp (Mcond cond args lbl :: c) rs m) + E0 (State s fb sp c' rs m) + | exec_Mcond_false: + forall s f sp cond args lbl c rs m, + eval_condition cond rs##args m = Some false -> + step (State s f sp (Mcond cond args lbl :: c) rs m) + E0 (State s f sp c rs m) + | exec_Mreturn: + forall s f stk soff c rs m, + load_stack m (Vptr stk soff) Tint (Int.repr 0) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint (Int.repr 12) = Some (parent_ra s) -> + step (State s f (Vptr stk soff) (Mreturn :: c) rs m) + E0 (Returnstate s rs (Mem.free m stk)) + | exec_function_internal: + forall s fb rs m f m1 m2 m3 stk, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + 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_sp s) = Some m2 -> + store_stack m2 sp Tint (Int.repr 12) (parent_ra s) = Some m3 -> + step (Callstate s fb rs m) + E0 (State s fb sp f.(fn_code) rs m3) + | exec_function_external: + forall s fb rs m t rs' ef args res, + Genv.find_funct_ptr ge fb = Some (External ef) -> + event_match ef args t res -> + extcall_arguments rs m (parent_sp s) ef.(ef_sig) args -> + rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) -> + step (Callstate s fb rs m) + t (Returnstate s rs' m) + | exec_return: + forall s f sp ra c rs m, + step (Returnstate (Stackframe f sp ra c :: s) rs m) + E0 (State s f sp c rs m). + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall fb, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some fb -> + initial_state p (Callstate nil fb (Regmap.init Vundef) m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r, + rs R3 = Vint r -> + final_state (Returnstate nil rs m) r. + +Definition exec_program (p: program) (beh: program_behavior) : Prop := + program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. |