From 4df03aaf5204d2f15885b49fe3f5c9cb61b4596d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Feb 2021 18:31:46 +0100 Subject: Ccompu expansion --- riscV/ValueAOp.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'riscV/ValueAOp.v') 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. -- cgit