From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:31:26 +0100 Subject: Update the back-end proofs to the new linking framework. --- backend/CSE.v | 28 +++++++++------------------- 1 file changed, 9 insertions(+), 19 deletions(-) (limited to 'backend/CSE.v') 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. -- cgit