package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file cfgInfos.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
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
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         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                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

module Cfg = Interpreted_automata
module Fset = Kernel_function.Set
module Sset = Cil_datatype.Stmt.Set
module Pset = Property.Set
module Shash = Cil_datatype.Stmt.Hashtbl

(* -------------------------------------------------------------------------- *)
(* --- Compute Kernel-Function & CFG Infos for WP                         --- *)
(* -------------------------------------------------------------------------- *)

module CheckPath = Graph.Path.Check(Cfg.G)

type t = {
  body : Cfg.automaton option ;
  checkpath : CheckPath.path_checker option ;
  reachability : WpReached.reachability option ;
  mutable annots : bool; (* has goals to prove *)
  mutable doomed : WpPropId.prop_id Bag.t;
  mutable calls : Kernel_function.Set.t;
  mutable no_variant_loops : Sset.t;
  mutable terminates_deps : Pset.t;
}

(* -------------------------------------------------------------------------- *)
(* --- Getters                                                            --- *)
(* -------------------------------------------------------------------------- *)

let body infos = infos.body
let calls infos = infos.calls
let annots infos = infos.annots
let doomed infos = infos.doomed

let wp_reached_smoking s = function
  | None -> false
  | Some reachability -> WpReached.smoking reachability s

let smoking infos s = wp_reached_smoking s infos.reachability

let unreachable infos v =
  match infos.body, infos.checkpath with
  | Some cfg , Some checkpath ->
    not @@ CheckPath.check_path checkpath cfg.entry_point v
  | _ -> true

let terminates_deps infos = infos.terminates_deps

(* -------------------------------------------------------------------------- *)
(* --- Selected Properties                                                --- *)
(* -------------------------------------------------------------------------- *)

let selected ~bhv ~prop pid =
  (prop = [] || WpPropId.select_by_name prop pid) &&
  (bhv = [] || WpPropId.select_for_behaviors bhv pid)

let selected_default ~bhv =
  bhv=[] || List.mem Cil.default_behavior_name bhv

let selected_name ~prop name =
  prop=[] || WpPropId.are_selected_names prop [name]

let selected_assigns ~prop = function
  | Cil_types.WritesAny -> false
  | Writes _ when prop = [] -> true
  | Writes l ->
    let collect_names l (t, _) =
      WpPropId.ident_names t.Cil_types.it_content.term_name @ l
    in
    let names = List.fold_left collect_names ["@assigns"] l in
    WpPropId.are_selected_names prop names

let selected_allocates ~prop = function
  | Cil_types.FreeAllocAny -> false
  | _ -> (selected_name ~prop "@allocates" || selected_name ~prop "@frees")

let selected_precond ~prop ip =
  prop = [] ||
  let tk_name = "@requires" in
  let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
  WpPropId.are_selected_names prop (tk_name :: tp_names)

let selected_postcond ~prop (tk,ip) =
  prop = [] ||
  let tk_name = "@" ^ WpPropId.string_of_termination_kind tk in
  let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
  WpPropId.are_selected_names prop (tk_name :: tp_names)

let selected_requires ~prop (b : Cil_types.funbehavior) =
  List.exists (selected_precond ~prop) b.b_requires

let selected_call ~bhv ~prop kf =
  bhv = [] && List.exists (selected_requires ~prop) (Annotations.behaviors kf)

let selected_clause ~prop name getter kf =
  getter kf <> [] && selected_name ~prop name

let selected_terminates ~prop kf =
  match Annotations.terminates kf with
  | None ->
    false
  | Some ip ->
    let tk_name = "@terminates" in
    let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
    WpPropId.are_selected_names prop (tk_name :: tp_names)

let selected_decreases ~prop kf =
  match Annotations.decreases kf with
  | None -> false
  | Some (it, _) ->
    let tk_name = "@decreases" in
    let tp_names = WpPropId.ident_names it.term_name in
    WpPropId.are_selected_names prop (tk_name :: tp_names)

