From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: 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 --- doc/backend.html | 250 -- doc/coqdoc.css | 62 + doc/index.html | 8561 ++---------------------------------------------------- doc/removeproofs | 2 +- doc/style.css | 4 +- 5 files changed, 334 insertions(+), 8545 deletions(-) delete mode 100644 doc/backend.html create mode 100644 doc/coqdoc.css (limited to 'doc') diff --git a/doc/backend.html b/doc/backend.html deleted file mode 100644 index e33896c..0000000 --- a/doc/backend.html +++ /dev/null @@ -1,250 +0,0 @@ - - - -The Compcert certified compiler back-end - - - - - - - - -

The Compcert certified compiler back-end

Commented Coq development

Version 0.2, 2006-01-07

- -

Introduction

- -

The Compcert back-end is a compiler that generates PowerPC assembly -code from a low-level intermediate language called Cminor and a -slightly more expressive intermediate language called Csharpminor. -The particularity of this compiler is that it is written mostly within -the specification language of the Coq proof assistant, and its -correctness --- the fact that the generated assembly code is -semantically equivalent to its source program --- was entirely proved -within the Coq proof assistant.

- -

A high-level overview of the Compcert back-end and its proof of -correctness can be found in the following paper:

-Xavier Leroy, Formal -certification of a compiler back-end, or: programming a compiler with -a proof assistant. Proceedings of the POPL 2006 symposium. - -

This Web site gives a commented listing of the underlying Coq -specifications and proofs. Proof scripts and the parts of the -compiler written directly in Caml are omitted. This development is a -work in progress; some parts may have changed since the overview paper -above was written.

- -

This document and all Coq source files referenced from it are -copyright 2005, 2006 Institut National de Recherche en Informatique et -en Automatique (INRIA) and distributed under the terms of the GNU General Public -License version 2.

- -

Libraries, algorithms, data structures

- -

Coqlib: addendum to the Coq standard library. - (Coq source file with proofs: - Coqlib.v.) -
Maps: finite maps. - (Coq source file with proofs: - Maps.v.) -
Sets: finite sets. -
Union-find: representation of -equivalence classes. - (Coq source file with proofs: - union_find.v.) -
Inclusion: tactics to prove list inclusions. -
AST: identifiers, whole programs and other -common elements of abstract syntaxes. - (Coq source file with proofs: - AST.v.) -
Integers: machine integers. - (Coq source file with proofs: - Integers.v.) -
Floats: machine floating-point numbers. -
Mem: the memory model. -
Globalenvs: global execution environments. -
Op: operators, addressing modes and their -semantics. -
Ordered: construction of -ordered types. -
Lattice: construction of -semi-lattices. -
Kildall: resolution of dataflow -inequations by fixpoint iteration. -

- -

Source, intermediate and target languages: syntax and semantics

- -

Csharpminor: low-level structured language. -
Cminor: low-level structured -language, with explicit stack allocation of certain local variables. -
RTL: register transfer language (3-address -code, control-flow graph, infinitely many pseudo-registers).
-See also: Registers (representation of -pseudo-registers). -
LTL: location transfer language (3-address -code, control-flow graph, finitely many physical registers, infinitely -many stack slots).
-See also: Locations (representation of -locations). -
Linear: like LTL, but the CFG is -replaced by a linear list of instructions with explicit branches and labels. -
Mach: like Linear, with a more concrete -view of the activation record.
-See also: an alternate semantics for the same -syntax is given in Machabstr.
-
PPC: abstract syntax for PowerPC assembly -code. -

- -

Compiler passes

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Pass	Source & target	Compiler code	Correctness proof
Recognition of operators and addressing modes	Csharpminor to Cminor	Cmconstr	Cmconstrproof
Stack allocation of local variables whose address is taken	Csharpminor to Cminor	Cminorgen	Cminorgenproof
Construction of the CFG, 3-address code generation	Cminor to RTL	RTLgen	RTLgenproof1 - RTLgenproof
Constant propagation	RTL to RTL	Constprop	Constpropproof
Common subexpression elimination	RTL to RTL	CSE	CSEproof
Register allocation by coloring of an interference graph	RTL to LTL	Conventions - InterfGraph - Coloring - Parallelmove - Allocation	- - Coloringproof - Allocproof_aux - Allocproof
Branch tunneling	LTL to LTL	Tunneling	Tunnelingproof
Linearization of the CFG	LTL to Linear	Linearize	Linearizeproof
Laying out the activation records	Linear to Mach	Stacking	Stackingproof
Storing the activation records in memory	Mach to Mach	(none) -	Machabstr2mach
Emission of PowerPC assembly	Mach to PPC	PPCgen	PPCgenproof1 - PPCgenproof

- -

Type systems

- -Trivial type systems are used to statically capture well-formedness -conditions on the intermediate languages. -

RTLtyping: typing for RTL + type -reconstruction. -
LTLtyping: typing for LTL. -
Lineartyping: typing for Linear. -
Machtyping: typing for Mach. -

-Proofs that compiler passes are type-preserving: -

Alloctyping_aux and - Alloctyping (register allocation). -
Tunnelingtyping (branch tunneling). -
Lineartyping (branch tunneling). -
Stackingtyping (layout of activation records). -

- -

All together

- -

Main: composing the passes together; the -final semantic preservation theorems. -

- -

Xavier.Leroy@inria.fr

- - - diff --git a/doc/coqdoc.css b/doc/coqdoc.css new file mode 100644 index 0000000..f2ae96d --- /dev/null +++ b/doc/coqdoc.css @@ -0,0 +1,62 @@ +body { + color: black; + background: white; + margin-left: 15%; + margin-right: 5%; +} + +#main a.idref:visited {color : #416DFF; text-decoration : none; } +#main a.idref:link {color : #416DFF; text-decoration : none; } +#main a.idref:hover {text-decoration : none; } +#main a.idref:active {text-decoration : none; } + +#main a.modref:visited {color : #416DFF; text-decoration : none; } +#main a.modref:link {color : #416DFF; text-decoration : none; } +#main a.modref:hover {text-decoration : none; } +#main a.modref:active {text-decoration : none; } + +#main .keyword { color : #cf1d1d } + +#main .doc { + margin-left: -5%; +} + +#main span.docright { + position: absolute; + left: 60%; + width: 40% +} + +h1.libtitle { + font-size: 2em; + margin-left: -15%; + margin-right: -5%; + text-align: center +} + +h1 { + font-size: 1.5em; +} +h2 { + font-size: 1.17em; +} + +h1, h2 { + font-family: sans-serif; +} + +.doc code { + color: #008000; +} + +/* Pied de page */ + +hr { margin-left: -15%; margin-right:-5%; } + +#footer { font-size: 0.83em; + font-family: sans-serif; } + +#footer a:visited { color: blue; } +#footer a:link { text-decoration: none; + color: #888888; } + diff --git a/doc/index.html b/doc/index.html index 33afe85..709767b 100644 --- a/doc/index.html +++ b/doc/index.html @@ -1,8295 +1,270 @@ - - -Index - + + + +The Compcert certified compiler back-end + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Global Index

(3806 entries)

Axiom Index

(39 entries)

Lemma Index

(1753 entries)

Constructor Index

(700 entries)

Inductive Index

(155 entries)

Definition Index

(1017 entries)

Module Index

(78 entries)

Library Index

(64 entries)

Global Index

A

B

C

D

E

F

G

H

-half_modulus [definition, in lib.Integers]
-has_type [definition, in backend.Values]
-has_type_list [definition, in backend.Values]
-head_but_last [definition, in backend.Parallelmove]
-high_bound [definition, in backend.Mem]
-high_bound_alloc [lemma, in backend.Mem]
-high_bound_free [lemma, in backend.Mem]
-high_bound_store [lemma, in backend.Mem]
-high_half_signed [axiom, in backend.PPC]
-high_half_signed_type [axiom, in backend.PPC]
-high_half_signed_zero [lemma, in backend.PPCgenproof1]
-high_half_unsigned [axiom, in backend.PPC]
-high_half_unsigned_type [axiom, in backend.PPC]
-high_half_unsigned_zero [lemma, in backend.PPCgenproof1]
-high_s [definition, in backend.PPCgen]
-high_u [definition, in backend.PPCgen]
-

