-
Notifications
You must be signed in to change notification settings - Fork 0
/
StrictC.grm
1920 lines (1732 loc) · 69.6 KB
/
StrictC.grm
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
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(**
** Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
**
** SPDX-License-Identifier: BSD-2-Clause
**)
open Absyn NameGeneration
val errorStr' = Feedback.errorStr'
val warnStr' = Feedback.warnStr'
val bogus = SourcePos.bogus
fun lleft [] = bogus
| lleft (h :: t) = left h
fun lright [] = bogus
| lright x = right (List.last x)
type adecl = (expr ctype -> expr ctype) wrap
type 'a ddecl = string wrap
* adecl
* (expr ctype * string wrap option) wrap list option
* 'a list
type addecl = gcc_attribute ddecl
(* composition of declarators *)
fun ooa(adec1, adec2) = let
(* composition of abstract declarators *)
val a1 = node adec1
val a2 = node adec2
in
wrap(a1 o a2, left adec1, right adec2)
end
fun ood(ddw, adec) = let
val (nm, adec0, params, data) = node ddw
in
wrap((nm, ooa(adec0,adec), params, data), left ddw, right adec)
end
infix ood
fun add_attributes(ddw, attrs) = let
val (nm, adec, ps, data0) = node ddw
in
wrap((nm, adec, ps, attrs @ data0), left ddw, right ddw)
end
fun addparams(dw : 'a ddecl wrap, ps) : 'a ddecl wrap = let
val (nm, a, pso, data) = node dw
in
case pso of
SOME _ => dw
| NONE => wrap((nm,a,SOME ps,data), left dw, right dw)
end
fun check_params
(plist : (expr ctype * string wrap option) wrap list wrap)
: (expr ctype * string wrap option) wrap list =
case node plist of
[] => (Feedback.warnStr'(left plist, right plist,
"Avoid empty parameter lists in C; \
\prefer \"(void)\"");
[])
| x as [tysw] => (case node tysw of
(Void, NONE) => []
| _ => x)
| x => x
fun fndecl l r (ps : expr ctype list) =
wrap((fn ty => Function(ty, ps)), l, r)
fun ptrdecl l r = wrap (Ptr, l, r)
fun arraydecl l r n = wrap ((fn ty => Array (ty, n)), l, r)
val one_const = expr_int 1
val zero_const = expr_int 0
fun postinc e = Assign(e,ebogwrap(BinOp(Plus,e,one_const)))
fun postdec e = Assign(e,ebogwrap(BinOp(Minus,e,one_const)))
fun resolve_fnname e =
case enode e of
Var (s,_) => s
| _ => (errorStr'(eleft e, eright e,
"Can't use this expression as function name");
"_bad name_")
fun handle_builtin_fns e =
case enode e of
EFnCall (fn_e, args) => let
in
case enode fn_e of
Var(s,_) =>
if s = NameGeneration.mkIdentUScoreSafe "__builtin_expect" then
case args of
[x,y] => x
| _ => (Feedback.errorStr'(eleft e, eright e,
"__builtin_expect must take 2 args.");
expr_int 0)
else e
| _ => e
end
| _ => e
fun delvoidcasts e =
case enode e of
TypeCast (tywrap, e0) => let
in
case node tywrap of
Void => e0
| _ => e
end
| _ => e
fun parse_stdassignop (e1,opn,e2) = let
val e2 = handle_builtin_fns e2
val r_e = case opn of
NONE => e2
| SOME abop => ewrap(BinOp(abop,e1,e2), eleft e2, eright e2)
in
case enode e2 of
EFnCall (f_e, args) => let
fun e_ok e =
case enode e of
Var _ => true
| StructDot(e0, fld) => e_ok e0
| _ => false
in
if e_ok e1 andalso opn = NONE then
AssignFnCall(SOME e1, f_e, args)
else
Assign(e1,r_e)
end
| _ => Assign(e1,r_e)
end
fun check_names (fname:string) plist = let
fun check i ps =
case ps of
[] => []
| pw :: rest =>
(case node pw of
(ty, SOME nm) => (ty,nm) :: check (i + 1) rest
| (ty, NONE) => (errorStr'(left pw, right pw,
"Parameter #"^Int.toString i^
" of function "^fname^
" has no name");
(ty, wrap("__fake", bogus, bogus)) ::
check (i + 1) rest))
in
check 1 plist
end
type struct_field = (expr ctype * string wrap * expr option)
type struct_fields = struct_field list
type struct_id_decl = string wrap * struct_fields
local val scount = ref 0
in
fun gen_struct_id () =
(scount := !scount + 1;
NameGeneration.internalAnonStructPfx^Int.toString (!scount))
end
datatype storage_class_specifier = TypeDef | Extern | Static | Auto | Register | Thread_Local
datatype type_qualifier = Const | Volatile | Restrict
datatype typespectok = ts_unsigned
| ts_signed
| ts_bool
| ts_char
| ts_int
| ts_long
| ts_longlong
| ts_short
| ts_void
type struct_or_union_specifier = expr ctype wrap * struct_id_decl wrap list
type enum_specifier = (string option wrap *
(string wrap * expr option) list) wrap
datatype type_specifier = Tstok of typespectok wrap
| Tsstruct of struct_or_union_specifier
| Tsenum of enum_specifier
| Tstypeid of string wrap
fun tsleft (Tstok tok) = left tok
| tsleft (Tsstruct (ty, _)) = left ty
| tsleft (Tstypeid s) = left s
| tsleft (Tsenum es) = left es
fun tsright (Tstok tok) = right tok
| tsright (Tsstruct (ty, _)) = right ty
| tsright (Tstypeid s) = right s
| tsright (Tsenum es) = right es
datatype decl_specifier = Storage of storage_class_specifier wrap
| TypeQual of type_qualifier wrap
| TypeSpec of type_specifier
| FunSpec of Absyn.fnspec wrap
fun scs_to_SC scs =
case scs of
Extern => SOME SC_EXTERN
| Static => SOME SC_STATIC
| Thread_Local => SOME SC_THRD_LOCAL
| Register => SOME SC_REGISTER
| Auto => SOME SC_AUTO
| TypeDef => NONE
val extract_storage_specs =
List.mapPartial (fn Storage scs_w => scs_to_SC (node scs_w)
| _ => NONE)
fun dslleft [] = raise Fail "dslleft: nil"
| dslleft (h :: t) =
case h of
Storage s => left s
| TypeQual s => left s
| FunSpec s => left s
| TypeSpec ts => tsleft ts
fun dslright dsl =
case dsl of
[] => raise Fail "dslright: nil"
| [h] => (case h of
Storage s => right s
| TypeQual s => right s
| FunSpec s => right s
| TypeSpec ts => tsright ts)
| h::t => dslright t
fun parse_siddecl (s : struct_id_decl wrap) : declaration wrap = let
val (nm, fields) = node s
fun ok_inttype ity = (ity = Int)
fun f (ty : expr ctype, s : string wrap, opbit : expr option) = let
fun error r = (errorStr'(left s, r, "Bad base-type for bitfield");
Bitfield(true, one_const))
val ty' : expr ctype =
case opbit of
NONE => ty
| SOME e => (case ty of
Signed ity =>
if ok_inttype ity then
Bitfield(true, e)
else error (eright e)
| Unsigned ity =>
if ok_inttype ity then
Bitfield(false, e)
else error (eright e)
| _ => error (eright e))
in
(ty',s)
end
val fields' = map f fields
in
wrap(StructDecl(nm, fields'), left s, right s)
end
fun empty_enumspec es = [wrap(EnumDecl (node es), left es, right es)]
fun empty_declarator (ds : decl_specifier list) : declaration wrap list =
case ds of
[] => raise Fail "empty_declarator: nil"
| Storage x :: rest =>
(errorStr'(left x, right x,
"Storage class qualifier not accompanied by \
\declarator");
empty_declarator rest)
| TypeQual tq :: rest =>
(errorStr'(left tq, right tq,
"Type-qualifier not accompanied by declarator");
empty_declarator rest)
| FunSpec fs :: rest =>
(errorStr'(left fs, right fs,
"Function-specifier not accompanied by declarator");
empty_declarator rest)
| TypeSpec (Tstok tok) :: rest =>
(errorStr'(left tok, right tok,
"Type not accompanied by declarator");
empty_declarator rest)
| TypeSpec (Tstypeid s) :: rest =>
(errorStr'(left s, right s,
"Type-id ("^node s^ ") not accompanied by declarator");
empty_declarator rest)
| [TypeSpec (Tsstruct (_, siddecls))] => map parse_siddecl siddecls
| TypeSpec (Tsstruct s) :: rest =>
(errorStr'(dslleft rest, dslright rest,
"Extraneous crap after struct declaration");
empty_declarator [TypeSpec (Tsstruct s)])
| [TypeSpec (Tsenum es)] => empty_enumspec es
| TypeSpec (Tsenum es) :: rest =>
(errorStr'(dslleft rest, dslright rest,
"Extraneous crap after enum declaration");
empty_enumspec es)
fun ity_of_tok tstok =
case node tstok of
ts_int => Int
| ts_char => Char
| ts_short => Short
| ts_long => Long
| ts_longlong => LongLong
| x => raise Fail "ty_of_tok: invariant failure"
fun sort_toks (bases, sgnmods) dsl =
case dsl of
[] => (bases, sgnmods)
| TypeSpec (Tstok tk) :: r =>
(case node tk of
ts_unsigned => sort_toks (bases, tk :: sgnmods) r
| ts_signed => sort_toks (bases, tk :: sgnmods) r
| _ => sort_toks (wrap(Tstok tk, left tk, right tk) :: bases,
sgnmods) r)
| TypeSpec (x as Tsstruct (ty,_)) :: r =>
sort_toks (wrap(x, left ty, right ty)::bases, sgnmods) r
| TypeSpec (x as Tstypeid sw) :: r =>
sort_toks (wrap(x,left sw,right sw)::bases, sgnmods) r
| TypeSpec (x as Tsenum es) :: r =>
sort_toks (wrap(x,left es, right es)::bases, sgnmods) r
| _ :: r => sort_toks (bases, sgnmods) r
fun extract_fnspecs (dsl : decl_specifier list) : fnspec list =
List.mapPartial (fn FunSpec fs => SOME (node fs) | _ => NONE) dsl
fun extract_fnspec_attrs (fs : fnspec list) : gcc_attribute list =
case fs of
[] => []
| gcc_attribs gcc_as::rest => gcc_as @ extract_fnspec_attrs rest
| _ :: rest => extract_fnspec_attrs rest
fun extract_type (dsl : decl_specifier list wrap) : expr ctype wrap = let
val (bases : type_specifier wrap list,
sgnmods : typespectok wrap list) = sort_toks ([], []) (node dsl)
fun is_base b (tn : type_specifier wrap) =
case node tn of
Tstok t => node t = b
| _ => false
fun is_intmod (tn : type_specifier wrap) =
case node tn of
Tstok t => (case node t of
ts_short => true
| ts_long => true
| _ => false)
| _ => false
fun handle_integral_remainder had_int list =
case list of
[] => NONE
| [x] => if had_int then
if is_intmod x then SOME x
else
(errorStr'(left x, right x, "Bad combination with 'int'");
SOME x)
else SOME x
| [x,y] => (case (node x, node y) of
(Tstok k1, Tstok k2) => let
(* order here is reverse of occurrence in input *)
val l = left y and r = right x
in
if node k1 = ts_long andalso node k2 = ts_long then
SOME (wrap (Tstok (wrap(ts_longlong, l, r)), l, r))
else
(errorStr'(l, r, "Two type-specifiers"); SOME x)
end
| _ => (errorStr'(left x, right x, "Two type-specifiers");
SOME x))
| h::t => (errorStr'(left h, right h, "Too many type-specifiers");
SOME h)
fun check_baseclashes list =
case list of
[] => NONE
| [x] => SOME x
| _ =>
case List.partition (is_base ts_int) list of
([], _) => handle_integral_remainder false list
| ([_], rest) => handle_integral_remainder true rest
| (t::_, _) => (errorStr'(left t, right t, "Too many 'int' specifiers");
SOME t)
fun check_modclashes list =
case list of
[] => NONE
| [x] => SOME x
| h :: t => (errorStr'(left h, right h, "Multiple type-specifiers");
SOME h)
val basety = check_baseclashes bases
val sgnmod = check_modclashes sgnmods
in
case (basety, sgnmod) of
(NONE, NONE) => (errorStr'(left dsl, right dsl,
"No base type in declaration");
wrap(Signed Int, bogus, bogus))
| (SOME b, NONE) => let
in
case node b of
Tstok tk => (case node tk of
ts_void => wrap(Void, left tk, right tk)
| ts_char => wrap(PlainChar, left tk, right tk)
| ts_bool => wrap(Bool, left tk, right tk)
| x => wrap(Signed (ity_of_tok tk),
left tk, right tk))
| Tsstruct (ty, _) => ty
| Tstypeid s => wrap(Ident (node s), left s, right s)
| Tsenum e => wrap (EnumTy (node (#1 (node e))), left e, right e)
end
| (NONE, SOME m) =>
(case node m of
ts_unsigned => wrap(Unsigned Int, left m, right m)
| ts_signed => wrap (Signed Int, left m, right m)
| x => raise Fail "finalty2: inv failure")
| (SOME b, SOME m) =>
case node b of
Tstok tk =>
(case node tk of
ts_void => (errorStr'(left m, right m,
"Signedness modifier on void");
wrap(Void, left tk, right tk))
| ts_bool => (errorStr'(left m, right m,
"Signedness modifier on _Bool");
wrap(Bool, left tk, right tk))
| _ =>
let
in
case node m of
ts_unsigned => wrap(Unsigned (ity_of_tok tk),
left m, right tk)
| ts_signed => wrap(Signed (ity_of_tok tk),
left m, right tk)
| x => raise Fail "finalty3: inv failure"
end)
| Tstypeid s => (errorStr'(left m, right m,
"Signedness modifier on typedef id");
wrap(Ident (node s), left s, right s))
| Tsstruct(ty,_) => (errorStr'(left m, right m,
"Signedness modifier on struct");
ty)
| Tsenum e => (errorStr'(left m, right m, "Signedness modifier on enum");
wrap(EnumTy (node (#1 (node e))), left e, right e))
end
(* returns a (SourcePos.t * SourcePos.t) option *)
fun has_typedef (dsl : decl_specifier list wrap) = let
fun check dsls =
case dsls of
[] => NONE
| Storage s :: rest =>
(case node s of TypeDef => SOME (left s, right s)
| _ => check rest)
| _ :: rest => check rest
in
check (node dsl)
end
(* returns a (SourcePos.t * SourcePos.t) option *)
fun has_extern (dsl : decl_specifier list wrap) = let
fun check dsls =
case dsls of
[] => NONE
| Storage s :: rest => (case node s of Extern => SOME (left s, right s)
| _ => check rest)
| _ :: rest => check rest
in
check (node dsl)
end
fun first_sdecls (dsl : decl_specifier list) =
case dsl of
[] => []
| TypeSpec (Tsstruct(ty, sdecls)) :: _ => sdecls
| _ :: rest => first_sdecls rest
fun first_enum_dec (dsl : decl_specifier list) =
case dsl of
[] => NONE
| TypeSpec (Tsenum es) :: rest => if null (#2 (node es)) then
first_enum_dec rest
else SOME es
| _ :: rest => first_enum_dec rest
fun wonky_pdec_check dsl = let
val _ =
case has_typedef dsl of
NONE => ()
| SOME (l,r) => errorStr'(l, r, "Typedefs forbidden in parameters")
val _ =
case has_extern dsl of
NONE => ()
| SOME (l,r) => errorStr'(l,r, "Extern forbidden in parameters")
val _ = case first_sdecls (node dsl) of
[] => ()
| sd :: _ => let
val sw = #1 (node sd)
in
errorStr' (left sw, right sw,
"Don't declare structs in parameters")
end
val _ = case first_enum_dec (node dsl) of
NONE => ()
| SOME es => errorStr'(left es, right es,
"Don't declare enumerations in parameters")
in
()
end
fun unwrap_params pms =
map (fn w => apsnd (Option.map node) (node w)) (valOf pms)
(* is not a function definition, is at least one declarator
This means this could be a
a) list of variable/function declarations (initialised or not)
b) list of typedefs
*)
fun make_declaration (dsl : decl_specifier list wrap)
(idl : (addecl wrap * initializer option) wrap list) =
let
val basetype = extract_type dsl
val is_typedef = isSome (has_typedef dsl)
val is_extern = isSome (has_extern dsl)
val sdecls = first_sdecls (node dsl)
val endecs = case first_enum_dec (node dsl) of
NONE => []
| SOME es => [wrap(EnumDecl (node es), left es, right es)]
val fnspecs = extract_fnspecs (node dsl)
val storage_specs = extract_storage_specs (node dsl)
val fnspec_attrs = extract_fnspec_attrs fnspecs
fun handle_declarator idw = let
val (d : addecl wrap, iopt : initializer option) = node idw
val (nm, a : adecl, params, attrs) = node d
val finaltype = (node a) (node basetype)
in
if is_typedef then let
val _ = case iopt of
SOME i => errorStr'(left idw, right idw,
"Can't initialise a typedef")
| _ => ()
in
wrap(TypeDecl[(finaltype,nm)], left idw, right idw)
end
else
case finaltype of
Function(rettype, ptys) => let
val _ = case iopt of
SOME _ => errorStr'(left idw, right idw,
"Can't initialise a function!")
| NONE => ()
in
wrap(ExtFnDecl { rettype = rettype, name = nm,
params = unwrap_params params,
specs = merge_specs [gcc_attribs attrs] fnspecs},
left idw, right idw)
end
| _ => let
val _ =
if is_extern andalso isSome iopt then
errorStr'(left idw, right idw, "Don't initialise externs")
else ()
in
wrap(VarDecl(finaltype, nm, storage_specs, iopt,
fnspec_attrs @ attrs ),
left idw, right idw)
end
end
in
endecs @
map handle_declarator idl @
map parse_siddecl sdecls
end
fun last_blockitem (bilist : block_item list) = let
val bi = List.last bilist
fun recurse bi =
case bi of
BI_Stmt st => (case snode st of
Block bilist => last_blockitem bilist
| _ => bi)
| _ => bi
in
recurse bi
end
fun CaseEndBI bi =
case bi of
BI_Stmt st => CaseEndStmt st
| BI_Decl d => false
and CaseEndStmt st =
case snode st of
Break => true
| Return _ => true
| ReturnFnCall _ => true
| IfStmt(g, t, e) => CaseEndStmt t andalso CaseEndStmt e
| Block bilist => CaseEndBI (last_blockitem bilist)
| _ => false
fun front [] = []
| front [h] = []
| front (x::xs) = x :: front xs
fun removelast_if_break bilist = let
fun singcase bi =
case bi of
BI_Stmt st => let
in
case snode st of
Break => []
| Block bilist => [BI_Stmt
(swrap (Block (removelast_if_break bilist),
sleft st, sright st))]
| _ => [bi]
end
| _ => [bi]
in
case bilist of
[] => []
| [bi] => singcase bi
| bi :: bis => bi :: removelast_if_break bis
end
fun mk_defaultcase_last caselist = let
fun extract_default caselist =
case caselist of
[] => (NONE, [])
| (c as (labs, bilist)) :: rest => let
fun is_dflt lab =
case node lab of
NONE => true
| _ => false
in
case List.find is_dflt (node labs) of
NONE => let
val (df, rest) = extract_default rest
in
(df, c::rest)
end
| SOME d => let
in
if length (node labs) > 1 then
warnStr'(left d, right d,
"This default: label should be the only label\
\ associated with this case")
else ();
(SOME (wrap([d], left labs, right labs), bilist), rest)
end
end
val (dflt, rest) = extract_default caselist
in
case dflt of
NONE => caselist @ [(bogwrap [bogwrap NONE],
[BI_Stmt (swrap(EmptyStmt, bogus, bogus))])]
| SOME d => rest @ [d]
end
fun switch_check scaselist leftp rightp = let
val _ = case length scaselist of
0 => errorStr'(leftp, rightp, "Switch has no cases")
| 1 => errorStr'(leftp, rightp, "Switch has only one case")
| _ => ()
fun check_for_breaks (labs, bilist) =
if not (CaseEndBI (last_blockitem bilist)) then
errorStr'(left labs, right labs,
"Switch case beginning here does not end with a break \
\or return")
else ()
val _ = app check_for_breaks (front scaselist)
(* only check front of list, allowing for last case to fall through
to end without a break *)
val scaselist = mk_defaultcase_last scaselist
fun striplabwrap (lab : expr option wrap) = node lab
fun striplablist llist = map striplabwrap (node llist)
in
map (fn (labs,bod) => (striplablist labs, removelast_if_break bod)) scaselist
end
fun check_for_proto d = let
val dec = node d
in
case dec of
ExtFnDecl _ => (errorStr'(left d, right d,
"Don't put function prototypes other than at \
\top level"); d)
| _ => d
end
%%
%name StrictC
%arg (source) : SourceFile.t
%nodefault
%keyword YWHILE YDO YIF STRUCT YRETURN YELSE INT CHAR LONG SHORT UNSIGNED TYPEDEF YSEMI LCURLY RCURLY
%change -> YSEMI
%nonterm begin of ext_decl list
| translation_unit of ext_decl list
| external_declaration of ext_decl list
| optfnspec of string option wrap
| optvolatile of bool
| storage_class_specifier of storage_class_specifier wrap
| enum_specifier of enum_specifier
| enumerator_list of (string wrap * expr option) list
| enumerator of (string wrap * expr option)
| type_qualifier of type_qualifier wrap
| type_qualifier_list of type_qualifier wrap list
| function_specifiers of fnspec wrap list wrap
| special_function_spec of fnspec wrap
| special_function_specs of fnspec wrap list wrap
| fnspecs of string wrap
| rel_spec of string wrap
| modlist of string wrap list
| invariant of string wrap
| invariant_option of string wrap option
| declaration_specifiers of decl_specifier list wrap
| specifier_qualifier_list of decl_specifier list wrap
| initializer_list of (designator list * initializer) list
| dinitializer of (designator list * initializer)
| initializer of initializer wrap
| designation of designator list
| designator_list of designator list
| designator of designator
| declaration of declaration wrap list
| struct_declaration_list of
struct_fields wrap * struct_id_decl wrap list
| struct_declaration of struct_fields wrap * struct_id_decl wrap list
| type_definition of declaration
| elementary_type of expr ctype
| integral_type of inttype wrap
| type_name of expr ctype wrap
| block_item_list of block_item list
| block_item of block_item list
| parameter_declaration of (expr ctype * string wrap option) wrap
| parameter_list of (expr ctype * string wrap option) wrap list wrap
| parameter_list1 of (expr ctype * string wrap option) wrap list wrap
| function_definition of ext_decl
| compound_statement of block_item list wrap
| statement of statement
| statement_list of statement list
| statement_list1 of statement list
| switchcase_list of (expr option wrap list wrap * block_item list) list
| switchcase of (expr option wrap list wrap * block_item list)
| labellist of expr option wrap list wrap
| label of expr option wrap
| opt_for1_bitem of block_item list
| opt_for1_expr of statement
| opt_for1_expr0 of statement list
| opt_for1_exprbase of statement
| opt_for2_expr of expr
| opt_for3_expr of statement
| opt_for3_expr0 of statement list
| opt_for3_exprbase of statement
| assignop of binoptype option
| pointer of adecl
| declarator of addecl wrap
| abstract_declarator of adecl
| direct_abstract_declarator of adecl
| struct_declarator of (addecl wrap * expr option) wrap
| struct_declarator_list of (addecl wrap * expr option) list wrap
| init_declarator of (addecl wrap * initializer option) wrap
| init_declarator_list of (addecl wrap * initializer option) wrap list
| direct_declarator of addecl wrap
| asm_declarator_mod of unit
| type_specifier of type_specifier
| struct_or_union_specifier of struct_or_union_specifier
| struct_id of string wrap
| lexpression of expr
| rexpression of expr
| rexpr_list of expr list wrap
| opt_rexpr_list of expr list wrap
| logical_AND_expression of expr
| logical_OR_expression of expr
| inclusive_OR_expression of expr
| exclusive_OR_expression of expr
| AND_expression of expr
| equality_expression of expr
| relational_expression of expr
| additive_expression of expr
| shift_expression of expr
| multiplicative_expression of expr
| unary_expression of expr
| cast_expression of expr
| postfix_expression of expr
| primary_expression of expr
| constant of literalconstant
| idlist of string wrap list
| attribute of gcc_attribute
| attribute_specifier of gcc_attribute list wrap
| attribute_list of gcc_attribute list
| attribute_parameter_list1 of expr list
| asmblock of asmblock
| asmmod1 of namedstringexp list * namedstringexp list * string list
| asmmod2 of namedstringexp list * string list
| asmmod3 of string list
| cstring_literal of string wrap
| stringlist1 of string list
| namedstringexp of namedstringexp
| namedstringexplist of namedstringexp list
| namedstringexplist1 of namedstringexp list
| calls_block of string wrap list option
%term EOF
| YSTAR | SLASH | MOD
| LPAREN | RPAREN | LCURLY | RCURLY | LBRACKET | RBRACKET
| YCOMMA | YSEMI | YCOLON | QMARK
| YEQ | YDOT | YPLUS | YMINUS | YAND | YNOT | YAMPERSAND | YBITNOT
| PLUSPLUS | MINUSMINUS
| PLUSEQ | MINUSEQ | BANDEQ | BOREQ | MULEQ
| DIVEQ | MODEQ | BXOREQ | LSHIFTEQ | RSHIFTEQ
| YENUM
| YIF | YELSE | YWHILE | YDO | YRETURN | YBREAK | YCONTINUE | YFOR
| SWITCH | CASE | DEFAULT
| YSIZEOF
| LOGICALOR | LOGICALAND | BITWISEOR | BITWISEXOR
| EQUALS | NOTEQUALS
| YLE | YGE | YLESS | YGREATER | LEFTSHIFT | RIGHTSHIFT
| INT | BOOL | CHAR | LONG | SHORT | SIGNED | UNSIGNED | VOID
| ARROW
| ID of string | TYPEID of string
| NUMERIC_CONSTANT of Absyn.numliteral_info
| STRUCT | UNION | TYPEDEF | EXTERN | CONST | VOLATILE | RESTRICT
| INVARIANT
| INLINE | STATIC | NORETURN | THREAD_LOCAL | AUTO
| FNSPEC
| RELSPEC
| AUXUPD
| GHOSTUPD
| MODIFIES
| CALLS
| OWNED_BY
| SPEC_BEGIN
| SPEC_END
| DONT_TRANSLATE
| STRING_LITERAL of string
| SPEC_BLOCKEND
| GCC_ATTRIBUTE
| YASM
| YREGISTER
%eop EOF
%pos SourcePos.t
%noshift EOF
%start begin
%verbose
%%
begin : translation_unit (translation_unit)
translation_unit
: external_declaration
(external_declaration)
| external_declaration translation_unit
(external_declaration @ translation_unit)
external_declaration
: function_definition
([function_definition])
| declaration
(map Decl declaration)
| YSEMI ([])
storage_class_specifier : TYPEDEF (wrap(TypeDef, TYPEDEFleft, TYPEDEFright))
| EXTERN (wrap(Extern, EXTERNleft, EXTERNright))
| STATIC (wrap(Static, STATICleft, STATICright))
| YREGISTER (wrap(Register, YREGISTERleft, YREGISTERright))
| AUTO (wrap(Auto, AUTOleft, AUTOright))
| THREAD_LOCAL (wrap(Thread_Local, THREAD_LOCALleft,
THREAD_LOCALright))
function_specifiers
: INLINE (wrap([], INLINEleft, INLINEright)) (* totally ignored by us *)
| NORETURN (wrap([wrap(gcc_attribs [GCC_AttribID "noreturn"],
NORETURNleft, NORETURNright)],
NORETURNleft, NORETURNright))
| special_function_specs SPEC_BLOCKEND
(special_function_specs)
| attribute_specifier
(wrap ([apnode gcc_attribs attribute_specifier],
left attribute_specifier,
right attribute_specifier))
attribute_specifier
: GCC_ATTRIBUTE LPAREN LPAREN attribute_list RPAREN RPAREN
(wrap(attribute_list, GCC_ATTRIBUTEleft, RPAREN2right))
| OWNED_BY ID SPEC_BLOCKEND
(wrap([OWNED_BY ID], OWNED_BYleft, SPEC_BLOCKENDright))
attribute_list
: ([])
| attribute ([attribute])
| attribute YCOMMA attribute_list
(attribute :: attribute_list)
attribute
: ID (let val idstr = if String.isPrefix "__" ID andalso
String.sub(ID,size ID - 1) = #"_" andalso
String.sub(ID,size ID - 2) = #"_" andalso
size ID > 4
then
String.substring(ID,2,size ID - 4)
else ID
in
GCC_AttribID idstr
end)
| CONST (GCC_AttribID "const")
| ID LPAREN RPAREN
(GCC_AttribFn (ID, []))
| ID LPAREN attribute_parameter_list1 RPAREN
(GCC_AttribFn (ID, attribute_parameter_list1))
attribute_parameter_list1
: rexpression ([rexpression])
| rexpression YCOMMA attribute_parameter_list1
(rexpression :: attribute_parameter_list1)
special_function_specs
: special_function_spec
(wrap([special_function_spec], left special_function_spec,
right special_function_spec))
| special_function_spec special_function_specs
(wrap (special_function_spec :: node special_function_specs,
left special_function_spec,
right special_function_specs))
special_function_spec
: MODIFIES idlist
(case idlist of
[] => wrap(fn_modifies [], MODIFIESleft, MODIFIESright)
| _ => wrap(fn_modifies (map node idlist),
MODIFIESleft,
right (List.last idlist)))
| FNSPEC fnspecs
(wrap(fnspec fnspecs, FNSPECleft, right fnspecs))
| RELSPEC rel_spec
(wrap(relspec rel_spec, RELSPECleft, right rel_spec))
| DONT_TRANSLATE
(wrap(didnt_translate, DONT_TRANSLATEleft, DONT_TRANSLATEright))
fnspecs
: ID YCOLON STRING_LITERAL
(wrap(ID ^ ": \"" ^ STRING_LITERAL ^ "\"", IDleft,
STRING_LITERALright))
| ID YCOLON STRING_LITERAL fnspecs
(wrap((ID ^ ": \"" ^ STRING_LITERAL ^ "\"\n" ^ node fnspecs,
IDleft,
right fnspecs)))
rel_spec
: STRING_LITERAL (wrap("\"" ^ STRING_LITERAL ^ "\"", STRING_LITERALleft,
STRING_LITERALright))
idlist
: ([])
| ID idlist
(wrap(ID,IDleft,IDright) :: idlist)
| LBRACKET YSTAR RBRACKET idlist
(wrap(NameGeneration.phantom_state_name, LBRACKETleft,
RBRACKETright) :: idlist)
(* there's ridiculous magic happening here to cope with the fact that
typedefs can happen just a token away from a use of the same identifier
as a new type.
For example
typedef int * intptr ;
intptr y;
That "intptr" has to change its lexical status from normal id to typename
id in the space of one semi-colon.
*)
declaration
: declaration_specifiers YSEMI
(empty_declarator (node declaration_specifiers))
(*| declaration_specifiers init_declarator_list attribute_specifier YSEMI
(let
val dspecs' = FunSpec
(apnode GCC_Attributes
attribute_specifier) ::
node declaration_specifiers
val ds_w = wrap(dspecs',
left declaration_specifiers,
right attribute_specifier)
in
make_declaration ds_w init_declarator_list
end) *)
| declaration_specifiers init_declarator_list YSEMI
(make_declaration declaration_specifiers init_declarator_list)