1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11(*<*) 12theory Chapter1_MinMax 13imports "AutoCorres.AutoCorres" 14begin 15 16external_file "minmax.c" 17(*>*) 18 19section {* Introduction *} 20 21text {* 22 23 AutoCorres is a tool that attempts to simplify the formal verification of C 24 programs in the Isabelle/HOL theorem prover. It allows C code 25 to be automatically abstracted to produce a higher-level functional 26 specification. 27 28 AutoCorres relies on the C-Parser~\cite{CParser_download} developed by Michael Norrish 29 at NICTA. This tool takes raw C code as input and produces a translation in 30 SIMPL~\cite{Simpl-AFP}, an imperative language written by Norbert Schirmer on top 31 of Isabelle. AutoCorres takes this SIMPL code to produce a "monadic" 32 specification, which is intended to be simpler to reason about in Isabelle. 33 The composition of these two tools (AutoCorres applied after the C-Parser) can 34 then be used to reason about C programs. 35 36 This guide is written for users of Isabelle/HOL, with some knowledge of C, to 37 get started proving properties of C programs. Using AutoCorres in conjunction 38 with the verification condition generator (VCG) \texttt{wp}, one 39 should be able to do this without an understanding of SIMPL nor of the monadic 40 representation produced by AutoCorres. We will see how this is possible in the 41 next chapter. 42 43*} 44 45section {* A First Proof with AutoCorres *} 46 47text {* 48 49 We will now show how to use these tools to prove correctness of some very 50 simple C functions. 51 52*} 53 54subsection {* Two simple functions: \texttt{min} and \texttt{max} *} 55 56text {* 57 58 Consider the following two functions, defined in a file \texttt{minmax.c}, 59 which (we expect) return the minimum and maximum respectively of two unsigned 60 integers. 61 62 \lstinputlisting[language=C, firstline=17]{../../minmax.c} 63 64 It is easy to see that \texttt{min} is correct, but perhaps less obvious why 65 \texttt{max} is correct. AutoCorres will hopefully allow us to prove these 66 claims without too much effort. 67 68*} 69 70subsection {* Invoking the C-parser *} 71 72text {* 73 74 As mentioned earlier, AutoCorres does not handle C code directly. The first 75 step is to apply the 76 C-Parser\footnote{\url{https://ts.data61.csiro.au/software/TS/c-parser}} to 77 obtain a SIMPL translation. We do this using the \texttt{install-C-file} 78 command in Isabelle, as shown. 79 80*} 81 82install_C_file "minmax.c" 83 84(* FIXME: Be consistent with \texttt and \emph *) 85text {* 86 87 For every function in the C source file, the C-Parser generates a 88 corresponding Isabelle definition. These definitions are placed in an Isabelle 89 "locale", whose name matches the input filename. For our file \emph{minmax.c}, 90 the C-Parser will place definitions in the locale \emph{minmax}.\footnote{The 91 C-parser uses locales to avoid having to make certain assumptions about the 92 behaviour of the linker, such as the concrete addresses of symbols in your 93 program.} 94 95 For our purposes, we just have to remember to enter the appropriate locale 96 before writing our proofs. This is done using the \texttt{context} keyword in 97 Isabelle. 98 99 Let's look at the C-Parser's outputs for \texttt{min} and \texttt{max}, which 100 are contained in the theorems \texttt{min\_body\_def} and \texttt{max\_body\_def}. 101 These are simply definitions of the generated names \emph{min\_body} and 102 \emph{max\_body}. We can also see here how our work is wrapped within the 103 \emph{minmax} context. 104 105*} 106 107context minmax begin 108 109 thm min_body_def 110 text {* @{thm [display] min_body_def} *} 111 thm max_body_def 112 text {* @{thm [display] max_body_def} *} 113 114end 115 116text {* 117 118 The definitions above show us the SIMPL generated for each of the 119 functions; we can see that C-parser has translated \texttt{min} and 120 \texttt{max} very literally and no detail of the C language has been 121 omitted. For example: 122 123 \begin{itemize} 124 \item C \texttt{return} statements have been translated into 125 exceptions which are caught at the outside of the 126 function's body; 127 128 \item \emph{Guard} statements are used to ensure that behaviour 129 deemed `undefined' by the C standard does not occur. In the 130 above functions, we see that a guard statement is emitted 131 that ensures that program execution does not hit the end 132 of the function, ensuring that we always return a value 133 (as is required by all non-\texttt{void} functions). 134 135 \item Function parameters are modelled as local variables, which 136 are setup prior to a function being called. Return variables 137 are also modelled as local variables, which are then 138 read by the caller. 139 \end{itemize} 140 141 While a literal translation of C helps to improve confidence that the 142 translation is sound, it does tend to make formal reasoning an arduous 143 task. 144 145*} 146 147subsection {* Invoking AutoCorres *} 148 149text {* 150 151 Now let's use AutoCorres to simplify our functions. This is done using 152 the \texttt{autocorres} command, in a similar manner to the 153 \texttt{install\_C\_file} command: 154 155*} 156 157autocorres "minmax.c" 158 159text {* 160 161 AutoCorres produces a definition in the \texttt{minmax} locale 162 for each function body produced by the C parser. For example, 163 our \texttt{min} function is defined as follows: 164 165*} 166context minmax begin 167thm min'_def 168text {* @{thm [display] min'_def} *} 169 170text {* 171 172 Each function's definition is named identically to its name in 173 C, but with a prime mark (\texttt{'}) appended. For example, 174 our functions \texttt{min} above was named @{term min'}, while 175 the function \texttt{foo\_Bar} would be named @{term foo_Bar'}. 176 177 AutoCorres does not require you to trust its translation is sound, 178 but also emits a \emph{correspondence} or \emph{refinement} proof, 179 as follows: 180 181*} 182 183(* FIXME *) 184(* thm min_autocorres *) 185 186text {* 187 188 Informally, this theorem states that, assuming the abstract function 189 @{term min'} can be proven to not fail for a partciular input, then 190 for the associated input, the concrete C SIMPL program also will not 191 fault, will always terminate, and will have a corresponding end state 192 to the generated abstract program. 193 194 For more technical details, see~\cite{Greenaway_AK_12} and~\cite{Greenaway_LAK_14}. 195 196*} 197 198subsection {* Verifying \texttt{min} *} 199 200text {* 201 202 In the abstracted version of @{term min'}, we can see that AutoCorres 203 has simplified away the local variable reads and writes in the 204 C-parser translation of \texttt{min}, simplified away the exception 205 throwing and handling code, and also simplified away the unreachable 206 guard statement at the end of the function. In fact, @{term min'} has 207 been simplified to the point that it exactly matches Isabelle's 208 built-in function @{term min}: 209 210*} 211thm min_def 212text {* @{thm [display] min_def} *} 213 214text {* 215 So, verifying @{term min'} (and by extension, the C function 216 \texttt{min}) should be easy: 217*} 218lemma min'_is_min: "min' a b = min a b" 219 unfolding min_def min'_def 220 by (rule refl) 221 222subsection {* Verifying \texttt{max} *} 223 224text {* 225 226 Now we also wish to verify that @{term max'} implements the built-in 227 function @{term max}. @{term min'} was nearly too simple to bother 228 verifying, but @{term max'} is a bit more complicated. Let's look at 229 AutoCorres' output for \texttt{max}: 230 231*} 232thm max'_def 233text {* @{thm [display] max'_def} *} 234 235text {* 236 237 At this point, you might still doubt that @{term max'} is indeed 238 correct, so perhaps a proof is in order. The basic idea is that 239 subtracting from \texttt{UINT\_MAX} flips the ordering of unsigned 240 ints. We can then use @{term min'} on the flipped numbers to compute 241 the maximum. 242 243 The next lemma proves that subtracting from \texttt{UINT\_MAX} flips 244 the ordering. To prove it, we convert all words to @{typ int}'s, which 245 does not change the meaning of the statement. 246 247 *} 248 249 lemma n1_minus_flips_ord: 250 "((a :: word32) \<le> b) = ((-1 - a) \<ge> (-1 - b))" 251 apply (subst word_le_def)+ 252 apply (subst word_n1_ge [simplified uint_minus_simple_alt])+ 253 txt {* Now that our statement uses @{typ int}, we can apply Isabelle's built-in \texttt{arith} method. *} 254 apply arith 255 done 256 257text {* 258 And now for the main proof: 259*} 260 lemma max'_is_max: "max' a b = max a b" 261 unfolding max'_def min'_def max_def 262 using n1_minus_flips_ord 263 by force 264 265end 266 267text {* 268 In the next section, we will see how to use AutoCorres to simplify 269 larger, more realistic C programs. 270*} 271 272 273(*<*) 274end 275(*>*) 276