From 63396e1bc246d6e96ef1ac6e8e70bfb6fb55a11f Mon Sep 17 00:00:00 2001
From: John Wickerson <>
Date: Tue, 7 Dec 2021 16:32:22 +0000
Subject: listings

---
 verified_resource_sharing.tex | 135 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 135 insertions(+)

diff --git a/verified_resource_sharing.tex b/verified_resource_sharing.tex
index 861fa21..f28fc2e 100644
--- a/verified_resource_sharing.tex
+++ b/verified_resource_sharing.tex
@@ -4,6 +4,25 @@
 \usepackage{soul}
 \usepackage{subcaption}
 
+\usepackage{listings}
+\lstset{
+basicstyle=\tt,
+escapeinside=@@,
+}
+\setlength{\fboxsep}{1.5pt} % to reduce \colorbox padding when highlighting
+
+%\usepackage{minted}
+%\setminted{
+%fontsize=\small,
+%escapeinside=@@,
+%}
+%\usemintedstyle{manni}
+
+\definecolor{highlight1}{HTML}{b4d6d0} % 8dd3c7
+\definecolor{highlight2}{HTML}{fcfcdc} % ffffb3
+\definecolor{highlight3}{HTML}{c9c7d6} % bebada
+\definecolor{highlight4}{HTML}{fcc1bb} % fb8072
+
 % Leave review comments using
 % \jwcomment{...} (for John) or \yhcomment{...} (for Yann)
 % Using either directly leaves a margin note, using it as,
@@ -80,6 +99,122 @@ In the 3AC language, each function in the program is represented as a numbered l
 
 \section{Rough notes}
 
+Figure~\ref{fig:example_C} shows an example C file.
+
+\begin{figure}
+\begin{lstlisting}
+int add(int a, int b) {
+  @return a + b;@
+}
+
+int main() {
+  @\colorbox{highlight1}{int v = 0;}@
+  @\colorbox{highlight2}{v = add(v, 1);}@
+  @\colorbox{highlight3}{v = add(v, 2);}@
+  @\colorbox{highlight4}{return v;}@
+}
+\end{lstlisting}
+\caption{Example C file}
+\label{fig:example_C}
+\end{figure}
+
+Figure~\ref{fig:example_3AC} shows the 3AC that the CompCert frontend compiles it to. \JW{In the HTL, the parameters to add are called a and b, but in the 3AC they're called x2 and x1. Presumably the HTL should use x2 and x1 too, right?}
+
+\begin{figure}
+\begin{lstlisting}
+add (x2, x1) {
+  @2: x3 = x2 + x1 + 0 (int)@
+  @1: return x3@
+}
+main () {
+  @\colorbox{highlight1}{9: x3 = 0}@
+  @\colorbox{highlight2}{8: x6 = 1}@
+  @\colorbox{highlight2}{7: x1 = "add"(x3, x6)}@
+  @\colorbox{highlight2}{6: x3 = x1}@
+  @\colorbox{highlight3}{5: x5 = 2}@
+  @\colorbox{highlight3}{4: x2 = "add"(x3, x5)}@
+  @\colorbox{highlight3}{3: x3 = x2}@
+  @\colorbox{highlight4}{2: x4 = x3}@
+  @\colorbox{highlight4}{1: return x4}@
+}
+\end{lstlisting}
+\caption{Example 3AC code}
+\label{fig:example_3AC}
+\end{figure}
+
+\begin{figure}
+\begin{lstlisting}[basicstyle=\tt\footnotesize]
+add (a, b) {
+  externctrl {
+    clk -> main.clk
+  }
+  controllogic {
+    2: reg_4 <= 1;
+    1: reg_4 <= 3;
+    3: ;
+  }
+  datapath {
+    2: reg_3 <= {{a + b} + 0};
+    1: finish = 1;
+       return = reg_3;
+    3: finish <= 0;
+  }
+}
+
+main () {
+  externctrl {
+    add_1_a -> add.param_0;
+    add_1_b -> add.param_1;
+    add_1_finish -> add.finish;
+    add_1_rst -> add.rst;
+    add_1_return -> add.return;
+    add_0_a -> add.param_0;
+    add_0_b -> add.param_1;
+    add_0_finish -> add.finish;
+    add_0_rst -> add.rst;
+    add_0_return -> add.return;
+    clk -> main.clk;
+  }
+  controllogic {
+    9: reg_7 <= 8;
+    8: reg_7 <= 7;
+    7: reg_7 <= 12;
+   12: if ({add_0_finish == 1}) reg_7 <= 6;
+    6: reg_7 <= 5;
+    5: reg_7 <= 4;
+    4: reg_7 <= 10;
+   10: if ({add_1_finish == 1}) reg_7 <= 3;
+    3: reg_7 <= 2;
+    2: reg_7 <= 1;
+    1: reg_7 <= 11;
+   11: ;
+  }
+  datapath {
+    9: reg_3 <= 0;
+    8: reg_6 <= 1;
+    7: add_0_rst <= 1;
+       add_0_a <= reg_3;
+       add_0_b <= reg_6;
+   12: add_0_rst <= 0;
+       reg_1 <= add_0_return;
+    6: reg_3 <= reg_1;
+    5: reg_5 <= 2;
+    4: add_1_rst <= 1;
+       add_1_a <= reg_3;
+       add_1_b <= reg_5;
+   10: add_1_rst <= 0;
+       reg_2 <= add_1_return;
+    3: reg_3 <= reg_2;
+    2: reg_4 <= reg_3;
+    1: finish = 1;
+       return = reg_4;
+   11: finish <= 0;
+  }
+}
+\end{lstlisting}
+\caption{Example HTL code}
+\label{fig:example_HTL}
+\end{figure}
 
 
 \begin{figure}
-- 
cgit