I

K

-Kildall [library]
-kill_loads [definition, in backend.CSE]
-kill_load_eqs [definition, in backend.CSE]
-kill_load_eqs_incl [lemma, in backend.CSEproof]
-kill_load_eqs_ops [lemma, in backend.CSEproof]
-kill_load_satisfiable [lemma, in backend.CSEproof]
-

L

M

N

O

P

R

S

T

U

V

W

X

Z

_

-_ [constructor, in backend.Lineartyping]
-_ [constructor, in backend.LTLtyping]
-

Axiom Index

A

-abs [in lib.Floats]
-add [in lib.Floats]
-addf_commut [in lib.Floats]
-

C

-cmp [in lib.Floats]
-cmp_ge_gt_eq [in lib.Floats]
-cmp_le_lt_eq [in lib.Floats]
-cmp_ne_eq [in lib.Floats]
-

D

-div [in lib.Floats]
-

E

-eq_dec [in lib.Floats]
-eq_zero_false [in lib.Floats]
-eq_zero_true [in lib.Floats]
-extensionality [in lib.Coqlib]
-

F

-float [in lib.Floats]
-floatofint [in lib.Floats]
-floatofintu [in lib.Floats]
-

G

-graph_coloring [in backend.Coloring]
-

H

-high_half_signed [in backend.PPC]
-high_half_signed_type [in backend.PPC]
-high_half_unsigned [in backend.PPC]
-high_half_unsigned_type [in backend.PPC]
-

I

-intoffloat [in lib.Floats]
-

L

-low_half_signed [in backend.PPC]
-low_half_signed_type [in backend.PPC]
-low_half_unsigned [in backend.PPC]
-low_half_unsigned_type [in backend.PPC]
-low_high_half_signed [in backend.PPC]
-low_high_half_unsigned [in backend.PPC]
-

M

-more_likely [in backend.RTLgen]
-mul [in lib.Floats]
-

N

-neg [in lib.Floats]
-neg_mul_distr_l [in lib.Integers]
-neg_mul_distr_r [in lib.Integers]
-

O

-one [in lib.Floats]
-

P

-proof_irrelevance [in lib.Coqlib]
-

S

-singleoffloat [in lib.Floats]
-singleoffloat_idem [in lib.Floats]
-sub [in lib.Floats]
-subf_addf_opp [in lib.Floats]
-

Z

-zero [in lib.Floats]
-

Lemma Index

A

B

C

D

E

F

G

H

-high_bound_alloc [in backend.Mem]
-high_bound_free [in backend.Mem]
-high_bound_store [in backend.Mem]
-high_half_signed_zero [in backend.PPCgenproof1]
-high_half_unsigned_zero [in backend.PPCgenproof1]
-

I

-identify_aux_decomp [in lib.union_find]
-identify_base_a_maps_to_b [in lib.union_find]
-identify_base_b_canon [in lib.union_find]
-identify_base_order_wf [in lib.union_find]
-identify_base_repr [in lib.union_find]
-identify_base_repr_order [in lib.union_find]
-identify_base_sameclass_1 [in lib.union_find]
-identify_base_sameclass_2 [in lib.union_find]
-included_consistent [in backend.RTLtyping]
-included_identify [in backend.RTLtyping]
-included_mapped [in backend.RTLtyping]
-included_mapped_forall [in backend.RTLtyping]
-included_refl [in backend.RTLtyping]
-included_trans [in backend.RTLtyping]
-inclusion_theorem [in lib.Inclusion]
-incl_app_inv_l [in lib.Coqlib]
-incl_app_inv_r [in lib.Coqlib]
-incl_cons_inv [in lib.Coqlib]
-incl_dst [in backend.Alloctyping_aux]
-incl_find_label [in backend.Machtyping]
-incl_nil [in backend.Alloctyping_aux]
-incl_same_head [in lib.Coqlib]
-incl_src [in backend.Alloctyping_aux]
-index_arg_valid [in backend.Stackingproof]
-index_float_callee_save_inj [in backend.Conventions]
-index_float_callee_save_pos [in backend.Conventions]
-index_float_callee_save_pos2 [in backend.Conventions]
-index_inj [in lib.Maps]
-index_inj [in backend.Locations]
-index_inj [in lib.Maps]
-index_int_callee_save_inj [in backend.Conventions]
-index_int_callee_save_pos [in backend.Conventions]
-index_int_callee_save_pos2 [in backend.Conventions]
-index_local_valid [in backend.Stackingproof]
-index_saved_float_valid [in backend.Stackingproof]
-index_saved_int_valid [in backend.Stackingproof]
-index_val_init_frame [in backend.Stackingproof]
-Indst_noOverlap_aux [in backend.Parallelmove]
-Ingetsrc_swap [in backend.Parallelmove]
-Ingetsrc_swap2 [in backend.Parallelmove]
-initial_state_invariant [in backend.Kildall]
-initmem_nullptr [in backend.Globalenvs]
-initmem_undef [in backend.Globalenvs]
-init_mapping_wf [in backend.RTLgenproof1]
-init_mem_transf [in backend.Globalenvs]
-init_mem_transf_partial [in backend.Globalenvs]
-init_state_wf [in backend.RTLgen]
-inject_incr_refl [in backend.Mem]
-inject_incr_trans [in backend.Mem]
-insert_bin_included [in lib.Inclusion]
-insert_lenv_lookup1 [in backend.Cmconstrproof]
-insert_lenv_lookup2 [in backend.Cmconstrproof]
-instr_at_incr [in backend.RTLgenproof1]
-interfere_incl [in backend.Coloringproof]
-interfere_mreg_incl [in backend.Coloringproof]
-interfere_sym [in backend.InterfGraph]
-interf_graph_correct_1 [in backend.Coloringproof]
-interf_graph_correct_2 [in backend.Coloringproof]
-interf_graph_correct_3 [in backend.Coloringproof]
-intval_correct [in backend.Constpropproof]
-int_add_no_overflow [in backend.Machabstr2mach]
-int_callee_save_bound [in backend.Linearizetyping]
-int_callee_save_norepet [in backend.Conventions]
-int_callee_save_not_destroyed [in backend.Conventions]
-int_callee_save_type [in backend.Conventions]
-int_float_callee_save_disjoint [in backend.Conventions]
-int_local_slot_bound [in backend.Linearizetyping]
-inv_eval_Eop_0 [in backend.Cmconstrproof]
-inv_eval_Eop_1 [in backend.Cmconstrproof]
-inv_eval_Eop_2 [in backend.Cmconstrproof]
-in_bounds_exten [in backend.Mem]
-in_bounds_holds [in backend.Mem]
-in_bounds_inject [in backend.Mem]
-in_cons_noteq [in backend.Allocproof_aux]
-in_incr_refl [in backend.Kildall]
-in_incr_trans [in backend.Kildall]
-In_Indst [in backend.Parallelmove]
-in_move__in_srcdst [in backend.Alloctyping_aux]
-In_norepet [in backend.Allocproof_aux]
-in_notin_diff [in backend.Locations]
-In_noTmp_notempo [in backend.Parallelmove]
-in_or_insert_bin [in lib.Inclusion]
-in_or_notin_callstack [in backend.Machabstr2mach]
-In_permute_app_head [in lib.Inclusion]
-in_range_range [in lib.Integers]
-in_remove_head [in lib.Inclusion]
-In_SD_diff [in backend.Parallelmove]
-In_SD_diff' [in backend.Parallelmove]
-In_SD_no_o [in backend.Parallelmove]
-in_split_move [in backend.Alloctyping_aux]
-in_xelements [in lib.Maps]
-in_xkeys [in lib.Maps]
-ireg_eq [in backend.PPC]
-ireg_of_is_data_reg [in backend.PPCgenproof1]
-ireg_of_not_GPR1 [in backend.PPCgenproof1]
-ireg_of_not_GPR2 [in backend.PPCgenproof1]
-ireg_val [in backend.PPCgenproof1]
-isfalse_not_istrue [in backend.Values]
-istrue_not_isfalse [in backend.Values]
-is_goto_block_correct [in backend.Tunnelingproof]
-is_label_correct [in backend.PPC]
-is_label_correct [in backend.Mach]
-is_label_correct [in backend.Linear]
-is_move_operation_correct [in backend.Op]
-is_power2_correct [in lib.Integers]
-is_power2_range [in lib.Integers]
-is_power2_rng [in lib.Integers]
-is_tail_cons_left [in backend.Linearizeproof]
-is_tail_exec_instr [in backend.Linearizeproof]
-is_tail_exec_instrs [in backend.Linearizeproof]
-is_tail_find_label [in backend.Linearizeproof]
-is_tail_in [in backend.Linearizeproof]
-iterate_base [in backend.Kildall]
-iterate_incr [in backend.Kildall]
-iterate_solution [in backend.Kildall]
-iterate_step [in backend.Kildall]
-

