Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / cocospec / kindLustreLexer.mll @ bc504848

History | View | Annotate | Download (15.1 KB)

1
{
2
(* This file is part of the Kind 2 model checker.
3

    
4
   Copyright (c) 2015 by the Board of Trustees of the University of Iowa
5

    
6
   Licensed under the Apache License, Version 2.0 (the "License"); you
7
   may not use this file except in compliance with the License.  You
8
   may obtain a copy of the License at
9

    
10
   http://www.apache.org/licenses/LICENSE-2.0 
11

    
12
   Unless required by applicable law or agreed to in writing, software
13
   distributed under the License is distributed on an "AS IS" BASIS,
14
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
15
   implied. See the License for the specific language governing
16
   permissions and limitations under the License. 
17

    
18
*)
19

    
20

    
21
open KindLustreParser
22

    
23

    
24
(* Imported from Kind flags.ml *)
25

    
26
    (* Input flag. *)
27
  let input_file_default = ""
28
  let input_file = ref input_file_default
29
  let set_input_file f = input_file := f
30
  let input_file () = !input_file
31

    
32
    
33
 (* All files in the cone of influence of the input file. *)
34
  let all_input_files = ref []
35
  let clear_input_files () = all_input_files := []
36
  let add_input_file file =
37
    (* Additional input file're relative to main input file. *)
38
    let path = input_file () |> Filename.dirname in
39
    all_input_files := (path ^ "/" ^ file) :: ! all_input_files
40
  let get_all_input_files () = (input_file ()) :: ! all_input_files
41

    
42
(* End of Import from Kind flags.ml *)
43
                                                    
44
       
45
(* Pretty-print an array of integers *)
46
let rec pp_print_int_array i ppf a = 
47

    
48
  if i = 0 then 
49
    Format.fprintf ppf "@[<hv 3>[|";
50
  
51
  if i >= Array.length a then
52

    
53
    Format.fprintf ppf "|]@]"
54

    
55
  else
56

    
57
    ( 
58

    
59
      Format.fprintf ppf "%d" a.(i);
60

    
61
      if i+2 = Array.length a then 
62
        Format.fprintf ppf ";@ ";
63
      
64
      pp_print_int_array (succ i) ppf a
65
    
66
    )
67

    
68
(* Pretty-print a position *)
69
let pp_print_position ppf 
70
    { Lexing.pos_fname;
71
      Lexing.pos_lnum;
72
      Lexing.pos_bol;
73
      Lexing.pos_cnum } =
74

    
75
  Format.fprintf ppf 
76
    "@[<hv 2>{ pos_fname : %s;@ \
77
     pos_lnum : %d;@ \
78
     pos_bol : %d;@ \
79
     pos_cnum : %d; }@]"
80
    pos_fname
81
    pos_lnum
82
    pos_bol
83
    pos_cnum
84

    
85

    
86
(* Pretty-print a lexing buffer *)
87
let pp_print_lexbuf ppf     
88
  { Lexing.lex_buffer; 
89
    Lexing.lex_buffer_len; 
90
    Lexing.lex_abs_pos; 
91
    Lexing.lex_start_pos; 
92
    Lexing.lex_curr_pos; 
93
    Lexing.lex_last_pos;
94
    Lexing.lex_last_action;
95
    Lexing.lex_eof_reached;
96
    Lexing.lex_mem;
97
    Lexing.lex_start_p;
98
    Lexing.lex_curr_p } =
99

    
100
  Format.fprintf ppf 
101
    "@[<hv 2>{ lex_buffer : %s;@ \
102
     lex_buffer_len : %d;@ \
103
     lex_abs_pos : %d;@ \
104
     lex_start_pos : %d;@ \
105
     lex_curr_pos : %d;@ \
106
     lex_last_pos : %d;@ \
107
     lex_last_action : %d;@ \
108
     lex_eof_reached : %B;@ \
109
     lex_mem : %a;@ \
110
     lex_start_p : %a;@ \
111
     lex_curr_p : %a;@]"
112
    (Bytes.to_string lex_buffer)
113
    lex_buffer_len
114
    lex_abs_pos
115
    lex_start_pos
116
    lex_curr_pos
117
    lex_last_pos
118
    lex_last_action
119
    lex_eof_reached
120
    (pp_print_int_array 0) lex_mem
121
    pp_print_position lex_start_p
122
    pp_print_position lex_curr_p
123

    
124

    
125
  let char_for_backslash = function
126
    | 'n' -> '\010'
127
    | 'r' -> '\013'
128
    | 'b' -> '\008'
129
    | 't' -> '\009'
130
    | c -> c
