diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-09-22 17:03:03 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-09-22 17:03:03 +0200 |
| commit | d5e332e8bc07ad2a67cc2878e620c02286b27142 (patch) | |
| tree | 610037510ff54827b56a0f9992a7c2c70ae0b338 /exportclight | |
| parent | ab0d9476db875a82cf293623d18552b62f239d5c (diff) | |
| download | compcert-kvx-d5e332e8bc07ad2a67cc2878e620c02286b27142.tar.gz compcert-kvx-d5e332e8bc07ad2a67cc2878e620c02286b27142.zip | |
Fix computation of next temporary in -canonical-idents mode
Variables were confused for temporaries, causing the temporaries introduced
by this pass to be very big integers.
Fixes: #370
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/Clightnorm.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml index a0001250..a6158b60 100644 --- a/exportclight/Clightnorm.ml +++ b/exportclight/Clightnorm.ml @@ -143,7 +143,18 @@ and norm_lbl_stmt ls = | LSnil -> LSnil | LScons(n, s, ls) -> LScons(n, norm_stmt s, norm_lbl_stmt ls) -let next_var curr (v, _) = if P.lt v curr then curr else P.succ v +(* In "canonical atoms" mode, temporaries are between 2^7 and 2^12 - 1. + Below 2^7 are single-letter identifiers and above 2^12 are all + other identifiers. *) + +let first_temp = P.of_int 128 +let last_temp = P.of_int 4095 + +let next_var curr (v, _) = + if P.lt v curr + || !use_canonical_atoms && (P.lt v first_temp || P.gt v last_temp) + then curr + else P.succ v let next_var_list vars start = List.fold_left next_var start vars |