let selected_disjoint_complete kf ~bhv ~prop =
  selected_default ~bhv &&
  ( selected_clause ~prop "@complete_behaviors" Annotations.complete kf ||
    selected_clause ~prop "@disjoint_behaviors" Annotations.disjoint kf )

let selected_bhv ~smoking ~bhv ~prop (b : Cil_types.funbehavior) =
  (bhv = [] || List.mem b.b_name bhv) &&
  begin
    (selected_assigns ~prop b.b_assigns) ||
    (selected_allocates ~prop b.b_allocation) ||
    (smoking && b.b_requires <> []) ||
    (List.exists (selected_postcond ~prop) b.b_post_cond)
  end

let selected_main_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
  (bhv = [] || List.mem b.b_name bhv) && (selected_requires ~prop b)

(* -------------------------------------------------------------------------- *)
(* --- Calls                                                              --- *)
(* -------------------------------------------------------------------------- *)

let collect_calls ~bhv ?(on_missing_calls=fun _ -> ()) kf stmt =
  let open Cil_types in
  match stmt.skind with
  | Instr(Call(_,fct,_,_)) ->
    begin
      match Kernel_function.get_called fct with
      | Some kf -> Fset.singleton kf
      | None ->
        let bhvs =
          if bhv = []
          then begin
            List.map (fun b -> b.b_name) (Annotations.behaviors kf)
          end
          else bhv in
        let calls =
          List.fold_left
            (fun fs bhv -> match Dyncall.get ~bhv stmt with
               | None -> fs
               | Some(_,kfs) -> List.fold_right Fset.add kfs fs
            ) Fset.empty bhvs
        in
        if Fset.is_empty calls then
          on_missing_calls stmt ;
        calls
    end
  | Instr(Local_init(x,ConsInit(vf, args, kind), loc)) ->
    Cil.treat_constructor_as_func
      (fun _r fct _args _loc ->
         match Kernel_function.get_called fct with
         | Some kf -> Fset.singleton kf
         | None -> Fset.empty)
      x vf args kind loc
  | _ -> Fset.empty

(* -------------------------------------------------------------------------- *)
(* --- Recursion                                                          --- *)
(* -------------------------------------------------------------------------- *)

module Callees = WpContext.StaticGenerator(Kernel_function)
    (struct
      type key = Kernel_function.t
      type data = Fset.t * Cil_types.stmt list
      (** functions + unspecified function pointer calls *)

      let name = "Wp.CfgInfos.SCallees"
      let compile = function
        | { Cil_types.fundec = Definition(fd, _ ) } as kf ->
          let stmts = ref [] in
          let on_missing_calls s = stmts := s :: !stmts in
          let fold e s =
            Fset.union e (collect_calls ~on_missing_calls ~bhv:[] kf s)
          in
          let kfs = List.fold_left fold Fset.empty fd.sallstmts in
          kfs, !stmts
        | _ -> Fset.empty, []
    end)

module RecursiveClusters : sig
  val is_recursive : Kernel_function.t -> bool
  val in_cluster : caller:Kernel_function.t -> Kernel_function.t -> bool
