From 35febfa5b231a71234a1b32c128169352e96eaca Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 7 Sep 2019 12:27:43 +0200 Subject: fixes for ARM --- arm/Asmgen.v | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) (limited to 'arm/Asmgen.v') diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 1a1e7f2f..016a1c5a 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -689,8 +689,12 @@ Definition transl_memory_access_float None mk_immed addr args k. -Definition transl_load (chunk: memory_chunk) (addr: addressing) - (args: list mreg) (dst: mreg) (k: code) := +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) + (args: list mreg) (dst: mreg) (k: code) := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm") + | TRAP => match chunk with | Mint8signed => transl_memory_access_int Pldrsb mk_immed_mem_small dst addr args k @@ -708,6 +712,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -747,8 +752,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_int IR13 f.(fn_link_ofs) IR12 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 arg) => -- cgit