blob: fb15310a45ffe7ae17fb0da9b4e4fe572ed36104 (
plain)
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
|
(* iR : input registers,
* oR : output registers,
* aR : registers feeding into the memory address *)
(* branch instructions currently are not writing to NIA *)
typedef regfp = const union {
(string) RFull;
(string,nat,nat) RSlice;
(string,nat) RSliceBit;
(string,string) RField;
}
typedef regfps = list <regfp>
typedef niafp = const union {
NIAFP_successor;
(bit[64]) NIAFP_concrete_address;
NIAFP_LR;
NIAFP_CTR;
(regfp) NIAFP_register;
}
typedef niafps = list <niafp>
(* only for MIPS *)
typedef diafp = const union {
DIAFP_none;
(bit[64]) DIAFP_concrete;
(regfp) DIAFP_reg;
}
typedef read_kind = enumerate {
Read_plain;
Read_tag;
Read_reserve;
Read_acquire;
Read_exclusive;
Read_exclusive_acquire;
Read_stream
}
typedef write_kind = enumerate {
Write_plain;
Write_tag;
Write_conditional;
Write_release;
Write_exclusive;
Write_exclusive_release;
}
typedef barrier_kind = enumerate {
Barrier_Sync;
Barrier_LwSync;
Barrier_Eieio;
Barrier_Isync;
Barrier_DMB;
Barrier_DMB_ST;
Barrier_DMB_LD;
Barrier_DSB;
Barrier_DSB_ST;
Barrier_DSB_LD;
Barrier_ISB;
Barrier_MIPS_SYNC;
}
typedef trans_kind = enumerate {
Transaction_start; Transaction_commit; Transaction_abort;
}
typedef instruction_kind = const union {
(barrier_kind) IK_barrier;
(read_kind) IK_mem_read;
(write_kind) IK_mem_write;
IK_cond_branch;
(trans_kind) IK_trans;
IK_simple
}
|