K

-kill_load_eqs_incl [in backend.CSEproof]
-kill_load_eqs_ops [in backend.CSEproof]
-kill_load_satisfiable [in backend.CSEproof]
-

L

M

N

O

P

R

S

T

U

-undef_is_bool [in backend.Values]
-unfold_transf_function [in backend.Stackingproof]
-unique_labels_lin_block [in backend.Linearizeproof]
-unique_labels_lin_function [in backend.Linearizeproof]
-unique_labels_lin_rec [in backend.Linearizeproof]
-unroll_positive_rec [in lib.Coqlib]
-unsigned_range [in lib.Integers]
-unsigned_range_2 [in lib.Integers]
-unsigned_repr [in lib.Integers]
-unsplit_move [in backend.Parallelmove]
-update_instr_extends [in backend.RTLgenproof1]
-update_instr_incr [in backend.RTLgenproof1]
-update_instr_wf [in backend.RTLgen]
-update_o [in backend.Mem]
-update_s [in backend.Mem]
-

V

W

X

Z

Constructor Index

A

B

-Bcall [in backend.LTL]
-Bcond [in backend.LTL]
-Bgetstack [in backend.LTL]
-Bgoto [in backend.LTL]
-bind_parameters_cons [in backend.Csharpminor]
-bind_parameters_nil [in backend.Csharpminor]
-Bload [in backend.LTL]
-bool_of_val_int_true [in backend.Values]
-Bop [in backend.LTL]
-Bot [in lib.Lattice]
-Bot_except [in lib.Lattice]
-Breturn [in backend.LTL]
-Bsetstack [in backend.LTL]
-Bstore [in backend.LTL]
-

C

-callstack_dom_cons [in backend.Machabstr2mach]
-callstack_dom_nil [in backend.Machabstr2mach]
-callstack_linked_cons [in backend.Machabstr2mach]
-callstack_linked_nil [in backend.Machabstr2mach]
-callstack_linked_one [in backend.Machabstr2mach]
-CARRY [in backend.PPC]
-Ccomp [in backend.Op]
-Ccompf [in backend.Op]
-Ccompimm [in backend.Op]
-Ccompu [in backend.Op]
-Ccompuimm [in backend.Op]
-CEcond [in backend.Cminor]
-CEcondition [in backend.Cminor]
-CEfalse [in backend.Cminor]
-Ceq [in backend.AST]
-CEtrue [in backend.Cminor]
-Cge [in backend.AST]
-Cgt [in backend.AST]
-Cint [in backend.PPC]
-Cle [in backend.AST]
-Clt [in backend.AST]
-Cmasknotzero [in backend.Op]
-Cmaskzero [in backend.Op]
-Cne [in backend.AST]
-Cnotcompf [in backend.Op]
-Cont [in backend.LTL]
-Cont [in backend.Mem]
-content_inject_cont [in backend.Mem]
-content_inject_datum16 [in backend.Mem]
-content_inject_datum32 [in backend.Mem]
-content_inject_datum64 [in backend.Mem]
-content_inject_datum8 [in backend.Mem]
-content_inject_undef [in backend.Mem]
-CRbit_0 [in backend.PPC]
-CRbit_1 [in backend.PPC]
-CRbit_2 [in backend.PPC]
-CRbit_3 [in backend.PPC]
-CR0_0 [in backend.PPC]
-CR0_1 [in backend.PPC]
-CR0_2 [in backend.PPC]
-CR0_3 [in backend.PPC]
-csr_case1 [in backend.Constprop]
-csr_case2 [in backend.Constprop]
-csr_default [in backend.Constprop]
-Csymbol_high_signed [in backend.PPC]
-Csymbol_high_unsigned [in backend.PPC]
-Csymbol_low_signed [in backend.PPC]
-Csymbol_low_unsigned [in backend.PPC]
-CTR [in backend.PPC]
-

D

-Datum16 [in backend.Mem]
-Datum32 [in backend.Mem]
-Datum64 [in backend.Mem]
-Datum8 [in backend.Mem]
-divu_case1 [in backend.Cmconstr]
-divu_default [in backend.Cmconstr]
-dstepp_refl [in backend.Parallelmove]
-dstepp_trans [in backend.Parallelmove]
-dstep_nop [in backend.Parallelmove]
-dstep_pop [in backend.Parallelmove]
-dstep_pop_loop [in backend.Parallelmove]
-dstep_push [in backend.Parallelmove]
-dstep_start [in backend.Parallelmove]
-

E

F

G

I

-Incoming [in backend.Locations]
-Inj [in lib.Lattice]
-Inop [in backend.RTL]
-insert_lenv_S [in backend.Cmconstrproof]
-insert_lenv_0 [in backend.Cmconstrproof]
-IR [in backend.PPC]
-is_tail_cons [in backend.Linearizeproof]
-is_tail_refl [in backend.Linearizeproof]
-IT1 [in backend.Locations]
-IT2 [in backend.Locations]
-IT3 [in backend.Locations]
-

L

M

N

-n [in backend.Op]
-Node [in lib.Maps]
-node [in lib.Inclusion]
-norepet_cons [in backend.Locations]
-norepet_nil [in backend.Locations]
-notint_case1 [in backend.Cmconstr]
-notint_case2 [in backend.Cmconstr]
-notint_case3 [in backend.Cmconstr]
-notint_default [in backend.Cmconstr]
-notin_callstack_cons [in backend.Machabstr2mach]
-notin_callstack_nil [in backend.Machabstr2mach]
-Novalue [in backend.Constprop]
-

O

P

R

S

T

-target_regs_cons [in backend.RTLgenproof1]
-target_regs_nil [in backend.RTLgenproof1]
-target_reg_immut_var [in backend.RTLgenproof1]
-Tfloat [in backend.AST]
-Tint [in backend.AST]
-tReg [in backend.RTLtyping]
-tTy [in backend.RTLtyping]
-

U

-Undef [in backend.Mem]
-

V

-val_cons_inject [in backend.Mem]
-val_content_inject_base [in backend.Mem]
-val_content_inject_8 [in backend.Mem]
-val_inject_float [in backend.Mem]
-val_inject_int [in backend.Mem]
-val_inject_ptr [in backend.Mem]
-val_nil_inject [in backend.Mem]
-vars_vals_cons [in backend.Cminorgenproof]
-vars_vals_nil [in backend.Cminorgenproof]
-Var_global [in backend.Cminorgen]
-Var_local [in backend.Cminorgen]
-Var_stack_array [in backend.Cminorgen]
-Var_stack_scalar [in backend.Cminorgen]
-Vfloat [in backend.Values]
-Vint [in backend.Values]
-vlma_cons [in backend.Constpropproof]
-vlma_nil [in backend.Constpropproof]
-Vptr [in backend.Values]
-Vundef [in backend.Values]
-

W

-wt_Bgetstack [in backend.LTLtyping]
-wt_Bop [in backend.LTLtyping]
-wt_Bopmove [in backend.LTLtyping]
-wt_Bopundef [in backend.LTLtyping]
-wt_Bsetstack [in backend.LTLtyping]
-wt_Inop [in backend.RTLtyping]
-wt_Iop [in backend.RTLtyping]
-wt_Iopmove [in backend.RTLtyping]
-wt_Iopundef [in backend.RTLtyping]
-wt_Lgetstack [in backend.Lineartyping]
-wt_Lop [in backend.Lineartyping]
-wt_Lopmove [in backend.Lineartyping]
-wt_Lopundef [in backend.Lineartyping]
-wt_Lsetstack [in backend.Lineartyping]
-wt_Mgetstack [in backend.Machtyping]
-wt_Mlabel [in backend.Machtyping]
-wt_Msetstack [in backend.Machtyping]
-

