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
type attr = [ `Nullable | `Allocated | `Garbage | `Readonly ]
type flags = A of int [@@ unboxed]
let flag = function
| `Nullable -> 0b0001
| `Allocated -> 0b0010
| `Garbage -> 0b0100
| `Readonly -> 0b1000
let empty = A 0
let add a (A w) = A (flag a lor w)
let mem a (A w) = flag a land w <> 0
let union (A x) (A y) = A (x lor y)
let subset (A x) (A y) = (x lor y) = y
let iter f w =
List.iter
(fun a -> if mem a w then f a)
[ `Nullable ; `Allocated ; `Garbage ; `Readonly ]
let pp_attr fmt = function
| `Nullable -> Format.pp_print_string fmt "nullable"
| `Allocated -> Format.pp_print_string fmt "allocated"
| `Garbage -> Format.pp_print_string fmt "garbage"
| `Readonly -> Format.pp_print_string fmt "readonly"
let reversed = flag `Readonly
let bottom = A reversed
let merge (A x) (A y) =
let flip w = reversed lxor w in
A (flip (flip x lor flip y))
let pretty fmt w =
begin
Format.fprintf fmt "@[<hov 2>" ;
let sep = ref false in
let next a =
if !sep then Format.fprintf fmt ",@," else sep := true ;
pp_attr fmt a in
iter next w ;
Format.fprintf fmt "@]" ;
end
open Cil_types
let is_local v =
not (v.vglob || v.vformal)
let is_initialized ~garbage v =
v.vglob || v.vdefined ||
(v.vformal && not garbage) ||
(v.vtemp && not @@ Ast_types.is_struct_or_union v.vtype)
let is_const v =
(v.vformal || v.vglob || v.vdefined) &&
Ast_types.is_const v.vtype
let cvar ~garbage v =
let flags = ref empty in
let set f = flags := add f !flags in
if is_local v then set `Allocated ;
if is_const v then set `Readonly ;
if not @@ is_initialized ~garbage v then set `Garbage ;
!flags
let null_or_valid ~loc ~from addr =
if mem `Nullable from then
let null = Logic_const.term ~loc Tnull addr.term_type in
Logic_const.prel ~loc (Rneq,null,addr)
else
Logic_const.ptrue
let readable ~loc ?(label=Logic_const.here_label) ~from addr =
if mem `Allocated from then
Logic_const.pvalid_read ~loc (label, addr)
else
null_or_valid ~loc ~from addr
let writable ~loc ?(label=Logic_const.here_label) ~from addr =
if mem `Readonly from then
Logic_const.pfalse
else
if mem `Allocated from then
Logic_const.pvalid ~loc (label, addr)
else
null_or_valid ~loc ~from addr
let requires ~loc ?(label=Logic_const.here_label) ?(readonly=false) ~from ~target addr =
let valid =
if readonly || mem `Readonly target then
readable ~loc ~label ~from addr
else
writable ~loc ~label ~from addr in
let init =
if mem `Garbage target || not @@ mem `Garbage from then
Logic_const.ptrue
else
Logic_const.pinitialized ~loc (label,addr) in
let allocated =
if mem `Allocated target then
Logic_const.pimplies ~loc (valid,init)
else
Logic_const.pand ~loc (valid,init) in
let nullable =
if mem `Nullable target then
let null = Logic_const.term ~loc Tnull addr.term_type in
Logic_const.prel ~loc (Req,null,addr)
else
Logic_const.pfalse in
Logic_const.por ~loc (nullable,allocated)