1 | \section{Compiler architecture} |
---|
2 | \label{sect.compiler.architecture} |
---|
3 | |
---|
4 | \subsection{The typical CerCo workflow} |
---|
5 | |
---|
6 | \begin{figure}[!t] |
---|
7 | \begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l} |
---|
8 | \begin{lstlisting} |
---|
9 | char a[] = {3, 2, 7, 14}; |
---|
10 | char threshold = 4; |
---|
11 | |
---|
12 | int count(char *p, int len) { |
---|
13 | char j; |
---|
14 | int found = 0; |
---|
15 | for (j=0; j < len; j++) { |
---|
16 | if (*p <= threshold) |
---|
17 | found++; |
---|
18 | p++; |
---|
19 | } |
---|
20 | return found; |
---|
21 | } |
---|
22 | |
---|
23 | int main() { |
---|
24 | return count(a,4); |
---|
25 | } |
---|
26 | \end{lstlisting} |
---|
27 | & |
---|
28 | % $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$ |
---|
29 | \begin{tikzpicture}[ |
---|
30 | baseline={([yshift=-.5ex]current bounding box)}, |
---|
31 | element/.style={draw, text width=1.6cm, on chain, text badly centered}, |
---|
32 | >=stealth |
---|
33 | ] |
---|
34 | {[start chain=going below, node distance=.5cm] |
---|
35 | \node [element] (cerco) {CerCo\\compiler}; |
---|
36 | \node [element] (cost) {CerCo\\cost plugin}; |
---|
37 | {[densely dashed] |
---|
38 | \node [element] (ded) {Deductive\\platform}; |
---|
39 | \node [element] (check) {Proof\\checker}; |
---|
40 | } |
---|
41 | } |
---|
42 | \coordinate [left=3.5cm of cerco] (left); |
---|
43 | {[every node/.style={above, text width=3.5cm, text badly centered, |
---|
44 | font=\scriptsize}] |
---|
45 | \draw [<-] ([yshift=-1ex]cerco.north west) coordinate (t) -- |
---|
46 | node {C source} |
---|
47 | (t-|left); |
---|
48 | \draw [->] (cerco) -- (cost); |
---|
49 | \draw [->] ([yshift=1ex]cerco.south west) coordinate (t) -- |
---|
50 | node {C source+\color{red}{cost annotations}} |
---|
51 | (t-|left) coordinate (cerco out); |
---|
52 | \draw [->] ([yshift=1ex]cost.south west) coordinate (t) -- |
---|
53 | node {C source+\color{red}{cost annotations}\\+\color{blue}{synthesized assertions}} |
---|
54 | (t-|left) coordinate (out); |
---|
55 | {[densely dashed] |
---|
56 | \draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) -- |
---|
57 | node {C source+\color{red}{cost annotations}\\+\color{blue}{complexity assertions}} |
---|
58 | (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out); |
---|
59 | \draw [->] ([yshift=1ex]ded.south west) coordinate (t) -- |
---|
60 | node {complexity obligations} |
---|
61 | (t-|left) coordinate (out); |
---|
62 | \draw [<-] ([yshift=-1ex]check.north west) coordinate (t) -- |
---|
63 | node {complexity proof} |
---|
64 | (t-|left) .. controls +(-.5, 0) and +(-.5, 0) .. (out); |
---|
65 | \draw [dash phase=2.5pt] (cerco out) .. controls +(-1, 0) and +(-1, 0) .. |
---|
66 | (ded in); |
---|
67 | }} |
---|
68 | %% user: |
---|
69 | % head |
---|
70 | \draw (current bounding box.west) ++(-.2,.5) |
---|
71 | circle (.2) ++(0,-.2) -- ++(0,-.1) coordinate (t); |
---|
72 | % arms |
---|
73 | \draw (t) -- +(-.3,-.2); |
---|
74 | \draw (t) -- +(.3,-.2); |
---|
75 | % body |
---|
76 | \draw (t) -- ++(0,-.4) coordinate (t); |
---|
77 | % legs |
---|
78 | \draw (t) -- +(-.2,-.6); |
---|
79 | \draw (t) -- +(.2,-.6); |
---|
80 | \end{tikzpicture} |
---|
81 | \end{tabular} |
---|
82 | \caption{On the left: C code to count the number of elements in an array |
---|
83 | that are less than or equal to a given threshold. On the right: CerCo's interaction |
---|
84 | diagram. Components provided by CerCo are drawn with a solid border.} |
---|
85 | \label{test1} |
---|
86 | \end{figure} |
---|
87 | We illustrate the workflow we envisage (on the right |
---|
88 | of~\autoref{test1}) on an example program (on the left |
---|
89 | of~\autoref{test1}). The user writes the program and feeds it to the |
---|
90 | CerCo compiler, which outputs an instrumented version of the same |
---|
91 | program that updates global variables that record the elapsed |
---|
92 | execution time and the stack space usage. The red lines in |
---|
93 | \autoref{itest1} introducing variables, functions and function calls |
---|
94 | starting with \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the |
---|
95 | compiler. For example, the two calls at the start of |
---|
96 | \lstinline'count' say that 4 bytes of stack are required, and that it |
---|
97 | takes 111 cycles to reach the next cost annotation (in the loop body). |
---|
98 | The compiler measures these on the labelled object code that it generates. |
---|
99 | |
---|
100 | The annotated program can then be enriched with complexity |
---|
101 | assertions in the style of Hoare logic, that are passed to a deductive |
---|
102 | platform (in our case Frama-C). We provide as a Frama-C cost plugin a |
---|
103 | simple automatic synthesiser for complexity assertions which can |
---|
104 | be overridden by the user to increase or decrease accuracy. These are the blue |
---|
105 | comments starting with \lstinline'/*@' in \autoref{itest1}, written in |
---|
106 | Frama-C's specification language, ACSL. From the |
---|
107 | assertions, a general purpose deductive platform produces proof |
---|
108 | obligations which in turn can be closed by automatic or interactive |
---|
109 | provers, ending in a proof certificate. |
---|
110 | |
---|
111 | % NB: if you try this example with the live CD you should increase the timeout |
---|
112 | |
---|
113 | Twelve proof obligations are generated from~\autoref{itest1} (to prove |
---|
114 | that the loop invariant holds after one execution if it holds before, |
---|
115 | to prove that the whole program execution takes at most 1358 cycles, and so on). Note that the synthesised time bound for \lstinline'count', |
---|
116 | $178+214*(1+\text{\lstinline'len'})$ cycles, is parametric in the length of |
---|
117 | the array. The CVC3 prover |
---|
118 | closes all obligations within half a minute on routine commodity |
---|
119 | hardware. A simpler non-parametric version can be solved in a few |
---|
120 | seconds. |
---|
121 | % |
---|
122 | \fvset{commandchars=\\\{\}} |
---|
123 | \lstset{morecomment=[s][\color{blue}]{/*@}{*/}, |
---|
124 | moredelim=[is][\color{blue}]{$}{$}, |
---|
125 | moredelim=[is][\color{red}]{|}{|}, |
---|
126 | lineskip=-2pt} |
---|
127 | \begin{figure}[!p] |
---|
128 | \begin{lstlisting} |
---|
129 | |int __cost = 33, __stack = 5, __stack_max = 5;| |
---|
130 | |void __cost_incr(int incr) { __cost += incr; }| |
---|
131 | |void __stack_incr(int incr) { |
---|
132 | __stack += incr; |
---|
133 | __stack_max = __stack_max < __stack ? __stack : __stack_max; |
---|
134 | }| |
---|
135 | |
---|
136 | char a[4] = {3, 2, 7, 14}; char threshold = 4; |
---|
137 | |
---|
138 | /*@ behavior stack_cost: |
---|
139 | ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack)); |
---|
140 | ensures __stack == \old(__stack); |
---|
141 | behavior time_cost: |
---|
142 | ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0)); |
---|
143 | */ |
---|
144 | int count(char *p, int len) { |
---|
145 | char j; int found = 0; |
---|
146 | |__stack_incr(4); __cost_incr(111);| |
---|
147 | $__l: /* internal */$ |
---|
148 | /*@ for time_cost: loop invariant |
---|
149 | __cost <= \at(__cost,__l)+ |
---|
150 | 214*(__max(\at((len-j)+1,__l), 0)-__max(1+(len-j), 0)); |
---|
151 | for stack_cost: loop invariant |
---|
152 | __stack_max == \at(__stack_max,__l); |
---|
153 | for stack_cost: loop invariant |
---|
154 | __stack == \at(__stack,__l); |
---|
155 | loop variant len-j; |
---|
156 | */ |
---|
157 | for (j = 0; j < len; j++) { |
---|
158 | |__cost_incr(78);| |
---|
159 | if (*p <= threshold) { |__cost_incr(136);| found ++; } |
---|
160 | else { |__cost_incr(114);| } |
---|
161 | p ++; |
---|
162 | } |
---|
163 | |__cost_incr(67); __stack_incr(-4);| |
---|
164 | return found; |
---|
165 | } |
---|
166 | |
---|
167 | /*@ behavior stack_cost: |
---|
168 | ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack)); |
---|
169 | ensures __stack == \old(__stack); |
---|
170 | behavior time_cost: |
---|
171 | ensures __cost <= \old(__cost)+1358; |
---|
172 | */ |
---|
173 | int main(void) { |
---|
174 | int t; |
---|
175 | |__stack_incr(2); __cost_incr(110);| |
---|
176 | t = count(a,4); |
---|
177 | |__stack_incr(-2);| |
---|
178 | return t; |
---|
179 | } |
---|
180 | \end{lstlisting} |
---|
181 | \caption{The instrumented version of the program in \autoref{test1}, |
---|
182 | with instrumentation added by the CerCo compiler in red and cost invariants |
---|
183 | added by the CerCo Frama-C plugin in blue. The \lstinline'__cost', |
---|
184 | \lstinline'__stack' and \lstinline'__stack_max' variables hold the elapsed time |
---|
185 | in clock cycles and the current and maximum stack usage. Their initial values |
---|
186 | hold the clock cycles spent in initialising the global data before calling |
---|
187 | \lstinline'main' and the space required by global data (and thus unavailable for |
---|
188 | the stack). |
---|
189 | } |
---|
190 | \label{itest1} |
---|
191 | \end{figure} |
---|