From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 May 2020 22:04:20 +0200 Subject: k1c -> kvx changes --- doc/index-kvx.html | 362 ++++++++++++++++++++++++++++++++++++++++++++++++ doc/index-mppa_k1c.html | 362 ------------------------------------------------ 2 files changed, 362 insertions(+), 362 deletions(-) create mode 100644 doc/index-kvx.html delete mode 100644 doc/index-mppa_k1c.html (limited to 'doc') diff --git a/doc/index-kvx.html b/doc/index-kvx.html new file mode 100644 index 00000000..ae01d2d6 --- /dev/null +++ b/doc/index-kvx.html @@ -0,0 +1,362 @@ + + + +The CompCert verified compiler + + + + + + + +

The CompCert verified compiler

Commented Coq development

Version 3.7, 2020-03-31

PATCHED for the Kalray MPPA-KVX VLIW CORE

+ +

Introduction

+ +

This web page is a patched version of the table of contents of the official CompCert documentation, + as given on the CompCert Web site. + The unmodified parts of this table appear in gray. + + +

+ +

General-purpose libraries, data structures and algorithms

+ +

Coqlib: addendum to the Coq standard library. +
Maps: finite maps. +
Integers: machine integers. +
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. +
UnionFind: a persistent union-find data structure. +
Postorder: postorder numbering of a directed graph. +

+ +

The `abstractbb` library, introduced for MPPA-KVX

AbstractBasicBlocksDef: an IR for verifying some semantic properties on basic-blocks. +
Parallelizability: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block. +
ImpSimuTest: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines SeqSimuTheory with hash-consing. +

+ + +

Definitions and theorems used in many parts of the development

+ +

Errors: the Error monad. +
AST: identifiers, whole programs and other +common elements of abstract syntaxes. +
Linking: generic framework to define syntactic linking over the CompCert languages. +
Values: run-time values. +
Events: observable events and traces. +
Memory: memory model.
+See also: Memdata (in-memory representation of data). +
Globalenvs: global execution environments. +
Smallstep: tools for small-step semantics. +
Behaviors: from small-step semantics to observable behaviors of programs. +
Determinism: determinism properties of small-step semantics. +
Op: operators, addressing modes and their +semantics. +
Unityping: a solver for atomic unification constraints. +

+ +

Source, intermediate and target languages: syntax and semantics

+ +

The CompCert C source language: +syntax and +semantics and +determinized semantics and +type system.
+See also: type expressions and +operators (syntax and semantics).
+See also: reference interpreter. +
Clight: a simpler version of CompCert C where expressions contain no side-effects. +
Csharpminor: low-level + structured language. +
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 of basic blocks, finitely many physical registers, infinitely +many stack slots).
+See also: Locations (representation of +locations) and Machregs (description of processor registers). +
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. +

+ +

Languages introduced for MPPA-KVX

Machblock: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step). +This IR is generic over the processor, even if currently, only used for MPPA_KVX. +
Asmvliw: abstract syntax and semantics for Mppa_KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. +
Asmblock: a variant of Asmvliw, with a sequential semantics within bundles, which make them corresponds here to usual basic-blocks. + This IR is an intermediate step between Machblock and Asmvliw. +
Asm: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of Asmvliw for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax). +

+ +

Compiler passes

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

Pass	Source & target	Compiler code	Correctness proof
Pulling side-effects out of expressions; + fixing an evaluation order	CompCert C to Clight	SimplExpr	SimplExprspec + SimplExprproof
Pulling non-adressable scalar local variables out of memory	Clight to Clight	SimplLocals	SimplLocalsproof
Simplification of control structures; + explication of type-dependent computations	Clight to Csharpminor	Cshmgen	Cshmgenproof
Stack allocation of local variables + whose address is taken; + simplification of switch statements	Csharpminor to Cminor	Cminorgen	Cminorgenproof
Recognition of operators and addressing modes	Cminor to CminorSel	Selection + SelectOp + SelectLong + SelectDiv + SplitLong	Selectionproof + SelectOpproof + SelectLongproof + SelectDivproof + SplitLongproof
Construction of the CFG, 3-address code generation	CminorSel to RTL	RTLgen	RTLgenspec + RTLgenproof
Recognition of tail calls	RTL to RTL	Tailcall	Tailcallproof
Function inlining	RTL to RTL	Inlining	Inliningspec + Inliningproof
Postorder renumbering of the CFG	RTL to RTL	Renumber	Renumberproof
Constant propagation	RTL to RTL	Constprop + ConstpropOp	Constpropproof + ConstproppOproof
Common subexpression elimination	RTL to RTL	CSE + CombineOp	CSEproof + CombineOpproof
Redundancy elimination	RTL to RTL	Deadcode	Deadcodeproof
Removal of unused static globals	RTL to RTL	Unusedglob	Unusedglobproof
Register allocation (validation a posteriori)	RTL to LTL	Allocation	Allocproof
Branch tunneling	LTL to LTL	Tunneling	Tunnelingproof
Linearization of the CFG	LTL to Linear	Linearize	Linearizeproof
Removal of unreferenced labels	Linear to Linear	CleanupLabels	CleanupLabelsproof
Synthesis of debugging information	Linear to Linear	Debugvar	Debugvarproof
Laying out the activation records	Linear to Mach	Stacking + Bounds + Stacklayout	Stackingproof + Separation

