diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-10 20:32:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-10 20:32:12 +0100 |
| commit | 8fa87b0930876d4edd9b26519832943b6ddae652 (patch) | |
| tree | 5ff8ab5ea7410550d293511bcdfbd1c96516b3a3 | |
| parent | 4d70347aaeeb121e2a81c77e9ddbfd4fa3663a31 (diff) | |
| download | compcert-kvx-ssa.tar.gz compcert-kvx-ssa.zip | |
fix kvxv3.8+ssa_aarch64_postpassssa
| -rw-r--r-- | kvx/ValueAOpSSA.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/kvx/ValueAOpSSA.v b/kvx/ValueAOpSSA.v index 9e718621..689ffdc8 100644 --- a/kvx/ValueAOpSSA.v +++ b/kvx/ValueAOpSSA.v @@ -71,7 +71,7 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := | Aindexed2, v1::v2::nil => addl v1 v2 | Aindexed2XS scale, v1::v2::nil => addl v1 (shll v2 (I (Int.repr scale))) | Aglobal s ofs, nil => Ptr (Gl s ofs) - | Ainstack ofs, nil => Ptr (Stk ofs) + | Ainstack ofs, nil => Vtop | _, _ => Vbot end. @@ -164,7 +164,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) - | Oaddrstack ofs, nil => Ptr (Stk ofs) + | Oaddrstack ofs, nil => Vtop | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast16signed, v1 :: nil => sign_ext 16 v1 | Oadd, v1::v2::nil => add v1 v2 @@ -317,7 +317,7 @@ Variable bc: block_classification. Variable ge: genv. Hypothesis GENV: genv_match bc ge. Variable sp: block. -Hypothesis STACK: bc sp = BCstack. +Hypothesis STACK: bc sp <> BCinvalid. Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). @@ -472,6 +472,7 @@ Proof. unfold eval_addressing, eval_static_addressing; intros; destruct addr; InvHyps; eauto with va. rewrite Ptrofs.add_zero_l; eauto with va. + constructor; constructor; auto. Qed. Theorem eval_static_addressing_sound_none: @@ -522,7 +523,7 @@ Proof. destruct op; InvHyps; eauto with va. - destruct (propagate_float_constants tt); constructor. - destruct (propagate_float_constants tt); constructor. - - rewrite Ptrofs.add_zero_l; eauto with va. + - rewrite Ptrofs.add_zero_l; eauto with va. constructor; constructor; auto. - replace(match Val.shl a1 (Vint (int_of_shift1_4 shift)) with | Vint n2 => Vint (Int.add n n2) | Vptr b2 ofs2 => |