diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-20 18:00:43 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-03-20 18:00:43 +0100 |
| commit | 1fdca8371317e656cb08eaec3adb4596d6447e9b (patch) | |
| tree | 8a5d390a4d38f4d840f516fb917eb824311a93a0 /backend/CSE.v | |
| parent | 1396a4051caef0957ede026f3b8fab5a9b10b6bc (diff) | |
| parent | 478ae4c3aeb1a31b0eec9ab7eb8fe20ec2671614 (diff) | |
| download | compcert-1fdca8371317e656cb08eaec3adb4596d6447e9b.tar.gz compcert-1fdca8371317e656cb08eaec3adb4596d6447e9b.zip | |
Merge pull request #93 from AbsInt/separate-compilation
This pull request implements "approach A" to separate compilation in CompCert from the paper
Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190
In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.
This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.
Diffstat (limited to 'backend/CSE.v')
| -rw-r--r-- | backend/CSE.v | 28 |
1 files changed, 9 insertions, 19 deletions
diff --git a/backend/CSE.v b/backend/CSE.v index 63dadbc7..d6b89557 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -13,22 +13,11 @@ (** Common subexpression elimination over RTL. This optimization proceeds by value numbering over extended basic blocks. *) -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import ValueDomain. -Require Import ValueAnalysis. -Require Import CSEdomain. -Require Import Kildall. -Require Import CombineOp. +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Values Memory. +Require Import Op Registers RTL. +Require Import ValueDomain ValueAnalysis CSEdomain CombineOp. (** The idea behind value numbering algorithms is to associate abstract identifiers (``value numbers'') to the contents of registers @@ -451,7 +440,8 @@ Module Solver := BBlock_solver(Numbering). For builtin invocations [Ibuiltin], we have three strategies: - Forget all equations. This is appropriate for builtins that can be - turned into function calls ([EF_external], [EF_malloc], [EF_free]). + turned into function calls + ([EF_external], [EF_runtime], [EF_malloc], [EF_free]). - Forget equations involving loads but keep equations over registers. This is appropriate for builtins that can modify memory, e.g. volatile stores, or [EF_builtin] @@ -481,7 +471,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb empty_numbering | Ibuiltin ef args res s => match ef with - | EF_external _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => + | EF_external _ _ | EF_runtime _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ => empty_numbering | EF_builtin _ _ | EF_vstore _ => set_res_unknown (kill_all_loads before) res @@ -582,5 +572,5 @@ Definition transf_fundef (rm: romem) (f: fundef) : res fundef := AST.transf_partial_fundef (transf_function rm) f. Definition transf_program (p: program) : res program := - transform_partial_program (transf_fundef (romem_for_program p)) p. + transform_partial_program (transf_fundef (romem_for p)) p. |