end =
struct
  (* Tarjan's algorithm, adapted from:
       http://pauillac.inria.fr/~levy/why3/graph/abs/scct/2/scc.html
     (proved in Why3)
  *)
  let successors kf = fst @@ Callees.get kf

  module HT = Cil_datatype.Kf.Hashtbl

  type env = {
    mutable stack: Fset.elt list;
    mutable id: int;
    table: (Fset.elt, int) Hashtbl.t ;
    clusters: Fset.t option HT.t ;
  }

  let rec unstack_to x ?(cluster=[]) = function
    | [] -> cluster, []
    | y :: s' when Kernel_function.equal y x -> x :: cluster, s'
    | y :: s' -> unstack_to x ~cluster:(y :: cluster) s'

  let rec dfs roots env =
    try
      let v = Fset.choose roots in
      let vn =
        try Hashtbl.find env.table v
        with Not_found -> visit_node v env
      in
      let others_n = dfs (Fset.remove v roots) env in
      min vn others_n
    with Not_found -> max_int
  and visit_node x env =
    let n = env.id in
    Hashtbl.replace env.table x n ;
    env.id <- n + 1;
    env.stack <- x :: env.stack;
    let base = dfs (successors x) env in
    if base < n then base
    else begin
      let (cluster, stack) = unstack_to x env.stack in
      List.iter (fun v -> Hashtbl.replace env.table v max_int) cluster ;
      env.stack <- stack;
      begin match cluster with
        | [ x ] when base = max_int ->
          HT.add env.clusters x None
        | cluster ->
          let set = Some (Fset.of_list cluster) in
          List.iter (fun kf -> HT.add env.clusters kf set) cluster
      end ;
      max_int
    end

  let make_clusters s =
    let e = {
      stack = []; id = 0; table = Hashtbl.create 37; clusters = HT.create 37
    } in
    ignore (dfs s e);
    e.clusters

  module RTable =
    State_builder.Option_ref(HT.Make(Datatype.Option(Fset)))
      (struct
        let name = "Wp.CfgInfo.RecursiveClusters"
        let dependencies = [ Ast.self ]
      end)

  let create () =
    let kfs = ref Kernel_function.Set.empty in
    Globals.Functions.iter(fun kf -> kfs := Fset.add kf !kfs) ;
    make_clusters !kfs

  let table () = RTable.memo create

  let get_cluster kf = HT.find (table ()) kf
  let is_recursive kf =
    (* in a recursive cluster or contains unspecified function pointer call *)
    None <> get_cluster kf || [] <> snd @@ Callees.get kf

  let in_cluster ~caller callee =
    match get_cluster caller with
    | None -> false
    | Some cluster -> Fset.mem callee cluster
end

let is_recursive = RecursiveClusters.is_recursive
let in_cluster = RecursiveClusters.in_cluster

let is_entry_point kf =
  not @@ Kernel.LibEntry.get () && Kernel_function.is_entry_point kf

(* -------------------------------------------------------------------------- *)
(* --- No variant loops                                                   --- *)
(* -------------------------------------------------------------------------- *)

let collect_loops_no_variant kf stmt =
  let open Cil_types in
  let fold_no_variant _ = function
    | { annot_content = AVariant v } as ca -> fun _ -> Some (ca, v)
    | _ -> Fun.id
  in
  let props_of_v ca v =
    let (d, _), (p, _) = CfgAnnot.mk_variant_properties kf stmt ca v in
    Pset.union
      (Pset.singleton @@ WpPropId.property_of_id d)
      (Pset.singleton @@ WpPropId.property_of_id p)
  in
  match stmt.skind with
  | Loop _ ->
    begin match Annotations.fold_code_annot fold_no_variant stmt None with
      | None -> Sset.singleton stmt, Pset.empty
      | Some (ca, v) -> Sset.empty, props_of_v ca (fst v)
    end
  | _ ->
    Sset.empty, Pset.empty

(* -------------------------------------------------------------------------- *)
(* --- Trivially terminates                                               --- *)
(* -------------------------------------------------------------------------- *)

let trivial_terminates = ref 0

let wp_trivially_terminates =
  Emitter.create
    "Trivial Termination"
    [Emitter.Property_status]
    ~correctness:[] (* TBC *)
    ~tuning:[] (* TBC *)

let set_trivially_terminates p hyps =
  incr trivial_terminates ;
  if Wp_parameters.has_dkey VCS.dkey_shell then
    Wp_parameters.feedback "[Valid] Goal %a (Cfg) (Trivial)"
      WpPropId.pp_propid p ;
  let pid = WpPropId.property_of_id p in
  let hyps = Property.Set.elements hyps in
  Property_status.emit wp_trivially_terminates ~hyps pid Property_status.True

(* -------------------------------------------------------------------------- *)
(* --- Memoization Key                                                    --- *)
(* -------------------------------------------------------------------------- *)

