-
Notifications
You must be signed in to change notification settings - Fork 1
/
psci_rsi.v
162 lines (158 loc) · 8.12 KB
/
psci_rsi.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
158
159
160
161
162
Require Import CodeDeps.
Require Import Ident.
Local Open Scope Z_scope.
Definition _arg0 := 1%positive.
Definition _arg1 := 2%positive.
Definition _arg2 := 3%positive.
Definition _function_id := 4%positive.
Definition _i := 5%positive.
Definition _rec := 6%positive.
Definition _rec__1 := 7%positive.
Definition _ret := 8%positive.
Definition _t'1 := 9%positive.
Definition psci_rsi_body :=
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592512) tulong) tint)
(Scall None
(Evar _psci_version (Tfunction (Tcons (tptr Tvoid) Tnil)
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Ssequence
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592513) tulong) tint)
(Sset _t'1 (Econst_int (Int.repr 1) tint))
(Sset _t'1
(Ecast
(Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 3288334337) tulong) tint) tbool)))
(Sifthenelse (Etempvar _t'1 tint)
(Scall None
(Evar _psci_cpu_suspend (Tfunction
(Tcons (tptr Tvoid)
(Tcons tulong (Tcons tulong Tnil))) tvoid
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _arg0 tulong) :: (Etempvar _arg1 tulong) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592514) tulong) tint)
(Scall None
(Evar _psci_cpu_off (Tfunction
(Tcons (tptr Tvoid) Tnil)
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592515) tulong) tint)
(Ssequence
(Sset _arg0 (Ecast (Ecast (Etempvar _arg0 tulong) tuint) tulong))
(Ssequence
(Sset _arg1
(Ecast (Ecast (Etempvar _arg1 tulong) tuint) tulong))
(Ssequence
(Sset _arg2
(Ecast (Ecast (Etempvar _arg2 tulong) tuint) tulong))
(Scall None
(Evar _psci_cpu_on (Tfunction
(Tcons (tptr Tvoid)
(Tcons tulong
(Tcons tulong (Tcons tulong Tnil))))
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _arg0 tulong) :: (Etempvar _arg1 tulong) ::
(Etempvar _arg2 tulong) :: nil)))))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 3288334339) tulong) tint)
(Scall None
(Evar _psci_cpu_on (Tfunction
(Tcons (tptr Tvoid)
(Tcons tulong
(Tcons tulong (Tcons tulong Tnil))))
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _arg0 tulong) :: (Etempvar _arg1 tulong) ::
(Etempvar _arg2 tulong) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592516) tulong) tint)
(Ssequence
(Sset _arg0
(Ecast (Ecast (Etempvar _arg0 tulong) tuint) tulong))
(Ssequence
(Sset _arg1
(Ecast (Ecast (Etempvar _arg1 tulong) tuint) tulong))
(Scall None
(Evar _psci_affinity_info (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong
(Tcons tulong Tnil)))
tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _arg0 tulong) :: (Etempvar _arg1 tulong) ::
nil))))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 3288334340) tulong)
tint)
(Scall None
(Evar _psci_affinity_info (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tulong
(Tcons tulong Tnil))) tvoid
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _arg0 tulong) :: (Etempvar _arg1 tulong) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592520) tulong)
tint)
(Scall None
(Evar _psci_system_off (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) :: nil))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592521) tulong)
tint)
(Scall None
(Evar _psci_system_reset (Tfunction
(Tcons
(tptr Tvoid)
Tnil) tvoid cc_default))
((Etempvar _rec (tptr Tvoid)) ::
nil))
(Sifthenelse (Ebinop Oeq (Etempvar _function_id tuint)
(Econst_long (Int64.repr 2214592522) tulong)
tint)
(Scall None
(Evar _psci_features (Tfunction
(Tcons
(tptr Tvoid)
(Tcons tuint Tnil)) tvoid
cc_default))
((Etempvar _rec (tptr Tvoid)) ::
(Etempvar _arg0 tulong) :: nil))
(Ssequence
(Scall None
(Evar _set_psci_result_x0 (Tfunction
(Tcons tulong Tnil)
tvoid cc_default))
((Econst_long (Int64.repr 4294967295) tulong) ::
nil))
(Scall None
(Evar _set_psci_result_forward_psci_call (Tfunction
(Tcons
tuint
Tnil)
tvoid
cc_default))
((Econst_int (Int.repr 0) tuint) :: nil))))))))))))))
.
Definition f_psci_rsi := {|
fn_return := tvoid;
fn_callconv := cc_default;
fn_params := ((_rec, (tptr Tvoid)) ::
(_function_id, tuint) :: (_arg0, tulong) ::
(_arg1, tulong) :: (_arg2, tulong) :: nil);
fn_vars := nil;
fn_temps := ((_t'1, tint) :: nil);
fn_body := psci_rsi_body
|}.