-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathhandle_data_abort.v
157 lines (153 loc) · 6.89 KB
/
handle_data_abort.v
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
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import RealmSyncHandlerAux.Spec.
Local Open Scope Z_scope.
Section SpecLow.
Definition handle_data_abort_spec0 (rec: Pointer) (esr: Z64) (adt: RData) : option RData :=
match rec, esr with
| (_rec_base, _rec_ofst), VZ64 _esr =>
let _far := 0 in
when' _hpfar == sysreg_read_spec 85 adt;
rely is_int64 _hpfar;
let _write_val := 0 in
when' _spsr == sysreg_read_spec 94 adt;
rely is_int64 _spsr;
rely is_int64 (Z.land _spsr 16);
if (negb ((Z.land _spsr 16) =? 0)) then
rely is_int64 (Z.land _esr 18446744073692774399);
let _esr := (Z.land _esr 18446744073692774399) in
rely is_int64 (Z.land _esr 16777216);
if ((Z.land _esr 16777216) =? 0) then
let _t'6 := 1 in
rely is_int64 (Z.lor 4227858432 63);
rely is_int64 (Z.land _esr (Z.lor 4227858432 63));
let _esr := (Z.land _esr (Z.lor 4227858432 63)) in
rely is_int64 _esr;
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
rely is_int64 _write_val;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
else
rely is_int64 _esr;
when _t'7 == access_in_par_spec (_rec_base, _rec_ofst) (VZ64 _hpfar) (VZ64 _esr) adt;
rely is_int _t'7;
let _t'6 := (_t'7 =? 0) in
if _t'6 then
rely is_int64 (Z.lor 4227858432 63);
rely is_int64 (Z.land _esr (Z.lor 4227858432 63));
let _esr := (Z.land _esr (Z.lor 4227858432 63)) in
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
rely is_int64 _write_val;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
else
when adt == set_rec_last_run_info_esr_spec (_rec_base, _rec_ofst) (VZ64 _esr) adt;
when _t'4 == esr_is_write_spec (VZ64 _esr) adt;
rely is_int _t'4;
if (_t'4 =? 1) then
when' _write_val == get_write_value_spec (_rec_base, _rec_ofst) (VZ64 _esr) adt;
rely is_int64 _write_val;
when' _t'5 == sysreg_read_spec 83 adt;
rely is_int64 _t'5;
rely is_int64 (Z.land _t'5 4095);
let _far := (Z.land _t'5 4095) in
rely is_int64 (Z.land _esr 4095);
let _esr := (Z.land _esr 4095) in
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
else
when' _t'5 == sysreg_read_spec 83 adt;
rely is_int64 _t'5;
rely is_int64 (Z.land _t'5 4095);
let _far := (Z.land _t'5 4095) in
rely is_int64 (Z.land _esr 4095);
let _esr := (Z.land _esr 4095) in
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
rely is_int64 _write_val;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
else
rely is_int64 (Z.land _esr 16777216);
if ((Z.land _esr 16777216) =? 0) then
let _t'6 := 1 in
rely is_int64 (Z.lor 4227858432 63);
rely is_int64 (Z.land _esr (Z.lor 4227858432 63));
let _esr := (Z.land _esr (Z.lor 4227858432 63)) in
rely is_int64 _esr;
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
rely is_int64 _write_val;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
else
rely is_int64 _esr;
when _t'7 == access_in_par_spec (_rec_base, _rec_ofst) (VZ64 _hpfar) (VZ64 _esr) adt;
rely is_int _t'7;
let _t'6 := (_t'7 =? 0) in
if _t'6 then
rely is_int64 (Z.lor 4227858432 63);
rely is_int64 (Z.land _esr (Z.lor 4227858432 63));
let _esr := (Z.land _esr (Z.lor 4227858432 63)) in
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
rely is_int64 _write_val;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
else
when adt == set_rec_last_run_info_esr_spec (_rec_base, _rec_ofst) (VZ64 _esr) adt;
when _t'4 == esr_is_write_spec (VZ64 _esr) adt;
rely is_int _t'4;
if (_t'4 =? 1) then
when' _write_val == get_write_value_spec (_rec_base, _rec_ofst) (VZ64 _esr) adt;
rely is_int64 _write_val;
when' _t'5 == sysreg_read_spec 83 adt;
rely is_int64 _t'5;
rely is_int64 (Z.land _t'5 4095);
let _far := (Z.land _t'5 4095) in
rely is_int64 (Z.land _esr 4095);
let _esr := (Z.land _esr 4095) in
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
else
when' _t'5 == sysreg_read_spec 83 adt;
rely is_int64 _t'5;
rely is_int64 (Z.land _t'5 4095);
let _far := (Z.land _t'5 4095) in
rely is_int64 (Z.land _esr 4095);
let _esr := (Z.land _esr 4095) in
when adt == set_rec_run_esr_spec (VZ64 _esr) adt;
rely is_int64 _far;
when adt == set_rec_run_far_spec (VZ64 _far) adt;
when adt == set_rec_run_hpfar_spec (VZ64 _hpfar) adt;
rely is_int64 _write_val;
when adt == set_rec_run_emulated_write_val_spec (VZ64 _write_val) adt;
Some adt
end
.
End SpecLow.