diff options
Diffstat (limited to 'backend/Machconcr.v')
| -rw-r--r-- | backend/Machconcr.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 5ca3cad7..41216d25 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -25,8 +25,8 @@ Require Import Op. Require Import Locations. Require Conventions. Require Import Mach. -Require Stacking. -Require PPCgenretaddr. +Require Stacklayout. +Require Asmgenretaddr. (** In the concrete semantics for Mach, the three stack-related Mach instructions are interpreted as memory accesses relative to the @@ -45,14 +45,14 @@ In addition to this linking of activation records, the concrete semantics also make provisions for storing a back link at offset [f.(fn_link_ofs)] from the stack pointer, and a return address at offset [f.(fn_retaddr_ofs)]. The latter stack location will be used -by the PPC code generated by [PPCgen] to save the return address into +by the Asm code generated by [Asmgen] 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. +[Asmgenretaddr] is used to guess the value of the return address that +the Asm code generated later will store in the reserved location. *) Definition chunk_of_type (ty: typ) := @@ -70,7 +70,7 @@ 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 (Stacking.fe_ofs_arg + 4 * ofs)) = Some v -> + load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 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 := @@ -90,7 +90,7 @@ Inductive stackframe: Set := | Stackframe: forall (f: block) (**r pointer to calling function *) (sp: val) (**r stack pointer in calling function *) - (retaddr: val) (**r PPC return address in calling function *) + (retaddr: val) (**r Asm return address in calling function *) (c: code), (**r program point in calling function *) stackframe. @@ -174,7 +174,7 @@ Inductive step: state -> trace -> state -> Prop := 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 -> + Asmgenretaddr.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) @@ -252,7 +252,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs R3 = Vint r -> + rs (Conventions.loc_result (mksignature nil (Some Tint))) = Vint r -> final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := |