aboutsummaryrefslogtreecommitdiffstats
path: root/backend/IRC.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-03-15 12:55:31 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-03-15 12:55:31 +0100
commit2185164c1845c30ebd4118ed5bc8d339b16663a9 (patch)
treeddba4ddb188d4a759829bfafb0777409f34376f6 /backend/IRC.ml
parent34a7ec51c1f1bbfeb973f8e295ac81b65c70251c (diff)
downloadcompcert-kvx-2185164c1845c30ebd4118ed5bc8d339b16663a9.tar.gz
compcert-kvx-2185164c1845c30ebd4118ed5bc8d339b16663a9.zip
Added back invariant checks for IRC.
Since the invariant checks are not currently used and they are not exported they are renamed to include a _ to avoid warning. Bug 18394
Diffstat (limited to 'backend/IRC.ml')
-rw-r--r--backend/IRC.ml36
1 files changed, 36 insertions, 0 deletions
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 8780bce3..76f194d2 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -451,6 +451,42 @@ let initialNodePartition g =
| _ -> assert false in
Hashtbl.iter (fun _ a -> part_node a) g.varTable
+(* Check invariants *)
+
+let _degreeInvariant _ n =
+ let c = ref 0 in
+ iterAdjacent (fun _ -> incr c) n;
+ if !c <> n.degree then
+ failwith("degree invariant violated by " ^ name_of_node n)
+
+let _simplifyWorklistInvariant g n =
+ if n.degree < g.num_available_registers.(n.regclass)
+ && not (moveRelated n)
+ then ()
+ else failwith("simplify worklist invariant violated by " ^ name_of_node n)
+
+let _freezeWorklistInvariant g n =
+ if n.degree < g.num_available_registers.(n.regclass)
+ && moveRelated n
+ then ()
+ else failwith("freeze worklist invariant violated by " ^ name_of_node n)
+
+let _spillWorklistInvariant g n =
+ if n.degree >= g.num_available_registers.(n.regclass)
+ then ()
+ else failwith("spill worklist invariant violated by " ^ name_of_node n)
+
+let _checkInvariants g =
+ DLinkNode.iter
+ (fun n -> _degreeInvariant g n; _simplifyWorklistInvariant g n)
+ g.simplifyWorklist;
+ DLinkNode.iter
+ (fun n -> _degreeInvariant g n; _freezeWorklistInvariant g n)
+ g.freezeWorklist;
+ DLinkNode.iter
+ (fun n -> _degreeInvariant g n; _spillWorklistInvariant g n)
+ g.spillWorklist
+
(* Enable moves that have become low-degree related *)
let enableMoves g n =