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
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2015-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. *)
(****************************************************************************)
open Printf
let arch = Archs.java
let endian = Endian.Little
(* a local variable, like "x" or "y", etc. *)
type reg = string
let parse_reg s = Some s
let pp_reg r = r
let reg_compare = String.compare
type varhandle = string
type barrier = AccessModes.t
let barrier_compare = compare
let pp_barrier b = match b with
| AccessModes.Volatile -> sprintf "VarHandle.fullFence();"
| AccessModes.Acquire -> sprintf "VarHandle.acquireFence();"
| AccessModes.Release -> sprintf "VarHandle.releaseFence();"
| _ -> sprintf "A fence that is not included in Java VarHandle API"
let symb_reg_name r =
let len = String.length r in
assert (len > 0) ;
match r.[0] with
| '%' -> Some (String.sub r 1 (len-1))
| _ -> None
let symb_reg r = sprintf "%%%s" r
type arch_op = ArchOp.no_arch_op
type op = arch_op Op.op
let pp_phantom_archop _ = assert false
let pp_op op = Op.pp_op op pp_phantom_archop
(* (M operation, access_mode for R, access_mode for W) *)
type rw = AccessModes.t * AccessModes.t
type rmw = op * AccessModes.t
type expression =
| Const of int
| LoadReg of reg
| LoadMem of varhandle * AccessModes.t
| CAS of varhandle * rw * expression * expression
| Rmw of varhandle * rmw * expression
| Op of op * expression * expression
type instruction =
| If of expression * instruction * instruction option
| StoreReg of reg * expression
| StoreMem of varhandle * AccessModes.t * expression
| Fence of barrier
| DeclReg of reg
| Seq of instruction list
type parsedInstruction = instruction
let dump_op =
let open Op in
function
| Add -> "add"
| Sub -> "sub"
| Or -> "or"
| Xor -> "xor"
| And -> "and"
| _ -> assert false
let rec dump_expr = function
| Const c -> sprintf "%d" c
| LoadReg r -> r
| LoadMem (varhandle, accessmode) ->
sprintf "%s.get%s()" varhandle (AccessModes.pp_access_modes accessmode)
| Op (op , e1 , e2) ->
sprintf "%s %s %s" (dump_expr e1) (pp_op op) (dump_expr e2)
| CAS (varhandle, rw, expect, target) ->
(sprintf "%s.compareAndExchange%s(%s, %s)"
varhandle
(match rw with
| (AccessModes.Volatile , AccessModes.Volatile) -> ""
| (AccessModes.Acquire, AccessModes.Plain) -> "Acquire"
| (AccessModes.Plain, AccessModes.Release) -> "Release"
| _ -> assert false)
(dump_expr expect)
(dump_expr target))
| Rmw (varhandle, rmw, value) ->
(sprintf "%s.getAnd%s(%s)"
varhandle
(match rmw with
| (Op.Add, AccessModes.Volatile) ->
"Add"
| (Op.Add, AccessModes.Acquire) ->
"AddAcquire"
| (Op.Add, AccessModes.Release) ->
"AddRelease"
| (Op.Or, AccessModes.Volatile) ->
"BitwiseOr"
| (Op.Or, AccessModes.Acquire) ->
"BitwiseOrAcquire"
| (Op.Or, AccessModes.Release) ->
"BitwiseOrRelease"
| (Op.And, AccessModes.Volatile) ->
"BitwiseAnd"
| (Op.And, AccessModes.Acquire) ->
"BitwiseAndAcquire"
| (Op.And, AccessModes.Release) ->
"BitwiseAndRelease"
| (Op.Xor, AccessModes.Volatile) ->
"BitwiseXor"
| (Op.Xor, AccessModes.Acquire) ->
"BitwiseXorAcquire"
| (Op.Xor, AccessModes.Release) ->
"BitwiseXorRelease"
| _ -> assert false)
(dump_expr value))
let rec dump_instruction i =
let rec dump_inst_list = function
| [] -> ""
| hd :: tl -> (dump_instruction hd) ^ "\n" ^ (dump_inst_list tl)
in
match i with
| If (grd, thn, els) ->
(let e = match els with
| None -> ""
| Some instr -> "{\n" ^ (dump_instruction instr) ^ "\n}"
in sprintf "if (%s) {\n %s \n} %s" (dump_expr grd) (dump_instruction thn) e )
| StoreReg (reg, e) -> sprintf "%s = %s;" reg (dump_expr e)
| StoreMem (vh, am, e) ->
sprintf "%s.set%s(%s);" vh (AccessModes.pp_access_modes am) (dump_expr e)
| Fence barrier -> pp_barrier barrier
| DeclReg reg -> sprintf "%s;" reg
| Seq ins_l -> sprintf "%s" (dump_inst_list ins_l)
let dump_parsedInstruction = dump_instruction
and dump_instruction_hash = dump_instruction
let pp_instruction _mode = dump_instruction
let allowed_for_symb = List.map (fun x -> "r"^(string_of_int x))
(Misc.interval 0 64)
let fold_regs (_fc,_fs) acc _ins = acc
let map_regs _fc _fs ins = ins
let fold_addrs _f acc _ins = acc
let map_addrs _f ins = ins
let norm_ins ins = ins
let get_next _ins = Warn.fatal "Java get_next not implemented"
let is_valid _ = true
include Pseudo.Make
(struct
type ins = instruction
type pins = parsedInstruction
type reg_arg = reg
(* we currently don't do anything to the AST *)
(* let parsed_expr_tr instr = instr *)
let parsed_tr e = e
let get_naccesses i =
let rec aux_count_exp n = function
| Const _ -> n
| LoadReg _ -> n
| LoadMem _ -> n + 1
| CAS _ -> n + 3
| Rmw _ -> n + 2
| Op (_,e1,e2) -> aux_count_exp (aux_count_exp n e1) e2
and aux_count_ins n = function
| If (grd, thn, els) ->
(let k = (aux_count_exp n grd) in
match els with
| None -> aux_count_ins k thn
| Some ins -> aux_count_ins (aux_count_ins k thn) ins)
| StoreReg _ -> n
| StoreMem (_, _, e) -> (aux_count_exp n e) + 1
| Fence _ -> n
| DeclReg _ -> n
| Seq l -> aux_count_inst_list n l
and aux_count_inst_list n = function
| [] -> n
| hd :: tl -> aux_count_inst_list (aux_count_ins n hd) tl
in
aux_count_ins 0 i
let size_of_ins _ = 1
let fold_labels acc _f _ins = acc
let map_labels _f ins = ins
end)
let get_macro _ = assert false
let hash_pteval _ = assert false
let base_type = CType.Base "int"
let type_reg _ = base_type
module Instr = Instr.No(struct type instr = instruction end)
|
