package frama-c

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

Source file Pcfg.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
(**************************************************************************)
(*                                                                        *)
(*  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 Lang
open Lang.F
open Sigs

(* -------------------------------------------------------------------------- *)
(* --- State Registry                                                     --- *)
(* -------------------------------------------------------------------------- *)

type label = {
  id : int ; (* index in the sequent, unique *)
  name : string ; (* (almost) unique *)
  state : Mstate.state ;
  mutable flag : bool ;
  mutable prev : label list ;
  mutable next : label list ;
}

type value =
  | Term
  | Addr of s_lval
  | Lval of s_lval * label
  | Init of s_lval * label
  | Chunk of string * label

module Imap = Datatype.Int.Map

type env = {
  mutable kid : int ; (* counter for anonymous labels *)
  mutable cfg : label list ; (* sorted by dominators *)
  mutable values : value Tmap.t ; (* cache *)
  mutable labels : label Imap.t ;
}

let label env ~id ?stmt ?descr state =
  let name =
    let open Cil_types in
    match descr , stmt with
    | Some lbl , _ -> lbl
    | None , Some { labels = Label(lbl,_,_) :: _ } -> lbl
    | _ -> env.kid <- succ env.kid ; Printf.sprintf "L%d" env.kid
  in
  { id ; name ; state ; flag = false ; prev = [] ; next = [] }

let insert env label =
  begin
    env.labels <- Imap.add label.id label env.labels ;
    env.cfg <- label :: env.cfg ;
  end

let create () = {
  kid = 0 ; cfg = [] ;
  values = Tmap.empty ;
  labels = Imap.empty ;
}

let at env ~id = Imap.find id env.labels
let flag lbl = lbl.flag <- true ; lbl
let visible lbl = lbl.flag

let rec find env e =
  try Tmap.find e env.values
  with Not_found ->
    env.values <- Tmap.add e Term env.values ;
    if F.is_primitive e then Term else
      let v = lookup env e env.cfg in
      env.values <- Tmap.add e v env.values ; v

and lookup env e = function
  | [] -> Term
  | lbl :: others ->
    try match Mstate.lookup lbl.state e with
      | Sigs.Mterm -> raise Not_found
      | Sigs.Maddr lv -> Addr lv
      | Sigs.Mlval (lv, KValue) -> Lval(lv,flag lbl)
      | Sigs.Mlval (lv, KInit) -> Init(lv,flag lbl)
      | Sigs.Mchunk (m, _) -> Chunk(m,flag lbl)
    with Not_found -> lookup env e others

let is_ref x k = (k == F.e_zero) && Cil.isPointerType x.vtype
let is_atomic = function
  | Mvar x , [Mindex k] -> is_ref x k
  | Mvar _ , [] -> true
  | _ -> false

let iter f lbl = Mstate.iter f lbl.state

let is_copy env lbl = function
  | Sigs.Mstore( lv , value ) ->
    begin
      match find env value with
      | Lval(lv0,lbl0) -> lbl0 == lbl && Mstate.equal lv lv0
      | _ -> false
    end

let updates env seq vars =
  Bag.filter
    (fun upd -> not (is_copy env seq.pre upd))
    (Mstate.updates { pre = seq.pre.state ; post = seq.post.state } vars)

(* -------------------------------------------------------------------------- *)
(* --- Label Control Flow                                                 --- *)
(* -------------------------------------------------------------------------- *)

let prev lbl = lbl.prev
let next lbl = lbl.next
let branching = function { next = [_] } -> false | _ -> true

let sequence_point a b =
  if a != b then
    match a,b with
    | Some p , Some q ->
      if not (List.memq q p.next) then p.next <- q :: p.next ;
      if not (List.memq p q.prev) then q.prev <- p :: q.prev ;
    | None , _ | _ , None -> ()

let rec control env prev sequence next =
  ignore (ctrl env prev (Conditions.list sequence) next)

and ctrl env prev steps next = match steps with
  | [] -> next
  | s :: others ->
    let open Conditions in
    match s.condition with
    | Type _ | Have _ | When _ | Core _ | Init _ | Probe _ ->
      (* Sequence of Labels on Hyp *)
      ctrl env prev others next
    | Branch(_,cthen,celse) ->
      let next = ctrl env None others next in
      control env prev cthen next ;
      control env prev celse next ;
      None
    | Either cases ->
      let next = ctrl env None others next in
      List.iter (fun s -> control env prev s next) cases ;
      None
    | State _ ->
      try
        let here = Some (at env ~id:s.id) in
        sequence_point prev here ;
        let next = ctrl env here others next in
        sequence_point here next ;
        here
      with Not_found ->
        ctrl env prev others next

(* -------------------------------------------------------------------------- *)
(* --- Priority Queue                                                     --- *)
(* -------------------------------------------------------------------------- *)

let register seq =
  ignore (Conditions.steps seq) ;
  let env = create () in
  let queue = Queue.create () in
  let push s = Queue.add s queue in
  let pop () = try Some (Queue.pop queue) with Queue.Empty -> None in
  let api = ref [] in (* Pre & Post *)
  let cfg = ref [] in (* Other labels *)
  let pool = function Some ("Pre"|"Post") -> api | _ -> cfg in
  let rec compile seq =
    Conditions.iter
      (fun s ->
         let open Conditions in
         match s with
         | { id ; stmt ; descr ; condition = State m } ->
           let label = label env ~id ?stmt ?descr m in
           let r = pool descr in r := label :: !r
         | { condition = Type _ | Have _ | When _ | Core _ | Init _ | Probe _ } -> ()
         | { condition = Branch(_,cthen,celse) } -> push cthen ; push celse
         | { condition = Either cases } -> List.iter push cases
      ) seq ;
    match pop () with Some s -> compile s | None -> ()
  in compile seq ;
  let insert = insert env in
  List.iter insert !cfg ; List.iter insert !api ;
  control env None seq None ; env

(* -------------------------------------------------------------------------- *)
(* --- Pretty Printer                                                     --- *)
(* -------------------------------------------------------------------------- *)

class virtual engine =
  object(self)

    method virtual pp_atom : Format.formatter -> F.term -> unit
    method virtual pp_flow : Format.formatter -> F.term -> unit

    (* --- L-Values --- *)

    method is_atomic_lv = is_atomic

    method pp_ofs fmt = function
      | Mfield fd -> Format.fprintf fmt ".%s@," fd.fname
      | Mindex k -> Format.fprintf fmt "[%a]@," self#pp_flow k

    method pp_offset fmt fs = List.iter (self#pp_ofs fmt) fs

    method pp_host fmt = function
      | Sigs.Mvar x -> Format.pp_print_string fmt x.vname
      | Sigs.Mmem p -> self#pp_atom fmt p
      | Sigs.Mval lv -> self#pp_lval fmt lv

    method pp_lval fmt = function
      | Mvar x , [] ->
        Format.pp_print_string fmt x.vname
      | Mvar x , [Mindex k] when is_ref x k ->
        Format.fprintf fmt "*%s" x.vname
      | Mvar x , ofs ->
        Format.fprintf fmt "@[<hov 2>%s%a@]" x.vname self#pp_offset ofs
      | host , [] ->
        Format.fprintf fmt "*%a" self#pp_host host
      | host , Mfield fd :: ofs ->
        Format.fprintf fmt "@[<hov 2>%a@,->%s%a@]"
          self#pp_host host fd.fname self#pp_offset ofs
      | host , ((Mindex _ :: _) as ofs) ->
        Format.fprintf fmt "@[<hov 2>%a@,%a@]"
          self#pp_host host self#pp_offset ofs

    method pp_init fmt lv =
      Format.fprintf fmt "initialized(%a)" self#pp_lval lv

    method pp_addr fmt = function
      | Mvar x , [] -> Format.fprintf fmt "&%s" x.vname
      | Mmem p , [] -> self#pp_atom fmt p
      | Mmem p , [Mindex k] ->
        Format.fprintf fmt "%a + %a" self#pp_atom p self#pp_atom k
      | lv -> Format.fprintf fmt "&(%a)" self#pp_lval lv

    method pp_label fmt lbl =
      Format.pp_print_string fmt lbl.name

    method pp_chunk fmt m = Format.fprintf fmt "µ:%s" m

  end

open Sigs

let rec lv_iter f (h,ofs) = host_iter f h ; List.iter (ofs_iter f) ofs
and host_iter f = function Mvar _ -> () | Mmem e -> f e | Mval lv -> lv_iter f lv
and ofs_iter f = function Mfield _ -> () | Mindex e -> f e

let subterms env f e =
  match find env e with
  | Term -> false
  | Chunk _ -> true
  | Addr lv | Lval(lv,_) | Init(lv,_) -> lv_iter f lv ; true
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