_

-_ [in backend.Lineartyping]
-_ [in backend.LTLtyping]
-

Inductive Index

A

-a [in backend.Op]
-a [in backend.Op]
-addf_cases [in backend.Cmconstr]
-addimm_cases [in backend.Cmconstr]
-addressing [in backend.Op]
-addressing_cases [in backend.Cmconstr]
-addr_strength_reduction_cases [in backend.Constprop]
-add_cases [in backend.Cmconstr]
-agree [in backend.Stackingproof]
-alloc_variables [in backend.Csharpminor]
-approx [in backend.Constprop]
-

B

-bin [in lib.Inclusion]
-bind_parameters [in backend.Csharpminor]
-block [in backend.LTL]
-block_contents [in backend.Mem]
-block_contents_inject [in backend.Mem]
-bool_of_val [in backend.Values]
-bounds [in backend.Lineartyping]
-

C

-callstack_dom [in backend.Machabstr2mach]
-callstack_invariant [in backend.Machabstr2mach]
-callstack_linked [in backend.Machabstr2mach]
-comparison [in backend.AST]
-condexpr [in backend.Cminor]
-condition [in backend.Op]
-cond_strength_reduction_cases [in backend.Constprop]
-constant [in backend.PPC]
-content [in backend.Mem]
-content_inject [in backend.Mem]
-cont_for_outcome [in backend.Linearizeproof]
-crbit [in backend.PPC]
-

D

-divu_cases [in backend.Cmconstr]
-dstep [in backend.Parallelmove]
-dstepp [in backend.Parallelmove]
-

E

-eval_expr [in backend.Csharpminor]
-eval_expr [in backend.Cminor]
-eval_static_condition_cases [in backend.Constprop]
-eval_static_operation_cases [in backend.Constprop]
-exec_instr [in backend.Machabstr]
-exec_instr [in backend.RTL]
-exec_instr [in backend.LTL]
-exec_instr [in backend.Linear]
-exec_instr [in backend.Mach]
-exec_step [in backend.PPC]
-exec_steps [in backend.PPC]
-exec_straight [in backend.PPCgenproof1]
-expr [in backend.Csharpminor]
-expr [in backend.Cminor]
-exprlist [in backend.Csharpminor]
-exprlist [in backend.Cminor]
-

F

-frame [in backend.Cminorgenproof]
-frame_env [in backend.Stacking]
-frame_index [in backend.Stacking]
-frame_match [in backend.Machabstr2mach]
-freg [in backend.PPC]
-function [in backend.Mach]
-function [in backend.Csharpminor]
-function [in backend.RTL]
-function [in backend.LTL]
-function [in backend.Cminor]
-function [in backend.Linear]
-

G

-genv [in backend.Globalenvs]
-get_slot [in backend.Machabstr]
-graph [in backend.InterfGraph]
-

I

-immediate [in backend.PPC]
-immediate [in backend.PPC]
-immediate [in backend.PPC]
-immediate [in backend.PPC]
-immediate [in backend.PPC]
-immediate [in backend.PPC]
-Incoming [in backend.LTLtyping]
-Incoming [in backend.Lineartyping]
-insert_lenv [in backend.Cmconstrproof]
-instruction [in backend.Linear]
-instruction [in backend.PPC]
-instruction [in backend.RTL]
-instruction [in backend.Mach]
-int [in lib.Integers]
-ireg [in backend.PPC]
-is_tail [in backend.Linearizeproof]
-

L

-list_forall2 [in lib.Coqlib]
-list_norepet [in lib.Coqlib]
-loc [in backend.Locations]
-local_variable [in backend.Csharpminor]
-

M

-mapping [in backend.RTLgen]
-map_wf [in backend.RTLgenproof1]
-match_callstack [in backend.Cminorgenproof]
-match_env [in backend.Cminorgenproof]
-match_env [in backend.RTLgenproof1]
-match_globalenvs [in backend.Cminorgenproof]
-match_var [in backend.Cminorgenproof]
-mem [in backend.Mem]
-memory_chunk [in backend.AST]
-memory_size [in backend.Mem]
-mem_inject [in backend.Mem]
-mreg [in backend.Locations]
-mulimm_cases [in backend.Cmconstr]
-mul_cases [in backend.Cmconstr]
-myT [in backend.RTLtyping]
-

N

-norepet [in backend.Locations]
-notint_cases [in backend.Cmconstr]
-notin_callstack [in backend.Machabstr2mach]
-numbering [in backend.CSE]
-

O

-operation [in backend.Csharpminor]
-operation [in backend.Op]
-op_strength_reduction_cases [in backend.Constprop]
-or_cases [in backend.Cmconstr]
-outcome [in backend.Cminor]
-outcome [in backend.LTL]
-outcome [in backend.PPC]
-outcome [in backend.Csharpminor]
-outcome_inject [in backend.Cminorgenproof]
-

P

-preg [in backend.PPC]
-program [in backend.AST]
-

R

-res [in backend.RTLgen]
-return_reg_ok [in backend.RTLgenproof1]
-rhs [in backend.CSE]
-rlw_state [in lib.Integers]
-rolm_cases [in backend.Cmconstr]
-

S

-set_slot [in backend.Machabstr]
-shift_cases [in backend.Cmconstr]
-signature [in backend.AST]
-slot [in backend.Locations]
-state [in backend.Kildall]
-state [in backend.RTLgen]
-state [in backend.Kildall]
-state_incr [in backend.RTLgenproof1]
-step [in backend.Parallelmove]
-stepp [in backend.Parallelmove]
-stmt [in backend.Csharpminor]
-stmt [in backend.Cminor]
-stmtlist [in backend.Csharpminor]
-stmtlist [in backend.Cminor]
-subf_cases [in backend.Cmconstr]
-sub_cases [in backend.Cmconstr]
-

T

-target_regs_ok [in backend.RTLgenproof1]
-target_reg_ok [in backend.RTLgenproof1]
-transl_code_at_pc [in backend.PPCgenproof]
-tree [in lib.Maps]
-typ [in backend.AST]
-t_ [in lib.Lattice]
-t_ [in lib.Lattice]
-

U

-unionfind [in lib.union_find]
-

V

-val [in backend.Values]
-val_content_inject [in backend.Mem]
-val_inject [in backend.Mem]
-val_list_inject [in backend.Mem]
-val_list_match_approx [in backend.Constpropproof]
-vars_vals_match [in backend.Cminorgenproof]
-var_info [in backend.Cminorgen]
-

W

-wt_block [in backend.LTLtyping]
-wt_function [in backend.RTLtyping]
-wt_function [in backend.Machtyping]
-wt_instr [in backend.Lineartyping]
-wt_instr [in backend.Machtyping]
-wt_instr [in backend.RTLtyping]
-

Definition Index

A

B

-base_case_Pmov_dec [in backend.Parallelmove]
-basic_block_list [in backend.Kildall]
-basic_block_map [in backend.Kildall]
-bbmap [in backend.Kildall]
-bind [in backend.RTLgen]
-bind [in backend.Cminorgen]
-bind2 [in backend.RTLgen]
-bin_A [in lib.Inclusion]
-bits_of_Z [in lib.Integers]
-bitwise_binop [in lib.Integers]
-block [in backend.Values]
-block_agree [in backend.Mem]
-block_contents_agree [in backend.Mem]
-block_contents_extends [in backend.Mem]
-bot [in lib.Lattice]
-bot [in lib.Lattice]
-bot [in backend.Constprop]
-bot [in lib.Sets]
-bot [in lib.Lattice]
-branch_target [in backend.Tunneling]
-branch_target_rec [in backend.Tunneling]
-build_compilenv [in backend.Cminorgen]
-

C

D

