-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathtutorial.tex
More file actions
6520 lines (5864 loc) · 245 KB
/
tutorial.tex
File metadata and controls
6520 lines (5864 loc) · 245 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass{article}
\usepackage[pdftex]{hyperref}
\usepackage{graphicx}
\usepackage{listings}
\usepackage[T1]{fontenc}
\usepackage{ae,aecompl}
\usepackage[scaled]{luximono}
\usepackage{array}
\usepackage{tikz}
\usepackage{marvosym}
\newcommand{\poison}{\textrm{\Biohazard}}
\DeclareMathAlphabet{\mathsfsl}{OT1}{cmss}{m}{sl}
\usetikzlibrary{arrows,shapes,snakes,automata,backgrounds,petri,positioning}
\tikzstyle{place}=[circle,draw,minimum size=5mm]
% -> Uses trick from http://tex.stackexchange.com/a/170207
\tikzstyle{transitionV}=[rectangle,thick,fill=black,minimum width=5mm,
inner ysep=1pt]
\tikzstyle{transitionH}=[rectangle,thick,fill=black,minimum height=5mm,
inner xsep=1pt]
\tikzstyle{every picture}+=[node distance=0.75cm,>=stealth',auto]
\tikzset{
state/.style={
rectangle,
draw=black
},
}
\addtolength{\hoffset}{-2cm}
\addtolength{\textwidth}{4cm}
\addtolength{\voffset}{-2cm}
\addtolength{\textheight}{3cm}
%\lstset{language=c,columns=fullflexible,basicstyle=\ttfamily,identifierstyle=\itshape} %,literate={&*&}{{$\mathrm{{\&}{*}{\&}}$}}1}
\lstset{language=c,columns=fullflexible,basicstyle=\ttfamily} %,literate={&*&}{{$\mathrm{{\&}{*}{\&}}$}}1}
\lstset{moredelim=**[s][\itshape]{/*}{*/},moredelim=**[l][\itshape]{//},morekeywords={requires,ensures,true,false,predicate,lemma,fixpoint,predicate_ctor,leak,open,close,bool,invariant,inductive,assert,predicate_family,predicate_family_instance}}
\newtheorem{exercise}{Exercise}
\title{The VeriFast Program Verifier: A Tutorial}
\author{Bart Jacobs \and Jan Smans \and Frank Piessens\\
{\small KU Leuven, Department of Computer Science, DistriNet Research Group}}
\begin{document}
\maketitle
\setcounter{tocdepth}{1}
\tableofcontents
\newpage
\section{Introduction}
VeriFast is a program verification tool for verifying certain
correctness properties of single-threaded and multithreaded C\footnote{VeriFast also supports Java. See \emph{VeriFast for Java: A Tutorial}.}
programs. The tool reads a C program consisting of one or more
.c source code files (plus any .h header files referenced from
these .c files) and reports either ``0 errors found'' or
indicates the location of a potential error. If the tool
reports ``0 errors found'', this means\footnote{There are a few
known reasons (known as \emph{unsoundnesses}) why the tool may
sometimes incorrectly report ``0 errors found''; see \textsf{soundness.md} at \textsf{https://github.com/verifast/verifast}. There
may also be unknown unsoundnesses.} that the program
\begin{itemize}
\item does not perform illegal memory accesses, such as reading or
writing a struct instance field after the struct instance has been
freed, or reading or writing beyond the end of an array (known as
a \emph{buffer overflow}, the most common cause of security
vulnerabilities in operating systems and internet services) and
\item does not include a certain type of concurrency errors known as
\emph{data races}, i.e.~unsynchronized conflicting accesses of the
same field by multiple threads. Accesses are considered
conflicting if at least one of them is a write access. And
\item complies with function preconditions and
postconditions specified by the programmer in the form
of special comments (known as \emph{annotations}) in
the source code.
\end{itemize}
Many errors in C programs, such as illegal memory accesses and
data races, are generally very difficult to detect by
conventional means such as testing or code review, since they
are often subtle and typically do not cause a clean crash but
have unpredictable effects that are difficult to diagnose.
However, many security-critical and safety-critical programs,
such as operating systems, device drivers, web servers (that
may serve e-commerce or e-banking applications), embedded
software for automobiles, airplanes, space applications,
nuclear and chemical plants, etc.\ are written in C, where
these programming errors may enable cyber-attacks or cause
injuries. For such programs, formal verification approaches
such as VeriFast may be the most effective way to achieve the
desired level of reliability.
To detect all errors, VeriFast performs \emph{modular symbolic execution}
of the program. In particular, VeriFast symbolically executes the body of
each function of the program, starting from the symbolic state described
by the function's precondition, checking that \emph{permissions} are
present in the symbolic state for each memory location accessed by a
statement, updating the symbolic state to take into account each
statement's effect, and checking, whenever the function returns, that the
final symbolic state satisfies the function's postcondition. A symbolic
state consists of a \emph{symbolic heap}, containing permissions (known as
\emph{chunks}) for accessing certain memory locations, a \emph{symbolic
store}, assigning a symbolic value to each local variable, and a
\emph{path condition}, which is the set of \emph{assumptions} about the
values of the \emph{symbols} used in the symbolic state on the current
execution path. Symbolic execution always terminates, because thanks to
the use of loop invariants each loop body needs to be symbolically
executed only once, and symbolically executing a function call uses only
the function's precondition and postcondition, not its body.
We will now proceed to introduce the tool's features step by
step. To try the examples and exercises in this tutorial
yourself, please download the release from the VeriFast website
at
\begin{center}
\texttt{https://github.com/verifast/verifast}
\end{center}
. You will find in the \texttt{bin} directory a command-line version of
the tool (\texttt{verifast.exe}), and a version that presents a graphical
user interface (\texttt{vfide.exe}).
Throughout this tutorial, you will find exercises that ask you to annotate a small C program so that it is accepted by VeriFast. You can find solutions to all exercises at the end of this tutorial. Furthermore, un-annotated and annotated versions of each solution are included in the VeriFast distribution in directories \verb|tutorial| and \verb|tutorial_solutions|, respectively.
\section{Example: illegal\_access.c}
To illustrate how VeriFast can be used to detect programming
errors that are difficult to spot through testing or code
review, we start by applying the tool to a very simple C
program that contains a subtle error.
Please start \texttt{vfide.exe} with the \texttt{illegal\_access.c}
program that can be downloaded from
\begin{center}
\texttt{https://www.cs.kuleuven.be/\symbol{126}bartj/verifast/illegal\_access.c}
\end{center}
. The program will be shown in the VeriFast IDE. To verify the program,
choose the \textbf{Verify program} command in the \textbf{Verify} menu,
press the \textbf{Play} toolbar button, or press F5. You will see
something like Fig~\ref{figure:illegal-access1}.
\begin{figure}
\begin{center}
\includegraphics[width=10cm]{illegal_access.png}
\end{center}
\caption{A screenshot of \texttt{illegal\_access.c} in the VeriFast IDE}\label{figure:illegal-access1}
\end{figure}
The program attempts to access the field \lstinline|balance| of the struct
instance \lstinline|myAccount| allocated using \lstinline|malloc|. However,
if there is insufficient memory, \lstinline|malloc| returns zero and no
memory is allocated. VeriFast detects the illegal memory access that
happens in this case. Notice the following GUI elements:
\begin{itemize}
\item The erroneous program element is displayed in a red
color with a double underline.
\item The error message states: ``No matching heap chunks: $\mathsf{account\_balance\_(myAccount, \_)}$''. Indeed, in the scenario where there
is insufficient memory, the memory location (or
\emph{heap chunk}) that the program attempts to access
is not accessible to the program.
$\mathsf{account\_balance\_}$ is the type of heap chunk
that represents the (possibly uninitialized) $\mathsf{balance}$ field of the
instance of struct $\mathsf{account}$ pointed to by pointer $\mathsf{myAccount}$.
\item The assignment statement is shown on a yellow
background. This is because the assignment statement is
the \emph{current step}. VeriFast verifies each
function by stepping through it, while keeping track of
a symbolic representation of the relevant program
state. You can inspect the symbolic state at each step
by selecting the step in the Steps pane in the lower
left corner of the VeriFast window. The program element
corresponding to the current step is shown on a yellow
background. The symbolic state consists of the
\emph{path condition}, shown in the Assumptions pane;
the \emph{symbolic heap}, shown in the Heap chunks
pane; and the \emph{symbolic store}, shown in the
Locals pane.
\end{itemize}
To correct the error, uncomment the commented statement. Now
press F5 again. We get a green bar: the program now verifies. This means VeriFast has symbolically executed all possible paths of execution through function \lstinline|main|, and found no errors.
Let's take a closer look at how VeriFast symbolically executed this function. After VeriFast has symbolically executed a program, you can view the \emph{symbolic execution tree} for each function in the Trees pane. The Trees pane is hidden by default, but you can reveal it by dragging the right-hand border of the VeriFast window to the left. At the top of the Trees pane is a drop-down list of all functions that have been symbolically executed. Select the \textsf{Verifying function \lstinline|main|} item to view the symbolic execution tree for function \lstinline|main|.
A symbolic execution tree has four kinds of nodes:
\begin{itemize}
\item The \emph{top node} represents the start of the symbolic execution. Click the top node: in the initial symbolic execution state, there are no heap chunks (the Heap chunks pane is empty), there are no local variables (the Locals pane is empty), and there are no assumptions (the Assumptions pane is empty).
\item There is one \emph{fork node} at each point where a symbolic execution path forks into two paths. This happens when multiple cases need to be considered in the symbolic execution; it is therefore also called a \emph{case split}. The symbolic execution of function \lstinline|main| involves three case splits: the first case split is where symbolic execution of the \lstinline|malloc| call forks into one branch where no memory is available and therefore \lstinline|malloc| returns a null pointer, and another branch where memory is available and therefore \lstinline|malloc| allocates the requested amount of memory and returns a pointer to it. A case split also happens on each of these branches when symbolically executing the \lstinline|if| statement.
\item A black \emph{final node} is shown for the final symbolic execution state on each path where additional symbolic execution steps were performed after the last fork. This is the case for one of the branches of each of the two fork nodes corresponding to the \lstinline|if| statement.
\item There is one green \emph{leaf node} at the end of each complete symbolic execution path through the function. Click the black node preceding any leaf node to see the full corresponding symbolic execution path in the Steps pane.
Function \lstinline|main| has four symbolic execution paths: two paths end when the \lstinline|if| branch is detected to be inconsistent with the preceding \lstinline|malloc| branch; one path where no memory is available ends when the program ends due to the call of \lstinline|abort|; and a fourth path, where memory is available, ends when the function returns.
\end{itemize}
Click the black node preceding the rightmost leaf node to view the (feasible) execution path where \lstinline|malloc| successfully allocates memory. Notice that VeriFast shows arrows in the left margin next to the code of function \lstinline|main| to indicate that this path executes the second case of the \lstinline|malloc| statement and the second case of the \lstinline|if| statement.
To better understand the details of VeriFast's symbolic execution, we will step through this path from the top. Select the first step in the Steps pane. Then, press the Down arrow key. The \textsf{Verifying function \lstinline|main|} step does not affect the symbolic state. The \textsf{Producing assertion} step adds the assumption \textsf{true} to the Assumptions. We will consider production and consumption of assertions in detail later in this tutorial. The first \textsf{Executing statement} step, indicating that we are starting the execution of the function body as a whole, also does nothing. We now arrive at the \textsf{Executing statement} step for the \lstinline|malloc| statement. This statement's effect takes place in the next step, the \textsf{Executing second branch} step; it affects the symbolic state in three ways:
\begin{itemize}
\item It adds the heap chunks $\mathsf{account\_balance\_}(\mathsf{myAccount}, \mathsf{dummy})$ and $\mathsf{malloc\_block\_account}(\mathsf{myAccount})$ to the symbolic heap (as shown in the Heap chunks pane). Here, $\mathsf{myAccount}$ and $\mathsf{dummy}$ are \emph{symbols} that represent unknown values. Specifically, $\mathsf{myAccount}$ represents a pointer to the newly allocated struct instance, and $\mathsf{dummy}$ represents the initial state of the \lstinline|balance| field of the struct instance. (In C, the initial state of the fields of a newly allocated struct instance is unspecified, unlike in Java where the fields of a new object are initialized to the default value of their type. In fact, in C, uninitialized fields might be in a special \emph{poisoned} state whose behavior is different from any initialized state.\footnote{See \url{https://www.ralfj.de/blog/2019/07/14/uninit.html}. We here use the term \emph{poisoned} instead of \emph{uninitialized} to indicate ``a memory state that behaves differently from any initialized state'' because VeriFast allows for the possibility that memory that has not yet been initialized is in fact in a regular state that behaves just like an initialized state.} VeriFast considers reading from poisoned memory to be an error.)
VeriFast \emph{freshly picks} these symbols during this symbolic execution step. That is, to represent the location in memory of the new struct instance and the initial state of the \lstinline|balance| field, VeriFast uses symbols that are not yet being used on this symbolic execution path. To see this, try verifying the function \lstinline|test| shown below:
\begin{lstlisting}
void test()
//@ requires true;
//@ ensures true;
{
{
struct account *myAccount = malloc(sizeof(struct account));
if (myAccount == 0) { abort(); }
}
{
struct account *myAccount = malloc(sizeof(struct account));
if (myAccount == 0) { abort(); }
}
}
\end{lstlisting}
Notice that to symbolically execute the first \lstinline|malloc| statement, VeriFast picked symbols $\mathsf{myAccount}$ and $\mathsf{dummy}$, and to symbolically execute the second \lstinline|malloc| statement, VeriFast picked symbols $\mathsf{myAccount0}$ and $\mathsf{dummy0}$.
\item It adds the assumption $\mathsf{myAccount} \neq 0$ (perhaps written differently) to the path condition (as shown in the Assumptions pane). Indeed, if \lstinline|malloc| succeeds, the returned pointer is not a null pointer.
\item It adds a binding to the symbolic store (shown in the Locals pane) that binds local variable \lstinline|myAccount| to symbolic value $\mathsf{myAccount}$. Indeed, the program assigns the result of the \lstinline|malloc| call (represented by the symbol $\mathsf{myAccount}$) to the local variable \lstinline|myAccount|. Note that the fact that in this case the local variable and the symbol have the same name is incidental and has no special significance.
\end{itemize}
\begin{figure}
\begin{center}
\begin{tabular}{c @{} l}
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:}\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:}\\
\textbf{Locals:}
\end{tabular}}}\\
\rule{0pt}{4ex}$\quad\quad\vcenter{\hbox{\includegraphics[width=1em]{branch-left.pdf}}}\quad\quad$ & \lstinline|struct account *myAccount = malloc(sizeof(struct account));|\\[2ex]
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$\\
\textbf{Assumptions:} & $\mathsf{myAccount} = 0$\\
\textbf{Heap chunks:}\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}
\end{tabular}
\end{center}
\caption{Symbolic execution of a \lstinline|malloc| statement (first case)}\label{fig:symexec-malloc-case1}
\end{figure}
\begin{figure}
\begin{center}
\begin{tabular}{c @{} l}
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:}\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:}\\
\textbf{Locals:}
\end{tabular}}}\\
\rule{0pt}{4ex}$\quad\quad\vcenter{\hbox{\reflectbox{\includegraphics[width=1em]{branch-left.pdf}}}}\quad\quad$ & \lstinline|struct account *myAccount = malloc(sizeof(struct account));|\\[2ex]
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$, $\mathsf{dummy}$\\
\textbf{Assumptions:} & $\mathsf{myAccount} \neq 0$\\
\textbf{Heap chunks:} & $\mathsf{account\_balance\_}(\mathsf{myAccount}, \mathsf{dummy})$, $\mathsf{malloc\_block\_account}(\mathsf{myAccount})$\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}
\end{tabular}
\end{center}
\caption{Symbolic execution of a \lstinline|malloc| statement (second case)}\label{fig:symexec-malloc-case2}
\end{figure}
Figure~\ref{fig:symexec-malloc-case2} summarizes the symbolic execution of \lstinline|malloc| statements, in the successful case. Figure~\ref{fig:symexec-malloc-case1} summarizes the unsuccessful case.
The next step in the symbolic execution trace is the symbolic execution of the \lstinline|if| statement. An \lstinline|if| statement is like a \lstinline|malloc| statement in the sense that there are two cases to consider; therefore, for \lstinline|if| statements, too, VeriFast performs a case split and forks the symbolic execution path into two branches. On the first branch, VeriFast considers the case where the condition of the \lstinline|if| statement is true. It adds the assumption that this is the case to the path condition and symbolically executes the \emph{then} block of the \lstinline|if| statement. On the second branch, VeriFast considers the case where the condition of the \lstinline|if| statement is false. It adds the corresponding assumption to the path condition and symbolically executes the \emph{else} block, if any. Note that after adding an assumption to the path condition, VeriFast always checks if it can detect an inconsistency in the resulting path condition; if so, the current symbolic execution path does not correspond to any real execution path, so there is no point in continuing the symbolic execution of this path and VeriFast abandons it. This is what happens with the first branch of the \lstinline|if| statement after a successful \lstinline|malloc|; it is also what happens with the second branch of the \lstinline|if| statement after an unsuccessful \lstinline|malloc|.
\begin{figure}
\begin{center}
\begin{tabular}{c @{} l}
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:}\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}\\
\rule{0pt}{4ex}$\quad\quad\vcenter{\hbox{\includegraphics[width=1em]{branch-left.pdf}}}\quad\quad$ & \lstinline|if (myAccount == 0)|\\[2ex]
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$\\
\textbf{Assumptions:} & $\mathsf{myAccount} = 0$\\
\textbf{Heap chunks:}\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}
\end{tabular}
\end{center}
\caption{Symbolic execution of an \lstinline|if| statement (first case). Symbolic execution continues with the \emph{then} block of the \lstinline|if| statement.}\label{fig:symexec-if-case1}
\end{figure}
\begin{figure}
\begin{center}
\begin{tabular}{c @{} l}
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:}\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}\\
\rule{0pt}{4ex}$\quad\quad\vcenter{\hbox{\reflectbox{\includegraphics[width=1em]{branch-left.pdf}}}}\quad\quad$ & \lstinline|if (myAccount == 0)|\\[2ex]
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$\\
\textbf{Assumptions:} & $\mathsf{myAccount} \neq 0$\\
\textbf{Heap chunks:}\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}
\end{tabular}
\end{center}
\caption{Symbolic execution of an \lstinline|if| statement (second case). Symbolic execution continues with the \emph{else} block of the \lstinline|if| statement, if any.}\label{fig:symexec-if-case2}
\end{figure}
Figures~\ref{fig:symexec-if-case1} and \ref{fig:symexec-if-case2} summarize the two cases of the symbolic execution of an \lstinline|if| statement.
The next step of the symbolic execution path symbolically executes the statement that assigns value 5 to the \lstinline|balance| field of the newly allocated struct instance. When symbolically executing an assignment to a field of a struct instance, VeriFast first checks that a (possibly uninitialized) heap chunk for that field of that struct instance is present in the symbolic heap. If not, it reports a ``No such heap chunk'' verification failure. It might mean that the program is trying to access unallocated memory. If the chunk is present, VeriFast replaces the chunk with a (definitely initialized) chunk whose value is the value of the right-hand side of the assignment. This is shown in Figure~\ref{fig:symexec-field-update}. Notice that for any type of chunk named $n$ (such as $\mathsf{account\_balance}$) that represents definitely initialized memory, there is a corresponding type of chunk named $n\mathsf{\_}$ (such as $\mathsf{account\_balance\_}$) that represents possibly uninitialized memory.
\begin{figure}
\begin{center}
\begin{tabular}{c @{} l}
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$, $\mathsf{dummy}$\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:} & $\mathsf{account\_balance\_}(\mathsf{myAccount}, \mathsf{dummy})$\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}\\
\rule{0pt}{4ex}$\quad\quad\vcenter{\hbox{\includegraphics[width=.5em]{step.pdf}}}\quad\quad$ & \lstinline|myAccount->balance = 5;|\\[2ex]
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$, $\mathsf{dummy}$\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:} & $\mathsf{account\_balance}(\mathsf{myAccount}, 5)$\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}
\end{tabular}
\end{center}
\caption{Symbolic execution of a struct field assignment statement}\label{fig:symexec-field-update}
\end{figure}
Finally, symbolic execution of the \lstinline|free| statement checks that the two heap chunks that were added by the \lstinline|malloc| statement (the chunk for the \lstinline|balance| field and the malloc block chunk) are still present in the symbolic heap. If not, VeriFast reports a verification failure; the program might be trying to free a struct instance that has already been freed. Otherwise, it removes the chunks, as shown in Figure~\ref{fig:symexec-free}. This ensures that if a program frees a struct instance and then attempts to access that struct instance's fields, symbolic execution of the statements accessing the fields will fail (because the heap chunks for the fields will be missing).
\begin{figure}
\begin{center}
\begin{tabular}{c @{} l}
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:} & $\mathsf{account\_balance}(\mathsf{myAccount}, 5)$, $\mathsf{malloc\_block\_account}(\mathsf{myAccount})$\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}\\
\rule{0pt}{4ex}$\quad\quad\vcenter{\hbox{\includegraphics[width=.5em]{step.pdf}}}\quad\quad$ & \lstinline|free(myAccount);|\\[2ex]
\multicolumn{2}{l}{\fbox{\begin{tabular}{l l}
\textbf{Symbols:} & $\mathsf{myAccount}$\\
\textbf{Assumptions:}\\
\textbf{Heap chunks:}\\
\textbf{Locals:} & \lstinline|myAccount| $\mapsto$ $\mathsf{myAccount}$
\end{tabular}}}
\end{tabular}
\end{center}
\caption{Symbolic execution of a \lstinline|free| statement}\label{fig:symexec-free}
\end{figure}
A program's \emph{symbolic execution forest} (consisting of one symbolic execution tree for each of the program's functions) constitutes a finite description of the program's (usually infinite-depth and infinite-width) \emph{concrete execution tree}, consisting of the program's \emph{concrete execution paths}.
\begin{figure}
\begin{center}
\begin{tikzpicture}
\node [state] (s1) {\begin{tabular}{l l}
\textbf{Chunks:}\\
\textbf{Locals:}\\
\end{tabular}};
\node [transitionV] (t1) [below=of s1, label=right:\parbox{10cm}{\lstinline|struct acc *a = malloc(sizeof(struct acc));|}] {}
edge [pre] (s1);
\node [state] (s22) [below=of t1] {\begin{tabular}{l @{\ } l}
\textbf{C:} & $\mathsf{acc\_bal\_}(4_{\#1}, \poison)$, $\mathsf{mb\_acc}(4_{\#1})$\\
\textbf{L:} & \lstinline|a| $\mapsto$ $4_{\#1}$
\end{tabular}}
edge [pre] (t1);
\node [state] (s23) [right=of s22] {\begin{tabular}{l @{\ } l}
\textbf{C:} & $\mathsf{acc\_bal\_}(8_{\#1}, 42)$, $\mathsf{mb\_acc}(8_{\#1})$\\
\textbf{L:} & \lstinline|a| $\mapsto$ $8_{\#1}$
\end{tabular}}
edge [pre] (t1);
\node (s24) [right=of s23] {$\cdots$};
\node [state] (s21) [left=of s22] {\begin{tabular}{l @{\ } l}
\textbf{C:}\\
\textbf{L:} & \lstinline|a| $\mapsto$ $0_{\#0}$
\end{tabular}}
edge [pre] (t1);
\node [transitionV] (t21) [below=of s21, label=right:\parbox{5cm}{\lstinline|if (a == 0)|}] {}
edge [pre] (s21);
\node [state] (s31) [below=of t21] {\begin{tabular}{l @{\ } l}
\textbf{C:}\\
\textbf{L:} & \lstinline|a| $\mapsto$ $0_{\#0}$
\end{tabular}}
edge [pre] (t21);
\node [transitionV] (t31) [below=of s31, label=right:\parbox{5cm}{\lstinline|abort();|}] {}
edge [pre] (s31);
\node [transitionV] (t22) [below=of s22, label=right:\parbox{5cm}{\lstinline|if (a == 0) \{ ... \}|}] {}
edge [pre] (s22);
\node [state] (s32) [below=of t22] {\begin{tabular}{l @{\ } l}
\textbf{C:} & $\mathsf{acc\_bal\_}(4_{\#1}, \poison)$, $\mathsf{mb\_acc}(4_{\#1})$\\
\textbf{L:} & \lstinline|a| $\mapsto$ $4_{\#1}$
\end{tabular}}
edge [pre] (t22);
\node [transitionV] (t32) [below=of s32, label=right:\parbox{5cm}{\lstinline|a->bal = 5;|}] {}
edge [pre] (s32);
\node [state] (s42) [below=of t32] {\begin{tabular}{l @{\ } l}
\textbf{C:} & $\mathsf{acc\_bal}(4_{\#1}, 5)$, $\mathsf{mb\_acc}(4_{\#1})$\\
\textbf{L:} & \lstinline|a| $\mapsto$ $4_{\#1}$
\end{tabular}}
edge [pre] (t32);
\node [transitionV] (t42) [below=of s42, label=right:\parbox{5cm}{\lstinline|free(a);|}] {}
edge [pre] (s42);
\node [state] (s52) [below=of t42] {\begin{tabular}{l @{\ } l}
\textbf{C:}\\
\textbf{L:} & \lstinline|a| $\mapsto$ $4_{\#1}$
\end{tabular}}
edge [pre] (t42);
\node [transitionV] (t52) [below=of s52, label=right:\parbox{5cm}{\lstinline|return 0;|}] {}
edge [pre] (s52);
\node [state] (s62) [below=of t52] {\begin{tabular}{l @{\ } l}
\textbf{C:}\\
\textbf{L:} & \lstinline|result| $\mapsto$ 0
\end{tabular}}
edge [pre] (t52);
\node [transitionV] (t23) [below=of s23, label=right:\parbox{5cm}{\lstinline|if (a == 0) \{ ... \}|}] {}
edge [pre] (s23);
\node [state] (s33) [below=of t23] {\begin{tabular}{l @{\ } l}
\textbf{C:} & $\mathsf{acc\_bal\_}(8_{\#1}, 42)$, $\mathsf{mb\_acc}(8_{\#1})$\\
\textbf{L:} & \lstinline|a| $\mapsto$ $8_{\#1}$
\end{tabular}}
edge [pre] (t23);
\node [transitionV] (t33) [below=of s33, label=right:\parbox{5cm}{\lstinline|a->bal = 5;|}] {}
edge [pre] (s33);
\node [state] (s43) [below=of t33] {\begin{tabular}{l @{\ } l}
\textbf{C:} & $\mathsf{acc\_bal}(8_{\#1}, 5)$, $\mathsf{mb\_acc}(8_{\#1})$\\
\textbf{L:} & \lstinline|a| $\mapsto$ $8_{\#1}$
\end{tabular}}
edge [pre] (t33);
\node [transitionV] (t43) [below=of s43, label=right:\parbox{5cm}{\lstinline|free(a);|}] {}
edge [pre] (s43);
\node [state] (s53) [below=of t43] {\begin{tabular}{l @{\ } l}
\textbf{C:}\\
\textbf{L:} & \lstinline|a| $\mapsto$ $8_{\#1}$
\end{tabular}}
edge [pre] (t43);
\node [transitionV] (t53) [below=of s53, label=right:\parbox{5cm}{\lstinline|return 0;|}] {}
edge [pre] (s53);
\node [state] (s63) [below=of t53] {\begin{tabular}{l @{\ } l}
\textbf{C:}\\
\textbf{L:} & \lstinline|result| $\mapsto$ 0
\end{tabular}}
edge [pre] (t53);
\end{tikzpicture}
\end{center}
\caption{Concrete execution tree of the program of Figure~\ref{figure:illegal-access1} (after uncommenting the \lstinline|if| statement). We abbreviate \textbf{Chunks} as \textbf{C}, \textbf{Locals} as \textbf{L}, \lstinline|account| as \lstinline|acc|, \lstinline|balance| as \lstinline|bal|, \lstinline|myAccount| as \lstinline|a|, and $\mathsf{malloc\_block}$ as $\mathsf{mb}$. Note that the tree is not shown fully: the \lstinline|malloc| node has one child node for each combination $(\ell, s)$ of a memory location $\ell$ for the new account and an initial state $s$ of its \lstinline|balance| field. Note that in C, a pointer/memory location $\ell = a_p$ consists of an \emph{address} $a$ and a \emph{provenance} $p$; see \url{https://www.ralfj.de/blog/2018/07/24/pointers-and-bytes.html}. The null pointer has address 0 and special provenance $\#0$. Pointers to allocated memory blocks have as their provenance the allocation identifier ($\#1$ is the provenance of the first block allocated by the program) and have a nondeterministically selected address; the diagram shows 4 and 8 as examples of such addresses for conciseness (although in reality pointers returned by \lstinline|malloc| are properly aligned for any type, so they should be multiples of 8 at the very least). (Note: the provenance model suggested here is just an example; in reality, VeriFast abstracts over the precise provenance model, and in fact, by specifying \lstinline|-assume_no_provenance| on the command line, you can make VeriFast assume (unsoundly!) that all pointers have the same provenance $\#0$.) The initial state $s$ of a memory location can be the poisoned state ($\poison$) or some value, e.g. 42.}\label{fig:concrete-execution-tree}
\end{figure}
The concrete execution tree of the corrected version of the program of Figure~\ref{figure:illegal-access1} is shown in Figure~\ref{fig:concrete-execution-tree}. Notice that it is in fact (practically) infinite-width. For this example program, the concrete execution tree is not infinite-depth, because the program has no loops or recursion. If the program had a loop with an unbounded number of iterations, the tree would have been infinite-depth as well.
\begin{exercise}\label{exercise:symex-tree}
Draw the symbolic execution tree of the \lstinline|main| function of the corrected version of the program of Figure~\ref{figure:illegal-access1}. A symbolic execution tree differs from a concrete execution tree in that each state includes a set of used \emph{symbols} and a set of \emph{assumptions} about these symbols, and in that the heap chunks and the local variable bindings are expressed using these symbols. Furthermore, by using these symbols, a single path in a symbolic execution tree can be used to describe infinitely many corresponding paths in the corresponding concrete execution tree.
\end{exercise}
\section{malloc\_block Chunks}\label{section:malloc_block}
To better understand why the $\mathit{malloc}$ statement
generates both an $\mathsf{account\_balance\_}$ chunk and a
$\mathsf{malloc\_}$\-$\mathsf{block\_account}$ chunk, change
the program so that the struct instance is allocated as a local
variable on the stack instead of being allocated on the heap:
\begin{lstlisting}
int main()
//@ requires true;
//@ ensures true;
{
struct account myAccountLocal;
struct account *myAccount = &myAccountLocal;
myAccount->balance = 5;
free(myAccount);
return 0;
}
\end{lstlisting}
This program first allocates an instance of struct
$\mathsf{account}$ on the stack and calls it
$\mathsf{myAccountLocal}$. It then assigns the address of this
struct instance to pointer variable $\mathsf{myAccount}$. The
remainder of the program is as before: the program initializes
the $\mathsf{balance}$ field to value 5 and then attempts to
free the struct instance.
If we ask VeriFast to verify this program, VeriFast reports the
error $$\textsf{No matching heap chunks:
malloc\_block\_account(myAccountLocal\_addr)}$$ at the
$\mathit{free}$ statement. Indeed, the call of $\mathit{free}$ is incorrect,
since $\mathit{free}$ may only be applied to a struct instance
allocated on the heap by $\mathsf{malloc}$, not to a struct
instance allocated on the stack as a local variable.
VeriFast detects this error as follows: 1) VeriFast generates a
$\mathsf{malloc\_block}$ chunk only for struct instances
allocated using $\mathit{malloc}$, not for struct instances
allocated on the stack. 2) When verifying a $\mathit{free}$
statement, VeriFast checks that a $\mathsf{malloc\_block}$
chunk exists for the struct instance being freed.
Notice that, in contrast, the $\mathsf{account\_balance\_}$ chunk
is generated in both cases. As a result, the statement that
initializes the $\mathsf{balance}$ field verifies successfully,
regardless of whether the struct instance was allocated on the
heap or on the stack.
\section{Functions and Contracts}\label{section:functions}
We continue to play with the example of the previous section.
The example currently consists of only one function: the main
function. Let's add another function. Write a function
$\mathsf{account\_set\_balance}$ that takes the address of an
$\mathsf{account}$ struct instance and a integer amount, and
assigns this amount to the struct instance's $\mathsf{balance}$
field. Then replace the field assignment in the main function
with a call to this function. We now have the following
program:
\begin{lstlisting}
#include "stdlib.h"
struct account {
int balance;
};
void account_set_balance(struct account *myAccount, int newBalance)
{
myAccount->balance = newBalance;
}
int main()
//@ requires true;
//@ ensures true;
{
struct account *myAccount = malloc(sizeof(struct account));
if (myAccount == 0) { abort(); }
account_set_balance(myAccount, 5);
free(myAccount);
return 0;
}
\end{lstlisting}
If we try to verify the new program, VeriFast complains that
the new function has no contract. Indeed, VeriFast verifies
each function separately, so it needs a precondition and a
postcondition for each function to describe the initial and
final state of calls of the function.
Add the same contract that the main function has:
\begin{lstlisting}
void account_set_balance(struct account *myAccount, int newBalance)
//@ requires true;
//@ ensures true;
\end{lstlisting}
Notice that contracts, like all VeriFast annotations, are in
comments, so that the C compiler ignores them. VeriFast also
ignores comments, except the ones that are marked with an at
(\verb|@|) sign.
VeriFast now no longer complains about missing contracts.
However, it now complains that the field assignment in the body
of $\mathsf{account\_set\_balance}$ cannot be verified because
the symbolic heap does not contain a heap chunk that grants
permission to access this field. To fix this, we need to
specify in the function's precondition that the function
requires permission to access the $\mathsf{balance}$ field of
the $\mathsf{account}$ struct instance at address
$\mathsf{myAccount}$. We achieve this simply by mentioning the
heap chunk in the precondition:
\begin{lstlisting}
void account_set_balance(struct account *myAccount, int newBalance)
//@ requires account_balance_(myAccount, _);
//@ ensures true;
\end{lstlisting}
Notice that we use an underscore in the position where the
state of the field belongs. This indicates that we do not care
about the old state of the field when the function is
called.\footnote{VeriFast also supports a more concise syntax
for field chunks. For example,
\lstinline!account_balance_(myAccount, _)! can also be written as
\lstinline!myAccount->balance |-> _!.
In fact, the latter (field chunk-specific) syntax is generally recommended
over the former (generic chunk) syntax because it causes
VeriFast to take into account the field chunk-specific information that there is at most one
chunk for a given field, and that the field's value is within the limits of
its type. However, for didactical reasons, in this tutorial we initially use the generic
chunk syntax so that the chunks written in the annotations and the heap chunks shown in the VeriFast IDE look the same.}
VeriFast now highlights the brace that closes the body of the
function. This means we successfully verified the field
assignment. However, VeriFast now complains that the function
leaks heap chunks. For now, let's simply work around this error
message by inserting a $\mathbf{leak}$ command, which indicates
that we're happy to leak this heap chunk. We will come back to
this later.
\begin{lstlisting}
void account_set_balance(struct account *myAccount, int newBalance)
//@ requires account_balance_(myAccount, _);
//@ ensures true;
{
myAccount->balance = newBalance;
//@ leak account_balance(myAccount, _);
}
\end{lstlisting}
Function $\mathsf{account\_set\_balance}$ now verifies, and
VeriFast attempts to verify function $\mathsf{main}$. It
complains that it cannot free the $\mathsf{account}$ struct
instance because it does not have permission to access the
$\mathsf{balance}$ field. Indeed, the symbolic heap contains
the $\mathsf{malloc\_block\_account}$ chunk but not the
$\mathsf{account\_balance}$ chunk. What happened to it? Let's
find out by stepping through the symbolic execution path.
Select the second step. The $\mathsf{malloc}$ statement is about
to be executed and the symbolic heap is empty. Select the next
step. The $\mathsf{malloc}$ statement has added the
$\mathsf{account\_balance\_}$ chunk and the
$\mathsf{malloc\_block\_account}$ chunk.
The if statement has no effect.
We then arrive at the call of $\mathsf{account\_set\_balance}$.
You will notice that this execution step has two sub-steps,
labeled ``Consuming assertion'' and ``Producing assertion''.
The verification of a function call consists of
\emph{consuming} the function's precondition and then
\emph{producing} the function's postcondition. The precondition
and the postcondition are \emph{assertions}, i.e., expressions
that may include heap chunks in addition to ordinary logic.
Consuming the precondition means passing the heap chunks
required by the function to the function, thus removing them
from the symbolic heap. Producing the postcondition means
receiving the heap chunks offered by the function when it
returns, thus adding them to the symbolic heap.
\begin{figure}
\begin{center}
\includegraphics[width=10cm]{illegal_access3.png}
\end{center}
\caption{When stepping through a function call, VeriFast shows both the call site (in green, in the lower pane) and the callee's contract (in yellow, in the upper pane).}\label{figure:call}
\end{figure}
Selecting the ``Consuming assertion'' step changes the layout
of the VeriFast window (see Figure~\ref{figure:call}).
The source code pane is split into two
parts. The upper part is used to display the contract of the
function being called, while the lower part is used to display
the function being verified. (Since in this example the
function being called is so close to the function being
verified, it is likely to be shown in the lower part as well.)
The call being verified is shown on a green background. The
part of the contract being consumed or produced is shown on a
yellow background. If you move from the ``Consuming assertion''
step to the ``Producing assertion'' step, you notice that the
``Consuming assertion'' step removes the
$\mathsf{account\_balance\_}$ chunk from the symbolic heap.
Conceptually, it is now in use by the
$\mathsf{account\_set\_balance}$ function while the
$\mathsf{main}$ function waits for this function to return.
Since function $\mathsf{account\_set\_balance}$'s postcondition
does not mention any heap chunks, the ``Producing assertion''
step does not add anything to the symbolic heap.
It is now clear why VeriFast complained that
$\mathsf{account\_set\_balance}$ leaked heap chunks: since the
function did not return the $\mathsf{account\_balance}$ chunk
to its caller, the chunk was lost and the field could never be
accessed again. VeriFast considers this an error since it is
usually not the intention of the programmer; furthermore, if
too many memory locations are leaked, the program will run out
of memory.
It is now also clear how to fix the error: we must specify in
the postcondition of function $\mathsf{account\_set\_balance}$
that the function must hand back the
$\mathsf{account\_balance}$ chunk to its caller.
\begin{lstlisting}
void account_set_balance(struct account *myAccount, int newBalance)
//@ requires account_balance_(myAccount, _);
//@ ensures account_balance(myAccount, newBalance);
{
myAccount->balance = newBalance;
}
\end{lstlisting}
This
eliminates the leak error message and the error at the
$\mathit{free}$ statement. The program now verifies. Notice
that we refer to the $\mathsf{newBalance}$ parameter in the
position where the value of the field belongs; this means that
the value of the field when the function returns must be equal
to the value of the parameter.
\begin{exercise}\label{exercise:account}
Now factor out the creation and the disposal of the
$\mathsf{account}$ struct instance into separate functions as
well. The creation function should initialize the balance to
zero. Note: if you need to mention multiple heap chunks in an
assertion, separate them using the \emph{separating conjunction}
\lstinline!&*&! (ampersand-star-ampersand). Also, you can refer
to a function's return value in its postcondition by the name
\lstinline!result!.
\end{exercise}
\section{Patterns}
Now, let's add a function that returns the current balance, and
let's test it in the main function. Here's our first attempt:
\begin{lstlisting}
int account_get_balance(struct account *myAccount)
//@ requires account_balance(myAccount, _);
//@ ensures account_balance(myAccount, _);
{
return myAccount->balance;
}
int main()
//@ requires true;
//@ ensures true;
{
struct account *myAccount = create_account();
account_set_balance(myAccount, 5);
int b = account_get_balance(myAccount);
assert(b == 5);
account_dispose(myAccount);
return 0;
}
\end{lstlisting}
The new function verifies successfully, but VeriFast complains
that it cannot prove the condition \lstinline!b == 5!. When
VeriFast is asked to check a condition, it first translates the
condition to a logical formula, by replacing each variable by
its symbolic value. We can see in the symbolic store, displayed
in the Locals pane, that the symbolic value of variable
\lstinline|b| is the logical symbol $\mathsf{b}$. Therefore, the
resulting logical formula is $\mathsf{b} = 5$. VeriFast then
attempts to derive this formula from the \emph{path condition},
i.e., the formulae shown in the Assumptions pane. Since the
only assumption in this case is $\mathsf{true}$, VeriFast
cannot prove the condition.
The problem is that the postcondition of function
$\mathsf{account\_get\_balance}$ does not specify the
function's return value. It does not state that the return
value is equal to the value of the $\mathsf{balance}$ field
when the function is called. To fix this, we need to be able to
assign a name to the value of the balance field when the
function is called. We can do so by replacing the underscore in
the precondition by the \emph{pattern} \lstinline!?theBalance!.
This causes the name \lstinline!theBalance! to be bound to the
value of the $\mathsf{balance}$ field. We can then use this
name in the postcondition to specify the return value using an
equality condition. A function's return value is available in
the function's postcondition under the name \lstinline!result!.
Logical conditions and heap chunks in an assertion must be
separated using the separating conjunction \lstinline!&*&!.
\begin{lstlisting}
int account_get_balance(struct account *myAccount)
//@ requires account_balance(myAccount, ?theBalance);
//@ ensures account_balance(myAccount, theBalance) &*& result == theBalance;
{
return myAccount->balance;
}
\end{lstlisting}
Notice that we use the \lstinline!theBalance! name also to
specify that the function does not modify the value of the
$\mathsf{balance}$ field, by using the name again in the field
value position in the postcondition.
The program now verifies. Indeed, if we use the \textbf{Run to
cursor} command to run to the $\mathit{assert}$ statement, we
see that the assumption \lstinline!(= b 5)! has appeared in the
Assumptions pane. If we step up, we see that it was added when
the equality condition in function
$\mathsf{account\_get\_balance}$'s postcondition was produced.
If we step up further, we see that the variable
\lstinline!theBalance! was added to the upper Locals pane when
the field chunk assertion was consumed, and bound to value 5.
It was bound to value 5 because that was the value found in the
symbolic heap. When verifying a function call, the upper Locals
pane is used to evaluate the contract of the function being
called. It initially contains the bindings of the function's
parameters to the arguments specified in the call; additional
bindings appear as patterns are encountered in the contract.
The assumption \lstinline!(= b 5)! is the logical formula
obtained by evaluating the equality condition %
\lstinline!result == theBalance! under the symbolic store shown
in the upper Locals pane.
\begin{exercise}\label{exercise:deposit}
Add a function that deposits a given amount into an account.
Verify the following \lstinline!main! function.
\begin{lstlisting}[basicstyle=\ttfamily\upshape]
int main()
//@ requires true;
//@ ensures true;
{
struct account *myAccount = create_account();
account_set_balance(myAccount, 5);
account_deposit(myAccount, 10);
int b = account_get_balance(myAccount);
assert(b == 15);
account_dispose(myAccount);
return 0;
}
\end{lstlisting}
Note: VeriFast checks for arithmetic overflow. For now, disable
this check in the \textbf{Verify} menu.
\end{exercise}
\begin{exercise}\label{exercise:limit}
Add a field \lstinline!limit! to struct \lstinline!account! that specifies the minimum balance of the account. (It is typically either zero or a negative number.)
The limit is specified at creation time. Further add a function
to withdraw a given amount from an account. The function must
respect the limit; if withdrawing the requested amount would violate the limit, then the largest amount that can be withdrawn without violating the limit is withdrawn. The function
returns the amount actually withdrawn as its return value. You
will need to use C's conditional expressions
\lstinline!condition ? value1 : value2!. Remove function
\lstinline!account_set_balance!. Use the shorthand notation for
field chunks: \lstinline!myAccount->balance |-> value!. Verify
the following \lstinline!main! function.
\begin{lstlisting}[basicstyle=\ttfamily\upshape]
int main()
//@ requires true;
//@ ensures true;
{
struct account *myAccount = create_account(-100);
account_deposit(myAccount, 200);
int w1 = account_withdraw(myAccount, 50);
assert(w1 == 50);
int b1 = account_get_balance(myAccount);
assert(b1 == 150);
int w2 = account_withdraw(myAccount, 300);
assert(w2 == 250);
int b2 = account_get_balance(myAccount);
assert(b2 == -100);
account_dispose(myAccount);
return 0;
}
\end{lstlisting}
\end{exercise}
\section{Predicates}
We continue with the program obtained in
Exercise~\ref{exercise:limit}. We observe that the contracts
are becoming rather long. Furthermore, if we consider the
account ``class'' and the main function to be in different
modules, then the internal implementation details of the
account module are exposed to the main function. We can achieve
more concise contracts as well as information hiding by
introducing a \emph{predicate} to describe an
$\mathsf{account}$ struct instance in the function contracts.
\begin{lstlisting}
/*@
predicate account_pred(struct account *myAccount, int theLimit, int theBalance) =
myAccount->limit |-> theLimit &*& myAccount->balance |-> theBalance
&*& malloc_block_account(myAccount);
@*/
\end{lstlisting}
A predicate is a named, parameterized assertion. Furthermore, it introduces a new type of heap chunk.
An \lstinline!account_pred! heap chunk bundles an \lstinline!account_limit! heap chunk, an \lstinline!account_balance! heap chunk,
and a \lstinline!malloc_block_account! heap chunk into one.
Let's use this predicate to rewrite the contract of the deposit function. Here's a first attempt:
\begin{lstlisting}
void account_deposit(struct account *myAccount, int amount)
//@ requires account_pred(myAccount, ?limit, ?balance) &*& 0 <= amount;
//@ ensures account_pred(myAccount, limit, balance + amount);
{
myAccount->balance += amount;
}
\end{lstlisting}
This function does not verify. The update of the
\lstinline!balance! field cannot be verified since there is no
\lstinline!account_balance! heap chunk in the symbolic heap.
There is only a \lstinline!account_pred! heap chunk. The
\lstinline!account_pred! heap chunk encapsulates the
\lstinline!account_balance! heap chunk, but VeriFast does not
``un-bundle'' the \lstinline!account_pred! predicate
automatically. We must instruct VeriFast to un-bundle predicate
heap chunks by inserting an \lstinline!open! ghost statement:
\begin{lstlisting}
void account_deposit(struct account *myAccount, int amount)
//@ requires account_pred(myAccount, ?limit, ?balance) &*& 0 <= amount;
//@ ensures account_pred(myAccount, limit, balance + amount);
{
//@ open account_pred(myAccount, limit, balance);
myAccount->balance += amount;
}
\end{lstlisting}
The assignment now verifies, but now VeriFast is stuck at the
postcondition. It complains that it cannot find the
\lstinline!account_pred! heap chunk that it is supposed to hand
back to the function's caller. The \lstinline!account_pred!
chunk's constituent chunks are present in the symbolic heap,
but VeriFast does not automatically bundle them up into an
\lstinline!account_pred! chunk. We must instruct VeriFast to do
so using a \lstinline!close! ghost statement:
\begin{lstlisting}
void account_deposit(struct account *myAccount, int amount)
//@ requires account_pred(myAccount, ?limit, ?balance) &*& 0 <= amount;
//@ ensures account_pred(myAccount, limit, balance + amount);
{
//@ open account_pred(myAccount, limit, balance);
myAccount->balance += amount;
//@ close account_pred(myAccount, limit, balance + amount);
}
\end{lstlisting}
The function now verifies. However, the main function does not,
since the call of \lstinline!account_deposit! expects an
\lstinline!account_pred! heap chunk.
\begin{exercise}\label{exercise:pred}
Rewrite the remaining contracts using the
\lstinline!account_pred! predicate. Insert \lstinline!open! and
\lstinline!close! statements as necessary.
\end{exercise}
\section{Recursive Predicates}
In the previous section, we introduced predicates for the sake
of conciseness and information hiding. However, there is an
even more compelling need for predicates: they are the only way
you can describe unbounded-size data structures in VeriFast.
Indeed, in the absence of predicates, the number of memory
locations described by an assertion is linear in the length of
the assertion. This limitation can be overcome through the use
of recursive predicates, i.e., predicates that invoke
themselves.
\begin{exercise}\label{exercise:stack}
Implement a stack of integers using a singly linked list data
structure: implement functions \lstinline!create_stack!,
\lstinline!stack_push!, \lstinline!stack_pop!, and
\lstinline!stack_dispose!. In order to be able to specify the
precondition of \lstinline!stack_pop!, your predicate will need
to have a parameter that specifies the number of elements in
the stack. Function \lstinline!stack_dispose! may be called
only on an empty stack. Do not attempt to specify the contents
of the stack; this is not possible with the annotation elements
we have seen. You will need to use conditional assertions:
\lstinline!condition ? assertion1 : assertion2!. Note: VeriFast
does not allow the use of field dereferences in
\lstinline!open! statements. If you want to use the value of a
field in an \lstinline!open! statement, you must first store
the value in a local variable. Verify the following main
function:
\end{exercise}
\begin{lstlisting}
int main()
//@ requires true;
//@ ensures true;
{
struct stack *s = create_stack();
stack_push(s, 10);
stack_push(s, 20);
stack_pop(s);
stack_pop(s);
stack_dispose(s);
return 0;
}
\end{lstlisting}
Now, let's extend the solution to Exercise~\ref{exercise:stack}
on page~\pageref{solution:stack} with a
\lstinline!stack_is_empty! function. Recall the predicate
definitions:
\begin{lstlisting}
predicate nodes(struct node *node, int count) =
node == 0 ?
count == 0
:
0 < count
&*& node->next |-> ?next &*& node->value |-> ?value
&*& malloc_block_node(node) &*& nodes(next, count - 1);
predicate stack(struct stack *stack, int count) =
stack->head |-> ?head &*& malloc_block_stack(stack) &*& 0 <= count &*& nodes(head, count);
\end{lstlisting}
Here's a first stab at a \lstinline!stack_is_empty! function:
\begin{lstlisting}
bool stack_is_empty(struct stack *stack)
//@ requires stack(stack, ?count);
//@ ensures stack(stack, count) &*& result == (count == 0);
{