+ +

Compilation passes introduced for MPPA-KVX

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

Reconstruction of basic-blocks at Mach level	Mach to Machblock	Machblockgen	ForwardSimulationBlock + Machblockgenproof
Emission of purely sequential assembly code	Machblock to Asmblock	Asmblockgen	Asmblockgenproof0 + Asmblockgenproof1 + Asmblockgenproof
Bundling (and basic-block scheduling)	Asmblock to Asmvliw	PostpassScheduling using + Asmblockdeps and the `abstractbb` library	PostpassSchedulingproof
Flattening bundles (only a bureaucratic operation)	Asmvliw to Asm	Asmgen	Asmgenproof

+ + +

All together

+ +

Compiler: composing the passes together; +whole-compiler semantic preservation theorems. +
Complements: interesting consequences of the semantic preservation theorems. +

+ +

Static analyses

+ +The following static analyses are performed over the RTL intermediate +representation to support optimizations such as constant propagation, +CSE, and dead code elimination. +

Liveness: liveness analysis. +
ValueAnalysis: value and alias analysis
+See also: ValueDomain: the abstract domain for value analysis.
+See also: ValueAOp: processor-dependent parts of value analysis. +
Deadcode: neededness analysis
+See also: NeedDomain: the abstract domain for neededness analysis.
+See also: NeedOp: processor-dependent parts of neededness analysis. +

+ +

Type systems

+ +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. +

Ctyping: typing for CompCert C + type-checking functions. +
RTLtyping: typing for RTL + type +reconstruction. +
Lineartyping: typing for Linear. +

+ + + + diff --git a/doc/index-mppa_k1c.html b/doc/index-mppa_k1c.html deleted file mode 100644 index 86fd4166..00000000 --- a/doc/index-mppa_k1c.html +++ /dev/null @@ -1,362 +0,0 @@ - - - -The CompCert verified compiler - - - - - - - -

The CompCert verified compiler

Commented Coq development

Version 3.7, 2020-03-31

PATCHED for the Kalray MPPA-K1C VLIW CORE

- -

Introduction

- -

This web page is a patched version of the table of contents of the official CompCert documentation, - as given on the CompCert Web site. - The unmodified parts of this table appear in gray. - - -

- -

General-purpose libraries, data structures and algorithms

- -

Coqlib: addendum to the Coq standard library. -
Maps: finite maps. -
Integers: machine integers. -
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. -
UnionFind: a persistent union-find data structure. -
Postorder: postorder numbering of a directed graph. -

- -

The `abstractbb` library, introduced for MPPA-K1C

AbstractBasicBlocksDef: an IR for verifying some semantic properties on basic-blocks. -
Parallelizability: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block. -
ImpSimuTest: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines SeqSimuTheory with hash-consing. -

- - -

Definitions and theorems used in many parts of the development

- -

Errors: the Error monad. -
AST: identifiers, whole programs and other -common elements of abstract syntaxes. -
Linking: generic framework to define syntactic linking over the CompCert languages. -
Values: run-time values. -
Events: observable events and traces. -
Memory: memory model.
-See also: Memdata (in-memory representation of data). -
Globalenvs: global execution environments. -
Smallstep: tools for small-step semantics. -
Behaviors: from small-step semantics to observable behaviors of programs. -
Determinism: determinism properties of small-step semantics. -
Op: operators, addressing modes and their -semantics. -
Unityping: a solver for atomic unification constraints. -

- -

Source, intermediate and target languages: syntax and semantics

- -

The CompCert C source language: -syntax and -semantics and -determinized semantics and -type system.
-See also: type expressions and -operators (syntax and semantics).
-See also: reference interpreter. -
Clight: a simpler version of CompCert C where expressions contain no side-effects. -
Csharpminor: low-level - structured language. -
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 of basic blocks, finitely many physical registers, infinitely -many stack slots).
-See also: Locations (representation of -locations) and Machregs (description of processor registers). -
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. -

- -

Languages introduced for MPPA-K1C

Machblock: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step). -This IR is generic over the processor, even if currently, only used for MPPA_K1C. -
Asmvliw: abstract syntax and semantics for Mppa_K1c VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles. -
Asmblock: a variant of Asmvliw, with a sequential semantics within bundles, which make them corresponds here to usual basic-blocks. - This IR is an intermediate step between Machblock and Asmvliw. -
Asm: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of Asmvliw for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax). -

- -

Compiler passes

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

