diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-12-17 15:43:37 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-12-17 15:43:37 +0100 |
| commit | ff1a4a32676fad3a78aad69d963f9f94bb07615c (patch) | |
| tree | 1be819074805478c2982ffefd44e060d543e2cd4 /mppa_k1c/Asmgen.v | |
| parent | f9de154cde1974a8fa9afec9ad83653384ec912f (diff) | |
| download | compcert-kvx-ff1a4a32676fad3a78aad69d963f9f94bb07615c.tar.gz compcert-kvx-ff1a4a32676fad3a78aad69d963f9f94bb07615c.zip | |
Added a simple postpass oracle that splits a bblock into single instruction bundles
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 6f61747f..58e80be1 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -17,6 +17,7 @@ Require Import Integers. Require Import Mach Asm Asmblock Asmblockgen Machblockgen. +Require Import PostpassScheduling. Require Import Errors. Local Open Scope error_monad_scope. @@ -24,7 +25,8 @@ 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; - OK (Asm.transf_program abp). + 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 |