update kvx

1 files changed, 16 insertions, 68 deletions

diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 91d119bf..8afe8d07 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -853,58 +853,6 @@ Definition cmpu_for_btest (bt: btest) :=
   end.
 
 
-(* **** a few lemma on comparisons of unsigned (e.g. pointers) *)
-
-Definition Val_cmpu_bool cmp v1 v2: option bool :=
-  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
-
-Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmpu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
-
-Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
-               (Val_cmpu cmp v1 v2).
-Proof.
-  unfold Val.cmpu, Val_cmpu.
-  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob; cbn.
-  - erewrite Val_cmpu_bool_correct; eauto.
-    econstructor.
-  - econstructor.
-Qed.
-
-Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
- := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
-
-Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmplu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
-
-Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
-               (Val_cmplu cmp v1 v2).
-Proof.
-  unfold Val.cmplu, Val_cmplu.
-  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob as [b|]; cbn.
-  - erewrite Val_cmplu_bool_correct; eauto.
-    cbn. econstructor.
-  - econstructor.
-Qed.
-
-
-
 (** **** Comparing integers *)
 Definition compare_int (t: itest) (v1 v2: val): val :=
   match t with
@@ -914,12 +862,12 @@ Definition compare_int (t: itest) (v1 v2: val): val :=
   | ITge  => Val.cmp Cge v1 v2
   | ITle  => Val.cmp Cle v1 v2
   | ITgt  => Val.cmp Cgt v1 v2
-  | ITneu => Val_cmpu Cne v1 v2
-  | ITequ => Val_cmpu Ceq v1 v2
-  | ITltu => Val_cmpu Clt v1 v2
-  | ITgeu => Val_cmpu Cge v1 v2
-  | ITleu => Val_cmpu Cle v1 v2
-  | ITgtu => Val_cmpu Cgt v1 v2
+  | ITneu => Val.mxcmpu Cne v1 v2
+  | ITequ => Val.mxcmpu Ceq v1 v2
+  | ITltu => Val.mxcmpu Clt v1 v2
+  | ITgeu => Val.mxcmpu Cge v1 v2
+  | ITleu => Val.mxcmpu Cle v1 v2
+  | ITgtu => Val.mxcmpu Cgt v1 v2
   end.
 
 Definition compare_long (t: itest) (v1 v2: val): val :=
@@ -930,12 +878,12 @@ Definition compare_long (t: itest) (v1 v2: val): val :=
   | ITge  => Val.cmpl Cge v1 v2
   | ITle  => Val.cmpl Cle v1 v2
   | ITgt  => Val.cmpl Cgt v1 v2
-  | ITneu => Some (Val_cmplu Cne v1 v2)
-  | ITequ => Some (Val_cmplu Ceq v1 v2)
-  | ITltu => Some (Val_cmplu Clt v1 v2)
-  | ITgeu => Some (Val_cmplu Cge v1 v2)
-  | ITleu => Some (Val_cmplu Cle v1 v2)
-  | ITgtu => Some (Val_cmplu Cgt v1 v2)
+  | ITneu => Some (Val.mxcmplu Cne v1 v2)
+  | ITequ => Some (Val.mxcmplu Ceq v1 v2)
+  | ITltu => Some (Val.mxcmplu Clt v1 v2)
+  | ITgeu => Some (Val.mxcmplu Cge v1 v2)
+  | ITleu => Some (Val.mxcmplu Cle v1 v2)
+  | ITgtu => Some (Val.mxcmplu Cgt v1 v2)
   end in 
   match res with
   | Some v => v
@@ -1147,13 +1095,13 @@ Definition cmove bt v1 v2 v3 :=
 Definition cmoveu bt v1 v2 v3 :=
   match cmpu_for_btest bt with
   | (Some c, Int)  =>
-    match Val_cmpu_bool c v2 (Vint Int.zero) with
+    match Val.mxcmpu_bool c v2 (Vint Int.zero) with
     | None => Vundef
     | Some true => v3
     | Some false => v1
     end
   | (Some c, Long) =>
-    match Val_cmplu_bool c v2 (Vlong Int64.zero) with
+    match Val.mxcmplu_bool c v2 (Vlong Int64.zero) with
     | None => Vundef
     | Some true => v3
     | Some false => v1
@@ -1529,8 +1477,8 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset)
       end
     | Pcbu bt r l => 
       match cmpu_for_btest bt with
-      | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val_cmpu_bool c rsr#r (Vint (Int.repr 0)))
-      | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val_cmplu_bool c rsr#r (Vlong (Int64.repr 0)))
+      | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val.mxcmpu_bool c rsr#r (Vint (Int.repr 0)))
+      | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.mxcmplu_bool c rsr#r (Vlong (Int64.repr 0)))
       | (None, _) => Stuck
       end
     (**r Pseudo-instructions *)