package frama-c

  1. Overview
  2. Docs

doc/src/frama-c-wp.core/MemZeroAlias.ml.html

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

(* -------------------------------------------------------------------------- *)
(* --- L-Value Indexed Memory Model                                       --- *)
(* -------------------------------------------------------------------------- *)

open Cil_types
open Cil_datatype
open Lang
open Lang.F
open Sigs

module Logic = Qed.Logic

let datatype = "MemZeroAlias"

let configure () =
  begin
    let orig_pointer = Context.push Lang.pointer Logic.Int in
    let orig_null    = Context.push Cvalues.null (p_equal e_zero) in
    let rollback () =
      Context.pop Lang.pointer orig_pointer ;
      Context.pop Cvalues.null orig_null ;
    in
    rollback
  end
let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder

(* TODO: compute actual separation hypotheses *)
let hypotheses p = p

(* -------------------------------------------------------------------------- *)
(* --- Chunks                                                             --- *)
(* -------------------------------------------------------------------------- *)

type chunk = varinfo * path list (* from left to right *)
and path = S | I | F of fieldinfo

let hash_path = function S -> 1 | I -> 2 | F fd -> Fieldinfo.hash fd

let equal_path p q = match p,q with
  | S , S -> true
  | I , I -> true
  | F f , F g -> Fieldinfo.equal f g
  | _ -> false

let compare_path p q = match p,q with
  | S , S -> 0
  | S , _ -> (-1)
  | _ , S -> 1
  | I , I -> 0
  | I , _ -> (-1)
  | _ , I -> 1
  | F f , F g -> Fieldinfo.compare f g

[@@@ warning "-32"]
let pp_path fmt = function
  | S -> Format.pp_print_char fmt '*'
  | I -> Format.pp_print_string fmt "[]"
  | F f -> Format.pp_print_char fmt '.' ; Fieldinfo.pretty fmt f
[@@@ warning "+32"]

let rec object_of_rpath x = function
  | [] -> Ctypes.object_of x.vtype
  | S :: p -> Ctypes.object_of_pointed (object_of_rpath x p)
  | I :: p -> Ctypes.object_of_array_elem (object_of_rpath x p)
  | F f :: _ -> Ctypes.object_of f.ftype

let rec dim_of_path t = function
  | [] -> t
  | S :: p | F _ :: p -> dim_of_path t p
  | I :: p -> dim_of_path Qed.Logic.(Array(Int,t)) p

module Chunk =
struct
  type t = chunk
  let self = "mtree"
  let hash (x,p) = Qed.Hcons.hash_list hash_path (Varinfo.hash x) p
  let equal (x,p) (y,q) = Varinfo.equal x y && Qed.Hcons.equal_list equal_path p q
  let compare (x,p) (y,q) =
    let cmp = Varinfo.compare x y in
    if cmp <> 0 then cmp else Qed.Hcons.compare_list compare_path p q

  let rec pp x fmt = function
    | [] -> Varinfo.pretty fmt x
    | [S] -> Format.fprintf fmt "*%a" Varinfo.pretty x
    | S::ps -> Format.fprintf fmt "*(%a)" (pp x) ps
    | I::ps -> Format.fprintf fmt "%a[]" (pp x) ps
    | F f::S::ps -> Format.fprintf fmt "%a->%a" (pp x) ps Fieldinfo.pretty f
    | F f::ps -> Format.fprintf fmt "%a.%a" (pp x) ps Fieldinfo.pretty f

  let pretty fmt (x,p) = Format.fprintf fmt "@[<hov 2>%a@]" (pp x) (List.rev p)
  let tau_of_chunk (x,p) =
    let te = Lang.tau_of_object (object_of_rpath x (List.rev p)) in
    dim_of_path te p
  let basename_of_chunk (x,_) = LogicUsage.basename x
  let is_framed (x,p) = not x.vglob && p = []
end

module Heap = Qed.Collection.Make(Chunk)
module Sigma = Sigma.Make(Chunk)(Heap)

type loc =
  | Null
  | Var of varinfo
  | Star of loc
  | Array of loc * F.term
  | Field of loc * fieldinfo

type sigma = Sigma.t
type domain = Sigma.domain
type segment = loc rloc

let rec pretty fmt = function
  | Null -> Format.pp_print_string fmt "null"
  | Var x -> Varinfo.pretty fmt x
  | Star(Var x) -> Format.fprintf fmt "*%a" Varinfo.pretty x
  | Star p -> Format.fprintf fmt "*(%a)" pretty p
  | Array(p,k) -> Format.fprintf fmt "%a[%a]" pretty p Lang.F.pp_term k
  | Field(Star p,f) -> Format.fprintf fmt "%a->%a" pretty p Fieldinfo.pretty f
  | Field(p,f) -> Format.fprintf fmt "%a.%a" pretty p Fieldinfo.pretty f

let rec vars = function
  | Var _ | Null -> Vars.empty
  | Star p | Field(p,_) -> vars p
  | Array(p,k) -> Vars.union (vars p) (F.vars k)

