diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /backend/LTLintyping.v | |
parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) | |
download | compcert-355b4abcee015c3fae9ac5653c25259e104a886c.tar.gz compcert-355b4abcee015c3fae9ac5653c25259e104a886c.zip |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/LTLintyping.v')
-rw-r--r-- | backend/LTLintyping.v | 104 |
1 files changed, 104 insertions, 0 deletions
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v new file mode 100644 index 00000000..06c50f8b --- /dev/null +++ b/backend/LTLintyping.v @@ -0,0 +1,104 @@ +(** Typing rules for LTLin. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Op. +Require Import RTL. +Require Import Locations. +Require Import LTLin. +Require Import Conventions. + +(** The following predicates define a type system for LTLin similar to that + of LTL. *) + +Section WT_INSTR. + +Variable funsig: signature. + +Inductive wt_instr : instruction -> Prop := + | wt_Lopmove: + forall r1 r, + Loc.type r1 = Loc.type r -> loc_acceptable r1 -> loc_acceptable r -> + wt_instr (Lop Omove (r1 :: nil) r) + | wt_Lop: + forall op args res, + op <> Omove -> + (List.map Loc.type args, Loc.type res) = type_of_operation op -> + locs_acceptable args -> loc_acceptable res -> + wt_instr (Lop op args res) + | wt_Lload: + forall chunk addr args dst, + List.map Loc.type args = type_of_addressing addr -> + Loc.type dst = type_of_chunk chunk -> + locs_acceptable args -> loc_acceptable dst -> + wt_instr (Lload chunk addr args dst) + | wt_Lstore: + forall chunk addr args src, + List.map Loc.type args = type_of_addressing addr -> + Loc.type src = type_of_chunk chunk -> + locs_acceptable args -> loc_acceptable src -> + wt_instr (Lstore chunk addr args src) + | wt_Lcall: + forall sig ros args res, + match ros with inl r => Loc.type r = Tint | inr s => True end -> + List.map Loc.type args = sig.(sig_args) -> + Loc.type res = match sig.(sig_res) with None => Tint | Some ty => ty end -> + match ros with inl r => loc_acceptable r | inr s => True end -> + locs_acceptable args -> loc_acceptable res -> + wt_instr (Lcall sig ros args res) + | wt_Ltailcall: + forall sig ros args, + match ros with inl r => Loc.type r = Tint | inr s => True end -> + List.map Loc.type args = sig.(sig_args) -> + match ros with inl r => loc_acceptable r | inr s => True end -> + locs_acceptable args -> + sig.(sig_res) = funsig.(sig_res) -> + Conventions.tailcall_possible sig -> + wt_instr (Ltailcall sig ros args) + | wt_Lalloc: + forall arg res, + Loc.type arg = Tint -> Loc.type res = Tint -> + loc_acceptable arg -> loc_acceptable res -> + wt_instr (Lalloc arg res) + | wt_Llabel: forall lbl, + wt_instr (Llabel lbl) + | wt_Lgoto: forall lbl, + wt_instr (Lgoto lbl) + | wt_Lcond: + forall cond args lbl, + List.map Loc.type args = type_of_condition cond -> + locs_acceptable args -> + wt_instr (Lcond cond args lbl) + | wt_Lreturn: + forall optres, + option_map Loc.type optres = funsig.(sig_res) -> + match optres with None => True | Some r => loc_acceptable r end -> + wt_instr (Lreturn optres). + +Definition wt_code (c: code) : Prop := + forall i, In i c -> wt_instr i. + +End WT_INSTR. + +Record wt_function (f: function): Prop := + mk_wt_function { + wt_params: + List.map Loc.type f.(fn_params) = f.(fn_sig).(sig_args); + wt_acceptable: + locs_acceptable f.(fn_params); + wt_norepet: + Loc.norepet f.(fn_params); + wt_instrs: + wt_code f.(fn_sig) f.(fn_code) +}. + +Inductive wt_fundef: fundef -> Prop := + | wt_fundef_external: forall ef, + wt_fundef (External ef) + | wt_function_internal: forall f, + wt_function f -> + wt_fundef (Internal f). + +Definition wt_program (p: program): Prop := + forall i f, In (i, f) (prog_funct p) -> wt_fundef f. |