131

    
132
  (* Buffer to store strings *)
133
  let string_buf = Buffer.create 1024
134

    
135
(* A stack of pairs of channels, a directory and lexing buffers to
136
   handle included files 
137

    
138
   The channel at the head of the list is the current channel to read
139
   from, the directory is the directory the channel is in, the lexing 
140
   buffer is the one to return to once all characters have been read 
141
   from the channel.
142

    
143
   Have only one lexing buffer and push a shallow copy of it to this
144
   stack when switching to an included file. At the end of the
145
   included file, restore the state of the lexing buffer from its
146
   shallow copy.
147

    
148
   When an eof is read from the lexing buffer, do not terminate but
149
   call pop_channel_of_lexbuf continue. If this raises the exception
150
   End_of_file, all input files have been read.
151
   
152
*)
153
let lexbuf_stack = ref []
154

    
155

    
156
(* Initialize the stack *)
157
let lexbuf_init channel curdir = 
158

    
159
  (* Reset input files before lexing. *)
160
  clear_input_files () ;
161

    
162
  (* A dummy lexing buffer to return to *)
163
  let lexbuf = Lexing.from_channel channel in
164

    
165
  (* Initialize the stack *)
166
  lexbuf_stack := [(channel, curdir, lexbuf)]
167

    
168

    
169
(* Switch to a new channel *)
170
let lexbuf_switch_to_channel lexbuf channel curdir = 
171

    
172
  (* Add channel and shallow copy of the previous lexing buffer to the
173
     top of the stack *)
174
  lexbuf_stack := 
175
    (channel, 
176
     curdir, 
177
     { lexbuf with 
178
         Lexing.lex_buffer = Bytes.copy lexbuf.Lexing.lex_buffer}) :: 
179
      !lexbuf_stack;
180
  
181
  (* Flush lexing buffer *)
182
  lexbuf.Lexing.lex_curr_pos <- 0;
183
  lexbuf.Lexing.lex_abs_pos <- 0;
184
  lexbuf.Lexing.lex_curr_p <- 
185
    { lexbuf.Lexing.lex_curr_p with Lexing.pos_cnum = 0 };
186
  lexbuf.Lexing.lex_buffer_len <- 0
187

    
188

    
189
(* Pop lexing buffer from the stack an restore state of the lexing buffer *)
190
let pop_channel_of_lexbuf lexbuf =
191

    
192
  match !lexbuf_stack with 
193

    
194
    (* Exception if last channel has been popped off the stack *)
195
    | [] -> raise End_of_file
196

    
197
    (* Take channel and lexing buffer from top of stack *)
198
    | (ch, _, prev_lexbuf) :: tl -> 
199

    
200

    
201
      (* Close channel *)
202
      close_in ch; 
203

    
204
      (* Pop off stack *)
205
      lexbuf_stack := tl; 
206

    
207
      (* Restore state of the lexing buffer *)
208
      lexbuf.Lexing.lex_curr_pos <- prev_lexbuf.Lexing.lex_curr_pos;
209
      lexbuf.Lexing.lex_abs_pos <- prev_lexbuf.Lexing.lex_abs_pos;
210
      lexbuf.Lexing.lex_curr_p <- prev_lexbuf.Lexing.lex_curr_p;
211
      lexbuf.Lexing.lex_buffer <- prev_lexbuf.Lexing.lex_buffer;
212
      lexbuf.Lexing.lex_buffer_len <- prev_lexbuf.Lexing.lex_buffer_len
213

    
214

    
215
(* Get the directory associated with the current channel *)
216
let curdir_of_lexbuf_stack () = match !lexbuf_stack with 
217
  | [] -> Sys.getcwd ()
218
  | (_, curdir, _) :: _ -> curdir
219

    
220

    
221

    
222
(* Function to read from the channel at the top of the stack *)
223
let read_from_lexbuf_stack buf n = 
224

    
225
  match !lexbuf_stack with 
226
    | [] -> 0
227
    | (ch, _, _) :: _ -> input ch buf 0 n
228

    
229

    
230
(* Create and populate a hashtable *)
231
let mk_hashtbl init =
232
  let tbl = List.length init |> Hashtbl.create in
233
  init |> List.iter (fun (k, v) -> Hashtbl.add tbl k v) ;
234
  tbl
235
  
236
(* Use hash tables instead of rule matches to keep numer of transition
237
   of lexer small *)
238

    
239
(* Hashtable of keywords *)
240
let keyword_table = mk_hashtbl [
241

    
242
  (* Types *)
243
  "type", TYPE ;
244
  "int", INT ;
245
  "real", REAL ;
246
  "bool", BOOL ;
247
  "subrange", SUBRANGE ;
248
  "of", OF ;
249
  (* "array", ARRAY) ; *)
