aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/Asmvliw.v
diff options
context:
space:
mode:
Diffstat (limited to 'kvx/Asmvliw.v')
-rw-r--r--kvx/Asmvliw.v136
1 files changed, 45 insertions, 91 deletions
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 296963a7..8afe8d07 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -163,6 +163,30 @@ Module PregEq.
Definition eq := preg_eq.
End PregEq.
+(* FIXME - R16 and R32 are excluded *)
+Definition preg_of (r: mreg) : preg :=
+ match r with
+ | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4
+ | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9
+ | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *)
+ | R15 => GPR15 (* | R16 => GPR16 *) | R17 => GPR17 | R18 => GPR18 | R19 => GPR19
+ | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24
+ | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29
+ | R30 => GPR30 | R31 => GPR31 (* | R32 => GPR32 *) | R33 => GPR33 | R34 => GPR34
+ | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39 => GPR39
+ | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44 => GPR44
+ | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49 => GPR49
+ | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54 => GPR54
+ | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59 => GPR59
+ | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
+ end.
+
+Definition ireg_of (r: mreg) : res ireg :=
+ match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.ireg_of") end.
+
+Definition freg_of (r: mreg) : res freg :=
+ match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end.
+
Module Pregmap := EMap(PregEq).
(** ** Conventional names for stack pointer ([SP]), return address ([RA]), frame pointer ([FP]) and other temporaries used *)
@@ -829,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; simpl.
- - 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|]; simpl.
- - erewrite Val_cmplu_bool_correct; eauto.
- simpl. econstructor.
- - econstructor.
-Qed.
-
-
-
(** **** Comparing integers *)
Definition compare_int (t: itest) (v1 v2: val): val :=
match t with
@@ -890,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 :=
@@ -906,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
@@ -1123,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
@@ -1426,13 +1398,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool :=
Lemma is_label_correct_true lbl bb:
List.In lbl (header bb) <-> is_label lbl bb = true.
Proof.
- unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+ unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition.
Qed.
Lemma is_label_correct_false lbl bb:
~(List.In lbl (header bb)) <-> is_label lbl bb = false.
Proof.
- unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition.
+ unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition.
Qed.
@@ -1505,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 *)
@@ -1548,24 +1520,6 @@ Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs'
code. *)
-(* FIXME - R16 and R32 are excluded *)
-Definition preg_of (r: mreg) : preg :=
- match r with
- | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4
- | R5 => GPR5 | R6 => GPR6 | R7 => GPR7 | R8 => GPR8 | R9 => GPR9
- | R10 => GPR10 | R11 => GPR11 (* | R12 => GPR12 | R13 => GPR13 | R14 => GPR14 *)
- | R15 => GPR15 (* | R16 => GPR16 *) | R17 => GPR17 | R18 => GPR18 | R19 => GPR19
- | R20 => GPR20 | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24
- | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29
- | R30 => GPR30 | R31 => GPR31 (* | R32 => GPR32 *) | R33 => GPR33 | R34 => GPR34
- | R35 => GPR35 | R36 => GPR36 | R37 => GPR37 | R38 => GPR38 | R39 => GPR39
- | R40 => GPR40 | R41 => GPR41 | R42 => GPR42 | R43 => GPR43 | R44 => GPR44
- | R45 => GPR45 | R46 => GPR46 | R47 => GPR47 | R48 => GPR48 | R49 => GPR49
- | R50 => GPR50 | R51 => GPR51 | R52 => GPR52 | R53 => GPR53 | R54 => GPR54
- | R55 => GPR55 | R56 => GPR56 | R57 => GPR57 | R58 => GPR58 | R59 => GPR59
- | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
- end.
-
(** **** Undefine all registers except SP and callee-save registers *)
Definition undef_caller_save_regs (rs: regset) : regset :=
@@ -1667,7 +1621,7 @@ Proof.
constructor 1.
- rewrite app_nil_r; auto.
- unfold parexec_wio_bblock.
- destruct (parexec_wio f _ _ _); simpl; auto.
+ destruct (parexec_wio f _ _ _); cbn; auto.
Qed.
@@ -1739,7 +1693,7 @@ Ltac Det_WIO X :=
exploit det_parexec_write_in_order; [ eapply H | idtac]; clear H; intro X
| _ => idtac
end.
- intros; constructor; simpl.
+ intros; constructor; cbn.
- (* determ *) intros s t1 s1 t2 s2 H H0. inv H; Det_WIO X1;
inv H0; Det_WIO X2; Equalities.
+ split. constructor. auto.
@@ -1754,7 +1708,7 @@ Ltac Det_WIO X :=
exploit external_call_determ. eexact H3. eexact H8. intros [A B].
split. auto. intros. destruct B; auto. subst. auto.
- (* trace length *)
- red; intros. inv H; simpl.
+ red; intros. inv H; cbn.
omega.
eapply external_call_trace_length; eauto.
eapply external_call_trace_length; eauto.
generated by cgit (git 2.34.1) at 2024-06-02 13:59:37 +0000