module Key =
struct
  type t = {
    kf: Kernel_function.t ;
    smoking: bool ;
    bhv : string list ;
    prop : string list ;
  }

  let compare a b =
    let cmp = Kernel_function.compare a.kf b.kf in
    if cmp <> 0 then cmp else
      let cmp = Stdlib.compare a.smoking b.smoking in
      if cmp <> 0 then cmp else
        let cmp = Stdlib.compare a.bhv b.bhv in
        if cmp <> 0 then cmp else
          Stdlib.compare a.prop b.prop

  let pp_filter kind fmt xs =
    match xs with
    | [] -> ()
    | x::xs ->
      Format.fprintf fmt "~%s:%s" kind x ;
      List.iter (Format.fprintf fmt ",%s") xs

  let pretty fmt k =
    begin
      Kernel_function.pretty fmt k.kf ;
      pp_filter "smoking" fmt (if k.smoking then ["true"] else []) ;
      pp_filter "bhv" fmt k.bhv ;
      pp_filter "prop" fmt k.prop ;
    end

end

(* -------------------------------------------------------------------------- *)
(* --- Main Collection Pass                                               --- *)
(* -------------------------------------------------------------------------- *)

let dead_posts ~bhv ~prop tk (bhvs : CfgAnnot.behavior list) =
  let post ~bhv ~prop tk (b: CfgAnnot.behavior) =
    let assigns, ps =  match tk with
      | Cil_types.Exits -> b.bhv_exit_assigns, b.bhv_exits
      | _ -> b.bhv_post_assigns, b.bhv_ensures in
    let ps = List.filter (selected ~prop ~bhv) @@ List.map fst ps in
    match assigns with
    | WpPropId.AssignsLocations(id, _) -> Bag.list (id :: ps)
    | _ -> Bag.list ps
  in Bag.umap_list (post ~bhv ~prop tk) bhvs

let loop_contract_pids kf stmt =
  match stmt.Cil_types.skind with
  | Loop _ ->
    let invs = CfgAnnot.get_loop_contract kf stmt in
    let add_assigns assigns l =
      match assigns with
      | WpPropId.NoAssignsInfo | AssignsAny _ -> l
      | AssignsLocations (pid, _) -> pid :: l
    in
    let verif_fold CfgAnnot.{ loop_est ; loop_ind } l =
      let l = Option.fold ~none:l ~some:(fun i -> i :: l) loop_est in
      Option.fold ~none:l ~some:(fun i -> i :: l) loop_ind
    in
    List.fold_right verif_fold invs.loop_invariants @@
    List.fold_right add_assigns invs.loop_assigns []
  | _ -> []

