← Back to branch summary

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

« back to all changes in this revision

Viewing changes to .pc/0004-Fix-some-typos.patch/src/ai/base.ml

  • Committer: Bazaar Package Importer
  • Author(s): Mehdi Dogguy
  • Date: 2010-07-16 13:53:55 UTC
  • Revision ID: james.westby@ubuntu.com-20100716135355-vmv6l7ymdan0cypw
Tags: 20100401+boron+dfsg-4
* Add 0009-unrollType-in-handle_signed_overflow from upstream.
* Add 0010-More-spelling-fixes.patch
* Convert to 3.0 (quilt) source format.
* Bump standards version to 3.9.0.

Show diffs side-by-side

added added

removed removed

Lines of Context:
.pc/0004-Fix-some-typos.patch/src/ai/base.ml
 
1
(**************************************************************************)
 
2
(*                                                                        *)
 
3
(*  This file is part of Frama-C.                                         *)
 
4
(*                                                                        *)
 
5
(*  Copyright (C) 2007-2010                                               *)
 
6
(*    CEA (Commissariat � l'�nergie atomique et aux �nergies              *)
 
7
(*         alternatives)                                                  *)
 
8
(*                                                                        *)
 
9
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
 
10
(*  Lesser General Public License as published by the Free Software       *)
 
11
(*  Foundation, version 2.1.                                              *)
 
12
(*                                                                        *)
 
13
(*  It is distributed in the hope that it will be useful,                 *)
 
14
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
 
15
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
 
16
(*  GNU Lesser General Public License for more details.                   *)
 
17
(*                                                                        *)
 
18
(*  See the GNU Lesser General Public License version 2.1                 *)
 
19
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
 
20
(*                                                                        *)
 
21
(**************************************************************************)
 
22
 
 
23
open Cil_types
 
24
open Cil
 
25
open Abstract_interp
 
26
open Abstract_value
 
27
 
 
28
type cell_class_attributes =
 
29
    { cname : string ;
 
30
      cid : int ;
 
31
      cneverexact : bool ;
 
32
      ctyp : Cil_types.typ ;
 
33
      cvolatile : bool ;
 
34
    }
 
35
 
 
36
let name = "base"
 
37
 
 
38
type validity =
 
39
  | All
 
40
  | Unknown of Abstract_interp.Int.t*Abstract_interp.Int.t
 
41
  | Known of Abstract_interp.Int.t*Abstract_interp.Int.t
 
42
 
 
43
type t =
 
44
  | Var of varinfo*validity
 
45
  | Initialized_Var of varinfo*validity
 
46
      (** base that is implicitely initialized. *)
 
47
  | Null (** base for adresses like [(int* )0x123] *)
 
48
  | String of int*string (** String constants *)
 
49
  | Cell_class of cell_class_attributes (** a class of memory cells *)
 
50
 
 
51
let invalid = Known(Int.one, Int.zero)
 
52
 
 
53
let id = function
 
54
  | Var (vi,_) | Initialized_Var (vi,_) -> vi.vid
 
55
  | Null -> 0
 
56
  | String (id,_) | Cell_class {cid = id} -> id
 
57
 
 
58
let hash = id
 
59
 
 
60
let null = Null
 
61
 
 
62
let is_null x = match x with Null -> true | _ -> false
 
63
 
 
64
let is_hidden_variable v =
 
65
  match v with
 
66
    Var (s,_) when s.vlogic -> true
 
67
  | _ -> false
 
68
 
 
69
let pretty_validity fmt v =
 
70
  match v with
 
71
  | All -> Format.fprintf fmt "All"
 
72
  | Unknown (b,e)  -> Format.fprintf fmt "Unknown %a-%a" Int.pretty b Int.pretty e
 
73
  | Known (b,e)  -> Format.fprintf fmt "Known %a-%a" Int.pretty b Int.pretty e
 
74
 
 
75
let pretty fmt t = Format.fprintf fmt "%s"
 
76
  (match t with
 
77
   | String (_,s) -> Format.sprintf "%S" s
 
78
   | Cell_class c -> Format.sprintf "%S" c.cname
 
79
   | Var (t,_) | Initialized_Var (t,_) ->
 
80
       Pretty_utils.sfprintf "@[%a@]" !Ast_printer.d_ident t.vname
 
81
   | Null -> "NULL")
 
82
 
 
83
(*
 
84
let pretty_caml fmt t =
 
85
  match t with
 
86
    String (_,s) -> Format.fprintf fmt "(Base.create_string %S)" s
 
87
  | Var (t,_) | Initialized_Var (t,_) ->
 
88
      Base.
 
89
*)
 
90
 
 
91
let compare v1 v2 = Pervasives.compare (id v1) (id v2)
 
92
 
 
93
let typeof v =
 
94
  match v with
 
95
  | String (_,_) -> Some charConstPtrType
 
96
  | Null -> None
 
97
  | Cell_class c ->
 
98
      Some c.ctyp
 
99
  | Var (v,_) | Initialized_Var (v,_) -> Some (unrollType v.vtype)
 
100
 
 
101
let bits_sizeof v =
 
102
  match v with
 
103
    | String (_,s) ->
 
104
        Int_Base.inject
 
105
          (Int.mul (Int.of_int 8) (Int.succ (Int.of_int (String.length s))))
 
106
    | Null -> Int_Base.top
 
107
    | Cell_class c ->
 
108
        Bit_utils.sizeof c.ctyp
 
109
    | Var (v,_) | Initialized_Var (v,_) ->
 
110
        Bit_utils.sizeof_vid v
 
111
 
 
112
(*        match findAttribute "original_type" (typeAttr typ) with
 
113
        | []  -> Bit_utils.sizeof_vid v
 
114
        | [ASizeOf (TArray (_, Some _,_) as pointed_typ)] ->
 
115
            bitsSizeOf pointed_typ
 
116
*)
 
117
 
 
118
(** All absolute address are invalid *)
 
119
module MinValidAbsoluteAddress =
 
120
  Computation.Ref
 
121
    (struct
 
122
       include Abstract_interp.Int.Datatype
 
123
       let default () = Abstract_interp.Int.zero
 
124
     end)
 
125
    (struct
 
126
       let name = "MinValidAbsoluteAddress"
 
127
       let dependencies = []
 
128
     end)
 
129
 
 
130
module MaxValidAbsoluteAddress =
 
131
  Computation.Ref
 
132
    (struct
 
133
       include Abstract_interp.Int.Datatype
 
134
       let default () = Abstract_interp.Int.minus_one
 
135
     end)
 
136
    (struct
 
137
       let name = "MaxValidAbsoluteAddress"
 
138
       let dependencies = []
 
139
     end)
 
140
 
 
141
let () =
 
142
  Parameters.AbsoluteValidRange.add_set_hook
 
143
    (fun _ x ->
 
144
       try Scanf.sscanf x "%Li-%Li"
 
145
         (fun min max ->
 
146
            let mul8 = Int64.mul 8L in
 
147
            MinValidAbsoluteAddress.set 
 
148
              (Abstract_interp.Int.of_int64 (mul8 min));
 
149
            MaxValidAbsoluteAddress.set 
 
150
              (Abstract_interp.Int.of_int64
 
151
                 (Int64.pred (mul8 (Int64.succ max)))))
 
152
       with End_of_file | Scanf.Scan_failure _ | Failure _ as e ->
 
153
         Kernel.abort "Invalid -absolute-valid-range integer-integer: each integer may be in decimal, hexadecimal (0x, 0X), octal (0o) or binary (0b) notation and has to hold in 64 bits. A correct example is -absolute-valid-range 1-0xFFFFFF0.@\nError was %S@."
 
154
           (Printexc.to_string e))
 
155
 
 
156
let min_valid_absolute_address = MinValidAbsoluteAddress.get
 
157
let max_valid_absolute_address = MaxValidAbsoluteAddress.get
 
158
 
 
159
let validity v =
 
160
  match v with
 
161
  | Null -> Known (min_valid_absolute_address (), max_valid_absolute_address ())
 
162
  | Var (_,v) | Initialized_Var (_,v) -> v
 
163
  | String _ | Cell_class _ ->
 
164
      let max_valid = bits_sizeof v in
 
165
      match max_valid with
 
166
      | Int_Base.Bottom -> assert false
 
167
      | Int_Base.Top -> All
 
168
      | Int_Base.Value size ->
 
169
          (*Format.printf "Got %a for %a@\n" Int.pretty size pretty v;*)
 
170
          Known (Int.zero,Int.pred size)
 
171
            (* they all start to be valid at offset 0 *)
 
172
 
 
173
exception Not_valid_offset
 
174
 
 
175
let is_valid_offset size base offset =
 
176
  match validity base with
 
177
  | Known (min_valid,max_valid) ->
 
178
      let min = Ival.min_int offset in
 
179
      begin match min with
 
180
      | None -> raise Not_valid_offset
 
181
      | Some v -> if Int.lt v min_valid then raise Not_valid_offset
 
182
      end;
 
183
      let max = Ival.max_int offset in
 
184
      begin match max with
 
185
      | None -> raise Not_valid_offset
 
186
      | Some v ->
 
187
          if Int.gt (Int.pred (Int.add v size)) max_valid then
 
188
            raise Not_valid_offset
 
189
      end
 
190
  | Unknown _ -> raise Not_valid_offset
 
191
  | All -> ()
 
192
 
 
193
(*
 
194
  let is_volatile v =
 
195
  match v with
 
196
  | String _ | Null -> false
 
197
  | Cell_class c -> c.cvolatile
 
198
  | Var vv ->
 
199
  hasAttribute "volatile" (typeAttrs vv.vtype)
 
200
*)
 
201
 
 
202
let equal v w = (id v) = (id w)
 
203
 
 
204
let hash = id
 
205
 
 
206
let is_aligned_by b alignment =
 
207
  if Int.is_zero alignment
 
208
  then false
 
209
  else
 
210
    match b with
 
211
      Var (v,_) | Initialized_Var (v,_) ->
 
212
        Int.is_zero (Int.rem (Int.of_int (Cil.alignOf_int(v.vtype))) alignment)
 
213
    | Null -> true
 
214
    | String _ -> Int.is_one alignment
 
215
    | Cell_class _ -> assert false
 
216
 
 
217
let is_any_formal_or_local v =
 
218
  match v with
 
219
  | Var (v,_) | Initialized_Var (v,_) -> not v.vlogic && not v.vglob
 
220
  | Null | String _ | Cell_class _  -> false
 
221
 
 
222
let is_any_local v =
 
223
  match v with
 
224
  | Var (v,_) | Initialized_Var (v,_) ->
 
225
      not v.vlogic && not v.vglob && not v.vformal
 
226
  | Null | String _ | Cell_class _  -> false
 
227
 
 
228
let is_formal_or_local v fundec =
 
229
  match v with
 
230
  | Var (v,_) | Initialized_Var (v,_) ->
 
231
      Ast_info.Function.is_formal_or_local v fundec
 
232
  | Null | String _ | Cell_class _  -> false
 
233
 
 
234
let is_formal_of_prototype v vi =
 
235
  match v with
 
236
  | Var (v,_) | Initialized_Var (v,_) ->
 
237
      Ast_info.Function.is_formal_of_prototype v vi
 
238
  | Null | String _ | Cell_class _   -> false
 
239
 
 
240
let is_local v fundec =
 
241
  match v with
 
242
  | Var (v,_) | Initialized_Var (v,_) -> Ast_info.Function.is_local v fundec
 
243
  | Null | String _ | Cell_class _   -> false
 
244
 
 
245
let is_block_local v block =
 
246
  match v with
 
247
  | Var (v,_) | Initialized_Var (v,_) -> Ast_info.is_block_local v block
 
248
  | Null | String _ | Cell_class _   -> false
 
249
 
 
250
let validity_from_type v =
 
251
  if isFunctionType v.vtype then invalid
 
252
  else
 
253
  let max_valid = Bit_utils.sizeof_vid v in
 
254
  match max_valid with
 
255
  | Int_Base.Bottom -> assert false
 
256
  | Int_Base.Top ->
 
257
      (* TODO:
 
258
         if (some configuration option)
 
259
         then Unknown (Int.zero, Bit_utils.max_bit_address ())
 
260
         else *)
 
261
      invalid
 
262
  | Int_Base.Value size when Int.gt size Int.zero ->
 
263
      (*Format.printf "Got %a for %s@\n" Int.pretty size v.vname;*)
 
264
      Known (Int.zero,Int.pred size)
 
265
  | Int_Base.Value size ->
 
266
      assert (Int.eq size Int.zero);
 
267
      Unknown (Int.zero, Bit_utils.max_bit_address ())
 
268
 
 
269
exception Not_a_variable
 
270
 
 
271
let get_varinfo t =
 
272
  match t with
 
273
  | Var (t,_) | Initialized_Var (t,_) -> t
 
274
  | _ -> raise Not_a_variable
 
275
 
 
276
let create_varinfo varinfo =
 
277
  assert (not varinfo.vlogic);
 
278
  Var (varinfo,validity_from_type varinfo)
 
279
 
 
280
let create_logic varinfo validity =
 
281
  assert varinfo.vlogic;
 
282
  Var (varinfo,validity)
 
283
 
 
284
let create_initialized varinfo validity =
 
285
  assert varinfo.vlogic;
 
286
  Initialized_Var (varinfo,validity)
 
287
 
 
288
type base = t
 
289
 
 
290
module LiteralStrings =
 
291
  Computation.Hashtbl
 
292
    (Datatype.String)
 
293
    ((* The function [copy] is used here but persistent strings are not
 
294
        required. *)
 
295
      Project.Datatype.Imperative
 
296
        (struct
 
297
           type t = base
 
298
           let copy = function
 
299
             | String _ as b -> b
 
300
             | _ -> assert false
 
301
           let name = "LiteralStrings"
 
302
         end))
 
303
    (struct
 
304
       let name = name
 
305
       let dependencies = [Ast.self]
 
306
       let size = 17
 
307
     end)
 
308
 
 
309
let create_string s =
 
310
  LiteralStrings.memo (fun _ -> String (Cil_const.new_raw_id (), s)) s
 
311
 
 
312
module Datatype =
 
313
  Project.Datatype.Imperative
 
314
    (struct
 
315
       type t = base
 
316
       let copy _ = assert false (* TODO if required *)
 
317
       let name = "base"
 
318
     end)
 
319
 
 
320
(*
 
321
Local Variables:
 
322
compile-command: "LC_ALL=C make -C ../.."
 
323
End:
 
324
*)