package frama-c

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

Source file MemMemory.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Memory Model                                                       --- *)
(* -------------------------------------------------------------------------- *)

open Lang
open Lang.F

module L = Qed.Logic

let library = "memory"

let a_addr = Lang.datatype ~library "addr"
let t_addr = L.Data(a_addr,[])
let f_base   = Lang.extern_f ~library ~result:L.Int
    ~link:(Qed.Engine.F_subst ("base", "%1.base")) "base"
let f_offset = Lang.extern_f ~library ~result:L.Int
    ~link:(Qed.Engine.F_subst ("offset", "%1.offset")) "offset"
let f_shift  = Lang.extern_f ~library ~result:t_addr "shift"
let f_global = Lang.extern_f ~library ~result:t_addr ~category:L.Injection "global"
let f_null   = Lang.extern_f ~library ~result:t_addr "null"

let a_table = Lang.datatype ~library "table"
let t_table = L.Data(a_table,[])

let f_table_of_base = Lang.extern_f ~library
    ~category:Qed.Logic.Function ~result:t_table "table_of_base"

let f_table_to_offset = Lang.extern_f ~library
    ~category:Qed.Logic.Injection ~result:L.Int "table_to_offset"

let ty_fst_arg = function
  | Some l :: _ -> l
  | _ -> raise Not_found

let l_havoc = Qed.Engine.F_call "havoc"
let l_set_init = Qed.Engine.F_call "set_init"

let p_valid_rd = Lang.extern_fp ~library "valid_rd"
let p_valid_rw = Lang.extern_fp ~library "valid_rw"
let p_valid_obj = Lang.extern_fp ~library "valid_obj"
let p_invalid = Lang.extern_fp ~library "invalid"
let p_separated = Lang.extern_fp ~library "separated"
let p_included = Lang.extern_fp ~library "included"
let p_eqmem = Lang.extern_fp ~library "eqmem"
let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
let f_region = Lang.extern_f ~coloring:true ~library ~result:L.Int "region" (* base -> region *)
let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
let p_linked = Lang.extern_fp ~coloring:true ~library "linked" (* allocation-table -> prop *)
let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
let f_set_init =
  Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
let p_cinits = Lang.extern_fp ~coloring:true ~library "cinits" (* initializaton-table -> prop *)
let p_is_init_r = Lang.extern_fp ~library "is_init_range"
let p_monotonic = Lang.extern_fp ~library "monotonic_init"

let f_addr_of_int = Lang.extern_f
    ~category:L.Injection
    ~library ~result:t_addr "addr_of_int"

let f_int_of_addr = Lang.extern_f
    ~category:L.Injection
    ~library ~result:L.Int "int_of_addr"

(* -------------------------------------------------------------------------- *)
(* --- Utilities                                                          --- *)
(* -------------------------------------------------------------------------- *)

let t_mem t = L.Array(t_addr,t)
let t_malloc = L.Array(L.Int,L.Int)
let t_init = L.Array(t_addr,L.Bool)

let a_null = F.constant (e_fun f_null [])
let a_base p = e_fun f_base [p]
let a_offset p = e_fun f_offset [p]
let a_global b = e_fun f_global [b]
let a_shift l k = e_fun f_shift [l;k]
let a_addr b k = a_shift (a_global b) k
let a_base_offset b k =
  let offset_index = e_fun f_table_of_base [b] in
  e_fun f_table_to_offset [offset_index ; k]

(* -------------------------------------------------------------------------- *)
(* --- Qed Simplifiers                                                    --- *)
(* -------------------------------------------------------------------------- *)

