1 | (* *********************************************************************) |
---|
2 | (* *) |
---|
3 | (* The Compcert verified compiler *) |
---|
4 | (* *) |
---|
5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
6 | (* *) |
---|
7 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
8 | (* Automatique. All rights reserved. This file is distributed *) |
---|
9 | (* under the terms of the GNU General Public License as published by *) |
---|
10 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
11 | (* (at your option) any later version. This file is also distributed *) |
---|
12 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
13 | (* *) |
---|
14 | (* *********************************************************************) |
---|
15 | |
---|
16 | |
---|
17 | open Cabs |
---|
18 | |
---|
19 | let nextident = ref 0 |
---|
20 | let getident () = |
---|
21 | nextident := !nextident + 1; |
---|
22 | !nextident |
---|
23 | |
---|
24 | let currentLoc_lexbuf lb = |
---|
25 | let p = Lexing.lexeme_start_p lb in |
---|
26 | { lineno = p.Lexing.pos_lnum; |
---|
27 | filename = p.Lexing.pos_fname; |
---|
28 | byteno = p.Lexing.pos_cnum; |
---|
29 | ident = getident ();} |
---|
30 | |
---|
31 | let currentLoc () = |
---|
32 | let p = Parsing.symbol_start_pos() in |
---|
33 | { lineno = p.Lexing.pos_lnum; |
---|
34 | filename = p.Lexing.pos_fname; |
---|
35 | byteno = p.Lexing.pos_cnum; |
---|
36 | ident = getident ();} |
---|
37 | |
---|
38 | let cabslu = {lineno = -10; |
---|
39 | filename = "cabs loc unknown"; |
---|
40 | byteno = -10; |
---|
41 | ident = 0} |
---|
42 | |
---|
43 | (*********** HELPER FUNCTIONS **********) |
---|
44 | |
---|
45 | let missingFieldDecl = ("___missing_field_name", JUSTBASE, [], cabslu) |
---|
46 | |
---|
47 | let rec isStatic = function |
---|
48 | [] -> false |
---|
49 | | (SpecStorage STATIC) :: _ -> true |
---|
50 | | _ :: rest -> isStatic rest |
---|
51 | |
---|
52 | let rec isExtern = function |
---|
53 | [] -> false |
---|
54 | | (SpecStorage EXTERN) :: _ -> true |
---|
55 | | _ :: rest -> isExtern rest |
---|
56 | |
---|
57 | let rec isInline = function |
---|
58 | [] -> false |
---|
59 | | SpecInline :: _ -> true |
---|
60 | | _ :: rest -> isInline rest |
---|
61 | |
---|
62 | let rec isTypedef = function |
---|
63 | [] -> false |
---|
64 | | SpecTypedef :: _ -> true |
---|
65 | | _ :: rest -> isTypedef rest |
---|
66 | |
---|
67 | |
---|
68 | let get_definitionloc (d : definition) : cabsloc = |
---|
69 | match d with |
---|
70 | | FUNDEF(_, _, l, _) -> l |
---|
71 | | DECDEF(_, l) -> l |
---|
72 | | TYPEDEF(_, l) -> l |
---|
73 | | ONLYTYPEDEF(_, l) -> l |
---|
74 | | GLOBASM(_, l) -> l |
---|
75 | | PRAGMA(_, l) -> l |
---|
76 | | LINKAGE (_, l, _) -> l |
---|
77 | |
---|
78 | let get_statementloc (s : statement) : cabsloc = |
---|
79 | begin |
---|
80 | match s with |
---|
81 | | NOP(loc) -> loc |
---|
82 | | COMPUTATION(_,loc) -> loc |
---|
83 | | BLOCK(_,loc) -> loc |
---|
84 | (* | SEQUENCE(_,_,loc) -> loc *) |
---|
85 | | IF(_,_,_,loc) -> loc |
---|
86 | | WHILE(_,_,loc) -> loc |
---|
87 | | DOWHILE(_,_,loc) -> loc |
---|
88 | | FOR(_,_,_,_,loc) -> loc |
---|
89 | | BREAK(loc) -> loc |
---|
90 | | CONTINUE(loc) -> loc |
---|
91 | | RETURN(_,loc) -> loc |
---|
92 | | SWITCH(_,_,loc) -> loc |
---|
93 | | CASE(_,_,loc) -> loc |
---|
94 | | CASERANGE(_,_,_,loc) -> loc |
---|
95 | | DEFAULT(_,loc) -> loc |
---|
96 | | LABEL(_,_,loc) -> loc |
---|
97 | | GOTO(_,loc) -> loc |
---|
98 | | COMPGOTO (_, loc) -> loc |
---|
99 | | DEFINITION d -> get_definitionloc d |
---|
100 | | ASM(_,_,_,loc) -> loc |
---|
101 | | TRY_EXCEPT(_, _, _, loc) -> loc |
---|
102 | | TRY_FINALLY(_, _, loc) -> loc |
---|
103 | end |
---|
104 | |
---|
105 | |
---|
106 | let explodeStringToInts (s: string) : int64 list = |
---|
107 | let rec allChars i acc = |
---|
108 | if i < 0 then acc |
---|
109 | else allChars (i - 1) (Int64.of_int (Char.code (String.get s i)) :: acc) |
---|
110 | in |
---|
111 | allChars (-1 + String.length s) [] |
---|
112 | |
---|
113 | let valueOfDigit chr = |
---|
114 | let int_value = |
---|
115 | match chr with |
---|
116 | '0'..'9' -> (Char.code chr) - (Char.code '0') |
---|
117 | | 'a'..'z' -> (Char.code chr) - (Char.code 'a') + 10 |
---|
118 | | 'A'..'Z' -> (Char.code chr) - (Char.code 'A') + 10 |
---|
119 | | _ -> assert false in |
---|
120 | Int64.of_int int_value |
---|
121 | |
---|
122 | let string_of_cabsloc l = |
---|
123 | Printf.sprintf "%s:%d" l.filename l.lineno |
---|
124 | |
---|
125 | let format_cabsloc pp l = |
---|
126 | Format.fprintf pp "%s:%d" l.filename l.lineno |
---|