diff options
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 45 |
1 files changed, 25 insertions, 20 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ade84e7b..36269954 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -28,6 +28,8 @@ Require Import Chunks. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Import PArithCoercions. + (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler, mostly that argument and result registers are of the correct @@ -912,12 +914,12 @@ end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (PLoadRRO Plw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO Pld rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO Pfls rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO Pfld rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO Plw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO Pld_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Plw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pld rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pfls rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pfld rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Plw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO TRAP Pld_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.loadind") end. @@ -933,7 +935,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) end. Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) := - indexed_memory_access (PLoadRRO Pld dst) base ofs. + indexed_memory_access (PLoadRRO TRAP Pld dst) base ofs. Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := indexed_memory_access (PStoreRRO Psd src) base ofs. @@ -993,27 +995,28 @@ Definition chunk2load (chunk: memory_chunk) := | Many64 => Pld_a end. -Definition transl_load_rro (chunk: memory_chunk) (addr: addressing) +Definition transl_load_rro (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access (PLoadRRO (chunk2load chunk) r) addr args k. + transl_memory_access (PLoadRRO trap (chunk2load chunk) r) addr args k. -Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) +Definition transl_load_rrr (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k. + transl_memory_access2 (PLoadRRR trap (chunk2load chunk) r) addr args k. -Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z) +Definition transl_load_rrrXS (trap: trapping_mode) (chunk: memory_chunk) (scale : Z) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k. + transl_memory_access2XS chunk (PLoadRRRXS trap (chunk2load chunk) r) scale args k. -Definition transl_load (chunk: memory_chunk) (addr: addressing) +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := match addr with - | Aindexed2XS scale => transl_load_rrrXS chunk scale args dst k - | Aindexed2 => transl_load_rrr chunk addr args dst k - | _ => transl_load_rro chunk addr args dst k + | Aindexed2XS scale => transl_load_rrrXS trap chunk scale args dst k + | Aindexed2 => transl_load_rrr trap chunk addr args dst k + | _ => transl_load_rro trap chunk addr args dst k end. Definition chunk2store (chunk: memory_chunk) := @@ -1073,8 +1076,8 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c) | MBop op args res => transl_op op args res k - | MBload chunk addr args dst => - transl_load chunk addr args dst k + | MBload trap chunk addr args dst => + transl_load trap chunk addr args dst k | MBstore chunk addr args src => transl_store chunk addr args src k end. @@ -1111,10 +1114,12 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := match i with + | MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP) | MBsetstack src ofs ty => before | MBgetparam ofs ty dst => negb (mreg_eq dst MFP) | MBop op args res => before && negb (mreg_eq res MFP) - | _ => false + | MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst MFP) + | MBstore chunk addr args res => before end. (** This is the naive definition, which is not tail-recursive unlike the other backends *) |