← Back to branch summary

~ubuntu-branches/debian/sid/frama-c/sid

« back to all changes in this revision

Viewing changes to src/ai/abstract_interp.mli

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2009-06-03 08:19:25 UTC
  • Revision ID: james.westby@ubuntu.com-20090603081925-kihvxvt0wy3zc4ar
Tags: upstream-20081201.dfsg
Import upstream version 20081201.dfsg

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/ai/abstract_interp.mli
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  This file is part of Frama-C.                                         *)
 
4
(*                                                                        *)
 
5
(*  Copyright (C) 2007-2008                                               *)
 
6
(*    CEA (Commissariat � l'�nergie Atomique)                             *)
 
7
(*                                                                        *)
 
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.                                              *)
 
11
(*                                                                        *)
 
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.                   *)
 
16
(*                                                                        *)
 
17
(*  See the GNU Lesser General Public License version 2.1                 *)
 
18
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
 
19
(*                                                                        *)
 
20
(**************************************************************************)
 
21
 
 
22
(** @plugin development guide *)
 
23
 
 
24
(** Raised by [cardinal_less_than] *)
 
25
exception Not_less_than
 
26
 
 
27
exception Is_not_included
 
28
 
 
29
(** Generic lattice.
 
30
    @plugin development guide *)
 
31
module type Lattice = sig
 
32
 
 
33
  exception Error_Top
 
34
  exception Error_Bottom
 
35
  type t (** type of element of the lattice *)
 
36
  type widen_hint (** hints for the widening *)
 
37
 
 
38
(*  val compare : t -> t -> int
 
39
    (** Does not need to be compatible with [is_included].
 
40
        Must be a total ordering function *)
 
41
*)
 
42
  val equal: t -> t -> bool
 
43
  val join: t -> t -> t (** over-approximation of union *)
 
44
  val link: t -> t -> t (** under-approximation of union *)
 
45
  val meet: t -> t -> t (** under-approximation of intersection *)
 
46
  val narrow: t -> t -> t (** over-approximation of intersection *)
 
47
  val bottom: t (** the smallest *)
 
48
  val top: t  (** the largest *)
 
49
 
 
50
  val is_included: t -> t -> bool
 
51
  val is_included_exn: t -> t -> unit
 
52
  val intersects: t -> t -> bool
 
53
  val pretty: Format.formatter -> t -> unit
 
54
 
 
55
  val widen: widen_hint -> t -> t -> t
 
56
    (** [widen h t1 t2] is an over-approximation of [join t1 t2].
 
57
        Assumes [is_included t1 t2] *)
 
58
 
 
59
  val cardinal_zero_or_one: t -> bool
 
60
 
 
61
  val cardinal_less_than: t -> int -> int
 
62
    (** [cardinal_less_than t v ]
 
63
        @raise Not_less_than whenever the cardinal of [t] is higher than [v] *)
 
64
 
 
65
  val tag : t -> int
 
66
 
 
67
  module Datatype: Project.Datatype.S with type t = t
 
68
 
 
69
end
 
70
 
 
71
module type Lattice_With_Diff = sig
 
72
  include Lattice
 
73
 
 
74
  val diff : t -> t -> t
 
75
    (** [diff t1 t2] is an over-approximation of [t1-t2]. *)
 
76
 
 
77
  val diff_if_one : t -> t -> t
 
78
    (** [diff t1 t2] is an over-approximation of [t1-t2].
 
79
        @return t1 if [t2] is not a singleton. *)
 
80
 
 
81
  val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a
 
82
  val hash : t -> int
 
83
  val pretty_debug : Format.formatter -> t -> unit
 
84
  val name : string
 
85
end
 
86
 
 
87
module type Lattice_Product = sig
 
88
  type t1
 
89
  type t2
 
90
  type tt = private Product of t1*t2 | Bottom
 
91
  include Lattice with type t = tt
 
92
  val inject : t1 -> t2 -> t
 
93
  val fst : t -> t1
 