250
  "struct", STRUCT ;
251
  "enum", ENUM ;
252

    
253
  (* Constant declaration *)
254
  "const", CONST ;
255
  
256
  (* Node / function declaration *)
257
  "imported", IMPORTED ;
258
  "node", NODE ;
259
  "function", FUNCTION ;
260
  "returns", RETURNS ;
261
  "var", VAR ;
262
  "let", LET ;
263
  "tel", TEL ;
264
  
265
  (* Assertion *)
266
  "assert", ASSERT ;
267

    
268
  (* Check *)
269
  "check", CHECK ;
270

    
271
  (* Annotations. *)
272
  "PROPERTY", PROPERTY ;
273
  "MAIN", MAIN ;
274
  
275
  (* Contract related things. *)
276
  "contract", CONTRACT ;
277
  "import", IMPORTCONTRACT ;
278

    
279
  (* Boolean operators *)
280
  "true", TRUE ;
281
  "false", FALSE ;
282
  "not", NOT ;
283
  "and", AND ;
284
  "xor", XOR ;
285
  "forall", FORALL ;
286
  "exists", EXISTS ;
287
  "or", OR ;
288
  "if", IF ;
289
  "then", THEN ;
290
  "else", ELSE ;
291
  "with", WITH ;
292
  "div", INTDIV ;
293
  "mod", MOD ;
294
  
295
  (* Clock operators *)
296
  "when", WHEN ;
297
  "current", CURRENT ;
298
  "condact", CONDACT ;
299
  "activate", ACTIVATE ;
300
  "initial", INITIAL ;
301
  "default", DEFAULT ;
302
  "every", EVERY ;
303
  "restart", RESTART ;
304
  "merge", MERGE ;
305

    
306
  (* Automata *)
307
  "automaton", AUTOMATON;
308
  "state", STATE;
309
  "unless", UNLESS;
310
  "until", UNTIL;
311
  "resume", RESUME;
312
  "elsif", ELSIF;
313
  "end", END;
314
  
315
  (* Temporal operators *)
316
  "pre", PRE ;
317
  "last", LAST ;
318
  "fby", FBY ;
319

    
320
  (* |===| Block annotation contract stuff. *)
321
  "mode", MODE;
322
  "assume", ASSUME;
323
  "guarantee", GUARANTEE;
324
  "require", REQUIRE;
325
  "ensure", ENSURE;
326
      
327
  ]
328

    
329
    
330
}
331

    
332

    
333
(* Identifier 
334

    
335
   C syntax: alphanumeric characters including the underscore, starting 
336
   with a letter or the underscore *)
337
let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '_' '0'-'9']*
338
         
339
(* Keep these separated from alphabetic characters, otherwise a->b would 
340
   be one token *)
