diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-02 18:31:46 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-02 18:31:46 +0100 |
| commit | 4df03aaf5204d2f15885b49fe3f5c9cb61b4596d (patch) | |
| tree | 89632035ea7de134700af303805fd4f4666ba494 /riscV/ValueAOp.v | |
| parent | 3e47c1b17e8ff03400106a80117eb86d7e7f9da6 (diff) | |
| download | compcert-kvx-4df03aaf5204d2f15885b49fe3f5c9cb61b4596d.tar.gz compcert-kvx-4df03aaf5204d2f15885b49fe3f5c9cb61b4596d.zip | |
Ccompu expansion
Diffstat (limited to 'riscV/ValueAOp.v')
| -rw-r--r-- | riscV/ValueAOp.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index ec4492ff..4c1f4625 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -149,7 +149,9 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32) | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32) + | OEsltuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) + | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => I (Int.shl n (Int.repr 12)) | OEaddiwr0 n, nil => add (I n) zero32 @@ -218,7 +220,7 @@ Proof. Qed. Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m, - c = Ceq \/ c = Cne -> + c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc (Op.apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) @@ -253,9 +255,10 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - 1,2: apply eval_cmpu_sound; auto. + 1,2,4: apply eval_cmpu_sound; auto. apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. + unfold Val.cmpu; apply of_optbool_sound; eauto with va. unfold zero32; simpl. eauto with va. Qed. |