package frama-c

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

Source file cfgGenerator.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
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Wp_parameters

(* -------------------------------------------------------------------------- *)
(* --- Task Manager                                                       --- *)
(* -------------------------------------------------------------------------- *)

module KFmap = Kernel_function.Map

type pool = {
  mutable modes: CfgCalculus.mode list KFmap.t ;
  mutable props: CfgCalculus.props ;
  mutable lemmas: LogicUsage.logic_lemma list ;
}

let empty () = {
  lemmas = [];
  modes = KFmap.empty;
  props = `All;
}

let get_kf_infos model kf ?bhv ?prop () =
  let missing = WpRTE.missing_guards model kf in
  if missing && Wp_parameters.RTE.get () then
    WpRTE.generate model kf ;
  let smoking =
    Wp_parameters.SmokeTests.get () &&
    Wp_parameters.SmokeDeadcode.get () in
  let infos = CfgInfos.get kf ~smoking ?bhv ?prop () in
  (*TODO: print warning first *)
  if missing then
    Wp_parameters.warning ~current:false ~once:true "Missing RTE guards" ;
  infos

(* -------------------------------------------------------------------------- *)
(* --- Target preparation                                                 --- *)
(* -------------------------------------------------------------------------- *)

let prepare_ip model ip =
  Option.iter (WpTarget.compute_kf model) @@ Property.get_kf ip

let prepare_main model ?fct ?bhv ?prop () =
  WpTarget.compute model ?fct ?bhv ?prop ()

(* -------------------------------------------------------------------------- *)
(* --- Behavior Selection                                                 --- *)
(* -------------------------------------------------------------------------- *)

let empty_default_behavior : funbehavior = {
  b_name = Cil.default_behavior_name ;
  b_requires = [] ;
  b_assumes = [] ;
  b_post_cond = [] ;
  b_assigns = WritesAny ;
  b_allocation = FreeAllocAny ;
  b_extended = [] ;
}

let default kf =
  match Annotations.behaviors kf with
  | [] -> [empty_default_behavior]
  | bhvs -> List.filter Cil.is_default_behavior bhvs

let select kf bnames =
  match Annotations.behaviors kf with
  | [] -> if bnames = [] then [empty_default_behavior] else []
  | bhvs -> if bnames = [] then bhvs else
      List.filter
        (fun b -> List.mem b.b_name bnames)
        bhvs

(* -------------------------------------------------------------------------- *)
(* --- Elementary Tasks                                                   --- *)
(* -------------------------------------------------------------------------- *)

let add_lemma_task pool ?(prop=[]) (l : LogicUsage.logic_lemma) =
  if Logic_utils.verify_predicate l.lem_predicate.tp_kind &&
     (prop=[] || WpPropId.select_by_name prop (WpPropId.mk_lemma_id l))
  then pool.lemmas <- l :: pool.lemmas

let add_fun_task model pool ~kf ?infos ?bhvs ?target () =
  let infos = match infos with
    | Some infos -> infos
    | None -> get_kf_infos model kf () in
  let bhvs = match bhvs with
    | Some bhvs -> bhvs
    | None ->
      let bhvs = Annotations.behaviors kf in
      if List.exists (Cil.is_default_behavior) bhvs then bhvs
      else empty_default_behavior :: bhvs in
  let add_mode kf m =
    let ms = try KFmap.find kf pool.modes with Not_found -> [] in
    pool.modes <- KFmap.add kf (m :: ms) pool.modes in
  begin
    List.iter (fun bhv -> add_mode kf CfgCalculus.{ infos ; kf ; bhv }) bhvs ;
    Option.iter (fun ip -> pool.props <- `PropId ip) target ;
  end

let notyet prop =
  let source = fst (Property.location prop) in
  Wp_parameters.warning ~once:true ~source
    "Not yet implemented wp for '%a'" Property.pretty prop

(* -------------------------------------------------------------------------- *)
(* --- Property Tasks                                                     --- *)
(* -------------------------------------------------------------------------- *)

