diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 09:49:58 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 09:49:58 +0200 |
| commit | f2831013b46d0486e5e134f26fde9ece7b78ff93 (patch) | |
| tree | 9baa6452b44cb21e471e589a011c324d816bae44 /x86/Asmgen.v | |
| parent | 75109076ec027675e297ff1273660fc6b5a5f239 (diff) | |
| download | compcert-kvx-f2831013b46d0486e5e134f26fde9ece7b78ff93.tar.gz compcert-kvx-f2831013b46d0486e5e134f26fde9ece7b78ff93.zip | |
more for passing notrap through x86
Diffstat (limited to 'x86/Asmgen.v')
| -rw-r--r-- | x86/Asmgen.v | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/x86/Asmgen.v b/x86/Asmgen.v index 73e3263e..99e9fc2b 100644 --- a/x86/Asmgen.v +++ b/x86/Asmgen.v @@ -636,9 +636,14 @@ Definition transl_op (** Translation of memory loads and stores *) -Definition transl_load (chunk: memory_chunk) +Definition transl_load + (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dest: mreg) (k: code) : res code := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load x86 does not support non trapping loads") + | TRAP => do am <- transl_addressing addr args; match chunk with | Mint8unsigned => @@ -659,6 +664,7 @@ Definition transl_load (chunk: memory_chunk) do r <- freg_of dest; OK(Pmovsd_fm r am :: k) | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) @@ -699,8 +705,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) loadind RSP f.(fn_link_ofs) Tptr AX k1) | 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 reg) => |