diff options
| -rwxr-xr-x | memoria.tex | 126 |
1 files changed, 105 insertions, 21 deletions
diff --git a/memoria.tex b/memoria.tex index ec9c4c2..1cfdf99 100755 --- a/memoria.tex +++ b/memoria.tex @@ -550,8 +550,6 @@ A lo largo de este capítulo se detallará el proceso que se ha seguido para implementar la funcionalidad que permita a la especificación del coste de algoritmos en EasyCrypt. -TODO referencias a dónde se explica qué. - \newpage \section{Motivación} \label{sec:motivacion} @@ -720,14 +718,14 @@ de abstracción distintos. Conceptualmente, las fases de análisis son las siguientes: \begin{itemize} -\item \textbf{Análisis léxico} -Esta fase es la primera que se lleva a cabo y la que tiene un menor nivel de -abstracción; su entrada es el propio fichero fuente. Durante el análisis léxico -se transforma la secuencia de caracteres que forma el código fuente en unidades -mínimas de información (\textbf{tokens}): número, cadena de caracteres, -identificador, comentario, inicio de bloque, etc. La salida de esta fase es una -lista conteniendo todos los tokens que describen el programa original, formando -una estructura de datos muy simple pero más sencilla de recorrer y manejar. +\item \textbf{Análisis léxico} Esta fase es la primera que se lleva a cabo y la + que tiene un menor nivel de abstracción; su entrada es el propio fichero + fuente. Durante el análisis léxico se transforma la secuencia de caracteres + que forma el código fuente en unidades mínimas de información + (\textbf{tokens}): número, cadena de caracteres, identificador, comentario, + inicio de bloque, etc. La salida de esta fase es una lista conteniendo todos + los tokens que describen el programa original, formando una estructura de + datos muy simple pero más sencilla de recorrer y manejar. \item \textbf{Análisis sintáctico} Durante esta fase se transforma la lista de tokens generada durante el análisis léxico en el denominado \textbf{árbol @@ -736,21 +734,21 @@ una estructura de datos muy simple pero más sencilla de recorrer y manejar. la gramática formal del lenguaje (gramáticas libres de contexto, por lo general), cuyas reglas determinan el algoritmo a seguir durante la construcción del árbol sintáctico. -\item \textbf{Análisis semántico/contextual} -Durante esta fase se recorre el árbol sintáctico generado previamente y se anota -con información de tipos, se construye la tabla de símbolos y se comprueba que -el programa, además de estar bien formado sintácticamente, tiene sentido -semánticamente. + +\item \textbf{Análisis semántico/contextual} Durante esta fase se recorre el + árbol sintáctico generado previamente y se anota con información de tipos, se + construye la tabla de símbolos y se comprueba que el programa, además de estar + bien formado sintácticamente, tiene sentido semánticamente. \end{itemize} EasyCrypt implementa cada una de estas etapas en tres módulos (EcLexer, EcParser y EcTyping) y define las estructuras de datos intermedias en otros dos (EcParseTree para el árbol sintáctico abstracto y EcFol para el árbol sintáctico anotado con información de tipos). Los módulos EcLexer y EcParser hacen uso de -la biblioteca Menhir mencionada anteriormente para generar los -analizadores. Estos módulos contienen las definiciones de tokens y las reglas de -las gramáticas regular y libre de contexto usadas para indicar, respectivamente, -el comportamiento de los analizadores léxico y sintáctico. Todo este proceso +la biblioteca Menhir mencionada anteriormente para generar los analizadores. +Estos módulos contienen las definiciones de tokens y las reglas de las +gramáticas regular y libre de contexto usadas para indicar, respectivamente, el +comportamiento de los analizadores léxico y sintáctico. Todo este proceso aparece ilustrado en la figura \ref{fig:ecparser}. \tikzstyle{line} = [draw] @@ -853,6 +851,7 @@ Form>>. La sintaxis concreta que usa Menhir es la siguiente: | [<tokens o reglas>] { <valor_semántico> } | [<tokens o reglas>] { <valor_semántico> } | ... + ; \end{lstlisting} Cada regla define un símbolo no terminal ($<$nombre_regla$>$) que la identifica, @@ -863,7 +862,90 @@ referencia a tokens o a otras reglas, y termina con una expresión entre llaves <<\{ , \}>> conteniendo las \textbf{acciones semánticas} de la regla (los efectos secundarios que se llevan a cabo durante su expansión). -TODO: modificaciones en EcParser y EcParseTree +Como el objetivo de esta fase es generar un árbol sintáctico abstracto, cada +regla será la responsable de generar un nodo con su representación abstracto +como acción semántica. Por eso, antes de escribir nuestras reglas modificaremos +el fichero que define el árbol sintáctico. + +Para empezar, añadiremos un nodo que represente el operador especial de +coste. De ahora en adelante lo llamaremos \textbf{expresión} de coste, ya que al +fin y al cabo es una expresión (se evalúa a un número entero) y no provoca +ambigüedad con el resto de operadores normales. La definición es la siguiente: + +\begin{code} + \begin{minted}{ocaml} +type pcexpr = (pqsymbol * pexpr list) located + \end{minted} + \caption{Nodo: expresión de coste (ecParseTree.ml)} +\end{code} + +Es decir, que ``pcexpr'' (<<parsed cost expression>>) es un tipo de datos cuyos +valores son tuplas <<(símbolo, [expresiones])>> que almacenan respectivamente el +operador cuyo coste se está evaluando y sus argumentos, y además contienen +información de su ubicación en el código fuente: fila y columna +(<<located>>). + +A continuación definiremos el nodo correspondiente al axioma de coste: + +\begin{code} + \begin{minted}{ocaml} +type pcaxiom = { + pca_name : psymbol; + pca_cargs : ptybindings option; + pca_spec : pformula; +} + \end{minted} + \caption{Nodo: axioma de coste (ecParseTree.ml)} +\end{code} + +El axioma de coste es un ``record'' (estructura de datos con varios campos) que +almacena su nombre, argumentos (opcionales) y especificación. La especificación +es una fórmula: expresiones que pueden estar cuantificadas existencialmente o +universalmente. Por tanto, también necesitaremos modificar el tipo de datos +fórmula para que pueda contener expresiones de coste: + +\begin{code} + \begin{minted}{ocaml} +type pformula = pformula_r located + +and pformula_r = + | PFhole + | PFint of int + | PFtuple of pformula list + + (* ... *) + + | PFcost of pcexpr + \end{minted} + \caption{Nodo: fórmulas (ecParseTree.ml)} +\end{code} + +Una vez tenemos los nodos definidos, volvemos al analizador sintáctico para +definir las reglas: + +\begin{lstlisting}[frame=lrtb] +cexpr: + | COST '[' op=qident ']' + { (* ... *) + (op, []) } + | COST '[' op=qident ',' ps=plist0(expr, ',') ']' + { (* ... *) + (op, ps) } + ; + +caxiom: + | CAXIOM x=ident args=ptybindings? ':' spec=form + { { pca_name=x; pca_cargs=args; pca_spec=spec } } + ; +\end{lstlisting} + +Se puede observar cómo cada regla, además de definir la sintaxis, crea su nodo +correspondiente y lo devuelve como valor semántico. Esto es todo lo que +necesitamos para que EasyCrypt reconozca sintácticamente las nuevas +construcciones. + +A continuación pasaremos a la última etapa de la implementación del coste, y la +más compleja: modificar el analizador semántico. \section{Modificaciones al analizador semántico} \label{sec:modif-al-anal-sem} @@ -1268,7 +1350,7 @@ A continuación veremos los pasos que se han realizado para abordar la implementación del cliente, partiendo del diseño de la figura \ref{fig:prototype}. -\subsection{Colocación de elementos} +\subsection{Colocación de elementos} %TODO quitar (índice) \label{sec:coloc-de-elem} A la hora de distribuir los elementos de la página principal se ha usado una @@ -1428,6 +1510,8 @@ A lo largo de este documento hemos abordado la mejora de dos aspectos relativamente independientes de EasyCrypt: una principalmente técnica (coste) y otra de usabilidad (interfaz web). +% TODO qué he aprendido + EasyCrypt es un marco orientado a un usuario muy concreto: profesionales de la criptografía. Si bien es cierto que en el propio Instituto IMDEA Software se usa y desarrolla activamente, el objetivo último sería crear comunidad. La |