diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocproof.v | 4 | ||||
| -rw-r--r-- | backend/Bounds.v | 8 | ||||
| -rw-r--r-- | backend/CSE.v | 4 | ||||
| -rw-r--r-- | backend/Cminor.v | 18 | ||||
| -rw-r--r-- | backend/CminorSel.v | 14 | ||||
| -rw-r--r-- | backend/Coloring.v | 4 | ||||
| -rw-r--r-- | backend/Coloringproof.v | 20 | ||||
| -rw-r--r-- | backend/InterfGraph.v | 22 | ||||
| -rw-r--r-- | backend/Kildall.v | 10 | ||||
| -rw-r--r-- | backend/LTL.v | 10 | ||||
| -rw-r--r-- | backend/LTLin.v | 10 | ||||
| -rw-r--r-- | backend/Linear.v | 10 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 2 | ||||
| -rw-r--r-- | backend/Locations.v | 4 | ||||
| -rw-r--r-- | backend/Mach.v | 4 | ||||
| -rw-r--r-- | backend/Machabstr.v | 6 | ||||
| -rw-r--r-- | backend/Machconcr.v | 4 | ||||
| -rw-r--r-- | backend/RTL.v | 10 | ||||
| -rw-r--r-- | backend/RTLgen.v | 20 | ||||
| -rw-r--r-- | backend/RTLgenspec.v | 185 | ||||
| -rw-r--r-- | backend/Registers.v | 6 | ||||
| -rw-r--r-- | backend/Stacking.v | 2 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 4 | ||||
| -rw-r--r-- | backend/Stackingtyping.v | 2 | ||||
| -rw-r--r-- | backend/Tailcallproof.v | 8 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 6 |
26 files changed, 168 insertions, 229 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 3971fb6..e2387b5 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -167,7 +167,7 @@ Proof. eapply DS.fixpoint_solution. unfold analyze in H; eauto. auto. auto. auto. auto. unfold transfer. rewrite H3. - red; intros. elim (Regset.empty_1 _ H4). + red; intros. elim (Regset.empty_1 H4). unfold RTL.successors in H0; rewrite H2 in H0; elim H0. Qed. @@ -581,7 +581,7 @@ Proof. rewrite H. simpl. caseEq (Regset.mem res live!!pc); intro LV; rewrite LV in AG. - generalize (Regset.mem_2 _ _ LV). intro LV'. + generalize (Regset.mem_2 LV). intro LV'. generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). unfold correct_alloc_instr, is_redundant_move. caseEq (is_move_operation op args). diff --git a/backend/Bounds.v b/backend/Bounds.v index d1ed28d..8c5f536 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -30,7 +30,7 @@ Require Import Conventions. These properties are used later to reason about the layout of the activation record. *) -Record bounds : Set := mkbounds { +Record bounds : Type := mkbounds { bound_int_local: Z; bound_float_local: Z; bound_int_callee_save: Z; @@ -116,7 +116,7 @@ Definition slots_of_instr (i: instruction) : list slot := | _ => nil end. -Definition max_over_list (A: Set) (valu: A -> Z) (l: list A) : Z := +Definition max_over_list (A: Type) (valu: A -> Z) (l: list A) : Z := List.fold_left (fun m l => Zmax m (valu l)) l 0. Definition max_over_instrs (valu: instruction -> Z) : Z := @@ -151,7 +151,7 @@ Definition outgoing_space (i: instruction) := match i with Lcall sig _ => size_arguments sig | _ => 0 end. Lemma max_over_list_pos: - forall (A: Set) (valu: A -> Z) (l: list A), + forall (A: Type) (valu: A -> Z) (l: list A), max_over_list A valu l >= 0. Proof. intros until valu. unfold max_over_list. @@ -196,7 +196,7 @@ Qed. (** We now show the correctness of the inferred bounds. *) Lemma max_over_list_bound: - forall (A: Set) (valu: A -> Z) (l: list A) (x: A), + forall (A: Type) (valu: A -> Z) (l: list A) (x: A), In x l -> valu x <= max_over_list A valu l. Proof. intros until x. unfold max_over_list. diff --git a/backend/CSE.v b/backend/CSE.v index 13e9be8..cad3503 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -49,7 +49,7 @@ Require Import Kildall. Definition valnum := positive. -Inductive rhs : Set := +Inductive rhs : Type := | Op: operation -> list valnum -> rhs | Load: memory_chunk -> addressing -> list valnum -> rhs. @@ -85,7 +85,7 @@ Qed. we maintain the next unused value number, so as to easily generate fresh value numbers. *) -Record numbering : Set := mknumbering { +Record numbering : Type := mknumbering { num_next: valnum; num_eqs: list (valnum * rhs); num_reg: PTree.t valnum diff --git a/backend/Cminor.v b/backend/Cminor.v index 35bf391..b48db2d 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -33,13 +33,13 @@ Require Import Switch. statements, functions and programs. We first define the constants and operators that occur within expressions. *) -Inductive constant : Set := +Inductive constant : Type := | Ointconst: int -> constant (**r integer constant *) | Ofloatconst: float -> constant (**r floating-point constant *) | Oaddrsymbol: ident -> int -> constant (**r address of the symbol plus the offset *) | Oaddrstack: int -> constant. (**r stack pointer plus the given offset *) -Inductive unary_operation : Set := +Inductive unary_operation : Type := | Ocast8unsigned: unary_operation (**r 8-bit zero extension *) | Ocast8signed: unary_operation (**r 8-bit sign extension *) | Ocast16unsigned: unary_operation (**r 16-bit zero extension *) @@ -55,7 +55,7 @@ Inductive unary_operation : Set := | Ofloatofint: unary_operation (**r float to signed integer *) | Ofloatofintu: unary_operation. (**r float to unsigned integer *) -Inductive binary_operation : Set := +Inductive binary_operation : Type := | Oadd: binary_operation (**r integer addition *) | Osub: binary_operation (**r integer subtraction *) | Omul: binary_operation (**r integer multiplication *) @@ -81,7 +81,7 @@ Inductive binary_operation : Set := arithmetic operations, reading store locations, and conditional expressions (similar to [e1 ? e2 : e3] in C). *) -Inductive expr : Set := +Inductive expr : Type := | Evar : ident -> expr | Econst : constant -> expr | Eunop : unary_operation -> expr -> expr @@ -97,7 +97,7 @@ Inductive expr : Set := Definition label := ident. -Inductive stmt : Set := +Inductive stmt : Type := | Sskip: stmt | Sassign : ident -> expr -> stmt | Sstore : memory_chunk -> expr -> expr -> stmt @@ -120,7 +120,7 @@ Inductive stmt : Set := automatically before the function returns. Pointers into this block can be taken with the [Oaddrstack] operator. *) -Record function : Set := mkfunction { +Record function : Type := mkfunction { fn_sig: signature; fn_params: list ident; fn_vars: list ident; @@ -172,7 +172,7 @@ Definition set_optvar (optid: option ident) (v: val) (e: env) : env := (** Continuations *) -Inductive cont: Set := +Inductive cont: Type := | Kstop: cont (**r stop program execution *) | Kseq: stmt -> cont -> cont (**r execute stmt, then cont *) | Kblock: cont -> cont (**r exit a block, then do cont *) @@ -181,7 +181,7 @@ Inductive cont: Set := (** States *) -Inductive state: Set := +Inductive state: Type := | State: (**r Execution within a function *) forall (f: function) (**r currently executing function *) (s: stmt) (**r statement under consideration *) @@ -536,7 +536,7 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop := statements evaluate to``outcomes'' indicating how execution should proceed afterwards. *) -Inductive outcome: Set := +Inductive outcome: Type := | Out_normal: outcome (**r continue in sequence *) | Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *) | Out_return: option val -> outcome (**r return immediately to caller *) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index bfe92a4..1e798b5 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -40,7 +40,7 @@ Require Import Smallstep. boolean value only and not their exact value. *) -Inductive expr : Set := +Inductive expr : Type := | Evar : ident -> expr | Eop : operation -> exprlist -> expr | Eload : memory_chunk -> addressing -> exprlist -> expr @@ -48,13 +48,13 @@ Inductive expr : Set := | Elet : expr -> expr -> expr | Eletvar : nat -> expr -with condexpr : Set := +with condexpr : Type := | CEtrue: condexpr | CEfalse: condexpr | CEcond: condition -> exprlist -> condexpr | CEcondition : condexpr -> condexpr -> condexpr -> condexpr -with exprlist : Set := +with exprlist : Type := | Enil: exprlist | Econs: expr -> exprlist -> exprlist. @@ -62,7 +62,7 @@ with exprlist : Set := if/then/else conditional is a [condexpr], and the [Sstore] construct uses a machine-dependent addressing mode. *) -Inductive stmt : Set := +Inductive stmt : Type := | Sskip: stmt | Sassign : ident -> expr -> stmt | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt @@ -78,7 +78,7 @@ Inductive stmt : Set := | Slabel: label -> stmt -> stmt | Sgoto: label -> stmt. -Record function : Set := mkfunction { +Record function : Type := mkfunction { fn_sig: signature; fn_params: list ident; fn_vars: list ident; @@ -108,7 +108,7 @@ Definition letenv := list val. (** Continuations *) -Inductive cont: Set := +Inductive cont: Type := | Kstop: cont (**r stop program execution *) | Kseq: stmt -> cont -> cont (**r execute stmt, then cont *) | Kblock: cont -> cont (**r exit a block, then do cont *) @@ -117,7 +117,7 @@ Inductive cont: Set := (** States *) -Inductive state: Set := +Inductive state: Type := | State: (**r execution within a function *) forall (f: function) (**r currently executing function *) (s: stmt) (**r statement under consideration *) diff --git a/backend/Coloring.v b/backend/Coloring.v index 7204bc7..67824ae 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -93,7 +93,7 @@ Require Import InterfGraph. Definition add_interf_live (filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph := - Regset.fold graph + Regset.fold (fun r g => if filter r then add_interf r res g else g) live g. Definition add_interf_op @@ -113,7 +113,7 @@ Definition add_interf_move Definition add_interf_destroyed (live: Regset.t) (destroyed: list mreg) (g: graph): graph := List.fold_left - (fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g) + (fun g mr => Regset.fold (fun r g => add_interf_mreg r mr g) live g) destroyed g. Definition add_interfs_indirect_call diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index c86652a..92ac067 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -148,7 +148,7 @@ Qed. Lemma add_interf_destroyed_incl_aux_2: forall mr live g, graph_incl g - (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g). + (Regset.fold (fun r g => add_interf_mreg r mr g) live g). Proof. intros. rewrite Regset.fold_1. apply add_interf_destroyed_incl_aux_1. Qed. @@ -219,7 +219,7 @@ Lemma add_interf_destroyed_correct_aux_2: forall mr live g r, Regset.In r live -> interfere_mreg r mr - (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g). + (Regset.fold (fun r g => add_interf_mreg r mr g) live g). Proof. intros. rewrite Regset.fold_1. apply add_interf_destroyed_correct_aux_1. apply Regset.elements_1. auto. @@ -619,12 +619,12 @@ Lemma check_coloring_1_correct: coloring r1 <> coloring r2. Proof. unfold check_coloring_1. intros. - assert (FSetInterface.compat_bool OrderedRegReg.eq + assert (compat_bool OrderedRegReg.eq (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2)) then false else true)). red. unfold OrderedRegReg.eq. unfold OrderedReg.eq. intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto. - generalize (SetRegReg.for_all_2 _ _ H1 H _ H0). + generalize (SetRegReg.for_all_2 H1 H H0). simpl. case (Loc.eq (coloring r1) (coloring r2)); intro. intro; discriminate. auto. Qed. @@ -636,12 +636,12 @@ Lemma check_coloring_2_correct: coloring r1 <> R mr2. Proof. unfold check_coloring_2. intros. - assert (FSetInterface.compat_bool OrderedRegMreg.eq + assert (compat_bool OrderedRegMreg.eq (fun r1r2 => if Loc.eq (coloring (fst r1r2)) (R (snd r1r2)) then false else true)). red. unfold OrderedRegMreg.eq. unfold OrderedReg.eq. intros x y [EQ1 EQ2]. rewrite EQ1; rewrite EQ2; auto. - generalize (SetRegMreg.for_all_2 _ _ H1 H _ H0). + generalize (SetRegMreg.for_all_2 H1 H H0). simpl. case (Loc.eq (coloring r1) (R mr2)); intro. intro; discriminate. auto. Qed. @@ -920,12 +920,12 @@ Proof. intros. rewrite H2. unfold allregs. elim (ordered_pair_charact x y); intro. apply alloc_of_coloring_correct_1. auto. - change OrderedReg.t with reg. rewrite <- H6. + change positive with reg. rewrite <- H6. change (interfere x y g). unfold g. apply interf_graph_correct_2; auto. apply sym_not_equal. apply alloc_of_coloring_correct_1. auto. - change OrderedReg.t with reg. rewrite <- H6. + change positive with reg. rewrite <- H6. change (interfere x y g). unfold g. apply interf_graph_correct_2; auto. Qed. @@ -942,12 +942,12 @@ Proof. rewrite H4; unfold allregs. elim (ordered_pair_charact r1 r2); intro. apply alloc_of_coloring_correct_1. auto. - change OrderedReg.t with reg. rewrite <- H5. + change positive with reg. rewrite <- H5. change (interfere r1 r2 g). unfold g. apply interf_graph_correct_3; auto. apply sym_not_equal. apply alloc_of_coloring_correct_1. auto. - change OrderedReg.t with reg. rewrite <- H5. + change positive with reg. rewrite <- H5. change (interfere r1 r2 g). unfold g. apply interf_graph_correct_3; auto. Qed. diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index 433c074..8a9dda6 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -55,7 +55,7 @@ Module OrderedRegMreg := OrderedPair(OrderedReg)(OrderedMreg). Module SetRegReg := FSetAVL.Make(OrderedRegReg). Module SetRegMreg := FSetAVL.Make(OrderedRegMreg). -Record graph: Set := mkgraph { +Record graph: Type := mkgraph { interf_reg_reg: SetRegReg.t; interf_reg_mreg: SetRegMreg.t; pref_reg_reg: SetRegReg.t; @@ -160,7 +160,7 @@ Lemma add_interf_correct: interfere x y (add_interf x y g). Proof. intros. unfold interfere, add_interf; simpl. - apply SetRegReg.add_1. red. apply OrderedRegReg.eq_refl. + apply SetRegReg.add_1. auto. Qed. Lemma add_interf_incl: @@ -177,7 +177,7 @@ Lemma add_interf_mreg_correct: interfere_mreg x y (add_interf_mreg x y g). Proof. intros. unfold interfere_mreg, add_interf_mreg; simpl. - apply SetRegMreg.add_1. red. apply OrderedRegMreg.eq_refl. + apply SetRegMreg.add_1. auto. Qed. Lemma add_interf_mreg_incl: @@ -214,17 +214,17 @@ Definition add_intf1 (r1m2: reg * mreg) (u: Regset.t) : Regset.t := Regset.add (fst r1m2) u. Definition all_interf_regs (g: graph) : Regset.t := - SetRegReg.fold _ add_intf2 + SetRegReg.fold add_intf2 g.(interf_reg_reg) - (SetRegMreg.fold _ add_intf1 + (SetRegMreg.fold add_intf1 g.(interf_reg_mreg) Regset.empty). Lemma in_setregreg_fold: forall g r1 r2 u, SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u -> - Regset.In r1 (SetRegReg.fold _ add_intf2 g u) /\ - Regset.In r2 (SetRegReg.fold _ add_intf2 g u). + Regset.In r1 (SetRegReg.fold add_intf2 g u) /\ + Regset.In r2 (SetRegReg.fold add_intf2 g u). Proof. set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u). assert (forall l r1 r2 u, @@ -235,7 +235,7 @@ Proof. elim H; intro. inversion H0. auto. apply IHl. destruct a as [a1 a2]. elim H; intro. inversion H0; subst. - red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 r2. + red in H2. simpl in H2. destruct H2. subst r1 r2. right; unfold add_intf2', add_intf2; simpl; split. apply Regset.add_1. auto. apply Regset.add_2. apply Regset.add_1. auto. @@ -250,7 +250,7 @@ Qed. Lemma in_setregreg_fold': forall g r u, Regset.In r u -> - Regset.In r (SetRegReg.fold _ add_intf2 g u). + Regset.In r (SetRegReg.fold add_intf2 g u). Proof. intros. exploit in_setregreg_fold. eauto. intros [A B]. eauto. @@ -259,7 +259,7 @@ Qed. Lemma in_setregmreg_fold: forall g r1 mr2 u, SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u -> - Regset.In r1 (SetRegMreg.fold _ add_intf1 g u). + Regset.In r1 (SetRegMreg.fold add_intf1 g u). Proof. set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u). assert (forall l r1 mr2 u, @@ -269,7 +269,7 @@ Proof. elim H; intro. inversion H0. auto. apply IHl with mr2. destruct a as [a1 a2]. elim H; intro. inversion H0; subst. - red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 mr2. + red in H2. simpl in H2. destruct H2. subst r1 mr2. right; unfold add_intf1', add_intf1; simpl. apply Regset.add_1; auto. tauto. diff --git a/backend/Kildall.v b/backend/Kildall.v index b4445ae..188a23f 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -108,7 +108,7 @@ End DATAFLOW_SOLVER. Module Type NODE_SET. - Variable t: Set. + Variable t: Type. Variable add: positive -> t -> t. Variable pick: t -> option (positive * t). Variable initial: positive -> t. @@ -147,7 +147,7 @@ Variable entrypoints: list (positive * L.t). - A worklist of program points that remain to be considered. *) -Record state : Set := +Record state : Type := mkstate { st_in: PMap.t L.t; st_wrk: NS.t }. (** Kildall's algorithm, in pseudo-code, is as follows: @@ -663,7 +663,7 @@ End Backward_Dataflow_Solver. Module Type ORDERED_TYPE_WITH_TOP. - Variable t: Set. + Variable t: Type. Variable ge: t -> t -> Prop. Variable top: t. Hypothesis top_ge: forall x, ge top x. @@ -736,7 +736,7 @@ Definition result := PMap.t L.t. - A worklist of program points that remain to be considered. *) -Record state : Set := mkstate +Record state : Type := mkstate { st_in: result; st_wrk: list positive }. (** The ``extended basic block'' algorithm, in pseudo-code, is as follows: @@ -1167,7 +1167,7 @@ Module NodeSetForward <: NODE_SET. rewrite positive_rec_succ. rewrite PositiveSetFacts.add_iff. elim (Plt_succ_inv _ _ H0); intro. right. apply H. auto. - left. red. red. auto. + left. auto. Qed. End NodeSetForward. diff --git a/backend/LTL.v b/backend/LTL.v index 0db5495..3a61e6d 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -34,7 +34,7 @@ Require Import Conventions. Definition node := positive. -Inductive instruction: Set := +Inductive instruction: Type := | Lnop: node -> instruction | Lop: operation -> list loc -> loc -> node -> instruction | Lload: memory_chunk -> addressing -> list loc -> loc -> node -> instruction @@ -44,9 +44,9 @@ Inductive instruction: Set := | Lcond: condition -> list loc -> node -> node -> instruction | Lreturn: option loc -> instruction. -Definition code: Set := PTree.t instruction. +Definition code: Type := PTree.t instruction. -Record function: Set := mkfunction { +Record function: Type := mkfunction { fn_sig: signature; fn_params: list loc; fn_stacksize: Z; @@ -103,7 +103,7 @@ Definition postcall_locs (ls: locset) : locset := (** LTL execution states. *) -Inductive stackframe : Set := +Inductive stackframe : Type := | Stackframe: forall (res: loc) (**r where to store the result *) (f: function) (**r calling function *) @@ -112,7 +112,7 @@ Inductive stackframe : Set := (pc: node), (**r program point in calling function *) stackframe. -Inductive state : Set := +Inductive state : Type := | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r function currently executing *) diff --git a/backend/LTLin.v b/backend/LTLin.v index 4c87c0d..10b7d83 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -41,7 +41,7 @@ Definition label := positive. transfer control to the given code label. Labels are explicitly inserted in the instruction list as pseudo-instructions [Llabel]. *) -Inductive instruction: Set := +Inductive instruction: Type := | Lop: operation -> list loc -> loc -> instruction | Lload: memory_chunk -> addressing -> list loc -> loc -> instruction | Lstore: memory_chunk -> addressing -> list loc -> loc -> instruction @@ -52,9 +52,9 @@ Inductive instruction: Set := | Lcond: condition -> list loc -> label -> instruction | Lreturn: option loc -> instruction. -Definition code: Set := list instruction. +Definition code: Type := list instruction. -Record function: Set := mkfunction { +Record function: Type := mkfunction { fn_sig: signature; fn_params: list loc; fn_stacksize: Z; @@ -109,7 +109,7 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := code sequences [c] (suffixes of the code of the current function). *) -Inductive stackframe : Set := +Inductive stackframe : Type := | Stackframe: forall (res: loc) (**r where to store the result *) (f: function) (**r calling function *) @@ -118,7 +118,7 @@ Inductive stackframe : Set := (c: code), (**r program point in calling function *) stackframe. -Inductive state : Set := +Inductive state : Type := | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r function currently executing *) diff --git a/backend/Linear.v b/backend/Linear.v index 34d6e5c..e025407 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -35,7 +35,7 @@ Require Import Conventions. Definition label := positive. -Inductive instruction: Set := +Inductive instruction: Type := | Lgetstack: slot -> mreg -> instruction | Lsetstack: mreg -> slot -> instruction | Lop: operation -> list mreg -> mreg -> instruction @@ -48,9 +48,9 @@ Inductive instruction: Set := | Lcond: condition -> list mreg -> label -> instruction | Lreturn: instruction. -Definition code: Set := list instruction. +Definition code: Type := list instruction. -Record function: Set := mkfunction { +Record function: Type := mkfunction { fn_sig: signature; fn_stacksize: Z; fn_code: code @@ -163,7 +163,7 @@ Definition return_regs (caller callee: locset) : locset := (** Linear execution states. *) -Inductive stackframe: Set := +Inductive stackframe: Type := | Stackframe: forall (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) @@ -171,7 +171,7 @@ Inductive stackframe: Set := (c: code), (**r program point in calling function *) stackframe. -Inductive state: Set := +Inductive state: Type := | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r function currently executing *) diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index b385429..c24d370 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -193,7 +193,7 @@ Proof. generalize EQ0; clear EQ0. caseEq (check_reachable f reach x); intros; inv EQ0. exploit check_reachable_correct; eauto. intro. exploit nodeset_of_list_correct; eauto. intros [A [B C]]. - rewrite B in H2. destruct H2. elim (Nodeset.empty_1 pc H2). auto. + rewrite B in H2. destruct H2. elim (Nodeset.empty_1 H2). auto. Qed. Lemma enumerate_norepet: diff --git a/backend/Locations.v b/backend/Locations.v index ca2f527..295df28 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -42,7 +42,7 @@ Require Export Machregs. cannot reside in hardware registers, as determined by the calling conventions. *) -Inductive slot: Set := +Inductive slot: Type := | Local: Z -> typ -> slot | Incoming: Z -> typ -> slot | Outgoing: Z -> typ -> slot. @@ -108,7 +108,7 @@ Qed. (** Locations are just the disjoint union of machine registers and activation record slots. *) -Inductive loc : Set := +Inductive loc : Type := | R: mreg -> loc | S: slot -> loc. diff --git a/backend/Mach.v b/backend/Mach.v index 3f25137..0bb2442 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -49,7 +49,7 @@ Require Import Locations. Definition label := positive. -Inductive instruction: Set := +Inductive instruction: Type := | Mgetstack: int -> typ -> mreg -> instruction | Msetstack: mreg -> int -> typ -> instruction | Mgetparam: int -> typ -> mreg -> instruction @@ -65,7 +65,7 @@ Inductive instruction: Set := Definition code := list instruction. -Record function: Set := mkfunction +Record function: Type := mkfunction { fn_sig: signature; fn_code: code; fn_stacksize: Z; diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 25819f7..aa17cd4 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -51,7 +51,7 @@ Require Stacklayout. values. Like location sets (see module [Locations]), overlap can occur. *) -Definition frame : Set := typ -> Z -> val. +Definition frame : Type := typ -> Z -> val. Definition typ_eq: forall (ty1 ty2: typ), {ty1=ty2} + {ty1<>ty2}. Proof. decide equality. Defined. @@ -154,7 +154,7 @@ End FRAME_ACCESSES. (** Mach execution states. *) -Inductive stackframe: Set := +Inductive stackframe: Type := | Stackframe: forall (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) @@ -162,7 +162,7 @@ Inductive stackframe: Set := (fr: frame), (**r frame state in calling function *) stackframe. -Inductive state: Set := +Inductive state: Type := | State: forall (stack: list stackframe) (**r call stack *) (f: function) (**r function currently executing *) diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 4417cc6..876f558 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -86,7 +86,7 @@ Definition extcall_arguments (** Mach execution states. *) -Inductive stackframe: Set := +Inductive stackframe: Type := | Stackframe: forall (f: block) (**r pointer to calling function *) (sp: val) (**r stack pointer in calling function *) @@ -94,7 +94,7 @@ Inductive stackframe: Set := (c: code), (**r program point in calling function *) stackframe. -Inductive state: Set := +Inductive state: Type := | State: forall (stack: list stackframe) (**r call stack *) (f: block) (**r pointer to current function *) diff --git a/backend/RTL.v b/backend/RTL.v index 5fad2f2..344d271 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -44,7 +44,7 @@ Require Import Registers. Definition node := positive. -Inductive instruction: Set := +Inductive instruction: Type := | Inop: node -> instruction (** No operation -- just branch to the successor. *) | Iop: operation -> list reg -> reg -> node -> instruction @@ -80,9 +80,9 @@ Inductive instruction: Set := (it has no successor). It returns the value of the given register, or [Vundef] if none is given. *) -Definition code: Set := PTree.t instruction. +Definition code: Type := PTree.t instruction. -Record function: Set := mkfunction { +Record function: Type := mkfunction { fn_sig: signature; fn_params: list reg; fn_stacksize: Z; @@ -152,7 +152,7 @@ a function call in progress. [rs] is the state of registers in the calling function. *) -Inductive stackframe : Set := +Inductive stackframe : Type := | Stackframe: forall (res: reg) (**r where to store the result *) (c: code) (**r code of calling function *) @@ -161,7 +161,7 @@ Inductive stackframe : Set := (rs: regset), (**r register state in calling function *) stackframe. -Inductive state : Set := +Inductive state : Type := | State: forall (stack: list stackframe) (**r call stack *) (c: code) (**r current code *) diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 709dc78..65e873e 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -36,7 +36,7 @@ Open Local Scope string_scope. The mapping for let-bound variables is initially empty and updated during translation of expressions, when crossing a [Elet] binding. *) -Record mapping: Set := mkmapping { +Record mapping: Type := mkmapping { map_vars: PTree.t reg; map_letvars: list reg }. @@ -45,7 +45,7 @@ Record mapping: Set := mkmapping { current state of the control-flow graph for the function being translated, as well as sources of fresh RTL registers and fresh CFG nodes. *) -Record state: Set := mkstate { +Record state: Type := mkstate { st_nextreg: positive; st_nextnode: positive; st_code: code; @@ -104,25 +104,25 @@ Qed. We now define this monadic encoding -- the ``state and error'' monad -- as well as convenient syntax to express monadic computations. *) -Inductive res (A: Set) (s: state): Set := +Inductive res (A: Type) (s: state): Type := | Error: Errors.errmsg -> res A s | OK: A -> forall (s': state), state_incr s s' -> res A s. Implicit Arguments OK [A s]. Implicit Arguments Error [A s]. -Definition mon (A: Set) : Set := forall (s: state), res A s. +Definition mon (A: Type) : Type := forall (s: state), res A s. -Definition ret (A: Set) (x: A) : mon A := +Definition ret (A: Type) (x: A) : mon A := fun (s: state) => OK x s (state_incr_refl s). Implicit Arguments ret [A]. -Definition error (A: Set) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. +Definition error (A: Type) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. Implicit Arguments error [A]. -Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B := +Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := fun (s: state) => match f s with | Error msg => Error msg @@ -135,7 +135,7 @@ Definition bind (A B: Set) (f: mon A) (g: A -> mon B) : mon B := Implicit Arguments bind [A B]. -Definition bind2 (A B C: Set) (f: mon (A * B)) (g: A -> B -> mon C) : mon C := +Definition bind2 (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C) : mon C := bind f (fun xy => g (fst xy) (snd xy)). Implicit Arguments bind2 [A B C]. @@ -145,7 +145,7 @@ Notation "'do' X <- A ; B" := (bind A (fun X => B)) Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) (at level 200, X ident, Y ident, A at level 100, B at level 200). -Definition handle_error (A: Set) (f g: mon A) : mon A := +Definition handle_error (A: Type) (f g: mon A) : mon A := fun (s: state) => match f s with | OK a s' i => OK a s' i @@ -498,7 +498,7 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree) [nlist] if it terminates by an [exit n] construct. [rret] is the register where the return value of the function must be stored, if any. *) -Definition labelmap : Set := PTree.t node. +Definition labelmap : Type := PTree.t node. Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) (nexits: list node) (ngoto: labelmap) (nret: node) (rret: option reg) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index e6adeb0..8e61271 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -47,7 +47,7 @@ Require Import RTLgen. *) Remark bind_inversion: - forall (A B: Set) (f: mon A) (g: A -> mon B) + forall (A B: Type) (f: mon A) (g: A -> mon B) (y: B) (s1 s3: state) (i: state_incr s1 s3), bind f g s1 = OK y s3 i -> exists x, exists s2, exists i1, exists i2, @@ -61,7 +61,7 @@ Proof. Qed. Remark bind2_inversion: - forall (A B C: Set) (f: mon (A*B)) (g: A -> B -> mon C) + forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) (z: C) (s1 s3: state) (i: state_incr s1 s3), bind2 f g s1 = OK z s3 i -> exists x, exists y, exists s2, exists i1, exists i2, @@ -827,20 +827,6 @@ Inductive tr_function: CminorSel.function -> RTL.function -> Prop := (** We now show that the translation functions in module [RTLgen] satisfy the specifications given above as inductive predicates. *) -Scheme tr_expr_ind3 := Minimality for tr_expr Sort Prop - with tr_condition_ind3 := Minimality for tr_condition Sort Prop - with tr_exprlist_ind3 := Minimality for tr_exprlist Sort Prop. - -Definition tr_expr_condition_exprlist_ind3 - (c: code) - (P : mapping -> list reg -> expr -> node -> node -> reg -> Prop) - (P0 : mapping -> list reg -> condexpr -> node -> node -> node -> Prop) - (P1 : mapping -> list reg -> exprlist -> node -> node -> list reg -> Prop) := - fun a b c' d e f g h i j k l => - conj (tr_expr_ind3 c P P0 P1 a b c' d e f g h i j k l) - (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l) - (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l)). - Lemma tr_move_incr: forall s1 s2, state_incr s1 s2 -> forall ns rs nd rd, @@ -850,69 +836,35 @@ Proof. induction 2; econstructor; eauto with rtlg. Qed. -Lemma tr_expr_condition_exprlist_incr: - forall s1 s2, state_incr s1 s2 -> - (forall map pr a ns nd rd, - tr_expr s1.(st_code) map pr a ns nd rd -> - tr_expr s2.(st_code) map pr a ns nd rd) -/\(forall map pr a ns ntrue nfalse, - tr_condition s1.(st_code) map pr a ns ntrue nfalse -> - tr_condition s2.(st_code) map pr a ns ntrue nfalse) -/\(forall map pr al ns nd rl, - tr_exprlist s1.(st_code) map pr al ns nd rl -> - tr_exprlist s2.(st_code) map pr al ns nd rl). -Proof. - intros s1 s2 EXT. - pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). - apply tr_expr_condition_exprlist_ind3; intros; econstructor; eauto. - eapply tr_move_incr; eauto. - eapply tr_move_incr; eauto. -Qed. - Lemma tr_expr_incr: forall s1 s2, state_incr s1 s2 -> forall map pr a ns nd rd, tr_expr s1.(st_code) map pr a ns nd rd -> - tr_expr s2.(st_code) map pr a ns nd rd. -Proof. - intros. - exploit tr_expr_condition_exprlist_incr; eauto. - intros [A [B C]]. eauto. -Qed. - -Lemma tr_condition_incr: + tr_expr s2.(st_code) map pr a ns nd rd +with tr_condition_incr: forall s1 s2, state_incr s1 s2 -> forall map pr a ns ntrue nfalse, tr_condition s1.(st_code) map pr a ns ntrue nfalse -> - tr_condition s2.(st_code) map pr a ns ntrue nfalse. -Proof. - intros. - exploit tr_expr_condition_exprlist_incr; eauto. - intros [A [B C]]. eauto. -Qed. - -Lemma tr_exprlist_incr: + tr_condition s2.(st_code) map pr a ns ntrue nfalse +with tr_exprlist_incr: forall s1 s2, state_incr s1 s2 -> forall map pr al ns nd rl, tr_exprlist s1.(st_code) map pr al ns nd rl -> tr_exprlist s2.(st_code) map pr al ns nd rl. Proof. - intros. - exploit tr_expr_condition_exprlist_incr; eauto. - intros [A [B C]]. eauto. + intros s1 s2 EXT. + pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). + induction 1; econstructor; eauto. + eapply tr_move_incr; eauto. + eapply tr_move_incr; eauto. + intros s1 s2 EXT. + pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). + induction 1; econstructor; eauto. + intros s1 s2 EXT. + pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). + induction 1; econstructor; eauto. Qed. -Scheme expr_ind3 := Induction for expr Sort Prop - with condexpr_ind3 := Induction for condexpr Sort Prop - with exprlist_ind3 := Induction for exprlist Sort Prop. - -Definition expr_condexpr_exprlist_ind - (P1: expr -> Prop) (P2: condexpr -> Prop) (P3: exprlist -> Prop) := - fun a b c d e f g h i j k l => - conj (expr_ind3 P1 P2 P3 a b c d e f g h i j k l) - (conj (condexpr_ind3 P1 P2 P3 a b c d e f g h i j k l) - (exprlist_ind3 P1 P2 P3 a b c d e f g h i j k l)). - Lemma add_move_charact: forall s ns rs nd rd s' i, add_move rs rd nd s = OK ns s' i -> @@ -923,30 +875,33 @@ Proof. constructor. eauto with rtlg. Qed. -Lemma transl_expr_condexpr_list_charact: - (forall a map rd nd s ns s' pr INCR +Lemma transl_expr_charact: + forall a map rd nd s ns s' pr INCR (TR: transl_expr map a rd nd s = OK ns s' INCR) (WF: map_valid map s) (OK: target_reg_ok map pr a rd) (VALID: regs_valid pr s) (VALID2: reg_valid rd s), - tr_expr s'.(st_code) map pr a ns nd rd) -/\ - (forall a map ntrue nfalse s ns s' pr INCR + tr_expr s'.(st_code) map pr a ns nd rd + +with transl_condexpr_charact: + forall a map ntrue nfalse s ns s' pr INCR (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR) - (WF: map_valid map s) - (VALID: regs_valid pr s), - tr_condition s'.(st_code) map pr a ns ntrue nfalse) -/\ - (forall al map rl nd s ns s' pr INCR + (VALID: regs_valid pr s) + (WF: map_valid map s), + tr_condition s'.(st_code) map pr a ns ntrue nfalse + +with transl_exprlist_charact: + forall al map rl nd s ns s' pr INCR (TR: transl_exprlist map al rl nd s = OK ns s' INCR) (WF: map_valid map s) (OK: target_regs_ok map pr al rl) (VALID1: regs_valid pr s) (VALID2: regs_valid rl s), - tr_exprlist s'.(st_code) map pr al ns nd rl). + tr_exprlist s'.(st_code) map pr al ns nd rl. + Proof. - apply expr_condexpr_exprlist_ind; intros; try (monadInv TR). + induction a; intros; try (monadInv TR). (* Evar *) generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1. econstructor; eauto. @@ -955,31 +910,31 @@ Proof. (* Eop *) inv OK. econstructor; eauto with rtlg. - eapply H; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. (* Eload *) inv OK. econstructor; eauto with rtlg. - eapply H; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. (* Econdition *) inv OK. econstructor; eauto with rtlg. - eapply H; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. - eapply H0; eauto with rtlg. constructor; auto. + eapply transl_expr_charact; eauto with rtlg. constructor; auto. apply tr_expr_incr with s0; auto. - eapply H1; eauto with rtlg. constructor; auto. + eapply transl_expr_charact; eauto with rtlg. constructor; auto. (* Elet *) inv OK. econstructor. eapply new_reg_not_in_map; eauto with rtlg. - eapply H; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. - eapply H0. eauto. + eapply transl_expr_charact. eauto. apply add_letvar_valid; eauto with rtlg. constructor; auto. red; unfold reg_in_map. simpl. intros [[id A] | [B | C]]. - elim H1. left; exists id; auto. + elim H. left; exists id; auto. subst x. apply valid_fresh_absurd with rd s. auto. eauto with rtlg. - elim H1. right; auto. + elim H. right; auto. eauto with rtlg. eauto with rtlg. (* Eletvar *) generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0. @@ -989,56 +944,41 @@ Proof. eapply add_move_charact; eauto. monadInv EQ1. +(* Conditions *) + induction a; intros; try (monadInv TR). + (* CEtrue *) constructor. (* CEfalse *) constructor. (* CEcond *) econstructor; eauto with rtlg. - eapply H; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. (* CEcondition *) econstructor. - eapply H; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. apply tr_condition_incr with s1; auto. - eapply H0; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. apply tr_condition_incr with s0; auto. - eapply H1; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. + +(* Lists *) + + induction al; intros; try (monadInv TR). (* Enil *) destruct rl; inv TR. constructor. (* Econs *) destruct rl; simpl in TR; monadInv TR. inv OK. econstructor. - eapply H; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. generalize (VALID2 r (in_eq _ _)). eauto with rtlg. apply tr_exprlist_incr with s0; auto. - eapply H0; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. apply regs_valid_cons. apply VALID2. auto with coqlib. auto. red; intros; apply VALID2; auto with coqlib. Qed. -Lemma transl_expr_charact: - forall a map rd nd s ns s' INCR - (TR: transl_expr map a rd nd s = OK ns s' INCR) - (WF: map_valid map s) - (OK: target_reg_ok map nil a rd) - (VALID2: reg_valid rd s), - tr_expr s'.(st_code) map nil a ns nd rd. -Proof. - destruct transl_expr_condexpr_list_charact as [A [B C]]. - intros. eapply A; eauto with rtlg. -Qed. - -Lemma transl_condexpr_charact: - forall a map ntrue nfalse s ns s' INCR - (TR: transl_condition map a ntrue nfalse s = OK ns s' INCR) - (WF: map_valid map s), - tr_condition s'.(st_code) map nil a ns ntrue nfalse. -Proof. - destruct transl_expr_condexpr_list_charact as [A [B C]]. - intros. eapply B; eauto with rtlg. -Qed. - Lemma tr_store_var_incr: forall s1 s2, state_incr s1 s2 -> forall map rs id ns nd, @@ -1076,7 +1016,7 @@ Lemma tr_stmt_incr: tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret. Proof. intros s1 s2 EXT. - destruct (tr_expr_condition_exprlist_incr s1 s2 EXT) as [A [B C]]. + generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3. pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). pose (STV := tr_store_var_incr s1 s2 EXT). pose (STOV := tr_store_optvar_incr s1 s2 EXT). @@ -1148,19 +1088,17 @@ Proof. apply tr_store_var_incr with s1; auto with rtlg. eapply store_var_charact; eauto. (* Sstore *) - destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]]. econstructor; eauto with rtlg. - eapply P3; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. apply tr_expr_incr with s3; eauto with rtlg. - eapply P1; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. (* Scall *) - destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]]. assert (state_incr s0 s3) by eauto with rtlg. assert (state_incr s3 s6) by eauto with rtlg. econstructor; eauto with rtlg. - eapply P1; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. apply tr_exprlist_incr with s6. auto. - eapply P3; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg. apply regs_valid_cons; eauto with rtlg. apply regs_valid_incr with s1; eauto with rtlg. @@ -1169,13 +1107,12 @@ Proof. apply tr_store_optvar_incr with s4; eauto with rtlg. eapply store_optvar_charact; eauto with rtlg. (* Stailcall *) - destruct transl_expr_condexpr_list_charact as [A [B C]]. assert (RV: regs_valid (x :: nil) s1). apply regs_valid_cons; eauto with rtlg. econstructor; eauto with rtlg. - eapply A; eauto with rtlg. + eapply transl_expr_charact; eauto with rtlg. apply tr_exprlist_incr with s4; auto. - eapply C; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. diff --git a/backend/Registers.v b/backend/Registers.v index c3d04d6..fceb7c2 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -24,7 +24,7 @@ Require Import Ordered. Require Import FSets. Require FSetAVL. -Definition reg: Set := positive. +Definition reg: Type := positive. Module Reg. @@ -41,14 +41,14 @@ Module Regmap := PMap. Set Implicit Arguments. Definition regmap_optget - (A: Set) (or: option reg) (dfl: A) (rs: Regmap.t A) : A := + (A: Type) (or: option reg) (dfl: A) (rs: Regmap.t A) : A := match or with | None => dfl | Some r => Regmap.get r rs end. Definition regmap_optset - (A: Set) (or: option reg) (v: A) (rs: Regmap.t A) : Regmap.t A := + (A: Type) (or: option reg) (v: A) (rs: Regmap.t A) : Regmap.t A := match or with | None => rs | Some r => Regmap.set r v rs diff --git a/backend/Stacking.v b/backend/Stacking.v index 158af8f..182c322 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -34,7 +34,7 @@ Require Import Stacklayout. (** Computation the frame offset for the given component of the frame. The component is expressed by the following [frame_index] sum type. *) -Inductive frame_index: Set := +Inductive frame_index: Type := | FI_link: frame_index | FI_retaddr: frame_index | FI_local: Z -> typ -> frame_index diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index a7560d0..d5819f7 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -955,7 +955,7 @@ Proof. exists ls'; exists rs'. split. assumption. split. intros. elim H2; intros. subst r. apply (agree_unused_reg _ _ _ _ _ D). - rewrite <- number_within_bounds. auto. omega. auto. + rewrite <- number_within_bounds. auto. auto. auto. split. intros. simpl in H2. apply C. tauto. assumption. Qed. @@ -1051,7 +1051,7 @@ End FRAME_PROPERTIES. Section LABELS. Remark find_label_fold_right: - forall (A: Set) (fn: A -> Mach.code -> Mach.code) lbl, + forall (A: Type) (fn: A -> Mach.code -> Mach.code) lbl, (forall x k, Mach.find_label lbl (fn x k) = Mach.find_label lbl k) -> forall (args: list A) k, Mach.find_label lbl (List.fold_right fn k args) = Mach.find_label lbl k. Proof. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index b88dd50..1bafc35 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -51,7 +51,7 @@ Variable tf: Mach.function. Hypothesis TRANSF_F: transf_function f = OK tf. Lemma wt_fold_right: - forall (A: Set) (f: A -> code -> code) (k: code) (l: list A), + forall (A: Type) (f: A -> code -> code) (k: code) (l: list A), (forall x k', In x l -> wt_instrs k' -> wt_instrs (f x k')) -> wt_instrs k -> wt_instrs (List.fold_right f k l). diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 8e97e1a..791db37 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -574,8 +574,8 @@ Proof. exploit loadv_lessdef; eauto. intros [v' [LOAD' VLD]]. left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. - eapply exec_Iload; eauto. rewrite <- ADDR'. - apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply regset_set; auto. (* store *) @@ -586,8 +586,8 @@ Proof. exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD. intros [m'1 [STORE' MLD']]. left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split. - eapply exec_Istore; eauto. rewrite <- ADDR'. - apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore with (a := a'). eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. eauto. destruct a; simpl in H1; try discriminate. econstructor; eauto. eapply match_stacksize_store; eauto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 49bf894..08f5f6c 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -268,16 +268,18 @@ Proof. (* Lload *) rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. left; econstructor; split. - eapply exec_Lload; eauto. + eapply exec_Lload with (a := a). rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eauto. econstructor; eauto. (* Lstore *) rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. left; econstructor; split. - eapply exec_Lstore; eauto. + eapply exec_Lstore with (a := a). rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eauto. econstructor; eauto. (* Lcall *) left; econstructor; split. |