From 498a9c2b5f0cf351ffb8bb734f38bfd25e8be205 Mon Sep 17 00:00:00 2001 From: Guillermo Ramos Date: Mon, 23 Jun 2014 20:44:11 +0200 Subject: Sección: Arquitectura --- memoria.tex | 148 ++++++++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 129 insertions(+), 19 deletions(-) diff --git a/memoria.tex b/memoria.tex index 68322d9..91cb653 100755 --- a/memoria.tex +++ b/memoria.tex @@ -8,6 +8,10 @@ \usepackage[pagebackref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref} \usepackage{perpage} +\usepackage{tikz} + +\usetikzlibrary{shapes,arrows} + \input{defs} \input{portada/defs} @@ -379,13 +383,14 @@ anteriormente como el de la inducción sobre listas (list_ind) o la definición Una táctica que vale la pena destacar es \rawec{smt}, que intenta resolver el objetivo actual de la demostración invocando \textbf{resolvedores} -(\textit{solvers}) \textbf{SMT}(<>). Estas -herramientas están diseñadas para intentar encontrar soluciones a fórmulas -expresadas en lógica de primer orden, permitiendo ciertas interpretaciones -adicionales sobre los símbolos. Normalmente soportan ciertas teorías muy útiles -en criptografía como arrays, listas, aritmética entera, etc., y a menudo son -capaces de resolver de forma automática partes repetitivas y tediosas de las -demostraciones, liberando de esa carga de trabajo al criptógrafo. +\textbf{SMT}(<>) (ver sección +\ref{sec:arqu-de-easycrypt}). Estas herramientas están diseñadas para intentar +encontrar soluciones a fórmulas expresadas en lógica de primer orden, +permitiendo ciertas interpretaciones adicionales sobre los símbolos. Normalmente +soportan ciertas teorías muy útiles en criptografía como arrays, listas, +aritmética entera, etc., y a menudo son capaces de resolver de forma automática +partes repetitivas y tediosas de las demostraciones, liberando de esa carga de +trabajo al criptógrafo. \section{Motivación y objetivos} \label{sec:motiv-y-objet} @@ -587,21 +592,126 @@ de su implementación. \section{Arquitectura de EasyCrypt} \label{sec:arqu-de-easycrypt} -EasyCrypt es un programa complejo, y antes de poder modificarlo hay que entender -qué partes lo integran y cómo está organizado a nivel de código. +EasyCrypt está escrito en el lenguaje de programación +OCaml\footnote{\url{http://ocaml.org/}}, que forma parte de la familia ML de +lenguajes especialmente diseñados para el desarrollo de demostraciones. La +unidad de compilación básica de OCaml es el \textbf{módulo}, consistente en un +fichero de implementación con extensión \textbf{.ml} y un fichero de interfaz +con extensión \textbf{.mli} donde se declaran las funciones, tipos, etc. La +compilación es relativamente compleja y se automatiza con ayuda de GNU +Make\footnote{\url{http://www.gnu.org/software/make/}} y +ocamlbuild\footnote{\url{http://caml.inria.fr/pub/docs/manual-ocaml-400/manual032.html}}. + +EasyCrypt usa varios programas externos para llevar a cabo ciertas tareas, pero +los más destacables son los dos siguientes: -\begin{enumerate} -\item Lexer -\item Parser -\item AST -\item ... -\end{enumerate} +\begin{itemize} +\item + \textbf{Resolvedores SMT}. Existen multitud de programas que deciden la + satisfacibilidad de instancias SMT. Como ya se dijo anteriormente, una + instancia de fórmula SMT está expresada en lógica de primer orden y tiene + interpretaciones en teorías como los números reales, vectores, bits, + etc. Durante una demostración en EasyCrypt se pueden invocar estos + resolvedores para tratar de encontrar una solución que satisfaga el objetivo + actual usando la táctica \rawec{smt}. Internamente, EasyCrypt estará + comunicándose con uno o varios resolvedores y obteniendo la respuesa al + problema, si es que existe. Para contar con una única interfaz de + programación ante la diversidad de resolvedores, EasyCrypt usa la plataforma + \textbf{Why3}\footnote{\url{http://why3.lri.fr/}}. +\item + \textbf{Menhir}\footnote{\url{http://gallium.inria.fr/~fpottier/menhir/}}. + Menhir es una biblioteca para generar analizadores léxicos y sintácticos en + OCaml. Volveremos a esto una vez hayamos introducido las fases del análisis + del lenguaje a continuación. +\end{itemize} -% ProofGeneral -% EasyCrypt -% Why3 -% Solvers +A fin de cuentas, EasyCrypt es un intérprete: lee un fichero fuente y realiza +acciones en función de su contenido. Por ello, el componente fundamental es el +\textbf{analizador del lenguaje}, cuya tarea es transformar el código fuente +(secuencia de caracteres) en un árbol sintáctico abstracto anotado con +información de tipos, o mostrar un error y finalizar en caso de que el programa +esté mal formado. + +El análisis del lenguaje consta de varias fases encargadas de abordar niveles +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 sintáctico} +Durante esta fase se transforma la lista de tokens generada durante el análisis +léxico en el denominado \textbf{árbol sintáctico abstracto}, una estructura de +datos que contiene la estructura sintáctica del código fuente. Este analizador +está especificado por 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. +L +\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. + +El siguiente diagrama resume el proceso de análisis del lenguaje de EasyCrypt: + +\tikzstyle{block} = [rectangle, draw, fill=blue!20, + text width=5em, text centered, rounded corners, minimum height=4em] +\tikzstyle{invisbl} = [ + text width=5em, text centered, rounded corners, minimum height=4em] +\tikzstyle{line} = [draw, -latex'] +\tikzstyle{cloud} = [draw, ellipse,fill=green!20, node distance=3cm, + minimum height=2em] + +\begin{center} +\begin{tikzpicture}[node distance = 3cm, auto] + % Nodes + \node [block] (lexer) {EcLexer}; + \node [block, below of=lexer] (parser) {EcParser}; + \node [block, below of=parser] (typing) {EcTyping}; + \node [invisbl, below of=typing] (resto) {...}; + \node [cloud, left of=lexer] (menhir1) {Menhir}; + \node [cloud, left of=parser] (menhir2) {Menhir}; + % Edges + \path [line,dashed] (menhir1) -- (lexer); + \path [line,dashed] (menhir2) -- (parser); + \path [line] + (lexer) edge [] node {\textbf{Tokens} (en EcParser/EcLexer)} (parser) + (parser) edge [] node {\textbf{AST} (en EcParseTree)} (typing) + (typing) edge [] node {\textbf{AST tipado} (en EcFol)} (resto); +\end{tikzpicture} +\end{center} + +Para la implementación del coste es necesario modificar cada uno de los módulos +involucrados en esta cadena. A continuación analizaremos cada una de las etapas +de la implementación tanto del operador especial de coste como del axioma de +coste. + +\section{Modificaciones al analizador léxico} +\label{sec:modif-al-anal-lex} + +\section{Modificaciones al analizador sintáctico} +\label{sec:modif-al-anal-sin} + +\section{Modificaciones al analizador semántico} +\label{sec:modif-al-anal-sem} \chapter{DESARROLLO: INTERFAZ WEB} -- cgit v1.2.3