1
(**************************************************************************)
3
(* This file is part of Frama-C. *)
5
(* Copyright (C) 2007-2008 *)
6
(* CEA (Commissariat � l'�nergie Atomique) *)
8
(* you can redistribute it and/or modify it under the terms of the GNU *)
9
(* Lesser General Public License as published by the Free Software *)
10
(* Foundation, version 2.1. *)
12
(* It is distributed in the hope that it will be useful, *)
13
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
14
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
15
(* GNU Lesser General Public License for more details. *)
17
(* See the GNU Lesser General Public License version 2.1 *)
18
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
20
(**************************************************************************)
22
(* $Id: cilE.ml,v 1.65 2008/10/20 15:25:30 uid525 Exp $ *)
24
(** Cil extensions for Frama-C *)
33
let (warn_h:(string*Cil_types.location,unit) Hashtbl.t) = Hashtbl.create 1789
36
let warn_once : ('a,Format.formatter, unit, unit) format4 -> 'a =
38
let v = string_of_format fmt,!Cil.currentLoc in
40
Hashtbl.find warn_h v;
41
Printf.kapr (fun _ _ -> Obj.magic ()) (fst v)
43
Hashtbl.add warn_h v ();
48
if not (Logic_env.LogicInfo.mem p.l_name) then
49
Logic_env.add_builtin_logic_function p
51
let init_builtins () =
53
l_name = "pointer_comparable";
56
l_profile = []; (* TODO: build this one somewhere else*)
58
l_body = LBreads []; (* TODO: give an explicit definition *)
61
l_name = "result_finite_float";
64
l_profile = []; (* TODO: build this one somewhere else*)
66
l_body = LBreads []; (* TODO: give an explicit definition *)
69
let () = Logic_env.Builtins.extend init_builtins
72
let b = Buffer.create 80 in
73
let bfmt = Format.formatter_of_buffer b in
76
Format.pp_print_flush fmt ();
77
let fmt = Buffer.contents b in
78
if not (Hashtbl.mem warn_h (fmt,Cil.CurrentLoc.get ())) then begin
79
Hashtbl.add warn_h (fmt,Cil.CurrentLoc.get ()) ();
84
let (log_h:(string,unit) Hashtbl.t) = Hashtbl.create 1789
87
let b = Buffer.create 80 in
88
let bfmt = Format.formatter_of_buffer b in
91
Format.pp_print_flush fmt ();
92
let fmt = Buffer.contents b in
93
if not (Hashtbl.mem log_h fmt)
95
Hashtbl.add log_h (fmt) ();
102
let lbl_tbl = Hashtbl.create 17 in
103
let goto_changer = object
104
inherit nopCilVisitor
107
| Label (l,_,_) -> Hashtbl.add lbl_tbl l s
113
List.iter (fun x -> ignore (visitCilStmt goto_changer x)) l;
116
let update_gotos sid_tbl block =
117
let goto_changer = object
118
inherit nopCilVisitor
119
method vstmt s = match s.skind with
122
(* Format.printf "Found goto %d@\n" !sref.sid;*)
123
let new_stmt = Cilutil.StmtMap.find !sref sid_tbl in
124
(* Format.printf "Resolved goto %d@\n" !sref.sid;*)
125
ChangeTo (mkStmt (Goto (ref new_stmt,loc)))
126
with Not_found -> DoChildren)
130
visitCilBlock goto_changer block
132
let compact_body fundec =
133
let labels_moved = ref false in
134
let stmt_map = ref Cilutil.StmtMap.empty in
135
let add_labels s l old_stmt =
136
stmt_map := Cilutil.StmtMap.add old_stmt s !stmt_map ;
137
s.labels <- l @ s.labels;
140
let docompact(s1,s2) = match s1.skind, s2.skind with
142
| Instr (Skip _), _ when s1.labels = [] ->
143
if debug then prerr_endline "[compact_body] skip/_";
145
| _, Instr (Skip _) when s2.labels = [] ->
146
if debug then prerr_endline "[compact_body] _/skip";
148
(* collapse useless blocks *)
149
| Block b1, Block b2 when b1.battrs = b2.battrs && (s2.labels = [] || b2.bstmts <> []) ->
150
if debug then prerr_endline "[compact_body] blck/blck";
151
if s2.labels <> [] then begin
152
let fst_b2 = List.hd b2.bstmts in
153
add_labels fst_b2 s2.labels s2
155
b1.bstmts <- b1.bstmts@b2.bstmts;
157
| Block b, _ when b.battrs = [] ->
158
if debug then prerr_endline "[compact_body] blck/instr";
159
b.bstmts <- b.bstmts@[s2];
161
| _, Block b when b.battrs = [] && (s2.labels = [] || b.bstmts <> []) ->
162
if debug then prerr_endline "[compact_body] instr/blck";
163
if s2.labels <> [] then begin
164
let fst_b = List.hd b.bstmts in
165
add_labels fst_b s2.labels s2
167
b.bstmts <- s1::b.bstmts;
171
let block = fundec.sbody in
172
(* Je pense que peepHole2 ne fonctionne pas correctement.
173
* Peut-�tre serait-il mieux de faire notre propre fonction...
174
* en plus, �a permettrait de combiner peepHole1 + peepHole2.
175
* Exemple : peepHole2 ( { { x = 1; skip; } return x; } )
176
* -> { { x = 1; skip; return x; } }
177
* Anne. 12/07/2007. *)
178
block.bstmts <- peepHole2 docompact block.bstmts;
180
if !labels_moved then update_gotos !stmt_map block
182
in let rec get_stmts b = match b.bstmts with
183
| ({skind=Block blk}) :: [] ->
184
if debug then prerr_endline "[compact_body] block(block)";
187
in fundec.sbody.bstmts <- get_stmts block
190
let current_stmt_tbl =
191
let s = Stack.create () in
192
Stack.push Kglobal s;
196
Stack.push ki current_stmt_tbl
200
ignore (Stack.pop current_stmt_tbl)
201
with Stack.Empty -> assert false
203
let current_stmt () =
205
Stack.top current_stmt_tbl
206
with Stack.Empty -> assert false
209
type syntactic_context =
211
| SyBinOp of Cil_types.binop * Cil_types.exp * Cil_types.exp
212
| SyUnOp of Cil_types.exp
213
| SyMem of Cil_types.lval
214
| SySep of Cil_types.exp * Cil_types.exp
216
let syntactic_context = ref SyNone
217
let set_syntactic_context e =
222
"New binary context: %a %a\n"
228
"New unary context: %a\n"
233
"New mem context: %a\n"
237
"New null context\n"));*)
238
syntactic_context := e
240
let get_syntactic_context () = current_stmt (),!syntactic_context
242
let value_analysis_alarm_status () =
243
{status = Checked{emitter="value analysis"; valid = Maybe}}
245
type alarm_behavior = Aignore | Alog | Acall of (unit -> unit)
246
type warn_mode = {unspecified:alarm_behavior; others: alarm_behavior;
247
imprecision_tracing:alarm_behavior}
250
{unspecified=Alog; others=Alog; imprecision_tracing=Alog}
252
{unspecified=Aignore; others=Aignore; imprecision_tracing=Aignore}
255
let warn_div warn_mode =
256
match warn_mode.others with
261
match get_syntactic_context () with
263
| _,(SyUnOp _ | SyMem _ | SySep _) -> assert false
264
| ki,SyBinOp ((Div|Mod),_,exp_d) ->
265
let lexpr = Logic_const.expr_to_term exp_d in
267
Logic_const.new_code_annotation
269
Logic_const.unamed (Prel (Rneq,lexpr, lzero())),
270
value_analysis_alarm_status ()))
272
if Alarms.register ki Alarms.Division_alarm annotation then
274
"division by zero: %a" !Ast_printer.d_code_annotation annotation
275
|_,SyBinOp (_,_,_) -> assert false
278
let warn_shift warn_mode size =
279
match warn_mode.others with
284
match get_syntactic_context () with
286
| _,(SyUnOp _ | SyMem _ | SySep _)-> assert false
287
| ki,SyBinOp ((Shiftrt | Shiftlt),_,exp_d) ->
288
let lexpr = Logic_const.expr_to_term exp_d in
290
Logic_const.new_code_annotation
294
(Logic_const.unamed (Prel (Rge,lexpr, lzero())),
296
(Prel (Rlt,lexpr, lconstant (Int64.of_int size)))),
297
value_analysis_alarm_status ()))
299
if Alarms.register ki Alarms.Shift_alarm annotation then
300
Cil.warn "invalid shift: %a" !Ast_printer.d_code_annotation annotation;
302
| _,SyBinOp(_,_,_) ->
306
let warn_mem warn_mode msg =
307
match warn_mode.others with
313
match get_syntactic_context () with
315
| _,(SyBinOp _ | SyUnOp _ | SySep _) -> assert false
317
let term = mkAddrOrStartOf lv_d in
318
let lexpr = Logic_const.expr_to_tsets_elem term in
320
Logic_const.new_code_annotation
322
Logic_const.unamed (Pvalid (TSSingleton lexpr)),
323
value_analysis_alarm_status ()))
325
if Alarms.register ki Alarms.Memory_alarm annotation then
327
"out of bounds %s. @[%a@]" msg !Ast_printer.d_code_annotation annotation;
329
| Mem _,_ | _, (Index _ | Field _) -> ()
333
let warn_index warn_mode msg =
334
match warn_mode.others with
339
match get_syntactic_context () with
341
| _,(SyMem _ | SyUnOp _ | SySep _) -> assert false
342
| ki ,SyBinOp (IndexPI,e1,e2) ->
343
let lexpr = Logic_const.expr_to_term e1 in
344
let rexpr = Logic_const.expr_to_term e2 in
345
let p0 = Logic_const.prel(Rle, lzero(), lexpr) in
346
let p1 = Logic_const.prel(Rlt, lexpr, rexpr) in
347
let p = Logic_const.pand (p0,p1) in
349
Logic_const.new_code_annotation (AAssert ([],p,value_analysis_alarm_status ()))
351
if Alarms.register ki Alarms.Memory_alarm annotation then
353
"%s out of bounds index. @[%a@]"
354
msg !Ast_printer.d_code_annotation annotation
355
| _,SyBinOp(_,_,_) ->
359
let warn_mem_read warn_mode = warn_mem warn_mode "read"
360
let warn_mem_write warn_mode = warn_mem warn_mode "write"
362
let comparable_pointers t1 t2 =
363
let pi = Logic_env.find_logic_function "pointer_comparable" in
364
Papp (pi, [], [t1;t2])
366
let warn_pointer_comparison warn_mode =
367
match warn_mode.others with
372
match get_syntactic_context () with
374
| _,(SyUnOp _ | SyMem _ | SySep _) -> assert false
375
| ki,SyBinOp ((Eq|Ne|Ge|Le|Gt|Lt),exp_l,exp_r) ->
376
let lexpr_l = Logic_const.expr_to_term exp_l in
377
let lexpr_r = Logic_const.expr_to_term exp_r in
379
Logic_const.new_code_annotation
381
Logic_const.unamed (comparable_pointers lexpr_l lexpr_r),
382
value_analysis_alarm_status ())) in
383
if Alarms.register ki Alarms.Pointer_compare_alarm annotation then
384
warn "pointer comparison: %a" !Ast_printer.d_code_annotation annotation
385
| _,SyBinOp(_,_,_) ->
389
let result_nan_infinite _op t1 t2 =
390
let pi = Logic_env.find_logic_function "result_finite_float" in
391
Papp (pi, [], [t1;t2])
393
let warn_result_nan_infinite warn_mode =
394
match warn_mode.others with
399
match get_syntactic_context () with
401
| _,(SyUnOp _ | SyMem _ | SySep _) -> assert false
402
| ki,SyBinOp (_op, exp_l, exp_r) ->
403
let lexpr_l = Logic_const.expr_to_term exp_l in
404
let lexpr_r = Logic_const.expr_to_term exp_r in
405
let op = lexpr_l in (* TODO: use op *)
407
Logic_const.new_code_annotation
410
Logic_const.unamed (result_nan_infinite op lexpr_l lexpr_r),
411
value_analysis_alarm_status ())) in
412
if Alarms.register ki Alarms.Result_is_nan_or_infinite_alarm annotation
414
warn "float operation: %a" !Ast_printer. d_code_annotation annotation
417
let warn_uninitialized warn_mode =
418
match warn_mode.unspecified with
423
match get_syntactic_context () with
425
| _,(SyBinOp _ | SyUnOp _ | SySep _) -> assert false
427
warn_once "(TODO: emit a proper alarm) accessing uninitialized left-value: %a" d_lval lv_d
430
let warn_escapingaddr warn_mode =
431
match warn_mode.unspecified with
436
match get_syntactic_context () with
438
| _,(SyBinOp _ | SyUnOp _ | SySep _) -> assert false
440
warn_once "(TODO: emit a proper alarm) accessing left-value that contains escaping addresses : %a" d_lval lv_d
443
let warn_separated warn_mode =
444
match warn_mode.unspecified with
449
match get_syntactic_context () with
451
| _,(SyBinOp _ | SyUnOp _ | SyMem _ ) -> assert false
452
| ki,SySep(lv1,lv2) ->
453
let llv1 = Logic_const.expr_to_tsets_elem lv1 in
454
let llv2 = Logic_const.expr_to_tsets_elem lv2 in
455
let tlv1 = TSSingleton llv1 in
456
let tlv2 = TSSingleton llv2 in
458
Logic_const.pseparated ~loc:(Instr.loc ki) [tlv1; tlv2]
460
Logic_const.new_code_annotation
461
(AAssert([],alarm,value_analysis_alarm_status ()))
463
if Alarms.register ki Alarms.Separation_alarm annotation then
465
"multiple accesses in unspecified order. \
466
assert \\separated(%a,%a);" d_exp lv1 d_exp lv2
470
compile-command: "LC_ALL=C make -C ../.."
added
removed
src/kernel/cilE.ml
