diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 12:55:31 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-15 12:55:31 +0100 |
commit | 2185164c1845c30ebd4118ed5bc8d339b16663a9 (patch) | |
tree | ddba4ddb188d4a759829bfafb0777409f34376f6 /backend | |
parent | 34a7ec51c1f1bbfeb973f8e295ac81b65c70251c (diff) | |
download | compcert-2185164c1845c30ebd4118ed5bc8d339b16663a9.tar.gz compcert-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')
-rw-r--r-- | backend/IRC.ml | 36 |
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 = |