diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
| commit | acb41b1af6e5e4c933e3be1b17f6e5012eca794d (patch) | |
| tree | db57a6b2543871312a952ffa2e462e35aef674e0 /riscV/ValueAOp.v | |
| parent | 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 (diff) | |
| download | compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.tar.gz compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.zip | |
cond and branches expanded
Diffstat (limited to 'riscV/ValueAOp.v')
| -rw-r--r-- | riscV/ValueAOp.v | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 4880a929..ece28eff 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -41,6 +41,18 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) + | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 + | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32 + | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32 + | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 + | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64 + | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cge) v1 v2 zero64 | _, _ => Bnone end. @@ -194,7 +206,9 @@ Proof. destruct cond; simpl; eauto with va. inv H2. destruct cond; simpl; eauto with va. - destruct cond; auto with va. + 13: destruct cond; simpl; eauto with va. + all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0; + unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. Lemma symbol_address_sound: |