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
(** To import spec from include file *)
open Logic_ptree
let dkey = Options.register_category "trace-inputs"
let get_input_channel ~pfile = open_in pfile
let get_input_channel ~iDir ~pfile =
Options.debug ~level:2 ~dkey "Looking for file: %s@." pfile;
if not (Filename.is_relative pfile) then (get_input_channel ~pfile), pfile
else
let get_channel ~dir =
let pfile = Filename.concat dir pfile in
(get_input_channel ~pfile), pfile
in
let rec get_input = function
| [] -> get_input_channel ~pfile, pfile
| [dir] -> get_channel ~dir
| dir::dirs -> (try get_channel ~dir with | _ -> get_input dirs)
in
get_input iDir
exception Eof of (Logic_ptree.ext_spec * string)
let parse ~iDir ~pfile ~init_module_from_file_name ~init_typenames ast =
try
let inc, file = get_input_channel ~iDir ~pfile in
try
Paste.init_ast ~file:(Filepath.of_string file)
~init_module_from_file_name ~init_typenames ast;
let lexbuf = Lexing.from_channel inc in
lexbuf.Lexing.lex_curr_p <-
{lexbuf.Lexing.lex_curr_p with Lexing.pos_fname=file;};
try
let ext_spec = Logic_lexer.ext_spec lexbuf
in raise (Eof ((ext_spec,file))) ;
with
| Failure s ->
Options.abort
~source:(Cil_datatype.Position.of_lexing_pos lexbuf.Lexing.lex_curr_p)
"[Failure while parsing] %s."
s
| Sys_error s ->
Options.abort
~source:(Cil_datatype.Position.of_lexing_pos lexbuf.Lexing.lex_curr_p)
"[System error while parsing] %s."
s
| Logic_utils.Not_well_formed(loc, s) ->
Options.abort ~source:(fst loc)
"[Syntax error] %s (near %s)." s
(Lexing.lexeme lexbuf)
| Parsing.Parse_error ->
Options.abort
~source:(Cil_datatype.Position.of_lexing_pos lexbuf.Lexing.lex_curr_p)
"[Syntax error] %s."
(Lexing.lexeme lexbuf)
with
| exn ->
close_in_noerr inc ;
raise exn
with
| Eof ext_spec_file -> ext_spec_file
let pp_stmt_markup = Pretty_utils.pp_list ~sep:" " Format.pp_print_string
type loop_markup_t =
| LoopBody
| LoopStmt
| Loop
type markup_t =
| AtLoop of loop_markup_t * int
| AtCallN of int
| AtCallF of Kernel_function.t option * int
| AtAsm of int
| AtStmt of int
| AtLabel of string
| AtReturn
| AtError
exception StmtMarkupError
let typecheck ~iDir ext_spec_file ast =
let decode =
let decode_pos number =
let v = int_of_string number in
if v <= 0 then raise StmtMarkupError;
v
in
let decode_place = function
| "stmt" -> LoopStmt
| "body" -> LoopBody
| _ -> raise StmtMarkupError
in function
| "loop"::loop_place::number::[] -> (try AtLoop (decode_place loop_place, decode_pos number) with _ -> AtError)
| "loop"::number::[] -> (try AtLoop (Loop, decode_pos number) with _ -> AtError)
| "asm"::number::[] -> (try AtAsm (decode_pos number) with _ -> AtError)
| "indirect_call"::[] -> AtCallF (None, 0)
| "call"::id_number::[] ->
(try AtCallN (int_of_string id_number) with _ -> (try AtCallF (Some (Paste.find_kf id_number), 0) with _ -> AtError))
| "indirect_call"::number::[] -> (try AtCallF (None, decode_pos number) with _ -> AtError)
| "call"::id::number::[] -> (try AtCallF (Some (Paste.find_kf id), decode_pos number) with _ -> AtError)
| "return"::[] -> AtReturn
| markup::[] -> (try AtStmt (decode_pos markup) with _ -> AtLabel markup)
| _ -> AtError
in
let rec typecheck (ext_spec, parsed_file) =
let dir = Filename.dirname parsed_file::iDir in
let paste_decl_spec = function
| Ext_decl decl -> if Options.continue_after_parsing () then Paste.add_global_annot [decl]
| Ext_macro (is_global_scope, macro, def) -> if Options.continue_after_parsing () then Paste.add_macro ~is_global_scope macro def
| Ext_include (_wide, pfile, _loc) ->
let ext_spec_file =
parse ~iDir:dir ~pfile ~init_module_from_file_name:false ~init_typenames:false ast
in
typecheck ext_spec_file
in
let paste_fun_spec = function
| Ext_glob decl_spec -> paste_decl_spec decl_spec
| Ext_spec (spec, loc) -> if Options.continue_after_parsing () then Paste.add_funspec spec loc
| Ext_stmt (stmt_markup, annot, (source,_loc2)) ->
if Options.continue_after_parsing () then
begin
let at_markup = decode stmt_markup in
try
let adds =
match at_markup, annot with
| AtLoop (Loop, loop), Acode_annot _
| AtLoop (LoopBody, loop), _ -> Paste.add_annots ~loop_number:loop (Paste.find_loop_body_set_from_loop_number ~source loop)
| AtLoop (Loop, loop), _
| AtLoop (LoopStmt, loop), _ -> Paste.add_annots (Paste.find_loop_stmt_set_from_loop_number ~source loop)
| AtStmt sid, _ -> Paste.add_annots (Paste.find_stmt_set_from_sid ~source sid)
| AtLabel label, _ -> Paste.add_annots (Paste.find_stmt_set_from_label ~source label)
| AtCallN call, _ -> Paste.add_annots (Paste.find_stmt_set_from_call_number ~source call)
| AtCallF (kf_opt, num_opt),_ -> Paste.add_annots (Paste.find_stmt_set_from_call_to ~source kf_opt num_opt)
| AtAsm asm, _ -> Paste.add_annots (Paste.find_stmt_set_from_asm_number ~source asm)
| AtReturn, _ -> Paste.add_annots (Paste.find_stmt_set_from_return ~source ())
| AtError, _ -> raise StmtMarkupError
in
match annot with
| Aloop_annot (loc, annots) ->
adds loc annots;
| Acode_annot (loc, annot) ->
adds loc [annot]
| Adecl _ ->
Options.annot_error ~source "disallowed declaration by ACSL importer."
| Aspec ->
Options.annot_error ~source "disallowed incomplete function specification by ACSL importer."
with
| StmtMarkupError ->
Options.annot_error ~source "invalid statement markup '%a' for ACSL importer."
pp_stmt_markup stmt_markup
| Paste.Kf_not_found ->
Options.annot_error ~source "invalid function markup for ACSL importer."
| Paste.Stmt_not_found kf ->
begin
match at_markup, annot with
| AtLoop(Loop, loop), Acode_annot _
| AtLoop(LoopBody, loop), _ ->
Options.annot_error ~source "loop body %d not found into %a function for ACSL importer."
loop Kernel_function.pretty kf
| AtLoop(Loop, loop), _
| AtLoop(LoopStmt, loop), _ ->
Options.annot_error ~source "loop %d not found into %a function for ACSL importer."
loop Kernel_function.pretty kf
| AtStmt sid, _ ->
Options.annot_error ~source "statement ID %d not found into %a function for ACSL importer."
sid Kernel_function.pretty kf
| AtLabel label, _ ->
Options.annot_error ~source "statement label %S not found into %a function for ACSL importer."
label Kernel_function.pretty kf
| AtCallN _, _
| AtCallF _, _ ->
Options.annot_error ~source "call %a not found into %a function for ACSL importer."
pp_stmt_markup (match stmt_markup with _::m | m -> m) Kernel_function.pretty kf
| AtAsm asm, _ ->
Options.annot_error ~source "assembly call %d not found into %a function for ACSL importer."
asm Kernel_function.pretty kf
| AtReturn, _ ->
Options.annot_error ~source "return statement not found into %a function for ACSL importer."
Kernel_function.pretty kf
| AtError, _ ->
Options.annot_error ~source "invalid statement markup '%a' for ACSL importer."
pp_stmt_markup stmt_markup
end
end
in
let paste_function_spec (f,specs) =
if Options.continue_after_parsing () then
(match f with | None -> () | Some f -> Paste.set_current_function f) ;
List.iter paste_fun_spec specs ;
in
let paste_module_spec (m,decl_specs,fun_specs) =
if Options.continue_after_parsing () then
(match m with | None -> () | Some m -> Paste.set_current_module ~is_from_file_name:false m) ;
List.iter paste_decl_spec decl_specs ;
List.iter paste_function_spec fun_specs ;
in
List.iter paste_module_spec ext_spec
in
typecheck ext_spec_file
let import ~iDir ~pfile ~init_typenames ast =
try
let ext_spec_file = parse ~iDir:[] ~pfile
~init_module_from_file_name:true ~init_typenames ast
in
typecheck ~iDir ext_spec_file ast;
let mode = match (Options.continue_after_typing ()), (Options.continue_after_parsing ()) with
| true,true -> ""
| true,false -> "full parsing (without import)"
| false,_ -> "full typing (without import)"
in
Options.feedback "Success%s for %s" mode (Filename.basename pfile) ;
Paste.MacroIndex.clear_macro_table Paste.MacroIndex.Sfile ;
with
| exn ->
Paste.MacroIndex.clear_macro_table Paste.MacroIndex.Sfile ;
raise exn