diff options
Diffstat (limited to 'x86')
-rw-r--r-- | x86/ConstpropOp.vp | 8 | ||||
-rw-r--r-- | x86/ConstpropOpproof.v | 4 | ||||
-rw-r--r-- | x86/Op.v | 33 |
3 files changed, 27 insertions, 18 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 diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v index 5eb46e34..ce20738c 100644 --- a/x86/ConstpropOpproof.v +++ b/x86/ConstpropOpproof.v @@ -292,8 +292,10 @@ Lemma addr_strength_reduction_correct: 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. - apply addr_strength_reduction_32_correct. + intros; exists res; auto. +- apply addr_strength_reduction_32_correct. Qed. Lemma make_cmp_base_correct: @@ -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 |