diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 17:14:23 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 17:14:23 +0100 |
| commit | 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 (patch) | |
| tree | 673c5cdb7b99756c4c6880e7ef0b14bed7544bc2 /riscV/ValueAOp.v | |
| parent | 7f8ccba038ce9bf7665341c05b89bb5d9b9b536b (diff) | |
| download | compcert-kvx-29ba37cc21cedc09b20bbd8adfa0ec52c48365c0.tar.gz compcert-kvx-29ba37cc21cedc09b20bbd8adfa0ec52c48365c0.zip | |
All Ocmp expanded in RTL
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. |