let compile Key.{ kf ; smoking ; bhv ; prop } =
  let open Current_loc.Operators in
  let<> UpdatedCurrentLoc = Kernel_function.get_location kf in
  let body, checkpath, reachability =
    if Kernel_function.has_definition kf then
      let cfg = Cfg.get_automaton kf in
      Some cfg,
      Some (CheckPath.create cfg.graph),
      if smoking then Some (WpReached.reachability kf) else None
    else None, None, None
  in
  let infos = {
    body ; checkpath ; reachability ;
    annots = false ;
    doomed = Bag.empty ;
    calls = Fset.empty ;
    no_variant_loops = Sset.empty ;
    terminates_deps = Pset.empty ;
  } in
  let behaviors = Annotations.behaviors kf in
  (* Inits *)
  if is_entry_point kf then
    infos.annots <- List.exists (selected_main_bhv ~bhv ~prop) behaviors ;
  (* Function Body *)
  Option.iter
    begin fun (cfg : Cfg.automaton) ->
      (* Spec Iteration *)
      if selected_decreases ~prop kf ||
         selected_terminates ~prop kf ||
         selected_disjoint_complete kf ~bhv ~prop ||
         (List.exists (selected_bhv ~smoking ~bhv ~prop) behaviors)
      then infos.annots <- true ;
      (* Stmt Iteration *)
      Shash.iter
        (fun stmt (src,_) ->
           let fs = collect_calls ~bhv kf stmt in
           let nv_loops, term_deps = collect_loops_no_variant kf stmt in
           let dead = unreachable infos src in
           let cas = CfgAnnot.get_code_assertions kf stmt in
           let ca_pids =
             List.filter_map
               (fun CfgAnnot.{ code_verified=ca } -> Option.map fst ca) cas in
           let loop_pids = loop_contract_pids kf stmt in
           if dead then
             begin
               if wp_reached_smoking stmt reachability then
                 (let p = CfgAnnot.get_unreachable kf stmt in
                  infos.doomed <- Bag.append infos.doomed p) ;
               infos.doomed <- Bag.concat infos.doomed (Bag.list ca_pids) ;
               infos.doomed <- Bag.concat infos.doomed (Bag.list loop_pids) ;
             end
           else
             begin
               if not infos.annots &&
                  ( List.exists (selected ~bhv ~prop) ca_pids ||
                    List.exists (selected ~bhv ~prop) loop_pids ||
                    Fset.exists (selected_call ~bhv ~prop) fs )
               then infos.annots <- true ;
               infos.calls <- Fset.union fs infos.calls ;
               infos.no_variant_loops <-
                 Sset.union nv_loops infos.no_variant_loops ;
               infos.terminates_deps <-
                 Pset.union term_deps infos.terminates_deps
             end
        ) cfg.stmt_table ;
      (* Dead Post Conditions *)
      let dead_exit = Fset.is_empty infos.calls in
      let dead_post = unreachable infos cfg.return_point in
      let bhvs =
        if dead_exit || dead_post then
          let exits = not dead_exit in
          List.map (CfgAnnot.get_behavior_goals kf ~exits) behaviors
        else [] in
      if dead_exit then
        infos.doomed <-
          Bag.concat infos.doomed (dead_posts ~bhv ~prop Exits bhvs) ;
      if dead_post then
        infos.doomed <-
          Bag.concat infos.doomed (dead_posts ~bhv ~prop Normal bhvs) ;
    end body ;
  (* Doomed *)
  Bag.iter
    (fun p -> if WpPropId.filter_status p then WpReached.set_unreachable p)
    infos.doomed ;
  (* Termination *)
  let infos =
    if Kernel_function.is_definition kf then
      match CfgAnnot.get_terminates_goal kf with
      | Some (id, _) when selected_terminates ~prop kf ->
        let warning_locs =
          List.map Cil_datatype.Stmt.loc @@ snd @@ Callees.get kf
        in
        if warning_locs <> [] then
          Wp_parameters.warning ~once:true
            "In '%a', no 'calls' specification for statement(s) on \
             line(s): %a, @\nAssuming that they can call '%a'"
            Kernel_function.pretty kf
            (Pretty_utils.pp_list ~sep:", " Cil_datatype.Location.pretty_line)
            warning_locs
            Kernel_function.pretty kf ;
        if is_recursive kf then
          (* Notes:
             - a recursive function never trivially terminates,
             - in absence of decreases, CfgCalculus will warn *)
          begin match CfgAnnot.get_decreases_goal kf with
            | None -> infos
            | Some (id, _) ->
              let deps =
                Pset.add (WpPropId.property_of_id id) infos.terminates_deps
              in
              { infos with terminates_deps = deps }
          end
        else if infos.calls = Fset.empty
             && infos.no_variant_loops = Sset.empty then begin
          set_trivially_terminates id infos.terminates_deps ;
          (* Drop dependencies for this terminates, we've used it. *)
          { infos with terminates_deps = Pset.empty }
        end
        else infos
      | _ -> infos
    else infos
  in
  (* Collected Infos *)
  infos

(* -------------------------------------------------------------------------- *)
(* --- Memoization Data                                                   --- *)
(* -------------------------------------------------------------------------- *)

module Generator = WpContext.StaticGenerator(Key)
    (struct
      type key = Key.t
      type data = t
      let name = "Wp.CfgInfos.Generator"
      let compile = compile
    end)

let get kf ?(smoking=false) ?(bhv=[]) ?(prop=[]) () =
  Generator.get { kf ; smoking ; bhv ; prop }

let clear () = Generator.clear ()

(* -------------------------------------------------------------------------- *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct