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
open Cil_types
open Cil_datatype
open Spec
open Memory
open Domain
type env = {
map : map ;
result : node option ;
formals : domain Varinfo.Map.t ;
context : Access.clause ;
}
let merge a b = Memory.merge a b ; min a b
let pointer (d:domain) : node =
match Domain.pointed merge d with
| Some p -> p
| None -> Options.fatal "Not a pointer value"
type lv_value =
| VAL of domain
| VAR of varinfo
let logic_var env lv =
match lv.lv_origin with
| None -> VAL (Memory.add_lvar env.map lv)
| Some x ->
if x.vformal then
try VAL (Varinfo.Map.find x env.formals) with Not_found -> VAR x
else VAR x
let rec load env lv (ty,r) : domain =
match Ast_types.unroll_node ty with
| TArray(te,_) ->
let re = Memory.add_index r te in
let ofs = TIndex (Logic_const.trange (None,None), TNoOffset) in
let lve = Logic_const.addTermOffsetLval ofs lv in
array (load env lve (te,re))
| TComp { cfields } ->
let add_field d fd =
let ofs = TField (fd,TNoOffset) in
let lvf = Logic_const.addTermOffsetLval ofs lv in
merge_domain d
@@ Domain.field fd
@@ load env lvf
@@ (fd.ftype, Memory.add_field r fd)
in List.fold_left add_field pure @@ Option.value ~default:[] cfields
| _ ->
let acs = Access.Term (env.context, lv) in
Memory.add_read r acs ;
Domain.scalar @@ Memory.add_value r ty
let rterm = ref (fun _ _ -> assert false)
let rec addr_offset ~loc (env:env) (ty:typ) (r:node) = function
| TNoOffset -> ty,r
| TModel _ ->
Options.not_yet_implemented ~source:(fst loc) "Unsupported model fields"
| TField (f,offset) ->
addr_offset ~loc env f.ftype (Memory.add_field r f) offset
| TIndex(k,offset) ->
ignore @@ !rterm env k ;
let te = Ast_types.direct_element_type ty in
addr_offset ~loc env te (Memory.add_index r ty) offset
let rec term_offset ~loc (env:env) (d:domain) = function
| TNoOffset -> d
| TModel _ ->
Options.not_yet_implemented ~source:(fst loc) "Unsupported model fields"
| TField (f,offset) ->
term_offset ~loc env (Domain.get_field merge d f) offset
| TIndex(k,offset) ->
ignore @@ !rterm env k ;
term_offset ~loc env (Domain.get_index merge d) offset
let add_term_lval ~loc (env:env) (lv : term_lval) : domain =
let lhost, loffset = lv in
match lhost with
| TMem e ->
let rh = pointer (!rterm env e) in
let te = Logic_typing.ctype_of_pointed e.term_type in
load env lv @@ addr_offset ~loc env te rh loffset
| TResult ty ->
begin match env.result with
| None -> Options.fatal "\\result undefined" ;
| Some node ->
load env lv @@ addr_offset ~loc env ty node loffset
end
| TVar v ->
begin match logic_var env v with
| VAL d -> term_offset ~loc env d loffset
| VAR x ->
let r = Memory.add_cvar env.map x in
load env lv @@ addr_offset ~loc env x.vtype r loffset
end
let add_addr_lval ~loc (env:env) ?(garbage=false) (lv : term_lval) : typ * node =
let lhost, loffset = lv in
match lhost with
| TMem e ->
let rh = pointer (!rterm env e) in
let te = Logic_typing.ctype_of_pointed e.term_type in
addr_offset ~loc env te rh loffset
| TResult ty ->
begin match env.result with
| None -> Options.fatal "\\result undefined" ;
| Some node -> addr_offset ~loc env ty node loffset
end
| TVar v ->
begin match logic_var env v with
| VAL _ ->
Options.fatal "address of logic value (%a)" Printer.pp_term_lval lv ;
| VAR x ->
let garbage =
garbage && x.vformal && Ast_types.is_struct_or_union x.vtype in
let r = Memory.add_cvar ~garbage env.map x in
addr_offset ~loc env x.vtype r loffset
end
let rec update_offset ~loc (env:env) loffest d =
match loffest with
| TNoOffset -> d
| TField(fd,offset) -> Domain.field fd @@ update_offset ~loc env offset d
| TModel _ ->
Options.not_yet_implemented ~source:(fst loc) "Unsupported model fields"
| TIndex(_,offset) -> Domain.array @@ update_offset ~loc env offset d
let call map (l:logic_info) (ds:domain list) : domain =
let sigma = ref Domain.empty in
let unify = Domain.unify merge sigma in
List.iter2 (fun x -> unify (Memory.add_lvar map x)) l.l_profile ds ;
Domain.subst !sigma @@ Memory.add_logic map l
let cons map (c:logic_ctor_info) (ds:domain list) : domain =
let sigma = ref Domain.empty in
let unify = Domain.unify merge sigma in
let fresh () = Memory.fresh map in
List.iter2 (fun t -> unify (of_ltype fresh t)) c.ctor_params ds ;
Domain.logic c.ctor_type @@
List.map (Domain.getvar !sigma) c.ctor_type.lt_params
let iadd_logic_var m v = ignore @@ add_lvar m v
let rec add_term (env:env) (t:term) : domain =
match t.term_node with
| TLval lval ->
add_term_lval ~loc:t.term_loc env lval
| TAddrOf lval | TStartOf lval ->
ptr @@ snd @@ add_addr_lval ~loc:t.term_loc env lval
| Tif (b,ct,cf) ->
add_predicate env b ;
let dt = add_term env ct in
let df = add_term env cf in
merge_domain dt df
| TUnOp(_,t) | TCast(_,_,t) | Tat(t,_) -> add_term env t
| TBinOp ((PlusPI|MinusPI),t1,t2) ->
let d1 = add_term env t1 in
let d2 = add_term env t2 in
merge_domain d1 d2
| TBinOp(_,t1,t2) -> iadd_term env t1 ; iadd_term env t2 ; pure
| Tbase_addr(_,t) | Toffset (_,t) | Tblock_length(_,t) ->
iadd_term env t ; pure
| TUpdate(lv,o,v) ->
merge_domain (add_term env lv) @@
update_offset ~loc:t.term_loc env o @@ add_term env v
| Tunion ts | Tinter ts ->
List.fold_left (fun d t -> merge_domain d @@ add_term env t) pure ts
| Tcomprehension(t,q,p) ->
Option.iter (add_predicate env) p ;
List.iter (iadd_logic_var env.map) q ;
add_term env t
| Tapp(f,_,ts) -> call env.map f @@ List.map (add_term env) ts
| TDataCons(c,ts) -> cons env.map c @@ List.map (add_term env) ts
| Tlambda(q,t) ->
Domain.arrow (List.map (Memory.add_lvar env.map) q) @@ add_term env t
| Tlet({ l_body ; l_var_info=v },b) ->
begin match l_body with
| LBterm a ->
let dv = add_lvar env.map v in
let da = add_term env a in
let sigma = ref Domain.empty in
Domain.unify merge sigma da dv ;
Domain.subst !sigma @@ add_term env b
| LBpred p ->
iadd_logic_var env.map v ;
add_predicate env p ;
add_term env t
| _ ->
Options.not_yet_implemented
~source:(fst t.term_loc) "Unsupported complex \\let"
end
| TConst _ | TSizeOf _ | TSizeOfE _ | TAlignOf _ | TAlignOfE _
| Tnull | Tempty_set | Ttypeof _ | Ttype _ | Trange _ -> pure
and iadd_term env t = ignore @@ add_term env t
and add_predicate (env:env) (p:predicate) = match p.pred_content with
| Pfalse | Ptrue -> ()
| Pseparated ts -> List.iter (iadd_term env) ts
| Prel(_,t1,t2) | Pfresh(_,_,t1,t2) ->
iadd_term env t1 ;
iadd_term env t2 ;
| Pand(p1,p2) | Por(p1,p2) | Pxor(p1,p2) | Piff(p1,p2) | Pimplies(p1,p2) ->
add_predicate env p1 ;
add_predicate env p2 ;
| Pnot p | Pat(p,_) -> add_predicate env p
| Pif(c,pt,pf) ->
add_predicate env c ;
add_predicate env pt ;
add_predicate env pf ;
| Pobject_pointer(_,t) | Pvalid(_,t) | Pvalid_read(_,t) | Paligned(t, _)
| Pvalid_function t | Pinitialized(_,t) | Pdangling(_,t)
| Pallocable(_,t) | Pfreeable(_,t) -> iadd_term env t
| Pforall (q,p) | Pexists (q,p) ->
List.iter (iadd_logic_var env.map) q ; add_predicate env p
| Plet({ l_var_info = v ; l_body = LBterm t ; },p2) ->
let dv = add_lvar env.map v in
let dt = add_term env t in
let sigma = ref empty in
Domain.unify merge sigma dt dv ;
add_predicate env p2
| Plet({ l_var_info = v ; l_body = LBpred p1 ; },p2) ->
iadd_logic_var env.map v ;
add_predicate env p1 ;
add_predicate env p2
| Plet({ l_body = LBnone ; },p2) ->
add_predicate env p2
| Plet _ ->
Options.not_yet_implemented
~source:(fst p.pred_loc) "Unsupported complex \\let-bindings"
| Papp(f,_,ts) -> ignore @@ call env.map f @@ List.map (add_term env) ts
let () = rterm := add_term
let add_path (env: env) Spec.{ named ; flags } = function
| Spec.Alias(loc,lv) ->
let garbage = Attr.mem `Garbage flags in
snd @@ add_addr_lval ~loc ~garbage env lv
| Spec.Field(loc,lv,f,g) ->
let r = snd @@ add_addr_lval ~loc env lv in
Memory.add_field_range r f g
| Spec.Range(_,ptr,typ,inf,sup) ->
iadd_term env inf ; iadd_term env sup ;
let rp = pointer @@ add_term env ptr in
let re = Memory.add_index rp typ in
let ip = match env.context with Prop ip -> ip | _ -> assert false in
let root = Root { ip ; named ; ptr ; typ ; inf ; sup ; flags } in
Memory.add_root env.map re root ; re
let add_region (env: env) (r : Spec.region) =
let rs = List.map (add_path env r) r.paths in
merge_all @@
if r.named = "" then rs else add_label env.map r.named :: rs
let add_body map (l:logic_info) (d:domain) =
let env = {
map ;
result = None ;
formals = Varinfo.Map.empty ;
context = Body l ;
} in
match l.l_body with
| LBnone -> ()
| LBpred p -> add_predicate env p
| LBterm t -> ignore @@ Memory.merge_domain d (add_term env t)
| LBreads ts ->
List.iter (fun t -> iadd_term env t.it_content) ts
| LBinductive l ->
List.iter (fun (_,_,_,t) -> add_predicate env t) l
let () = Memory.body[@alert "-internal"] := add_body