diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-11 09:30:51 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-11 09:30:51 +0100 |
| commit | 4d1e02eb67a027d968979ed37f9d90426c634ccd (patch) | |
| tree | 6e493a4ce7772095023572920221cf23ff4a27f6 /ia32 | |
| parent | 866e612bf63568cbe9871bb1d6724323493651e7 (diff) | |
| download | compcert-4d1e02eb67a027d968979ed37f9d90426c634ccd.tar.gz compcert-4d1e02eb67a027d968979ed37f9d90426c634ccd.zip | |
Prevent constant propagation on Oindirectsymbol addresses.
(Otherwise they are turned into Oaddrsymbol or global addressing modes,
causing linking issues on MacOS X.)
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/ValueAOp.v | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 874c2be3..53013337 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -58,7 +58,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop - | Oindirectsymbol id, nil => Ptr (Gl id Int.zero) + | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero) | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast8unsigned, v1 :: nil => zero_ext 8 v1 | Ocast16signed, v1 :: nil => sign_ext 16 v1 @@ -145,7 +145,16 @@ Proof. intros; apply symbol_address_sound; apply GENV. Qed. -Hint Resolve symbol_address_sound: va. +Lemma symbol_address_sound_2: + forall id ofs, + vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. + constructor. constructor. apply GENV; auto. + constructor. +Qed. + +Hint Resolve symbol_address_sound symbol_address_sound_2: va. Ltac InvHyps := match goal with |