From 8fa87b0930876d4edd9b26519832943b6ddae652 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 10 Jan 2021 20:32:12 +0100 Subject: fix kvx --- kvx/ValueAOpSSA.v | 9 +++++---- 1 file 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 => -- cgit