diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-02-04 17:27:33 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-02-08 17:11:46 +0100 |
| commit | 14aad5e8f330423427e63265dcb9bff45a3f55f3 (patch) | |
| tree | 6bb84e8abfd2a8dced23388e712f909cda0cc16f /x86 | |
| parent | de0ff0bcb9df3dba542d22336e58e70ba8bda947 (diff) | |
| download | compcert-kvx-14aad5e8f330423427e63265dcb9bff45a3f55f3.tar.gz compcert-kvx-14aad5e8f330423427e63265dcb9bff45a3f55f3.zip | |
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.
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/ConstpropOp.vp | 10 | ||||
| -rw-r--r-- | x86/ConstpropOpproof.v | 15 |
2 files changed, 15 insertions, 10 deletions
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 diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v index e82c2963..5d79de6c 100644 --- a/x86/ConstpropOpproof.v +++ b/x86/ConstpropOpproof.v @@ -291,11 +291,16 @@ Lemma addr_strength_reduction_correct: let (addr', args') := addr_strength_reduction addr args vl in exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' e##args' = Some res' /\ Val.lessdef res res'. Proof. - unfold eval_addressing, addr_strength_reduction. destruct Archi.ptr64. -- intros until res. destruct (addressing_valid (fst (addr_strength_reduction_64 addr args vl))). - apply addr_strength_reduction_64_correct. - intros; exists res; auto. -- apply addr_strength_reduction_32_correct. + intros until res. unfold addr_strength_reduction. + set (aa := if Archi.ptr64 + then addr_strength_reduction_64 addr args vl + else addr_strength_reduction_32 addr args vl). + intros. + destruct (addressing_valid (fst aa)). +- unfold aa, eval_addressing in *. destruct Archi.ptr64. ++ apply addr_strength_reduction_64_correct; auto. ++ apply addr_strength_reduction_32_correct; auto. +- exists res; auto. Qed. Lemma make_cmp_base_correct: |