-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathpsci_cpu_on.v
154 lines (150 loc) · 7.06 KB
/
psci_cpu_on.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
Require Import CodeDeps.
Require Import Ident.
Local Open Scope Z_scope.
Definition _addr := 1%positive.
Definition _context_id := 2%positive.
Definition _entry_point_address := 3%positive.
Definition _g_rec := 4%positive.
Definition _g_target_rec := 5%positive.
Definition _granule := 6%positive.
Definition _idx := 7%positive.
Definition _idx1 := 8%positive.
Definition _idx2 := 9%positive.
Definition _par_base := 10%positive.
Definition _par_end := 11%positive.
Definition _rec := 12%positive.
Definition _rec__1 := 13%positive.
Definition _ret := 14%positive.
Definition _target_cpu := 15%positive.
Definition _target_rec := 16%positive.
Definition _t'1 := 17%positive.
Definition _t'2 := 18%positive.
Definition _t'3 := 19%positive.
Definition _t'4 := 20%positive.
Definition _t'5 := 21%positive.
Definition _t'6 := 22%positive.
Definition _t'7 := 23%positive.
Definition _t'8 := 24%positive.
Definition psci_cpu_on_body :=
(Ssequence
(Ssequence
(Scall (Some _t'1)
(Evar _get_rec_par_base (Tfunction
(Tcons (tptr Tvoid) Tnil)
tulong cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Sset _par_base (Etempvar _t'1 tulong)))
(Ssequence
(Ssequence
(Scall (Some _t'2)
(Evar _get_rec_par_end (Tfunction
(Tcons (tptr Tvoid) Tnil)
tulong cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Sset _par_end (Etempvar _t'2 tulong)))
(Ssequence
(Sifthenelse (Ebinop Olt (Etempvar _entry_point_address tulong)
(Etempvar _par_base tulong) tint)
(Sset _t'8 (Econst_int (Int.repr 1) tint))
(Sset _t'8
(Ecast
(Ebinop Oge (Etempvar _entry_point_address tulong)
(Etempvar _par_end tulong) tint) tbool)))
(Sifthenelse (Etempvar _t'8 tint)
(Scall None
(Evar _set_psci_result_x0 (Tfunction (Tcons tulong Tnil) tvoid
cc_default))
((Econst_long (Int64.repr 4294967287) tulong) :: nil))
(Ssequence
(Ssequence
(Scall (Some _t'3)
(Evar _mpidr_to_rec_idx (Tfunction (Tcons tulong Tnil) tulong
cc_default))
((Etempvar _target_cpu tulong) :: nil))
(Sset _idx1 (Ecast (Etempvar _t'3 tulong) tuint)))
(Ssequence
(Ssequence
(Scall (Some _t'4)
(Evar _get_rec_rec_idx (Tfunction
(Tcons (tptr Tvoid)
Tnil) tulong cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Sset _idx2 (Ecast (Etempvar _t'4 tulong) tuint)))
(Sifthenelse (Ebinop Oeq (Etempvar _idx1 tuint)
(Etempvar _idx2 tuint) tint)
(Scall None
(Evar _set_psci_result_x0 (Tfunction (Tcons tulong Tnil)
tvoid cc_default))
((Econst_long (Int64.repr 4294967292) tulong) :: nil))
(Ssequence
(Ssequence
(Scall (Some _t'5)
(Evar _psci_lookup_target (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong Tnil))
(tptr Tvoid)
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _target_cpu tulong) :: nil))
(Sset _g_target_rec
(Etempvar _t'5 (tptr Tvoid))))
(Ssequence
(Scall (Some _t'7)
(Evar _is_null (Tfunction (Tcons (tptr Tvoid) Tnil) tuint
cc_default))
((Etempvar _g_target_rec (tptr Tvoid)) ::
nil))
(Sifthenelse (Ebinop Oeq (Etempvar _t'7 tuint)
(Econst_int (Int.repr 1) tuint) tint)
(Scall None
(Evar _set_psci_result_x0 (Tfunction
(Tcons tulong Tnil) tvoid
cc_default))
((Econst_long (Int64.repr 4294967294) tulong) :: nil))
(Ssequence
(Ssequence
(Scall (Some _t'6)
(Evar _granule_map (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tuint Tnil))
(tptr Tvoid) cc_default))
((Etempvar _g_target_rec (tptr Tvoid)) ::
(Econst_int (Int.repr 4) tuint) :: nil))
(Sset _target_rec (Etempvar _t'6 (tptr Tvoid))))
(Scall None
(Evar _psci_cpu_on_target (Tfunction
(Tcons
(tptr Tvoid)
(Tcons
(tptr Tvoid)
(Tcons
(tptr Tvoid)
(Tcons tulong
(Tcons tulong
Tnil))))) tvoid
cc_default))
((Etempvar _g_target_rec (tptr Tvoid)) ::
(Etempvar _target_rec (tptr Tvoid)) ::
(Etempvar _rec (tptr Tvoid)) ::
(Etempvar _entry_point_address tulong) ::
(Etempvar _target_cpu tulong) :: nil)))))))))))))
.
Definition f_psci_cpu_on := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_rec, (tptr Tvoid)) ::
(_target_cpu, tulong) :: (_entry_point_address, tulong) ::
(_context_id, tulong) :: nil);
fn_vars := nil;
fn_temps := ((_g_target_rec, (tptr Tvoid)) ::
(_target_rec, (tptr Tvoid)) ::
(_par_base, tulong) :: (_par_end, tulong) ::
(_g_rec, (tptr Tvoid)) ::
(_idx1, tuint) :: (_idx2, tuint) :: (_t'8, tint) ::
(_t'7, tuint) :: (_t'6, (tptr Tvoid)) ::
(_t'5, (tptr Tvoid)) :: (_t'4, tulong) ::
(_t'3, tulong) :: (_t'2, tulong) :: (_t'1, tulong) :: nil);
fn_body := psci_cpu_on_body
|}.