Source file node_kind.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
open Dive_types
module DatatypeInput =
struct
include Datatype.Undefined
open Cil_datatype
type t = node_kind
let (<?>) c (cmp,x,y) =
if c = 0
then cmp x y
else c
let name = "Node_kind"
let reprs = [ Scalar (
List.hd Varinfo.reprs,
List.hd Typ.reprs,
List.hd Offset.reprs) ]
let compare k1 k2 =
match k1, k2 with
| Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
Varinfo.compare vi1 vi2 <?> (OffsetStructEq.compare, offset1, offset2)
| Scalar _, _ -> 1
| _, Scalar _ -> -1
| Composite vi1, Composite vi2 -> Varinfo.compare vi1 vi2
| Composite _, _ -> 1
| _, Composite _ -> -1
| Scattered (lv1,stmt1), Scattered (lv2,stmt2) ->
LvalStructEq.compare lv1 lv2 <?> (Stmt.compare, stmt1, stmt2)
| Scattered _, _ -> 1
| _, Scattered _ -> -1
| Unknown (lv1,stmt1), Unknown (lv2,stmt2) ->
LvalStructEq.compare lv1 lv2 <?> (Stmt.compare, stmt1, stmt2)
| Unknown _, _ -> 1
| _, Unknown _ -> -1
| Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
Stmt.compare stmt1 stmt2 <?> (Alarms.compare, alarm1, alarm2)
| Alarm _, _ -> 1
| _, Alarm _ -> -1
| AbsoluteMemory, AbsoluteMemory -> 0
| AbsoluteMemory, _ -> 1
| _, AbsoluteMemory -> -1
| String (i1,_), String (i2,_) ->
Datatype.Int.compare i1 i2
| String _, _ -> 1
| _, String _ -> -1
| Const e1, Const e2 ->
Cil_datatype.Exp.compare e1 e2
| Const _, _ -> 1
| _, Const _ -> -1
| Error s1, Error s2 ->
Datatype.String.compare s1 s2
let equal k1 k2 =
match k1, k2 with
| Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
Varinfo.equal vi1 vi2 && OffsetStructEq.equal offset1 offset2
| Composite vi1, Composite vi2 -> Varinfo.equal vi1 vi2
| Scattered (lv1, stmt1), Scattered (lv2, stmt2) ->
LvalStructEq.equal lv1 lv2 && Stmt.equal stmt1 stmt2
| Unknown (lv1, stmt1), Unknown (lv2, stmt2) ->
LvalStructEq.equal lv1 lv2 && Stmt.equal stmt1 stmt2
| Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
| AbsoluteMemory, AbsoluteMemory -> true
| String (i,_), String (j,_) -> Datatype.Int.equal i j
| Const e1, Const e2 -> Cil_datatype.Exp.equal e1 e2
| Error s1, Error s2 -> Datatype.String.equal s1 s2
| _ -> false
let hash k =
match k with
| Scalar (vi, _, offset) ->
Hashtbl.hash (1, Varinfo.hash vi, OffsetStructEq.hash offset)
| Composite vi -> Hashtbl.hash (2, Varinfo.hash vi)
| Scattered (lv, stmt) ->
Hashtbl.hash (3, LvalStructEq.hash lv, Stmt.hash stmt)
| Unknown (lv, stmt) ->
Hashtbl.hash (4, LvalStructEq.hash lv, Stmt.hash stmt)
| Alarm (stmt, alarm) ->
Hashtbl.hash (5, Stmt.hash stmt, Alarms.hash alarm)
| AbsoluteMemory -> 6
| String (i, _) -> Hashtbl.hash (7, i)
| Const e -> Hashtbl.hash (8, Cil_datatype.Exp.hash e)
| Error s -> Hashtbl.hash (9, s)
end
include Datatype.Make (DatatypeInput)
let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
| Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory
| String _ | Const _ | Error _ -> None
let to_lval = function
| Scalar (vi,_typ,offset) -> Some (Cil_types.Var vi, offset)
| Composite (vi) -> Some (Cil_types.Var vi, Cil_types.NoOffset)
| Scattered (lval,_) -> Some lval
| Unknown (lval,_) -> Some lval
| Alarm (_,_) | AbsoluteMemory | String _ | Const _ | Error _ -> None
let pretty fmt = function
| (Scalar _ | Composite _ | Scattered _ | Unknown _) as kind ->
Cil_printer.pp_lval fmt (Option.get (to_lval kind))
| Alarm (_stmt,alarm) ->
Cil_printer.pp_predicate fmt (Alarms.create_predicate alarm)
| AbsoluteMemory ->
Format.fprintf fmt "%s" (Kernel.AbsoluteValidRange.get ())
| String (_, CSString s) ->
Format.fprintf fmt "%S" s
| String (_, CSWstring s) ->
Format.fprintf fmt "L\"%s\"" (Escape.escape_wstring s)
| Const e ->
Format.fprintf fmt "%a" Cil_printer.pp_exp e
| Error s ->
Format.fprintf fmt "%s" s