diff options
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: |