Ccomp for long

1 files changed, 57 insertions, 0 deletions

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 4c1f4625..9218d80d 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -18,6 +18,7 @@ Require Import Zbits.
 (** Value analysis for RISC V operators *)
 
 Definition zero32 := (I Int.zero).
+Definition zero64 := (L Int64.zero).
   
 Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 vz: aval): B :=
   match optR0 with
@@ -155,6 +156,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | 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
+  | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64)
+  | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64)
+  | OEsltl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64)
+  | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64)
+  | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
+  | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
+  | OExoril n, v1::nil => xorl v1 (L n)
+  | 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)
   | _, _ => Vbot
   end.
 
@@ -219,6 +230,20 @@ Proof.
   rewrite Ptrofs.add_zero_l; eauto with va.
 Qed.
 
+Lemma of_optbool_maketotal_sound:
+  forall ob ab, cmatch ob ab -> vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (of_optbool ab).
+Proof.
+  intros.
+  assert (DEFAULT: vmatch bc (Val.maketotal (option_map Val.of_bool ob)) (Uns Pbot 1)).
+  {
+    destruct ob; simpl; auto with va.
+    destruct b; constructor; try omega.
+    change 1 with (usize Int.one). apply is_uns_usize.
+    red; intros. apply Int.bits_zero.
+  }
+  inv H; auto. simpl. destruct b; constructor.
+Qed.
+
 Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m,
   c = Ceq \/ c = Cne \/ c = Clt->
   vmatch bc a1 b1 ->
@@ -231,6 +256,21 @@ Proof.
   apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
 Qed.
 
+Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR0 m,
+  c = Ceq \/ c = Cne \/ c = Clt->
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc
+    (Val.maketotal
+       (Op.apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) c) a1 a0
+          Op.zero64))
+    (of_optbool (apply_bin_r0 optR0 (cmplu_bool c) b1 b0 zero64)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va.
+Qed.
+
 Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0,
   vmatch bc a1 b1 ->
   vmatch bc a0 b0 ->
@@ -242,6 +282,18 @@ Proof.
   apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va.
 Qed.
 
+Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0,
+  vmatch bc a1 b1 ->
+  vmatch bc a0 b0 ->
+  vmatch bc
+    (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl Clt) a1 a0 Op.zero64))
+    (of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) b1 b0 zero64)).
+Proof.
+  intros.
+  destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0;
+  apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va.
+Qed.
+
 Theorem eval_static_operation_sound:
   forall op vargs m vres aargs,
   eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
@@ -260,6 +312,11 @@ Proof.
   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.
+  1,2,4: apply eval_cmplu_sound; auto.
+  apply eval_cmpl_sound; auto.
+  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.
 Qed.
 
 End SOUNDNESS.