blob: 58e80be1ed34505c72c182f1b515774c2614e91f (
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Prashanth Mundkur, SRI International *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* The contributions by Prashanth Mundkur are reused and adapted *)
(* under the terms of a Contributor License Agreement between *)
(* SRI International and INRIA. *)
(* *)
(* *********************************************************************)
Require Import Integers.
Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
Require Import PostpassScheduling.
Require Import Errors.
Local Open Scope error_monad_scope.
Definition transf_program (p: Mach.program) : res Asm.program :=
let mbp := Machblockgen.transf_program p in
do abp <- Asmblockgen.transf_program mbp;
do abp' <- PostpassScheduling.transf_program abp;
OK (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).
|
