diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-05-17 15:00:55 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-05-17 15:00:55 +0200 |
commit | 7a44249f8256058156053fd56ceb3dbf63426bbe (patch) | |
tree | dbf310cbe43e91f10248d0496a93d6defa36c6e6 /x86/Op.v | |
parent | 7eaaa6aee670b06c427017a9af888d3469e53126 (diff) | |
download | compcert-7a44249f8256058156053fd56ceb3dbf63426bbe.tar.gz compcert-7a44249f8256058156053fd56ceb3dbf63426bbe.zip |
Issues with invalid x86 addressing modes (Github issue #183)
- x86/Op: in 32-bit mode all addressings are valid because offsets are always interpreted as 32-bit signed integers in Asmgen.
- x86/ConstpropOp: in addr_strength_reduction, make sure no invalid addressing mode is generated.
Diffstat (limited to 'x86/Op.v')
-rw-r--r-- | x86/Op.v | 33 |
1 files changed, 19 insertions, 14 deletions
@@ -196,24 +196,29 @@ Defined. Global Opaque eq_condition eq_addressing eq_operation. -(** In addressing modes, offsets are 32-bit signed integers, even in 64-bit mode. - The following function checks that an addressing mode is valid, i.e. that - the offsets are in range. *) +(** In addressing modes, offsets are 32-bit signed integers, even in + 64-bit mode. The following function checks that an addressing + mode is valid, i.e. that the offsets are in range. + The check always succeeds in 32-bit mode because offsets are + always 32-bit integers and are normalized as 32-bit signed integers + during code generation (see [Asmgen.normalize_addrmode_32]). *) Definition offset_in_range (n: Z) : bool := zle Int.min_signed n && zle n Int.max_signed. Definition addressing_valid (a: addressing) : bool := - match a with - | Aindexed n => offset_in_range n - | Aindexed2 n => offset_in_range n - | Ascaled sc ofs => offset_in_range ofs - | Aindexed2scaled sc ofs => offset_in_range ofs - | Aglobal s ofs => true - | Abased s ofs => true - | Abasedscaled sc s ofs => true - | Ainstack ofs => offset_in_range (Ptrofs.signed ofs) - end. - + if Archi.ptr64 then + match a with + | Aindexed n => offset_in_range n + | Aindexed2 n => offset_in_range n + | Ascaled sc ofs => offset_in_range ofs + | Aindexed2scaled sc ofs => offset_in_range ofs + | Aglobal s ofs => true + | Abased s ofs => true + | Abasedscaled sc s ofs => true + | Ainstack ofs => offset_in_range (Ptrofs.signed ofs) + end + else true. + (** * Evaluation functions *) (** Evaluation of conditions, operators and addressing modes applied |