# Changeset 2622 for Papers

Ignore:
Timestamp:
Feb 6, 2013, 6:11:49 PM (6 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2616 \usepackage{bcprules} \usepackage{verbatim} \usepackage{alltt} % NB: might be worth removing this if changing class in favour of \texttt{f(g(x));}. We need to inject an emission statement/instrumentation instruction just after the execution of \texttt{g}. The only way to do that is to rewrite the code as \texttt{y = g(x); emit L$_1$; f(y);} for some fresh is to rewrite the code as \texttt{y = g(x); emit L; f(y);} for some fresh variable \texttt{y}. It is pretty clear how in certain situations the obtained code would be more obfuscated and then more difficult to manually reason on. For the previous reasons, in this paper and in the CerCo project we adopt a different approach. We do not inject any more emission statement after every different approach. We do not inject emission statements after every function call. However, we want to propagate a strong additional invariant in the forward simulation proof. The invariant is the propagation of the structure In the original labelling approach of~\cite{easylabelling}, the second property was granted statically (syntactically) as a property of the generated code. In our revised approach, instead, we will grant the property dinamically: it will be possible to generate code that does not respect it, as soon as all execution traces do respect it. For instance, dead code will no longer was granted syntactically as a property of the generated code. In our revised approach, instead, we will impose the property on the runs: it will be possible to generate code that does not respect the syntactic property, as soon as all possible runs respect it. For instance, dead code will no longer be required to have all basic blocks correctly labelled. The switch is suggested from the fact that the first of the two properties --- that related to function calls/returns --- can only be defined as a dinamic property, i.e. as a property of execution traces, not of the static code. The switch is function calls/returns --- can only be defined as property of runs, not of the static code. The switch is beneficial to the proof because the original proof was made of two parts: the forward simulation proof and the proof that the static property was granted. In order to capture the structure semantics so that it is preserved by a forward simulation argument, we need to make the structure observable in the semantics. This is the topic of the next Section. in the semantics. This is the topic of the next section. \section{Structured traces} We present here a new definition of semantics where the structure of execution, as defined in the previous Section, is now observable. The idea is to replace as defined in the previous section, is now observable. The idea is to replace the stream of observables with a structured data type that makes explicit function call and returns and that grants some additional invariants by we abstract the type of structure traces over an abstract data type of abstract statuses: \begin{verbatim} record abstract_status := { S: Type[0] ;  as_execute: S -> S -> Prop ;  as_classify: S -> classification ;  as_costed: S -> Prop ;  as_label: \forall s. as_costed S s -> label ;  as_call_ident: \forall s. as_classify S s = cl_call -> label ;  as_after_return: (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop } \end{verbatim} \begin{alltt} record abstract_status := \{ S: Type[0]; as_execute: S $$\to$$ S $$\to$$ Prop;     as_classify: S $$\to$$ classification; as_costed: S $$\to$$ Prop;      as_label: $$\forall$$ s. as_costed S s $$\to$$ label; as_call_ident: $$\forall$$ s. as_classify S s = cl_call $$\to$$ label; as_after_return: ($$\Sigma$$s:as_status. as_classify s = Some ? cl_call) $$\to$$ as_status $$\to$$ Prop \} \end{alltt} The predicate $\texttt{as\_execute}~s_1~s_2$ holds if $s_1$ evolves into $s_2$ in one step; $\texttt{as\_classify}~s~c$ holds if the next instruction $s_2$ in one step;\\ $\texttt{as\_classify}~s~c$ holds if the next instruction to be executed in $s$ is classified according to $c \in \{\texttt{return,jump,call,other}\}$ (we omit tailcalls for simplicity); \{\texttt{cl\_return,cl\_jump,cl\_call,cl\_other}\}$(we omit tailcalls for simplicity); the predicate$\texttt{as\_costed}~s$holds if the next instruction to be executed in$s$is a cost emission statement (also classified as \texttt{other}); finally$(\texttt{as\_after\_return}~s_1~s_2)$holds as \texttt{cl\_other}); finally$(\texttt{as\_after\_return}~s_1~s_2)$holds if the next instruction to be executed in$s_2$follows the function call to be executed in (the witness of the$\Sigma$-type)$s_1\$.