blob: c0792df0da5f2ff5bcc14b367384a6f594323263 (
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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
(* 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;
Read_RISCV_acquire;
Read_RISCV_strong_acquire;
Read_RISCV_reserved;
Read_RISCV_reserved_acquire;
Read_RISCV_reserved_strong_acquire;
}
typedef write_kind = enumerate {
Write_plain;
Write_tag;
Write_conditional;
Write_release;
Write_exclusive;
Write_exclusive_release;
Write_RISCV_release;
Write_RISCV_strong_release;
Write_RISCV_conditional;
Write_RISCV_conditional_release;
Write_RISCV_conditional_strong_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;
Barrier_RISCV_rw_rw;
Barrier_RISCV_r_rw;
Barrier_RISCV_rw_w;
Barrier_RISCV_w_w;
Barrier_RISCV_i;
Barrier_x86_MFENCE;
}
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;
(read_kind, write_kind) IK_mem_rmw;
IK_cond_branch;
(trans_kind) IK_trans;
IK_simple
}
|
