diff options
Diffstat (limited to 'riscV/ValueAOp.v')
-rw-r--r-- | riscV/ValueAOp.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |