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
|
/* Moved and tightened an assertion */
val aarch64_memory_exclusive_pair : forall ('datasize : Int) ('regsize : Int) ('elsize : Int).
(AccType, atom('datasize), atom('elsize), MemOp, int, bool, atom('regsize), int, int, int) -> unit effect {escape, undef, rreg, wreg, rmem, wmem}
function aarch64_memory_exclusive_pair (acctype, datasize, elsize, memop, n, pair, regsize, s, t, t2) = {
assert(constraint('regsize >= 0), "regsize constraint");
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
address : bits(64) = undefined;
data : bits('datasize) = undefined;
rt_unknown : bool = false;
rn_unknown : bool = false;
if (memop == MemOp_LOAD & pair) & t == t2 then {
c : Constraint = ConstrainUnpredictable(Unpredictable_LDPOVERLAP);
assert(c == Constraint_UNKNOWN | c == Constraint_UNDEF | c == Constraint_NOP, "((c == Constraint_UNKNOWN) || ((c == Constraint_UNDEF) || (c == Constraint_NOP)))");
match c {
Constraint_UNKNOWN => rt_unknown = true,
Constraint_UNDEF => UnallocatedEncoding(),
Constraint_NOP => EndOfInstruction()
}
} else ();
if memop == MemOp_STORE then {
if s == t | pair & s == t2 then {
c : Constraint = ConstrainUnpredictable(Unpredictable_DATAOVERLAP);
assert(c == Constraint_UNKNOWN | c == Constraint_NONE | c == Constraint_UNDEF | c == Constraint_NOP, "((c == Constraint_UNKNOWN) || ((c == Constraint_NONE) || ((c == Constraint_UNDEF) || (c == Constraint_NOP))))");
match c {
Constraint_UNKNOWN => rt_unknown = true,
Constraint_NONE => rt_unknown = false,
Constraint_UNDEF => UnallocatedEncoding(),
Constraint_NOP => EndOfInstruction()
}
} else ();
if s == n & n != 31 then {
c : Constraint = ConstrainUnpredictable(Unpredictable_BASEOVERLAP);
assert(c == Constraint_UNKNOWN | c == Constraint_NONE | c == Constraint_UNDEF | c == Constraint_NOP, "((c == Constraint_UNKNOWN) || ((c == Constraint_NONE) || ((c == Constraint_UNDEF) || (c == Constraint_NOP))))");
match c {
Constraint_UNKNOWN => rn_unknown = true,
Constraint_NONE => rn_unknown = false,
Constraint_UNDEF => UnallocatedEncoding(),
Constraint_NOP => EndOfInstruction()
}
} else ()
} else ();
if n == 31 then {
CheckSPAlignment();
address = aget_SP()
} else if rn_unknown then address = undefined
else address = aget_X(n);
secondstage : bool = undefined;
iswrite : bool = undefined;
match memop {
MemOp_STORE => {
if rt_unknown then data = undefined
else if pair then let 'v = ex_int(datasize / 2) in {
assert(constraint(2 * 'v = 'datasize));
el1 : bits('v) = aget_X(t);
el2 : bits('v) = aget_X(t2);
data = if BigEndian() then el1 @ el2 else el2 @ el1
} else data = aget_X(t);
status : bits(1) = 0b1;
if AArch64_ExclusiveMonitorsPass(address, dbytes) then {
aset_Mem(address, dbytes, acctype, data);
status = ExclusiveMonitorsStatus()
} else ();
aset_X(s, ZeroExtend(status, 32))
},
MemOp_LOAD => {
AArch64_SetExclusiveMonitors(address, dbytes);
if pair then
if rt_unknown then aset_X(t, undefined : bits(32)) else if elsize == 32 then {
assert(constraint(- 'elsize + 'datasize > 0 & 'elsize >= 0), "datasize constraint");
data = aget_Mem(address, dbytes, acctype);
if BigEndian() then {
aset_X(t, slice(data, elsize, negate(elsize) + datasize));
aset_X(t2, slice(data, 0, elsize))
} else {
aset_X(t, slice(data, 0, elsize));
aset_X(t2, slice(data, elsize, negate(elsize) + datasize))
}
} else {
if address != Align(address, dbytes) then {
iswrite = false;
secondstage = false;
AArch64_Abort(address, AArch64_AlignmentFault(acctype, iswrite, secondstage))
} else ();
aset_X(t, aget_Mem(address + 0, 8, acctype));
aset_X(t2, aget_Mem(address + 8, 8, acctype))
}
else {
data = aget_Mem(address, dbytes, acctype);
aset_X(t, ZeroExtend(data, regsize))
}
}
}
}
|