94
  val snd : t -> t2
 
95
end
 
96
 
 
97
module type Lattice_Sum = sig
 
98
  type t1
 
99
  type t2
 
100
  type sum = private Top | Bottom | T1 of t1 | T2 of t2
 
101
  include Lattice with type t = sum
 
102
  val inject_t1 : t1 -> t
 
103
  val inject_t2 : t2 -> t
 
104
end
 
105
 
 
106
module type Lattice_Base = sig
 
107
  type l
 
108
  type tt = private Top | Bottom | Value of l
 
109
  include Lattice with type t = tt
 
110
  val project : t -> l
 
111
  val inject: l -> t
 
112
end
 
113
 
 
114
module type Lattice_Set = sig
 
115
  module O: Ptset.S
 
116
  type tt = private Set of O.t | Top
 
117
  include Lattice with type t = tt and type widen_hint = O.t
 
118
  val hash : t -> int
 
119
  val inject_singleton: O.elt -> t
 
120
  val inject: O.t -> t
 
121
  val empty: t
 
122
  val apply2: (O.elt -> O.elt -> O.elt) -> (t -> t -> t)
 
123
  val apply1: (O.elt -> O.elt) -> (t -> t)
 
124
  val fold: ( O.elt -> 'a -> 'a) -> t -> 'a -> 'a
 
125
  val iter: ( O.elt -> unit) -> t -> unit
 
126
  val project : t -> O.t
 
127
  val mem : O.elt -> t -> bool
 
128
end
 
129
 
 
130
module type Value = sig
 
131
  type t
 
132
  val pretty: Format.formatter -> t -> unit
 
133
  val compare : t -> t -> int
 
134
  val hash: t -> int
 
135
  module Datatype: Project.Datatype.S with type t = t
 
136
end
 
137
 
 
138
module type Arithmetic_Value = sig
 
139
  include Value
 
140
  val gt : t -> t -> bool
 
141
  val le : t -> t -> bool
 
142
  val ge : t -> t -> bool
 
143
  val lt : t -> t -> bool
 
144
  val eq : t -> t -> bool
 
145
  val add : t -> t -> t
 
146
  val sub : t -> t -> t
 
147
  val mul : t -> t -> t
 
148
  val native_div : t -> t -> t
 
149
  val rem : t -> t -> t
 
150
  val pos_div : t -> t -> t
 
151
  val c_div : t -> t -> t
 
152
  val c_rem : t -> t -> t
 
153
  val cast: size:t -> signed:bool -> value:t -> t
 
154
  val abs : t -> t
 
155
  val zero : t
 
156
  val one : t
 
157
  val two : t
 
158
  val four : t
 
159
  val minus_one : t
 
160
  val is_zero : t -> bool
 
161
  val is_one : t -> bool
 
162
  val equal : t -> t -> bool
 
163
  val pgcd : t -> t -> t
 
164
  val ppcm : t -> t -> t
 
165
  val min : t -> t -> t
 
166
  val max : t -> t -> t
 
167
  val length : t -> t -> t (** b - a + 1 *)
 
168
  val of_int : int -> t
 
169
  val of_float : float -> t
 
170
  val of_int64 : Int64.t -> t
 
171
  val to_int : t -> int
 
172
  val to_float : t -> float
 
173
  val neg : t -> t
 
174
  val succ : t -> t
 
175
  val pred : t -> t
 
176
  val round_up_to_r : min:t -> r:t -> modu:t -> t
 
177
  val round_down_to_r : max:t -> r:t -> modu:t -> t
 
178
  val pos_rem : t -> t -> t
 
179
  val shift_left : t -> t -> t
 
180
  val shift_right : t -> t -> t
 
181
  val fold : (t -> 'a -> 'a) -> inf:t -> sup:t -> step:t -> 'a -> 'a
 
182
  val logand : t -> t -> t
 
183
  val logor : t -> t -> t
 
184
  val logxor : t -> t -> t
 
