-
Notifications
You must be signed in to change notification settings - Fork 1
/
psci_rsi.v
154 lines (131 loc) · 8.49 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
Require Import CodeProofDeps.
Require Import Ident.
Require Import Constants.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import CommonLib.
Require Import PSCI.Spec.
Require Import AbsAccessor.Spec.
Require Import PSCI.Layer.
Require Import PSCIHandler.Code.psci_rsi.
Require Import PSCIHandler.LowSpecs.psci_rsi.
Local Open Scope Z_scope.
Section CodeProof.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Let L : compatlayer (cdata RData) :=
_psci_version ↦ gensem psci_version_spec
⊕ _psci_cpu_suspend ↦ gensem psci_cpu_suspend_spec
⊕ _psci_cpu_off ↦ gensem psci_cpu_off_spec
⊕ _psci_cpu_on ↦ gensem psci_cpu_on_spec
⊕ _psci_affinity_info ↦ gensem psci_affinity_info_spec
⊕ _psci_system_off ↦ gensem psci_system_off_spec
⊕ _psci_system_reset ↦ gensem psci_system_reset_spec
⊕ _psci_features ↦ gensem psci_features_spec
⊕ _set_psci_result_x0 ↦ gensem set_psci_result_x0_spec
⊕ _set_psci_result_forward_psci_call ↦ gensem set_psci_result_forward_psci_call_spec
.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_psci_version: block.
Hypothesis h_psci_version_s : Genv.find_symbol ge _psci_version = Some b_psci_version.
Hypothesis h_psci_version_p : Genv.find_funct_ptr ge b_psci_version
= Some (External (EF_external _psci_version
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque psci_version_spec.
Variable b_psci_cpu_suspend: block.
Hypothesis h_psci_cpu_suspend_s : Genv.find_symbol ge _psci_cpu_suspend = Some b_psci_cpu_suspend.
Hypothesis h_psci_cpu_suspend_p : Genv.find_funct_ptr ge b_psci_cpu_suspend
= Some (External (EF_external _psci_cpu_suspend
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default).
Local Opaque psci_cpu_suspend_spec.
Variable b_psci_cpu_off: block.
Hypothesis h_psci_cpu_off_s : Genv.find_symbol ge _psci_cpu_off = Some b_psci_cpu_off.
Hypothesis h_psci_cpu_off_p : Genv.find_funct_ptr ge b_psci_cpu_off
= Some (External (EF_external _psci_cpu_off
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque psci_cpu_off_spec.
Variable b_psci_cpu_on: block.
Hypothesis h_psci_cpu_on_s : Genv.find_symbol ge _psci_cpu_on = Some b_psci_cpu_on.
Hypothesis h_psci_cpu_on_p : Genv.find_funct_ptr ge b_psci_cpu_on
= Some (External (EF_external _psci_cpu_on
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong (Tcons tulong Tnil)))) tvoid cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong (Tcons tulong Tnil)))) tvoid cc_default).
Local Opaque psci_cpu_on_spec.
Variable b_psci_affinity_info: block.
Hypothesis h_psci_affinity_info_s : Genv.find_symbol ge _psci_affinity_info = Some b_psci_affinity_info.
Hypothesis h_psci_affinity_info_p : Genv.find_funct_ptr ge b_psci_affinity_info
= Some (External (EF_external _psci_affinity_info
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tvoid cc_default).
Local Opaque psci_affinity_info_spec.
Variable b_psci_system_off: block.
Hypothesis h_psci_system_off_s : Genv.find_symbol ge _psci_system_off = Some b_psci_system_off.
Hypothesis h_psci_system_off_p : Genv.find_funct_ptr ge b_psci_system_off
= Some (External (EF_external _psci_system_off
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque psci_system_off_spec.
Variable b_psci_system_reset: block.
Hypothesis h_psci_system_reset_s : Genv.find_symbol ge _psci_system_reset = Some b_psci_system_reset.
Hypothesis h_psci_system_reset_p : Genv.find_funct_ptr ge b_psci_system_reset
= Some (External (EF_external _psci_system_reset
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque psci_system_reset_spec.
Variable b_psci_features: block.
Hypothesis h_psci_features_s : Genv.find_symbol ge _psci_features = Some b_psci_features.
Hypothesis h_psci_features_p : Genv.find_funct_ptr ge b_psci_features
= Some (External (EF_external _psci_features
(signature_of_type (Tcons Tptr (Tcons tuint Tnil)) tvoid cc_default))
(Tcons Tptr (Tcons tuint Tnil)) tvoid cc_default).
Local Opaque psci_features_spec.
Variable b_set_psci_result_x0: block.
Hypothesis h_set_psci_result_x0_s : Genv.find_symbol ge _set_psci_result_x0 = Some b_set_psci_result_x0.
Hypothesis h_set_psci_result_x0_p : Genv.find_funct_ptr ge b_set_psci_result_x0
= Some (External (EF_external _set_psci_result_x0
(signature_of_type (Tcons tulong Tnil) tvoid cc_default))
(Tcons tulong Tnil) tvoid cc_default).
Local Opaque set_psci_result_x0_spec.
Variable b_set_psci_result_forward_psci_call: block.
Hypothesis h_set_psci_result_forward_psci_call_s : Genv.find_symbol ge _set_psci_result_forward_psci_call = Some b_set_psci_result_forward_psci_call.
Hypothesis h_set_psci_result_forward_psci_call_p : Genv.find_funct_ptr ge b_set_psci_result_forward_psci_call
= Some (External (EF_external _set_psci_result_forward_psci_call
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Local Opaque set_psci_result_forward_psci_call_spec.
Lemma psci_rsi_body_correct:
forall m d d' env le rec_base rec_offset function_id arg0 arg1 arg2
(Henv: env = PTree.empty _)
(Hinv: high_level_invariant d)
(HPTrec: PTree.get _rec le = Some (Vptr rec_base (Int.repr rec_offset)))
(HPTfunction_id: PTree.get _function_id le = Some (Vint function_id))
(HPTarg0: PTree.get _arg0 le = Some (Vlong arg0))
(HPTarg1: PTree.get _arg1 le = Some (Vlong arg1))
(HPTarg2: PTree.get _arg2 le = Some (Vlong arg2))
(Hspec: psci_rsi_spec0 (rec_base, rec_offset) (Int.unsigned function_id) (VZ64 (Int64.unsigned arg0)) (VZ64 (Int64.unsigned arg1)) (VZ64 (Int64.unsigned arg2)) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) psci_rsi_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec psci_rsi_body; eexists; solve_proof_low;
repeat (repeat sstep; try big_vcgen;
match goal with
| [H: ?a = ?c |- context[zeq ?a ?b]] =>
destruct (zeq a b); try omega
| _ => idtac
end).
Qed.
End BodyProof.
End CodeProof.