diff options
Diffstat (limited to 'backend/AST.v')
| -rw-r--r-- | backend/AST.v | 216 |
1 files changed, 216 insertions, 0 deletions
diff --git a/backend/AST.v b/backend/AST.v new file mode 100644 index 00000000..aae9e860 --- /dev/null +++ b/backend/AST.v @@ -0,0 +1,216 @@ +(** This file defines a number of data types and operations used in + the abstract syntax trees of many of the intermediate languages. *) + +Require Import Coqlib. + +Set Implicit Arguments. + +(** Identifiers (names of local variables, of global symbols and functions, + etc) are represented by the type [positive] of positive integers. *) + +Definition ident := positive. + +Definition ident_eq := peq. + +(** The languages are weakly typed, using only two types: [Tint] for + integers and pointers, and [Tfloat] for floating-point numbers. *) + +Inductive typ : Set := + | Tint : typ + | Tfloat : typ. + +Definition typesize (ty: typ) : Z := + match ty with Tint => 4 | Tfloat => 8 end. + +(** Additionally, function definitions and function calls are annotated + by function signatures indicating the number and types of arguments, + as well as the type of the returned value if any. These signatures + are used in particular to determine appropriate calling conventions + for the function. *) + +Record signature : Set := mksignature { + sig_args: list typ; + sig_res: option typ +}. + +(** 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. *) + +Inductive memory_chunk : Set := + | Mint8signed : memory_chunk (**r 8-bit signed integer *) + | Mint8unsigned : memory_chunk (**r 8-bit unsigned integer *) + | Mint16signed : memory_chunk (**r 16-bit signed integer *) + | Mint16unsigned : memory_chunk (**r 16-bit unsigned integer *) + | Mint32 : memory_chunk (**r 32-bit integer, or pointer *) + | Mfloat32 : memory_chunk (**r 32-bit single-precision float *) + | Mfloat64 : memory_chunk. (**r 64-bit double-precision float *) + +(** Comparison instructions can perform one of the six following comparisons + between their two operands. *) + +Inductive comparison : Set := + | Ceq : comparison (**r same *) + | Cne : comparison (**r different *) + | Clt : comparison (**r less than *) + | Cle : comparison (**r less than or equal *) + | Cgt : comparison (**r greater than *) + | Cge : comparison. (**r greater than or equal *) + +Definition negate_comparison (c: comparison): comparison := + match c with + | Ceq => Cne + | Cne => Ceq + | Clt => Cge + | Cle => Cgt + | Cgt => Cle + | Cge => Clt + end. + +Definition swap_comparison (c: comparison): comparison := + match c with + | Ceq => Ceq + | Cne => Cne + | Clt => Cgt + | Cle => Cge + | Cgt => Clt + | Cge => Cle + end. + +(** Whole programs consist of: +- a collection of function definitions (name and description); +- the name of the ``main'' function that serves as entry point in the program; +- a collection of global variable declarations (name and size in bytes). + +The type of function descriptions varies among the various intermediate +languages and is taken as parameter to the [program] type. The other parts +of whole programs are common to all languages. *) + +Record program (funct: Set) : Set := mkprogram { + prog_funct: list (ident * funct); + prog_main: ident; + prog_vars: list (ident * Z) +}. + +(** We now define a general iterator over programs that applies a given + code transformation function to all function descriptions and leaves + the other parts of the program unchanged. *) + +Section TRANSF_PROGRAM. + +Variable A B: Set. +Variable transf: A -> B. + +Fixpoint transf_program (l: list (ident * A)) : list (ident * B) := + match l with + | nil => nil + | (id, fn) :: rem => (id, transf fn) :: transf_program rem + end. + +Definition transform_program (p: program A) : program B := + mkprogram + (transf_program p.(prog_funct)) + p.(prog_main) + p.(prog_vars). + +Remark transf_program_functions: + forall fl i tf, + In (i, tf) (transf_program fl) -> + exists f, In (i, f) fl /\ transf f = tf. +Proof. + induction fl; simpl. + tauto. + destruct a. simpl. intros. + elim H; intro. exists a. split. left. congruence. congruence. + generalize (IHfl _ _ H0). intros [f [IN TR]]. + exists f. split. right. auto. auto. +Qed. + +Lemma transform_program_function: + forall p i tf, + In (i, tf) (transform_program p).(prog_funct) -> + exists f, In (i, f) p.(prog_funct) /\ transf f = tf. +Proof. + simpl. intros. eapply transf_program_functions; eauto. +Qed. + +End TRANSF_PROGRAM. + +(** The following is a variant of [transform_program] where the + code transformation function can fail and therefore returns an + option type. *) + +Section TRANSF_PARTIAL_PROGRAM. + +Variable A B: Set. +Variable transf_partial: A -> option B. + +Fixpoint transf_partial_program + (l: list (ident * A)) : option (list (ident * B)) := + match l with + | nil => Some nil + | (id, fn) :: rem => + match transf_partial fn with + | None => None + | Some fn' => + match transf_partial_program rem with + | None => None + | Some res => Some ((id, fn') :: res) + end + end + end. + +Definition transform_partial_program (p: program A) : option (program B) := + match transf_partial_program p.(prog_funct) with + | None => None + | Some fl => Some (mkprogram fl p.(prog_main) p.(prog_vars)) + end. + +Remark transf_partial_program_functions: + forall fl tfl i tf, + transf_partial_program fl = Some tfl -> + In (i, tf) tfl -> + exists f, In (i, f) fl /\ transf_partial f = Some tf. +Proof. + induction fl; simpl. + intros; injection H; intro; subst tfl; contradiction. + case a; intros id fn. intros until tf. + caseEq (transf_partial fn). + intros tfn TFN. + caseEq (transf_partial_program fl). + intros tfl1 TFL1 EQ. injection EQ; intro; clear EQ; subst tfl. + simpl. intros [EQ1|IN1]. + exists fn. intuition congruence. + generalize (IHfl _ _ _ TFL1 IN1). + intros [f [X Y]]. + exists f. intuition congruence. + intros; discriminate. + intros; discriminate. +Qed. + +Lemma transform_partial_program_function: + forall p tp i tf, + transform_partial_program p = Some tp -> + In (i, tf) tp.(prog_funct) -> + exists f, In (i, f) p.(prog_funct) /\ transf_partial f = Some tf. +Proof. + intros until tf. + unfold transform_partial_program. + caseEq (transf_partial_program (prog_funct p)). + intros. apply transf_partial_program_functions with l; auto. + injection H0; intros; subst tp. exact H1. + intros; discriminate. +Qed. + +Lemma transform_partial_program_main: + forall p tp, + transform_partial_program p = Some tp -> + tp.(prog_main) = p.(prog_main). +Proof. + intros p tp. unfold transform_partial_program. + destruct (transf_partial_program (prog_funct p)). + intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; reflexivity. + intro; discriminate. +Qed. + +End TRANSF_PARTIAL_PROGRAM. |