185
  val lognot : t -> t
 
186
  val power_two : int -> t
 
187
  val two_power : t -> t
 
188
  val extract_bits : with_alarms:CilE.warn_mode -> start:t -> stop:t -> t -> t
 
189
end
 
190
 
 
191
module type Card = sig
 
192
  type t
 
193
  val n : t
 
194
end
 
195
 
 
196
 
 
197
module type Float_Abstract_Sig =
 
198
sig
 
199
  type t
 
200
  type integer
 
201
  exception Nan_or_infinite
 
202
  exception Bottom
 
203
  val compare : t -> t -> int
 
204
  val pretty : Format.formatter -> t -> unit
 
205
  val hash : t -> int
 
206
  val widen : t -> t -> t
 
207
  val is_singleton : t -> bool
 
208
  val is_zero : t -> bool
 
209
  val contains_zero : t -> bool
 
210
  val zero : t
 
211
  val meet : t -> t -> t
 
212
  val join : t -> t -> t
 
213
  val top : t
 
214
  val is_included : t -> t -> bool
 
215
  val diff : t -> t -> t
 
216
  val filter_le : t -> t -> t
 
217
  val filter_ge : t -> t -> t
 
218
  val filter_lt : t -> t -> t
 
219
  val filter_gt : t -> t -> t
 
220
end
 
221
 
 
222
 
 
223
module Int : sig
 
224
  include Arithmetic_Value with type t = My_bigint.big_int
 
225
  val pretty_s : unit -> t -> string
 
226
  val neq : t -> t -> bool
 
227
  val to_int64 : t -> int64
 
228
  val zero : t
 
229
  val eight : t
 
230
  val div : t -> t -> t
 
231
 
 
232
  val billion_one : t
 
233
  val hash : t -> int
 
234
  val tag : t -> int
 
235
  val equal : t -> t -> bool
 
236
  val log_shift_right : t -> t -> t
 
237
  val shift_right : t -> t -> t
 
238
  val shift_left : t -> t -> t
 
239
 
 
240
  val to_int : t -> int
 
241
  val of_int : int -> t
 
242
  val of_int64 : int64 -> t
 
243
  val of_string : string -> t
 
244
  val to_string : t -> string
 
245
  val to_float : t -> float
 
246
  val of_float : 'a -> 'b
 
247
  val minus_one : t
 
248
  val pretty : Format.formatter -> t -> unit
 
249
  val pretty_debug : Format.formatter -> t -> unit
 
250
  val is_zero : t -> bool
 
251
  val compare : t -> t -> int
 
252
  val is_one : t -> bool
 
253
  val pos_div : t -> t -> t
 
254
  val pos_rem : t -> t -> t
 
255
  val native_div :
 
256
    t -> t -> t
 
257
  val c_div : t -> t -> t
 
258
  val c_rem : t -> t -> t
 
259
  val power_two : int -> t
 
260
  val extract_bits :
 
261
    with_alarms:CilE.warn_mode ->
 
262
    start:t ->
 
263
    stop:t -> t -> t
 
264
  val is_even : t -> bool
 
265
  val pgcd : t -> t -> t
 
266
  val ppcm : t -> t -> t
 
267
  val length : t -> t -> t
 
268
  val min : t -> t -> t
 
269
  val max : t -> t -> t
 
270
  val round_down_to_zero :
 
271
    t -> t -> t
 
272
  val round_up_to_r :
 
273
    min:t ->
 
274
    r:t -> modu:t -> t
 
275
  val round_down_to_r :
 
276
    max:t ->
 
277
    r:t -> modu:t -> t
 
278
  val fold :
 
279
    (t -> 'a -> 'a) ->
 
280
    inf:t ->
 
281
    sup:t -> step:t -> 'a -> 'a
 
282
 
 
283
end
 
284
 
 
285
module Make_Lattice_Base (V : Value) : Lattice_Base with type l = V.t
 
286
 
 
287
module Make_Lattice_Mod
 
