aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-12-07 17:39:27 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-12-07 17:39:27 +0100
commitf4b66ff05ab0affb47ebf390502cba5c277caea3 (patch)
tree4dbeac244b5f004f529be9f2111d85b7fb31dc7d /backend
parenta79f0f99831aa0b0742bf7cce459cc9353bd7cd0 (diff)
downloadcompcert-kvx-f4b66ff05ab0affb47ebf390502cba5c277caea3.tar.gz
compcert-kvx-f4b66ff05ab0affb47ebf390502cba5c277caea3.zip
Enforce evaluation order in IRC.add_interf and IRC.add_pref
As written previously, OCaml can evaluate `nodeOfVar g v1` and `nodeOfVar g v2` in any order. Consequently, `v1` and `v2` can be entered in the `varTable` hash table in different order. This can result in different (but equally valid) register allocations. It's better to enforce one evaluation order for the sake of reproducible compilations when the OCaml version changes.
Diffstat (limited to 'backend')
-rw-r--r--backend/IRC.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 6f4bbe29..1246a2d0 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -911,10 +911,10 @@ let location_of_var g v =
(* The exported interface *)
let add_interf g v1 v2 =
- addEdge g (nodeOfVar g v1) (nodeOfVar g v2)
+ let n1 = nodeOfVar g v1 in let n2 = nodeOfVar g v2 in addEdge g n1 n2
let add_pref g v1 v2 =
- addMovePref g (nodeOfVar g v1) (nodeOfVar g v2)
+ let n1 = nodeOfVar g v1 in let n2 = nodeOfVar g v2 in addMovePref g n1 n2
let coloring g =
initialNodePartition g;