-decode [in backend.RTLtyping]
-def [in backend.Parallelmove]
-definite [in backend.RTLtyping]
-destroyed_at_call [in backend.Conventions]
-destroyed_at_call_regs [in backend.Conventions]
-diff [in backend.Locations]
-diff_dec [in backend.Parallelmove]
-disjoint [in backend.Locations]
-divf [in backend.Values]
-divf [in backend.Cmconstr]
-divs [in backend.Cmconstr]
-divs [in lib.Integers]
-divs [in backend.Values]
-divu [in backend.Cmconstr]
-divu [in backend.Values]
-divu [in lib.Integers]
-divu_match [in backend.Cmconstr]
-Done_well_formed [in backend.Allocproof_aux]
-drop1 [in backend.Conventions]
-drop2 [in backend.Conventions]
-

E

-elements [in lib.Sets]
-elements [in lib.Maps]
-elt [in lib.Maps]
-elt [in backend.RTLtyping]
-elt [in lib.Sets]
-elt [in lib.union_find]
-elt [in lib.union_find]
-elt [in lib.union_find]
-elt [in lib.Maps]
-elt [in lib.Maps]
-elt [in lib.Maps]
-elt_eq [in lib.Maps]
-elt_eq [in lib.Maps]
-elt_eq [in lib.Maps]
-elt_eq [in lib.Maps]
-empty [in lib.Sets]
-empty [in lib.Maps]
-empty [in lib.union_find]
-empty [in backend.RTLtyping]
-empty [in backend.Globalenvs]
-empty [in backend.Mem]
-empty_block [in backend.Mem]
-empty_env [in backend.Csharpminor]
-empty_frame [in backend.Machabstr]
-empty_graph [in backend.InterfGraph]
-empty_numbering [in backend.CSE]
-encode [in backend.RTLtyping]
-enumerate [in backend.Linearize]
-env [in backend.Csharpminor]
-Env [in backend.Parallelmove]
-env [in backend.Cminor]
-eq [in backend.Mach]
-eq [in lib.Ordered]
-eq [in backend.RTLtyping]
-eq [in backend.CSEproof]
-eq [in lib.Maps]
-eq [in backend.Locations]
-eq [in lib.Ordered]
-eq [in backend.Registers]
-eq [in lib.Ordered]
-eq [in backend.PPC]
-eq [in lib.Integers]
-eqm [in lib.Integers]
-eqmod [in lib.Integers]
-equation_holds [in backend.CSE]
-eq_block [in backend.Values]
-eq_list_valnum [in backend.CSE]
-eq_rhs [in backend.CSE]
-eq_valnum [in backend.CSE]
-error [in backend.RTLtyping]
-error [in backend.RTLgen]
-eval_addressing [in backend.Op]
-eval_addressing_total [in backend.Op]
-eval_compare_null [in backend.Op]
-eval_compare_null [in backend.Csharpminor]
-eval_condition [in backend.Op]
-eval_condition_total [in backend.Op]
-eval_exprlist_prop [in backend.Cminorgenproof]
-eval_expr_prop [in backend.Cminorgenproof]
-eval_funcall_prop [in backend.Cminorgenproof]
-eval_operation [in backend.Op]
-eval_operation [in backend.Csharpminor]
-eval_operation_total [in backend.Op]
-eval_static_condition [in backend.Constprop]
-eval_static_condition_match [in backend.Constprop]
-eval_static_operation [in backend.Constprop]
-eval_static_operation_match [in backend.Constprop]
-exec [in backend.Parallelmove]
-exec_blocks_prop [in backend.Linearizeproof]
-exec_blocks_prop [in backend.Tunnelingproof]
-exec_block_prop [in backend.Linearizeproof]
-exec_block_prop [in backend.Tunnelingproof]
-exec_function_body_prop [in backend.Machabstr2mach]
-exec_function_body_prop [in backend.PPCgenproof]
-exec_function_body_prop [in backend.Machtyping]
-exec_function_prop [in backend.Stackingproof]
-exec_function_prop [in backend.Machtyping]
-exec_function_prop [in backend.PPCgenproof]
-exec_function_prop [in backend.Constpropproof]
-exec_function_prop [in backend.Linearizeproof]
-exec_function_prop [in backend.Machabstr2mach]
-exec_function_prop [in backend.CSEproof]
-exec_function_prop [in backend.Tunnelingproof]
-exec_function_prop [in backend.Allocproof]
-exec_function_subject_reduction [in backend.RTLtyping]
-exec_instr [in backend.PPC]
-exec_instrs_prop [in backend.Allocproof]
-exec_instrs_prop [in backend.Tunnelingproof]
-exec_instrs_prop [in backend.Machabstr2mach]
-exec_instrs_prop [in backend.CSEproof]
-exec_instrs_prop [in backend.Constpropproof]
-exec_instrs_prop [in backend.Linearizeproof]
-exec_instr_prop [in backend.Allocproof]
-exec_instr_prop [in backend.Machabstr2mach]
-exec_instr_prop [in backend.Machtyping]
-exec_instr_prop [in backend.Constpropproof]
-exec_instr_prop [in backend.CSEproof]
-exec_instr_prop [in backend.Tunnelingproof]
-exec_instr_prop [in backend.Stackingproof]
-exec_instr_prop [in backend.Linearizeproof]
-exec_instr_prop [in backend.PPCgenproof]
-exec_instr_subject_reduction [in backend.RTLtyping]
-exec_program [in backend.Csharpminor]
-exec_program [in backend.LTL]
-exec_program [in backend.Cminor]
-exec_program [in backend.RTL]
-exec_program [in backend.Mach]
-exec_program [in backend.Machabstr]
-exec_program [in backend.Linear]
-exec_program [in backend.PPC]
-exec_stmtlist_prop [in backend.Cminorgenproof]
-exec_stmt_prop [in backend.Cminorgenproof]
-extends [in backend.Mem]
-extend_inject [in backend.Mem]
-

F

-find_funct [in backend.Globalenvs]
-find_function [in backend.LTL]
-find_function [in backend.Mach]
-find_function [in backend.RTL]
-find_function [in backend.Linear]
-find_function2 [in backend.Allocproof]
-find_funct_ptr [in backend.Globalenvs]
-find_instr [in backend.PPC]
-find_label [in backend.Mach]
-find_label [in backend.PPCgenproof]
-find_label [in backend.Linear]
-find_letvar [in backend.RTLgen]
-find_load [in backend.CSE]
-find_op [in backend.CSE]
-find_rhs [in backend.CSE]
-find_symbol [in backend.Globalenvs]
-find_symbol_offset [in backend.Op]
-find_valnum_rhs [in backend.CSE]
-find_var [in backend.RTLgen]
-fixpoint [in backend.Kildall]
-fixpoint [in backend.Kildall]
-fixpoint [in backend.Kildall]
-flatten [in lib.Inclusion]
-flatten_aux [in lib.Inclusion]
-floatcomp [in backend.PPCgen]
-floatofint [in backend.Values]
-floatofint [in backend.Cmconstr]
-floatofintu [in backend.Cmconstr]
-floatofintu [in backend.Values]
-float_callee_save [in backend.Lineartyping]
-float_callee_save_regs [in backend.Conventions]
-float_local [in backend.Lineartyping]
-float_param_regs [in backend.Conventions]
-fn_params_names [in backend.Csharpminor]
-fn_variables [in backend.Csharpminor]
-fn_vars_names [in backend.Csharpminor]
-fold [in lib.Sets]
-fold [in lib.Maps]
-fold2 [in backend.RTLtyping]
-for_all [in lib.Sets]
-frame [in backend.Machabstr]
-free [in backend.Mem]
-free_list [in backend.Mem]
-freg_of [in backend.PPCgen]
-function_bounds [in backend.Lineartyping]
-

G

-ge [in lib.Lattice]
-ge [in backend.CSE]
-ge [in lib.Lattice]
-ge [in backend.Constprop]
-ge [in lib.Lattice]
-ge [in lib.Sets]
-genv [in backend.Cminor]
-genv [in backend.LTL]
-genv [in backend.PPC]
-genv [in backend.Csharpminor]
-genv [in backend.RTL]
-genv [in backend.Mach]
-genv [in backend.Linear]
-get [in lib.Maps]
-get [in lib.Maps]
-get [in lib.Maps]
-Get [in backend.Parallelmove]
-get [in backend.Locations]
-get [in lib.Lattice]
-get [in lib.Maps]
-get [in backend.Parallelmove]
-get [in backend.RTLtyping]
-getdst [in backend.Parallelmove]
-getN [in backend.Mem]
-getsrc [in backend.Parallelmove]
-globalenv [in backend.Globalenvs]
-globalenv_initmem [in backend.Globalenvs]
-good_state [in backend.Kildall]
-goto_label [in backend.PPC]
-gpr_or_zero [in backend.PPC]
-graph_incl [in backend.InterfGraph]
-

