bparodi/UniTO
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of http://francescomecca.eu/git/git/pesceWanda/UNITO

Browse source
This commit is contained in:
Francesco Mecca 2020-04-08 11:20:13 +02:00
commit d2c9f70bf8
10 changed files with 910 additions and 102 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
tesi/conv.py
View file

@ -3,8 +3,8 @@ import re
from sys import argv from sys import argv
allsymbols = json.load(open('./unicode-latex.json')) allsymbols = json.load(open('./unicode-latex.json'))
mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒' ] mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', 'ε', '₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈' ]
extrasymbols = {'〚': '\llbracket', '〛': '\rrbracket'} extrasymbols = {'〚': '\llbracket', '〛': r'\rrbracket', '̸': '\neg', '¬̸': '\neg', '∈': '\in ', 'ₛ': '_S', 'ₜ': '_T'}
symbols = {s: allsymbols[s] for s in mysymbols} symbols = {s: allsymbols[s] for s in mysymbols}
symbols.update(extrasymbols) symbols.update(extrasymbols)
@ -13,8 +13,8 @@ mathsymbols = {s: '$'+v+'$' for s, v in symbols.items()}
def read_by_char(fname): def read_by_char(fname):
# Yield character and True/False if inside mathmode block # Yield character and True/False if inside mathmode block
mathmode = False mathmode = False
mathmode_begin = set(['\\begin{equation*}', '\\begin{equation}']) mathmode_begin = set(['\\begin{equation*}', '\\begin{equation}', '\[', '\\begin{mathpar}'])
mathmode_end = set(['\\end{equation*}', '\\end{equation}']) mathmode_end = set(['\\end{equation*}', '\\end{equation}', '\]', '\\end{mathpar}'])
cnt = 0 cnt = 0
with open(fname, 'r') as fp: with open(fname, 'r') as fp:
for line in fp.readlines(): for line in fp.readlines():
@ -50,11 +50,26 @@ def latex_errors_replacements(charlist):
yield from word yield from word
yield ' ' yield ' '
def ll_rr_bracket(charlist):
llrr_mode = False
for i, ch in enumerate(charlist):
if ch == '\\':
if charlist[i:i+10] == '\llbracket':
assert llrr_mode is False ; llrr_mode = True
elif charlist[i:i+10] == '\rrbracket':
assert llrr_mode is True ; llrr_mode = False
if not (llrr_mode and ch == '$'):
yield ch
# convert symbols except the one requiring math mode modifiers # convert symbols except the one requiring math mode modifiers
firstpass = [convert(*c) for c in read_by_char(argv[1])] firstpass = [convert(*c) for c in read_by_char(argv[1])]
# remove a latex error # remove a latex error
secondpass = latex_errors_replacements(firstpass) secondpass = latex_errors_replacements(firstpass)
thirdpass = ll_rr_bracket(list(secondpass))
newfile = ''.join(secondpass) newfile = ''.join(thirdpass)
with open(argv[2], 'w') as f: with open(argv[2], 'w') as f:
f.write(newfile) f.write(newfile)

1
tesi/files/symb_exec Normal file
View file

@ -0,0 +1 @@
<mxfile host="app.diagrams.net" modified="2020-04-07T18:00:18.130Z" agent="5.0 (X11)" etag="UqJT9eDZirhT4ZuYmnlI" version="12.9.9" type="device"><diagram id="vkyFxs9FE47iKiCmcqWQ" name="Page-1">7VpLk+I2EP41rpoccFnyA/sIDJsckspjDsnuJaWxBahiW0QWC+yvj2RLfsmzDCwBdoYqCqyvpZb0dUvqlrHcWbb7kaH16hea4NSCTrKz3EcLwjAIxLcE9hXgRVEFLBlJKgg0wBP5ghXoKHRDElx0KnJKU07WXTCmeY5j3sEQY3TbrbagabfXNVpiA3iKUWqif5KEr9S0fKfBf8JkudI9A0dJMqQrK6BYoYRuW5A7t9wZo5RXT9luhlPJnealavfhBWk9MIZz/poGPz99+n3y6dcYzpztl+c/wH7ERiOl5TNKN2rCMc3WiAvswbbtH9TQ+V7zwegmT7BUCSx3ul0Rjp/WKJbSrXAAga14liqxUo4Zx7sXRw1qLoQPYZphzvaiimrgavq0/6jitjFGTfmqZQhdDyn7L2vNDUXiQbF0BGPQYMzyp8DyHw2qxKR5l4+CM/oPntGUMoHkNBc1pwuSpj0IpWSZi2IsSMICn0oKiXDKiRJkJElkN4MGaEzknMcGMOzawDdt4A2YAP5fJnBNE4zFPEV3QSoZL9Yo75gi+HcjV9k0xQvxMxEy33Ns33PXO9lMkiR2lXUlGvuBDUPYEi1ozkdFuTXJCiC0QQjCfoUFyki6r6oUKC9GBWZk0XQunpbl7+yDFdZjFQRUw1VCBUuNUo/eD7USMKBPz3rzbECvIMJ37MgZDxIRQNtzjHm2iACnczC3yrl8jQMJm3MSaEWOgsu+RtYcWmFoRfPKDVAmF4Kq7+jeBiTtZuM3vIS94OASBuNLrmHPXMN98nGeTOQJLllMUVGQuGsKvCP8L0mR7avSx5bkcafYKwt7XcjF4FuNZPFjW9Y0K0v7jglwYgQLPQOICdANi/HhI5cjtsT8K/WCYYO2LOYPGExjDKeIk8/d4Q5ZUfXwGyXljqOPXa/rL7VzaBXVNFWrdtTRV9RzPND3qIoHQ1HpVPW0T/ezwPCzjMg98aHcht1yAxAfQdCs3CnaILy98Kem72rxz3go/oHvKv4B7pUDoPAMAVDg2KEDjwiAXn22HzGIUGzDbnizUdgL8ImR1hjYILh8pFXuaKdEWm89Br1Q9Dl00hjHzIHQ1L2nN9+Va91KeiMl8CQHus5mdWDf/f5PlBO9OJJePLychTWCzkrvzSr6JieGxzlxqdS27bedS/uHw8E67blIPBgZ8WCMCv6w+VskVfJwuc2rXOhcO5cB5vX3e7mFCF55CxHd0i1E/Vbo6FuIqLdkg8veQoDBtwbuu8qaa+NdK2sG53hvcE+b72nzPW0+S1bjWCrLjayJZ9WJ8j0bfmsec8+G79nwPRt+o2GeB/2DYV4dfl8mzvO/Pas7Y6Z13Qxq3AvCo1MzqL6i8MIZlPkiV686ohccw4UcMV3ILWGFpQF3ON5wQnNd95kNrFnSYLd2RRKai+lcVySi2Pz5sDJT8w9Od/4f</diagram></mxfile>

BIN
tesi/files/symb_exec.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 18 KiB

3
tesi/files/symb_exec.svg Normal file
View file

