← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/inout/context.ml

  • 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/inout/context.ml
 
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
open Cil_types
 
23
open Cil
 
24
open Pretty
 
25
open Db
 
26
open Db_types
 
27
open Locations
 
28
open Abstract_interp
 
29
open Abstract_value
 
30
 
 
31
(* Computation of over-approximed operational inputs:
 
32
   An acurate computation of these inputs needs the computation of
 
33
   under-approximed outputs.
 
34
   Computation principle for the treatement of a basic statement:
 
35
   *  I_new+ = I_old+ \/+ (Rd+(stmt) /+ O_old-)
 
36
   *  O_new- = O_old- \/-  Wr-(stmt)
 
37
*)
 
38
 
 
39
type compute_t =
 
40
    { over_inputs : Zone.t ;
 
41
      under_outputs : Zone.t }
 
42
 
 
43
(* Initial value for the computation *)
 
44
let empty =
 
45
  { (* initial value for the computation of over_inputs *)
 
46
    over_inputs = Zone.bottom;
 
47
    under_outputs = Zone.bottom;
 
48
  }
 
49
 
 
50
let non_terminating =
 
51
  {
 
52
    over_inputs = Zone.bottom ;
 
53
    under_outputs = Zone.top
 
54
  }
 
55
 
 
56
(*
 
57
let unknown =
 
58
  { over_inputs = Zone.top ;
 
59
  under_outputs = Zone.bottom }
 
60
*)
 
61
 
 
62
let call_stack : kernel_function Stack.t =
 
63
  Stack.create ()
 
64
    (* Stack of function being processed *)
 
65
 
 
66
let find_deps_no_transitivity = !From.find_deps_no_transitivity
 
67
  (* The value of the expression [expr], just before executing the statement [instr],
 
68
     is a function of the values of the returned zones. *)
 
69
 
 
70
module Computer (REACH:sig
 
71
                   val stmt_can_reach : stmt -> stmt -> bool
 
72
                 end) = struct
 
73
  let name = "InOut context"
 
74
 
 
75
  let debug = ref false
 
76
 
 
77
  let current_stmt = ref Kglobal
 
78
 
 
79
  let stmt_can_reach = REACH.stmt_can_reach
 
80
 
 
81
  let under_inputs_termination_no_depend = ref Zone.bottom
 
82
 
 
83
  type t = compute_t
 
84
 
 
85
  module StmtStartData =
 
86
    Dataflow.StmtStartData(struct type t = compute_t let size = 107 end)
 
87
 
 
88
  let display_one fmt k v =
 
89
    Format.fprintf fmt "Statement: %d@\n"
 
90
      k;
 
91
    InOutContext.pretty fmt v
 
92
 
 
93
  let pretty fmt x =
 
94
    Format.fprintf fmt "@[Over-approximated operational inputs: %a@]@\n@[Under-approximated operational outputs: %a@]"
 
95
      Zone.pretty x.over_inputs
 
96
      Zone.pretty x.under_outputs
 
97
 
 
98
  let display fmt f =
 
99
    Format.fprintf fmt "=========INOUT CONTEXT START=======@\n";
 
100
    Inthash.iter
 
101
      (display_one fmt)
 
102
      f;
 
103
    Format.fprintf fmt "=========INOUT CONTEXT END=======@\n"
 
104
 
 
105
  let copy (d: t) = d
 
106
 
 
107
 
 
108
  let computeFirstPredecessor (s: stmt) data =
 
109
    match s.skind with
 
110
      | Switch (exp,_,_,_)
 
111
      | If (exp,_,_,_) ->
 
112
          (* update [over_inputs] using the [exp] condition:
 
113
             I+ = I+ \/+ (D+(exp) /+ O-)
 
114
          *)
 
115
          let inputs = find_deps_no_transitivity (Kstmt s) exp in
 
116
            {data with
 
117
               over_inputs =
 
118
                Zone.join data.over_inputs
 
119
                  (Zone.diff inputs data.under_outputs)}
 
120
      | _ -> data
 
121
 
 
122
  let combinePredecessors
 
123
      (s: stmt)
 
124
      ~old:{under_outputs = old_outputs;
 
125
            over_inputs = old_inputs}
 
126
      new_ =
 
