blob: 61856acfafc4d443c1c5910276415c543cecbafe (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Require Import Integers.
Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
Require Import PostpassScheduling.
Require Import Errors String.
Require Compopts.
Local Open Scope error_monad_scope.
Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := Compopts.time name f.
Definition transf_program (p: Mach.program) : res Asm.program :=
let mbp := (time "Machblock generation" Machblockgen.transf_program) p in
do abp <- (time "Asmblock generation" Asmblockgen.transf_program) mbp;
do abp' <- (time "PostpassScheduling total oracle+verification" PostpassScheduling.transf_program) abp;
OK ((time "Asm generation" Asm.transf_program) abp').
Definition transf_function (f: Mach.function) : res Asm.function :=
let mbf := Machblockgen.transf_function f in
do abf <- Asmblockgen.transf_function mbf;
OK (Asm.transf_function abf).
Definition transl_code (f: Mach.function) (l: Mach.code) : res (list Asm.instruction) :=
let mbf := Machblockgen.transf_function f in
let mbc := Machblockgen.trans_code l in
do abc <- transl_blocks mbf mbc true;
OK (unfold abc).
|
