From 2ed836d9fd798c17b0858468bda07bfa70dc9e43 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 7 Dec 2021 11:49:31 +0100 Subject: doc --- doc/index-verimag.html | 263 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 226 insertions(+), 37 deletions(-) (limited to 'doc') diff --git a/doc/index-verimag.html b/doc/index-verimag.html index 1eb857d9..56b16991 100644 --- a/doc/index-verimag.html +++ b/doc/index-verimag.html @@ -24,9 +24,9 @@ a:active {color : Red; text-decoration : underline; }

The CompCert verified compiler

Commented Coq development

-

Version 3.9, 2021-05-10

+

Version 3.10, 2021-11-19

 -

VERIMAG fork version 2021-29-10

+

VERIMAG fork version 2021-12-07

The CompCert Verimag's fork

This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on the CompCert Web site. @@ -304,8 +304,97 @@ Specific to KVX: Inliningproof + + Passes introduced for profiling (for later use in trace selection) + + + Insert profiling annotations (for recording experiments -- see PROFILE.md). + + RTL to RTL + Profiling + Profilingproof + + + Update ICond nodes (from recorded experiments -- see PROFILE.md). + + RTL to RTL + ProfilingExploit + ProfilingExploitproof + + + + FirstNop: Inserting a no-op instruction at each RTL function entrypoint + RTL to RTL + FirstNop + FirstNopproof + + - Postorder renumbering of the CFG + Postorder renumbering of the CFG (1) + RTL to RTL + Renumber + Renumberproof + + + + [CSE1] Common subexpression elimination (1) + RTL to RTL + CSE
+ CombineOp + CSEproof
+ CombineOpproof + + + + [Duplicate pass] Static Prediction + Unroll single + + Add static prediction information to Icond nodes
+ Unrolls a single iteration of innermost loops + + RTL to RTL + Duplicate (generic checker) + Duplicateproof (generic proof)
+ Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (2) + RTL to RTL + Renumber + Renumberproof + + + + [Duplicate pass] Tail Duplication + + Performs tail duplication on interesting traces to form superblocks + + RTL to RTL + Duplicate (generic checker) + Duplicateproof (generic proof)
+ Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (3) + RTL to RTL + Renumber + Renumberproof + + + + [Duplicate pass] Unroll body + + Unrolling the body of innermost loops + + RTL to RTL + Duplicate (generic checker) + Duplicateproof (generic proof)
+ Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (4) RTL to RTL Renumber Renumberproof @@ -321,7 +410,14 @@ Specific to KVX: - Common subexpression elimination + Postorder renumbering of the CFG (5) + RTL to RTL + Renumber + Renumberproof + + + + [CSE1] Common subexpression elimination (1) RTL to RTL CSE
CombineOp @@ -329,67 +425,159 @@ Specific to KVX: CombineOpproof + + [CSE2] Common subexpression elimination + RTL to RTL + CSE2
+ + CSE2proof
+ + + + + [CSE3] Common subexpression elimination (1) + RTL to RTL + CSE3
+ + CSE3proof
+ + + + + KillUselessMoves: removing useless moves instructions after CSE3 + RTL to RTL + KillUselessMoves
+ + KillUselessMovesproof
+ + + + + Forwarding Moves + RTL to RTL + ForwardMoves
+ + ForwardMovesproof
+ + + - Redundancy elimination + Redundancy elimination (1) RTL to RTL Deadcode Deadcodeproof + + + RTL Tunneling + RTL to RTL + RTLTunneling
+ + RTLTunnelingproof
+ + + - Removal of unused static globals + Postorder renumbering of the CFG (6) RTL to RTL - Unusedglob - Unusedglobproof + Renumber + Renumberproof - Passes introduced for profiling (for later use in trace selection) - + [Duplicate pass] Loop Rotate - Insert profiling annotations (for recording experiments -- see PROFILE.md). + Loop rotation RTL to RTL - Profiling - Profilingproof + Duplicate (generic checker) + Duplicateproof (generic proof)
+ Duplicatepasses (several passes from several oracles) + + + + Postorder renumbering of the CFG (7) + RTL to RTL + Renumber + Renumberproof + - Update ICond nodes (from recorded experiments -- see PROFILE.md). + Loop Invariant Code Motion RTL to RTL - ProfilingExploit - ProfilingExploitproof + LICM + LICMproof + + + + Postorder renumbering of the CFG (8) + RTL to RTL + Renumber + Renumberproof + + - Passes introduced for superblock prepass scheduling + [CSE3] Common subexpression elimination (2) + RTL to RTL + CSE3
+ + CSE3proof
+ + + + + Redundancy elimination (2) + RTL to RTL + Deadcode + Deadcodeproof + - Code duplications (trace selection, loop unrollings, etc) + Allnontrap: transforming loads to non-trapping ones + RTL to RTL + Allnontrap
+ Allnontrapproof
+ + + + + Removal of unused static globals RTL to RTL - Duplicate (generic checker) - Duplicateproof (generic proof)
- Duplicatepasses (several passes from several oracles) + Unusedglob + Unusedglobproof + - Superblock selection (with Liveness information) - RTL to RTLPath - RTLpathLivegen - RTLpathLivegenproof + Passes introduced for BTL + + + Block selection (with Liveness information) + RTL to BTL + RTLtoBTL + RTLtoBTLproof
+ BTLmatchRTL
+ BTL_Livecheck + Superblock prepass scheduling - RTLPath to RTLPath - RTLpathScheduler - RTLpathSchedulerproof
- with RTLpathSE_theory (the theory of symbolic execution on RTLpath)
- and RTLpathSE_simu_specs (the low-level specifications of the simulation checker)
- and RTLpathSE_impl (the simulation checker with hash-consing) + BTL to BTL + BTL_Scheduler + BTL_Schedulerproof
+ with BTL_SEtheory (the theory of symbolic execution on BTL_)
+ and BTL_SEsimuref (the low-level specifications of the simulation checker)
+ and BTL_SEimpl (the simulation checker with hash-consing) - Forgeting superblocks - RTLPath to RTL - RTLpath.transf_program - RTLpathproof + Forgeting blocks + BTL to RTL + BTLtoRTL + BTLtoRTLproof
+ BTLmatchRTL + @@ -442,7 +630,7 @@ Specific to KVX: - Passes introduced for KVX VLIW + Passes introduced for backends with postpass scheduling Reconstruction of basic-blocks at Mach level @@ -467,7 +655,8 @@ Specific to KVX: PostpassScheduling
using Asmblockdeps
and the abstractbb library - PostpassSchedulingproof + PostpassSchedulingproof
+ Asmblockprops -- cgit