Source file libraryDesc.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
(** Library function descriptor (specification). *)
module Cil = GoblintCil
open Cil
(** Pointer argument access specification. *)
module Access =
struct
type t = {
kind: AccessKind.t; (** Kind of access. *)
deep: bool; (** Depth of access
- Shallow only accesses directly pointed values (may point to).
- Deep additionally follows all pointers in values (reachable). Rarely needed. *)
}
end
type math =
| Nan of (CilType.Fkind.t * Basetype.CilExp.t)
| Inf of CilType.Fkind.t
| Isfinite of Basetype.CilExp.t
| Isinf of Basetype.CilExp.t
| Isnan of Basetype.CilExp.t
| Isnormal of Basetype.CilExp.t
| Signbit of Basetype.CilExp.t
| Isgreater of (Basetype.CilExp.t * Basetype.CilExp.t)
| Isgreaterequal of (Basetype.CilExp.t * Basetype.CilExp.t)
| Isless of (Basetype.CilExp.t * Basetype.CilExp.t)
| Islessequal of (Basetype.CilExp.t * Basetype.CilExp.t)
| Islessgreater of (Basetype.CilExp.t * Basetype.CilExp.t)
| Isunordered of (Basetype.CilExp.t * Basetype.CilExp.t)
| Abs of (CilType.Ikind.t * Basetype.CilExp.t)
| Ceil of (CilType.Fkind.t * Basetype.CilExp.t)
| Floor of (CilType.Fkind.t * Basetype.CilExp.t)
| Fabs of (CilType.Fkind.t * Basetype.CilExp.t)
| Fmax of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t)
| Fmin of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t)
| Acos of (CilType.Fkind.t * Basetype.CilExp.t)
| Asin of (CilType.Fkind.t * Basetype.CilExp.t)
| Atan of (CilType.Fkind.t * Basetype.CilExp.t)
| Atan2 of (CilType.Fkind.t * Basetype.CilExp.t * Basetype.CilExp.t)
| Cos of (CilType.Fkind.t * Basetype.CilExp.t)
| Sin of (CilType.Fkind.t * Basetype.CilExp.t)
| Tan of (CilType.Fkind.t * Basetype.CilExp.t)
| Sqrt of (CilType.Fkind.t * Basetype.CilExp.t) [@@deriving eq, ord, hash]
(** Type of special function, or {!Unknown}. *)
type special =
| Alloca of Cil.exp
| Malloc of Cil.exp
| Calloc of { count: Cil.exp; size: Cil.exp; }
| Realloc of { ptr: Cil.exp; size: Cil.exp; }
| Free of Cil.exp
| Assert of { exp: Cil.exp; check: bool; refine: bool; }
| Lock of { lock: Cil.exp; try_: bool; write: bool; return_on_success: bool; }
| Unlock of Cil.exp
| ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
| ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
| ThreadExit of { ret_val: Cil.exp; }
| ThreadSelf
| Globalize of Cil.exp
| Signal of Cil.exp
| Broadcast of Cil.exp
| MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
| MutexInit of { mutex:Cil.exp; attr: Cil.exp; }
| SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; }
| SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;}
| SemPost of Cil.exp
| SemDestroy of Cil.exp
| Wait of { cond: Cil.exp; mutex: Cil.exp; }
| TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
| Math of { fun_args: math; }
| Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
| Bzero of { dest: Cil.exp; count: Cil.exp; }
| Memcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp; }
| Strcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; }
| Strcat of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; }
| Strlen of Cil.exp
| Strstr of { haystack: Cil.exp; needle: Cil.exp; }
| Strcmp of { s1: Cil.exp; s2: Cil.exp; n: Cil.exp option; }
| Abort
| Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
| Setjmp of { env: Cil.exp; }
| Longjmp of { env: Cil.exp; value: Cil.exp; }
| Bounded of { exp: Cil.exp} (** Used to check for bounds for termination analysis. *)
| Rand
| Unknown (** Anything not belonging to other types. *)
(** Pointer arguments access specification. *)
module Accesses =
struct
type t = Cil.exp list -> (Access.t * Cil.exp list) list
let find (accs: t): Access.t -> Cil.exp list -> Cil.exp list = fun acc args ->
BatOption.(List.assoc_opt acc (accs args) |? [])
let find_kind (accs: t): AccessKind.t -> Cil.exp list -> Cil.exp list = fun kind args ->
let f a = find accs a args in
f { kind; deep = true; } @ f { kind; deep = false; }
let iter (accs: t) (f: Access.t -> Cil.exp -> unit) args: unit =
accs args
|> List.iter (fun (acc, exps) ->
List.iter (fun exp -> f acc exp) exps
)
let fold (accs: t) (f: Access.t -> Cil.exp -> 'a -> 'a) args (a: 'a): 'a =
accs args
|> List.fold_left (fun a (acc, exps) ->
List.fold_left (fun a exp -> f acc exp a) a exps
) a
end
(** Function attribute. *)
type attr =
| ThreadUnsafe (** Function is not thread-safe to call, e.g. due to its own internal (global) state.
@see <https://man7.org/linux/man-pages/man7/pthreads.7.html> for list of thread-unsafe functions under POSIX.
@see <https://github.com/goblint/analyzer/issues/723> for Goblint issue about the (future) use of this attribute. *)
| InvalidateGlobals (** Function invalidates all globals when called. *)
(** Library function descriptor. *)
type t = {
special: Cil.exp list -> special; (** Conversion to {!type-special} using arguments. *)
accs: Accesses.t; (** Pointer arguments access specification. *)
attrs: attr list; (** Attributes of function. *)
}
module MathPrintable = struct
include Printable.StdLeaf
type t = math [@@deriving eq, ord, hash]
let name () = "MathPrintable"
let pretty () = function
| Nan (fk, exp) -> Pretty.dprintf "(%a )nan(%a)" d_fkind fk d_exp exp
| Inf fk -> Pretty.dprintf "(%a )inf()" d_fkind fk
| Isfinite exp -> Pretty.dprintf "isFinite(%a)" d_exp exp
| Isinf exp -> Pretty.dprintf "isInf(%a)" d_exp exp
| Isnan exp -> Pretty.dprintf "isNan(%a)" d_exp exp
| Isnormal exp -> Pretty.dprintf "isNormal(%a)" d_exp exp
| Signbit exp -> Pretty.dprintf "signbit(%a)" d_exp exp
| Isgreater (exp1, exp2) -> Pretty.dprintf "isGreater(%a, %a)" d_exp exp1 d_exp exp2
| Isgreaterequal (exp1, exp2) -> Pretty.dprintf "isGreaterEqual(%a, %a)" d_exp exp1 d_exp exp2
| Isless (exp1, exp2) -> Pretty.dprintf "isLess(%a, %a)" d_exp exp1 d_exp exp2
| Islessequal (exp1, exp2) -> Pretty.dprintf "isLessEqual(%a, %a)" d_exp exp1 d_exp exp2
| Islessgreater (exp1, exp2) -> Pretty.dprintf "isLessGreater(%a, %a)" d_exp exp1 d_exp exp2
| Isunordered (exp1, exp2) -> Pretty.dprintf "isUnordered(%a, %a)" d_exp exp1 d_exp exp2
| Abs (ik, exp) -> Pretty.dprintf "(%a )abs(%a)" d_ikind ik d_exp exp
| Ceil (fk, exp) -> Pretty.dprintf "(%a )ceil(%a)" d_fkind fk d_exp exp
| Floor (fk, exp) -> Pretty.dprintf "(%a )floor(%a)" d_fkind fk d_exp exp
| Fabs (fk, exp) -> Pretty.dprintf "(%a )fabs(%a)" d_fkind fk d_exp exp
| Fmax (fk, exp1, exp2) -> Pretty.dprintf "(%a )fmax(%a, %a)" d_fkind fk d_exp exp1 d_exp exp2
| Fmin (fk, exp1, exp2) -> Pretty.dprintf "(%a )fmin(%a, %a)" d_fkind fk d_exp exp1 d_exp exp2
| Acos (fk, exp) -> Pretty.dprintf "(%a )acos(%a)" d_fkind fk d_exp exp
| Asin (fk, exp) -> Pretty.dprintf "(%a )asin(%a)" d_fkind fk d_exp exp
| Atan (fk, exp) -> Pretty.dprintf "(%a )atan(%a)" d_fkind fk d_exp exp
| Atan2 (fk, exp1, exp2) -> Pretty.dprintf "(%a )atan2(%a, %a)" d_fkind fk d_exp exp1 d_exp exp2
| Cos (fk, exp) -> Pretty.dprintf "(%a )cos(%a)" d_fkind fk d_exp exp
| Sin (fk, exp) -> Pretty.dprintf "(%a )sin(%a)" d_fkind fk d_exp exp
| Tan (fk, exp) -> Pretty.dprintf "(%a )tan(%a)" d_fkind fk d_exp exp
| Sqrt (fk, exp) -> Pretty.dprintf "(%a )sqrt(%a)" d_fkind fk d_exp exp
include Printable.SimplePretty (
struct
type nonrec t = t
let pretty = pretty
end
)
end
module MathLifted = Lattice.FlatConf (struct
include Printable.DefaultConf
let top_name = "Unknown or no math desc"
let bot_name = "Nonexistent math desc"
end) (MathPrintable)