let rec strategy_ip model pool target =
  let open Property in
  match target with
  | IPLemma { il_name } ->
    add_lemma_task pool (LogicUsage.logic_lemma il_name)
  | IPAxiomatic { iax_props } ->
    List.iter (strategy_ip model pool) iax_props
  | IPBehavior { ib_kf = kf ; ib_bhv = bhv } ->
    add_fun_task model pool ~kf ~bhvs:[bhv] ()
  | IPPredicate { ip_kf = kf ; ip_kind ; ip_kinstr = ki } ->
    begin match ip_kind with
      | PKAssumes _ -> ()
      | PKRequires bhv ->
        begin
          match ki with
          | Kglobal -> (*TODO*) notyet target
          | Kstmt _ -> add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
        end
      | PKEnsures(bhv,_) ->
        add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
      | PKTerminates ->
        add_fun_task model pool ~kf ~bhvs:(default kf) ~target ()
    end
  | IPDecrease { id_kf = kf } ->
    add_fun_task model pool ~kf ~bhvs:(default kf) ~target ()
  | IPAssigns { ias_kf=kf ; ias_bhv=Id_loop ca }
  | IPAllocation { ial_kf=kf ; ial_bhv=Id_loop ca } ->
    let bhvs = match ca.annot_content with
      | AAssigns(bhvs,_) | AAllocation(bhvs,_) -> bhvs
      | _ -> [] in
    add_fun_task model pool ~kf ~bhvs:(select kf bhvs) ~target ()
  | IPAssigns { ias_kf=kf ; ias_bhv=Id_contract(_,bhv) }
  | IPAllocation { ial_kf=kf ; ial_bhv=Id_contract(_,bhv) }
    -> add_fun_task model pool ~kf ~bhvs:[bhv] ~target ()
  | IPCodeAnnot { ica_kf = kf ; ica_ca = ca } ->
    begin match ca.annot_content with
      | AExtended _ | APragma _ -> ()
      | AStmtSpec(fors,_) ->
        (*TODO*) notyet target ;
        add_fun_task model pool ~kf ~bhvs:(select kf fors) ()
      | AVariant _ ->
        add_fun_task model pool ~kf ~target ()
      | AAssert(fors, _)
      | AInvariant(fors, _, _)
      | AAssigns(fors, _)
      | AAllocation(fors, _) ->
        add_fun_task model pool ~kf ~bhvs:(select kf fors) ~target ()
    end
  | IPComplete _ -> (*TODO*) notyet target
  | IPDisjoint _ -> (*TODO*) notyet target
  | IPFrom _ | IPReachable _ | IPTypeInvariant _ | IPGlobalInvariant _
  | IPPropertyInstance _ -> notyet target (* ? *)
  | IPExtended _ | IPOther _ -> ()

(* -------------------------------------------------------------------------- *)
(* --- Function Strategy Tasks                                            --- *)
(* -------------------------------------------------------------------------- *)

let strategy_main model pool ?(fct=Fct_all) ?(bhv=[]) ?(prop=[]) () =
  begin
    if fct = Fct_all && bhv = [] then
      LogicUsage.iter_lemmas (add_lemma_task pool ~prop) ;
    Wp_parameters.iter_fct
      (fun kf ->
         let infos = get_kf_infos model kf ~bhv ~prop () in
         if CfgInfos.annots infos then
           if bhv=[]
           then add_fun_task model pool ~infos ~kf ()
           else add_fun_task model pool ~infos ~kf ~bhvs:(select kf bhv) ()
      ) fct ;
    pool.props <- (if prop=[] then `All else `Names prop);
  end

(* -------------------------------------------------------------------------- *)
(* --- Compute All Tasks                                                  --- *)
(* -------------------------------------------------------------------------- *)

