From 615fb53c13f2407a0b6b470bbdf8e468fc4a1d78 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 5 Jun 2009 13:39:59 +0000 Subject: Adapted to work with Coq 8.2-1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 16 ++++++++-------- powerpc/Asmgen.v | 2 +- powerpc/Constprop.v | 12 ++++++------ powerpc/Machregs.v | 2 +- powerpc/Op.v | 24 ++++++++++++------------ powerpc/Selection.v | 38 +++++++++++++++++++------------------- powerpc/Selectionproof.v | 2 ++ powerpc/eabi/Stacklayout.v | 2 +- powerpc/macosx/Stacklayout.v | 2 +- 9 files changed, 51 insertions(+), 49 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 63f0232a..91de0b1e 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -30,7 +30,7 @@ Require Conventions. (** Integer registers, floating-point registers. *) -Inductive ireg: Set := +Inductive ireg: Type := | GPR0: ireg | GPR1: ireg | GPR2: ireg | GPR3: ireg | GPR4: ireg | GPR5: ireg | GPR6: ireg | GPR7: ireg | GPR8: ireg | GPR9: ireg | GPR10: ireg | GPR11: ireg @@ -40,7 +40,7 @@ Inductive ireg: Set := | GPR24: ireg | GPR25: ireg | GPR26: ireg | GPR27: ireg | GPR28: ireg | GPR29: ireg | GPR30: ireg | GPR31: ireg. -Inductive freg: Set := +Inductive freg: Type := | FPR0: freg | FPR1: freg | FPR2: freg | FPR3: freg | FPR4: freg | FPR5: freg | FPR6: freg | FPR7: freg | FPR8: freg | FPR9: freg | FPR10: freg | FPR11: freg @@ -63,7 +63,7 @@ Proof. decide equality. Defined. resolved later by the linker. *) -Inductive constant: Set := +Inductive constant: Type := | Cint: int -> constant | Csymbol_low: ident -> int -> constant | Csymbol_high: ident -> int -> constant. @@ -80,7 +80,7 @@ Inductive constant: Set := (** Bits in the condition register. We are only interested in the first 4 bits. *) -Inductive crbit: Set := +Inductive crbit: Type := | CRbit_0: crbit | CRbit_1: crbit | CRbit_2: crbit @@ -95,7 +95,7 @@ Inductive crbit: Set := Definition label := positive. -Inductive instruction : Set := +Inductive instruction : Type := | Padd: ireg -> ireg -> ireg -> instruction (**r integer addition *) | Paddi: ireg -> ireg -> constant -> instruction (**r add immediate *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) @@ -303,7 +303,7 @@ Definition program := AST.program fundef unit. (** The PowerPC has a great many registers, some general-purpose, some very specific. We model only the following registers: *) -Inductive preg: Set := +Inductive preg: Type := | IR: ireg -> preg (**r integer registers *) | FR: freg -> preg (**r float registers *) | PC: preg (**r program counter *) @@ -441,7 +441,7 @@ Definition const_high (c: constant) := set and memory state after execution of the instruction at [rs#PC], or [Error] if the processor is stuck. *) -Inductive outcome: Set := +Inductive outcome: Type := | OK: regset -> mem -> outcome | Error: outcome. @@ -819,7 +819,7 @@ Definition loc_external_result (sg: signature) : preg := (** Execution of the instruction at [rs#PC]. *) -Inductive state: Set := +Inductive state: Type := | State: regset -> mem -> state. Inductive step: state -> trace -> state -> Prop := diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 0c3ac75d..5c37a570 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -225,7 +225,7 @@ Definition crbit_for_cond (cond: condition) := (** Recognition of comparisons [>= 0] and [< 0]. *) -Inductive condition_class: condition -> list mreg -> Set := +Inductive condition_class: condition -> list mreg -> Type := | condition_ge0: forall n r, n = Int.zero -> condition_class (Ccompimm Cge n) (r :: nil) | condition_lt0: diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v index 6ec27a3f..76ea153c 100644 --- a/powerpc/Constprop.v +++ b/powerpc/Constprop.v @@ -32,7 +32,7 @@ Require Import Kildall. (** To each pseudo-register at each program point, the static analysis associates a compile-time approximation taken from the following set. *) -Inductive approx : Set := +Inductive approx : Type := | Novalue: approx (** No value possible, code is unreachable. *) | Unknown: approx (** All values are possible, no compile-time information is available. *) @@ -139,7 +139,7 @@ Definition eval_static_condition (cond: condition) (vl: list approx) := end. *) -Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Set := +Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type := | eval_static_condition_case1: forall c n1 n2, eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil) @@ -271,7 +271,7 @@ Definition eval_static_operation (op: operation) (vl: list approx) := end. *) -Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Set := +Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type := | eval_static_operation_case1: forall v1, eval_static_operation_cases (Omove) (v1::nil) @@ -696,7 +696,7 @@ Variable approx: D.t. Definition intval (r: reg) : option int := match D.get r approx with I n => Some n | _ => None end. -Inductive cond_strength_reduction_cases: condition -> list reg -> Set := +Inductive cond_strength_reduction_cases: condition -> list reg -> Type := | csr_case1: forall c r1 r2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) @@ -789,7 +789,7 @@ Definition make_xorimm (n: int) (r: reg) := then (Omove, r :: nil) else (Oxorimm n, r :: nil). -Inductive op_strength_reduction_cases: operation -> list reg -> Set := +Inductive op_strength_reduction_cases: operation -> list reg -> Type := | op_strength_reduction_case1: forall (r1: reg) (r2: reg), op_strength_reduction_cases Oadd (r1 :: r2 :: nil) @@ -949,7 +949,7 @@ Definition op_strength_reduction (op: operation) (args: list reg) := (op, args) end. -Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Set := +Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg), Type := | addr_strength_reduction_case1: forall (r1: reg) (r2: reg), addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index d0f7cf46..88b70c1d 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -29,7 +29,7 @@ Require Import AST. The type [mreg] does not include special-purpose or reserved machine registers such as the stack pointer and the condition codes. *) -Inductive mreg: Set := +Inductive mreg: Type := (** Allocatable integer regs *) | R3: mreg | R4: mreg | R5: mreg | R6: mreg | R7: mreg | R8: mreg | R9: mreg | R10: mreg diff --git a/powerpc/Op.v b/powerpc/Op.v index 300a8043..27e12c2c 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -36,7 +36,7 @@ Set Implicit Arguments. (** Conditions (boolean-valued operators). *) -Inductive condition : Set := +Inductive condition : Type := | Ccomp: comparison -> condition (**r signed integer comparison *) | Ccompu: comparison -> condition (**r unsigned integer comparison *) | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *) @@ -49,7 +49,7 @@ Inductive condition : Set := (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) -Inductive operation : Set := +Inductive operation : Type := | Omove: operation (**r [rd = r1] *) | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) @@ -104,7 +104,7 @@ Inductive operation : Set := (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) -Inductive addressing: Set := +Inductive addressing: Type := | Aindexed: int -> addressing (**r Address is [r1 + offset] *) | Aindexed2: addressing (**r Address is [r1 + r2] *) | Aglobal: ident -> int -> addressing (**r Address is [symbol + offset] *) @@ -182,7 +182,7 @@ Definition offset_sp (sp: val) (delta: int) : option val := end. Definition eval_operation - (F: Set) (genv: Genv.t F) (sp: val) + (F: Type) (genv: Genv.t F) (sp: val) (op: operation) (vl: list val): option val := match op, vl with | Omove, v1::nil => Some v1 @@ -265,7 +265,7 @@ Definition eval_operation end. Definition eval_addressing - (F: Set) (genv: Genv.t F) (sp: val) + (F: Type) (genv: Genv.t F) (sp: val) (addr: addressing) (vl: list val) : option val := match addr, vl with | Aindexed n, Vptr b1 n1 :: nil => @@ -360,7 +360,7 @@ Qed. Section GENV_TRANSF. -Variable F1 F2: Set. +Variable F1 F2: Type. Variable ge1: Genv.t F1. Variable ge2: Genv.t F2. Hypothesis agree_on_symbols: @@ -389,14 +389,14 @@ End GENV_TRANSF. (** Recognition of move operations. *) Definition is_move_operation - (A: Set) (op: operation) (args: list A) : option A := + (A: Type) (op: operation) (args: list A) : option A := match op, args with | Omove, arg :: nil => Some arg | _, _ => None end. Lemma is_move_operation_correct: - forall (A: Set) (op: operation) (args: list A) (a: A), + forall (A: Type) (op: operation) (args: list A) (a: A), is_move_operation op args = Some a -> op = Omove /\ args = a :: nil. Proof. @@ -497,7 +497,7 @@ Definition type_of_chunk (c: memory_chunk) : typ := Section SOUNDNESS. -Variable A: Set. +Variable A: Type. Variable genv: Genv.t A. Lemma type_of_operation_sound: @@ -560,7 +560,7 @@ End SOUNDNESS. Section EVAL_OP_TOTAL. -Variable F: Set. +Variable F: Type. Variable genv: Genv.t F. Definition find_symbol_offset (id: ident) (ofs: int) : val := @@ -746,7 +746,7 @@ End EVAL_OP_TOTAL. Section EVAL_LESSDEF. -Variable F: Set. +Variable F: Type. Variable genv: Genv.t F. Ltac InvLessdef := @@ -834,7 +834,7 @@ End EVAL_LESSDEF. Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. Lemma eval_op_for_binary_addressing: - forall (F: Set) (ge: Genv.t F) sp addr args v, + forall (F: Type) (ge: Genv.t F) sp addr args v, (length args >= 2)%nat -> eval_addressing ge sp addr args = Some v -> eval_operation ge sp (op_for_binary_addressing addr) args = Some v. diff --git a/powerpc/Selection.v b/powerpc/Selection.v index 46d80390..286517ef 100644 --- a/powerpc/Selection.v +++ b/powerpc/Selection.v @@ -118,7 +118,7 @@ Definition notint (e: expr) := characterizes the expressions that match each of the 4 cases of interest. *) -Inductive notint_cases: forall (e: expr), Set := +Inductive notint_cases: forall (e: expr), Type := | notint_case1: forall (t1: expr) (t2: expr), notint_cases (Eop Oand (t1:::t2:::Enil)) @@ -208,7 +208,7 @@ Definition addimm (n: int) (e: expr) := (** Addition of an integer constant. *) -Inductive addimm_cases: forall (e: expr), Set := +Inductive addimm_cases: forall (e: expr), Type := | addimm_case1: forall (m: int), addimm_cases (Eop (Ointconst m) Enil) @@ -268,7 +268,7 @@ Definition add (e1: expr) (e2: expr) := end. *) -Inductive add_cases: forall (e1: expr) (e2: expr), Set := +Inductive add_cases: forall (e1: expr) (e2: expr), Type := | add_case1: forall (n1: int) (t2: expr), add_cases (Eop (Ointconst n1) Enil) (t2) @@ -342,7 +342,7 @@ l)) end. *) -Inductive sub_cases: forall (e1: expr) (e2: expr), Set := +Inductive sub_cases: forall (e1: expr) (e2: expr), Type := | sub_case1: forall (t1: expr) (n2: int), sub_cases (t1) (Eop (Ointconst n2) Enil) @@ -410,7 +410,7 @@ Definition rolm (e1: expr) := end *) -Inductive rolm_cases: forall (e1: expr), Set := +Inductive rolm_cases: forall (e1: expr), Type := | rolm_case1: forall (n1: int), rolm_cases (Eop (Ointconst n1) Enil) @@ -488,7 +488,7 @@ Definition mulimm (n1: int) (e2: expr) := end. *) -Inductive mulimm_cases: forall (e2: expr), Set := +Inductive mulimm_cases: forall (e2: expr), Type := | mulimm_case1: forall (n2: int), mulimm_cases (Eop (Ointconst n2) Enil) @@ -532,7 +532,7 @@ Definition mul (e1: expr) (e2: expr) := end. *) -Inductive mul_cases: forall (e1: expr) (e2: expr), Set := +Inductive mul_cases: forall (e1: expr) (e2: expr), Type := | mul_case1: forall (n1: int) (t2: expr), mul_cases (Eop (Ointconst n1) Enil) (t2) @@ -584,7 +584,7 @@ Definition mod_aux (divop: operation) (e1 e2: expr) := Definition mods := mod_aux Odiv. -Inductive divu_cases: forall (e2: expr), Set := +Inductive divu_cases: forall (e2: expr), Type := | divu_case1: forall (n2: int), divu_cases (Eop (Ointconst n2) Enil) @@ -645,7 +645,7 @@ Definition same_expr_pure (e1 e2: expr) := | _, _ => false end. -Inductive or_cases: forall (e1: expr) (e2: expr), Set := +Inductive or_cases: forall (e1: expr) (e2: expr), Type := | or_case1: forall (amount1: int) (mask1: int) (t1: expr) (amount2: int) (mask2: int) (t2: expr), @@ -678,7 +678,7 @@ Definition or (e1: expr) (e2: expr) := (** ** General shifts *) -Inductive shift_cases: forall (e1: expr), Set := +Inductive shift_cases: forall (e1: expr), Type := | shift_case1: forall (n2: int), shift_cases (Eop (Ointconst n2) Enil) @@ -723,7 +723,7 @@ Definition addf (e1: expr) (e2: expr) := end. *) -Inductive addf_cases: forall (e1: expr) (e2: expr), Set := +Inductive addf_cases: forall (e1: expr) (e2: expr), Type := | addf_case1: forall (t1: expr) (t2: expr) (t3: expr), addf_cases (Eop Omulf (t1:::t2:::Enil)) (t3) @@ -770,7 +770,7 @@ Definition subf (e1: expr) (e2: expr) := end. *) -Inductive subf_cases: forall (e1: expr) (e2: expr), Set := +Inductive subf_cases: forall (e1: expr) (e2: expr), Type := | subf_case1: forall (t1: expr) (t2: expr) (t3: expr), subf_cases (Eop Omulf (t1:::t2:::Enil)) (t3) @@ -798,7 +798,7 @@ Definition subf (e1: expr) (e2: expr) := (** ** Truncations and sign extensions *) -Inductive cast8signed_cases: forall (e1: expr), Set := +Inductive cast8signed_cases: forall (e1: expr), Type := | cast8signed_case1: forall (e2: expr), cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) @@ -826,7 +826,7 @@ Definition cast8signed (e: expr) := | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) end. -Inductive cast8unsigned_cases: forall (e1: expr), Set := +Inductive cast8unsigned_cases: forall (e1: expr), Type := | cast8unsigned_case1: forall (e2: expr), cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) @@ -854,7 +854,7 @@ Definition cast8unsigned (e: expr) := | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) end. -Inductive cast16signed_cases: forall (e1: expr), Set := +Inductive cast16signed_cases: forall (e1: expr), Type := | cast16signed_case1: forall (e2: expr), cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) @@ -882,7 +882,7 @@ Definition cast16signed (e: expr) := | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) end. -Inductive cast16unsigned_cases: forall (e1: expr), Set := +Inductive cast16unsigned_cases: forall (e1: expr), Type := | cast16unsigned_case1: forall (e2: expr), cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) @@ -910,7 +910,7 @@ Definition cast16unsigned (e: expr) := | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) end. -Inductive singleoffloat_cases: forall (e1: expr), Set := +Inductive singleoffloat_cases: forall (e1: expr), Type := | singleoffloat_case1: forall (e2: expr), singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) @@ -940,7 +940,7 @@ Definition singleoffloat (e: expr) := (** ** Comparisons *) -Inductive comp_cases: forall (e1: expr) (e2: expr), Set := +Inductive comp_cases: forall (e1: expr) (e2: expr), Type := | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2) @@ -1043,7 +1043,7 @@ Definition addressing (e: expr) := end. *) -Inductive addressing_cases: forall (e: expr), Set := +Inductive addressing_cases: forall (e: expr), Type := | addressing_case1: forall (s: ident) (n: int), addressing_cases (Eop (Oaddrsymbol s n) Enil) diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v index 6ffffc18..8a02c997 100644 --- a/powerpc/Selectionproof.v +++ b/powerpc/Selectionproof.v @@ -1357,10 +1357,12 @@ Proof. econstructor. destruct k; simpl in H; simpl; auto. rewrite <- H0; reflexivity. constructor; auto. +(* (* assign *) exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split. constructor. auto with evalexpr. constructor; auto. +*) (* store *) econstructor; split. eapply eval_store; eauto with evalexpr. diff --git a/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v index 48e26a76..0de1ccd6 100644 --- a/powerpc/eabi/Stacklayout.v +++ b/powerpc/eabi/Stacklayout.v @@ -45,7 +45,7 @@ the boundaries between areas in the frame part. Definition fe_ofs_arg := 8. -Record frame_env : Set := mk_frame_env { +Record frame_env : Type := mk_frame_env { fe_size: Z; fe_ofs_link: Z; fe_ofs_retaddr: Z; diff --git a/powerpc/macosx/Stacklayout.v b/powerpc/macosx/Stacklayout.v index 0e9be224..c57f3f92 100644 --- a/powerpc/macosx/Stacklayout.v +++ b/powerpc/macosx/Stacklayout.v @@ -42,7 +42,7 @@ the boundaries between areas in the frame part. Definition fe_ofs_arg := 24. -Record frame_env : Set := mk_frame_env { +Record frame_env : Type := mk_frame_env { fe_size: Z; fe_ofs_link: Z; fe_ofs_retaddr: Z; -- cgit