127
    let {under_outputs = new_outputs;
 
128
         over_inputs = new_inputs} = computeFirstPredecessor s new_
 
129
    in
 
130
    let result_inputs = Zone.join old_inputs new_inputs in
 
131
    (* over-approximation :
 
132
       I+ = I_old+ \/+ (I_new+  \/+ (D+(exp) /+ Onew-)
 
133
    *)
 
134
    let result_outputs = Zone.meet old_outputs new_outputs in
 
135
    (* under-approximation :
 
136
       O- = O_old- /\- O_new-
 
137
    *)
 
138
    (*display Format.std_formatter stmtStartData;*)
 
139
    if Zone.is_included result_inputs old_inputs
 
140
      (* test for an over-approximation *)
 
141
      && Zone.is_included old_outputs result_outputs
 
142
      (* test for an under-approximation *)
 
143
    then
 
144
      ((*Format.printf "STABLE RESULT:[Under-outputs=%a][Over-inputs=%a]@\nOLD:[Under-outputs=%a][Over-inputs=%a]@\n"
 
145
         Zone.pretty result_outputs
 
146
         Zone.pretty result_inputs
 
147
         Zone.pretty old_outputs
 
148
         Zone.pretty old_inputs
 
149
         ;*)
 
150
        None)
 
151
    else
 
152
      ((*Format.printf "LATER  RESULT:[Under-outputs=%a][Over-inputs=%a]@\nOLD:[Under-outputs=%a][Over-inputs=%a]@\n"
 
153
         Zone.pretty result_outputs
 
154
         Zone.pretty result_inputs
 
155
         Zone.pretty old_outputs
 
156
         Zone.pretty old_inputs
 
157
         ;*)
 
158
        Some {under_outputs = result_outputs; over_inputs = result_inputs})
 
159
 
 
160
  let resolv_func_vinfo ?deps kinstr funcexp =
 
161
    !Value.expr_to_kernel_function ?deps kinstr funcexp
 
162
 
 
163
  let doInstr _stmt (i: instr) (_d: t) =
 
164
    let kinstr = !current_stmt
 
165
    in
 
166
    let add_with_additional_var k j st =
 
167
      let deps, looking_for =
 
168
        (* The modified tsets are [looking_for], those address are
 
169
           function of [deps]. *)
 
170
        !Value.lval_to_loc_with_deps
 
171
           ~with_alarms:CilE.warn_none_mode
 
172
          ~deps:j
 
173
          kinstr
 
174
          k
 
175
      in
 
176
      let new_inputs =
 
177
        Zone.join st.over_inputs (Zone.diff deps st.under_outputs) in
 
178
      let new_outputs =
 
179
        if Location_Bits.cardinal_zero_or_one looking_for.loc
 
180
        then
 
181
          (* There is only one modified zone. So, this is an exact output.
 
182
             Add it into the under-approximed outputs. *)
 
183
          Zone.link st.under_outputs (Locations.valid_enumerate_bits looking_for)
 
184
        else (* Impossible to add these outputs into the under-approximed outputs. *)
 
185
          st.under_outputs
 
186
      in
 
187
      (* Format.printf "doInstr:@\n <-new_inputs: %a@\n <-new_outputs: %a@\n ->old_inputs: %a@\n ->old_outputs: %a@\n ->additional_var: %a@\n ->read_loc: %a@\n ->writen_loc: %a@\n ->cardinal_zero_or_one: %s@\n"
 
188
        Zone.pretty new_inputs
 
189
        Zone.pretty new_outputs
 
190
        Zone.pretty st.over_inputs
 
191
        Zone.pretty st.under_outputs
 
192
        Zone.pretty j
 
193
        Zone.pretty deps
 
194
        Location_Bits.pretty looking_for.loc
 
195
        (if Location_Bits.cardinal_zero_or_one looking_for.loc then "true" else "false");
 
196
      *)
 
197
      { over_inputs = new_inputs;
 
198
        under_outputs = new_outputs }
 
199
    in
 
200
    match i with
 
201
    | Set (lv, exp, _) ->
 
202
        Dataflow.Post
 
203
          (fun state ->
 
204
 
 
205
             let exp_inputs_deps =
 
206
               find_deps_no_transitivity kinstr exp
 
207
             in
 
208
            (*  Format.printf "ADD INPUTS (line %d): %a\n"
 
209
                location.Cil_types.line Zone.pretty exp_inputs_deps; *)
 
210
             add_with_additional_var
 
211
               lv
 
212
               exp_inputs_deps
 
213
               state)
 
214
    | Call (lvaloption,funcexp,argl,_) ->
 
215
        Dataflow.Post
 
216
          (fun state ->
 
217
               let funcexp_inputs, called_vinfos =
 
218
                 (* [funcexp_inputs]: inputs for the evaluation of [funcexp],
 
219
                    [called_vinfos]: list of called functions *)
 
220
                 resolv_func_vinfo
 
221
                   ~with_alarms:CilE.warn_none_mode
 
222
                   ~deps:Zone.bottom
 
223
                   kinstr
 
224
                   funcexp
 
225
               in
 
226
               let acc_funcexp_inputs =
 
227
                 (* inputs used by [funcexp] and inputs for the evaluation of [funcexp] *)
 
228
                 Zone.join funcexp_inputs state.over_inputs
 
229
               in
 
230
               let acc_funcexp_arg_inputs =
 
231
                 (* inputs used by [funcexp], inputs for the evaluation of [funcexp] and its [argl] *)
 
232
                 List.fold_right
 
233
                   (fun arg inputs ->
 
234
                      let arg_inputs = find_deps_no_transitivity kinstr arg
 
235
                      in Zone.join inputs arg_inputs)
 
236
                   argl
 
237
                   acc_funcexp_inputs
 
238
               in let result =
 
239
                   match called_vinfos with
 
240
                     | [] -> { over_inputs = acc_funcexp_arg_inputs ;
 
241
                               under_outputs = state.under_outputs }
 
242
                     | h::t ->
 
243
                         let do_on kernel_function =
 
244
                           let { over_inputs_if_termination = called_inputs;
 
245
                                 under_outputs_if_termination = called_outputs ;
 
246
 
 
247
                                 Inout_type.over_inputs = called_input_termination_no_depend} = !Db.InOutContext.get_external kernel_function
 
248
 
 
249
                           in
 
250
                           let _ = under_inputs_termination_no_depend := Zone.join
 
251
                             !under_inputs_termination_no_depend
 
252
                             (Zone.diff called_input_termination_no_depend state.under_outputs);
 
253
                           in { over_inputs = (* the real inputs of the call to those of the curent state *)
 
254
                                 Zone.diff called_inputs state.under_outputs;
 
255
                                under_outputs = called_outputs }
 
256
                         in
 
257
                         let acc = do_on h (* First call *)
 
258
                         in let done_on = List.fold_left (* Combine other calls *)
 
259
                             (fun acc_memory called_vinfo ->
 
260
                                let done_on = do_on called_vinfo
 
261
                                in {over_inputs = Zone.join done_on.over_inputs acc_memory.over_inputs; (* over-approximation *)
 
262
                                    under_outputs = Zone.meet done_on.under_outputs acc_memory.under_outputs (* under-approximation intersec*)
 
263
                                   })
 
264
                             acc
 
265
                             t
 
266
                         in (* state just after the call, but before the result asssigment *)
 
267
                           { over_inputs = Zone.join acc_funcexp_arg_inputs done_on.over_inputs ;
 
268
                             under_outputs = Zone.link state.under_outputs done_on.under_outputs (* under-approximed union *) }
 
269
               in let result =
 
270
                   (* Treatement for the eventual assignement of the call result *)
 
271
                   (match lvaloption with
 
272
                    | None -> result
 
273
                    | Some lv ->
 
274
                        add_with_additional_var
 
275
                          lv
 
276
                          Zone.bottom (* Inputs are already got using [!InOutContext.get_external kernel_function]. *)
 
277
                          result)
 
278
               in result
 
279
)
 
280
    | _ -> Dataflow.Default
 
281
 
 
282
  let doStmt (s: stmt) (_d: t) =
 
283
    current_stmt := Kstmt s;
 
284
    Dataflow.SDefault
 
285
 
 
286
  let filterStmt (s:stmt) =
 
287
    let state = Value.noassert_get_state (Kstmt s) in
 
288
    Value.is_reachable state
 
289
(*
 
290
  let clear_for_function f =
 
291
    StmtStartData.clear ();
 
292
    StmtStartData.iter (StmtStartData.add stmtStartData) f
 
293
*)
 
294
  let doGuard s _e _t =
 
295
    current_stmt := Kstmt s;
 
296
    Dataflow.GDefault
 
297
 
 
298
end
 
299
 
 
300
let get_using_prototype kf =
 
301
  let state = Value.get_initial_state kf in
 
302
  let behaviors = !Value.valid_behaviors kf state in
 
303
  let assigns = Ast_info.merge_assigns behaviors in
 
304
  let over_inputs_if_termination =
 
305
    !Value.assigns_to_zone_inputs_state state assigns
 
306
  in
 
307
  { Inout_type.under_outputs_if_termination =
 
308
      (* car les sorties s�re ne sont pas sp�cifi�es ! *)
 
309
      Zone.bottom ;
 
310
    over_inputs_if_termination =
 
311
      (* [over_inputs_if_termination] = [Zone.top] ou [over_inputs_if_termination] ?
 
312
         La valeur [over_inputs_if_termination] est l�g�rement incorrect car les
 
313
         le d�tail de l'implementation n'est pas pr�cis� dans la sp�cification.
 
314
         La meilleure implementation peut se contenter [over_inputs_if_termination]
 
315
         comme entr�es op�rationelles. *)
 
316
      over_inputs_if_termination;
 
317
    over_inputs =
 
318
      (* [over_inputs] = [Zone.top] ou [over_inputs_if_termination] ?
 
319
         La valeur [over_inputs_if_termination] est l�g�rement incorrect car les
 
320
         fonctions feuilles ne sont pas specifi�es en cas de non terminaison. *)
 
321
      over_inputs_if_termination
 
322
  }
 
323
 
 
324
let compute_internal_using_prototype kf =
 
325
  match kf.fundec with
 
326
    | Definition _ -> assert false
 
327
    | Declaration _ -> get_using_prototype kf
 
328
 
 
329
let compute_internal_using_cfg kf =
 
330
  let compute_for_definition kf f =
 
331
    try
 
332
      let module Computer =
 
333
        Computer(struct let stmt_can_reach = Stmts_graph.stmt_can_reach kf end)
 
334
      in
 
335
      let module Compute = Dataflow.ForwardsDataFlow(Computer)
 
336
      in
 
337
      Stack.iter
 
338
        (fun g -> if kf == g then begin
 
339
           ignore
 
340
             (error
 
341
                "ignoring recursive call detected in function %s during [inout context] computation."
 
342
                (Kernel_function.get_name kf));
 
343
           raise Exit
 
344
         end)
 
345
        call_stack;
 
346
      Stack.push kf call_stack;
 
347
      let res_if_termination = (* result if termination *)
 
348
        match f.sbody.bstmts with
 
349
        [] -> assert false
 
350
      | start :: _ ->
 
351
          let ret_id = Kernel_function.find_return kf in
 
352
          (* Format.printf "Return is %d@\n\n" ret_id; *)
 
353
          (* We start with only the start block *)
 
354
          Computer.StmtStartData.add
 
355
            start.sid
 
356
            (Computer.computeFirstPredecessor
 
357
               start
 
358
               empty);
 
359
          Compute.compute [start];
 
360
          let _poped = Stack.pop call_stack in
 
361
          (*Format.printf "[inout] poped %s\n@\n" (get_name _poped);
 
362
            Stack.iter
 
363
            (fun g -> Format.printf "[inout] stack with %s\n@\n" (get_name g))
 
364
            call_stack;
 
365
          *)
 
366
          try
 
367
            Computer.StmtStartData.find ret_id.sid
 
368
          with Not_found ->
 
369
            non_terminating
 
370
      in
 
371
 
 
372
      { Inout_type.over_inputs_if_termination = res_if_termination.over_inputs ;
 
373
        under_outputs_if_termination = res_if_termination.under_outputs ;
 
374
        over_inputs = let acc = Computer.under_inputs_termination_no_depend
 
375
        in Computer.StmtStartData.iter (fun _sid data -> acc := Zone.join data.over_inputs !acc) ; !acc }
 
376
 
 
377
    with Exit ->
 
378
      { Inout_type.over_inputs_if_termination = empty.over_inputs ;
 
379
        under_outputs_if_termination = empty.under_outputs ;
 
380
        over_inputs = empty.over_inputs
 
381
      }
 
382
  in
 
383
  match kf.fundec with
 
384
  | Declaration _ ->
 
385
      invalid_arg
 
386
        "compute_using_cfg cannot be called on leaf functions"
 
387
  | Definition (f, _) ->
 
388
      compute_for_definition kf f
 
389
 
 
390
 
 
391
module Internals =
 
392
  Kf_state.Context
 
393
    (struct
 
394
       let name = "internal_inouts"
 
395
       let dependencies = [ Value.self ]
 
396
     end)
 
397
 
 
398
let get_internal =
 
399
  Internals.memo
 
400
    (fun kf ->
 
401
       !Value.compute ();
 
402
       Cil.log
 
403
         "[inout context] computing for function %a%s"
 
404
         Kernel_function.pretty_name kf
 
405
         (let s = ref "" in
 
406
          Stack.iter
 
407
            (fun kf -> s := !s^" <-"^
 
408
               (fprintf_to_string "%a" Kernel_function.pretty_name kf))
 
409
            call_stack;
 
410
            !s);
 
411
       let res =
 
412
         match kf.fundec with
 
413
         | Definition _ ->
 
414
             compute_internal_using_cfg kf
 
415
         | Declaration _ ->
 
416
             compute_internal_using_prototype kf
 
417
       in
 
418
       Cil.log "[inout context] done for function %a"
 
419
         Kernel_function.pretty_name kf;
 
420
       res)
 
421
 
 
422
let get_external_using_prototype = get_using_prototype
 
423
 
 
424
let externalize fundec =
 
425
  match fundec with
 
426
  | Definition (fundec,_) ->
 
427
      Zone.filter_base
 
428
        (fun v -> not (Base.is_formal_or_local v fundec))
 
429
  | Declaration (_,vd,_,_) ->
 
430
      Zone.filter_base
 
431
        (fun v -> not (Base.is_formal_of_prototype v vd))
 
432
 
 
433
module Externals =
 
434
  Kf_state.Context
 
435
    (struct
 
436
       let name = "external_inouts"
 
437
       let dependencies = [ Internals.self ]
 
438
     end)
 
439
 
 
440
let get_external =
 
441
  Externals.memo
 
442
    (fun kf ->
 
443
       let internals = get_internal kf in
 
444
       let filter = externalize kf.fundec in
 
445
 
 
446
         { Inout_type.over_inputs_if_termination = filter internals.Inout_type.over_inputs_if_termination;
 
447
           under_outputs_if_termination = filter internals.Inout_type.under_outputs_if_termination;
 
448
           over_inputs = filter internals.Inout_type.over_inputs })
 
449
 
 
450
let compute_external kf = ignore (get_external kf)
 
451
 
 
452
let pretty_internal fmt kf =
 
453
  Format.fprintf fmt "@[InOut (internal) for function %a:@\n%a@]@\n"
 
454
    Kernel_function.pretty_name kf
 
455
    InOutContext.pretty (get_internal kf)
 
456
 
 
457
let pretty_external fmt kf =
 
458
  Format.fprintf fmt "@[InOut for function %a:@\n%a@]@\n"
 
459
    Kernel_function.pretty_name kf
 
460
    InOutContext.pretty (get_external kf)
 
461
 
 
462
let () =
 
463
  (* Derefs.statement := statement; *)
 
464
  InOutContext.self_internal := Internals.self;
 
465
  InOutContext.self_external := Externals.self;
 
466
  InOutContext.get_internal := get_internal;
 
467
  InOutContext.get_external := get_external;
 
468
  InOutContext.compute := compute_external;
 
469
  InOutContext.display := pretty_internal
 
470
 
 
471
let option =
 
472
  "-inout",
 
473
  Arg.Unit Cmdline.ForceInout.on,
 
474
  ": force operational inout display; this gives the operational inputs, an over-approximation of the set of locations whose initial value is used; and the sure outputs, an under-approximation of the set of writen tsets "
 
475
 
 
476
(*
 
477
Local Variables:
 
478
compile-command: "LC_ALL=C make -C ../.."
 
479
End:
 
480
*)