H

-half_modulus [in lib.Integers]
-has_type [in backend.Values]
-has_type_list [in backend.Values]
-head_but_last [in backend.Parallelmove]
-high_bound [in backend.Mem]
-high_s [in backend.PPCgen]
-high_u [in backend.PPCgen]
-

I

-ident [in backend.AST]
-identify [in lib.union_find]
-identify_base [in lib.union_find]
-ident_eq [in backend.AST]
-ifthenelse [in backend.Cmconstr]
-included [in backend.RTLtyping]
-index [in backend.Locations]
-index [in lib.Maps]
-index [in lib.Maps]
-index_diff [in backend.Stackingproof]
-index_float_callee_save [in backend.Conventions]
-index_int_callee_save [in backend.Conventions]
-index_val [in backend.Stackingproof]
-index_valid [in backend.Stackingproof]
-init [in lib.Maps]
-init [in backend.Locations]
-init [in lib.Maps]
-init [in lib.Maps]
-init_frame [in backend.Machabstr]
-init_mapping [in backend.RTLgen]
-init_mem [in backend.Globalenvs]
-init_regs [in backend.RTL]
-init_state [in backend.RTLgen]
-inject_incr [in backend.Mem]
-insert_bin [in lib.Inclusion]
-interfere [in backend.InterfGraph]
-interfere_mreg [in backend.InterfGraph]
-interf_graph [in backend.Coloring]
-intoffloat [in backend.Cmconstr]
-intoffloat [in backend.Values]
-intval [in backend.Constprop]
-int_callee_save [in backend.Lineartyping]
-int_callee_save_regs [in backend.Conventions]
-int_local [in backend.Lineartyping]
-int_of_one_bits [in lib.Integers]
-int_param_regs [in backend.Conventions]
-in_bounds [in backend.Mem]
-in_incr [in backend.Kildall]
-in_range [in lib.Integers]
-ireg_of [in backend.PPCgen]
-is_basic_block_head [in backend.Kildall]
-is_bool [in backend.Values]
-is_data_reg [in backend.PPCgenproof1]
-is_false [in lib.Integers]
-is_false [in backend.Values]
-is_goto_block [in backend.Tunneling]
-is_label [in backend.PPC]
-is_label [in backend.Mach]
-is_label [in backend.Linear]
-is_move_operation [in backend.Op]
-is_power2 [in lib.Integers]
-is_rlw_mask [in lib.Integers]
-is_rlw_mask_rec [in lib.Integers]
-is_trivial_op [in backend.CSE]
-is_true [in lib.Integers]
-is_true [in backend.Values]
-iterate [in backend.Kildall]
-iter_step [in backend.Kildall]
-

K

-kill_loads [in backend.CSE]
-kill_load_eqs [in backend.CSE]
-

L

-label [in backend.Linear]
-label [in backend.PPC]
-label [in backend.Mach]
-label_pos [in backend.PPC]
-last [in backend.Parallelmove]
-lbl [in backend.Linearize]
-lbl [in backend.Linearize]
-leaf [in lib.Inclusion]
-leaf [in lib.Inclusion]
-leaf [in lib.Inclusion]
-letenv [in backend.Cminor]
-letenv [in backend.Csharpminor]
-lift [in backend.Cmconstr]
-lift_condexpr [in backend.Cmconstr]
-lift_expr [in backend.Cmconstr]
-lift_exprlist [in backend.Cmconstr]
-linearize_block [in backend.Linearize]
-linearize_body [in backend.Linearize]
-linearize_function [in backend.Linearize]
-link_invariant [in backend.Machtyping]
-listsLoc2Moves [in backend.Parallelmove]
-listsLoc2Moves [in backend.Allocation]
-list_disjoint [in lib.Coqlib]
-live0 [in backend.Allocproof]
-load [in backend.Mem]
-load [in backend.Cmconstr]
-loadimm [in backend.PPCgen]
-loadind [in backend.PPCgen]
-loadind_aux [in backend.PPCgen]
-loadv [in backend.Mem]
-load1 [in backend.PPC]
-load2 [in backend.PPC]
-load_contents [in backend.Mem]
-load_result [in backend.Values]
-load_stack [in backend.Mach]
-locset [in backend.LTL]
-locset [in backend.Linear]
-locs_acceptable [in backend.Conventions]
-locs_read_ok [in backend.Alloctyping]
-locs_write_ok [in backend.Alloctyping]
-loc_acceptable [in backend.Conventions]
-loc_arguments [in backend.Conventions]
-loc_arguments_rec [in backend.Conventions]
-loc_argument_acceptable [in backend.Conventions]
-loc_is_acceptable [in backend.Coloring]
-loc_parameters [in backend.Conventions]
-loc_read_ok [in backend.Alloctyping]
-loc_result [in backend.Conventions]
-loc_write_ok [in backend.Alloctyping]
-low_bound [in backend.Mem]
-low_s [in backend.PPCgen]
-low_u [in backend.PPCgen]
-lt [in lib.Integers]
-lt [in lib.Ordered]
-lt [in lib.Ordered]
-lt [in lib.Ordered]
-ltu [in lib.Integers]
-lub [in lib.Lattice]
-lub [in lib.Lattice]
-lub [in lib.Sets]
-lub [in lib.Lattice]
-lub [in backend.Constprop]
-

M

N

O

-offset_of_index [in backend.Stacking]
-offset_sp [in backend.Op]
-of_bool [in backend.Values]
-one [in lib.Integers]
-one_bits [in lib.Integers]
-option_fold2 [in backend.RTLtyping]
-option_map [in lib.Coqlib]
-op_strength_reduction [in backend.Constprop]
-op_strength_reduction_match [in backend.Constprop]
-or [in lib.Integers]
-or [in backend.Values]
-or [in backend.Cmconstr]
-ordered_pair [in backend.InterfGraph]
-orimm [in backend.PPCgen]
-or_match [in backend.Cmconstr]
-outcome_block [in backend.Csharpminor]
-outcome_block [in backend.Cminor]
-outcome_node [in backend.RTLgenproof]
-outcome_result_value [in backend.Cminor]
-outcome_result_value [in backend.Csharpminor]
-outgoing_slot [in backend.Lineartyping]
-outgoing_space [in backend.Lineartyping]
-overlap [in backend.Locations]
-overlap_aux [in backend.Locations]
-

P

-parallel_move [in backend.Allocation]
-parallel_move_order [in backend.Allocation]
-parameter_of_argument [in backend.Conventions]
-path [in backend.Parallelmove]
-peq [in lib.Coqlib]
-pexec [in backend.Parallelmove]
-Ple [in lib.Coqlib]
-Plt [in lib.Coqlib]
-plt [in lib.Coqlib]
-Pmov [in backend.Parallelmove]
-positive_rec [in lib.Coqlib]
-powerserie [in lib.Integers]
-predecessors [in backend.Kildall]
-preg_of [in backend.PPCgenproof1]
-program [in backend.LTL]
-program [in backend.Cminor]
-program [in backend.Linear]
-program [in backend.RTL]
-program [in backend.Csharpminor]
-program [in backend.PPC]
-program [in backend.Mach]
-propagate_succ [in backend.Kildall]
-propagate_successors [in backend.Kildall]
-propagate_succ_list [in backend.Kildall]
-Pstate [in backend.Kildall]
-p_move [in backend.Allocproof_aux]
-P_move [in backend.Parallelmove]
-

R

