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