diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-09 14:51:52 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-09 14:51:52 +0100 |
| commit | 37de1399449067121a8bb9a51a7cc7a043ad17e2 (patch) | |
| tree | 11429171ae1f49b57f8d7f98a09d5ea0511680c0 /aarch64/Asmgen.v | |
| parent | dd1c78c840bf5eb1ad7e101f2da05578245c5998 (diff) | |
| parent | e2c64b54bf5df0927c684a70167378c91cba0ff4 (diff) | |
| download | compcert-kvx-37de1399449067121a8bb9a51a7cc7a043ad17e2.tar.gz compcert-kvx-37de1399449067121a8bb9a51a7cc7a043ad17e2.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-work-upstream-merge
Diffstat (limited to 'aarch64/Asmgen.v')
| -rw-r--r-- | aarch64/Asmgen.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 1c0e41a1..c7332329 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -957,8 +957,12 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) (** Translation of loads and stores *) -Definition transl_load (chunk: memory_chunk) (addr: Op.addressing) +Definition transl_load (trap: trapping_mode) + (chunk: memory_chunk) (addr: Op.addressing) (args: list mreg) (dst: mreg) (k: code) : res code := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64") + | TRAP => match chunk with | Mint8unsigned => do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrb W rd) k @@ -980,6 +984,7 @@ Definition transl_load (chunk: memory_chunk) (addr: Op.addressing) do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k | Many64 => do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k + end end. Definition transl_store (chunk: memory_chunk) (addr: Op.addressing) @@ -1063,8 +1068,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 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) => |