aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-17 14:42:01 +0200
committerJustus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>2021-08-17 14:42:01 +0200
commit0170983b100074c615600afb934b0813aaa761eb (patch)
tree7b2e648bfee1134c8e1661ede16c1c498eb8e287
parent1dca24dd3360b61d9ea00893e6de12fb5bc2e56f (diff)
downloadcompcert-kvx-0170983b100074c615600afb934b0813aaa761eb.tar.gz
compcert-kvx-0170983b100074c615600afb934b0813aaa761eb.zip
Make warning about worse schedule with relaxed problem non-fatal unless
in debug mode. Compiling glpk-4.65 exhibited this problem but not when using the ILP-based instruction scheduling.
-rw-r--r--scheduling/MyRTLpathScheduleraux.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/scheduling/MyRTLpathScheduleraux.ml b/scheduling/MyRTLpathScheduleraux.ml
index 7d493d14..63e362ad 100644
--- a/scheduling/MyRTLpathScheduleraux.ml
+++ b/scheduling/MyRTLpathScheduleraux.ml
@@ -945,8 +945,10 @@ let downschedule_compensation_code sb code pm live_renames ~next_free_pc ~next_f
| Some (idealized_schedule, idealized_final_time)
, Some (default_schedule, default_final_time) ->
if idealized_final_time >= default_final_time then (
- if (idealized_final_time > default_final_time) then (
+ if (!debug_flag && idealized_final_time > default_final_time) then (
debug "Unexpectedly, idealized dependencies lead to a worse expected final time.\n";
+ debug "idealized_final_time = %d, default_final_time = %d\n" idealized_final_time default_final_time;
+ debug "For superblock %d" (Camlcoq.P.to_int sb.instructions.(0));
failwith "Unexpectedly bad final time for idealized schedule";
);
(* Early exit *)