diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:44:56 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:44:56 +0200 |
| commit | 98206d8c97cf9ecdff8d892ecafb9a9fa8455f74 (patch) | |
| tree | 5d05d5a2907de5152c4566c1a172734c6a8ab651 /mppa_k1c | |
| parent | 9f256a4ad30c93749e6c1192a84f996feac3b023 (diff) | |
| download | compcert-kvx-98206d8c97cf9ecdff8d892ecafb9a9fa8455f74.tar.gz compcert-kvx-98206d8c97cf9ecdff8d892ecafb9a9fa8455f74.zip | |
fix slow globals etc.
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/ConstpropOp.vp | 2 | ||||
| -rw-r--r-- | mppa_k1c/ConstpropOpproof.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/ConstpropOp.vp b/mppa_k1c/ConstpropOp.vp index aab2424d..b5128357 100644 --- a/mppa_k1c/ConstpropOp.vp +++ b/mppa_k1c/ConstpropOp.vp @@ -298,7 +298,7 @@ Nondetfunction addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => - if Archi.pic_code tt + if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt))) then (addr, args) else (Aglobal symb (Ptrofs.add n1 n), nil) | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v index b6c73281..ae11a220 100644 --- a/mppa_k1c/ConstpropOpproof.v +++ b/mppa_k1c/ConstpropOpproof.v @@ -730,7 +730,7 @@ Proof. intros until res. unfold addr_strength_reduction. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). -- destruct (Archi.pic_code tt). +- destruct (orb _ _). + exists (Val.offset_ptr e#r1 n); auto. + simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. inv H0; simpl; auto. |