From 54846ce3ee63b8fff66ac5bf27d1c89ac701ed94 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 7 Sep 2019 14:20:34 +0200 Subject: fix for Risc-V --- riscV/Asmgen.v | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'riscV/Asmgen.v') 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) => -- cgit