341
let printable = ['+' '-' '*' '/' '>' '<' '=' ]+
342

    
343
(* Floating point decimal 
344

    
345
   Don't allow floats like "2." this will conflict with array slicing "2..3" *)
346
let decimal = ['0'-'9']* '.' ['0'-'9']+ (('E'|'e') ('+'|'-')? ['0'-'9']+)?
347

    
348
(* Floating-point decimal with exponent only *)
349
let exponent_decimal = ['0'-'9']+ '.'? ('E'|'e') ('+'|'-')? ['0'-'9']+
350

    
351
(* Integer numeral *)
352
let numeral = ['0'-'9']+
353

    
354
(* Hexadecimal numerals *)
355
let hexdigit = ['0'-'9' 'a'-'f' 'A'-'F']
356
let hexpo = 'p' ('+'|'-')? ['0'-'9']+
357

    
358
let hex_num  = "0x" hexdigit+ 
359
let hex_dec1 = "0x" hexdigit+ ('.' hexdigit*)? hexpo?
360
let hex_dec2 = "0x" '.' hexdigit+ hexpo?
361
              
362
(* Whitespace *)
363
let whitespace = [' ' '\t']
364

    
365
(* Newline *)
366
let newline = '\r'* '\n'
367

    
368
(* Toplevel function *)
369
rule token = parse
370

    
371
  (* |===| Annotations. *)
372

    
373
  (* Inline. *)
374
  |"--%" { PERCENTANNOT }
375
  |"--!" { BANGANNOT }
376

    
377
  (* Parenthesis star (PS) block annotations. *)
378
  | "(*" ('%'|'!') { PSBLOCKSTART }
379
  | "(*@" { PSATBLOCK }
380

    
381
  (* End of parenthesis star (PS). *)
382
  | "*)" { PSBLOCKEND }
383

    
384
  (* Slash star (SS) block annotations. *)
385
  | "/*" ('%'|'!') { SSBLOCKSTART }
386
  | "/*@" { SSATBLOCK }
387

    
388
  (* End of slash star (SS). *)
389
  | "*/" { SSBLOCKEND }
390

    
391

    
392
  (* |===| Actual comments. *)
393

    
394
  (* Inline.
395
    Need to have the '-'* here, otherwise "---" would be matched 
396
    as operator *)
397
  | "--" '-'* { skip_to_eol lexbuf }
398

    
399
  (* Multi-line. *)
400
  | "/*" { skip_commented_slashstar lexbuf }
401
  | "(*" { skip_commented_parenstar lexbuf }
402

    
403

    
404
  (* |===| Include file. *)
405
  | "include" whitespace* '\"' ([^'\"']* as p) '\"' {
406

    
407
    (* Open include file *)
408
    let include_channel, include_curdir =
409
      try (
410
        let include_channel, include_curdir = 
411
          open_in (Filename.concat (curdir_of_lexbuf_stack ()) p),
412
          Filename.dirname p
413
        in
414

    
415
        include_channel, include_curdir
416
      ) with Sys_error e -> 
417
        Format.sprintf "Error opening include file %s: %s" p e
418
        |> failwith
419
    in
420

    
421
    (* Add `p` to the list of input files. *)
422
    add_input_file p ;
423
    
424
    (* New lexing buffer from include file *)
425
    lexbuf_switch_to_channel lexbuf include_channel include_curdir ;
426
    
427
    Lexing.flush_input lexbuf ;
428

    
429
    (* Starting position in new file *)
430
    let zero_pos =
431
      { Lexing.pos_fname = p ;
432
        Lexing.pos_lnum = 1  ;
433
        Lexing.pos_bol = 0   ;
434
        Lexing.pos_cnum = 0  }
435
    in
436

    
437
    (* Set new position in lexing buffer *)
438
    lexbuf.Lexing.lex_curr_p <- zero_pos ;
439

    
440
    (* Continue with included file *)
441
    token lexbuf
442
  }
443

    
444
  (* Operators that are not identifiers *)
445
  | ';' { SEMICOLON }
446
  | '=' { EQUALS }
447
  | ':' { COLON }
448
  | ',' { COMMA }
449
  | '[' { LSQBRACKET }
450
  | ']' { RSQBRACKET }
451
  | '(' { LPAREN }
452
  | ')' { RPAREN }
453
  | ')' { RPAREN }
454
  | '.' { DOT }
455
  | ".." { DOTDOT }
456
  | '^' { CARET }
457
  | '{' { LCURLYBRACKET }
458
  | '}' { RCURLYBRACKET }
459
  | '}' { RCURLYBRACKET }
460
  | ".%" { DOTPERCENT }
461
  | '|' { PIPE }
462
  | "<<" { LPARAMBRACKET }
463
  | ">>" { RPARAMBRACKET }
464
  | "=>" { IMPL }
465
  | '#' { HASH }
466
  | "<=" { LTE }
467
  | ">=" { GTE }
468
  | '<' { LT }
469
  | '>' { GT }
470
  | "<>" { NEQ }
471
  | '-' { MINUS }
472
  | '+' { PLUS }
473
  | '/' { DIV }
474
  | '*' { MULT }
475
  | "->" { ARROW }
476

    
477
  (* Decimal or numeral *)
478
  | decimal as p { DECIMAL p }
479
  | exponent_decimal as p { DECIMAL p }
480
  | numeral as p { NUMERAL p }
481

    
482
  | hex_num as p { NUMERAL p }
483
  | hex_dec1 as p { DECIMAL p }
484
  | hex_dec2 as p { DECIMAL p }
485

    
486
  (* Keyword *)
487
  | id as p {
488
    (*Format.printf "seeking symbol '%s' @." p;*)
489
    try Hashtbl.find keyword_table p with Not_found -> (SYM p)
490
  }
491

    
492
  (* Identifier with quote, throw quote away *)
493
  | '\'' (id as p) { QUOTSYM p }
494

    
495
  (* Whitespace *)
496
  | whitespace { token lexbuf }
497

    
498
  (* Newline *)
499
  | newline { Lexing.new_line lexbuf ; token lexbuf }
500

    
501
  (* String *)
502
  | "\"" { Buffer.clear string_buf; string lexbuf }
503
      
504
  (* End of file *)
505
  | eof {
506
    (* Pop previous lexing buffer form stack if at end of included file *)
507
    try pop_channel_of_lexbuf lexbuf ; token lexbuf with End_of_file -> EOF
508
  }
509

    
510
  (* Unrecognized character *)
511
  | _ as c {
512
    Format.sprintf "Unrecognized token %c (0x%X)" c (Char.code c) |> failwith
513
  }
514

    
515
(* Parse until end of comment, count newlines and otherwise discard
516
   characters *)
517
and skip_commented_slashstar = parse 
518

    
519
  (* End of comment *)
520
  | "*/" { token lexbuf } 
521

    
522
  (* Count new line *)
523
  | newline { Lexing.new_line lexbuf ; skip_commented_slashstar lexbuf } 
524

    
525
  | eof { Format.sprintf "Unterminated comment" |> failwith }
526

    
527
  (* Ignore characters in comments *)
528
  | _ { skip_commented_slashstar lexbuf }
529

    
530

    
531
(* Parse until end of comment, count newlines and otherwise discard
532
   characters *)
533
and skip_commented_parenstar = parse 
534

    
535
  (* End of comment *)
536
  | "*)" { token lexbuf } 
537

    
538
  (* Count new line *)
539
  | newline { Lexing.new_line lexbuf; skip_commented_parenstar lexbuf } 
540

    
541
  | eof { Format.sprintf "Unterminated comment" |> failwith }
542

    
543
  (* Ignore characters in comments *)
544
  | _ { skip_commented_parenstar lexbuf }
545

    
546
and skip_to_eol = parse
547

    
548
  (* Count new line and resume *)
549
  | newline { Lexing.new_line lexbuf; token lexbuf } 
550

    
551
  (* Line ends at end of file *)
552
  | eof { token lexbuf }
553

    
554
  (* Ignore characters *)
555
  | _ { skip_to_eol lexbuf }
556

    
557

    
558
and return_at_eol t = parse
559

    
560
  (* Count new line and resume *)
561
  | newline { Lexing.new_line lexbuf; t } 
562

    
563
  (* Line ends at end of file *)
564
  | eof { t }
565

    
566
  (* Ignore characters *)
567
  | _ { return_at_eol t lexbuf }
568

    
569

    
570
and string = parse
571
  | "\""
572
      { STRING (Buffer.contents string_buf) }
573
  | "\\" (_ as c)
574
      { Buffer.add_char string_buf (char_for_backslash c); string lexbuf }
575
  | newline
576
      { Lexing.new_line lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
577
  | eof
578
      { failwith (Format.sprintf "Unterminated string") }
579
  | _ as c
580
      { Buffer.add_char string_buf c; string lexbuf }
581

    
582

    
583

    
584
{
585

    
586
(*
587

    
588
  (* Test code *)
589
  let main () = 
590
    
591
    (* Read all tokens and output their positions *)
592
    let rec aux ppf lexbuf =
593

    
594
      (* Read a token *)
595
      let token = token lexbuf in
596

    
597
      (* Output position and the token *)
598
      Format.fprintf 
599
        ppf 
600
        "%a %s" 
601
        pp_print_position lexbuf.Lexing.lex_start_p
602
        (Lexing.lexeme lexbuf);
603

    
604
      (* Terminate at the end of the file, otherwise continue *)
605
      if token = EOF then () else
606
        
607
        (Format.fprintf ppf "@,";
608
         aux ppf lexbuf)
609
         
610
    in
611
    
612
    (* Create lexing buffer *)
613
    let lexbuf = Lexing.from_function read_from_lexbuf_stack in
614

    
615
    (* Read from file or standard input *)
616
    let in_ch = 
617
      if Array.length Sys.argv > 1 then 
618
        (let fname = Sys.argv.(1) in    
619

    
620
         let zero_pos = 
621
           { Lexing.pos_fname = fname;
622
             Lexing.pos_lnum = 1;
623
             Lexing.pos_bol = 0;
624
             Lexing.pos_cnum = 0 } 
625
        in
626
         lexbuf.Lexing.lex_curr_p <- zero_pos; 
627

    
628
         open_in fname) 
629
      else
630
        stdin
631
    in
632

    
633
    (* Initialize lexing buffer with channel *)
634
    lexbuf_init in_ch;
635

    
636
    (* Output all tokens and their positions *)
637
    Format.printf "@[<v>%t@]@." (function ppf -> aux ppf lexbuf)
638

    
639
;;
640

    
641
main ()
642
*)
643

    
644
}
645

    
646
(* 
647
   Local Variables:
648
   compile-command: "make -C .. -k"
649
   indent-tabs-mode: nil
650
   End: 
651
*)
652