package frama-c

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

Source file RegionAccess.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
(**************************************************************************)
(*                                                                        *)
(*  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 Layout
open Region

(* -------------------------------------------------------------------------- *)
(* --- Location Compiler                                                  --- *)
(* -------------------------------------------------------------------------- *)

type addr = {
  addrof : Region.region ;
  typeOfPointed : typ ;
  shift : bool ;
}

type value =
  | Pure
  | Read_at of typ * region
  | Addr_of of addr

[@@@ warning "-32"]
let pp_value fmt = function
  | Pure -> Format.pp_print_string fmt "scalar"
  | Read_at(_,r) -> Format.fprintf fmt "read %a" R.pretty r
  | Addr_of a ->
    if a.shift then
      Format.fprintf fmt "addr %a+" R.pretty a.addrof
    else
      Format.fprintf fmt "addr %a" R.pretty a.addrof
[@@@ warning "+32"]

(* -------------------------------------------------------------------------- *)
(* --- Strings                                                            --- *)
(* -------------------------------------------------------------------------- *)

let cc_string map exp =
  let cst = Pretty_utils.to_string Cil_datatype.Exp.pretty exp in
  let addrof = Region.of_cstring map ~eid:exp.eid ~cst in
  { addrof ; typeOfPointed = Cil.charType ; shift=false }

(* -------------------------------------------------------------------------- *)
(* --- Reading Values                                                     --- *)
(* -------------------------------------------------------------------------- *)

let read acs = function
  | Pure -> ()
  | Addr_of _ -> ()
  | Read_at(tr,r) ->
    acs_deref r (Value,tr) ;
    acs_read r acs

let points_to = function { shift ; addrof = pointed ; typeOfPointed = typ } ->
  acs_deref pointed ((if shift then Array else Deref),typ)

let addrof map = function
  | Pure -> failwith "Wp.Region: physical address"
  | Read_at(tr,r) ->
    acs_deref r (Value,tr) ;
    {
      addrof = add_pointed map r ;
      typeOfPointed = Cil.typeOf_pointed tr ;
      shift = false ;
    }
  | Addr_of addr -> addr

let cast ty value =
  if Cil.isPointerType ty then
    match value with
    | Addr_of addr ->
      Addr_of { addr with typeOfPointed = Cil.typeOf_pointed ty }
    | Read_at (_,r) -> Read_at(ty,r)
    | Pure -> Pure
  else
    value

let is_pointer_value = function
  | Pure -> false
  | Addr_of _ -> true
  | Read_at(tr,_) -> Cil.isPointerType tr

let merge_type t t' =
  if Cil.isVoidType t then t' else
  if Cil.isVoidType t' then t else
  if Cil_datatype.Typ.equal t t' then t
  else failwith "Wp.Region: merge incompatible pointer types"

let merge_addrof (map:map) v1 v2 =
  if not (is_pointer_value v1) then v2 else
  if not (is_pointer_value v2) then v1 else
    let a1 = addrof map v1 in
    let a2 = addrof map v2 in
    let typeOfPointed = merge_type a1.typeOfPointed a2.typeOfPointed in
    let addrof = Region.alias map a1.addrof a2.addrof in
    let shift = a1.shift || a2.shift in
    Addr_of { addrof ; typeOfPointed ; shift }

(* -------------------------------------------------------------------------- *)
(* --- Expressions & L-values                                             --- *)
(* -------------------------------------------------------------------------- *)

let rec cc_exp (map:map) exp =
  match exp.enode with
  | BinOp( (PlusPI | MinusPI) , a , b , _ ) ->
    cc_read map b ;
    let { addrof = pointed } as addr = cc_addr map a in
    acs_shift pointed (Eval exp) ;
    Addr_of { addr with shift = true }
  | AddrOf lv | StartOf lv ->
    Addr_of {
      addrof = cc_lval map lv ;
      typeOfPointed = Cil.typeOfLval lv ;
      shift = false ;
    }
  | Lval lv -> Read_at (Cil.typeOfLval lv , cc_lval map lv)
  | CastE(ty,e) -> cast ty (cc_exp map e)
  | Const (CStr _ | CWStr _) -> Addr_of (cc_string map exp)
  | Const (CInt64 _ | CChr _ | CEnum _ | CReal _)
  | SizeOf _ | SizeOfE _ | SizeOfStr _
  | AlignOf _ | AlignOfE _ -> Pure
  | UnOp(_,e,ty) ->
    assert (not (Cil.isPointerType ty)) ;
    cc_read map e ; Pure
  | BinOp(_,a,b,ty) ->
    assert (not (Cil.isPointerType ty)) ;
    cc_read map a ; cc_read map b ; Pure

and cc_host map = function
  | Var x -> of_cvar map x , x.vtype
  | Mem e ->
    let a = cc_addr map e in
    points_to a ; (* deref, not read !*)
    a.addrof , a.typeOfPointed

and cc_lval map (host , offset) =
  let r,ty = cc_host map host in cc_offset map r ty offset

and cc_offset map r ty = function
  | Cil_types.NoOffset -> r
  | Cil_types.Field(fd,ofs) ->
    let df = Offset.field fd in
    cc_offset map (add_offset map r df) fd.ftype ofs
  | Cil_types.Index(e,ofs) ->
    cc_read map e ;
    let de = Offset.index ty in
    let te = Offset.typeof de in
    cc_offset map (add_offset map r de) te ofs

and cc_addr map a = addrof map (cc_exp map a)

and cc_read map e = read (Eval e) (cc_exp map e)

and cc_comp map e =
  match cc_exp map e with
  | Pure | Addr_of _ -> failwith "Wp.Region: comp expected"
  | Read_at(_,r) -> r

let cc_writes map stmt tgt typ e =
  acs_deref tgt (Value,typ) ;
  acs_write tgt (Assigned stmt) ;
  match Cil.unrollType typ with
  | TPtr _ ->
    let a = cc_addr map e in
    points_to a ; (* deref, not read! *)
    do_alias map a.addrof (add_pointed map tgt)
  | TComp _ ->
    let src = cc_comp map e in
    acs_copy ~src ~tgt
  | _ ->
    cc_read map e

let cc_assign map stmt lv e =
  cc_writes map stmt (cc_lval map lv) (Cil.typeOfLval lv) e

let cc_return map stmt e =
  cc_writes map stmt (Region.of_return map) (Cil.typeOf e) e

(* -------------------------------------------------------------------------- *)
(* ---  Stmt & Instructions                                               --- *)
(* -------------------------------------------------------------------------- *)

let rec cc_init map stmt lv = function
  | SingleInit e -> cc_assign map stmt lv e
  | CompoundInit(_,content) ->
    List.iter
      (fun (ofs,vi) ->
         cc_init map stmt (Cil.addOffsetLval ofs lv) vi
      ) content

let cc_local_init map stmt x = function
  | AssignInit vi -> cc_init map stmt (Var x,NoOffset) vi
  | ConsInit _ -> failwith "Wp.Region: cons-init not implemented"

let cc_instr map stmt = function
  | Set(lv,e,_) -> cc_assign map stmt lv e
  | Call _ -> failwith "Wp.Region: call not implemented"
  | Local_init(x,vi,_) -> cc_local_init map stmt x vi
  | Asm _ | Skip _ | Code_annot _ -> ()

let cc_skind map stmt =
  match stmt.skind with
  | Instr instr -> cc_instr map stmt instr
  | Return(Some ve,_) -> cc_return map stmt ve
  | If(e,_,_,_) -> cc_read map e
  | Switch(e,_,_,_) -> cc_read map e

  | Return(None,_) | Goto _ | Break _ | Continue _ | Loop _
  | Block _ | UnspecifiedSequence _
  | Throw _ | TryCatch _ | TryFinally _ | TryExcept _ -> ()

(* -------------------------------------------------------------------------- *)
(* --- ACSL Terms                                                         --- *)
(* -------------------------------------------------------------------------- *)

let rec cc_term map t = read (Tval t) (cc_term_value map t)

and cc_term_value (map:map) (term:term) =
  match term.term_node with
  | TLval lv ->
    begin match cc_term_lval map lv with
      | None -> Pure
      | Some(ty,reg) -> Read_at(ty,reg)
    end
  | TAddrOf lv | TStartOf lv ->
    begin match cc_term_lval map lv with
      | None -> failwith "Wp.Region: pure term-value"
      | Some(ty,reg) -> Addr_of {
          addrof = reg ;
          typeOfPointed = ty ;
          shift = false ;
        }
    end
  | TBinOp( (PlusPI | MinusPI) , a , b ) ->
    begin
      cc_term map b ;
      let { addrof = pointed } as addr = cc_term_addr map a in
      acs_shift pointed (Tval term) ;
      Addr_of { addr with shift = true }
    end

  | Tnull ->
    Addr_of {
      addrof = Region.of_null map ;
      typeOfPointed = Cil.charType ;
      shift = false ;
    }

  | TUnOp(_,a) -> cc_term map a ; Pure
  | TBinOp(_,a,b) -> cc_term map a ; cc_term map b ; Pure

  | Tat(t,_) -> cc_term_value map t

  | TCast (_, Ctype ty,t) -> cast ty @@ cc_term_value map t
  | TCast (true, _,t) -> cc_term_value map t
  | TCast (false, _,_) -> assert false

  | TConst _
  | TSizeOf _ | TSizeOfE _ | TSizeOfStr _
  | TAlignOf _ | TAlignOfE _ | Ttype _ | Ttypeof _
    -> Pure

  | TDataCons(_,ts) -> List.iter (cc_term map) ts ; Pure
  | TUpdate(w,ofs,v) ->
    cc_term map w ;
    cc_term map v ;
    cc_term_offset_read map ofs ;
    Pure

  | Tbase_addr(_at,t) -> cast Cil.voidPtrType @@ cc_term_value map t
  | Tblock_length(_at,t) | Toffset(_at,t) -> cc_term map t ; Pure

  | Tif(c,a,b) ->
    cc_term map c ;
    merge_addrof map (cc_term_value map a) (cc_term_value map b)

  | Tempty_set -> Pure
  | Tunion ts | Tinter ts ->
    List.fold_left
      (fun v t -> merge_addrof map v (cc_term_value map t)) Pure ts

  | Tcomprehension(t,_,None) -> cc_term_value map t
  | Tcomprehension(t,_,Some p) -> cc_pred map p ; cc_term_value map t
  | Trange(a,b) -> cc_term_option map a ; cc_term_option map b ; Pure

  | Tlet _ | Tlambda _ | Tapp _ ->
    failwith "Wp.Region: unsupported logic functions and bindings"

and cc_term_lval map (lhost,loffset) =
  match lhost with
  | TResult typ -> Some(typ,of_return map)
  | TVar lvar ->
    begin
      match lvar.lv_origin with
      | Some x ->
        let ty,rv = cc_term_offset map (of_cvar map x) x.vtype loffset in
        Some(ty,rv)
      | None ->
        cc_term_offset_read map loffset ;
        None
    end
  | TMem p ->
    begin
      let a = cc_term_addr map p in
      points_to a ;
      let ty,ra = cc_term_offset map a.addrof a.typeOfPointed loffset in
      Some(ty,ra)
    end

and cc_term_offset map r ty = function
  | TNoOffset -> ty,r
  | TField(fd,ofs) ->
    let df = Offset.field fd in
    cc_term_offset map (add_offset map r df) fd.ftype ofs
  | TIndex(t,ofs) ->
    cc_term map t ;
    let de = Offset.index ty in
    let te = Offset.typeof de in
    cc_term_offset map (add_offset map r de) te ofs
  | TModel _ -> failwith "Wp.Region: model field"

and cc_term_offset_read map = function
  | TNoOffset -> ()
  | TField(_,ofs) -> cc_term_offset_read map ofs
  | TModel(_,ofs) -> cc_term_offset_read map ofs
  | TIndex(t,ofs) -> cc_term map t ; cc_term_offset_read map ofs

and cc_term_addr map t = addrof map @@ cc_term_value map t

and cc_term_option map = function None -> () | Some t -> cc_term map t

(* -------------------------------------------------------------------------- *)
(* --- ACSL Predicates                                                    --- *)
(* -------------------------------------------------------------------------- *)

and cc_pred (map:map) (p:predicate) =
  match p.pred_content with
  | Pfalse | Ptrue -> ()

  | Prel(_,a,b) ->
    cc_term map a ; cc_term map b

  | Pnot a -> cc_pred map a
  | Pif(t,a,b) ->
    cc_term map t ; cc_pred map a ; cc_pred map b
  | Pand(a,b) | Por(a,b) | Pxor(a,b) | Pimplies(a,b) | Piff(a,b) ->
    cc_pred map a ; cc_pred map b

  | Pforall(_,p) | Pexists(_,p) -> cc_pred map p

  | Pseparated ts -> List.iter (cc_term map) ts
  | Pvalid(_,t) | Pvalid_read(_,t) | Pobject_pointer(_,t) | Pvalid_function t
  | Pinitialized(_,t) | Pdangling(_,t) | Pallocable(_,t)
  | Pfreeable(_,t) -> cc_term map t
  | Pfresh(_,_,ptr,n) -> cc_term map ptr ; cc_term map n

  | Pat(p,_at) -> cc_pred map p

  | Plet _ | Papp _ ->
    failwith "Wp.Region: unsupported logic predicates and bindings"

(* -------------------------------------------------------------------------- *)
(* --- ACSL Spec & Defs                                                   --- *)
(* -------------------------------------------------------------------------- *)

class visitor map =
  object
    inherit Visitor.frama_c_inplace as super

    method! vpredicate p = cc_pred map p ; Cil.SkipChildren
    method! vterm t = cc_term map t ; Cil.SkipChildren
    method! vstmt s = cc_skind map s ; super#vstmt s
    (* vpredicate and vterm are called from vcode_annot *)

    (* speed up: skip non interesting subtrees *)
    method! vloop_pragma _ =  Cil.SkipChildren (* no need *)
    method! vvdec _ = Cil.SkipChildren (* done via stmt *)
    method! vexpr _ = Cil.SkipChildren (* done via stmt *)
    method! vlval _ = Cil.SkipChildren (* done via stmt *)
    method! vattr _ = Cil.SkipChildren (* done via stmt *)
    method! vinst _ =  Cil.SkipChildren (* done via stmt *)
  end

let cc_fundec map def =
  let visitor = new visitor map in
  ignore (Cil.visitCilFunction (visitor:>Cil.cilVisitor) def)

let cc_spec map spec =
  let visitor = new visitor map in
  ignore (Cil.visitCilFunspec (visitor:>Cil.cilVisitor) spec)

(* -------------------------------------------------------------------------- *)
(* --- L-path Iterator                                                    --- *)
(* -------------------------------------------------------------------------- *)

open RegionAnnot

let iter_star map f t r =
  let pointed = add_pointed map r in
  acs_deref pointed (Deref,t) ; f pointed

let iter_shift map f t r =
  let pointed = add_pointed map r in
  acs_deref pointed (Array,t) ; f r

let iter_index map f tarr r =
  f (add_offset map r (Offset.index tarr))

let iter_fields map f fds r =
  List.iter (fun fd -> f (add_offset map r (Offset.field fd))) fds

let rec iter_lpath map f lv =
  match lv.lnode with
  | L_var x -> f (of_cvar map x)
  | L_region a -> f (of_name map a)
  | L_cast(_,a) -> iter_lpath map f a
  | L_addr a -> iter_lpath map (fun r -> f (get_addrof map r)) a
  | L_star(te,a) -> iter_lpath map (iter_star map f te) a
  | L_shift(a,te,_) -> iter_lpath map (iter_shift map f te) a
  | L_index(a,_,_) -> iter_lpath map (iter_index map f lv.ltype) a
  | L_field(a,fs) -> iter_lpath map (iter_fields map f fs) a

(* -------------------------------------------------------------------------- *)
(* --- Region Specs                                                       --- *)
(* -------------------------------------------------------------------------- *)

let cc_lpath map rclass _rpattern lv =
  iter_lpath map (Region.add_alias map ~into:rclass) lv

let cc_region map spec =
  let rclass = Region.of_class map spec.region_name in
  let rpattern = spec.region_pattern in
  List.iter (cc_lpath map rclass rpattern) spec.region_lpath

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