From 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 3 Feb 2021 17:14:23 +0100 Subject: All Ocmp expanded in RTL --- riscV/ValueAOp.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'riscV/ValueAOp.v') diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 9218d80d..4880a929 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -166,6 +166,12 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEluil n, nil => L (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) + | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) + | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) + | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) + | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2) + | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2) + | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2) | _, _ => Vbot end. @@ -317,6 +323,7 @@ Proof. unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. unfold zero64; simpl. eauto with va. + all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. End SOUNDNESS. -- cgit