let rec occurs x = function
  | Null | Var _ -> false
  | Star p | Field(p,_) -> occurs x p
  | Array(p,k) -> F.occurs x k || occurs x p

let source = "Tree Model"

let null = Null
let literal ~eid:_ _ = Warning.error ~source "No Literal"
let pointer_loc _t = Warning.error ~source "No Pointer Loc"
let pointer_val _v = Warning.error ~source "No Pointer Val"

let cvar x = Var x
let field l f = Field(l,f)
let shift l _obj k = Array(l,k)

let base_addr _l = Warning.error ~source "No Base Addr"
let base_offset _l = Warning.error ~source "No Offset Addr"
let block_length _s _obj _l = Warning.error ~source "No Block Length"

let cast _ _l = Warning.error ~source "No Cast"
let loc_of_int _ _ = Warning.error ~source "No Hardware Address"
let int_of_loc _ _ = Warning.error ~source "No Hardware Address"

let rec walk ps ks = function
  | Null -> Warning.error ~source "No Null Walk"
  | Var x -> (x,ps),ks
  | Star l -> walk (S::ps) ks l
  | Array(l,k) -> walk (I::ps) (k::ks) l
  | Field(l,f) -> walk (F f::ps) ks l

let access l = walk [] [] l

let domain _obj l =
  try Heap.Set.singleton (fst (access l))
  with _ -> Heap.Set.empty

let is_well_formed _s = p_true

let value sigma l =
  let m,ks = access l in
  let x = Sigma.get sigma m in
  List.fold_left F.e_get (e_var x) ks

let rec update a ks v =
  match ks with
  | [] -> v
  | k::ks -> F.e_set a k (update (F.e_get a k) ks v)

let set s m ks v = if ks = [] then v else update (e_var (Sigma.get s m)) ks v

let load sigma obj l =
  if Ctypes.is_pointer obj then Loc (Star l) else Val(value sigma l)

let load_init _sigma _obj _l = Warning.error ~source "Mem0Alias: No initialized"

let stored seq _obj l e =
  let m,ks = access l in
  let x = F.e_var (Sigma.get seq.post m) in
  [Set( x , set seq.pre m ks e )]

let stored_init _seq _obj _l _e = Warning.error ~source "Mem0Alias: No initialized"

let copied seq obj a b =
  stored seq obj a (value seq.pre b)

let copied_init _seq _obj _a _b = Warning.error ~source "Mem0Alias: No initialized"

let assigned _s _obj _sloc = []

type state = Chunk.t Tmap.t
let state (s:sigma) =
  let m = ref Tmap.empty in
  Sigma.iter (fun c x -> m := Tmap.add (F.e_var x) c !m) s ; !m

let imval c = Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KValue)
let iter f s = Tmap.iter (fun v c -> f (imval c) v) s
let lookup (s : state) (e : Lang.F.term) = imval (F.Tmap.find e s)
let apply f s =
  let m = ref Tmap.empty in
  Tmap.iter (fun e c -> m := Tmap.add (f e) c !m) s ; !m

let rec ipath lv = function
  | [] -> lv
  | S::w -> ipath (Mval lv,[]) w
  | I::_ -> raise Not_found
  | F f::w ->
    let (host,path) = lv in
    ipath (host, path @ [Mfield f]) w
let ilval (x,p) = ipath (Mvar x,[]) p

let heap domain state =
  Tmap.fold
    (fun m c w ->
       if Vars.intersect (F.vars m) domain
       then Heap.Map.add c m w else w
    ) state Heap.Map.empty

let updates seq domain =
  let pre = heap domain seq.pre in
  let post = heap domain seq.post in
  let pool = ref Bag.empty in
  Heap.Map.iter2
    (fun c v1 v2 ->
       try
         match v1,v2 with
         | _,None -> ()
         | None,Some v ->
           pool := Bag.add (Mstore(ilval c,v)) !pool
         | Some v1,Some v2 ->
           if v2 != v1 then
             pool := Bag.add (Mstore (ilval c,v2)) !pool
       with Not_found -> ()
    ) pre post ;
  !pool

let no_pointer () = Warning.error ~source "No Pointer"

let is_null = function Null -> F.p_true | _ -> no_pointer ()
let loc_eq _ _ = no_pointer ()
let loc_lt _ _ = no_pointer ()
let loc_leq _ _ = no_pointer ()
let loc_neq _ _ = no_pointer ()
let loc_diff _ _ _ = no_pointer ()

let frame _sigma = []
let alloc sigma _xs = sigma
let scope _seq _s _xs = []
let valid _sigma _acs _l = Warning.error ~source "No validity"
let invalid _sigma _l = Warning.error ~source "No validity"
let initialized _sigma _l = Warning.error ~source "Mem0Alias: No initialized"
let global _sigma _p = p_true

let included _s1 _s2 = no_pointer ()
let separated _s1 _s2 = no_pointer ()
OCaml

Innovation. Community. Security.