traces

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)

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
+feasible and in case of explosion usually symbolic execution engines
-implement heuristics to reduce the size of the search space.[CIT]
+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
+;; include_file example0.ml
-  | 2 -> observe 2
+We can see from this first source file the usage of the /observe/
-  | 3 -> observe 3
+directive.
-  | 4 -> observe 4
+The following is the target file generated by the OCaml compiler.
-  | _ -> observe 5
+;; include_file example0.lambda
-\end{lstlisting}
+The prototype tool states that the compilation was successful and the
-\par\noindent\rule{\textwidth}{0.4pt}
+two programs are equivalent.
-\begin{lstlisting}
+;; include_file example0.trace
-(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}
 
 
 \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}

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)))

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

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.