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/ConstpropOp.vp | |
| 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/ConstpropOp.vp')
| -rw-r--r-- | x86/ConstpropOp.vp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp index 759d7c16..f0000a85 100644 --- a/x86/ConstpropOp.vp +++ b/x86/ConstpropOp.vp @@ -192,9 +192,11 @@ Nondetfunction addr_strength_reduction_64 Definition addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := - if Archi.ptr64 - then addr_strength_reduction_64 addr args vl - else addr_strength_reduction_32 addr args vl. + if Archi.ptr64 then + let addr_args' := addr_strength_reduction_64 addr args vl in + if addressing_valid (fst addr_args') then addr_args' else (addr, args) + else + addr_strength_reduction_32 addr args vl. Definition make_addimm (n: int) (r: reg) := if Int.eq n Int.zero |