Fix: Parser now supports files with a lot of consecutive single-line …

…comments (dafny-lang#4424) This PR fixes dafny-lang#4261 I added the corresponding test. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
keyboardDrummer · Sep 15, 2023 · bfa4340 · bfa4340
1 parent 744062b
commit bfa4340
Show file tree

Hide file tree

Showing 4 changed files with 336 additions and 24 deletions.
diff --git a/Source/DafnyCore/Coco/Scanner.frame b/Source/DafnyCore/Coco/Scanner.frame
@@ -443,37 +443,46 @@ public class Scanner {
   }
 
   Token/*!*/ NextToken() {
-    Contract.Ensures(Contract.Result<Token>() != null);
-    if(!parsingTrivia) {
-      posTrailingStart = pos;
-      posTrailingEndLeadingStart = pos;
-      parsingTrivia = true;
-      triviaTrailing = pos > 0;
-      triviaNewlines = 0;
-      lastWasCr = false;
-    } else {
-      // We just skipped a comment. Any newline coming after the comment doesn't count for the splitting of the trivia
-      if(triviaTrailing && (ch == '\r' || (ch == '\n' && !lastWasCr)) && oldEols == 0) {
+    while(true) { // To avoid recursion
+      Contract.Ensures(Contract.Result<Token>() != null);
+      if(!parsingTrivia) {
+        posTrailingStart = pos;
+        posTrailingEndLeadingStart = pos;
+        parsingTrivia = true;
+        triviaTrailing = pos > 0;
         triviaNewlines = 0;
-        lastWasCr = (ch == '\r');
+        lastWasCr = false;
+      } else {
+        // We just skipped a comment. Any newline coming after the comment doesn't count for the splitting of the trivia
+        if(triviaTrailing && (ch == '\r' || (ch == '\n' && !lastWasCr)) && oldEols == 0) {
+          triviaNewlines = 0;
+          lastWasCr = (ch == '\r');
+        }
       }
-    }
-    while (ch == ' ' ||
+      while (ch == ' ' ||
 -->scan1
-    ) {
-      if(triviaTrailing && (ch == '\r' || ch == '\n') && oldEols == 0) {
-        if(ch == '\r' || (ch == '\n' && !lastWasCr)) { // Don't count \r\n as two newlines.
-          triviaNewlines++;
+      ) {
+        if(triviaTrailing && (ch == '\r' || ch == '\n') && oldEols == 0) {
+          if(ch == '\r' || (ch == '\n' && !lastWasCr)) { // Don't count \r\n as two newlines.
+            triviaNewlines++;
+          }
+          lastWasCr = (ch == '\r');
+        }
+        NextCh();
+        if(triviaTrailing && triviaNewlines == 2 && (ch != '\n' || !lastWasCr)) {
+          triviaTrailing = false;
+          posTrailingEndLeadingStart = pos;
         }
-        lastWasCr = (ch == '\r');
       }
-      NextCh();
-      if(triviaTrailing && triviaNewlines == 2 && (ch != '\n' || !lastWasCr)) {
-        triviaTrailing = false;
-        posTrailingEndLeadingStart = pos;
+      if (ch == '/' && Comment0() ||ch == '/' && Comment1()) { // From COCO's scan2
+        continue; // Avoid recursive calls to NextToken() that crashes MAC devices
       }
-    }
+      break;/*
+      // Default Coco frame
 -->scan2
+      */
+    }
+    int apx = 0; // From Coco
     parsingTrivia = false;
     if(t == null) { // There is no trailing trivia before the first token
       posTrailingEndLeadingStart = 0;

diff --git a/Test/git-issues/git-issue-4261.dfy b/Test/git-issues/git-issue-4261.dfy
@@ -0,0 +1,300 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module M {
+  // 0
+  // 1
+  // 2
+  // 3
+  // 4
+  // 5
+  // 6
+  // 7
+  // 8
+  // 9
+  // 10
+  // 11
+  // 12
+  // 13
+  // 14
+  // 15
+  // 16
+  // 17
+  // 18
+  // 19
+  // 20
+  // 21
+  // 22
+  // 23
+  // 24
+  // 25
+  // 26
+  // 27
+  // 28
+  // 29
+  // 30
+  // 31
+  // 32
+  // 33
+  // 34
+  // 35
+  // 36
+  // 37
+  // 38
+  // 39
+  // 40
+  // 41
+  // 42
+  // 43
+  // 44
+  // 45
+  // 46
+  // 47
+  // 48
+  // 49
+  // 50
+  // 51
+  // 52
+  // 53
+  // 54
+  // 55
+  // 56
+  // 57
+  // 58
+  // 59
+  // 60
+  // 61
+  // 62
+  // 63
+  // 64
+  // 65
+  // 66
+  // 67
+  // 68
+  // 69
+  // 70
+  // 71
+  // 72
+  // 73
+  // 74
+  // 75
+  // 76
+  // 77
+  // 78
+  // 79
+  // 80
+  // 81
+  // 82
+  // 83
+  // 84
+  // 85
+  // 86
+  // 87
+  // 88
+  // 89
+  // 90
+  // 91
+  // 92
+  // 93
+  // 94
+  // 95
+  // 96
+  // 97
+  // 98
+  // 99
+  // 100
+  // 101
+  // 102
+  // 103
+  // 104
+  // 105
+  // 106
+  // 107
+  // 108
+  // 109
+  // 110
+  // 111
+  // 112
+  // 113
+  // 114
+  // 115
+  // 116
+  // 117
+  // 118
+  // 119
+  // 120
+  // 121
+  // 122
+  // 123
+  // 124
+  // 125
+  // 126
+  // 127
+  // 128
+  // 129
+  // 130
+  // 131
+  // 132
+  // 133
+  // 134
+  // 135
+  // 136
+  // 137
+  // 138
+  // 139
+  // 140
+  // 141
+  // 142
+  // 143
+  // 144
+  // 145
+  // 146
+  // 147
+  // 148
+  // 149
+  // 150
+  // 151
+  // 152
+  // 153
+  // 154
+  // 155
+  // 156
+  // 157
+  // 158
+  // 159
+  // 160
+  // 161
+  // 162
+  // 163
+  // 164
+  // 165
+  // 166
+  // 167
+  // 168
+  // 169
+  // 170
+  // 171
+  // 172
+  // 173
+  // 174
+  // 175
+  // 176
+  // 177
+  // 178
+  // 179
+  // 180
+  // 181
+  // 182
+  // 183
+  // 184
+  // 185
+  // 186
+  // 187
+  // 188
+  // 189
+  // 190
+  // 191
+  // 192
+  // 193
+  // 194
+  // 195
+  // 196
+  // 197
+  // 198
+  // 199
+  // 200
+  // 201
+  // 202
+  // 203
+  // 204
+  // 205
+  // 206
+  // 207
+  // 208
+  // 209
+  // 210
+  // 211
+  // 212
+  // 213
+  // 214
+  // 215
+  // 216
+  // 217
+  // 218
+  // 219
+  // 220
+  // 221
+  // 222
+  // 223
+  // 224
+  // 225
+  // 226
+  // 227
+  // 228
+  // 229
+  // 230
+  // 231
+  // 232
+  // 233
+  // 234
+  // 235
+  // 236
+  // 237
+  // 238
+  // 239
+  // 240
+  // 241
+  // 242
+  // 243
+  // 244
+  // 245
+  // 246
+  // 247
+  // 248
+  // 249
+  // 250
+  // 251
+  // 252
+  // 253
+  // 254
+  // 255
+  // 256
+  // 257
+  // 258
+  // 259
+  // 260
+  // 261
+  // 262
+  // 263
+  // 264
+  // 265
+  // 266
+  // 267
+  // 268
+  // 269
+  // 270
+  // 271
+  // 272
+  // 273
+  // 274
+  // 275
+  // 276
+  // 277
+  // 278
+  // 279
+  // 280
+  // 281
+  // 282
+  // 283
+  // 284
+  // 285
+  // 286
+  // 287
+  // 288
+  // 289
+  // 290
+  // 291
+  // 292
+  // 293
+  // 294
+}
diff --git a/Test/git-issues/git-issue-4261.dfy.expect b/Test/git-issues/git-issue-4261.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
diff --git a/docs/dev/news/4261.fix b/docs/dev/news/4261.fix
@@ -0,0 +1 @@
+Parser now supports files with a lot of consecutive single-line comments