module Make(VCG : CfgWP.VCgen) =
struct

  module WP = CfgCalculus.Make(VCG)

  let compute model pool =
    begin
      let collection = ref Bag.empty in
      Lang.F.release () ;
      if pool.lemmas <> [] then
        WpContext.on_context (model,WpContext.Global)
          begin fun () ->
            LogicUsage.iter_lemmas
              (fun (l : LogicUsage.logic_lemma) ->
                 if Logic_utils.use_predicate l.lem_predicate.tp_kind
                 then VCG.register_lemma l) ;
            List.iter
              (fun (l : LogicUsage.logic_lemma) ->
                 if Logic_utils.verify_predicate l.lem_predicate.tp_kind then
                   let wpo = VCG.compile_lemma l in
                   collection := Bag.add wpo !collection
              ) pool.lemmas ;
          end () ;
      KFmap.iter
        (fun kf modes ->
           List.iter
             begin fun (mode: CfgCalculus.mode) ->
               WpContext.on_context (model,WpContext.Kf kf)
                 begin fun () ->
                   if Kernel_function.is_entry_point kf &&
                      not @@ Kernel_function.is_not_called kf
                   then
                     Wp_parameters.error
                       "Main entry point function '%a' is (potentially) \
                        recursive.@\n\
                        This case is not supported yet \
                        (skipped verification)."
                       Kernel_function.pretty kf
                   else
                     begin
                       (* ensures lemmas are already compiled in context *)
                       LogicUsage.iter_lemmas
                         (fun (l : LogicUsage.logic_lemma) ->
                            if Logic_utils.use_predicate l.lem_predicate.tp_kind
                            then VCG.register_lemma l) ;
                       let bhv =
                         if Cil.is_default_behavior mode.bhv then None
                         else Some mode.bhv.b_name in
                       let index = Wpo.Function(kf,bhv) in
                       let props = pool.props in
                       try
                         let wp = WP.compute ~mode ~props in
                         let wcs = VCG.compile_wp index wp in
                         collection := Bag.concat !collection wcs
                       with WP.NonNaturalLoop loc ->
                         Wp_parameters.error
                           ~source:(fst loc)
                           "Non-natural loop detected in function '%a'.@\n\
                            This case is not supported yet \
                            (skipped verification)."
                           Kernel_function.pretty kf
                     end
                 end ()
             end
             (List.rev modes)
        ) pool.modes ;
      CfgAnnot.clear () ;
      CfgInfos.clear () ;
      !collection
    end

  let compute_ip model ip =
    prepare_ip model ip ;
    let pool = empty () in
    strategy_ip model pool ip ;
    compute model pool

  let compute_call _model _stmt =
    Wp_parameters.warning
      ~once:true "Not yet implemented call preconds" ;
    Bag.empty

  let compute_main model ?fct ?bhv ?prop () =
    prepare_main model ?fct ?bhv ?prop () ;
    let pool = empty () in
    strategy_main model pool ?fct ?bhv ?prop () ;
    compute model pool

end

(* -------------------------------------------------------------------------- *)
(* --- New WP Computer (main entry points)                                --- *)
(* -------------------------------------------------------------------------- *)

let generators = WpContext.MINDEX.create 1

let generator setup driver =
  let model = Factory.instance setup driver in
  try WpContext.MINDEX.find generators model
  with Not_found ->
    let module VCG = (val CfgWP.vcgen setup driver) in
    let module CC = Make(VCG) in
    let generator : Wpo.generator =
      object
        method model = model
        method compute_ip = CC.compute_ip model
        method compute_call = CC.compute_call model
        method compute_main = CC.compute_main model
      end in
    WpContext.MINDEX.add generators model generator ;
    generator

(* -------------------------------------------------------------------------- *)
(* --- Dumper                                                             --- *)
(* -------------------------------------------------------------------------- *)

let dump pool =
  let module WP = CfgCalculus.Make(CfgDump) in
  let props = pool.props in
  KFmap.iter
    (fun _ modes ->
       List.iter
         begin fun (mode : CfgCalculus.mode) ->
           let bhv =
             if Cil.is_default_behavior mode.bhv
             then None else Some mode.bhv.b_name in
           try
             CfgDump.fopen mode.kf bhv ;
             ignore (WP.compute ~mode ~props) ;
             CfgDump.flush () ;
           with err ->
             CfgDump.flush () ;
             raise err
         end
         (List.rev modes)
    ) pool.modes

let dumper setup driver =
  let model = Factory.instance setup driver in
  let generator : Wpo.generator =
    object
      method model = model
      method compute_ip ip =
        prepare_ip model ip ;
        let pool = empty () in
        strategy_ip model pool ip ;
        dump pool ; Bag.empty
      method compute_call _ = Bag.empty
      method compute_main ?fct ?bhv ?prop () =
        prepare_main model ?fct ?bhv ?prop () ;
        let pool = empty () in
        strategy_main model pool ?fct ?bhv ?prop () ;
        dump pool ; Bag.empty
    end
  in generator

(* -------------------------------------------------------------------------- *)
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