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
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(* Event components *)
type loc = Data of string | Code of Label.t
let as_data = function
| Data loc -> loc
| Code _ -> assert false
let is_data = function
| Data _ -> true
| Code _ -> false
let pp_loc = function Data s | Code s -> s
let loc_eq loc1 loc2 = match loc1,loc2 with
| (Data s1,Data s2)
| (Code s1,Code s2)
-> Misc.string_eq s1 s2
| (Data _,Code _)
| (Code _,Data _)
-> false
let loc_compare loc1 loc2 = match loc1,loc2 with
| Data _,Code _ -> -1
| Code _,Data _ -> 1
| (Data s1,Data s2)
| (Code s1,Code s2)
-> compare s1 s2
module LocOrd = struct
type t = loc
let compare = loc_compare
end
module LocSet = MySet.Make(LocOrd)
module LocMap = MyMap.Make(LocOrd)
let loc_none = Data "*"
let ok_str = "ok"
let ok = Data ok_str
let myok p n = Data (Printf.sprintf "ok%i%i" p n)
let myok_proc p = Data (Printf.sprintf "ok%i" p)
type v = int
let pp_v ?(hexa=false) =
Printf.sprintf
(if hexa then "0x%x" else "%d")
type proc = Proc.t
let pp_proc p = Proc.pp p
type env = (string * v) list
(* Direction of event *)
type dir = W | R | J
(* Edges compoments that do not depend on architecture *)
(* Change or proc accross edge *)
type ie = Int|Ext
(* Change of location across edge *)
type sd = Same|Diff
(* Direction of related events *)
type extr = Dir of dir | Irr | NoDir
(* Associated pretty print & generators *)
let pp_dir = function
| W -> "W"
| R -> "R"
| J -> "J"
let pp_ie = function
| Int -> "i"
| Ext -> "e"
let pp_extr = function
| Dir d -> pp_dir d
| Irr -> "*"
| NoDir -> ""
let pp_sd = function
| Same -> "s"
| Diff -> "d"
let seq_sd sd1 sd2 =
match sd1,sd2 with
| Same,Same -> Same
| Diff,_|_,Diff -> Diff
let fold_ie f r = f Ext (f Int r)
let fold_sd f r = f Diff (f Same r)
let do_fold_extr withj f r =
let r = f (Dir W) (f (Dir R) (f Irr r)) in
if withj then f (Dir J) r
else r
let fold_extr f r = do_fold_extr false f r
let fold_sd_extr f = fold_sd (fun sd -> fold_extr (fun e -> f sd e))
let fold_sd_extr_extr f =
fold_sd_extr (fun sd e1 -> fold_extr (fun e2 -> f sd e1 e2))
type check =
| Default | Sc | Uni | Thin | Critical
| Free | Ppo | Transitive | Total | MixedCheck
let pp_check =
function
| Default -> "default"
| Sc -> "sc"
| Uni -> "uni"
| Thin -> "thin"
| Critical -> "critical"
| Free -> "free"
| Ppo -> "ppo"
| Transitive -> "transitive"
| Total -> "total"
| MixedCheck -> "mixedcheck"
let checks =
[
"default";
"sc";
"uni";
"thin";
"critical";
"free";
"ppo";
"transitive";
"total";
"mixedcheck";
]
(* Com relation *)
type com = CRf | CFr | CWs
let pp_com = function
| CRf -> "Rf"
| CFr -> "Fr"
| CWs -> "Co"
let fold_com f r = f CRf (f CFr (f CWs r))
(* Info in tests *)
type info = (string * string) list
let plain = "Na"
(* Memory Space *)
type 'a bank = Ord | Tag | CapaTag | CapaSeal | Pte | VecReg of 'a | Pair | Instr
let pp_bank = function
| Ord -> "Ord"
| Tag -> "Tag"
| CapaTag -> "CapaTag"
| CapaSeal -> "CapaSeal"
| Pte -> "Pte"
| VecReg _ -> "VecReg"
| Pair -> "Pair"
| Instr -> "Instr"
let tag_of_int = function
| 0 -> "green"
| 1 -> "red"
| 2 -> "blue"
| 3 -> "black"
| 4 -> "white"
| 5 -> "cyan"
| 6 -> "yellow"
| 7 -> "magenta"
| n -> Warn.fatal "Sorry, not pretty tag for number %i" n
let add_tag s t = Printf.sprintf "%s:%s" s (tag_of_int t)
let add_capability s t = Printf.sprintf "0xffffc0000:%s:%i" s (if t = 0 then 1 else 0)
let add_vector hexa v =
let open Printf in
let pp = pp_v ~hexa:hexa in
sprintf "{%s}"
(String.concat "," (List.map pp v))
|