288
  (V:Arithmetic_Value)
 
289
  (CARD:Card with type t = int)
 
290
  (F:Float_Abstract_Sig with type integer = V.t):
 
291
sig
 
292
  module O : Set.S with type elt = V.t
 
293
 
 
294
  type tt = 
 
295
      Set of O.t
 
296
    | Float of F.t 
 
297
    | Top of V.t option * V.t option * V.t * V.t
 
298
 
 
299
  module Widen_Hints : sig 
 
300
    module V : Arithmetic_Value with type t = V.t
 
301
    include SetWithNearest.S with type elt = V.t
 
302
    val default_widen_hints : t
 
303
  end
 
304
 
 
305
  include Lattice with type t = tt and type widen_hint = Widen_Hints.t
 
306
 
 
307
  val hash : t -> int
 
308
  val equal : t -> t -> bool
 
309
  val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a
 
310
  val diff : t -> t -> t
 
311
  val diff_if_one : t -> t -> t
 
312
  val add : t -> t -> t
 
313
  val neg : t -> t
 
314
  val sub : t -> t -> t
 
315
  val min_int : t -> V.t option
 
316
  val max_int : t -> V.t option
 
317
  val min_and_max : t -> V.t option * V.t option
 
318
  val bitwise_and : size:int -> t -> t -> t
 
319
  val bitwise_or : size:int -> t -> t -> t
 
320
    
 
321
  val inject_range : V.t option -> V.t option -> t
 
322
    (** the interval is inclusive. *)
 
323
 
 
324
  val all_positives : V.t option -> bool
 
325
  val all_negatives : V.t option -> bool
 
326
  val cardinal_zero_or_one : t -> bool
 
327
  val is_singleton_int : t -> bool
 
328
  val inject_singleton : V.t -> t
 
329
  val zero : t
 
330
  val one : t
 
331
  val is_zero : t -> bool
 
332
  val is_one : t -> bool
 
333
 
 
334
  val inject_float : F.t -> t
 
335
  val top_float : t
 
336
 
 
337
  val project_float : t -> F.t 
 
338
    (** @raise F.Nan_or_infinite when the float is Nan or infinite. *)
 
339
 
 
340
  val in_interval :
 
341
    V.t -> V.t option -> V.t option -> V.t -> V.t -> bool
 
342
  val contains_zero : t -> bool
 
343
 
 
344
  exception Not_Singleton_Int
 
345
  val project_int : t -> V.t
 
346
    (** @raise Not_Singleton_Int when the cardinal is not 1. *)
 
347
 
 
348
 
 
349
  val cardinal_less_than : t -> int -> int
 
350
  val inject_top : V.t option -> V.t option -> V.t -> V.t -> t
 
351
  val inject_set : O.t -> t
 
352
  val fold : (V.t -> 'a -> 'a) -> t -> 'a -> 'a
 
353
 
 
354
 
 
355
  exception Apply_Set_Exn of exn
 
356
  val apply_set :
 
357
    string -> (V.t -> V.t -> V.t) -> t -> t -> t
 
358
  val apply_set_unary : 'a -> (V.t -> V.t) -> t -> t
 
359
 
 
360
  val singleton_zero : t
 
361
  val singleton_one : t
 
362
  val zero_or_one : t
 
363
  val contains_non_zero : t -> bool
 
364
 
 
365
  val scale : V.t -> t -> t
 
366
  val scale_div : pos:bool -> V.t -> t -> t
 
367
 
 
368
  val negative : t
 
369
  val div : t -> t -> t
 
370
 
 
371
  val scale_rem : pos:bool -> V.t -> t -> t
 
372
 
 
373
  val cast : size:V.t -> signed:bool -> value:t -> t
 
374
 
 
375
(*  val cast_int_to_float : t -> t
 
376
  val cast_float_to_int : t -> t
 
377
*)                     
 
378
  val c_rem : t -> t -> t
 
379
  val mul : t -> t -> t
 
