From 14aad5e8f330423427e63265dcb9bff45a3f55f3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 4 Feb 2018 17:27:33 +0100 Subject: x86 ConstpropOp.addr_strength_reduction: always check validity of resulting addressing In the original code, the addressing_valid check is skipped if we are in 32 bits, because we know the check is always true. This is correct but not obvious nor future-proof. (In the future we may want to make addressing_valid more strict.) This commit restructures ConstpropOp.addr_strength_reduction so that the addressing_valid check is always performed. --- x86/ConstpropOp.vp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'x86/ConstpropOp.vp') diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp index be0cc09a..59719cf6 100644 --- a/x86/ConstpropOp.vp +++ b/x86/ConstpropOp.vp @@ -192,11 +192,11 @@ Nondetfunction addr_strength_reduction_64 Definition addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := - 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. + let addr_args' := + if Archi.ptr64 + then addr_strength_reduction_64 addr args vl + else addr_strength_reduction_32 addr args vl in + if addressing_valid (fst addr_args') then addr_args' else (addr, args). Definition make_addimm (n: int) (r: reg) := if Int.eq n Int.zero -- cgit