Pass	Source & target	Compiler code	Correctness proof
Pulling side-effects out of expressions; - fixing an evaluation order	CompCert C to Clight	SimplExpr	SimplExprspec - SimplExprproof
Pulling non-adressable scalar local variables out of memory	Clight to Clight	SimplLocals	SimplLocalsproof
Simplification of control structures; - explication of type-dependent computations	Clight to Csharpminor	Cshmgen	Cshmgenproof
Stack allocation of local variables - whose address is taken; - simplification of switch statements	Csharpminor to Cminor	Cminorgen	Cminorgenproof
Recognition of operators and addressing modes	Cminor to CminorSel	Selection - SelectOp - SelectLong - SelectDiv - SplitLong	Selectionproof - SelectOpproof - SelectLongproof - SelectDivproof - SplitLongproof
Construction of the CFG, 3-address code generation	CminorSel to RTL	RTLgen	RTLgenspec - RTLgenproof
Recognition of tail calls	RTL to RTL	Tailcall	Tailcallproof
Function inlining	RTL to RTL	Inlining	Inliningspec - Inliningproof
Postorder renumbering of the CFG	RTL to RTL	Renumber	Renumberproof
Constant propagation	RTL to RTL	Constprop - ConstpropOp	Constpropproof - ConstproppOproof
Common subexpression elimination	RTL to RTL	CSE - CombineOp	CSEproof - CombineOpproof
Redundancy elimination	RTL to RTL	Deadcode	Deadcodeproof
Removal of unused static globals	RTL to RTL	Unusedglob	Unusedglobproof
Register allocation (validation a posteriori)	RTL to LTL	Allocation	Allocproof
Branch tunneling	LTL to LTL	Tunneling	Tunnelingproof
Linearization of the CFG	LTL to Linear	Linearize	Linearizeproof
Removal of unreferenced labels	Linear to Linear	CleanupLabels	CleanupLabelsproof
Synthesis of debugging information	Linear to Linear	Debugvar	Debugvarproof
Laying out the activation records	Linear to Mach	Stacking - Bounds - Stacklayout	Stackingproof - Separation

- -

Compilation passes introduced for MPPA-K1C

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

Reconstruction of basic-blocks at Mach level	Mach to Machblock	Machblockgen	ForwardSimulationBlock - Machblockgenproof
Emission of purely sequential assembly code	Machblock to Asmblock	Asmblockgen	Asmblockgenproof0 - Asmblockgenproof1 - Asmblockgenproof
Bundling (and basic-block scheduling)	Asmblock to Asmvliw	PostpassScheduling using - Asmblockdeps and the `abstractbb` library	PostpassSchedulingproof
Flattening bundles (only a bureaucratic operation)	Asmvliw to Asm	Asmgen	Asmgenproof

- - -

All together

- -

Compiler: composing the passes together; -whole-compiler semantic preservation theorems. -
Complements: interesting consequences of the semantic preservation theorems. -

- -

Static analyses

- -The following static analyses are performed over the RTL intermediate -representation to support optimizations such as constant propagation, -CSE, and dead code elimination. -

Liveness: liveness analysis. -
ValueAnalysis: value and alias analysis
-See also: ValueDomain: the abstract domain for value analysis.
-See also: ValueAOp: processor-dependent parts of value analysis. -
Deadcode: neededness analysis
-See also: NeedDomain: the abstract domain for neededness analysis.
-See also: NeedOp: processor-dependent parts of neededness analysis. -

- -

Type systems

- -The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. -

Ctyping: typing for CompCert C + type-checking functions. -
RTLtyping: typing for RTL + type -reconstruction. -
Lineartyping: typing for Linear. -

- - - - -- cgit

The CompCert verified compiler

Commented Coq development

Version 3.7, 2020-03-31

PATCHED for the Kalray MPPA-KVX VLIW CORE

Introduction

Table of contents

General-purpose libraries, data structures and algorithms

The `abstractbb` library, introduced for MPPA-KVX

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics

Languages introduced for MPPA-KVX

Compiler passes

Compilation passes introduced for MPPA-KVX

All together

Static analyses

Type systems

The CompCert verified compiler

Commented Coq development

Version 3.7, 2020-03-31

PATCHED for the Kalray MPPA-K1C VLIW CORE

Introduction

Table of contents

General-purpose libraries, data structures and algorithms

The `abstractbb` library, introduced for MPPA-K1C

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics

Languages introduced for MPPA-K1C

Compiler passes

Compilation passes introduced for MPPA-K1C

All together

Static analyses

Type systems

The CompCert verified compiler

Commented Coq development

Version 3.7, 2020-03-31

PATCHED for the Kalray MPPA-KVX VLIW CORE

Introduction

Table of contents

General-purpose libraries, data structures and algorithms

The abstractbb library, introduced for MPPA-KVX

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics

Languages introduced for MPPA-KVX

Compiler passes

Compilation passes introduced for MPPA-KVX

All together

Static analyses

Type systems

The CompCert verified compiler

Commented Coq development

Version 3.7, 2020-03-31

PATCHED for the Kalray MPPA-K1C VLIW CORE

Introduction

Table of contents

General-purpose libraries, data structures and algorithms

The abstractbb library, introduced for MPPA-K1C

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics

Languages introduced for MPPA-K1C

Compiler passes

Compilation passes introduced for MPPA-K1C

All together

Static analyses

Type systems

The `abstractbb` library, introduced for MPPA-KVX

The `abstractbb` library, introduced for MPPA-K1C