File diff suppressed because one or more lines are too long
Side by side

After

Width:  |  Height:  |  Size: 15 KiB

469
tesi/mathpartir.sty Normal file
View file

@ -0,0 +1,469 @@
%%
%% This is file `mathpartir.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% mathpartir.dtx (with options: `package')
%%
%% This is a generated file.
%%
%% Copyright (C) 2015, 2020 by Didier Remy <didier.remy(at)inria(dot)fr>
%%
%% This file is part of mathpartir.
%%
%% mathpartir is free software: you can redistribute it and/or modify
%% it under the terms of the GNU General Public License as published by
%% the Free Software Foundation, either version 2 of the License, or
%% (at your option) any later version.
%%
%% mathpartir is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
%% GNU General Public License for more details.
%%
%% You should have received a copy of the GNU General Public License
%% along with mathpartir. If not, see <http://www.gnu.org/licenses/>.
%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{mathpartir}
[2020/02/15 version 1.4.0 Math Paragraph for Typesetting Inference Rules]
%% Identification
%% Preliminary declarations
\RequirePackage {keyval}
%% Options
%% More declarations
%% PART I: Typesetting maths in paragraphe mode
%% \newdimen \mpr@tmpdim
%% Dimens are a precious ressource. Uses seems to be local.
\let \mpr@tmpdim \@tempdima
\let \mpr@hva \empty
%% normal paragraph parametters, should rather be taken dynamically
\def \mpr@savepar {%
\edef \MathparNormalpar
{\noexpand \lineskiplimit \the\lineskiplimit
\noexpand \lineskip \the\lineskip}%
}
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
\let \MathparLineskip \mpr@lineskip
\def \mpr@paroptions {\MathparLineskip}
\let \mpr@prebindings \relax
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
\def \mpr@goodbreakand
{\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
\def \mpr@and {\hskip \mpr@andskip}
\def \mpr@andcr {\penalty 50\mpr@and}
\def \mpr@cr {\penalty -10000\mpr@and}
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
\def \mpr@bindings {%
\let \and \mpr@andcr
\let \par \mpr@andcr
\let \\\mpr@cr
\let \eqno \mpr@eqno
\let \hva \mpr@hva
}
\let \MathparBindings \mpr@bindings
\def \MathparBeginhook {}
\def \MathparEndhook {}
\let \MathparCentering \centering
\newenvironment{mathpar}[1][]
{$$
\MathparBeginhook
%% We save \lineskip parameters so that the user can restore them
%% inside math \MathparNormalpar
\mpr@savepar
%% We define the shape of the paragrah
\parskip 0em \hsize \linewidth \MathparCentering
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
\noindent $\displaystyle\fi
\MathparBindings}
{\MathparEndhook \unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
\newenvironment{mathparpagebreakable}[1][]
{\begingroup
\par
\mpr@savepar \parskip 0em \hsize \linewidth \centering
\mpr@prebindings \mpr@paroptions #1%
\vskip \abovedisplayskip \vskip -\lineskip%
\ifmmode \else $\displaystyle\fi
\MathparBindings
}
{\unskip
\ifmmode $\fi \par\endgroup
\vskip \belowdisplayskip
\noindent
\ignorespacesafterend}
%%% HOV BOXES
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
\vbox \bgroup \tabskip 0em \let \\ \cr
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
\egroup}
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
\box0\else \mathvbox {#1}\fi}
%% Part II -- operations on lists
\newtoks \mpr@lista
\newtoks \mpr@listb
\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
\mpr@flatten \mpr@all \mpr@to \mpr@one
\expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
\mpr@all \mpr@stripend
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
\ifx 1\mpr@isempty
\repeat
}
\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
\def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
%% Part III -- Type inference rules
\newif \if@premisse
\newbox \mpr@hlist
\newbox \mpr@vlist
\newif \ifmpr@center \mpr@centertrue
\def \mpr@vskip {}
\let \mpr@vbox \vbox
\def \mpr@htovlist {%
\setbox \mpr@hlist
\hbox {\strut
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
\unhbox \mpr@hlist}%
\setbox \mpr@vlist
\mpr@vbox {\if@premisse
\box \mpr@hlist
\ifx \mpr@vskip \empty \else
\hrule height 0em depth \mpr@vskip width 0em
\fi
\unvbox \mpr@vlist
\else
\unvbox \mpr@vlist
\ifx \mpr@vskip \empty \else
\hrule height 0em depth \mpr@vskip width 0em
\fi
\box \mpr@hlist
\fi}%
}
\def \mpr@item #1{$\displaystyle #1$}
\def \mpr@sep{2em}
\def \mpr@blank { }
\def \mpr@hovbox #1#2{\hbox
\bgroup
\ifx #1T\@premissetrue
\else \ifx #1B\@premissefalse
\else
\PackageError{mathpartir}
{Premisse orientation should either be T or B}
{Fatal error in Package}%
\fi \fi
\def \@test {#2}\ifx \@test \mpr@blank\else
\setbox \mpr@hlist \hbox {}%
\setbox \mpr@vlist \vbox {}%
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
\let \@hvlist \empty \let \@rev \empty
\mpr@tmpdim 0em
\expandafter \mpr@makelist #2\mpr@to \mpr@flat
\if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
\def \\##1{%
\def \@test {##1}\ifx \@test \empty
\mpr@htovlist
\mpr@tmpdim 0em %%% last bug fix not extensively checked
\else
\setbox0 \hbox{\mpr@item {##1}}\relax
\advance \mpr@tmpdim by \wd0
%\mpr@tmpdim 1.02\mpr@tmpdim
\ifnum \mpr@tmpdim < \hsize
\ifnum \wd\mpr@hlist > 0
\if@premisse
\setbox \mpr@hlist
\hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
\else
\setbox \mpr@hlist
\hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
\fi
\else
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\else
\ifnum \wd \mpr@hlist > 0
\mpr@htovlist
\mpr@tmpdim \wd0
\fi
\setbox \mpr@hlist \hbox {\unhbox0}%
\fi
\advance \mpr@tmpdim by \mpr@sep
\fi
}%
\@rev
\mpr@htovlist
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
\fi
\egroup
}
%%% INFERENCE RULES
\@ifundefined{@@over}{%
\let\@@over\over % fallback if amsmath is not loaded
\let\@@overwithdelims\overwithdelims
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
\let\@@above\above \let\@@abovewithdelims\abovewithdelims
}{}
%% The default
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
$\displaystyle {#1\mpr@over #2}$}}
\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
$\displaystyle {#1\@@atop #2}$}}
\let \mpr@fraction \mpr@@fraction
%% A generic solution to arrow
\def \mpr@@fractionaboveskip {0ex}
\def \mpr@@fractionbelowskip {0.22ex}
\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
\def \mpr@tail{#1}%
\def \mpr@body{#2}%
\def \mpr@head{#3}%
\setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
\setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
\dimen0\ht3\advance\dimen0 by \dp3\relax
\dimen0 0.5\dimen0\relax
\advance \dimen0 by \mpr@@fractionaboveskip
\setbox1=\hbox {\raise \dimen0 \box1}\relax
\dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
\advance \dimen0 by \mpr@@fractionbelowskip
\setbox2=\hbox {\lower \dimen0 \box2}\relax
\setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
\dimen0=\wd0\box0
\box0 \hskip -\dimen0\relax
\hbox to \dimen0 {$%\color{blue}
\mathrel{\mpr@tail}\joinrel
\xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
$}}}
%% Old stuff should be removed in next version
\def \mpr@@nothing #1#2
{$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
\def \mpr@@reduce #1#2{\hbox
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
\def \mpr@@rewrite #1#2#3{\hbox
{$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
\def \mpr@empty {}
\def \mpr@inferrule
{\bgroup
\ifnum \linewidth<\hsize \hsize \linewidth\fi
\mpr@rulelineskip
\let \and \qquad
\let \hva \mpr@hva
\let \@rulename \mpr@empty
\let \@rule@options \mpr@empty
\let \mpr@over \@@over
\mpr@inferrule@}
\newcommand {\mpr@inferrule@}[3][]
{\everymath={\displaystyle}%
\def \@test {#2}\ifx \empty \@test
\def \@test {#3}\ifx \empty \@test
\PackageWarning {mathpartir}
{\string\inferrule\space empty arguments substituted}{}%
\setbox0 \mpr@fraction {?}{?}%
\else
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
\fi
\else
\def \@test {#3}\ifx \empty \@test
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
\else
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
\fi \fi
\def \@test {#1}\ifx \@test\empty \box0
\else \vbox
%%% Suggestion de Francois pour les etiquettes longues
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
{\hbox {\DefTirName {#1}}\box0}\fi
\egroup}
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
%% Version for Hoare triples
\def \triple@hlinebox{\noalign{\setbox0\hbox {}\dp0 0.1ex\ht0 0.1ex\box0}}
\def \triple@hline {\triple@hlinebox\hline\triple@hlinebox}
\newcommand{\triplerule}[4][]
{\bgroup
\ifnum \linewidth<\hsize \hsize \linewidth\fi
\mpr@rulelineskip
\let \and \qquad
\let \hva \mpr@hva
\setbox0 \hbox {\begin{array}[b]{@{}c@{}}
\mpr@hovbox{T}{#2}\cr\triple@hline
\mpr@hovbox{T}{#3}\cr\triple@hline
\let \mpr@vbox \vtop \ht0 0em
\setbox0 \strut \@tempdima \ht0
\setbox0 \mpr@hovbox{B}{#4}\advance \@tempdima by -\ht0
\setbox0 \hbox{\raise \@tempdima \box0}\box0
\end{array}}%
\def \@test {#1}\ifx \@test\empty \box0
\else \vbox
%%% Suggestion de Francois pour les etiquettes longues
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
{\hbox {\DefTirName {#1}}\box0}\fi
\egroup}
%% Keys that make sence in all kinds of rules
\def \mprset #1{\setkeys{mprset}{#1}}
\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
\define@key {mprset}{lineskip}[]{\lineskip=#1}
\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
\define@key {mprset}{center}[]{\mpr@centertrue}
\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction}
\define@key {mprset}{sep}{\def\mpr@sep{#1}}
\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def}
\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}}
\newbox \mpr@right
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
\define@key {mpr}{center}[]{\mpr@centertrue}
\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
\define@key {mpr}{width}{\hsize #1}
\define@key {mpr}{sep}{\def\mpr@sep{#1}}
\define@key {mpr}{before}{#1}
\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}}
\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def}
\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}}
\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}}
\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}}
\define@key {mpr}{narrower}{\hsize #1\hsize}
\define@key {mpr}{leftskip}{\hskip -#1}
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
\define@key {mpr}{rightskip}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax
\advance \hsize by -\wd0\box0}
\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}}
\define@key {mpr}{right}
{\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{RIGHT}
{\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
\define@key {mpr}{Right}
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}}
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
\define@key {mpr}{vcenter}[]{\mpr@vcentertrue}
\newif \ifmpr@vcenter \mpr@vcenterfalse
\newcommand \mpr@inferstar@ [3][]{\begingroup
\setbox0 \hbox
{\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
\setbox \mpr@right \hbox{}%
\setkeys{mpr}{#1}%
$\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
\box \mpr@right \mpr@vdots$
\ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi}
\ifmpr@vcenter
\box0
\else
\setbox1 \hbox {\strut}
\@tempdima \dp0 \advance \@tempdima by -\dp1
\raise \@tempdima \box0
\fi
\endgroup}
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
\newcommand \mpr@err@skipargs[3][]{}
\def \mpr@inferstar*{\ifmmode
\let \@do \mpr@inferstar@
\else
\let \@do \mpr@err@skipargs
\PackageError {mathpartir}
{\string\inferrule* can only be used in math mode}{}%
\fi \@do}
%%% Exports
\let \inferrule \mpr@infer
\@ifundefined {infer}{\let \infer \mpr@infer}{}
\def \TirNameStyle #1{\small \textsc{#1}}
\def \LeftTirNameStyle #1{\TirNameStyle {#1}}
\def \RightTirNameStyle #1{\TirNameStyle {#1}}
\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}}
\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}}
\let \TirName \lefttir@name
\let \LeftTirName \lefttir@name
\let \DefTirName \lefttir@name
\let \LabTirName \lefttir@name
\let \RightTirName \righttir@name
%%% Other Exports
\endinput
%%
%% End of file `mathpartir.sty'.

2
tesi/mumble_meeting_gabriel
View file

@ -12,7 +12,7 @@ Test(S,true) = Yes
------------------------------- -------------------------------
equiv \emptyset Cs Ct gs ~> Yes equiv \emptyset Cs Ct gs \to Yes
----------------------------------------- -----------------------------------------
equiv S Failure (Leaf BBt) gs ~>No(vs, vt) equiv S Failure (Leaf BBt) gs ~>No(vs, vt)

36
tesi/notations.sty Normal file
View file

@ -0,0 +1,36 @@
\newcommand{\bnfeq}{\mathrel{::=}\;}
\newcommand{\bnfor}{\mathrel{\vert}}
\newcommand{\paramrel}[3]{#2 \mathrel{\approx_{#1}} #3}
\newcommand{\vrel}[2]{\paramrel{\mathsf{val}}{#1}{#2}}
\newcommand{\trel}[2]{\paramrel{\mathsf{term}}{#1}{#2}}
\newcommand{\sem}[1]{{\llbracket{#1}\rrbracket}}
\newcommand{\Fam}[2]{{(#2)}^{#1}}
\newcommand{\match}[2]{\mathtt{match}(#1,#2)}
\newcommand{\var}[1]{\mathtt{#1}}
\newcommand{\pK}{\mathtt{K}}
\newcommand{\any}{\mathtt{\_}}
% \equiv is already taken
\newcommand{\Equiv}[4]{\mathsf{equiv}(#1, #2, #3, #4)}
\newcommand{\Equivrel}[4]{#1 \vdash_{#4} #2 \approx #3}
\newcommand{\covers}[2]{#1 \mathrel{\mathsf{covers}} #2}
\newcommand{\Yes}{\mathsf{Yes}}
\newcommand{\No}[2]{\mathsf{No}(#1, #2)}
\newcommand{\Leaf}[1]{\mathsf{Leaf}(#1)}
\newcommand{\Failure}{\mathsf{Failure}}
\newcommand{\Switch}[3]{\mathsf{Switch}(#1, #2, #3)}
\newcommand{\Guard}[3]{\mathsf{Guard}(#1, #2, #3)}
\newcommand{\emptyqueue}{\mathord{[]}}
\newcommand{\Cfb}{C_{\mathsf{fb}}}
\newcommand{\trim}[2]{\mathsf{trim}(#1, #2)}

BIN
tesi/tesi.pdf
View file

Binary file not shown.

476
tesi/tesi_unicode.org
View file

@ -1,11 +1,11 @@
\begin{comment} \begin{comment}
* TODO Scaletta [1/6] * TODO Scaletta [1/6]
- [X] Introduction - [X] Introduction
- [-] Background [60%] - [-] Background [80%]
- [X] Low level representation - [X] Low level representation
- [X] Lambda code [0%] - [X] Lambda code [0%]
- [X] Pattern matching - [X] Pattern matching
- [ ] Symbolic execution - [X] Symbolic execution
- [ ] Translation Validation - [ ] Translation Validation
- [ ] Translation validation of the Pattern Matching Compiler - [ ] Translation validation of the Pattern Matching Compiler
- [ ] Source translation - [ ] Source translation
@ -31,6 +31,7 @@ Magari prima pattern matching poi compilatore?
#+LANGUAGE: en #+LANGUAGE: en
#+LaTeX_CLASS: article #+LaTeX_CLASS: article
#+LaTeX_HEADER: \linespread{1.25}
#+LaTeX_HEADER: \usepackage{algorithm} #+LaTeX_HEADER: \usepackage{algorithm}
#+LaTeX_HEADER: \usepackage{comment} #+LaTeX_HEADER: \usepackage{comment}
#+LaTeX_HEADER: \usepackage{algpseudocode} #+LaTeX_HEADER: \usepackage{algpseudocode}
@ -41,11 +42,32 @@ Magari prima pattern matching poi compilatore?
#+LaTeX_HEADER: \usepackage{listings} #+LaTeX_HEADER: \usepackage{listings}
#+LaTeX_HEADER: \usepackage{color} #+LaTeX_HEADER: \usepackage{color}
#+LaTeX_HEADER: \usepackage{stmaryrd} #+LaTeX_HEADER: \usepackage{stmaryrd}
#+LaTeX_HEADER: \newcommand{\sem}[1]{{\llbracket{#1}\rrbracket}} #+LaTeX_HEADER: \newcommand{\semTEX}[1]{{\llbracket{#1}\rrbracket}}
#+LaTeX_HEADER: \newcommand{\Equiv}[3]{\mathsf{equiv}(#1, #2, #3)} % \equiv is already taken #+LaTeX_HEADER: \newcommand{\EquivTEX}[3]{\mathsf{equiv}(#1, #2, #3)} % \equiv is already taken
#+LaTeX_HEADER: \newcommand{\covers}[2]{#1 \mathrel{\mathsf{covers}} #2} #+LaTeX_HEADER: \newcommand{\coversTEX}[2]{#1 \mathrel{\mathsf{covers}} #2}
#+LaTeX_HEADER: \newcommand{\Yes}{\mathsf{Yes}} #+LaTeX_HEADER: \newcommand{\YesTEX}{\mathsf{Yes}}
#+LaTeX_HEADER: \newcommand{\No}[2]{\mathsf{No}(#1, #2)} #+LaTeX_HEADER: \newcommand{\NoTEX}[2]{\mathsf{No}(#1, #2)}
#+LaTeX_HEADER: \usepackage{comment}
#+LaTeX_HEADER: \usepackage{mathpartir}
#+LaTeX_HEADER: \usepackage{stmaryrd} % llbracket, rrbracket
#+LaTeX_HEADER: \usepackage{listings}
#+LaTeX_HEADER: \usepackage{notations}
#+LaTeX_HEADER: \lstset{
#+LaTeX_HEADER: mathescape=true,
#+LaTeX_HEADER: language=[Objective]{Caml},
#+LaTeX_HEADER: basicstyle=\ttfamily,
#+LaTeX_HEADER: extendedchars=true,
#+LaTeX_HEADER: showstringspaces=false,
#+LaTeX_HEADER: aboveskip=\smallskipamount,
#+LaTeX_HEADER: % belowskip=\smallskipamount,
#+LaTeX_HEADER: columns=fullflexible,
#+LaTeX_HEADER: moredelim=**[is][\color{blue}]{/*}{*/},
#+LaTeX_HEADER: moredelim=**[is][\color{green!60!black}]{/!}{!/},
#+LaTeX_HEADER: moredelim=**[is][\color{orange}]{/(}{)/},
#+LaTeX_HEADER: moredelim=[is][\color{red}]{/[}{]/},
#+LaTeX_HEADER: xleftmargin=1em,
#+LaTeX_HEADER: }
#+LaTeX_HEADER: \lstset{aboveskip=0.4ex,belowskip=0.4ex}
#+EXPORT_SELECT_TAGS: export #+EXPORT_SELECT_TAGS: export
#+EXPORT_EXCLUDE_TAGS: noexport #+EXPORT_EXCLUDE_TAGS: noexport
@ -121,7 +143,6 @@ the case of a production compiler and to integrate with an existing code base. T
black-box and proof only depends on our equivalence algorithm. black-box and proof only depends on our equivalence algorithm.
\subsection{Our approach} \subsection{Our approach}
%% replace common TODO
Our algorithm translates both source and target programs into a common Our algorithm translates both source and target programs into a common
representation, decision trees. Decision trees where chosen because representation, decision trees. Decision trees where chosen because
they model the space of possible values at a given branch of they model the space of possible values at a given branch of
@ -206,12 +227,12 @@ matched by the source clauses.
\texttt{Unreachable} is used when we statically know that no value \texttt{Unreachable} is used when we statically know that no value
can flow to that subtree. can flow to that subtree.
We write $\sem{t_S}_S$ for the decision tree of the source program We write 〚tₛ〛ₛ for the decision tree of the source program
$t_S$, computed by a matrix decomposition algorithm (each column t_S, computed by a matrix decomposition algorithm (each column
decomposition step gives a \texttt{Switch} node). decomposition step gives a \texttt{Switch} node).
It satisfies the following correctness statement: It satisfies the following correctness statement:
\[ \[
\forall t_S, \forall v_S, \quad t_S(v_S) = \sem{t_S}_S(v_S) \forall t_s, \forall v_s, \quad t_s(v_s) = \semTEX{t_s}_s(v_s)
\] \]
Running any source value $v_S$ against the source program gives the Running any source value $v_S$ against the source program gives the
same result as running it against the decision tree. same result as running it against the decision tree.
@ -229,10 +250,10 @@ nodes are never emitted.
Guards result in branching. In comparison with the source decision Guards result in branching. In comparison with the source decision
trees, \texttt{Unreachable} nodes are never emitted. trees, \texttt{Unreachable} nodes are never emitted.
We write $\sem{t_T}_T$ for the decision tree of the target program We write $\semTEX{t_T}_T$ for the decision tree of the target program
$t_T$, satisfying the following correctness statement: $t_T$, satisfying the following correctness statement:
\[ \[
\forall t_T, \forall v_T, \quad t_T(v_T) = \sem{t_T}_T(v_T) \forall t_T, \forall v_T, \quad t_T(v_T) = \semTEX{t_T}_T(v_T)
\] \]
\subsection{Equivalence checking} \subsection{Equivalence checking}
@ -241,38 +262,38 @@ possible values \emph{S} and a pair of source and target decision trees and
in case the two trees are not equivalent it returns a counter example. in case the two trees are not equivalent it returns a counter example.
The algorithm respects the following correctness statement: The algorithm respects the following correctness statement:
\begin{comment} \begin{comment}
% TODO: we have to define what \covers mean for readers to understand the specifications % TODO: we have to define what \coversTEX mean for readers to understand the specifications
% (or we use a simplifying lie by hiding \covers in the statements). % (or we use a simplifying lie by hiding \coversTEX in the statements).
\end{comment} \end{comment}
\begin{align*} \begin{align*}
\Equiv S {C_S} {C_T} = \Yes \;\land\; \covers {C_T} S \EquivTEX S {C_S} {C_T} = \YesTEX \;\land\; \coversTEX {C_T} S
& \implies & \implies
\forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T) \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T)
\\ \\
\Equiv S {C_S} {C_T} = \No {v_S} {v_T} \;\land\; \covers {C_T} S \EquivTEX S {C_S} {C_T} = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S
& \implies & \implies
v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T) v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T)
\end{align*} \end{align*}
The algorithm proceeds by case analysis. Inference rules are shown. The algorithm proceeds by case analysis. Inference rules are shown.
If $S$ is empty the results is $\Yes$. If $S$ is empty the results is $\YesTEX$.
\begin{mathpar}
\begin{verbatim} \infer{ }
------------------------ {\EquivTEX \emptyset {C_S} {C_T} G}
equiv \emptyset Cs Ct gs \end{mathpar}
\end{verbatim}
If the two decision trees are both terminal nodes the algorithm checks If the two decision trees are both terminal nodes the algorithm checks
for content equality. for content equality.
\begin{verbatim} \begin{mathpar}
-------------------------- \infer{ }
equiv S Failure Failure [] {\EquivTEX S \Failure \Failure \emptyqueue}
\\
\infer
{\trel {t_S} {t_T}}
{\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
equiv_BB BBs BBt \end{mathpar}
-------------------------------
equiv S (Leaf BBs) (Leaf BBt) []
\end{verbatim}
If the source decision tree (left hand side) is a terminal while the If the source decision tree (left hand side) is a terminal while the
target decistion tree (right hand side) is not, the algorithm proceeds target decistion tree (right hand side) is not, the algorithm proceeds
@ -280,13 +301,16 @@ by \emph{explosion} of the right hand side. Explosion means that every
child of the right hand side is tested for equality against the left child of the right hand side is tested for equality against the left
hand side. hand side.
\begin{verbatim} \begin{mathpar}
(equiv S Cs Ci gs)^i \infer
equiv S Cs Cf gs {C_S \in {\Leaf t, \Failure}
----------------------------------------- \\
equiv S Cs (Node(a, (Domi,Ci)^i, Cf)) gs \forall i,\; \EquivTEX {(S \land a \in D_i)} {C_S} {C_i} G
\end{verbatim} \\
\EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
{\EquivTEX S
{C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G}
\end{mathpar}
\begin{comment} \begin{comment}
% TODO: [Gabriel] in practice the $dom_S$ are constructors and the % TODO: [Gabriel] in practice the $dom_S$ are constructors and the
@ -304,12 +328,20 @@ the accessors on both side are equal, and removing the branches that
result in an empty intersection. If the accessors are different, result in an empty intersection. If the accessors are different,
\emph{$dom_T$} is left unchanged. \emph{$dom_T$} is left unchanged.
\begin{verbatim} \begin{mathpar}
equiv S Ci (trim Ct a=Ki) gs \infer
equiv S Cf (trim Ct (a\notin(K_i)^i) gs {\forall i,\;
------------------------------------- \EquivTEX
equiv S (Node(a, (Ki,Ci)^i, Cf) Ct gs {(S \land a = K_i)}
\end{verbatim} {C_i} {\trim {C_T} {a = K_i}} G
\\
\EquivTEX
{(S \land a \notin \Fam i {K_i})}
\Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G
}
{\EquivTEX S
{\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G}
\end{mathpar}
The equivalence checking algorithm deals with guards by storing a The equivalence checking algorithm deals with guards by storing a
queue. A guard blackbox is pushed to the queue whenever the algorithm queue. A guard blackbox is pushed to the queue whenever the algorithm
@ -321,17 +353,21 @@ continues by exploding to two subtrees, one in which the guard
condition evaluates to true, the other when it evaluates to false. condition evaluates to true, the other when it evaluates to false.
Termination of the algorithm is successful only when the guards queue Termination of the algorithm is successful only when the guards queue
is empty. is empty.
\begin{verbatim} \begin{mathpar}
equiv S Ctrue Ct (gs++[condition]) \infer
equiv S Cfalse Ct (gs++[condition]) {\EquivTEX S {C_0} {C_T} {G, (t_S = 0)}
-------------------------------------------- \\
equiv S (Guard condition Ctrue Cfalse) Ct gs \EquivTEX S {C_1} {C_T} {G, (t_S = 1)}}
{\EquivTEX S
{\Guard {t_S} {C_0} {C_1}} {C_T} G}
equiv S Cs Ctrue gs \infer
equiv S Cs Cfalse gs {\trel {t_S} {t_T}
-------------------------------------------- \\
equiv S Cs (Guard condition Ctrue Cfalse) ([condition]++gs) \EquivTEX S {C_S} {C_b} G}
\end{verbatim} {\EquivTEX S
{C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}}
\end{mathpar}
\begin{comment} \begin{comment}
TODO: replace inference rules with good latex TODO: replace inference rules with good latex
@ -678,8 +714,8 @@ bad:
The tree of the execution when the function is evaluated considering The tree of the execution when the function is evaluated considering
/int len/ our symbolic variable α, sa->sa_len as symbolic variable β /int len/ our symbolic variable α, sa->sa_len as symbolic variable β
and π as the set of constraints on a symbolic variable: and π as the set of constraints on a symbolic variable:
[[./files/symb_exec.png]]
#+BEGIN_SRC \begin{comment}
[1] compat (...) { π_{α}: -∞ < α < ∞ } [1] compat (...) { π_{α}: -∞ < α < ∞ }
| |
[2] min (σ₁, σ₂) { π_{σ}: -∞ < (σ₁,σ₂) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...} [2] min (σ₁, σ₂) { π_{σ}: -∞ < (σ₁,σ₂) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...}
@ -687,7 +723,7 @@ and π as the set of constraints on a symbolic variable:
[3] cast(u_int) (...) { π_{σ}: 0 ≤ (σ) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...} [3] cast(u_int) (...) { π_{σ}: 0 ≤ (σ) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...}
| |
... // rest of the execution ... // rest of the execution
#+END_SRC \end{comment}
We can see that at step 3 the set of possible values of the scrutinee We can see that at step 3 the set of possible values of the scrutinee
α is bigger than the set of possible values of the input σ to the α is bigger than the set of possible values of the input σ to the
/cast/ directive, that is: π_{α} ⊈ π_{σ}. For this reason the /cast/ may fail when α is /len/ /cast/ directive, that is: π_{α} ⊈ π_{σ}. For this reason the /cast/ may fail when α is /len/
@ -695,9 +731,9 @@ negative number, outside the domain π_{σ}. In C this would trigger undefined b
overflow) that made the exploitation possible. overflow) that made the exploitation possible.
Every step of evaluation can be modelled as the following transition: Every step of evaluation can be modelled as the following transition:
#+BEGIN_SRC \[
(π_{σ}, (πᵢ)ⁱ) → (π'_{σ}, (π'ᵢ)ⁱ) (π_{σ}, (πᵢ)ⁱ) → (π'_{σ}, (π'ᵢ)ⁱ)
#+END_SRC \]
if we express the π constraints as logical formulas we can model the if we express the π constraints as logical formulas we can model the
execution of the program in terms of Hoare Logic. execution of the program in terms of Hoare Logic.
State of the computation is a Hoare triple {P}C{Q} where P and Q are State of the computation is a Hoare triple {P}C{Q} where P and Q are
@ -706,50 +742,47 @@ constitute the assertions of the program. C is the directive being
executed. executed.
The language of the assertions P is: The language of the assertions P is:
#+BEGIN_SRC #+BEGIN_SRC
P ::= true | false | a < b | P₁ ∧ P₂ | P₁ ∨ P₂ | ~P P ::= true | false | a < b | P_{1} \wedge P_{2} | P_{1} \lor P_{2} | \notP
#+END_SRC #+END_SRC
where a and b are numbers. where a and b are numbers.
In the Hoare rules assertions could also take the form of In the Hoare rules assertions could also take the form of
#+BEGIN_SRC #+BEGIN_SRC
P ::= ∀i. P | ∃i. P | P₁ ⇒ P₂ P ::= \forall i. P | \exists i. P | P_{1} \Rightarrow P_{2}
#+END_SRC #+END_SRC
where i is a logical variable, but assertions of these kinds increases where i is a logical variable, but assertions of these kinds increases
the complexity of the symbolic engine. the complexity of the symbolic engine.
Execution follows the rules of Hoare logic: Execution follows the rules of Hoare logic:
- Empty statement : - Empty statement :
\begin{verbatim} \begin{mathpar}
———————————— \infer{ }
{P}/skip/{P} { \{P\} skip \{P\} }
\end{verbatim} \end{mathpar}
- Assignment statement : The truthness of P[a/x] is equivalent to the - Assignment statement : The truthness of P[a/x] is equivalent to the
truth of {P} after the assignment. truth of {P} after the assignment.
\begin{verbatim} \begin{mathpar}
———————————— \infer{ }
{P[a/x]}x:=a{P} { \{P[a/x]\}x:=a\{P\} }
\end{verbatim} \end{mathpar}
- Composition : c₁ and c₂ are directives that are executed in order; - Composition : c₁ and c₂ are directives that are executed in order;
{Q} is the /midcondition/. {Q} is called the /midcondition/.
\begin{verbatim} \begin{mathpar}
{P}c₁{R}, {R}c₂{Q} \infer { \{P\}c_1\{R\}, \{R\}c_2\{Q\} }
—————————————————— { \{P\}c₁;c₂\{Q\} }
{P}c₁;c₂{Q} \end{mathpar}
\end{verbatim}
- Conditional : - Conditional :
\begin{verbatim} \begin{mathpar}
{P∧b}c₁{Q}, {P∧~b}c₂{Q} \infer { \{P \wedge b \} c_1 \{Q\}, \{P\wedge\not b\}c_2\{Q\} }
———————————————————————— { \{P\}if b then c_1 else c_2\{Q\} }
{P}if b then c₁ else c₂{Q} \end{mathpar}
\end{verbatim}
- Loop : {P} is the loop invariant. After the loop is finished /P/ - Loop : {P} is the loop invariant. After the loop is finished /P/
holds and ~b caused the loop to end. holds and ¬̸b caused the loop to end.
\begin{verbatim} \begin{mathpar}
{P∧b}c{P} \infer { \{P \wedge b \}c\{P\} }
———————————————————————— { \{P\} while b do c \{P \wedge \neg b\} }
{P}while b do c{P∧~b} \end{mathpar}
\end{verbatim}
Even if the semantics of symbolic execution engines are well defined, Even if the semantics of symbolic execution engines are well defined,
the user may run into different complications when applying such the user may run into different complications when applying such
@ -1129,9 +1162,111 @@ following four rules:
apply, and P₂ → L₂ containing the remaining rows. The algorithm is apply, and P₂ → L₂ containing the remaining rows. The algorithm is
applied to both matrices. applied to both matrices.
** Target translation
TODO
** Equivalence checking
The equivalence checking algorithm takes as input a domain of
possible values \emph{S} and a pair of source and target decision trees and
in case the two trees are not equivalent it returns a counter example.
The algorithm respects the following correctness statement:
\begin{comment}
TODO: we have to define what \coversTEX mean for readers to understand the specifications
(or we use a simplifying lie by hiding \coversTEX in the statements).
\end{comment}
\begin{align*}
\EquivTEX S {C_S} {C_T} \emptyqueue = \YesTEX \;\land\; \coversTEX {C_T} S
& \implies
\forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T)
\\
\EquivTEX S {C_S} {C_T} \emptyqueue = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S
& \implies
v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T)
\end{align*}
Our equivalence-checking algorithm $\EquivTEX S {C_S} {C_T} G$ is
a exactly decision procedure for the provability of the judgment
$(\EquivTEX S {C_S} {C_T} G)$, defined below.
\begin{mathpar}
\begin{array}{l@{~}r@{~}l}
& & \text{\emph{constraint trees}} \\
C & \bnfeq & \Leaf t \\
& \bnfor & \Failure \\
& \bnfor & \Switch a {\Fam i {\pi_i, C_i}} \Cfb \\
& \bnfor & \Guard t {C_0} {C_1} \\
\end{array}
\begin{array}{l@{~}r@{~}l}
& & \text{\emph{boolean result}} \\
b & \in & \{ 0, 1 \} \\[0.5em]
& & \text{\emph{guard queues}} \\
G & \bnfeq & (t_1 = b_1), \dots, (t_n = b_n) \\
\end{array}
\begin{array}{l@{~}r@{~}l}
& & \text{\emph{input space}} \\
S & \subseteq & \{ (v_S, v_T) \mid \vrel {v_S} {v_T} \} \\
\end{array}
\\
\infer{ }
{\EquivTEX \emptyset {C_S} {C_T} G}
\infer{ }
{\EquivTEX S \Failure \Failure \emptyqueue}
\infer
{\trel {t_S} {t_T}}
{\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
\infer
{\forall i,\;
\EquivTEX
{(S \land a = K_i)}
{C_i} {\trim {C_T} {a = K_i}} G
\\
\EquivTEX
{(S \land a \notin \Fam i {K_i})}
\Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G
}
{\EquivTEX S
{\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G}
\begin{comment}
% TODO explain somewhere why the judgment is not symmetric:
% we avoid defining trimming on source trees, which would
% require more expressive conditions than just constructors
\end{comment}
\infer
{C_S \in {\Leaf t, \Failure}
\\
\forall i,\; \EquivTEX {(S \land a \in D_i)} {C_S} {C_i} G
\\
\EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
{\EquivTEX S
{C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G}
\infer
{\EquivTEX S {C_0} {C_T} {G, (t_S = 0)}
\\
\EquivTEX S {C_1} {C_T} {G, (t_S = 1)}}
{\EquivTEX S
{\Guard {t_S} {C_0} {C_1}} {C_T} G}
\infer
{\trel {t_S} {t_T}
\\
\EquivTEX S {C_S} {C_b} G}
{\EquivTEX S
{C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}}
\end{mathpar}
* Correctness of the algorithm * Correctness of the algorithm
Running a program tₛ or its translation 〚tₛ〛 against an input vₛ Running a program tₛ or its translation 〚tₛ〛 against an input vₛ
produces as a result a result /r/ in the following way: produces as a result /r/ in the following way:
| ( 〚tₛ〛ₛ(vₛ) = Cₛ(vₛ) ) → r | ( 〚tₛ〛ₛ(vₛ) = Cₛ(vₛ) ) → r
| tₛ(vₛ) → r | tₛ(vₛ) → r
Likewise Likewise
@ -1206,6 +1341,7 @@ and an optional fallback.
Failure is emitted only when the patterns don't cover the whole set of Failure is emitted only when the patterns don't cover the whole set of
possible input values /S/. The fallback is not needed when the user possible input values /S/. The fallback is not needed when the user
doesn't use a wildcard pattern. doesn't use a wildcard pattern.
%%% Give example of thing
| Cₛ ::= Leaf bb | Node(a, (Kᵢ → Cᵢ)^{i∈S} , C?) | Cₛ ::= Leaf bb | Node(a, (Kᵢ → Cᵢ)^{i∈S} , C?)
| a ::= Here | n.a | a ::= Here | n.a
@ -1216,17 +1352,17 @@ Are K and Here clear here?
\end{comment} \end{comment}
We define the decomposition matrix /mₛ/ as We define the decomposition matrix /mₛ/ as
| SMatrix mₛ := (aⱼ)^{j∈J}, ((pᵢⱼ)^{j∈J} → bbᵢ)^{i∈I} | SMatrix mₛ := (aⱼ)^{j∈J}, ((p_{ij})^{j∈J} → bbᵢ)^{i∈I}
\begin{comment} \begin{comment}
Correggi prendendo in considerazione l'accessor Correggi prendendo in considerazione l'accessor
\end{comment} \end{comment}
We define the decision tree of source programs We define the decision tree of source programs
[|tₛ|] 〚tₛ〛
in terms of the decision tree of pattern matrices in terms of the decision tree of pattern matrices
[|mₛ|] 〚mₛ〛
by the following: by the following:
〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛 # i ∈ I 〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛
decision tree computed from pattern matrices respect the following invariant: decision tree computed from pattern matrices respect the following invariant:
| ∀v (vᵢ)^{i∈I} = v(aᵢ)^{i∈I} → 〚m〛(v) = m(vᵢ)^{i∈I} for m = ((aᵢ)^{i∈I}, (rᵢ)^{i∈I}) | ∀v (vᵢ)^{i∈I} = v(aᵢ)^{i∈I} → 〚m〛(v) = m(vᵢ)^{i∈I} for m = ((aᵢ)^{i∈I}, (rᵢ)^{i∈I})
@ -1249,16 +1385,138 @@ Base cases:
2. [| (aⱼ)ʲ, ∅ |] := Failure 2. [| (aⱼ)ʲ, ∅ |] := Failure
Regarding non base cases: Regarding non base cases:
We define Let's first define
| let Idx(k) = [0; arity(k)[ | let Idx(k) := [0; arity(k)[
| let First(∅) = ⊥ | let First(∅) := ⊥
| let First((aⱼ)ʲ) = a_{min(j)} ## where j ∈ J ≠ ∅ | let First((aⱼ)ʲ) := a_{min(j∈J≠∅)}
\[
m := ((a_i)^i ((p_{ij})^i \to e_j)^{ij})
\]
\[
(k_k)^k := headconstructor(p_{i0})^i
\]
\begin{equation}
\begin{align}
Groups(m) := ( k_k \to ((a)_{0.l})^{l \in Idx(k_k)} +++ (a_i)^{i \in I\backslash \{0\} }), \\
( if p_{0j} is k(q_l) then \\
(qₗ)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}} \to e_j \\
if p_{0j} is \_ then \\
(\_)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}} \to e_j \\
else \bot )^j ), \\
((a_i)^{i \in I\backslash \{0\}}, ((p_{ij})^{i \in I\backslash \{0\}} \to eⱼ if p_{0j} is \_ else \bot)^{j \in J})
\end{align}
\end{equation}
Groups(m) is an auxiliary function that decomposes a matrix m into
submatrices, according to the head constructor of their first pattern.
Groups(m) returns one submatrix m_r for each head constructor k that
occurs on the first row of m, plus one "wildcard submatrix" m_{wild}
that matches on all values that do not start with one of those head
constructors.
Intuitively, m is equivalent to its decompositionin the following
sense: if the first pattern of an input vector (v_i)^i starts with one
of the head constructors k, then running (v_i)^i against m is the same
as running it against the submatrix m_k; otherwise (its head
constructor is none of the k) it is equivalent to running it against
the wildcard submatrix.
We formalize this intuition as follows:
Lemma (Groups):
Let \[m\] be a matrix with \[Groups(m) = (k_r \to m_r)^k, m_{wild}\].
For any value vector \[(v_i)^l\] such that \[v_0 = k(v'_l)^l\] for some
constructor k,
we have:
\[
if k = kₖ for some k then
m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)^{i∈I\backslash \{0\}})
else
m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\backslash \{0\}}
\]
*** Proof:
Let \[m\] be a matrix with \[Group(m) = (k_r \to m_r)^k, m_{wild}\].
Let \[(v_i)^i\] be an input matrix with \[v_0 = k(v'_l)^l\] for some k.
We proceed by case analysis:
- either k is one of the kₖ for some k
- or k is none of the (kₖ)ᵏ
Both m(vᵢ)ⁱ and mₖ(vₖ)ᵏ are defined as the first matching result of
a family over each row rⱼ of a matrix
We know, from the definition of
Groups(m), that mₖ is
\[
((a){0.l})^{l∈Idx(kₖ)} +++ (aᵢ)^{i∈I\backslash \{0\}}),
(
if p_{0j} is k(qₗ) then
(qₗ)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}} → eⱼ
if p_{0j} is _ then
(_)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}} → eⱼ
else ⊥
)ʲ
\]
By definition, m(vᵢ)ⁱ is
m(vᵢ)ⁱ = First(rⱼ(vᵢ)ⁱ)ʲ for m = ((aᵢ)ⁱ, (rⱼ)ʲ)
(pᵢ)ⁱ (vᵢ)ⁱ = {
if p₀ = k(qₗ)ˡ, v₀ = k'(v'ₖ)ᵏ, k=Idx(k') and l=Idx(k)
if k ≠ k' then ⊥
if k = k' then ((qₗ)ˡ +++ (pᵢ)^{i∈I\backslash \{0\}}) ((v'ₖ)ᵏ +++ (vᵢ)^{i∈I\backslash \{0\}})
if p₀ = (q₁|q₂) then
First( (q₁pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}}, (q₂pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}} )
}
For this reason, if we can prova that
| ∀j, rⱼ(vᵢ)ⁱ = r'ⱼ((v'ₖ)ᵏ ++ (vᵢ)ⁱ)
it follows that
| m(vᵢ)ⁱ = mₖ((v'ₖ)ᵏ ++ (vᵢ)ⁱ)
from the above definition.
We can also show that aᵢ = a){0.l}ˡ +++ a_{i∈I\backslash \{0\}} because v(a₀) = K(v(a){0.l})ˡ)
** Proof of equivalence checking ** Proof of equivalence checking
\begin{comment}
TODO: put ^i∈I where needed
\end{comment}
\subsubsection{The trimming lemma}
The trimming lemma allows to reduce the size of a decision tree given
an accessor → π relation (In other words???)
| ∀vₜ ∈ (a→π), Cₜ(vₜ) = C_{t/a→π(kᵢ)}(vₜ)
We prove this by induction on Cₜ:
a. Case where Cₜ = Leaf_{bb}:
Leaf_{bb/a→π}(v) = Leaf_{bb}(v)
That means that the result of trimming on a Leaf is
the Leaf itself
b. Same for failure terminal
e. Unreachabe → ⊥
c. When Cₜ = Node(b, (π→Cᵢ)ⁱ)_{/a→π} then
we define πᵢ' = πᵢ if a≠b else πᵢ∩π ;
Node(b, (π→Cᵢ)ⁱ)_{/a→π} := Node(b, (π'ᵢ→C_{i/a→π})ⁱ)
Goal: prove that Cₜ(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ)
Either vₜ∉(b→πᵢ)ⁱ and that means that the node is a Failure node
Or vₜ∈(b→πₖ) for some k, then
C_{k/a→π}(vₜ) = Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ)
because when a ≠ b then πₖ'= πₖ => vₜ∈πₖ'
while when a = b then πₖ'=(πₖ∩π)
- vₜ∈π because of hypothesis
- we already know that vₜ∈πₖ
So vₜ ∈ πₖ' and by induction Cₖ(vₜ) = C_{k/a→π}(vₜ)
and Cₜ(vₜ) = Cₖ(vₜ) when vₜ∈(b→πₖ)
This proves that Node(b, (πᵢ'→C_{i/a→π})ⁱ)(vₜ) = Cₜ(vₜ)
Covering lemma:
∀a,π covers(Cₜ,S) => covers(C_{t/a→π}, (S∩a→π))
Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %%
\begin{comment}
Should I swap π and π'
\end{comment}
\subsubsection Proof of equivalence checking
The equivalence checking algorithm takes as parameters an input space The equivalence checking algorithm takes as parameters an input space
/S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/: /S/, a source decision tree /Cₛ/ and a target decision tree /Cₜ/:
| equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ) | equiv(S, Cₛ, Cₜ) → Yes | No(vₛ, vₜ)
@ -1292,10 +1550,15 @@ TODO: explain:
\end{comment} \end{comment}
We proceed by case analysis: We proceed by case analysis:
1. equiv(∅, Cₛ, Cₜ) := Yes
\begin{comment} \begin{comment}
Devo spiegarlo? I start numbering from zero to leave the numbers as they were on the blackboard, were we skipped some things
I think the unreachable case should go at the end.
\end{comment} \end{comment}
0. in case of unreachable: Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ
1. In the case of an empty input space
| equiv(∅, Cₛ, Cₜ) := Yes
and that is trivial to prove because there is no pair of values (vₛ, vₜ) that could be
tested against the decision trees.
In the other subcases S is always non-empty. In the other subcases S is always non-empty.
2. equiv(S, Failure, Failure) := Yes 2. equiv(S, Failure, Failure) := Yes
the statement holds because of equality between Failure nodes in the statement holds because of equality between Failure nodes in
@ -1318,3 +1581,24 @@ In the other subcases S is always non-empty.
| vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ)
and the result of the algorithm is and the result of the algorithm is
| equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I
4. equiv(S, Node(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) :=
let π' = ⋃π(kᵢ) ∀i in
Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++ equiv(S∩(a→π(kᵢ)), Cₛ, C_{/a̸¬̸π'}))
The statement holds because:
a. Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ = Yes
In the yes case let's reason by case analysis:
i. When k∈(kᵢ)ⁱ
there is a k=kₖ for some k and this means that Cₛ(vₛ) = Cₛᵢ(vₛ)
By induction we know that Cₛᵢ(vₛ) = c_{t/a→πᵢ}(vₜ)
and because of the trimming lemma:
Cₜ(vₜ) = C_{t/a→πᵢ}(vₜ)
Putting all together:
Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) = Cₜ(vₜ)
ii. when k∉(kᵢ)ⁱ ???
b. Forall(...) = No(vₛ, vₜ)
for a minimum k, equiv(Sₖ, Cₛₖ, C_{t/a→πₖ} = No(vₛ, vₜ)
then Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ) and C_{t/a→πₖ}(vₜ) = Cₜ(vt)
=> (Cₛₖ(vₛ) = Cₛ(vₛ)) ≠ Cₜ(vₜ)
# Same for fallback?

BIN
tesi/tesi_unicode.pdf Normal file
View file

Binary file not shown.