diff options
Diffstat (limited to 'kvx/Asmvliw.v')
-rw-r--r-- | kvx/Asmvliw.v | 84 |
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 *) |