diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 10:31:56 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-20 10:31:56 +0200 |
| commit | aa25ec270b651186154523ec71a3888b50994d70 (patch) | |
| tree | a4572adf5cde4f97642885cb1f90f73a20d169cd /mppa_k1c/Asm.v | |
| parent | 41a048fa4bb9ddefd4e4acff2207251bb3ddbf06 (diff) | |
| download | compcert-kvx-aa25ec270b651186154523ec71a3888b50994d70.tar.gz compcert-kvx-aa25ec270b651186154523ec71a3888b50994d70.zip | |
MPPA - Oshrximm + Mgetparam + FP is GPR10 + bug
Added Oshrximm and Mgetparam -> mmult.c divide & conqueer generates
FP is now GPR10 instead of being a mix of GPR30 and GPR32
Corrected a bug where Pgoto and Pj_l were given the same interpretation,
where in fact there's a fundamental difference : Pgoto is supposed to
have a function name (symbol), while Pj_l is supposed to have a label
name (print_label). This led to having undefinite labels in the code.
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index f8ab1e8d..d199495b 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -92,6 +92,7 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]). *) Notation "'SP'" := GPR12 (only parsing) : asm. +Notation "'FP'" := GPR10 (only parsing) : asm. Notation "'RTMP'" := GPR31 (only parsing) : asm. Inductive btest: Type := @@ -1008,7 +1009,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out let sp := (Vptr stk Ptrofs.zero) in match Mem.storev Mptr m1 (Val.offset_ptr sp pos) rs#SP with | None => Stuck - | Some m2 => Next (nextinstr (rs #GPR32 <- (rs SP) #SP <- sp #GPR31 <- Vundef)) m2 + | Some m2 => Next (nextinstr (rs #FP <- (rs SP) #SP <- sp #GPR31 <- Vundef)) m2 end | Pfreeframe sz pos => match Mem.loadv Mptr m (Val.offset_ptr rs#SP pos) with @@ -1082,7 +1083,7 @@ Definition preg_of (r: mreg) : preg := match r with | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4 | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R9 => GPR9 -(*| R10 => GPR10 | R11 => GPR11 | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *) + | R10 => GPR10 (*| R11 => GPR11 | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *) | R15 => GPR15 | R16 => GPR16 | R17 => GPR17 | R18 => GPR18 | R19 => GPR19 | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 |