mmodel_analysis.ml 28.2 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Patrick Baudin's avatar
Patrick Baudin committed
3
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
4
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
Virgile Prevosto's avatar
Virgile Prevosto committed
6
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
7
8
9
10
11
12
13
14
15
16
17
18
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
Virgile Prevosto's avatar
Virgile Prevosto committed
19
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
20
21
22
23
24
25
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil_datatype

26
27
module Dataflow = Dataflow2

28
let must_never_monitor vi =
29
30
31
  (* E-ACSL, please do not monitor yourself! *)
  Functions.RTL.is_rtl_name vi.vname
  ||
32
  (* extern ghost variables are usually used (by the Frama-C libc) to
33
34
       represent some internal invisible states in ACSL specifications. They do
       not correspond to something concrete *)
35
36
  (vi.vghost && vi.vstorage = Extern)
  ||
37
38
  (* incomplete types cannot be properly monitored. See BTS #2406. *)
  not (Cil.isCompleteType vi.vtype)
39

Julien Signoles's avatar
Julien Signoles committed
40
41
42
43
44
(* ********************************************************************** *)
(* Backward dataflow analysis to compute a sound over-approximation of what
   left-values must be tracked by the memory model library *)
(* ********************************************************************** *)

45
let dkey = Options.dkey_analysis
46
module Env: sig
47
  val has_heap_allocations: unit -> bool
48
  val check_heap_allocations: kernel_function -> unit
49
  val default_varinfos: Varinfo.Hptset.t option -> Varinfo.Hptset.t
50
51
  val apply: (kernel_function -> 'a) -> kernel_function -> 'a
  val clear: unit -> unit
52
53
54
  val add: kernel_function -> Varinfo.Hptset.t option Stmt.Hashtbl.t -> unit
  val add_init: kernel_function -> Varinfo.Hptset.t option -> unit
  val mem_init: kernel_function -> Varinfo.Hptset.t option -> bool
55
56
  val find: kernel_function -> Varinfo.Hptset.t option Stmt.Hashtbl.t
  module StartData:
57
    Dataflow.StmtStartData with type data = Varinfo.Hptset.t option
58
  val is_consolidated: unit -> bool
59
  val consolidate: Varinfo.Hptset.t -> unit
60
  val consolidated_mem: varinfo -> bool
61
  val is_empty: unit -> bool
62
63
end = struct

64
65
  let heap_allocation_ref = ref false
  let has_heap_allocations () = !heap_allocation_ref
66
  let check_heap_allocations kf =
67
    (* a function with no definition potentially allocates memory *)
68
69
    heap_allocation_ref :=
      !heap_allocation_ref || not (Kernel_function.is_definition kf)
70

71
  let current_kf = ref None
72
  let default_varinfos = function None -> Varinfo.Hptset.empty | Some s -> s
73
74
75

  let apply f kf =
    let old = !current_kf in
76
    current_kf := Some kf;
77
78
79
80
81
82
83
84
    let res = f kf in
    current_kf := old;
    res

  let tbl = Kernel_function.Hashtbl.create 7
  let add = Kernel_function.Hashtbl.add tbl
  let find = Kernel_function.Hashtbl.find tbl

85
86
87
  module S = Set.Make(Datatype.Option(Varinfo.Hptset))

  let tbl_init = Kernel_function.Hashtbl.create 7
88
  let add_init kf init =
89
90
91
92
93
94
95
    let set =
      try Kernel_function.Hashtbl.find tbl_init kf
      with Not_found -> S.empty
    in
    let set = S.add init set in
    Kernel_function.Hashtbl.replace tbl_init kf set

96
97
  let mem_init kf init =
    try
98
99
      let set = Kernel_function.Hashtbl.find tbl_init kf in
      S.mem init set
100
    with Not_found ->
101
102
      false

103
  module StartData = struct
104
    type data = Varinfo.Hptset.t option
105
    let apply f =
106
      try
107
        let kf = Extlib.opt_conv (Kernel_function.dummy()) !current_kf in
Julien Signoles's avatar
Julien Signoles committed
108
109
        let h = Kernel_function.Hashtbl.find tbl kf in
        f h
110
      with Not_found ->
Julien Signoles's avatar
Julien Signoles committed
111
        assert false
112
113
114
115
116
117
118
119
120
    let clear () = apply Stmt.Hashtbl.clear
    let mem k = apply Stmt.Hashtbl.mem k
    let find k = apply Stmt.Hashtbl.find k
    let replace k v = apply Stmt.Hashtbl.replace k v
    let add k v = apply Stmt.Hashtbl.add k v
    let iter f = apply (Stmt.Hashtbl.iter f)
    let length () = apply Stmt.Hashtbl.length
  end

121
122
123
124
  (* TODO: instead of this costly consolidation, why do not take the state of
     the entry point of the function? *)

  let consolidated_set = ref Varinfo.Hptset.empty
125
126
  let is_consolidated_ref = ref false

127
  let consolidate set =
128
    let set = Varinfo.Hptset.union set !consolidated_set in
129
130
    consolidated_set := set

131
  let consolidated_mem v =
132
    is_consolidated_ref := true;
133
    Varinfo.Hptset.mem v !consolidated_set
134
135
136

  let is_consolidated () = !is_consolidated_ref

137
138
139
  let is_empty () =
    try
      Kernel_function.Hashtbl.iter
140
        (fun _ h ->
Julien Signoles's avatar
Julien Signoles committed
141
142
143
144
145
146
          Stmt.Hashtbl.iter
            (fun _ set -> match set with
            | None -> ()
            | Some s -> if not (Varinfo.Hptset.is_empty s) then raise Exit)
            h)
        tbl;
147
148
149
150
      true
    with Exit ->
      false

151
  let clear () =
152
    Kernel_function.Hashtbl.clear tbl;
153
    consolidated_set := Varinfo.Hptset.empty;
154
155
    is_consolidated_ref := false;
    heap_allocation_ref := false
156
157
158

end

159
let reset () =
160
161
  Options.feedback ~dkey ~level:2 "clearing environment.";
  Env.clear ()
162
163

module rec Transfer
164
  : Dataflow.BackwardsTransfer with type t = Varinfo.Hptset.t option
165
166
167
168
  = struct

  let name = "E_ACSL.Pre_analysis"

169
  let debug = false
170

171
  type t = Varinfo.Hptset.t option
172
173
174

  module StmtStartData = Env.StartData

175
176
  let pretty fmt state = match state with
    | None -> Format.fprintf fmt "None"
177
    | Some s -> Format.fprintf fmt "%a" Varinfo.Hptset.pretty s
178
179
180
181
182
183
184
185
186
187

  (** The data at function exit. Used for statements with no successors.
      This is usually bottom, since we'll also use doStmt on Return
      statements. *)
  let funcExitData = None

  (** When the analysis reaches the start of a block, combine the old data with
      the one we have just computed. Return None if the combination is the same
      as the old data, otherwise return the combination. In the latter case, the
      predecessors of the statement are put on the working list. *)
188
189
190
  let combineStmtStartData stmt ~old state = match stmt.skind, old, state with
    | _, _, None -> assert false
    | _, None, Some _ -> Some state (* [old] already included in [state] *)
191
    | Return _, Some old, Some new_ ->
192
      Some (Some (Varinfo.Hptset.union old new_))
193
    | _, Some old, Some new_ ->
194
      if Varinfo.Hptset.equal old new_ then
Julien Signoles's avatar
Julien Signoles committed
195
        None
196
      else
Julien Signoles's avatar
Julien Signoles committed
197
        Some (Some (Varinfo.Hptset.union old new_))
198
199

  (** Take the data from two successors and combine it *)
200
201
  let combineSuccessors s1 s2 =
    Some
202
      (Varinfo.Hptset.union (Env.default_varinfos s1) (Env.default_varinfos s2))
203

204
  let is_ptr_or_array ty = Cil.isPointerType ty || Cil.isArrayType ty
205
206
207
208
209

  let is_ptr_or_array_exp e =
    let ty = Cil.typeOf e in
    is_ptr_or_array ty

210
211
212
213
214
215
216
  let may_alias li = match li.l_var_info.lv_type with
    | Ctype ty -> is_ptr_or_array ty
    | Linteger | Lreal -> false
    | Ltype _ -> Error.not_yet "user defined type"
    | Lvar _ -> Error.not_yet "named type"
    | Larrow _ -> Error.not_yet "functional type"

217
  let rec base_addr_node = function
218
    | Lval lv | AddrOf lv | StartOf lv ->
219
220
221
      (match lv with
      | Var vi, _ -> Some vi
      | Mem e, _ -> base_addr e)
222
    | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
223
224
      if is_ptr_or_array_exp e1 then base_addr e1
      else begin
Julien Signoles's avatar
Julien Signoles committed
225
226
        assert (is_ptr_or_array_exp e2);
        base_addr e2
227
228
      end
    | Info(e, _) | CastE(_, e) -> base_addr e
229
    | BinOp((MinusPP | PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
Julien Signoles's avatar
Julien Signoles committed
230
231
                | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
            _, _, _)
232
233
    | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
    | AlignOfE _ ->
234
235
236
237
238
239
      None

  and base_addr e = base_addr_node e.enode

  let extend_to_expr always state lhost e =
    let add_vi state vi =
240
241
      if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state)
      then begin
Julien Signoles's avatar
Julien Signoles committed
242
243
        match base_addr e with
        | None -> state
244
        | Some vi_e ->
245
246
247
248
249
250
251
252
253
          if must_never_monitor vi then state
          else begin
            Options.feedback ~level:4 ~dkey
              "monitoring %a from %a."
              Printer.pp_varinfo vi_e
              Printer.pp_lval (lhost, NoOffset);
            Varinfo.Hptset.add vi_e state
          end
      end else
Julien Signoles's avatar
Julien Signoles committed
254
        state
255
256
257
    in
    match lhost with
    | Var vi -> add_vi state vi
258
    | Mem e ->
259
      match base_addr e with
260
      | None -> state
261
262
      | Some vi -> add_vi state vi

263
  (* if [e] contains a pointer left-value, then also monitor the host *)
264
  let rec extend_from_addr state lv e = match e.enode with
265
266
    | Lval(lhost, _) ->
      if is_ptr_or_array_exp e then
Julien Signoles's avatar
Julien Signoles committed
267
268
        extend_to_expr true state lhost (Cil.new_exp ~loc:e.eloc (Lval lv)),
        true
269
      else
Julien Signoles's avatar
Julien Signoles committed
270
        state, false
271
    | AddrOf(lhost, _) ->
272
273
      extend_to_expr true state lhost (Cil.new_exp ~loc:e.eloc (Lval lv)),
      true
274
    | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
275
276
      if is_ptr_or_array_exp e1 then extend_from_addr state lv e1
      else begin
Julien Signoles's avatar
Julien Signoles committed
277
278
        assert (is_ptr_or_array_exp e2);
        extend_from_addr state lv e2
279
280
281
282
283
      end
    | CastE(_, e) | Info(e, _) -> extend_from_addr state lv e
    | _ -> state, false

  let handle_assignment state (lhost, _ as lv) e =
284
    (* if [e] is a pointer left-value, then also monitor the host *)
285
286
287
    let state, always = extend_from_addr state lv e in
    extend_to_expr always state lhost e

288
  let rec register_term_lval kf varinfos (thost, _) =
Julien Signoles's avatar
Julien Signoles committed
289
    let add_vi kf vi =
290
291
      Options.feedback ~level:4 ~dkey "monitoring %a from annotation of %a."
        Printer.pp_varinfo vi
Julien Signoles's avatar
Julien Signoles committed
292
        Kernel_function.pretty kf;
293
      Varinfo.Hptset.add vi varinfos
Julien Signoles's avatar
Julien Signoles committed
294
295
    in
    match thost with
296
    | TVar { lv_origin = None } -> varinfos
Julien Signoles's avatar
Julien Signoles committed
297
298
    | TVar { lv_origin = Some vi } -> add_vi kf vi
    | TResult _ -> add_vi kf (Misc.result_vi kf)
299
300
301
    | TMem t -> register_term kf varinfos t

  and register_term kf varinfos term = match term.term_node with
302
    | TLval tlv | TAddrOf tlv | TStartOf tlv ->
303
      register_term_lval kf varinfos tlv
304
    | TCastE(_, t) | Tat(t, _) ->
305
      register_term kf varinfos t
306
307
308
309
310
311
    | Tlet(li, t) ->
      if may_alias li then Error.not_yet "let-binding on array or pointer"
      else begin
        let varinfos = register_term kf varinfos t in
        register_body kf varinfos li.l_body
      end
312
313
314
315
316
317
    | Tif(_, t1, t2) ->
      let varinfos = register_term kf varinfos t1 in
      register_term kf varinfos t2
    | TBinOp((PlusPI | IndexPI | MinusPI), t1, t2) ->
      (match t1.term_type with
      | Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t1
318
      | _ ->
Julien Signoles's avatar
Julien Signoles committed
319
320
        match t2.term_type with
        | Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t2
321
        | _ ->
322
323
          if Misc.is_set_of_ptr_or_array t1.term_type ||
             Misc.is_set_of_ptr_or_array t2.term_type then
324
            (* Occurs for example from:
325
326
327
328
              \valid(&multi_dynamic[2..4][1..7])
              where multi_dynamic has been dynamically allocated *)
            let varinfos = register_term kf varinfos t1 in
            register_term kf varinfos t2
329
330
          else
            assert false)
331
332
333
334
    | TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
    | TAlignOfE _ | Tnull | Ttype _ | TUnOp _ | TBinOp _ ->
      varinfos
    | Tlambda(_, _) -> Error.not_yet "lambda function"
335
    | Tapp(_, _, _) -> Error.not_yet "function application"
336
337
338
339
    | TDataCons _ -> Error.not_yet "data constructor"
    | Tbase_addr _ -> Error.not_yet "\\base_addr"
    | Toffset _ -> Error.not_yet "\\offset"
    | Tblock_length _ -> Error.not_yet "\\block_length"
340
    | TLogic_coerce(_, t) -> register_term kf varinfos t
341
342
343
344
345
346
    | TUpdate _ -> Error.not_yet "functional update"
    | Ttypeof _ -> Error.not_yet "typeof"
    | Tempty_set -> Error.not_yet "empty set"
    | Tunion _ -> Error.not_yet "set union"
    | Tinter _ -> Error.not_yet "set intersection"
    | Tcomprehension _ -> Error.not_yet "set comprehension"
347
348
349
350
351
    | Trange(Some t1, Some t2) ->
      let varinfos = register_term kf varinfos t1 in
      register_term kf varinfos t2
    | Trange(None, _) | Trange(_, None) ->
      Options.abort "unbounded ranges are not part of E-ACSL"
352

353
354
355
356
357
358
  and register_body kf varinfos = function
    | LBnone | LBreads _ -> varinfos
    | LBterm t -> register_term kf varinfos t
    | LBpred _ -> Options.fatal "unexpected predicate"
    | LBinductive _ -> Error.not_yet "inductive definitions"

359
360
  let register_object kf state_ref = object
    inherit Visitor.frama_c_inplace
361
    method !vpredicate_node = function
362
363
    | Pvalid(_, t) | Pvalid_read(_, t) | Pvalid_function t
    | Pinitialized(_, t) | Pfreeable(_, t) ->
364
      (*	Options.feedback "REGISTER %a" Cil.d_term t;*)
365
      state_ref := register_term kf !state_ref t;
366
      Cil.DoChildren
367
368
369
    | Pallocable _ -> Error.not_yet "\\allocable"
    | Pfresh _ -> Error.not_yet "\\fresh"
    | Pseparated _ -> Error.not_yet "\\separated"
370
    | Pdangling _ -> Error.not_yet "\\dangling"
371
    | Ptrue | Pfalse | Papp _ | Prel _
372
    | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
373
    | Pforall _ | Pexists _ | Pat _ ->
374
      Cil.DoChildren
375
376
377
378
379
380
    | Plet(li, _) ->
      if may_alias li then Error.not_yet "let-binding on array or pointer"
      else begin
        state_ref := register_term kf !state_ref (Misc.term_of_li li);
        Cil.DoChildren
      end
381
    method !vterm term = match term.term_node with
382
    | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) | Tlet(_, t) ->
383
      state_ref := register_term kf !state_ref t;
384
      Cil.DoChildren
385
386
    | TConst _ | TSizeOf _ | TSizeOfStr _ | TAlignOf _  | Tnull | Ttype _
    | Tempty_set ->
387
      (* no left-value inside inside: skip for efficiency *)
388
      Cil.SkipChildren
389
    | TUnOp _ | TBinOp _ | Ttypeof _ | TSizeOfE _
390
391
    | TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
    | TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
392
    | TUpdate _ | Tunion _ | Tinter _
393
    | Tcomprehension _ | Trange _ | TLogic_coerce _ ->
394
      (* potential sub-term inside *)
395
      Cil.DoChildren
396
397
    method !vlogic_label _ = Cil.SkipChildren
    method !vterm_lhost = function
398
    | TMem t ->
399
      (* potential RTE *)
400
      state_ref := register_term kf !state_ref t;
401
      Cil.DoChildren
402
    | TVar _ | TResult _ ->
403
404
405
      Cil.SkipChildren
  end

406
let register_predicate kf pred state =
Julien Signoles's avatar
Julien Signoles committed
407
408
409
410
411
412
413
  let state_ref = ref state in
  Error.handle
    (fun () ->
      ignore
        (Visitor.visitFramacIdPredicate (register_object kf state_ref) pred))
    ();
  !state_ref
414

415
  let register_code_annot kf a state =
416
    let state_ref = ref state in
417
418
    Error.handle
      (fun () ->
419
        ignore
Julien Signoles's avatar
Julien Signoles committed
420
          (Visitor.visitFramacCodeAnnotation (register_object kf state_ref) a))
421
      ();
422
423
    !state_ref

424
425
    let rec do_init vi init state = match init with
      | SingleInit e -> handle_assignment state (Var vi, NoOffset) e
426
      | CompoundInit(_, l) ->
Julien Signoles's avatar
Julien Signoles committed
427
        List.fold_left (fun state (_, init) -> do_init vi init state) state l
428
429

  let register_initializers state =
430
    let do_one vi init state = match init.init with
431
432
433
      | None -> state
      | Some init -> do_init vi init state
    in
434
435
436
437
    Globals.Vars.fold_in_file_rev_order do_one state
(* below: compatibility with Fluorine *)
(*    let l = Globals.Vars.fold_in_file_order (fun v i l -> (v, i) :: l) [] in
    List.fold_left (fun state (v, i) -> do_one v i state) state l*)
438

439
440
441
442
443
444
  (** The (backwards) transfer function for a branch. The [(Cil.CurrentLoc.get
      ())] is set before calling this. If it returns None, then we have some
      default handling. Otherwise, the returned data is the data before the
      branch (not considering the exception handlers) *)
  let doStmt stmt =
    let _, kf = Kernel_function.find_from_sid stmt.sid in
445
446
    let is_first = Kernel_function.is_first_stmt kf stmt in
    let is_last = Kernel_function.is_return_stmt kf stmt in
447
    Dataflow.Post
448
      (fun state ->
Julien Signoles's avatar
Julien Signoles committed
449
        let state = Env.default_varinfos state in
450
        let state =
Julien Signoles's avatar
Julien Signoles committed
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
          if Functions.check kf then
            let state =
              if (is_first || is_last) && Functions.RTL.is_generated_kf kf then
                Annotations.fold_behaviors
                  (fun _ bhv s ->
                    let handle_annot test f s =
                      if test then
                        f
                          (fun _ p s -> register_predicate kf p s)
                          kf
                          bhv.b_name
                          s
                      else
                        s
                  in
                    let s = handle_annot is_first Annotations.fold_requires s in
                    let s = handle_annot is_first Annotations.fold_assumes s in
                    handle_annot
                      is_last
                      (fun f ->
                        Annotations.fold_ensures (fun e (_, p) -> f e p)) s)
                  kf
                  state
              else
                state
            in
            let state =
              Annotations.fold_code_annot
                (fun _ -> register_code_annot kf) stmt state
            in
            if stmt.ghost then
              let rtes = Rte.stmt kf stmt in
              List.fold_left
                (fun state a -> register_code_annot kf a state) state rtes
            else
Julien Signoles's avatar
Julien Signoles committed
486
              state
Julien Signoles's avatar
Julien Signoles committed
487
          else (* not (Options.Functions.check kf): do not monitor [kf] *)
Julien Signoles's avatar
Julien Signoles committed
488
489
490
491
492
493
            state
        in
        let state =
        (* take initializers into account *)
          if is_first then
            let main, lib = Globals.entry_point () in
494
            if Kernel_function.equal kf main && not lib then
Julien Signoles's avatar
Julien Signoles committed
495
496
497
498
499
500
501
              register_initializers state
            else
              state
          else
            state
        in
        Some state)
502

503
504
  let do_call res f args state =
    let kf = Globals.Functions.get f in
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
    Env.check_heap_allocations kf;
    let params = Globals.Functions.get_params kf in
    let state =
      if Kernel_function.is_definition kf then
        try
          (* compute the initial state of the called function *)
          let init =
            List.fold_left2
              (fun acc p a -> match base_addr a with
              | None -> acc
              | Some vi ->
                if Varinfo.Hptset.mem vi state
                then Varinfo.Hptset.add p acc
                else acc)
              state
              params
521
              args
522
          in
523
          let init = match res with
524
525
526
527
528
            | None -> init
            | Some lv ->
              match base_addr_node (Lval lv) with
              | None -> init
              | Some vi ->
529
                if Varinfo.Hptset.mem vi state
530
531
532
533
534
535
536
537
538
539
540
541
542
543
                then Varinfo.Hptset.add (Misc.result_vi kf) init
                else init
          in
          let state = Compute.get ~init kf in
          (* compute the resulting state by keeping arguments whenever the
             corresponding formals must be kept *)
          List.fold_left2
            (fun acc p a -> match base_addr a with
            | None -> acc
            | Some vi ->
              if Varinfo.Hptset.mem p state then Varinfo.Hptset.add vi acc
              else acc)
            state
            params
544
545
            args
        with Invalid_argument _ ->
546
          Options.warning ~current:true
547
            "ignoring effect of variadic function %a"
548
549
550
551
552
553
            Kernel_function.pretty
            kf;
          state
      else
        state
    in
554
    let state = match res, Kernel_function.is_definition kf with
555
556
557
558
      | None, _ | _, false -> state
      | Some (lhost, _), true ->
        (* add the result if \result must be kept after calling the kf *)
        let vi = Misc.result_vi kf in
559
        if  Varinfo.Hptset.mem vi state then
560
561
          match lhost with
          | Var vi -> Varinfo.Hptset.add vi state
562
          | Mem e ->
563
564
565
566
567
568
569
            match base_addr e with
            | None -> state
            | Some vi -> Varinfo.Hptset.add vi state
        else
          state
    in
    Dataflow.Done (Some state)
570
571
572
573
574
575


  (** The (backwards) transfer function for an instruction. The
      [(Cil.CurrentLoc.get ())] is set before calling this. If it returns
      None, then we have some default handling. Otherwise, the returned data is
      the data before the branch (not considering the exception handlers) *)
576
  let doInstr _stmt instr state =
577
578
    let state = Env.default_varinfos state in
    match instr with
579
    | Set(lv, e, _) ->
580
581
582
583
584
      let state = handle_assignment state lv e in
      Dataflow.Done (Some state)
    | Local_init(v,AssignInit i,_) ->
      let state = do_init v i state in
      Dataflow.Done (Some state)
Virgile Prevosto's avatar
Virgile Prevosto committed
585
586
587
588
589
    | Local_init(v,ConsInit(f,args,Constructor),_) ->
      do_call None f (Cil.mkAddrOfVi v :: args) state
    | Local_init(v,ConsInit(f,args,Plain_func),_) ->
      do_call (Some (Cil.var v)) f args state
    | Call(result, f_exp, l, _) ->
590
591
      (match f_exp.enode with
      | Lval(Var vi, NoOffset) -> do_call result vi l state
592
      | _ ->
Andre Maroneze's avatar
Andre Maroneze committed
593
594
        Options.warning ~current:true
          "function pointers may introduce too limited instrumentation.";
Julien Signoles's avatar
Julien Signoles committed
595
(* imprecise function call: keep each argument *)
596
        Dataflow.Done
Julien Signoles's avatar
Julien Signoles committed
597
598
599
600
601
          (Some
             (List.fold_left
                (fun acc e -> match base_addr e with
                | None -> acc
                | Some vi -> Varinfo.Hptset.add vi acc)
602
                state
Julien Signoles's avatar
Julien Signoles committed
603
                l)))
604
605
606
607
608
609
610
611
612
    | Asm _ -> Error.not_yet "asm"
    | Skip _ | Code_annot _ -> Dataflow.Default

  (** Whether to put this statement in the worklist. This is called when a
      block would normally be put in the worklist. *)
  let filterStmt _predecessor _block = true

end

613
614
and Compute: sig
  val get: ?init:Varinfo.Hptset.t -> kernel_function -> Varinfo.Hptset.t
615
end = struct
616
617
618

  module D = Dataflow.Backwards(Transfer)

619
620
  let compute init_set kf =
    Options.feedback ~dkey ~level:2 "entering in function %a."
621
      Kernel_function.pretty kf;
622
    assert (not (Misc.is_library_loc (Kernel_function.get_location kf)));
623
624
625
626
    let tbl, is_init =
      try Env.find kf, true
      with Not_found -> Stmt.Hashtbl.create 17, false
    in
Julien Signoles's avatar
Julien Signoles committed
627
    (*    Options.feedback "ANALYSING %a" Kernel_function.pretty kf;*)
628
    if not is_init then Env.add kf tbl;
629
    (try
Julien Signoles's avatar
Julien Signoles committed
630
631
       let fundec = Kernel_function.get_definition kf in
       let stmts, returns = Dataflow.find_stmts fundec in
632
       if is_init then
Julien Signoles's avatar
Julien Signoles committed
633
         Extlib.may
634
635
636
637
638
           (fun set ->
             List.iter
               (fun s ->
                 let old =
                   try Extlib.the (Stmt.Hashtbl.find tbl s)
Julien Signoles's avatar
Julien Signoles committed
639
640
                   with Not_found -> assert false
                 in
641
                 Stmt.Hashtbl.replace
Julien Signoles's avatar
Julien Signoles committed
642
643
644
645
646
647
648
649
                   tbl
                   s
                   (Some (Varinfo.Hptset.union set old)))
               returns)
           init_set
       else begin
         List.iter (fun s -> Stmt.Hashtbl.add tbl s None) stmts;
         Extlib.may
650
           (fun set ->
Julien Signoles's avatar
Julien Signoles committed
651
652
653
654
             List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
           init_set
       end;
       D.compute stmts
655
     with Kernel_function.No_Definition | Kernel_function.No_Statement ->
Julien Signoles's avatar
Julien Signoles committed
656
       ());
657
    Options.feedback ~dkey ~level:2 "function %a done."
658
659
      Kernel_function.pretty kf;
    tbl
660

661
  let get ?init kf =
662
    if Misc.is_library_loc (Kernel_function.get_location kf) then
663
      Varinfo.Hptset.empty
664
665
    else
      try
Julien Signoles's avatar
Julien Signoles committed
666
667
        let stmt = Kernel_function.find_first_stmt kf in
(*      Options.feedback "GETTING %a" Kernel_function.pretty kf;*)
668
        let tbl =
Julien Signoles's avatar
Julien Signoles committed
669
670
671
672
673
          if Env.mem_init kf init then
            try Env.find kf with Not_found -> assert false
          else begin
    (* WARN: potentially incorrect in case of recursive call *)
            Env.add_init kf init;
674
            Env.apply (compute init) kf
Julien Signoles's avatar
Julien Signoles committed
675
676
677
678
679
680
          end
        in
        try
          let set = Stmt.Hashtbl.find tbl stmt in
          Env.default_varinfos set
        with Not_found ->
681
          Options.fatal "[pre_analysis] stmt never analyzed: %a"
Julien Signoles's avatar
Julien Signoles committed
682
            Printer.pp_stmt stmt
683
      with Kernel_function.No_Statement ->
Julien Signoles's avatar
Julien Signoles committed
684
        Varinfo.Hptset.empty
685
686
687

end

688
let consolidated_must_model_vi vi =
689
690
  if Env.is_consolidated () then
    Env.consolidated_mem vi
691
  else begin
692
693
    Options.feedback ~level:2 "performing pre-analysis for minimal memory \
instrumentation.";
694
695
696
697
698
699
    (try
       let main, _ = Globals.entry_point () in
       let set = Compute.get main in
       Env.consolidate set
     with Globals.No_such_entry_point s ->
       Options.warning ~once:true "%s@ \
700
701
@[The generated program may miss memory instrumentation@ \
if there are memory-related annotations.@]"
Julien Signoles's avatar
Julien Signoles committed
702
 s);
703
    Options.feedback ~level:2 "pre-analysis done.";
704
705
    Env.consolidated_mem vi
  end
706

707
let must_model_vi ?kf ?stmt vi =
708
  let _kf = match kf, stmt with
709
710
711
    | None, None | Some _, _ -> kf
    | None, Some stmt -> Some (Kernel_function.find_englobing_kf stmt)
  in
712
713
714
  (* [JS 2013/05/07] that is unsound to take the env from the given stmt in
     presence of aliasing with an address (see tests address.i).
     TODO: could be optimized though *)
715
  consolidated_must_model_vi vi
716
(*  match stmt, kf with
717
  | None, _ -> consolidated_must_model_vi vi
718
719
720
  | Some _, None ->
    assert false
  | Some stmt, Some kf  ->
721
    if not (Env.is_consolidated ()) then
722
      ignore (consolidated_must_model_vi vi);
723
    try
724
725
      let tbl = Env.find kf in
      try
Julien Signoles's avatar
Julien Signoles committed
726
727
let set = Stmt.Hashtbl.find tbl stmt in
Varinfo.Hptset.mem vi (Env.default_varinfos set)
728
      with Not_found ->
Julien Signoles's avatar
Julien Signoles committed
729
730
(* new statement *)
consolidated_must_model_vi vi
731
    with Not_found ->
732
733
      (* [kf] is dead code *)
      false
734
 *)
735

736
737
738
let rec apply_on_vi_base_from_lval f ?kf ?stmt = function
  | Var vi, _ -> f ?kf ?stmt vi
  | Mem e, _ -> apply_on_vi_base_from_exp f ?kf ?stmt e
739

740
and apply_on_vi_base_from_exp f ?kf ?stmt e = match e.enode with
741
  | Lval lv | AddrOf lv | StartOf lv ->
742
    apply_on_vi_base_from_lval f ?kf ?stmt lv
743
  | BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) ->
744
    apply_on_vi_base_from_exp f ?kf ?stmt e1
745
  | BinOp(MinusPP, e1, e2, _) ->
746
747
748
    apply_on_vi_base_from_exp f ?kf ?stmt e1
    || apply_on_vi_base_from_exp f ?kf ?stmt e2
  | Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f ?kf ?stmt e
749
750
  | BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt | Lt | Gt | Le
            | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
751
  | Const _ -> (* possible in case of static address *) false
752
  | UnOp _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
753
    Options.fatal "[pre_analysis] unexpected expression %a" Exp.pretty e
754

755
756
757
let must_model_lval = apply_on_vi_base_from_lval must_model_vi
let must_model_exp = apply_on_vi_base_from_exp must_model_vi

758
let must_never_monitor_lval ?kf ?stmt lv =
759
  apply_on_vi_base_from_lval
760
    (fun ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
761
762
763
764
    ?kf
    ?stmt
    lv

765
let must_never_monitor_exp ?kf ?stmt lv  =
766
  apply_on_vi_base_from_exp
767
    (fun ?kf:_ ?stmt:_ vi -> must_never_monitor vi)
768
769
770
771
    ?kf
    ?stmt
    lv

772
(* ************************************************************************** *)
773
(** {1 Public API} *)
774
775
(* ************************************************************************** *)

776
let must_model_vi ?kf ?stmt vi =
777
  not (must_never_monitor vi)
778
779
  &&
    (Options.Full_mmodel.get ()
780
     || Error.generic_handle (must_model_vi ?kf ?stmt) false vi)
781

782
783
let must_model_lval ?kf ?stmt lv =
  not (must_never_monitor_lval ?kf ?stmt lv)
784
785
  &&
    (Options.Full_mmodel.get ()
786
     || Error.generic_handle (must_model_lval ?kf ?stmt) false lv)
787

788
789
let must_model_exp ?kf ?stmt exp =
  not (must_never_monitor_exp ?kf ?stmt exp)
790
791
  &&
    (Options.Full_mmodel.get ()
792
     || Error.generic_handle (must_model_exp ?kf ?stmt) false exp)
793

794
795
796
797
let use_model () =
  not (Env.is_empty ())
  || Options.Full_mmodel.get ()
  || Env.has_heap_allocations ()
798

799
800
(*
Local Variables:
801
compile-command: "make -C ../.."
802
803
End:
*)