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: widen.ml,v 1.39 2008/10/03 13:09:17 uid568 Exp $ *)
33
class widen_visitor kf init_widen_hints (init_enclosing_loop_info:(Cil_types.stmt list * StmtSet.t) option) =
34
object (* visit all sub-expressions from [kf] definition *)
35
inherit Visitor.generic_frama_c_visitor
36
(Project.current ()) (Cil.inplace_visit())
37
val widen_hints = init_widen_hints
38
val enclosing_loop_info = init_enclosing_loop_info
39
method vstmt (s:stmt) =
41
let infer_widen_variables bl enclosing_loop_info =
42
(* Look at the if-goto and if-break statements.
43
The variables of the condition are added to the
44
widening variable set for this loop.
45
These variables may control the loop. That may be not the case ! *)
46
(* Format.printf "Look at widening variables.\n" ; *)
47
let visitor = new widen_visitor kf widen_hints enclosing_loop_info
49
ignore (visitFramacBlock visitor bl);
52
begin match s.skind with
53
| Loop (_, bl,_,_,_) ->
54
let annot = Annotations.get s in
56
Ast_info.lift_annot_list_func
57
Logic_const.extract_loop_pragma annot
59
let widening_stmts = match bl.bstmts with
63
(* Look at the loop pragmas *)
64
let is_pragma_widen_variables = ref false
67
| Widen_variables l ->
70
| { term_node= TLval (TVar {lv_origin = Some vi}, _)} ->
71
let vid = Base.create_varinfo vi in
72
(* Format.printf "Reading user pragma for widening variable: %a.\n"
73
Base.pretty (Base.Var vi); *)
76
in begin match List.fold_left f ([], []) l with
78
(* the annotation is empty or else, there are only variables *)
79
let var_hints = List.fold_right BaseSet.add lv BaseSet.empty
84
Widen_type.add_var_hints widening_stmt var_hints !widen_hints)
86
is_pragma_widen_variables := true
91
"could not interpret loop pragma relative to widening variables")
94
let f (lv, lnum, lt) t =
97
TLval (TVar { lv_origin = Some vi}, _)} ->
98
let vid = Base.create_varinfo vi in
100
| { term_node= TConst (CInt64(v,_,_))} ->
101
let v = Ival.Widen_Hints.V.of_int64 v
103
| _ -> (lv, lnum, t::lt)
104
in begin match List.fold_left f ([], [], []) l with
106
(* the annotation is emty or else, there are only variables *)
108
List.fold_right Ival.Widen_Hints.add lnum Ival.Widen_Hints.empty
113
(fun widening_stmt -> widen_hints :=
114
Widen_type.add_num_hints (Some(widening_stmt))
115
(Widen_type.VarKey(key)) hints !widen_hints)
119
ignore (CilE.warn_once "could not interpret loop pragma relative to widening hint")
122
in List.iter f l_pragma ;
123
if not !is_pragma_widen_variables then
125
try Loop.get_loop_stmts kf s
126
with Loop.No_such_while -> assert false
128
(* There is no Widen_variables pragma for this loop. *)
129
infer_widen_variables bl (Some (widening_stmts, loop))
132
| If (exp, bl_then, bl_else, _) ->
134
match enclosing_loop_info with
136
| Some (widening_stmts, loop_stmts) ->
140
| {bstmts = []} -> ()
142
({skind = Break _; succs = [stmt]}|
143
{skind = Goto ({contents=stmt},_)})::_}
144
when not (StmtSet.mem stmt loop_stmts) ->
145
let varinfos = extract_varinfos_from_exp exp
149
(*Format.printf "Inferring pragma for widening variable: %a.\n" Base.pretty (Base.Var vi);*)
151
(Base.create_varinfo vi) lv)
156
(fun widening_stmt ->
158
Widen_type.add_var_hints
170
method vexpr (e:exp) = begin
171
let with_succ v = [v ; Ival.Widen_Hints.V.succ v]
172
and with_pred v = [Ival.Widen_Hints.V.pred v ; v ]
173
and with_s_p_ v = [(Ival.Widen_Hints.V.pred v) ; v ; (Ival.Widen_Hints.V.succ v)]
174
and default_visit e =
175
match Cil.isInteger e with
177
let v = Ival.Widen_Hints.V.of_int64 int64
178
in widen_hints := Db.Widen_Hints.add_to_all v !widen_hints ;
182
and comparison_visit add1 add2 e1 e2 =
188
Ival.Widen_Hints.empty
190
(*Format.printf "Adding widen hint %a for base %a@\n" Ival.Widen_Hints.pretty hints
192
widen_hints := Widen_type.add_num_hints None (Widen_type.VarKey key) hints !widen_hints
195
let e1,e2 = constFold true e1, constFold true e2 in
196
match (Cil.isInteger e1, Cil.isInteger e2, e1, e2) with
197
| Some int64, _, _, Lval (Var varinfo, _) ->
199
(Base.create_varinfo varinfo)
200
(add1 (Ival.Widen_Hints.V.of_int64 int64));
202
| _, Some int64, Lval (Var varinfo, _), _ ->
204
(Base.create_varinfo varinfo)
205
(add2 (Ival.Widen_Hints.V.of_int64 int64));
211
| BinOp (Lt, e1, e2, _)
212
| BinOp (Gt, e2, e1, _)
213
| BinOp (Le, e2, e1, _)
214
| BinOp (Ge, e1, e2, _) ->
215
comparison_visit with_succ with_pred e1 e2
216
| BinOp (Eq, e1, e2, _)
217
| BinOp (Ne, e1, e2, _) ->
218
comparison_visit with_s_p_ with_s_p_ e1 e2
219
| _ -> default_visit e
223
let compute_widen_hints kf _s default_widen_hints = (* [s] isn't used yet *)
227
| Declaration _ -> default_widen_hints
228
| Definition (fd,_) ->
230
let widen_hints = ref default_widen_hints
231
in let visitor = new widen_visitor kf widen_hints None
232
in ignore (visitFramacFunction visitor fd) ;
239
Kernel_function.Make_Table
240
(Widen_type.Datatype)
242
let name = "Widen.Hints"
244
let dependencies = [ Cil_state.self ]
247
let getWidenHints (kf:kernel_function) (s:stmt) =
248
let widen_hints_map =
249
Hints.memo (fun kf -> compute_widen_hints kf s Widen_type.default) kf
251
Widen_type.hints_from_keys s widen_hints_map
255
compile-command: "make -C ../.."
added
removed
src/memory_state/widen.ml
