diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 14:20:34 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 14:20:34 +0200 |
| commit | 54846ce3ee63b8fff66ac5bf27d1c89ac701ed94 (patch) | |
| tree | 305a5d18e95f1513c4d160467786c5527cbb634c /riscV/Asmgen.v | |
| parent | d84a003dc41c1ce572e86f399f5a610a78eda15f (diff) | |
| download | compcert-kvx-54846ce3ee63b8fff66ac5bf27d1c89ac701ed94.tar.gz compcert-kvx-54846ce3ee63b8fff66ac5bf27d1c89ac701ed94.zip | |
fix for Risc-V
Diffstat (limited to 'riscV/Asmgen.v')
| -rw-r--r-- | riscV/Asmgen.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..ecaca7b3 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -770,9 +770,13 @@ Definition transl_memory_access Error(msg "Asmgen.transl_memory_access") end. -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: code) := - match chunk with + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm") + | TRAP => + match chunk with | Mint8signed => do r <- ireg_of dst; transl_memory_access (Plb r) addr args k @@ -799,6 +803,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access (Pfld r) addr args k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -848,8 +853,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_ptr SP f.(fn_link_ofs) X30 c) | Mop op args res => transl_op op args res k - | Mload chunk addr args dst => - transl_load chunk addr args dst k + | Mload trap chunk addr args dst => + transl_load trap chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl r) => |