-R [in backend.Coloring]
-reachable [in backend.Linearize]
-reachable_aux [in backend.Linearize]
-reg [in backend.Registers]
-Reg [in backend.Parallelmove]
-regalloc [in backend.Coloring]
-regenv [in backend.RTLtyping]
-reglist [in backend.LTL]
-regmap_optget [in backend.Registers]
-regmap_optset [in backend.Registers]
-regset [in backend.Mach]
-regset [in backend.RTL]
-regset [in backend.PPC]
-regs_for [in backend.Allocation]
-regs_for_rec [in backend.Allocation]
-regs_match_approx [in backend.Constpropproof]
-regs_of_instr [in backend.Lineartyping]
-reg_for [in backend.Allocation]
-reg_fresh [in backend.RTLgenproof1]
-reg_in_map [in backend.RTLgenproof1]
-reg_list_dead [in backend.Allocation]
-reg_list_live [in backend.Allocation]
-reg_of_crbit [in backend.PPC]
-reg_option_live [in backend.Allocation]
-reg_sum_live [in backend.Allocation]
-reg_valid [in backend.RTLgenproof1]
-reg_valnum [in backend.CSE]
-remove [in lib.Sets]
-remove [in lib.Maps]
-remove_all_leaves [in lib.Inclusion]
-repet [in backend.RTLtyping]
-replace_last_s [in backend.Parallelmove]
-repr [in lib.union_find]
-repr [in lib.Integers]
-repr_aux [in lib.union_find]
-repr_order [in lib.union_find]
-repr_rec [in lib.union_find]
-reserve_instr [in backend.RTLgen]
-restore_callee_save [in backend.Stacking]
-restore_float_callee_save [in backend.Stacking]
-restore_int_callee_save [in backend.Stacking]
-result [in backend.Kildall]
-reswellFormed [in backend.Allocproof_aux]
-ret [in backend.RTLgen]
-return_regs [in backend.LTL]
-ret_reg [in backend.RTLgen]
-rhs_evals_to [in backend.CSEproof]
-right [in backend.Parallelmove]
-rlw_accepting [in lib.Integers]
-rlw_transition [in lib.Integers]
-rol [in lib.Integers]
-rolm [in backend.Values]
-rolm [in backend.Cmconstr]
-rolm [in lib.Integers]
-rolm_match [in backend.Cmconstr]
-

S

T

U

-unchecked_store [in backend.Mem]
-union [in lib.Sets]
-unique_labels [in backend.Linearizeproof]
-unsigned [in lib.Integers]
-update [in backend.Mem]
-update [in backend.Parallelmove]
-update_instr [in backend.RTLgen]
-

V

-valid_block [in backend.Mem]
-valid_outcome [in backend.Linearizeproof]
-valid_pointer [in backend.Mem]
-valnum [in backend.CSE]
-valnum_reg [in backend.CSE]
-valnum_regs [in backend.CSE]
-Value [in backend.Parallelmove]
-valu_agree [in backend.CSEproof]
-val_cond_reg [in backend.PPC]
-val_match_approx [in backend.Constpropproof]
-val_normalized [in backend.Cminorgenproof]
-var_addr [in backend.Cminorgen]
-var_get [in backend.Cminorgen]
-var_set [in backend.Cminorgen]
-Vfalse [in backend.Values]
-Vmone [in backend.Values]
-Vone [in backend.Values]
-Vtrue [in backend.Values]
-Vzero [in backend.Values]
-

W

-wf_equation [in backend.CSEproof]
-wf_numbering [in backend.CSEproof]
-wf_rhs [in backend.CSEproof]
-wordsize [in lib.Integers]
-wt_content [in backend.Machtyping]
-wt_frame [in backend.Machtyping]
-wt_function [in backend.LTLtyping]
-wt_function [in backend.Lineartyping]
-wt_instrs [in backend.Stackingtyping]
-wt_program [in backend.Lineartyping]
-wt_program [in backend.RTLtyping]
-wt_program [in backend.LTLtyping]
-wt_program [in backend.Machtyping]
-wt_regset [in backend.RTLtyping]
-wt_regset [in backend.Machtyping]
-

X

-xcombine_l [in lib.Maps]
-xcombine_r [in lib.Maps]
-xelements [in lib.Maps]
-xget [in lib.Maps]
-xkeys [in lib.Maps]
-xmap [in lib.Maps]
-xor [in backend.Cmconstr]
-xor [in backend.Values]
-xor [in lib.Integers]
-xorimm [in backend.PPCgen]
-

Z

-Zdiv_round [in lib.Integers]
-zeq [in lib.Coqlib]
-zero [in lib.Integers]
-zle [in lib.Coqlib]
-zlt [in lib.Coqlib]
-Zmod_round [in lib.Integers]
-ztonat [in backend.Mem]
-Z_bin_decomp [in lib.Integers]
-Z_of_bits [in lib.Integers]
-Z_one_bits [in lib.Integers]
-Z_shift_add [in lib.Integers]
-

Module Index

A

-Approx [in backend.Constprop]
-

B

-BACKWARD_DATAFLOW_SOLVER [in backend.Kildall]
-Backward_Dataflow_Solver [in backend.Kildall]
-BBlock_solver [in backend.Kildall]
-BBLOCK_SOLVER [in backend.Kildall]
-

D

-D [in backend.Constprop]
-Dataflow_Solver [in backend.Kildall]
-DATAFLOW_SOLVER [in backend.Kildall]
-DS [in backend.Kildall]
-DS [in backend.Constprop]
-DS [in backend.Linearize]
-DS [in backend.Allocation]
-

E

-ELEMENT [in lib.union_find]
-EMap [in lib.Maps]
-EQUALITY_TYPE [in lib.Maps]
-

F

-Float [in lib.Floats]
-

G

-Genv [in backend.Globalenvs]
-GENV [in backend.Globalenvs]
-

I

-Identset [in backend.Cminorgen]
-IMap [in lib.Maps]
-IndexedMreg [in backend.Locations]
-INDEXED_TYPE [in lib.Maps]
-Int [in lib.Integers]
-

L

-L [in backend.Kildall]
-L [in backend.Kildall]
-L [in backend.Kildall]
-L [in backend.Kildall]
-L [in backend.Kildall]
-L [in backend.Kildall]
-L [in backend.Kildall]
-L [in backend.Kildall]
-L [in backend.Kildall]
-LBoolean [in lib.Lattice]
-LFlat [in lib.Lattice]
-Loc [in backend.Locations]
-Locmap [in backend.Locations]
-LPMap [in lib.Lattice]
-

M

-MakeSet [in lib.Sets]
-MAP [in lib.Maps]
-MAP [in lib.union_find]
-mymap [in backend.RTLtyping]
-myreg [in backend.RTLtyping]
-

N

-NIndexed [in lib.Maps]
-NMap [in lib.Maps]
-Numbering [in backend.CSE]
-

O

-OrderedIndexed [in lib.Ordered]
-OrderedMreg [in backend.InterfGraph]
-OrderedPair [in lib.Ordered]
-OrderedPositive [in lib.Ordered]
-OrderedReg [in backend.InterfGraph]
-OrderedRegMreg [in backend.InterfGraph]
-OrderedRegReg [in backend.InterfGraph]
-ORDERED_TYPE_WITH_TOP [in backend.Kildall]
-

P

-PMap [in lib.Maps]
-PregEq [in backend.PPC]
-Pregmap [in backend.PPC]
-PTree [in lib.Maps]
-

R

-Reg [in backend.Registers]
-RegEq [in backend.Mach]
-Regmap [in backend.Mach]
-Regmap [in backend.Registers]
-Regset [in backend.Registers]
-

S

-SEMILATTICE [in lib.Lattice]
-SEMILATTICE_WITH_TOP [in lib.Lattice]
-SetDepRegMreg [in backend.InterfGraph]
-SetDepRegReg [in backend.InterfGraph]
-SetRegMreg [in backend.InterfGraph]
-SetRegReg [in backend.InterfGraph]
-Solver [in backend.CSE]
-

T

-TREE [in lib.Maps]
-

U

-Uf [in backend.RTLtyping]
-UNIONFIND [in lib.union_find]
-Unionfind [in lib.union_find]
-

V

-Val [in backend.Values]
-ValnumEq [in backend.CSEproof]
-VMap [in backend.CSEproof]
-

Z

-ZIndexed [in lib.Maps]
-ZMap [in lib.Maps]
-

Library Index

A

-Allocation
-Allocproof
-Allocproof_aux
-Alloctyping
-Alloctyping_aux
-AST
-

C

-Cmconstr
-Cmconstrproof
-Cminor
-Cminorgen
-Cminorgenproof
-Coloring
-Coloringproof
-Constprop
-Constpropproof
-Conventions
-Coqlib
-CSE
-CSEproof
-Csharpminor
-

