From 7717d9e5f781a0b0d79f72c5439cf822f4ea78d0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 1 May 2013 09:22:49 +0000 Subject: Coq-defined equality functions for Allocation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2225 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocation.v | 40 ++++++++++++++++------------------------ backend/Allocproof.v | 4 ++-- common/AST.v | 23 ++++++++++++++++++++--- extraction/extraction.v | 11 ----------- ia32/Op.v | 16 +++++++++++----- lib/Coqlib.v | 7 +++++++ 6 files changed, 56 insertions(+), 45 deletions(-) diff --git a/backend/Allocation.v b/backend/Allocation.v index 8674335..e4d0972 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -127,14 +127,6 @@ Definition check_succ (s: node) (b: LTL.bblock) : bool := | _ => false end. -Parameter eq_operation: forall (x y: operation), {x=y} + {x<>y}. -Parameter eq_addressing: forall (x y: addressing), {x=y} + {x<>y}. -Parameter eq_opt_addressing: forall (x y: option addressing), {x=y} + {x<>y}. -Parameter eq_condition: forall (x y: condition), {x=y} + {x<>y}. -Parameter eq_chunk: forall (x y: memory_chunk), {x=y} + {x<>y}. -Parameter eq_external_function: forall (x y: external_function), {x=y} + {x<>y}. -Parameter eq_signature: forall (x y: signature), {x=y} + {x<>y}. - Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) (at level 200, X ident, A at level 100, B at level 200) : option_monad_scope. @@ -205,15 +197,15 @@ Definition pair_instr_block let (mv1, b1) := extract_moves nil b in match b1 with | Lload chunk' addr' args' dst' :: b2 => - if eq_chunk chunk Mint64 then - assertion (eq_chunk chunk' Mint32); + if chunk_eq chunk Mint64 then + assertion (chunk_eq chunk' Mint32); let (mv2, b3) := extract_moves nil b2 in match b3 with | Lload chunk'' addr'' args'' dst'' :: b4 => let (mv3, b5) := extract_moves nil b4 in - assertion (eq_chunk chunk'' Mint32); + assertion (chunk_eq chunk'' Mint32); assertion (eq_addressing addr addr'); - assertion (eq_opt_addressing (offset_addressing addr (Int.repr 4)) (Some addr'')); + assertion (option_eq eq_addressing (offset_addressing addr (Int.repr 4)) (Some addr'')); assertion (check_succ s b5); Some(BSload2 addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s) | _ => @@ -221,12 +213,12 @@ Definition pair_instr_block if (eq_addressing addr addr') then Some(BSload2_1 addr args dst mv1 args' dst' mv2 s) else - (assertion (eq_opt_addressing (offset_addressing addr (Int.repr 4)) (Some addr')); + (assertion (option_eq eq_addressing (offset_addressing addr (Int.repr 4)) (Some addr')); Some(BSload2_2 addr addr' args dst mv1 args' dst' mv2 s)) end else ( let (mv2, b3) := extract_moves nil b2 in - assertion (eq_chunk chunk chunk'); + assertion (chunk_eq chunk chunk'); assertion (eq_addressing addr addr'); assertion (check_succ s b3); Some(BSload chunk addr args dst mv1 args' dst' mv2 s)) @@ -238,20 +230,20 @@ Definition pair_instr_block let (mv1, b1) := extract_moves nil b in match b1 with | Lstore chunk' addr' args' src' :: b2 => - if eq_chunk chunk Mint64 then + if chunk_eq chunk Mint64 then let (mv2, b3) := extract_moves nil b2 in match b3 with | Lstore chunk'' addr'' args'' src'' :: b4 => - assertion (eq_chunk chunk' Mint32); - assertion (eq_chunk chunk'' Mint32); + assertion (chunk_eq chunk' Mint32); + assertion (chunk_eq chunk'' Mint32); assertion (eq_addressing addr addr'); - assertion (eq_opt_addressing (offset_addressing addr (Int.repr 4)) (Some addr'')); + assertion (option_eq eq_addressing (offset_addressing addr (Int.repr 4)) (Some addr'')); assertion (check_succ s b4); Some(BSstore2 addr addr'' args src mv1 args' src' mv2 args'' src'' s) | _ => None end else ( - assertion (eq_chunk chunk chunk'); + assertion (chunk_eq chunk chunk'); assertion (eq_addressing addr addr'); assertion (check_succ s b2); Some(BSstore chunk addr args src mv1 args' src' s)) @@ -262,7 +254,7 @@ Definition pair_instr_block match b1 with | Lcall sg' ros' :: b2 => let (mv2, b3) := extract_moves nil b2 in - assertion (eq_signature sg sg'); + assertion (signature_eq sg sg'); assertion (check_succ s b3); Some(BScall sg ros args res mv1 ros' mv2 s) | _ => None @@ -271,7 +263,7 @@ Definition pair_instr_block let (mv1, b1) := extract_moves nil b in match b1 with | Ltailcall sg' ros' :: b2 => - assertion (eq_signature sg sg'); + assertion (signature_eq sg sg'); Some(BStailcall sg ros args mv1 ros') | _ => None end @@ -280,11 +272,11 @@ Definition pair_instr_block match b1 with | Lbuiltin ef' args' res' :: b2 => let (mv2, b3) := extract_moves nil b2 in - assertion (eq_external_function ef ef'); + assertion (external_function_eq ef ef'); assertion (check_succ s b3); Some(BSbuiltin ef args res mv1 args' res' mv2 s) | Lannot ef' args' :: b2 => - assertion (eq_external_function ef ef'); + assertion (external_function_eq ef ef'); assertion (check_succ s b2); match ef with | EF_annot txt typ => Some(BSannot txt typ args res mv1 args' s) @@ -1132,7 +1124,7 @@ Definition check_entrypoints_aux (rtl: RTL.function) (ltl: LTL.function) (e1: eq (loc_parameters (RTL.fn_sig rtl)) e2); assertion (can_undef destroyed_at_function_entry e2); assertion (zeq (RTL.fn_stacksize rtl) (LTL.fn_stacksize ltl)); - assertion (eq_signature (RTL.fn_sig rtl) (LTL.fn_sig ltl)); + assertion (signature_eq (RTL.fn_sig rtl) (LTL.fn_sig ltl)); Some tt. Local Close Scope option_monad_scope. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 76e9744..a4aa861 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -297,7 +297,7 @@ Proof. destruct b0. MonadInv; UseParsingLemmas. destruct i; MonadInv; UseParsingLemmas. - destruct (eq_chunk m Mint64). + destruct (chunk_eq m Mint64). MonadInv; UseParsingLemmas. destruct b; MonadInv; UseParsingLemmas. destruct i; MonadInv; UseParsingLemmas. eapply ebs_load2; eauto. @@ -308,7 +308,7 @@ Proof. inv H. eapply ebs_load_dead; eauto. (* store *) destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. - destruct (eq_chunk m Mint64). + destruct (chunk_eq m Mint64). MonadInv; UseParsingLemmas. destruct b; MonadInv. destruct i; MonadInv; UseParsingLemmas. eapply ebs_store2; eauto. diff --git a/common/AST.v b/common/AST.v index 1f7f7d3..fb80b46 100644 --- a/common/AST.v +++ b/common/AST.v @@ -54,9 +54,8 @@ Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. Proof. decide equality. Defined. Global Opaque typ_eq. -Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}. -Proof. decide equality. apply typ_eq. Defined. -Global Opaque opt_typ_eq. +Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2} + := option_eq typ_eq. Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} := list_eq_dec typ_eq. @@ -78,6 +77,10 @@ Definition proj_sig_res (s: signature) : typ := | Some t => t end. +Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. +Proof. generalize opt_typ_eq, list_typ_eq; intros; decide equality. Defined. +Global Opaque signature_eq. + (** Memory accesses (load and store instructions) are annotated by a ``memory chunk'' indicating the type, size and signedness of the chunk of memory being accessed. *) @@ -93,6 +96,10 @@ Inductive memory_chunk : Type := | Mfloat64 (**r 64-bit double-precision float *) | Mfloat64al32. (**r 64-bit double-precision float, 4-aligned *) +Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}. +Proof. decide equality. Defined. +Global Opaque chunk_eq. + (** The type (integer/pointer or float) of a chunk. *) Definition type_of_chunk (c: memory_chunk) : typ := @@ -526,6 +533,16 @@ Definition ef_reloads (ef: external_function) : bool := | _ => true end. +(** Equality between external functions. Used in module [Allocation]. *) + +Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. +Proof. + generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. + decide equality. + apply list_eq_dec. decide equality. apply Float.eq_dec. +Defined. +Global Opaque external_function_eq. + (** Function definitions are the union of internal and external functions. *) Inductive fundef (F: Type): Type := diff --git a/extraction/extraction.v b/extraction/extraction.v index 804ccef..211569e 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -19,7 +19,6 @@ Require RTLgen. Require Inlining. Require ConstpropOp. Require Constprop. -Require Allocation. Require Compiler. (* Standard lib *) @@ -73,16 +72,6 @@ Extract Constant ConstpropOp.propagate_float_constants => Extract Constant Constprop.generate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 2". -(* Allocation *) -Extract Constant Allocation.eq_operation => "(=)". -Extract Constant Allocation.eq_addressing => "(=)". -Extract Constant Allocation.eq_opt_addressing => "(=)". -Extract Constant Allocation.eq_condition => "(=)". -Extract Constant Allocation.eq_chunk => "(=)". -Extract Constant Allocation.eq_external_function => "(=)". -Extract Constant Allocation.eq_signature => "(=)". -Extract Constant Allocation.regalloc => "Regalloc.regalloc". - (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". diff --git a/ia32/Op.v b/ia32/Op.v index 3dc1f77..998f34d 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -122,7 +122,14 @@ Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id of Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs). Definition Oaddimm (n: int) : operation := Olea (Aindexed n). -(** Comparison functions (used in module [CSE]). *) +(** Comparison functions (used in modules [CSE] and [Allocation]). *) + +Definition eq_condition (x y: condition) : {x=y} + {x<>y}. +Proof. + generalize Int.eq_dec; intro. + assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + decide equality. +Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. @@ -136,14 +143,13 @@ Proof. generalize Int.eq_dec; intro. generalize Float.eq_dec; intro. generalize Int64.eq_dec; intro. - assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. - assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. - assert (forall (x y: condition), {x=y}+{x<>y}). decide equality. decide equality. + apply peq. apply eq_addressing. + apply eq_condition. Defined. -Global Opaque eq_addressing eq_operation. +Global Opaque eq_condition eq_addressing eq_operation. (** * Evaluation functions *) diff --git a/lib/Coqlib.v b/lib/Coqlib.v index ce5d94e..58c9572 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -633,6 +633,13 @@ Qed. Set Implicit Arguments. +(** Comparing option types. *) + +Definition option_eq (A: Type) (eqA: forall (x y: A), {x=y} + {x<>y}): + forall (x y: option A), {x=y} + {x<>y}. +Proof. decide equality. Defined. +Global Opaque option_eq. + (** Mapping a function over an option type. *) Definition option_map (A B: Type) (f: A -> B) (x: option A) : option B := -- cgit v1.2.3