(*
    Pointer arithmetic for structure access and array access could be
    defined directly using the record [{ base = p.base; offset = p.offset
    + c*i + c' }]. However that gives very bad triggers for the memory
    model axiomatization, so `shift p (c*i+c')` was used instead. It is
    not sufficient for user axiomatisation because memory access in
    axioms require trigger with arithmetic operators which is badly
    handled by provers. So for each c and c', ie for each kind of
    structure access and array access a specific function is used
    `shift_xxx`.

    Moreover no simplification of `shift_xxx` is done for keeping the
    same terms in axioms and the goal. `base` and `offset` function
    simplify all the `shift_xxx` because it seems they don't appear
    often in axioms and they are useful for simplifying `separated`,
    `assigns` and pointer comparisons in goals.

    To sum up memory access should match, but not `\base`, `\offset`,
    `\separated`, ...
*)

type addr_builtin = {
  base: term list -> term ;
  offset: term list -> term ;
}

module ADDR_BUILTIN = WpContext.Static
    (struct
      type key = lfun
      type data = addr_builtin
      let name = "MemMemory.ADDR_BUILTIN"
      include Lang.Fun
    end)

let phi_base l =
  match F.repr l with
  | L.Fun(f,[p;_]) when f==f_shift -> a_base p
  | L.Fun(f,[b]) when f==f_global -> b
  | L.Fun(f,[]) when f==f_null -> e_zero
  | L.Fun(f,args) -> (ADDR_BUILTIN.find f).base args
  | _ -> raise Not_found

let phi_offset l = match F.repr l with
  | L.Fun(f,[p;k]) when f==f_shift -> e_add (a_offset p) k
  | L.Fun(f,_) when f==f_global || f==f_null -> F.e_zero
  | L.Fun(f,args) -> (ADDR_BUILTIN.find f).offset args
  | _ -> raise Not_found

let phi_shift f p i =
  match F.repr p with
  | L.Fun(g,[q;j]) when f == g -> F.e_fun f [q;F.e_add i j]
  | _ -> raise Not_found

let eq_shift a b =
  let p = a_base a in
  let q = a_base b in
  let i = a_offset a in
  let j = a_offset b in
  if i==j then F.p_equal p q else
    match F.is_equal p q with
    | L.No -> F.p_false
    | L.Yes -> F.p_equal i j
    | L.Maybe -> raise Not_found

let eq_shift_gen phi a b =
  try phi a b with Not_found -> eq_shift a b

let nop _ = raise Not_found

let register ?(base=nop) ?(offset=nop) ?equal ?(linear=false) lfun =
  begin
    if base != nop || offset != nop then
      ADDR_BUILTIN.define lfun { base ; offset } ;
    if linear then
      F.set_builtin_2 lfun (phi_shift lfun) ;
    let phi_equal = match equal with
      | None -> eq_shift
      | Some phi -> eq_shift_gen phi
    in
    F.set_builtin_eqp lfun phi_equal ;
  end

(* -------------------------------------------------------------------------- *)
(* --- Simplifier for 'separated'                                         --- *)
(* -------------------------------------------------------------------------- *)

let r_separated = function
  | [p;a;q;b] ->
    if a == F.e_one && b == F.e_one then F.e_neq p q
    else
      begin
        let a_negative = F.e_leq a F.e_zero in
        let b_negative = F.e_leq b F.e_zero in
        if a_negative == e_true || b_negative == e_true then e_true else
          let bp = a_base p in
          let bq = a_base q in
          let open Qed.Logic in
          match F.is_true (F.e_eq bp bq) with
          | No -> e_true (* Have S *)
          | Yes when (a_negative == e_false && b_negative == e_false) ->
            (* Reduced to S *)
            let p_ofs = a_offset p in
            let q_ofs = a_offset q in
            let p_ofs' = F.e_add p_ofs a in
            let q_ofs' = F.e_add q_ofs b in
            F.e_or [ F.e_leq q_ofs' p_ofs ;
                     F.e_leq p_ofs' q_ofs ]
          | _ -> raise Not_found
      end
  | _ -> raise Not_found

let is_separated args = F.is_true (r_separated args)

(* -------------------------------------------------------------------------- *)
(* --- Simplifier for 'included'                                          --- *)
(* -------------------------------------------------------------------------- *)

(* See: tests/why3/test_memory.why

   logic a : int
   logic b : int

   predicate R = p.base = q.base
              /\ (q.offset <= p.offset)
              /\ (p.offset + a <= q.offset + b)

   predicate included = 0 < a -> ( 0 <= b and R )
   predicate a_empty = a <= 0
   predicate b_negative = b < 0

   lemma SAME_P: p=q -> (R <-> a<=b)
   lemma SAME_A: a=b -> (R <-> p=q)

   goal INC_P:  p=q -> (included <-> ( 0 < a -> a <= b )) (by SAME_P)
   goal INC_A:  a=b -> 0 < a -> (included <-> R) (by SAME_A)
   goal INC_1:  a_empty -> (included <-> true)
   goal INC_2:  b_negative -> (included <-> a_empty)
   goal INC_3:  not R -> (included <-> a_empty)
   goal INC_4:  not a_empty -> not b_negative -> (included <-> R)
*)

let r_included = function
  | [p;a;q;b] ->
    if F.e_eq p q == F.e_true
    then F.e_imply [F.e_lt F.e_zero a] (F.e_leq a b) (* INC_P *)
    else
    if (F.e_eq a b == F.e_true) && (F.e_lt F.e_zero a == F.e_true)
    then F.e_eq p q (* INC_A *)
    else
      begin
        let a_empty = F.e_leq a F.e_zero in
        let b_negative = F.e_lt b F.e_zero in
        if a_empty == F.e_true then F.e_true (* INC_1 *) else
        if b_negative == F.e_true then a_empty (* INC_2 *) else
          let bp = a_base p in
          let bq = a_base q in
          let open Qed.Logic in
          match F.is_true (F.e_eq bp bq) with
          | No -> a_empty (* INC_3 *)
          | Yes when (a_empty == e_false && b_negative == e_false) ->
            (* INC_4 *)
            let p_ofs = a_offset p in
            let q_ofs = a_offset q in
            if a == b then F.e_eq p_ofs q_ofs
            else
              let p_ofs' = e_add p_ofs a in
              let q_ofs' = e_add q_ofs b in
              e_and [ F.e_leq q_ofs p_ofs ; F.e_leq p_ofs' q_ofs' ]
          | _ -> raise Not_found
      end
  | _ -> raise Not_found

(* -------------------------------------------------------------------------- *)
(* --- Simplifier for 'havoc'                                             --- *)
(* -------------------------------------------------------------------------- *)

(* havoc(m_undef, havoc(_undef,m0,p0,a0), p1,a1) =
   - havoc(m_undef, m0, p1,a1) WHEN included (p1,a1,p0,a0) *)
let r_havoc = function
  | [undef1;m1;p1;a1] -> begin
      match F.repr m1 with
      | L.Fun( f , [_undef0;m0;p0;a0] ) when f == f_havoc -> begin
          let open Qed.Logic in
          match F.is_true (r_included [p0;a0;p1;a1]) with
          | Yes -> F.e_fun f_havoc [undef1;m0;p1;a1]
          | _ -> raise Not_found
        end
      | _ -> raise Not_found
    end
  | _ -> raise Not_found

(* havoc(undef,m,p,a)[k] =
   - m[k]     WHEN separated (p,a,k,1)
   - undef[k] WHEN NOT separated (p,a,k,1)
*)
let r_get_havoc = function
  | [undef;m;p;a] ->
    (fun _ k ->
       match is_separated [p;a;k;e_one] with
       | L.Yes -> F.e_get m k
       | L.No  -> F.e_get undef k
       | _ -> raise Not_found)
  | _ -> raise Not_found

(* -------------------------------------------------------------------------- *)
(* --- Simplifier for int/addr conversion                                 --- *)
(* -------------------------------------------------------------------------- *)

let phi_int_of_addr p =
  if p == a_null then F.e_zero else
    match F.repr p with
    | L.Fun(f,[a]) when f == f_addr_of_int -> a
    | _ -> raise Not_found

let phi_addr_of_int p =
  if p == F.e_zero then a_null else
    match F.repr p with
    | L.Fun(f,[a]) when f == f_int_of_addr -> a
    | _ -> raise Not_found

(* -------------------------------------------------------------------------- *)
(* --- Simplifier for (in)validity                                        --- *)
(* -------------------------------------------------------------------------- *)

let null_base p = e_eq (F.e_fun f_base [p]) F.e_zero

(* See: tests/why3/test_memory.why *)

(* - lemma valid_rd_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rd m p n)
   - lemma valid_rw_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rw m p n)
*)
let r_valid_unref = function
  | [_; p; n] when F.decide (null_base p) ->
    e_leq n e_zero
  | _ -> raise Not_found

(* - lemma valid_obj_null: forall m n. valid_obj m null n *)
let r_valid_obj = function
  | [_; p; _] when F.decide (e_eq p a_null) -> e_true
  | _ -> raise Not_found

(* - lemma invalid_null: forall m n p. p.base = 0 -> invalid m p n *)
let r_invalid = function
  | [_; p; _] when F.decide (null_base p) -> e_true
  | _ -> raise Not_found

(* -------------------------------------------------------------------------- *)
(* --- Simplifiers Registration                                           --- *)
(* -------------------------------------------------------------------------- *)

let () = Context.register
    begin fun () ->
      F.set_builtin_1   f_base   phi_base ;
      F.set_builtin_1   f_offset phi_offset ;
      F.set_builtin_2   f_shift  (phi_shift f_shift) ;
      F.set_builtin_eqp f_shift  eq_shift ;
      F.set_builtin_eqp f_global eq_shift ;
      F.set_builtin p_separated r_separated ;
      F.set_builtin p_included  r_included ;
      F.set_builtin f_havoc r_havoc ;
      F.set_builtin_get f_havoc r_get_havoc ;
      F.set_builtin_1 f_addr_of_int phi_addr_of_int ;
      F.set_builtin_1 f_int_of_addr phi_int_of_addr ;
      F.set_builtin p_invalid r_invalid ;
      F.set_builtin p_valid_rd r_valid_unref ;
      F.set_builtin p_valid_rw r_valid_unref ;
      F.set_builtin p_valid_obj r_valid_obj ;
    end

(* -------------------------------------------------------------------------- *)
(* --- Frame Conditions                                                   --- *)
(* -------------------------------------------------------------------------- *)

module T = Definitions.Trigger

let frames ~addr:p ~offset:n ~sizeof:s ?(basename="mem") tau =
  let t_mem = L.Array(t_addr,tau) in
  let m  = F.e_var (Lang.freshvar ~basename t_mem) in
  let m' = F.e_var (Lang.freshvar ~basename t_mem) in
  let p' = F.e_var (Lang.freshvar ~basename:"q" t_addr) in
  let n' = F.e_var (Lang.freshvar ~basename:"n" L.Int) in
  let mh = F.e_fun f_havoc [m';m;p';n'] in
  let v' = F.e_var (Lang.freshvar ~basename:"v" tau) in
  let meq = F.p_call p_eqmem [m;m';p';n'] in
  let diff = F.p_call p_separated [p;n;p';s] in
  let sep = F.p_call p_separated [p;n;p';n'] in
  let inc = F.p_call p_included [p;n;p';n'] in
  let teq = T.of_pred meq in
  [
    "update" , [] , [diff] , m , e_set m p' v' ;
    "eqmem" , [teq] , [inc;meq] , m , m' ;
    "havoc" , [] , [sep] , m , mh ;
  ]

(* -------------------------------------------------------------------------- *)
(* --- Range Comparison                                                   --- *)
(* -------------------------------------------------------------------------- *)

type range =
  | LOC of term * term (* loc - size *)
  | RANGE of term * Vset.set (* base - range offset *)

let range ~shift ~addrof ~sizeof = function
  | Sigs.Rloc(obj,loc) ->
    LOC( addrof loc , sizeof obj )
  | Sigs.Rrange(loc,obj,Some a,Some b) ->
    let s = sizeof obj in
    let p = addrof (shift loc obj a) in
    let n = e_mul s (e_range a b) in
    LOC( p , n )
  | Sigs.Rrange(loc,_obj,None,None) ->
    RANGE( a_base (addrof loc) , Vset.range None None )
  | Sigs.Rrange(loc,obj,Some a,None) ->
    let s = sizeof obj in
    RANGE( a_base (addrof loc) , Vset.range (Some (e_mul s a)) None )
  | Sigs.Rrange(loc,obj,None,Some b) ->
    let s = sizeof obj in
    RANGE( a_base (addrof loc) , Vset.range None (Some (e_mul s b)) )

let range_set = function
  | LOC(l,n) ->
    let a = a_offset l in
    let b = e_add a n in
    a_base l , Vset.range (Some a) (Some b)
  | RANGE(base,set) -> base , set

let r_included r1 r2 =
  match r1 , r2 with
  | LOC(l1,n1) , LOC(l2,n2) ->
    F.p_call p_included [l1;n1;l2;n2]
  | _ ->
    let base1,set1 = range_set r1 in
    let base2,set2 = range_set r2 in
    F.p_if (F.p_equal base1 base2)
      (Vset.subset set1 set2)
      (Vset.is_empty set1)

let r_disjoint r1 r2 =
  match r1 , r2 with
  | LOC(l1,n1) , LOC(l2,n2) ->
    F.p_call p_separated [l1;n1;l2;n2]
  | _ ->
    let base1,set1 = range_set r1 in
    let base2,set2 = range_set r2 in
    F.p_imply (F.p_equal base1 base2) (Vset.disjoint set1 set2)

let included ~shift ~addrof ~sizeof s1 s2  =
  let range = range ~shift ~addrof ~sizeof in
  r_included (range s1) (range s2)

let separated ~shift ~addrof ~sizeof s1 s2 =
  let range = range ~shift ~addrof ~sizeof in
  r_disjoint (range s1) (range s2)

(* -------------------------------------------------------------------------- *)
(* --- Unsupported Unions                                                 --- *)
(* -------------------------------------------------------------------------- *)

let wkey = Wp_parameters.register_warn_category "union"

let unsupported_union (fd : Cil_types.fieldinfo) =
  if not fd.fcomp.cstruct then
    Wp_parameters.warning ~once:true ~wkey
      "Accessing union fields with WP might be unsound.@\n\
       Please refer to WP manual."

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