diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asmgenproof1.v | 4 | ||||
-rw-r--r-- | arm/ConstpropOp.v | 18 | ||||
-rw-r--r-- | arm/ConstpropOpproof.v | 16 | ||||
-rw-r--r-- | arm/Op.v | 40 | ||||
-rw-r--r-- | arm/SelectOp.v | 8 | ||||
-rw-r--r-- | arm/SelectOpproof.v | 20 |
6 files changed, 53 insertions, 53 deletions
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index b18ae91..0776413 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1089,10 +1089,10 @@ Proof. simpl in H1. destruct (ms m0); try discriminate. exists i0; split; auto. destruct (Int.ltu i (Int.repr 31)); discriminate || auto. destruct H3 as [n [ARG1 LTU]]. - assert (LTU': Int.ltu i (Int.repr 32) = true). + assert (LTU': Int.ltu i Int.iwordsize = true). exploit Int.ltu_inv. eexact LTU. intro. unfold Int.ltu. apply zlt_true. - assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto. + assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto. omega. assert (RSm0: rs (ireg_of m0) = Vint n). rewrite <- ARG1. symmetry. eapply ireg_val; eauto. diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v index b5e5a03..e55c7f9 100644 --- a/arm/ConstpropOp.v +++ b/arm/ConstpropOp.v @@ -174,9 +174,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) := | Obicshift s, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not (eval_shift s n2))) | Onot, I n1 :: nil => I(Int.not n1) | Onotshift s, I n1 :: nil => I(Int.not (eval_shift s n1)) - | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown - | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown - | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown + | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown + | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown + | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown | Oshift s, I n1 :: nil => I(eval_shift s n1) | Onegf, F n1 :: nil => F(Float.neg n1) | Oabsf, F n1 :: nil => F(Float.abs n1) @@ -543,11 +543,11 @@ Definition eval_static_operation (op: operation) (vl: list approx) := | eval_static_operation_case36 s n1 => I(Int.not (eval_shift s n1)) | eval_static_operation_case37 n1 n2 => - if Int.ltu n2 (Int.repr 32) then I(Int.shl n1 n2) else Unknown + if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown | eval_static_operation_case38 n1 n2 => - if Int.ltu n2 (Int.repr 32) then I(Int.shr n1 n2) else Unknown + if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown | eval_static_operation_case39 n1 n2 => - if Int.ltu n2 (Int.repr 32) then I(Int.shru n1 n2) else Unknown + if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown | eval_static_operation_case40 s n1 => I(eval_shift s n1) | eval_static_operation_case41 n1 => @@ -954,7 +954,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := | op_strength_reduction_case16 r1 r2 => (* Oshl *) match intval r2 with | Some n => - if Int.ltu n (Int.repr 32) + if Int.ltu n Int.iwordsize then make_shlimm n r1 else (op, args) | _ => (op, args) @@ -962,7 +962,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := | op_strength_reduction_case17 r1 r2 => (* Oshr *) match intval r2 with | Some n => - if Int.ltu n (Int.repr 32) + if Int.ltu n Int.iwordsize then make_shrimm n r1 else (op, args) | _ => (op, args) @@ -970,7 +970,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := | op_strength_reduction_case18 r1 r2 => (* Oshru *) match intval r2 with | Some n => - if Int.ltu n (Int.repr 32) + if Int.ltu n Int.iwordsize then make_shruimm n r1 else (op, args) | _ => (op, args) diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index bb9caff..b718fc2 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -130,13 +130,13 @@ Proof. replace n2 with i0. destruct (Int.eq i0 Int.zero). discriminate. injection H0; intro; subst v. simpl. congruence. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. - replace n2 with i0. destruct (Int.ltu i0 (Int.repr 32)). + replace n2 with i0. destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v. simpl. congruence. discriminate. congruence. rewrite <- H3. replace v0 with (Vfloat n1). reflexivity. congruence. @@ -284,7 +284,7 @@ Proof. with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). apply make_shlimm_correct. simpl. generalize (Int.is_power2_range _ _ H2). - change (Z_of_nat wordsize) with 32. intro. rewrite H3. + change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3. destruct rs#r; auto. rewrite (Int.mul_pow2 i0 _ _ H2). auto. simpl List.map. rewrite H. auto. Qed. @@ -400,7 +400,7 @@ Proof. with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). apply make_shruimm_correct. simpl. destruct rs#r1; auto. - change 32 with (Z_of_nat wordsize). + change 32 with (Z_of_nat Int.wordsize). rewrite (Int.is_power2_range _ _ H0). generalize (Int.eq_spec i Int.zero); case (Int.eq i Int.zero); intros. subst i. discriminate. @@ -474,19 +474,19 @@ Proof. assumption. (* Oshl *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shlimm_correct. assumption. assumption. (* Oshr *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shrimm_correct. assumption. assumption. (* Oshru *) caseEq (intval app r2); intros. - caseEq (Int.ltu i (Int.repr 32)); intros. + caseEq (Int.ltu i Int.iwordsize); intros. rewrite (intval_correct _ _ H). apply make_shruimm_correct. assumption. assumption. @@ -37,7 +37,7 @@ Set Implicit Arguments. Record shift_amount : Type := mk_shift_amount { s_amount: int; - s_amount_ltu: Int.ltu s_amount (Int.repr 32) = true + s_amount_ltu: Int.ltu s_amount Int.iwordsize = true }. Inductive shift : Type := @@ -267,11 +267,11 @@ Definition eval_operation | Onot, Vint n1 :: nil => Some (Vint (Int.not n1)) | Onotshift s, Vint n1 :: nil => Some (Vint (Int.not (eval_shift s n1))) | Oshl, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shl n1 n2)) else None | Oshr, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None | Oshru, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None + if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None | Oshift s, Vint n :: nil => Some (Vint (eval_shift s n)) | Oshrximm n, Vint n1 :: nil => if Int.ltu n (Int.repr 31) then Some (Vint (Int.shrx n1 n)) else None @@ -548,11 +548,11 @@ Proof. injection H0; intro; subst v; exact I. destruct (Int.eq i0 Int.zero). discriminate. injection H0; intro; subst v; exact I. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. - destruct (Int.ltu i0 (Int.repr 32)). + destruct (Int.ltu i0 Int.iwordsize). injection H0; intro; subst v; exact I. discriminate. destruct (Int.ltu i (Int.repr 31)). injection H0; intro; subst v; exact I. discriminate. @@ -724,12 +724,12 @@ Proof. unfold eq_block in H. destruct (zeq b b0); congruence. destruct (Int.eq i0 Int.zero); congruence. destruct (Int.eq i0 Int.zero); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. - destruct (Int.ltu i0 (Int.repr 32)); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. + destruct (Int.ltu i0 Int.iwordsize); congruence. unfold Int.ltu in H. destruct (zlt (Int.unsigned i) (Int.unsigned (Int.repr 31))). unfold Int.ltu. rewrite zlt_true. congruence. - assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto. + assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto. omega. discriminate. caseEq (eval_condition c vl); intros; rewrite H0 in H. replace v with (Val.of_bool b). @@ -825,11 +825,11 @@ Proof. destruct (eq_block b b0); inv H0. TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists. - destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. caseEq (eval_condition c vl1); intros. rewrite H1 in H0. @@ -853,10 +853,10 @@ End EVAL_LESSDEF. (** Recognition of integers that are valid shift amounts. *) Definition is_shift_amount_aux (n: int) : - { Int.ltu n (Int.repr 32) = true } + - { Int.ltu n (Int.repr 32) = false }. + { Int.ltu n Int.iwordsize = true } + + { Int.ltu n Int.iwordsize = false }. Proof. - intro. case (Int.ltu n (Int.repr 32)). left; auto. right; auto. + intro. case (Int.ltu n Int.iwordsize). left; auto. right; auto. Defined. Definition is_shift_amount (n: int) : option shift_amount := @@ -875,7 +875,7 @@ Proof. Qed. Lemma is_shift_amount_None: - forall n, is_shift_amount n = None -> Int.ltu n (Int.repr 32) = true -> False. + forall n, is_shift_amount n = None -> Int.ltu n Int.iwordsize = true -> False. Proof. intro n. unfold is_shift_amount. destruct (is_shift_amount_aux n). diff --git a/arm/SelectOp.v b/arm/SelectOp.v index 4b5fde7..abf39af 100644 --- a/arm/SelectOp.v +++ b/arm/SelectOp.v @@ -385,7 +385,7 @@ Definition shlimm (e1: expr) := if Int.eq n Int.zero then e1 else match e1 with | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) - | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil) + | Eop (Oshift (Olsl n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Olsl (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsl n)) (e1:::Enil) | _ => Eop (Oshift (Olsl n)) (e1:::Enil) end. *) @@ -436,7 +436,7 @@ Definition shruimm (e1: expr) := if Int.eq n Int.zero then e1 else match e1 with | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) - | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil) + | Eop (Oshift (Olsr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Olsr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Olsr n)) (e1:::Enil) | _ => Eop (Oshift (Olsr n)) (e1:::Enil) end. *) @@ -486,7 +486,7 @@ Definition shruimm (e1: expr) (n: int) := Definition shrimm (e1: expr) := match e1 with | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) - | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) (Int.repr 32) then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil) + | Eop (Oshift (Oasr n1)) (t1:::Enil) => if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Oasr (Int.add n n1))) (t1:::Enil) else Eop (Oshift (Oasr n)) (e1:::Enil) | _ => Eop (Oshift (Oasr n)) (e1:::Enil) end. *) @@ -825,7 +825,7 @@ Definition or_match (e1: expr) (e2: expr) := Definition or (e1: expr) (e2: expr) := match or_match e1 e2 with | or_case1 n1 t1 n2 t2 => - if Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32) + if Int.eq (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize && same_expr_pure t1 t2 then Eop (Oshift (Sror n2)) (t1:::Enil) else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 68b49fd..32aba30 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -342,7 +342,7 @@ Qed. Theorem eval_shlimm: forall le a n x, eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> + Int.ltu n Int.iwordsize = true -> eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)). Proof. intros until x. unfold shlimm, is_shift_amount. @@ -365,7 +365,7 @@ Qed. Theorem eval_shruimm: forall le a n x, eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> + Int.ltu n Int.iwordsize = true -> eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)). Proof. intros until x. unfold shruimm, is_shift_amount. @@ -388,7 +388,7 @@ Qed. Theorem eval_shrimm: forall le a n x, eval_expr ge sp e m le a (Vint x) -> - Int.ltu n (Int.repr 32) = true -> + Int.ltu n Int.iwordsize = true -> eval_expr ge sp e m le (shrimm a n) (Vint (Int.shr x n)). Proof. intros until x. unfold shrimm, is_shift_amount. @@ -416,7 +416,7 @@ Proof. intros; unfold mulimm_base. generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). - change (Z_of_nat wordsize) with 32. + change (Z_of_nat Int.wordsize) with 32. destruct (Int.one_bits n). intros. EvalOp. constructor. EvalOp. simpl; reflexivity. constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto. @@ -497,7 +497,7 @@ Proof. rewrite (Int.divs_pow2 x y i H0). auto. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. - change (Int.unsigned (Int.repr 32)) with 32. + change (Int.unsigned Int.iwordsize) with 32. omega. apply eval_divs_base. auto. EvalOp. auto. apply eval_divs_base. auto. EvalOp. auto. @@ -634,10 +634,10 @@ Lemma eval_or: eval_expr ge sp e m le (or a b) (Vint (Int.or x y)). Proof. intros until y; unfold or; case (or_match a b); intros; InvEval. - caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32) + caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize && same_expr_pure t1 t2); intro. destruct (andb_prop _ _ H1). - generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) (Int.repr 32)). + generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize). rewrite H4. intro. exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. simpl. EvalOp. simpl. decEq. decEq. apply Int.or_ror. @@ -666,7 +666,7 @@ Theorem eval_shl: forall le a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> + Int.ltu y Int.iwordsize = true -> eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)). Proof. intros until y; unfold shl; case (shift_match b); intros. @@ -678,7 +678,7 @@ Theorem eval_shru: forall le a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> + Int.ltu y Int.iwordsize = true -> eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)). Proof. intros until y; unfold shru; case (shift_match b); intros. @@ -690,7 +690,7 @@ Theorem eval_shr: forall le a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> - Int.ltu y (Int.repr 32) = true -> + Int.ltu y Int.iwordsize = true -> eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)). Proof. intros until y; unfold shr; case (shift_match b); intros. |