diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /backend/Machtyping.v | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) | |
download | compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.tar.gz compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.zip |
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
1- new register allocator (+ live range splitting, spilling&reloading, etc)
based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Machtyping.v')
-rw-r--r-- | backend/Machtyping.v | 108 |
1 files changed, 0 insertions, 108 deletions
diff --git a/backend/Machtyping.v b/backend/Machtyping.v deleted file mode 100644 index 2dc19be0..00000000 --- a/backend/Machtyping.v +++ /dev/null @@ -1,108 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Type system for the Mach intermediate language. *) - -Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Op. -Require Import Locations. -Require Import Conventions. -Require Import Mach. - -(** * Typing rules *) - -Inductive wt_instr : instruction -> Prop := - | wt_Mlabel: - forall lbl, - wt_instr (Mlabel lbl) - | wt_Mgetstack: - forall ofs ty r, - mreg_type r = ty -> - wt_instr (Mgetstack ofs ty r) - | wt_Msetstack: - forall ofs ty r, - mreg_type r = ty -> - wt_instr (Msetstack r ofs ty) - | wt_Mgetparam: - forall ofs ty r, - mreg_type r = ty -> - wt_instr (Mgetparam ofs ty r) - | wt_Mopmove: - forall r1 r, - mreg_type r1 = mreg_type r -> - wt_instr (Mop Omove (r1 :: nil) r) - | wt_Mop: - forall op args res, - op <> Omove -> - (List.map mreg_type args, mreg_type res) = type_of_operation op -> - wt_instr (Mop op args res) - | wt_Mload: - forall chunk addr args dst, - List.map mreg_type args = type_of_addressing addr -> - mreg_type dst = type_of_chunk chunk -> - wt_instr (Mload chunk addr args dst) - | wt_Mstore: - forall chunk addr args src, - List.map mreg_type args = type_of_addressing addr -> - mreg_type src = type_of_chunk chunk -> - wt_instr (Mstore chunk addr args src) - | wt_Mcall: - forall sig ros, - match ros with inl r => mreg_type r = Tint | inr s => True end -> - wt_instr (Mcall sig ros) - | wt_Mtailcall: - forall sig ros, - tailcall_possible sig -> - match ros with inl r => mreg_type r = Tint | inr s => True end -> - wt_instr (Mtailcall sig ros) - | wt_Mbuiltin: - forall ef args res, - List.map mreg_type args = (ef_sig ef).(sig_args) -> - mreg_type res = proj_sig_res (ef_sig ef) -> - wt_instr (Mbuiltin ef args res) - | wt_Mannot: - forall ef args, - ef_reloads ef = false -> - wt_instr (Mannot ef args) - | wt_Mgoto: - forall lbl, - wt_instr (Mgoto lbl) - | wt_Mcond: - forall cond args lbl, - List.map mreg_type args = type_of_condition cond -> - wt_instr (Mcond cond args lbl) - | wt_Mjumptable: - forall arg tbl, - mreg_type arg = Tint -> - list_length_z tbl * 4 <= Int.max_unsigned -> - wt_instr (Mjumptable arg tbl) - | wt_Mreturn: - wt_instr Mreturn. - -Record wt_function (f: function) : Prop := mk_wt_function { - wt_function_instrs: - forall instr, In instr f.(fn_code) -> wt_instr instr; - wt_function_stacksize: - 0 <= f.(fn_stacksize) <= Int.max_unsigned -}. - -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, Gfun f) (prog_defs p) -> wt_fundef f. |