diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-18 14:26:17 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-18 14:26:17 +0200 |
| commit | 7f1025fa2da08e68b839b7b6ea89771822dcfe83 (patch) | |
| tree | 30cf2e840c19e7ba91a9f647ed29e8c7b083f360 | |
| parent | a42baf15372e64f398685aaef079a82ea0db834e (diff) | |
| download | compcert-kvx-7f1025fa2da08e68b839b7b6ea89771822dcfe83.tar.gz compcert-kvx-7f1025fa2da08e68b839b7b6ea89771822dcfe83.zip | |
Detailing oracle/vérificateur in the timings
| -rw-r--r-- | mppa_k1c/Asmgen.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 704a0ac5..c3588871 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -27,7 +27,7 @@ Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := 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 optimization" PostpassScheduling.transf_program) abp; + 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 := diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index fa61d588..327901f3 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -991,4 +991,5 @@ let rec bundles_to_coq_schedule = function (** Called schedule function from Coq *) -let schedule bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto +let schedule_notime bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto +let schedule bb = Timing.time_coq ('P'::('o'::('s'::('t'::('p'::('a'::('s'::('s'::('S'::('c'::('h'::('e'::('d'::('u'::('l'::('i'::('n'::('g'::(' '::('o'::('r'::('a'::('c'::('l'::('e'::([])))))))))))))))))))))))))) schedule_notime bb |