Commit 8fa87b09 authored by David Monniaux's avatar David Monniaux
Browse files

fix kvx

parent 4d70347a
Pipeline #56417 waiting for manual action with stage
......@@ -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 =>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment