-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathrpp_extend_checker.ml
258 lines (243 loc) · 11 KB
/
rpp_extend_checker.ml
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
(**************************************************************************)
(* This file is part of RPP plug-in of Frama-C. *)
(* *)
(* Copyright (C) 2016-2023 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file LICENSE). *)
(**************************************************************************)
open Filecheck
open Cil_types
let fun_type_param p =
match p.vtype with
| TFun (_,Some t,_,_) -> t
| TFun (_,None,_,_) -> []
| _ -> assert false;;
let fun_type_return p =
match p.vtype with
| TFun (t,_,_,_) -> t
| _ -> assert false;;
let id_checker identifier loc id_hash =
match identifier with
| FormalLabel(s) ->
( match Str.bounded_split (Str.regexp "_") s 2 with
| "Pre":: id :: [] | "Post" :: id :: []->
if not (Hashtbl.mem id_hash id) then
Rpp_options.Self.fatal ~source:loc "Unknown label: @ @[%s@] @." s
| _ -> ())
| _ -> ()
let id_update identifier loc id_hash =
match identifier with
| FormalLabel(s) ->
(match Str.bounded_split (Str.regexp "_") s 2 with
| "Pre":: id :: [] ->
let _ = try (Hashtbl.find id_hash id) with
| Not_found -> Rpp_options.Self.fatal ~source:loc"Unknown label: @ @[%s@] @." s
| _ -> assert false
in
BuiltinLabel(Pre)
| "Post" :: id :: []->
let _ = try (Hashtbl.find id_hash id) with
| Not_found -> Rpp_options.Self.fatal ~source:loc "Unknown label: @ @[%s@] @." s
| _ -> assert false
in
BuiltinLabel(Here)
| _ -> identifier)
| _ -> identifier
let check_param_type param funct loc=
List.iter2 (fun x (_,t,_) ->
match x.term_type with
| Ctype(ty) ->
if Cil_datatype.Typ.equal t ty then ()
else
Rpp_options.Self.fatal ~source:loc
"Cast are not supported:@. @[%a and %a are not \
compatible@] for term @[%a@] in callpure of %s @."
(Printer.pp_logic_type) x.term_type
(Printer.pp_typ) t (Printer.pp_term) x (funct.vname)
| Linteger ->
begin match t with
| TInt _ -> ()
| _ -> Rpp_options.Self.fatal ~source: loc
"Cast are not supported:@. @[%a and %a are not compatible@] \
for term @[%a@] in callpure of %s @."
(Printer.pp_logic_type) x.term_type (Printer.pp_typ) t
Printer.pp_term x (funct.vname)
end
| Lreal ->
begin match t with
| TFloat _ -> ()
| _ -> Rpp_options.Self.fatal ~source: loc
"Cast are not supported:@. @[%a and %a are not compatible@] \
for term @[%a@] in callpure of %s @."
(Printer.pp_logic_type) x.term_type (Printer.pp_typ) t
Printer.pp_term x (funct.vname)
end
| _ -> Rpp_options.Self.fatal ~source:loc
"Function %s is called with a parameter with type \
is not a C type:@. @[%a@] @." (funct.vname) Printer.pp_term x
) param (fun_type_param funct)
let rpp_extend_checker check =
let module Origin = (val check: Extensible_checker) in
let module New_check =
struct
class check ?is_normalized id = object(self)
inherit Origin.check ?is_normalized id as super
val id_hash = Hashtbl.create 3
method! vterm t =
let (loc,_) = t.term_loc in
match t.term_node with
| Tapp({l_var_info={lv_name ="\\callpure"}},[],terms) ->
begin
match terms with
| {term_node = TConst (Integer(_,_))} :: q ->
begin
match q with
| {term_node=TLval(TVar({lv_origin=Some(x)}),TNoOffset)} :: p ->
begin
match x with
| {vtype=TFun(_)} ->
check_param_type p x loc;
if Cil_datatype.Logic_type.equal (t.term_type) (Ctype(fun_type_return x)) then ()
else
begin
Rpp_options.Self.fatal ~source:loc
"\\callpure type (@[%a@]) is different from result type \
of function @[%a@] (@[%a@]):@.@[%a@]"
Printer.pp_logic_type (t.term_type) Printer.pp_varinfo x
Printer.pp_logic_type (Ctype(fun_type_return x))
(Printer.pp_term) t
end;
Cil.DoChildren
| _ -> Rpp_options.Self.fatal ~source:loc
"Expected a function as seconde parameter::@. @[%a@] @."
(Printer.pp_term) t
end
| _ -> Rpp_options.Self.fatal ~source:loc
"Expected a logical variable as seconde parameter :@. @[%a@] @."
(Printer.pp_term) t
end
| _ -> Rpp_options.Self.fatal ~source:loc
"Expected an integer for first parameter:@. @[%a@] @."
(Printer.pp_term) t
end
| Tapp({l_var_info={lv_name ="\\call"}},[],terms) ->
begin
match terms with
|{term_node =TConst(LStr(s))} :: k ->
begin
match Hashtbl.find id_hash s with
| exception Not_found ->
begin
match k with
| {term_node = TConst (Integer(_,_))} :: q ->
begin
match q with
| {term_node=TLval(TVar({lv_origin=Some(x)}),TNoOffset)} :: p ->
begin
match x with
| {vtype=TFun(_)} ->
check_param_type p x loc;
Hashtbl.add id_hash s x;
Cil.DoChildren
| _ -> Rpp_options.Self.fatal ~source:loc
"Expected a function as thrid parameter:@. @[%a@] @."
(Printer.pp_term) t
end
| _ -> Rpp_options.Self.fatal ~source:loc
"Expected a logical variable as third parameter:@. @[%a@] @."
(Printer.pp_term) t
end
| _ -> Rpp_options.Self.fatal ~source:loc
"Expected an integer for seconde parameter:@. @[%a@] @."
(Printer.pp_term) t
end
| _ -> Rpp_options.Self.fatal ~source:loc
"Multiple use of identifier %s @." s
end
| _ -> Rpp_options.Self.fatal ~source:loc
"Expected an string for first parameter (identifier):@. @[%a@] @."
(Printer.pp_term) t
end
| Tapp({l_var_info={lv_name ="\\callresult"}},[],terms) ->
if (List.length terms) <> 1 then
Rpp_options.Self.fatal ~source:loc
"\\callresult contain more then one parameter:@. @[%a@] @."
(Printer.pp_term) t
else
let term = List.hd terms in
begin
match term.term_node with
| TConst (LStr(s)) ->
let v = (try (Hashtbl.find id_hash s) with
| Not_found -> Rpp_options.Self.fatal ~source:loc
"Unknown identifier %s in \\callresult:@. @[%a@] @."
s (Printer.pp_term) t
| _ -> assert false)
in
if (Cil_datatype.Logic_type.equal (Ctype(fun_type_return v)) (t.term_type)) then ()
else
begin
Rpp_options.Self.fatal ~source:loc
"\\callresult type (@[%a@]) is different from result type of function @[%a@] \
(@[%a@]) with identifier %s @."
Printer.pp_logic_type (t.term_type) Printer.pp_varinfo v
Printer.pp_logic_type (Ctype(fun_type_return v)) s
end
| _ -> Rpp_options.Self.fatal ~source:loc
"\\callresult contain no string : @[%a@] @." Printer.pp_term term
end;
Cil.SkipChildren
| Tapp ({l_var_info={lv_name ="\\callpure"}},_::_, _) ->
Rpp_options.Self.fatal ~source:loc "Expect no label for built-in \\callpure:@. @[%a@]"
Printer.pp_term t
| Tapp ({l_var_info={lv_name ="\\callresult"}}, _::_, _) ->
Rpp_options.Self.fatal ~source:loc "Expect no label for built-in \\callresult:@. @[%a@]"
Printer.pp_term t
| Tapp ({l_var_info={lv_name ="\\call"}}, _::_, _) ->
Rpp_options.Self.fatal ~source:loc "Expect no label for built-in \\callresult:@. @[%a@]"
Printer.pp_term t
| Tat(v,l)->
id_checker l loc id_hash;
self#vterm v
| _ -> super#vterm t
method! vpredicate p =
let (loc,_) = p.pred_loc in
match p.pred_content with
| Papp({l_var_info={lv_name ="\\callset"}},[],terms) ->
Hashtbl.clear id_hash;
List.iter
(fun x ->
match x.term_node with
| Tapp({l_var_info={lv_name ="\\call"}},_,_)->
let _ = self#vterm x in ()
| _ -> Rpp_options.Self.fatal ~source:loc
"\\callset contain no \\call: @. @[%a@] @." Printer.pp_term x
) terms;
Cil.SkipChildren
| Papp (li,labels,params) ->
List.iter (fun l -> id_checker l loc id_hash) labels;
ignore (super#vlogic_info_use li);
List.iter
(fun t ->
ignore
(Visitor.visitFramacTerm (self:>Visitor.frama_c_visitor) t))
params;
Cil.SkipChildren
| _ -> super#vpredicate p
end
end
in
(module New_check: Extensible_checker)
let () = extend_checker rpp_extend_checker