diff --git a/tesi/conv.py b/tesi/conv.py index 53584c7..5b963c2 100644 --- a/tesi/conv.py +++ b/tesi/conv.py @@ -69,13 +69,46 @@ def ll_rr_bracket(charlist): if not (llrr_mode and ch == '$'): yield ch +def include_files(text): + def put_header(key): + text = '''\\begin{Verbatim}[fontsize=\\footnotesize, + frame=lines, % top and bottom rule only + framesep=2em, % separation between frame and text + rulecolor=\color{Gray}, + label=\\fbox{\color{Black}REPLACEME2}, + labelposition=topline, +]'''.replace('REPLACEME2', key) + return text + + assert type(text) is str + + result = [] + + text = text.split('\n') + cnt = 0 + key = ';; include\_file ' + for line in text: + if key in line: + cnt+=1 + file = line[len(key):] + source = f"traces/{file}" + result.append(put_header(file)) + with open(source, 'r') as f: + result.append(f.read()) + result.append('\end{Verbatim}') + else: + result.append(line) + + i = 45 + return result # convert symbols except the one requiring math mode modifiers firstpass = [convert(*c) for c in read_by_char(argv[1])] # remove a latex error secondpass = latex_errors_replacements(firstpass) thirdpass = ll_rr_bracket(list(secondpass)) +fourthpass = include_files(''.join(thirdpass)) -newfile = ''.join(thirdpass) +newfile = '\n'.join(fourthpass) with open(argv[2], 'w') as f: f.write(newfile) diff --git a/tesi/ltximg/org-ltximg_aaacf10525fe3fe23deb0e9f4989467886d00fc1.png b/tesi/ltximg/org-ltximg_aaacf10525fe3fe23deb0e9f4989467886d00fc1.png new file mode 100644 index 0000000..6edcedb Binary files /dev/null and b/tesi/ltximg/org-ltximg_aaacf10525fe3fe23deb0e9f4989467886d00fc1.png differ diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf index 987c9fb..d7acbc6 100644 Binary files a/tesi/tesi.pdf and b/tesi/tesi.pdf differ diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org index a825d53..c44dfc9 100644 --- a/tesi/tesi_unicode.org +++ b/tesi/tesi_unicode.org @@ -34,6 +34,8 @@ TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerent #+LaTeX_HEADER: \linespread{1.25} #+LaTeX_HEADER: \usepackage{algorithm} #+LaTeX_HEADER: \usepackage{comment} +#+LaTeX_HEADER: \usepackage[dvipsnames]{xcolor} +#+LaTeX_HEADER: \usepackage{fancyvrb} #+LaTeX_HEADER: \usepackage{algpseudocode} #+LaTeX_HEADER: \usepackage{amsmath,amssymb,amsthm} #+LaTeX_HEADER: \newtheorem{definition}{Definition} @@ -75,6 +77,17 @@ TODO: chiedi a Gabriel se T e S vanno bene, ma prima controlla che siano coerent #+LaTeX_HEADER: moredelim=[is][\color{red}]{/[}{]/}, #+LaTeX_HEADER: xleftmargin=1em, #+LaTeX_HEADER: } +#+LaTeX_HEADER: \RecustomVerbatimCommand{\VerbatimInput}{VerbatimInput}% +#+LaTeX_HEADER: {fontsize=\footnotesize, +#+LaTeX_HEADER: frame=lines, % top and bottom rule only +#+LaTeX_HEADER: framesep=2em, % separation between frame and text +#+LaTeX_HEADER: rulecolor=\color{Gray}, +#+LaTeX_HEADER: label=\fbox{\color{Black}DATA}, +#+LaTeX_HEADER: labelposition=topline, +#+LaTeX_HEADER: commandchars=\|\(\), % escape character and argument delimiters for +#+LaTeX_HEADER: commentchar=* % comment character +#+LaTeX_HEADER: } + #+LaTeX_HEADER: \lstset{aboveskip=0.4ex,belowskip=0.4ex} #+EXPORT_SELECT_TAGS: export #+EXPORT_EXCLUDE_TAGS: noexport @@ -536,11 +549,6 @@ set to 0. ** Lambda form compilation -\begin{comment} -https://dev.realworld.org/compiler-backend.html -CITE: realworldocaml -[CIT] -\end{comment} A Lambda code target file is produced by the compiler and consists of a single s-expression. Every s-expression consist of /(/, a sequence of elements separated by a whitespace and a closing /)/. @@ -551,7 +559,7 @@ Elements of s-expressions are: - S-expressions: allowing arbitrary nesting \\ The Lambda form is a key stage where the compiler discards type -informations and maps the original source code to the runtime memory +informations\cite{realworld} and maps the original source code to the runtime memory model described. In this stage of the compiler pipeline pattern match statements are analyzed and compiled into an automata. @@ -651,7 +659,7 @@ Spiega che la sintassi che supporti e` quella nella BNF \end{comment} ** Pattern matching -Pattern matching is a widely adopted mechanism to interact with ADT[CIT]. +Pattern matching is a widely adopted mechanism to interact with ADT\cite{adt_pat}. C family languages provide branching on predicates through the use of if statements and switch statements. Pattern matching on the other hands express predicates through @@ -828,14 +836,14 @@ Execution follows the following inference rules: \\ Even if the semantics of symbolic execution engines are well defined, the user may run into different complications when applying such -analysis to non trivial codebases.[CIT] +analysis to non trivial codebases\cite{symb_tec} For example, depending on the domain, loop termination is not guaranteed. Even when termination is guaranteed, looping causes exponential branching that may lead to path explosion or state -explosion.[CIT] +explosion. Reasoning about all possible executions of a program is not always -feasible[CIT] and in case of explosion usually symbolic execution engines -implement heuristics to reduce the size of the search space.[CIT] +feasible and in case of explosion usually symbolic execution engines +implement heuristics to reduce the size of the search space\cite{sym_three}. ** Translation Validation Translators, such as compilers and code generators, are huge pieces of @@ -851,13 +859,13 @@ equivalence. \subsubsection{Translation Validation as Transation Systems} There are many successful attempts at translation validation of code -translators[CIT] and to a less varying degree of compilers[CIT]. +translators\cite{trans-uno} and to a less varying degree of compilers\cite{trans_due}. Pnueli et al. provide a computational model based on synchronous transition systems to prove a translation verification tool based on the following model. [[./files/translation.png]] The description of the computational models resembles closely the one -in [CIT]. +in \cite{trans-uno}. A synchronous transition system (STS) A = (V, Θ, ρ) where - V: is a finite set of variables; ∑ᵥ is the set of all states over V - Θ: a satisfiable assertion over the state variables of A, @@ -894,7 +902,7 @@ Our work uses bisimulation to prove equivalence. OCaml encourages widespread usage of composite types to encapsulate data. Composite types include /discriminated unions/, of which we have seen different use cases, and /records/, that are a form of /product -types/ [CIT] such as /structures/ in C. \\ +types/ such as /structures/ in C. \\ \begin{minipage}{0.6\linewidth} \begin{verbatim} struct Shape { @@ -1030,7 +1038,7 @@ This BNF grammar describes formally the grammar of the source program: | condition ::= "when" b_guard | assignment ::= "as" id | b_guard ::= ocaml_expression ;; arbitrary code -The source program is parsed using the ocaml-compiler-libs [CIT] library. +The source program is parsed using the ocaml-compiler-libs\cite{o-libs} library. The result of parsing, when successful, results in a list of clauses and a list of type declarations. Every clause consists of three objects: a left-hand-side that is the @@ -1356,10 +1364,10 @@ In our prototype the source matrix mₛ is defined as follows ** Target translation The target program of the following general form is parsed using a parser -generated by Menhir[CIT], a LR(1) parser generator for the OCaml programming language. +generated by Menhir\cite{menhir}, a LR(1) parser generator for the OCaml programming language. Menhir compiles LR(1) a grammar specification, in this case a subset of the Lambda intermediate language, down to OCaml code. -This is the grammar of the target language[CIT] (TODO: check menhir grammar) +This is the grammar of the target language\cite{malfunction} (TODO: check menhir grammar) | start ::= sexpr | sexpr ::= variable \vert{} string \vert{} "(" special_form ")" | string ::= "\"" identifier "\"" ;; string between doublequotes @@ -2136,36 +2144,15 @@ I think the unreachable case should go at the end. * Examples In this section we discuss some examples given as input and output of the prototype tool. -\par\noindent\rule{\textwidth}{0.4pt} -\begin{lstlisting} -external observe : int -> int = "observe" -let mm = function - | 2 -> observe 2 - | 3 -> observe 3 - | 4 -> observe 4 - | _ -> observe 5 -\end{lstlisting} -\par\noindent\rule{\textwidth}{0.4pt} -\begin{lstlisting} -(setglobal Example0! - (let - (mm/81 = - (function param/82[int] : int - (catch - (let (switcher/85 =a (-2+ param/82)) - (if (isout 2 switcher/85) (exit 1) - (switch* switcher/85 - case int 0: (observe 2) - case int 1: (observe 3) - case int 2: (observe 4)))) - with (1) (observe 5)))) - (makeblock 0 mm/81))) -\end{lstlisting} -\par\noindent\rule{\textwidth}{0.4pt} - -\begin{lstlisting} -\end{lstlisting} +;; include_file example0.ml +We can see from this first source file the usage of the /observe/ +directive. +The following is the target file generated by the OCaml compiler. +;; include_file example0.lambda +The prototype tool states that the compilation was successful and the +two programs are equivalent. +;; include_file example0.trace \begin{thebibliography}{9} @@ -2217,4 +2204,40 @@ Charguéraud, A., Filliâtre, J. C., Pereira, M., Pottier F. (2017). \textit{VOCAL–A Verified OCAml Library}. https://hal.inria.fr/hal-01561094/ +\bibitem{realworld} +Yaron Minsky, Anil Madhavapeddy, Jason Hickey +\textit{Real World OCaml: Functional Programming for the masses}. +https://dev.realworld.org/compiler-backend.html + +\bibitem{pat_adt} +Syme, Don, Gregory Neverov, James Margetson. +\textit{Extensible pattern matching via a lightweight language extension}. +Proceedings of the 12th ACM SIGPLAN international conference on Functional programming (2007). + +\bibitem{symb_tec} +Baldoni, Roberto and Coppa, Emilio and D'Elia, Daniele Cono and Demetrescu, Camil and Finocchi, Irene. +\textit{A Survey of Symbolic Execution Techniques}. +ACM Computing Surveys (CSUR), 51(3), 1-39. + +\bibitem{symb_three} +Cadar, Cristian, and Koushik Sen. +\textit{Symbolic execution for software testing: three decades later}. +Communications of the ACM 56.2 (2013): 82-90. + +\bibitem{trans-uno} +Amir Pnueli, Ofer Shtrichman, Michael Siegel. +\textit{Translation Validation: from SIGNAL to C}. +Correct System Design. Springer, Berlin, Heidelberg, 1999. 231-255. + +\bibitem{trans_due} +Necula, George C. +\textit{Translation validation for an optimizing compiler}. +Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation (2000). + +\bibitem{o_libs} +https://github.com/janestreet/ocaml-compiler-libs + +\bibitem{menhir} +Régis-Gianas, François Pottier Yann. +\textit{Menhir Reference Manual}. \end{thebibliography} diff --git a/tesi/traces/example0.lambda b/tesi/traces/example0.lambda new file mode 100644 index 0000000..614a492 --- /dev/null +++ b/tesi/traces/example0.lambda @@ -0,0 +1,13 @@ +(setglobal Example0! + (let + (mm/81 = + (function param/82 + (catch + (let (switcher/85 =a (-2+ param/82)) + (if (isout 2 switcher/85) (exit 1) + (switch* switcher/85 + case int 0: (observe 2) + case int 1: (observe 3) + case int 2: (observe 4)))) + with (1) (observe 5)))) + (makeblock 0 mm/81))) \ No newline at end of file diff --git a/tesi/traces/example0.ml b/tesi/traces/example0.ml new file mode 100644 index 0000000..414d171 --- /dev/null +++ b/tesi/traces/example0.ml @@ -0,0 +1,7 @@ +external observe : 'a -> 'b = "observe" + +let mm = function + | 2 -> observe 2 + | 3 -> observe 3 + | 4 -> observe 4 + | _ -> observe 5 diff --git a/tesi/traces/example0.trace b/tesi/traces/example0.trace new file mode 100644 index 0000000..1f0d6da --- /dev/null +++ b/tesi/traces/example0.trace @@ -0,0 +1,27 @@ +Target program constraint tree +Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [-inf; -1] [3; +inf] v Tag _; }) = + Leaf=VConstant:5 +Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int [0; 2]; }) = + Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int 0; }) = + Leaf=VConstant:2 + Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int 1; }) = + Leaf=VConstant:3 + Switch ({ var=AcAdd(-2 AcRoot=param/82); dom=Int 2; }) = + Leaf=VConstant:4 + Fallback=None +Fallback=None + + +Source program constraint tree +Switch AcRoot:{ + Int 3 -> + Leaf='Int 3 ' + + Int 4 -> + Leaf='Int 4 ' + + Int 2 -> + Leaf='Int 2 ' +} Fallback: Leaf='Int 5 ' + +The two programs are equivalent.