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 Chapter3_HoareHeap 13imports "AutoCorres.AutoCorres" 14begin 15 16external_file "swap.c" 17(*>*) 18 19subsection {* \texttt{swap} *} 20 21text {* 22 23 Here, we use AutoCorres to verify a C program that reads and writes to the heap. 24 Our C function, \texttt{swap}, swaps two words in memory: 25 26\lstinputlisting[language=C, firstline=15]{../../swap.c} 27 28 Again, we translate the program using the C parser and AutoCorres. 29*} 30 31install_C_file "swap.c" 32autocorres [heap_abs_syntax, ts_rules = nondet] "swap.c" 33(*<*) 34context swap begin 35(*>*) 36 37text {* 38 Most heap operations in C programs consist of accessing a pointer. 39 AutoCorres abstracts the global C heap by creating one heap for 40 each type. (In our simple \texttt{swap} example, it creates only 41 a @{typ word32} heap.) This makes verification easier as long as 42 the program does not access the same memory as two different types. 43 44 There are other operations that are relevant to program verification, 45 such as changing the type that occupies a given region of memory. 46 AutoCorres will not abstract any functions that use these operations, 47 so verifying them will be more complicated (but still possible). 48*} 49 50text {* 51 The C parser expresses \texttt{swap} like this: 52*} 53 54thm swap_body_def 55text {* @{thm [display] swap_body_def} *} 56 57text {* 58 AutoCorres abstracts the function to this: 59*} 60 61thm swap'_def 62text {* @{thm [display] swap'_def } *} 63 64text {* 65 There are some things to note: 66 67 The function contains guards (assertions) that the pointers 68 \texttt{a} and \texttt{b} are valid. We need to prove that 69 these guards never fail when verifying \texttt{swap}. 70 Conversely, when verifying any function that calls 71 \texttt{swap}, we need to show that the arguments are 72 valid pointers. 73 74 We saw a monadic program in the previous section, but here 75 the monad is actually being used to carry the program heap. 76*} 77 78(* FIXME: something about heap syntax here. *) 79 80text {* 81 Now we prove that \texttt{swap} is correct. We use @{term x} 82 and @{term y} to ``remember'' the initial values so that we can 83 talk about them in the postcondition. 84*} 85lemma "\<lbrace> \<lambda>s. is_valid_w32 s a \<and> s[a] = x \<and> is_valid_w32 s b \<and> s[b] = y \<rbrace> 86 swap' a b 87 \<lbrace> \<lambda>_ s. s[a] = y \<and> s[b] = x \<rbrace>!" 88 apply (unfold swap'_def) 89 apply wp 90 apply clarsimp 91 txt {* 92 The C parser and AutoCorres both model the C heap using functions, 93 which takes a pointer to some object in memory. Heap updates are 94 modelled using the functional update @{term fun_upd}: 95 96 @{thm [display] fun_upd_def} 97 98 To reason about functional updates, we use the rule fun\_upd\_apply. 99 *} 100 apply (simp add: fun_upd_apply) 101 done 102 103text {* 104 Note that we have ``only'' proved that the function swaps its 105 arguments. We have not proved that it does \emph{not} change 106 any other state. This is a typical \emph{frame problem} with 107 pointer reasoning. We can prove a more complete specification 108 of \texttt{swap}: 109*} 110lemma "(\<And>x y s. P (s[a := x][b := y]) = P s) \<Longrightarrow> 111 \<lbrace> \<lambda>s. is_valid_w32 s a \<and> s[a] = x \<and> is_valid_w32 s b \<and> s[b] = y \<and> P s \<rbrace> 112 swap' a b 113 \<lbrace> \<lambda>_ s. s[a] = y \<and> s[b] = x \<and> P s \<rbrace>!" 114 apply (unfold swap'_def) 115 apply wp 116 apply (clarsimp simp: fun_upd_apply) 117 done 118 119text {* 120 In other words, if predicate @{term P} does not depend on the 121 inputs to \texttt{swap}, it will continue to hold. 122 123 \emph{Separation logic} provides a more structured approach 124 to this problem. 125*} 126 127(*<*) 128end 129end 130(*>*) 131