1 | \section{A Modular Approach to the Correctness of the Graph Passes} |
---|
2 | \label{modular} |
---|
3 | |
---|
4 | We will now outline how the proof can be carried out generally in the |
---|
5 | graph passes of the back-end that share the \verb+joint+ language interface. |
---|
6 | |
---|
7 | An instance of the record \verb=sem_graph_params= contains all common information about |
---|
8 | programs of a joint-language whose source code can be logically organized as a graph. |
---|
9 | Thus, every program of this kind will be an inhabitant of the type \verb=joint_program p=, |
---|
10 | where \verb=p= is an instance of \verb=sem_graph_params=. We want to stress that such a record |
---|
11 | is in a sub-type relation with the record \verb=params=, which was explained in Deliverable 4.3. |
---|
12 | |
---|
13 | In order to establish the correctness of our cost-model in each compiler's back-end pass, where |
---|
14 | both source and target programs are joint-graph-programs, i.e.\ the source program \verb=src= |
---|
15 | (resp.\ the target program \verb=out=) is such that there is a \verb=p_in= |
---|
16 | (resp.\ \verb=p_out=) of type \verb=sem_graph_params= such that |
---|
17 | \verb=src : joint_program p_in= (resp.\ \verb=out : joint_program p_out=), we would like to |
---|
18 | prove a statement similar to this shape. |
---|
19 | \begin{lstlisting} |
---|
20 | theorem joint_correctness : ∀p_in,p_out : sem_graph_params. |
---|
21 | ∀prog : joint_program p_in.∀stack_size. |
---|
22 | let trans_prog ≝ transform_program … prog in |
---|
23 | ∀init_in. |
---|
24 | make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → |
---|
25 | ∃init_out. |
---|
26 | make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧ |
---|
27 | ∃[1] R : status_rel (joint_abstract_status (mk_prog_params p_in prog stack_size)) |
---|
28 | (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)). |
---|
29 | status_simulation_with_init |
---|
30 | (joint_abstract_status (mk_prog_params p_in prog stack_size)) |
---|
31 | (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)) |
---|
32 | R init_in init_out. |
---|
33 | \end{lstlisting} |
---|
34 | When proving this statement (for each concrete instance of language), |
---|
35 | we need to proceed by cases according the classification of |
---|
36 | each state in the source program (\verb=cl_jmp=, \verb=cl_other=, \verb=cl_call= and |
---|
37 | \verb=cl_return=) and then prove the suitable conditions explained in |
---|
38 | \cite{simulation}, according to the case we are currently considering (Condition 1 for |
---|
39 | \verb=cl_other= and \verb=cl_jump= case, Condition 2 for \verb=cl_call= or |
---|
40 | Condition 3 for \verb=cl_return= case). Roughly speaking, proving these conditions |
---|
41 | means producing traces of some kind in the target language that are in a suitable |
---|
42 | correspondence with an execution step in the source language. |
---|
43 | |
---|
44 | Since traces carry both extensional and intensional information, the main disadvantage |
---|
45 | with this approach is that the extensional part of the proof (for example |
---|
46 | the preservation the semantic relation between states of the program under evaluation) |
---|
47 | and the intensional part (for example, all proof obligation dealing with |
---|
48 | the presence of a cost label in some point of the code) are mixed together in a not very clear way. |
---|
49 | |
---|
50 | Furthermore, some proof obligations concerning the relation among program counters |
---|
51 | (for example, the call relation between states which is one of the field of |
---|
52 | \verb=status_rel= record) depend only on the way the translation from source to target program is done. |
---|
53 | In particular if the translation satisfies some suitable properties, then it is possible |
---|
54 | to define some ``standard relations'' that automatically satisfy these proof obligations, |
---|
55 | in an independent way from the specific source and target languages. |
---|
56 | |
---|
57 | So our question is whether there is a way to use these observation in order to factorize all common |
---|
58 | aspects of all correctness proofs of each pass involving joint languages. |
---|
59 | The aim is having a layer on top of the one talking about traces, that ask the user wishing to prove |
---|
60 | the correctness of a single pass involving two joint-languages, to provide some semantic state relation that |
---|
61 | satisfies some conditions. These conditions never speak about traces and they are mostly |
---|
62 | extensional, with the intensional part being limited to some additional required properties of |
---|
63 | the translation. This layer will use the trace machinery in order to deliver the desired correctness |
---|
64 | proof of the pass. |
---|
65 | |
---|
66 | In order to reach this goal, we have to analyse first whether there is a common way to perform language |
---|
67 | translation for each pass. After having defined and specified the translation machinery, we will |
---|
68 | explain how it is possible to use it in order to build such a layer. So this section is organized as follows: |
---|
69 | in the first part we explain the translation machinery while in the second part we explain such a layer. |
---|
70 | |
---|
71 | \subsection{Graph translation} |
---|
72 | Since a program is just a collection of functions, the compositional approach suggests us to define the |
---|
73 | translation of a program in terms of the way we translate each internal function. Thus, if we let |
---|
74 | \verb=src_g_pars= and \verb=dst_g_pars= being the graph parameters of respectively the source and |
---|
75 | the target program, the aim is writing a \s{matita}'s function that takes as input an object of type |
---|
76 | \verb=joint_closed_internal_function src_g_pars= together with additional information |
---|
77 | (that we will explain better later) and gives as output an object of type |
---|
78 | \verb=joint_closed_internal_function dst_g_pars= with some properties, that corresponds |
---|
79 | to the result of the translation (for the definition of \verb=joint_closed_internal_function=, see |
---|
80 | Deliverable 4.2 and 4.3) . The signature of the definition is the following one. |
---|
81 | \begin{lstlisting} |
---|
82 | definition b_graph_translate : |
---|
83 | ∀src_g_pars,dst_g_pars : graph_params. |
---|
84 | ∀globals: list ident. |
---|
85 | ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals. |
---|
86 | ∀def_in : joint_closed_internal_function src_g_pars globals. |
---|
87 | Σdef_out : joint_closed_internal_function dst_g_pars globals. |
---|
88 | ∃data',regs,f_lbls,f_regs. |
---|
89 | bind_new_instantiates ?? data' data regs ∧ |
---|
90 | b_graph_translate_props … data' def_in def_out f_lbls f_regs. |
---|
91 | \end{lstlisting} |
---|
92 | |
---|
93 | Let us now discuss in detail what are the parameter to be provide in input and what is the output of the |
---|
94 | translation process. |
---|
95 | |
---|
96 | \subsubsection{Input requested by the translation process} |
---|
97 | Clearly, \verb=b_graph_translate= takes as input the internal function of the source language we want to translate. |
---|
98 | But it also takes in input some useful information which will be used in order to dictate the translation process. |
---|
99 | These informations are all contained in an instance of the following record, |
---|
100 | where we skip some technical details. |
---|
101 | |
---|
102 | \begin{lstlisting} |
---|
103 | record b_graph_translate_data |
---|
104 | (src, dst : graph_params) |
---|
105 | (globals : list ident) : Type[0] ≝ |
---|
106 | { init_ret : call_dest dst |
---|
107 | ; init_params : paramsT dst |
---|
108 | ; init_stack_size : ℕ |
---|
109 | ; added_prologue : list (joint_seq dst globals) |
---|
110 | ; new_regs : list register |
---|
111 | ; f_step : label → joint_step src globals → bind_step_block dst globals |
---|
112 | ; f_fin : label → joint_fin_step src → bind_fin_block dst globals |
---|
113 | ; good_f_step : … |
---|
114 | ; good_f_fin : … |
---|
115 | ; f_step_on_cost : |
---|
116 | ∀l,c.f_step l (COST_LABEL … c) = |
---|
117 | bret ? (step_block ??) 〈 [ ], λ_.COST_LABEL dst globals c, [ ] 〉 |
---|
118 | ; cost_in_f_step : |
---|
119 | ∀l,s,c. |
---|
120 | bind_new_P ?? |
---|
121 | (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c → |
---|
122 | s = COST_LABEL … c) (f_step l s) |
---|
123 | } |
---|
124 | \end{lstlisting} |
---|
125 | \autoref{tab:translate_data} summarizes what each field means and how it is used in the translation process. We will say that an identifier of |
---|
126 | a pseudo-register (resp.\ a code label) is {\em fresh} when it never appears in the code of the source function. |
---|
127 | \begin{table} |
---|
128 | \centering |
---|
129 | \begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}} |
---|
130 | Field & Explanation \\[5pt] |
---|
131 | \hline |
---|
132 | \texttt{init\_ret} & It tells where the result for the translated function is stored.\\[5pt] |
---|
133 | \texttt{init\_params} & It tells what is the translation of the formal parameters.\\[5pt] |
---|
134 | \texttt{init\_stack\_size} & It tells how to fill the field \texttt{joint\_if\_stacksize} of the translated function, which tells how much stack is required by the function at the given stage of compilation. \\[5pt] |
---|
135 | \texttt{added\_prologue} & It is a list of sequential statements of the target language which is always added at the beginning of the translated function. \\[5pt] |
---|
136 | \texttt{new\_regs} & It is a list of identifiers for fresh pseudo-registers that are generated when instantiating |
---|
137 | this record. They are typically used to store data that must be saved across the call (e.g.\ the return address |
---|
138 | popped from the internal stack).\\[5pt] |
---|
139 | \texttt{f\_step} & It is a function that tells how to translate all {\em step statements} i.e.\ statements admitting a syntactical successor. Statements of this kind are sequential statements, a cost emission statement, a call statement or a conditional statement: in the two latter cases the syntactical successors are respectively the returning address (at the end of a function call) and the point where the flow will continue in case the guard is false. \\[5pt] |
---|
140 | \texttt{f\_fin} & As above, but for {\em final statements} i.e.\ statements do not admitting a syntactical successor. Statements of this kind are return and unconditioned jump statements.\\[5pt] |
---|
141 | \texttt{good\_f\_step} & It tells that the translation function of all step statement is well formed in the sense that |
---|
142 | the block \verb=f_step I= for a step \verb=I= only uses code labels and register appearing in \verb=I=, \verb=new_regs= or generated by the appropriate identifier universe fields of the translated function. \\[5pt] |
---|
143 | \texttt{good\_f\_fin} & As above, but for \verb=f_fin=.\\[5pt] |
---|
144 | \texttt{f\_step\_on\_cost}, \texttt{cost\_in\_f\_step}& They give a particular restriction on the translation of a cost-emission statement: it tells that the translation of a cost-emission has to be the identity, i.e.\ it should be translated as the same cost-emission statement. Furthermore, the translation never introduce new cost-emission statements which do not correspond to a cost emission in the source.\\[5pt] |
---|
145 | \end{tabular*} |
---|
146 | \caption{The explanation of the various fields of the \verb=b_graph_translate_data= record.} |
---|
147 | \label{tab:translate_data} |
---|
148 | \end{table} |
---|
149 | |
---|
150 | \subsubsection{Output given the translation process} |
---|
151 | Clearly \verb=g_graph_translate= gives in output the translated internal function. Unfortunately, |
---|
152 | for what we are going to develop later, this information is insufficient because we need some information |
---|
153 | about the correspondence between the source internal function and the translated one. Such an information |
---|
154 | is given by the second component of the $\Sigma$-type returned by the translation process. |
---|
155 | We remind that the return type of \verb=b_graph_translate= is the following. |
---|
156 | \begin{lstlisting} |
---|
157 | Σdef_out : joint_closed_internal_function dst_g_pars globals. |
---|
158 | ∃data',regs,f_lbls,f_regs. |
---|
159 | bind_new_instantiates ?? data' data regs ∧ |
---|
160 | b_graph_translate_props … data' def_in def_out f_lbls f_regs. |
---|
161 | \end{lstlisting} |
---|
162 | The correspondence between the source internal function and the translated one is made explicit by two functions: |
---|
163 | \verb=f_lbls : code_point src_g_pars → list (code_point dst_g_pars)= and |
---|
164 | \verb=f_regs : code_point src_g_pars → list (register)=. To understand their meaning, we need to stress the |
---|
165 | fact that the translation process translates every statement appearing in the code of the source internal function |
---|
166 | in a given code point $l$ into a block of statements in the code of the translated function where the first |
---|
167 | instruction of the block has $l$ as code point identifier and all succeeding instructions of the block have |
---|
168 | fresh code points identifiers. Furthermore statements of this block may use fresh identifiers of pseudo-registers or |
---|
169 | (even worse) they may use some fresh code-point identifiers being generated by the translation (we will see later |
---|
170 | that this will be important when translating a call statement). We will use the above mentioned functions |
---|
171 | to retrieve this information. \verb=f_lbls= takes in input an identifier $l$ for a code point in the |
---|
172 | source code and it gives back the list of all fresh code point identifiers generated by the translation process |
---|
173 | of the statement in the source located in $l$. \verb=f_regs= takes in input an identifier $l$ for a code point |
---|
174 | in the source code and it gives back the list of all fresh register identifiers generated by the translation process |
---|
175 | of the statement in the source located in $l$. |
---|
176 | |
---|
177 | The above mentioned properties about the functions \verb=f_lbls= and \verb=f_regs=, together with some other |
---|
178 | ones, are expressed and formalized by the following propositional record. |
---|
179 | \begin{lstlisting} |
---|
180 | record b_graph_translate_props |
---|
181 | (src_g_pars, dst_g_pars : graph_params) |
---|
182 | (globals: list ident) |
---|
183 | (data : b_graph_translate_data src_g_pars dst_g_pars globals) |
---|
184 | (def_in : joint_closed_internal_function src_g_pars globals) |
---|
185 | (def_out : joint_closed_internal_function dst_g_pars globals) |
---|
186 | (f_lbls : label → list label) |
---|
187 | (f_regs : label → list register) : Prop ≝ |
---|
188 | { res_def_out_eq : |
---|
189 | joint_if_result … def_out = init_ret … data |
---|
190 | ; pars_def_out_eq : |
---|
191 | joint_if_params … def_out = init_params … data |
---|
192 | ; ss_def_out_eq : |
---|
193 | joint_if_stacksize … def_out = init_stack_size … data |
---|
194 | ; partition_lbls : partial_partition … f_lbls |
---|
195 | ; partition_regs : partial_partition … f_regs |
---|
196 | ; freshness_lbls : |
---|
197 | (∀l.All … |
---|
198 | (λlbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧ |
---|
199 | in_universe … lbl (joint_if_luniverse … def_out)) (f_lbls l)) |
---|
200 | ; freshness_regs : |
---|
201 | (∀l.All … |
---|
202 | (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧ |
---|
203 | in_universe … reg (joint_if_runiverse … def_out)) (f_regs l)) |
---|
204 | ; freshness_data_regs : |
---|
205 | All … (λreg.¬in_universe … reg (joint_if_runiverse … def_in) ∧ |
---|
206 | in_universe … reg (joint_if_runiverse … def_out)) |
---|
207 | (new_regs … data) |
---|
208 | ; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False |
---|
209 | ; multi_fetch_ok : |
---|
210 | ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → |
---|
211 | let lbls ≝ f_lbls l in let regs ≝ f_regs l in |
---|
212 | match s with |
---|
213 | [ sequential s' nxt ⇒ |
---|
214 | let block ≝ |
---|
215 | if not_emptyb … (added_prologue … data) ∧ |
---|
216 | eq_identifier … (joint_if_entry … def_in) l then |
---|
217 | bret … [ ] |
---|
218 | else |
---|
219 | f_step … data l s' in |
---|
220 | l -(block, l::lbls, regs)-> nxt in joint_if_code … def_out |
---|
221 | | final s' ⇒ |
---|
222 | l -(f_fin … data l s', l::lbls, regs)-> it in joint_if_code … def_out |
---|
223 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
224 | ] |
---|
225 | ; prologue_ok : |
---|
226 | if not_emptyb … (added_prologue … data) then |
---|
227 | ∃lbl.¬in_universe … lbl (joint_if_luniverse … def_in) ∧ |
---|
228 | joint_if_entry … def_out |
---|
229 | -( 〈 [ ],λ_.COST_LABEL … (get_first_costlabel … def_in), |
---|
230 | added_prologue … data 〉, |
---|
231 | f_lbls … lbl)-> joint_if_entry … def_in in joint_if_code … def_out |
---|
232 | else (joint_if_entry … def_out = joint_if_entry … def_in) |
---|
233 | }. |
---|
234 | \end{lstlisting} |
---|
235 | \autoref{tab:translate_props} summarizes the meaning of each field of the record. |
---|
236 | \begin{table} |
---|
237 | \centering |
---|
238 | \begin{tabular*}{\textwidth}{@{}p{.25\linewidth}@{}p{.75\linewidth}@{}} |
---|
239 | Field & Explanation \\[5pt] |
---|
240 | \hline |
---|
241 | \texttt{res\_def\_out\_eq}, \texttt{pars\_def\_out\_eq}, \texttt{ss\_def\_out\_eq}& |
---|
242 | The return value location, the formal parameters and the syntactic stack size are |
---|
243 | all as dictated by the corresponding \verb=b_graph_translate_data= fields.\\[5pt] |
---|
244 | \texttt{partition\_lbls}, \texttt{partition\_regs}& |
---|
245 | \verb=f_lbls= and \verb=f_regs= are partial partitions, i.e.\ all lists in their |
---|
246 | image are repetition-free and disjoint for different input values. \\[5pt] |
---|
247 | \texttt{freshness\_lbls}, \texttt{freshness\_regs}, \texttt{freshness\_data\_regs}& |
---|
248 | All lists of code-point identifiers and register generated at a source code-point, and the registers in |
---|
249 | \verb=new_regs= are fresh: |
---|
250 | they were not in the former source universe and they are in the new one.\\[5pt] |
---|
251 | & All identifiers of pseudo-register being element of the field \texttt{new\_regs} of the record of type \verb=b_graph_translate_data= provided in input are fresh. \\[5pt] |
---|
252 | \texttt{data\_regs\_disjoint} & All pseudo-register in \texttt{new\_regs} never appear in \verb=f_regs=. \\[5pt] |
---|
253 | \texttt{multi\_fetch\_ok} & Given a statement $I$ and a code-point identifier $l$ of the source internal function such that $I$ is located in $l$, if the translation process translate $I$ into a statement block $\langle I_1,\ldots ,I_n\rangle$ then |
---|
254 | $f\_lbls(l) = [l_1,\ldots,l_{n-1}]$ in the translated source code we have that $I_1$ is located in $l$ with $l1$ as syntactical |
---|
255 | successor, $I_2$ is located in $l_1$ with $l_2$ as syntactical successor, and so on with the last statement $I_n$ located in $l_{n-1}$ |
---|
256 | and it may have a syntactical successor depending whether $I$ is a step-statement or not: in the former case we have that the |
---|
257 | syntactical successor of $I_n$ is the syntactical successor of $I$, in the latter case, $I_n$ is a final statement.\\[5pt] |
---|
258 | \texttt{prologue\_ok} & If the field \texttt{added\_prologue} of the record of type \verb=b_graph_translate_data= provided in input is empty, then the code-point identifier of the first instruction of the translated function is the same of the one of the source internal function. Otherwise the two code points are different, with the first instruction of the translated function being a cost-emission statement followed by the instructions of \texttt{added\_prologue}; the last instruction of \texttt{added\_prologue} has an identifier $l$ as syntactical successor and $l$ is the same identifier as the one of the first instruction of the source internal function and in $l$ we fetch a \s{NOP} instruction. |
---|
259 | \end{tabular*} |
---|
260 | \caption{The explanation of the various fields of the \verb=b_graph_translate_props= record.} |
---|
261 | \label{tab:translate_props} |
---|
262 | \end{table} |
---|
263 | |
---|
264 | \subsection{A general correctness proof} |
---|
265 | In order to prove our general result, we need to define the usual semantic (data) relation among states of the source and target language and call relation between states. We remind that two states are in call relation whenever a call statement is fetched at state's current program counter. These two relations have to satisfy some condition, already explained at the beginning of this deliverable (see Section ??). In this section we will give some general conditions that these two relations have to satisfy in order to obtain the desired simulation result. We begin our analysis from the latter relation (the call one) and then we show how to relate it with a semantic relation satisfying some conditions that allow us to prove our general result. |
---|
266 | |
---|
267 | \subsubsection{A standard calling relation} |
---|
268 | Two states are in call relation whenever it is possible to fetch a call statement at the program counter given by the two states. We will exploit the properties of the translation explained in previous subsection in order to define a standard calling relation. We remind that the translation of a given statement $I$ is a block of statements $b= \langle I_1,\ldots I_n\rangle$ with $n \geq 1$. When $I$ is a call, then we will require that there is a unique $k \in [1,n]$ such $I_k$ has to be a call statement (we will see the formalization of this condition in the following subsection when we relate the calling relation with the semantic one). The idea of defining a standard calling relation is to compute the code-point identifier of this $I_k$, starting from the code-point identifier of the statement $I$ in the code of the source internal function. We will see how to use the information provided by the translation process (in particular the function \verb=f_lbls=) in order to obtain this result. We will see that, for technical reason, we will compute the code point of $I$ starting from the code point of $I_k$. |
---|
269 | |
---|
270 | In order to explain how this machinery work. we need to enter more in the detail of the translation process. Given a step-statement |
---|
271 | $I$, formally its translation is a triple $f\_step(s) = \langle pre,p,post \rangle$ such that $pre$ is a list of sequential |
---|
272 | statements called {\em preamble}, $p$ is a step-statement (we call it {\em pivot}) and $post$ is again a list of sequential statements |
---|
273 | called {\em postamble}. When $pre = [s_1,\ldots,s_n]$ and $post = [s_1',\ldots,s_m']$, the corresponding block being the translation |
---|
274 | of $I$ is $\langle s_1,\ldots,s_n,p,s_1',\ldots,s_m'\rangle$. In case $I$ is a final statement, than its translation does not have |
---|
275 | postamble, i.e.\ it is a pair $f\_fin(s) = \langle pre,p\rangle$ where the pivot $p$ is a final statement. |
---|
276 | |
---|
277 | Given a statement $I$ at a given code point $l$ in the source internal function and given the pivot statement $p$ of the translation |
---|
278 | of $I$ staying at code-point $l'$ in the translated internal function, there is an easy way to relate $l$ and $l'$. Notice that, |
---|
279 | in case the preamble is empty, for the property of the translation process we have then $l = l'$, while if the preamble is non-empty. |
---|
280 | then $l'$ is $n-1$-th element of $f\_lbls(l)$, where $n \geq 0$ is the length of the preamble. |
---|
281 | The \s{matita}'s definition computing the code points according to the above mentioned specification is the following one. |
---|
282 | \begin{lstlisting} |
---|
283 | definition sigma_label : ∀p_in,p_out : sem_graph_params. |
---|
284 | joint_program p_in → (ident → option ℕ) → |
---|
285 | (∀globals.joint_closed_internal_function p_in globals |
---|
286 | →bound_b_graph_translate_data p_in p_out globals) → |
---|
287 | (block → list register) → lbl_funct_type → regs_funct_type → |
---|
288 | block → label → option label ≝ |
---|
289 | λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. |
---|
290 | ! bl ← code_block_of_block bl ; |
---|
291 | ! <id,fn> ← res_to_opt … (fetch_internal_function … |
---|
292 | (joint_globalenv p_in prog stack_size) bl); |
---|
293 | ! <res,s> ← find ?? (joint_if_code ?? fn) |
---|
294 | (λlbl.λ_. |
---|
295 | match preamble_length … prog stack_size init init_regs f_regs bl lbl with |
---|
296 | [ None ⇒ false |
---|
297 | | Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with |
---|
298 | [ None ⇒ false |
---|
299 | | Some x ⇒ eq_identifier … searched x |
---|
300 | ] |
---|
301 | ]); |
---|
302 | return res. |
---|
303 | \end{lstlisting} |
---|
304 | This function takes in input all the information provided by the translation process (in particular the function $f\_lbls$), a |
---|
305 | function location and a code-point identifier $l$; it fetches the internal function of the source language in the corresponding location. |
---|
306 | Then it unfolds the code of the fetched function looking for a label $l'$ and a statement $I$ located in $l'$, such that, |
---|
307 | either $l = l'$ in case the preamble of the translation of $I$ is empty or $l'$ is the $n -1$-th where $n \geq 0$ is the length |
---|
308 | of the preamble of $I$. The function $find$ is the procedure realizing this search. If $preamble\_length$ is the function giving in |
---|
309 | output the length of the preamble and if $nth\_opt$ is the function giving the $n$-th element of a list, then this condition can |
---|
310 | be summarized as following: we are looking for a label $l'$ such that $l$ is the $n$-th element of the list $l :: f\_lbls (l)$, |
---|
311 | where $n$ is the length of the preamble. |
---|
312 | |
---|
313 | We can prove that, starting from a code point identifier of the translated internal function, |
---|
314 | whenever there exists a code-point identifier in the source internal function satisfying the above condition, then it is always unique. |
---|
315 | The properties \verb=partition_lbls= and \verb=freshness_lbls= provided by the translation process are crucial in the proof |
---|
316 | of this statement. |
---|
317 | We can wrap this function inside the definition of the desired relation between program counter states in the following way |
---|
318 | The conditional at the beginning is put to deal with the pre-main case, which is translated without following the standard |
---|
319 | translation process we explained in previous section. |
---|
320 | \begin{lstlisting} |
---|
321 | definition sigma_pc_opt : |
---|
322 | ∀p_in,p_out : sem_graph_params. |
---|
323 | joint_program p_in → (ident → option ℕ) → |
---|
324 | (∀globals.joint_closed_internal_function p_in globals |
---|
325 | →bound_b_graph_translate_data p_in p_out globals) → |
---|
326 | (block → list register) → lbl_funct_type → regs_funct_type → |
---|
327 | program_counter → option program_counter ≝ |
---|
328 | λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. |
---|
329 | let target_point ≝ point_of_pc p_out pc in |
---|
330 | if eqZb (block_id (pc_block pc)) (-1) then |
---|
331 | return pc |
---|
332 | else |
---|
333 | ! source_point ← sigma_label p_in p_out prog stack_size init init_regs |
---|
334 | f_lbls f_regs (pc_block pc) target_point; |
---|
335 | return pc_of_point p_in (pc_block pc) source_point. |
---|
336 | |
---|
337 | definition sigma_stored_pc ≝ |
---|
338 | λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. |
---|
339 | match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with |
---|
340 | [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x]. |
---|
341 | \end{lstlisting} |
---|
342 | |
---|
343 | The main result about the program counter relation we have defined is the following. If we fetch a statement $I$ in |
---|
344 | at a given program counter $pc$ in the source program, then there is a program counter $pc'$ in the target program |
---|
345 | which is in relation with $pc$ (i.e.\ $sigma\_stored\_pc pc' = pc$) and the fetched statement at $pc'$ is the pivot |
---|
346 | statement of the translation. The formalization of this statement in \s{matita} is given in the following. |
---|
347 | |
---|
348 | \begin{lstlisting} |
---|
349 | lemma fetch_statement_sigma_stored_pc : |
---|
350 | ∀p_in,p_out,prog,stack_sizes, |
---|
351 | init,init_regs,f_lbls,f_regs,pc,f,fn,stmt. |
---|
352 | b_graph_transform_program_props p_in p_out stack_sizes |
---|
353 | init prog init_regs f_lbls f_regs → |
---|
354 | block_id … (pc_block pc) ≠ -1 → |
---|
355 | let trans_prog ≝ b_graph_transform_program p_in p_out init prog in |
---|
356 | fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc = |
---|
357 | return 〈 f,fn,stmt 〉 → |
---|
358 | ∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧ |
---|
359 | match stmt with |
---|
360 | [ sequential step nxt ⇒ |
---|
361 | ∃step_block : step_block p_out (prog_names … trans_prog). |
---|
362 | bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) |
---|
363 | (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧ |
---|
364 | ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init |
---|
365 | init_regs f_lbls f_regs pc' = pc ∧ |
---|
366 | ∃fn',nxt'. |
---|
367 | fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' = |
---|
368 | if not_emptyb … (added_prologue … data) ∧ |
---|
369 | eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn) |
---|
370 | then OK ? <f,fn',sequential ?? (NOOP …) nxt'> |
---|
371 | else OK ? <f,fn', |
---|
372 | sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'> |
---|
373 | | final fin ⇒ |
---|
374 | ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin) |
---|
375 | (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧ |
---|
376 | ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init |
---|
377 | init_regs f_lbls f_regs pc' = pc ∧ |
---|
378 | ∃fn'.fetch_statement p_out … |
---|
379 | (joint_globalenv p_out trans_prog stack_sizes) pc' |
---|
380 | = return 〈 f,fn',final ?? (\snd fin_block) 〉 |
---|
381 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
382 | ]. |
---|
383 | \end{lstlisting} |
---|
384 | |
---|
385 | If we combine the statement above with the fact that the pivot statement of the translation |
---|
386 | of a call statement is always a call statement (which we will formalize better in the |
---|
387 | following section), then we can define our standard calling relation in the following way. |
---|
388 | |
---|
389 | \begin{lstlisting} |
---|
390 | (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call. |
---|
391 | λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call. |
---|
392 | pc ? s1 = sigma_stored_pc |
---|
393 | p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)). |
---|
394 | \end{lstlisting} |
---|
395 | |
---|
396 | We stress the fact that such a call relation will be always defined in this way for all joint-languages, |
---|
397 | in an independent way from the specific pass. The only condition we will ask is that the pass should |
---|
398 | use the translation process we explain in the previous section. |
---|
399 | |
---|
400 | \subsubsection{The semantic relation} |
---|
401 | The semantic relation between states is the classical relation used in forward simulation proofs. |
---|
402 | It correlates the data of the status (e.g. register, memory, \emph{etc}). We remind that the notion of state |
---|
403 | in joint language is summarized in the following record. |
---|
404 | \begin{lstlisting} |
---|
405 | record state_pc (semp : sem_state_params) : Type[0] ≝ |
---|
406 | { st_no_pc :> state semp |
---|
407 | ; pc : program_counter |
---|
408 | ; last_pop : program_counter |
---|
409 | }. |
---|
410 | \end{lstlisting} |
---|
411 | It consists of three fields: the field \verb=st_no_pc= contains all data information of the state |
---|
412 | (the content of the registers, of the memory and so on), the field \verb=pc= contains the current |
---|
413 | program counter, while the field \verb=last_pop= is the address of the last popped calling address |
---|
414 | when executing a return instruction. |
---|
415 | |
---|
416 | The type of the semantic relation between state is the following. |
---|
417 | |
---|
418 | \begin{lstlisting} |
---|
419 | definition joint_state_pc_relation ≝ |
---|
420 | λP_in,P_out : sem_graph_params.state_pc P_in → state_pc P_out → Prop. |
---|
421 | \end{lstlisting} |
---|
422 | |
---|
423 | We would like to state some conditions the semantic relation between states have to satisfy in order |
---|
424 | to get our simulation result. We would like that this relation have some flavour of compositionality. |
---|
425 | In particular we would like that it depends strictly on the contents of the field \verb=st_no_pc=, i.e. |
---|
426 | the field that really contains data information of the state. So we need also a data relation, i.e.\ |
---|
427 | a relation of this type. |
---|
428 | |
---|
429 | \begin{lstlisting} |
---|
430 | definition joint_state_relation ≝ |
---|
431 | λP_in,P_out.program_counter → state P_in → state P_out → Prop. |
---|
432 | \end{lstlisting} |
---|
433 | |
---|
434 | Notice that the data relation cab depend on a specific program counter of the source. This is done |
---|
435 | to capture complex data relations like the ones in the \s{ERTL} to \s{LTL} pass, in which you need to know |
---|
436 | where data in pseudo-registers of \s{ERTL} are stored by the translation (either in hardware register or |
---|
437 | in memory) and this information depends on the code point on the statement being translated. |
---|
438 | |
---|
439 | The compositionality requirement is expressed by several conditions (which are part of a bigger |
---|
440 | record). |
---|
441 | % |
---|
442 | % \begin{lstlisting} |
---|
443 | % ; fetch_ok_sigma_state_ok : |
---|
444 | % ∀st1,st2,f,fn. st_rel st1 st2 → |
---|
445 | % fetch_internal_function … |
---|
446 | % (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) |
---|
447 | % = return <f,fn> → |
---|
448 | % st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2) |
---|
449 | % ; fetch_ok_pc_ok : |
---|
450 | % ∀st1,st2,f,fn.st_rel st1 st2 → |
---|
451 | % fetch_internal_function … |
---|
452 | % (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) |
---|
453 | % = return <f,fn> → |
---|
454 | % pc … st1 = pc … st2 |
---|
455 | % ; fetch_ok_sigma_last_pop_ok : |
---|
456 | % ∀st1,st2,f,fn.st_rel st1 st2 → |
---|
457 | % fetch_internal_function … |
---|
458 | % (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) |
---|
459 | % = return <f,fn> → |
---|
460 | % (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs |
---|
461 | % f_lbls f_regs (last_pop … st2) |
---|
462 | % ; st_rel_def : |
---|
463 | % ∀st1,st2,pc,lp1,lp2,f,fn. |
---|
464 | % fetch_internal_function … |
---|
465 | % (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return <f,fn> → |
---|
466 | % st_no_pc_rel pc st1 st2 → |
---|
467 | % lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs |
---|
468 | % f_lbls f_regs lp2 → |
---|
469 | % st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2) |
---|
470 | % \end{lstlisting} |
---|
471 | % |
---|
472 | Condition \texttt{fetch\_ok\_sigma\_state\_ok} postulates that two state that are in semantic |
---|
473 | relation should have their data field also in relation. Condition \texttt{fetch\_ok\_pc\_ok} postulates |
---|
474 | that two states that are in semantic relation should have the same program counter. This is due |
---|
475 | to the way the translation is performed. In fact a statement $I$ at a code point $l$ in the source |
---|
476 | internal function is translated with a block of instructions in the translated internal function |
---|
477 | whose initial statement is at the same code point $l$. The condition \texttt{fetch\_ok\_sigma\_last\_pop\_ok} |
---|
478 | postulates that two states that are in semantic relation have the last popped calling address |
---|
479 | in call relation. Finally \texttt{st\_rel\_def} postulates that given two states having the same |
---|
480 | program counter, the last pop fields in call relation and the data fields also in data relation, then |
---|
481 | they are in semantic relation. |
---|
482 | |
---|
483 | Another important condition is that the pivot statement of the translation of a call statement is |
---|
484 | always a call statement. This is important in order to obtain the correctness of the call relation |
---|
485 | and return relation between state. % This condition is formalized by the following Matita's code, and |
---|
486 | We call this condition \texttt{call\_is\_call}. |
---|
487 | |
---|
488 | % \begin{lstlisting} |
---|
489 | % ; call_is_call :∀f,fn,bl. |
---|
490 | % fetch_internal_function … |
---|
491 | % (joint_globalenv P_in prog stack_sizes) bl = return <f,fn> → |
---|
492 | % ∀id,args,dest,lbl. |
---|
493 | % bind_new_P' ?? |
---|
494 | % (λregs1.λdata.bind_new_P' ?? |
---|
495 | % (λregs2.λblp. |
---|
496 | % ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') |
---|
497 | % (f_step … data lbl (CALL P_in ? id args dest))) |
---|
498 | % (init ? fn) |
---|
499 | % \end{lstlisting} |
---|
500 | |
---|
501 | The conditions we are going to present now are standard semantic commutation lemmas that are commonly |
---|
502 | used when proving the correctness of the operational semantics of many imperative languages. We introduce some notation. |
---|
503 | We will use $I,J\ldots$ to range over by statements. We will use $l_1,\ldots,l_n$ to range over by code point identifiers. |
---|
504 | We will use $r_1,\ldots,r_n$ to range over by register identifiers. We will use $s_1,s_1',s_1'',\ldots$ to range |
---|
505 | over by states of programs of the source language. We will use $s_2,s_2',s_2'',\ldots$ to range over by |
---|
506 | states of programs of the target language. We denote respectively with $\simeq_{S}$, $\simeq_C$ and $\simeq_L$ |
---|
507 | the semantic relation, the call relation and the cost-label relation between states. These relations have |
---|
508 | been introduced at the beginning of this Deliverable (see Section ??). If $instr = [I_1,\ldots,I_n]$ is a list |
---|
509 | of instructions, then we write $s_i \stackrel{instr}{\longrightarrow} s_i'$ ($i \in [1,2]$) when $s_i'$ is |
---|
510 | the state being the result of the evaluation of the sequence of instructions $instr$ (performed in the order |
---|
511 | they appear in the list) starting from the initial state $s_i$. When $instr = [I]$ is a singleton, we use |
---|
512 | to omit square brackets and we write $s_i \stackrel{I}{\longrightarrow} s_i'$. |
---|
513 | We will denote with $\pi_i$ ($i \in [1,t]$) the projecting functions of $t$-uples. We will denote with $f\_step$ and $f\_fin$ |
---|
514 | the translating functions of respectively step-statements and final statements. We remind that $f\_step$ gives |
---|
515 | a triple as output (a list of instruction called preamble,an instruction called pivot and a list of instructions |
---|
516 | called postamble) while $f\_fin$ gives a pair as output (a list of instruction called preamble and an instruction |
---|
517 | called pivot). Furthermore, we denote with $prologue$ the content of the field \texttt{added\_prologue} of the record |
---|
518 | provided in input to the translation process. |
---|
519 | |
---|
520 | Many commutation conditions can be depicted using diagrams. We will use them to give a pictorial flavour of the conditions |
---|
521 | we will ask in order to obtain the final correctness statement. Given the states $s_1,s_1',s_2,s_2'$ and the instructions |
---|
522 | $I,J_1,\ldots,J_k$, the following diagram |
---|
523 | $$ |
---|
524 | \xymatrix{ |
---|
525 | s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S} && s_1' \ar@{-}[d]^{\simeq_S}\\ |
---|
526 | s_2 \ar[rr]^{[J_1,\ldots,J_k]} && s_2' |
---|
527 | } |
---|
528 | $$ |
---|
529 | depicts a situation in which the state $s_1 \stackrel{I}{\longrightarrow} s_1'$, $s_2 \stackrel{I}{\longrightarrow} s_2'$, |
---|
530 | $s_1 \simeq_S s_2$ and $s_1' \simeq_S s_2'$. |
---|
531 | |
---|
532 | \paragraph{Commutation of pre-main instructions (\verb=pre_main_ok=).} |
---|
533 | In order to get the commutation of pre-main instructions (states whose function location of program counter is -1), we have |
---|
534 | to prove the following condition: for all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$, |
---|
535 | then there exists an $s_2'$ such that $s_2 \stackrel{J}{\longrightarrow} s_2'$ and $s_1 \simeq_S s_2'$ i.e.\ such that the following |
---|
536 | diagram commutes. |
---|
537 | $$ |
---|
538 | \xymatrix{ |
---|
539 | s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S} && s_1' \ar@{-}[d]^{\simeq_S}\\ |
---|
540 | s_2 \ar[rr]^{J} && s_2' |
---|
541 | } |
---|
542 | $$ |
---|
543 | % The formalization of this statement in Matita is the following one. |
---|
544 | % \begin{lstlisting} |
---|
545 | % ; pre_main_ok : |
---|
546 | % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
547 | % ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . |
---|
548 | % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). |
---|
549 | % block_id … (pc_block (pc … st1)) = -1 → |
---|
550 | % st_rel st1 st2 → |
---|
551 | % as_label (joint_status P_in prog stack_sizes) st1 = |
---|
552 | % as_label (joint_status P_out trans_prog stack_sizes) st2 ∧ |
---|
553 | % joint_classify … (mk_prog_params P_in prog stack_sizes) st1 = |
---|
554 | % joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧ |
---|
555 | % (eval_state P_in … (joint_globalenv P_in prog stack_sizes) |
---|
556 | % st1 = return st1' → |
---|
557 | % ∃st2'. st_rel st1' st2' ∧ |
---|
558 | % eval_state P_out … |
---|
559 | % (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2') |
---|
560 | % \end{lstlisting} |
---|
561 | |
---|
562 | \paragraph{Commutation of conditional jump (\verb=cond_commutation=).} |
---|
563 | For all $s_1,s_1'$ and $s_2$ such that $s_1 \stackrel{COND \ r \ l}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$ then |
---|
564 | \begin{itemize} |
---|
565 | \item there are $s_2^{fin}$ and $s_2'$ such that $s_2 \stackrel{\pi_1(f\_step(COND \ r \ l))}{\longrightarrow} s_2^{fin}$, |
---|
566 | $s_2^{fin} \stackrel{\pi_2(f\_step(COND \ r \ l))} s_2'$ and $s_1' \simeq_S s_2'$, i.e.\ the following diagram commutes |
---|
567 | $$ |
---|
568 | \xymatrix{ |
---|
569 | s_1 \ar@{->}[rrrrrr]^{COND \ l \ r} \ar@{-}[d]^{\simeq_S} &&&&&& s_1' \ar@{-}[d]^{\simeq_S}\\ |
---|
570 | s_2 \ar[rrr]^{\pi_1(f\_step(COND \ r \ l))} &&& s_2^{fin} \ar[rrr]^{\pi_2(f\_step(COND \ r \ l))} &&& s_2' |
---|
571 | } |
---|
572 | $$ |
---|
573 | \item $\pi_3(f\_step(COND \ r \ l))$ is empty, while $\pi_2(f\_step(COND \ r \ l)) = COND \ r' \ l'$ is a conditional jump |
---|
574 | such that $l = l'$. |
---|
575 | \end{itemize} |
---|
576 | % This condition is formalized in Matita in the following way. |
---|
577 | % \begin{lstlisting} |
---|
578 | % ; cond_commutation : |
---|
579 | % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
580 | % ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . |
---|
581 | % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). |
---|
582 | % ∀f,fn,a,ltrue,lfalse,bv,b. |
---|
583 | % block_id … (pc_block (pc … st1)) ≠ -1 → |
---|
584 | % let cond ≝ (COND P_in ? a ltrue) in |
---|
585 | % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = |
---|
586 | % return <f, fn, sequential … cond lfalse> → |
---|
587 | % acca_retrieve … P_in (st_no_pc … st1) a = return bv → |
---|
588 | % bool_of_beval … bv = return b → |
---|
589 | % st_rel st1 st2 → |
---|
590 | % ∀t_fn. |
---|
591 | % fetch_internal_function … |
---|
592 | % (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = |
---|
593 | % return 〈 f,t_fn 〉 → |
---|
594 | % bind_new_P' ?? |
---|
595 | % (λregs1.λdata.bind_new_P' ?? |
---|
596 | % (λregs2.λblp.(\snd blp) = [ ] ∧ |
---|
597 | % ∀mid. |
---|
598 | % stmt_at P_out … (joint_if_code ?? t_fn) mid |
---|
599 | % = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ |
---|
600 | % ∃st2_pre_mid_no_pc. |
---|
601 | % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f |
---|
602 | % (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) |
---|
603 | % = return st2_pre_mid_no_pc ∧ |
---|
604 | % let new_pc ≝ if b then |
---|
605 | % (pc_of_point P_in (pc_block (pc … st1)) ltrue) |
---|
606 | % else |
---|
607 | % (pc_of_point P_in (pc_block (pc … st1)) lfalse) in |
---|
608 | % st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧ |
---|
609 | % ∃a'. ((\snd (\fst blp)) mid) = COND P_out ? a' ltrue ∧ |
---|
610 | % ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧ |
---|
611 | % bool_of_beval … bv' = return b |
---|
612 | % ) (f_step … data (point_of_pc P_in (pc … st1)) cond) |
---|
613 | % ) (init ? fn) |
---|
614 | % \end{lstlisting} |
---|
615 | |
---|
616 | \paragraph{Commutation of sequential statements (\verb=seq_commutation=).} |
---|
617 | In case of a sequential statement $I$, its translation $f\_step(I) = \langle pre , J , post \rangle$ is coerced |
---|
618 | into a list of sequential statements $pre$ \verb=@= $[J]$ \verb=@= $post$. Then we can state the condition in the |
---|
619 | following way. For all $s_1,s_1',s_2$ such that $s_1 \stackrel{I}{\longrightarrow} s_1'$ and $s_1 \simeq_S s_2$ then |
---|
620 | there is $s_2'$ such that $s_2 \stackrel{f\_step(I)}{\longrightarrow} s_s'$ and $s_1' \simeq_S s_2'$, i.e.\ such that |
---|
621 | the following diagram commutes. |
---|
622 | $$ |
---|
623 | \xymatrix{ |
---|
624 | s_1 \ar@{->}[rr]^{I} \ar@{-}[d]^{\simeq_S} && s_1' \ar@{-}[d]^{\simeq_S}\\ |
---|
625 | s_2 \ar[rr]^{f\_step(I)} && s_2' |
---|
626 | } |
---|
627 | $$ |
---|
628 | % The formalization in Matita of the above statement is as follows. |
---|
629 | % \begin{lstlisting} |
---|
630 | % ; seq_commutation : |
---|
631 | % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
632 | % ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . |
---|
633 | % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). |
---|
634 | % ∀f,fn,stmt,nxt. |
---|
635 | % block_id … (pc_block (pc … st1)) ≠ -1 → |
---|
636 | % let seq ≝ (step_seq P_in ? stmt) in |
---|
637 | % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = |
---|
638 | % return <f, fn, sequential … seq nxt> → |
---|
639 | % eval_state P_in … (joint_globalenv P_in prog stack_sizes) |
---|
640 | % st1 = return st1' → |
---|
641 | % st_rel st1 st2 → |
---|
642 | % ∀t_fn. |
---|
643 | % fetch_internal_function … |
---|
644 | % (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = |
---|
645 | % return <f,t_fn> → |
---|
646 | % bind_new_P' ?? |
---|
647 | % (λregs1.λdata.bind_new_P' ?? |
---|
648 | % (λregs2.λblp. |
---|
649 | % ∃l : list (joint_seq P_out |
---|
650 | % (globals ? (mk_prog_params P_out trans_prog stack_sizes))). |
---|
651 | % blp = (ensure_step_block ?? l) ∧ |
---|
652 | % ∃st2_fin_no_pc. |
---|
653 | % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f |
---|
654 | % l (st_no_pc … st2)= return st2_fin_no_pc ∧ |
---|
655 | % st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc |
---|
656 | % ) (f_step … data (point_of_pc P_in (pc … st1)) seq) |
---|
657 | % ) (init ? fn) |
---|
658 | % \end{lstlisting} |
---|
659 | |
---|
660 | \paragraph{Commutation of call statement (\verb=call_commutation=).} |
---|
661 | For all $s_1,s_1',s_2$ such that we have $s_1 \stackrel{CALL \ id \ arg \ dst}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$ and |
---|
662 | the statement fetched in the target function at the program counter in call relation |
---|
663 | with the program counter of $s_1$ is $\pi_2(f\_step(CALL \ id \ arg \ dst)) = CALL \ id' \ arg' \ dst'$ |
---|
664 | for some $id',ags',dst'$, then there are $s_2^{pre},s_2^{after},s_2'$ such that |
---|
665 | \begin{itemize} |
---|
666 | \item $s_2 \stackrel{\pi_1(f\_step(CALL \ id \ arg \ dst))}{\longrightarrow} s_2^{pre}$, |
---|
667 | \item $s_2^{pre} \stackrel{CALL \ id' \arg' \ dst'}{\longrightarrow} s_2^{after}$, |
---|
668 | \item $s_2^{after} \stackrel{prologue}{\longrightarrow} s_2'$, |
---|
669 | \item $s_1' \simeq_L s_2^{after}$ and $s_1' \simeq_S s_2'$. |
---|
670 | \end{itemize} |
---|
671 | The situation is depicted by the following diagram. |
---|
672 | $$ |
---|
673 | \xymatrix{ |
---|
674 | s_1 \ar@{-}[d]^{\simeq_S} \ar@{-}[d]^{\simeq_S} \ar[rrrrrrrrrr]^{CALL \ id \ arg \ dst} &&&&&&&&&& s_1' \ar@{-}[d]^{\simeq_S} \\ |
---|
675 | s_2 \ar[rrrr]^{\pi_1(f\_step(CALL \ id \ arg \ dst))} &&&& s_2^{pre} \ar[rrr]^{CALL \ id' \ arg' \ dst'} &&& s_2^{after} \ar[rrr]^{prologue} &&& s_2' |
---|
676 | } |
---|
677 | $$ |
---|
678 | % The statement is formalized in Matita in the following way. |
---|
679 | % \begin{lstlisting} |
---|
680 | % ; call_commutation : |
---|
681 | % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
682 | % ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . |
---|
683 | % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). |
---|
684 | % ∀f,fn,id,arg,dest,nxt. |
---|
685 | % block_id … (pc_block (pc … st1)) ≠ -1 → |
---|
686 | % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = |
---|
687 | % return 〈 f, fn, sequential P_in ? (CALL P_in ? id arg dest) nxt 〉 → |
---|
688 | % ∀bl. |
---|
689 | % block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1) |
---|
690 | % = return bl → |
---|
691 | % ∀f1,fn1. |
---|
692 | % fetch_internal_function … |
---|
693 | % (joint_globalenv P_in prog stack_sizes) bl = return 〈 f1,fn1 〉 → |
---|
694 | % ∀st1_pre. |
---|
695 | % save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre → |
---|
696 | % ∀n.stack_sizes f1 = return n → |
---|
697 | % ∀st1'. |
---|
698 | % setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' → |
---|
699 | % st_rel st1 st2 → |
---|
700 | % ∀t_fn1. |
---|
701 | % fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl = |
---|
702 | % return 〈 f1,t_fn1 〉 → |
---|
703 | % bind_new_P' ?? |
---|
704 | % (λregs1.λdata. |
---|
705 | % bind_new_P' ?? |
---|
706 | % (λregs2.λblp. |
---|
707 | % ∀pc',t_fn,id',arg',dest',nxt1. |
---|
708 | % sigma_stored_pc P_in P_out prog stack_sizes init init_regs |
---|
709 | % f_lbls f_regs pc' = (pc … st1) → |
---|
710 | % fetch_statement P_out … (joint_globalenv P_out trans_prog stack_sizes) pc' |
---|
711 | % = return 〈 f,t_fn, |
---|
712 | % sequential P_out ? ((\snd (\fst blp)) (point_of_pc P_out pc')) nxt1 〉→ |
---|
713 | % ((\snd (\fst blp)) (point_of_pc P_out pc')) = (CALL P_out ? id' arg' dest') → |
---|
714 | % ∃st2_pre_call. |
---|
715 | % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f |
---|
716 | % (map_eval ?? (\fst (\fst blp)) (point_of_pc P_out pc')) (st_no_pc ? st2) = return st2_pre_call ∧ |
---|
717 | % block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id' |
---|
718 | % st2_pre_call = return bl ∧ |
---|
719 | % ∃st2_pre. |
---|
720 | % save_frame … P_out (kind_of_call P_out id') dest' |
---|
721 | % (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧ |
---|
722 | % ∃st2_after_call. |
---|
723 | % setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre |
---|
724 | % = return st2_after_call ∧ |
---|
725 | % bind_new_P' ?? |
---|
726 | % (λregs11.λdata1. |
---|
727 | % ∃st2'. |
---|
728 | % repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 |
---|
729 | % (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) = |
---|
730 | % return st2' ∧ |
---|
731 | % st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1)) |
---|
732 | % (increment_stack_usage P_in n st1') st2' |
---|
733 | % ) (init ? fn1) |
---|
734 | % ) |
---|
735 | % (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest)) |
---|
736 | % ) (init ? fn) |
---|
737 | % \end{lstlisting} |
---|
738 | \paragraph{Commutation of return statement (\verb=return_commutation=).} |
---|
739 | For all $s_1,s_1',s_2$ such that $s_1 \stackrel{RETURN}{\longrightarrow} s_1'$, $s_1 \simeq_S s_2$, if $CALL \ id \ arg \ dst$ |
---|
740 | is the call statement that caused the function call ened by the current return (i.e.\ it is the statement whose code point identifier |
---|
741 | is the syntactical predecessor of the program counter of $s_1'$), then $\pi_2(f\_fin(RETURN)) = RETURN$, there are |
---|
742 | $s_2^{pre},s_2^{after},s_2'$ such that $s_2 \stackrel{\pi_1(f\_fin(RETURN))}{\longrightarrow} s_2^{pre}$, |
---|
743 | $s_2^{pre} \stackrel{RETURN}{\longrightarrow} s_2^{after}$, |
---|
744 | $s_2^{after} \stackrel{\pi_3(f\_step(CALL \ id \ arg \ dst))}{\longrightarrow} s_2'$ and $s_1' \simeq_S s_2'$. The following diagram |
---|
745 | depicts the above described requested situation. |
---|
746 | $$ |
---|
747 | \xymatrix{ |
---|
748 | s_1 \ar@{-}[d]^{\simeq_S} \ar@{-}[d]^{\simeq_S} \ar[rrrrrrrrrrr]^{RETURN} &&&&&&&&&&& s_1' \ar@{-}[d]^{\simeq_S} \\\ |
---|
749 | s_2 \ar[rrrr]^{\pi_1(f\_fin(RETURN))} &&&& s_2^{pre} \ar[rrr]^{RETURN} &&& s_2^{after} \ar[rrrr]^{\pi_3(f\_step(CALL \ id \ arg \ dst))} &&&& s_2' |
---|
750 | } |
---|
751 | $$ |
---|
752 | % The statement is formalized in Matita in the following way. |
---|
753 | % \begin{lstlisting} |
---|
754 | % ; return_commutation : |
---|
755 | % let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
756 | % ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . |
---|
757 | % ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). |
---|
758 | % ∀f,fn. |
---|
759 | % block_id … (pc_block (pc … st1)) ≠ -1 → |
---|
760 | % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = |
---|
761 | % return 〈 f, fn, final P_in ? (RETURN …) 〉 → |
---|
762 | % ∀n. stack_sizes f = return n → |
---|
763 | % let curr_ret ≝ joint_if_result … fn in |
---|
764 | % ∀st_pop,pc_pop. |
---|
765 | % pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret |
---|
766 | % (st_no_pc … st1) = return 〈 st_pop,pc_pop 〉 → |
---|
767 | % ∀nxt.∀f1,fn1,id,args,dest. |
---|
768 | % fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop = |
---|
769 | % return 〈 f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt 〉 → |
---|
770 | % st_rel st1 st2 → |
---|
771 | % ∀t_fn. |
---|
772 | % fetch_internal_function … |
---|
773 | % (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = |
---|
774 | % return 〈 f,t_fn 〉 → |
---|
775 | % bind_new_P' ?? |
---|
776 | % (λregs1.λdata. |
---|
777 | % bind_new_P' ?? |
---|
778 | % (λregs2.λblp. |
---|
779 | % \snd blp = (RETURN …) ∧ |
---|
780 | % ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f |
---|
781 | % (\fst blp) (st_no_pc … st2)= return st_fin ∧ |
---|
782 | % ∃t_st_pop,t_pc_pop. |
---|
783 | % pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f |
---|
784 | % (joint_if_result … t_fn) st_fin = return 〈 t_st_pop,t_pc_pop 〉 ∧ |
---|
785 | % sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs |
---|
786 | % t_pc_pop = pc_pop ∧ |
---|
787 | % if eqZb (block_id (pc_block pc_pop)) (-1) then |
---|
788 | % st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) |
---|
789 | % (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*) |
---|
790 | % else |
---|
791 | % bind_new_P' ?? |
---|
792 | % (λregs4.λdata1. |
---|
793 | % bind_new_P' ?? |
---|
794 | % (λregs3.λblp1. |
---|
795 | % ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 |
---|
796 | % (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧ |
---|
797 | % st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) |
---|
798 | % (decrement_stack_usage ? n st_pop) st2' |
---|
799 | % ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest)) |
---|
800 | % ) (init ? fn1) |
---|
801 | % ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …)) |
---|
802 | % ) (init ? fn) |
---|
803 | % \end{lstlisting} |
---|
804 | |
---|
805 | \subsubsection{Conclusion} |
---|
806 | After having provided a semantic relation among states that satisfies some conditions that correspond to |
---|
807 | commutation lemmas that are commonly proved in a forward simulation proof, it is possible to prove the |
---|
808 | general theorem. All these condition are summarized in a propositional record called \verb=good_state_relation=. |
---|
809 | The statement we are able to prove have the following shape. |
---|
810 | \begin{lstlisting} |
---|
811 | theorem joint_correctness : ∀p_in,p_out : sem_graph_params. |
---|
812 | ∀prog : joint_program p_in.∀stack_size : ident → option ℕ. |
---|
813 | ∀init : (∀globals.joint_closed_internal_function p_in globals → |
---|
814 | bound_b_graph_translate_data p_in p_out globals). |
---|
815 | ∀init_regs : block → list register.∀f_lbls : lbl_funct_type. |
---|
816 | ∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out. |
---|
817 | ∀st_rel : joint_state_pc_relation p_in p_out. |
---|
818 | good_state_relation p_in p_out prog stack_size init init_regs |
---|
819 | f_lbls f_regs st_no_pc_rel st_rel → |
---|
820 | let trans_prog ≝ b_graph_transform_program … init prog in |
---|
821 | ∀init_in. |
---|
822 | make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → |
---|
823 | ∃init_out. |
---|
824 | make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧ |
---|
825 | ∃[1] R. |
---|
826 | status_simulation_with_init |
---|
827 | (joint_abstract_status (mk_prog_params p_in prog stack_size)) |
---|
828 | (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)) |
---|
829 | R init_in init_out. |
---|
830 | \end{lstlisting} |
---|
831 | The module formalizing the formal machinery we described in this document consists of about 3000 lines of |
---|
832 | \s{matita} code. We stress the fact that this machinery proves general properties that do not depend on the |
---|
833 | specific back-end graph compiler pass. |
---|