380
  val shift_left : size:V.t -> t -> t -> t
 
381
  val shift_right : size:V.t -> t -> t -> t
 
382
  val interp_boolean :
 
383
    contains_zero:bool -> contains_non_zero:bool -> t
 
384
  val filter_set : (int -> bool) -> V.t -> O.t -> t
 
385
  val extract_bits : with_alarms:CilE.warn_mode -> start:V.t -> stop:V.t -> t -> t
 
386
  val create_all_values : modu:V.t -> size:int -> t
 
387
  val all_values : size:V.t -> t -> bool
 
388
 
 
389
  (*TODO To be hidden *)
 
390
  val filter_le_int : V.t option -> t -> t
 
391
  val filter_ge_int : V.t option -> t -> t
 
392
  val filter_lt_int : V.t option -> t -> t
 
393
  val filter_gt_int : V.t option -> t -> t
 
394
  val filter_le : t -> t -> t
 
395
  val filter_ge : t -> t -> t
 
396
  val filter_lt : t -> t -> t
 
397
  val filter_gt : t -> t -> t
 
398
 
 
399
  val filter_le_float : t -> t -> t
 
400
  val filter_ge_float : t -> t -> t
 
401
  val filter_lt_float : t -> t -> t
 
402
  val filter_gt_float : t -> t -> t
 
403
 
 
404
  val compare_C :
 
405
    (V.t option ->
 
406
       V.t option -> V.t option -> V.t option -> 'a) -> t -> t -> 'a
 
407
  val max_max :  V.t option -> V.t option -> V.t option
 
408
end
 
409
 
 
410
module Make_Pair (V:Value)(W:Value) :
 
411
  sig
 
412
    type t = V.t * W.t
 
413
    val compare : t -> t -> int
 
414
    val pretty : Format.formatter -> t -> unit
 
415
  end
 
416
 
 
417
module Make_Lattice_Interval_Set (V:Arithmetic_Value) : 
 
418
sig 
 
419
  type elt = Make_Pair(V)(V).t
 
420
  type tt = private Top | Set of elt list
 
421
  include Lattice with type t = tt
 
422
  val hash : t -> int
 
423
  val inject_one : size:V.t -> value:V.t -> t
 
424
  val inject_bounds : V.t -> V.t -> t
 
425
  val inject : elt list -> t
 
426
  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
 
427
end
 
428
 
 
429
module Make_Lattice_Set (V : Value) : Lattice_Set with type O.elt=V.t
 
430
 
 
431
module type Value_With_Id = sig
 
432
  include Value
 
433
  val id: t -> int
 
434
  val name : string
 
435
end
 
436
 
 
437
module Make_Hashconsed_Lattice_Set (V : Value_With_Id) 
 
438
  : Lattice_Set with type O.elt=V.t
 
439
 
 
440
module LocationSetLattice : 
 
441
sig include Lattice_Set with type O.elt = Cil_types.location
 
442
    val currentloc_singleton : unit -> t
 
443
end
 
444
 
 
445
module type Key =
 
446
sig
 
447
  type t
 
448
  val compare : t -> t -> int
 
449
  val pretty : Format.formatter -> t -> unit
 
450
  val is_null : t -> bool
 
451
  val null : t
 
452
  val hash : t -> int
 
453
  val id : t -> int
 
454
  val name : string
 
455
  module Datatype : Project.Datatype.S with type t = t
 
456
end
 
457
 
 
458
module VarinfoSetLattice : Lattice_Set with type O.elt = Cil_types.varinfo
 
459
 
 
460
module type Collapse = sig
 
461
  val collapse : bool
 
462
end
 
463
  
 
464
(** If [C.collapse] then [L1.bottom,_] = [_,L2.bottom] = [bottom] *)
 
465
module Make_Lattice_Product (L1:Lattice) (L2:Lattice) (C:Collapse):
 
466
  Lattice_Product with type t1 = L1.t and type t2 = L2.t