F

-Floats
-

G

-Globalenvs
-

I

-Inclusion
-Integers
-InterfGraph
-

K

-Kildall
-

L

-Lattice
-Linear
-Linearize
-Linearizeproof
-Linearizetyping
-Lineartyping
-Locations
-LTL
-LTLtyping
-

M

-Mach
-Machabstr
-Machabstr2mach
-Machtyping
-Main
-Maps
-Mem
-

O

-Op
-Ordered
-

P

-Parallelmove
-PPC
-PPCgen
-PPCgenproof
-PPCgenproof1
-

R

-Registers
-RTL
-RTLgen
-RTLgenproof
-RTLgenproof1
-RTLtyping
-

S

-Sets
-Stacking
-Stackingproof
-Stackingtyping
-

T

-Tunneling
-Tunnelingproof
-Tunnelingtyping
-

U

-union_find
-

V

-Values
-

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Global Index

(3806 entries)

Axiom Index

(39 entries)

Lemma Index

(1753 entries)

Constructor Index

(700 entries)

Inductive Index

(155 entries)

Definition Index

(1017 entries)

Module Index

(78 entries)

Library Index

(64 entries)

This page has been generated by coqdoc - - \ No newline at end of file + + + + +

The Compcert certified compiler back-end

Commented Coq development

Version 0.2, 2006-01-07

+ +

Introduction

+ +

The Compcert back-end is a compiler that generates PowerPC assembly +code from a low-level intermediate language called Cminor and a +slightly more expressive intermediate language called Csharpminor. +The particularity of this compiler is that it is written mostly within +the specification language of the Coq proof assistant, and its +correctness --- the fact that the generated assembly code is +semantically equivalent to its source program --- was entirely proved +within the Coq proof assistant.

+ +

A high-level overview of the Compcert back-end and its proof of +correctness can be found in the following paper:

+Xavier Leroy, Formal +certification of a compiler back-end, or: programming a compiler with +a proof assistant. Proceedings of the POPL 2006 symposium. + +

This Web site gives a commented listing of the underlying Coq +specifications and proofs. Proof scripts and the parts of the +compiler written directly in Caml are omitted. This development is a +work in progress; some parts may have changed since the overview paper +above was written.

+ +

This document and all Coq source files referenced from it are +copyright 2005, 2006 Institut National de Recherche en Informatique et +en Automatique (INRIA) and distributed under the terms of the GNU General Public +License version 2.

+ +

General-purpose libraries, data structures and algorithms

+ +

Coqlib: addendum to the Coq standard library. + (Coq source file with proofs: + Coqlib.v.) +
Maps: finite maps. + (Coq source file with proofs: + Maps.v.) +
Integers: machine integers. + (Coq source file with proofs: + Integers.v.) +
Floats: machine floating-point numbers. +
Iteration: various forms of "while" loops. +
Ordered: construction of +ordered types. +
Lattice: construction of +semi-lattices. +
Kildall: resolution of dataflow +inequations by fixpoint iteration. +
Parmov: compilation of parallel assignments. +

+ +

Definitions and properties used in many parts of the development

+ +

Errors: the Error monad. +
AST: identifiers, whole programs and other +common elements of abstract syntaxes. + (Coq source file with proofs: AST.v.) +
Values: run-time values. +
Events: observable events and traces. +
Mem: the memory model. +
Globalenvs: global execution environments. +
Smallstep: tools for small-step semantics. +
Op: operators, addressing modes and their +semantics. +

+ +

Source, intermediate and target languages: syntax and semantics

+ +

Cminor: low-level structured +language, with explicit stack allocation of certain local variables. +
CminorSel: like Cminor, +with machine-specific operators and addressing modes. +
RTL: register transfer language (3-address +code, control-flow graph, infinitely many pseudo-registers).
+See also: Registers (representation of +pseudo-registers). +
LTL: location transfer language (3-address +code, control-flow graph, finitely many physical registers, infinitely +many stack slots).
+See also: Locations (representation of +locations). +
LTLin: like LTL, but the CFG is +replaced by a linear list of instructions with explicit branches and labels. +
Linear: like LTLin, with explicit +spilling, reloading and enforcement of calling conventions. +
Mach: like Linear, with a more concrete +view of the activation record.
+See also: Machabstr abstract semantics for Mach.
+See also: Machconcr concrete semantics for Mach. +
PPC: abstract syntax for PowerPC assembly +code. +

+ +

Compiler passes

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +

Pass	Source & target	Compiler code	Correctness proof
Recognition of operators and addressing modes	Cminor to CminorSel	Selection	Selectionproof
Construction of the CFG, 3-address code generation	Cminor to RTL	RTLgen	RTLgenspec + RTLgenproof
Constant propagation	RTL to RTL	Constprop	Constpropproof
Common subexpression elimination	RTL to RTL	CSE	CSEproof
Register allocation by coloring of an interference graph	RTL to LTL	InterfGraph + Coloring + Allocation	+ Coloringproof + Allocproof
Branch tunneling	LTL to LTL	Tunneling	Tunnelingproof
Linearization of the CFG	LTL to LTLin	Linearize	Linearizeproof
Spilling, reloading, calling conventions	LTLin to Linear	Conventions + Reload	Parallelmove + Reloadproof
Laying out the activation records	Linear to Mach	Bounds + Stacking	Stackingproof
Storing the activation records in memory	Mach to Mach	(none) +	PPCgenretaddr + Machabstr2mach
Emission of PowerPC assembly	Mach to PPC	PPCgen	PPCgenproof1 + PPCgenproof

+ +

Type systems

+ +Trivial type systems are used to statically capture well-formedness +conditions on the intermediate languages. +

RTLtyping: typing for RTL + type +reconstruction. +
LTLtyping: typing for LTL. +
LTLintyping: typing for LTLin. +
Lineartyping: typing for Linear. +
Machtyping: typing for Mach. +

+Proofs that compiler passes are type-preserving: +

Alloctyping (register allocation). +
Tunnelingtyping (branch tunneling). +
Linearizetyping (code linearization). +
Reloadtyping (spilling and reloading). +
Stackingtyping (layout of activation records). +

+ +

All together

+ +

Main: composing the passes together; the +final semantic preservation theorems. +

+ +

Xavier.Leroy@inria.fr

+ + + diff --git a/doc/removeproofs b/doc/removeproofs index 0ebe3a8..82809ba 100755 --- a/doc/removeproofs +++ b/doc/removeproofs @@ -2,7 +2,7 @@ for i in $*; do mv $i $i.bak - sed -e '/

Proof<\/code>\./,/Qed<\/code>\./d' $i.bak > $i
+  sed -e '/Proof<\/code> *\./,/\(Qed\|Defined\)<\/code> *\./d' $i.bak > $i
   rm $i.bak
 done
 
diff --git a/doc/style.css b/doc/style.css
index 9c1eb49..dced2ff 100644
--- a/doc/style.css
+++ b/doc/style.css
@@ -26,7 +26,9 @@ tr { background-color : White }
 # .doc { background-color :#66ff66  }
 .doc { margin-left: -5%; }
 .docright { margin-left: 40%; }
-h1 { margin-left: -10%; text-align: right; }
+div.doc code { color : #008000; font-weight: bold }
+h1.libtitle { text-align: center; }
+h1 { margin-left: -5%; }
 h2 { margin-left: -5%; }
 h3,h4,h5,h6 { margin-left: -3%; }
 hr { margin-left: -10%; margin-right:-10%; }
-- 
cgit v1.2.3

The Compcert certified compiler back-end

Commented Coq development

Version 0.2, 2006-01-07

Introduction

Table of contents

Libraries, algorithms, data structures

Source, intermediate and target languages: syntax and semantics

Compiler passes

Type systems

All together

Global Index

A

B

C

D

E

F

G

H

I

K

L

M

N

O

P

R

S

T

U

V

W

X

Z

_

Axiom Index

A

C

D

E

F

G

H

I

L

M

N

O

P

S

Z

Lemma Index

A

B

C

D

E

F

G

H

I

K

L

M

N

O

P

R

S

T

U

V

W

X

Z

Constructor Index

A

B

C

D