-
Notifications
You must be signed in to change notification settings - Fork 0
/
2015-06-15-000-using-quickcheck-to-test-c-apis.html
402 lines (345 loc) · 31.4 KB
/
2015-06-15-000-using-quickcheck-to-test-c-apis.html
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
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<link rel="alternate"
type="application/rss+xml"
href="https://magnus.therning.org/feed.xml"
title="RSS feed for https://magnus.therning.org/">
<title>Using QuickCheck to test C APIs</title>
<meta name="author" content="Magnus Therning"><meta name="referrer" content="no-referrer"><link href= "static/style.css" rel="stylesheet" type="text/css" /><link href= "static/htmlize.css" rel="stylesheet" type="text/css" /><link href= "static/extra_style.css" rel="stylesheet" type="text/css" /></head>
<body>
<div id="preamble" class="status"><div class="nav-bar"><a class="nav-link" href="./index.html">Top</a><a class="nav-link" href="./archive.html">Archive</a><a class="nav-link align-right" href="./feed.xml"><img src="static/rss-feed-icon.png" style="height: 24px;" /></a></div></div>
<div id="content">
<div class="post-date">15 Jun 2015</div><h1 class="post-title"><a href="https://magnus.therning.org/2015-06-15-000-using-quickcheck-to-test-c-apis.html">Using QuickCheck to test C APIs</a></h1>
<p>
Last year at ICFP I attended the <a href="http://cufp.org/2014/t12-john-hughes-introduction-to-testing-with-quickcheck.html">tutorial on QuickCheck</a> with John Hughes. We got
to use the Erlang implementation of QuickCheck to test a C API. Ever since I've
been planning to do the same thing using Haskell. I've put it off for the better
part of a year now, but then Francesco Mazzoli wrote about <a href="http://hackage.haskell.org/package/inline-c">inline-c</a> (<a href="https://www.fpcomplete.com/blog/2015/05/inline-c">Call C
functions from Haskell without bindings</a> and I found the motivation to actually
start writing some code.
</p>
<div id="outline-container-org755182d" class="outline-2">
<h2 id="org755182d">The general idea</h2>
<div class="outline-text-2" id="text-org755182d">
<p>
Many C APIs are rather stateful beasts so to test it I
</p>
<ol class="org-ol">
<li>generate a sequence of API calls (a program of sorts),</li>
<li>run the sequence against a model,</li>
<li>run the sequence against the real implementation, and</li>
<li>compare the model against the real state each step of the way.</li>
</ol>
</div>
</div>
<div id="outline-container-org5c47d51" class="outline-2">
<h2 id="org5c47d51">The C API</h2>
<div class="outline-text-2" id="text-org5c47d51">
<p>
To begin with I hacked up a simple implementation of a stack in C. The
"specification" is
</p>
<div class="org-src-container">
<pre class="src src-c"><span class="org-doc">/**</span>
<span class="org-doc"> * Create a stack.</span>
<span class="org-doc"> */</span>
<span class="org-type">void</span> *<span class="org-function-name">create</span><span class="org-rainbow-delimiters-depth-1">()</span>;
<span class="org-doc">/**</span>
<span class="org-doc"> * Push a value onto an existing stack.</span>
<span class="org-doc"> */</span>
<span class="org-type">void</span> <span class="org-function-name">push</span> <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-type">void</span> *, <span class="org-type">int</span><span class="org-rainbow-delimiters-depth-1">)</span>;
<span class="org-doc">/**</span>
<span class="org-doc"> * Pop a value off an existing stack.</span>
<span class="org-doc"> */</span>
<span class="org-type">int</span> <span class="org-function-name">pop</span><span class="org-rainbow-delimiters-depth-1">(</span><span class="org-type">void</span> *<span class="org-rainbow-delimiters-depth-1">)</span>;
</pre>
</div>
<p>
Using <code>inline-c</code> to create bindings for it is amazingly simple:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-pragma">{-# LANGUAGE QuasiQuotes #-}</span>
<span class="org-haskell-pragma">{-# LANGUAGE TemplateHaskell #-}</span>
<span class="org-haskell-keyword">module</span> <span class="org-haskell-constructor">CApi</span>
<span class="org-haskell-keyword">where</span>
<span class="org-haskell-keyword">import</span> <span class="org-haskell-keyword">qualified</span> <span class="org-haskell-constructor">Language.C.Inline</span> <span class="org-haskell-keyword">as</span> <span class="org-haskell-constructor">C</span>
<span class="org-haskell-keyword">import</span> <span class="org-haskell-constructor">Foreign.Ptr</span>
C<span class="org-haskell-definition">.</span>include <span class="org-string">"stack.h"</span>
<span class="org-haskell-definition">create</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">IO</span> <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-type">Ptr</span> <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-2">()</span></span><span class="org-rainbow-delimiters-depth-1">)</span>
<span class="org-haskell-definition">create</span> <span class="org-haskell-operator">=</span> <span class="org-rainbow-delimiters-depth-1">[</span>C.exp<span class="org-haskell-quasi-quote">| void * { create() } |</span><span class="org-rainbow-delimiters-depth-1">]</span>
<span class="org-haskell-definition">push</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">Ptr</span> <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-1">()</span></span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">C.CInt</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">IO</span> <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-1">()</span></span>
<span class="org-haskell-definition">push</span> s i <span class="org-haskell-operator">=</span> <span class="org-rainbow-delimiters-depth-1">[</span>C.exp<span class="org-haskell-quasi-quote">| void { push($(void *s), $(int i)) } |</span><span class="org-rainbow-delimiters-depth-1">]</span>
<span class="org-haskell-definition">pop</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">Ptr</span> <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-1">()</span></span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">IO</span> <span class="org-haskell-type">C.CInt</span>
<span class="org-haskell-definition">pop</span> s <span class="org-haskell-operator">=</span> <span class="org-rainbow-delimiters-depth-1">[</span>C.exp<span class="org-haskell-quasi-quote">| int { pop($(void *s)) } |</span><span class="org-rainbow-delimiters-depth-1">]</span>
</pre>
</div>
<p>
In the code below I import this module qualified.
</p>
</div>
</div>
<div id="outline-container-org7f43b7c" class="outline-2">
<h2 id="org7f43b7c">Representing a program</h2>
<div class="outline-text-2" id="text-org7f43b7c">
<p>
To represent a sequence of calls I first used a custom type, but later realised
that there really was no reason at all to not use a wrapped list:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-keyword">newtype</span> <span class="org-haskell-type">Program</span> a <span class="org-haskell-operator">=</span> <span class="org-haskell-constructor">P</span> <span class="org-rainbow-delimiters-depth-1">[</span>a<span class="org-rainbow-delimiters-depth-1">]</span>
<span class="org-haskell-keyword">deriving</span> <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">Eq</span>, <span class="org-haskell-constructor">Foldable</span>, <span class="org-haskell-constructor">Functor</span>, <span class="org-haskell-constructor">Show</span>, <span class="org-haskell-constructor">Traversable</span><span class="org-rainbow-delimiters-depth-1">)</span>
</pre>
</div>
<p>
Then each of the C API functions can be represented with
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-keyword">data</span> <span class="org-haskell-type">Statement</span> <span class="org-haskell-operator">=</span> <span class="org-haskell-constructor">Create</span> <span class="org-haskell-operator">|</span> <span class="org-haskell-constructor">Push</span> <span class="org-haskell-constructor">Int</span> <span class="org-haskell-operator">|</span> <span class="org-haskell-constructor">Pop</span>
<span class="org-haskell-keyword">deriving</span> <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">Eq</span>, <span class="org-haskell-constructor">Show</span><span class="org-rainbow-delimiters-depth-1">)</span>
</pre>
</div>
</div>
</div>
<div id="outline-container-org63a6359" class="outline-2">
<h2 id="org63a6359"><code>Arbitrary</code> for <code>Statement</code></h2>
<div class="outline-text-2" id="text-org63a6359">
<p>
My implementation of <code>Arbitrary</code> for <code>Statement</code> is very simple:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-keyword">instance</span> <span class="org-haskell-type">Arbitrary</span> <span class="org-haskell-type">Statement</span> <span class="org-haskell-keyword">where</span>
arbitrary <span class="org-haskell-operator">=</span> oneof <span class="org-rainbow-delimiters-depth-1">[</span>return <span class="org-haskell-constructor">Create</span>, return <span class="org-haskell-constructor">Pop</span>, liftM <span class="org-haskell-constructor">Push</span> arbitrary<span class="org-rainbow-delimiters-depth-1">]</span>
shrink <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">Push</span> i<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator">=</span> <span class="org-haskell-constructor">Push</span> <span class="org-haskell-operator"><$></span> shrink i
shrink <span class="org-haskell-keyword">_</span> <span class="org-haskell-operator">=</span> <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-1">[]</span></span>
</pre>
</div>
<p>
That is, <code>arbitrary</code> just returns one of the constructors of <code>Statement</code>, and
shrinking only returns anything for the one constructor that takes an argument,
<code>Push</code>.
</p>
</div>
</div>
<div id="outline-container-org2a84010" class="outline-2">
<h2 id="org2a84010">Prerequisites of <code>Arbitrary</code> for <code>Program Statement</code></h2>
<div class="outline-text-2" id="text-org2a84010">
<p>
I want to ensure that all <code>Program Statement</code> are valid, which means I need to
define the model for running the program and functions for checking the
precondition of a statement as well as for updating the model (i.e. for running
the <code>Statement</code>).
</p>
<p>
Based on the <a href="#org5c47d51">C API</a> above it seems necessary to track creation, the contents of
the stack, and even if it isn't explicitly mentioned it's probably a good idea
to track the popped value. Using <a href="http://hackage.haskell.org/package/record"><code>record</code></a> (<code>Record</code> is imported as <code>R</code>, and
<code>Record.Lens</code> as <code>RL</code>) I defined it like this:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-keyword">type</span> <span class="org-haskell-type">ModelContext</span> <span class="org-haskell-operator">=</span> <span class="org-rainbow-delimiters-depth-1">[</span>R.r<span class="org-haskell-quasi-quote">| { created :: Bool, pop :: Maybe Int, stack :: [Int] } |</span><span class="org-rainbow-delimiters-depth-1">]</span>
</pre>
</div>
<p>
Based on the rather informal specification I coded the pre-conditions for the
three statements as
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">preCond</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">ModelContext</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">Statement</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">Bool</span>
<span class="org-haskell-definition">preCond</span> ctx <span class="org-haskell-constructor">Create</span> <span class="org-haskell-operator">=</span> not <span class="org-haskell-operator">$</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| created |</span><span class="org-rainbow-delimiters-depth-1">]</span> ctx
<span class="org-haskell-definition">preCond</span> ctx <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">Push</span> <span class="org-haskell-keyword">_</span><span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| created |</span><span class="org-rainbow-delimiters-depth-1">]</span> ctx
<span class="org-haskell-definition">preCond</span> ctx <span class="org-haskell-constructor">Pop</span> <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| created |</span><span class="org-rainbow-delimiters-depth-1">]</span> ctx
</pre>
</div>
<p>
That is
</p>
<ul class="org-ul">
<li><code>Create</code> requires that the stack hasn't been created already.</li>
<li><code>Push i</code> requires that the stack has been created.</li>
<li><code>Pop</code> also requires that the stack has been created.</li>
</ul>
<p>
Furthermore the "specification" suggests the following definition of a function
for running a statement:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">modelRunStatement</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">ModelContext</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">Statement</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">ModelContext</span>
<span class="org-haskell-definition">modelRunStatement</span> ctx <span class="org-haskell-constructor">Create</span> <span class="org-haskell-operator">=</span> RL.set <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| created |</span><span class="org-rainbow-delimiters-depth-1">]</span> <span class="org-haskell-constructor">True</span> ctx
<span class="org-haskell-definition">modelRunStatement</span> ctx <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">Push</span> i<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator">=</span> RL.over <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| stack |</span><span class="org-rainbow-delimiters-depth-1">]</span> <span class="org-rainbow-delimiters-depth-1">(</span>i <span class="org-haskell-constructor">:</span><span class="org-rainbow-delimiters-depth-1">)</span> ctx
<span class="org-haskell-definition">modelRunStatement</span> ctx <span class="org-haskell-constructor">Pop</span> <span class="org-haskell-operator">=</span> <span class="org-rainbow-delimiters-depth-1">[</span>R.r<span class="org-haskell-quasi-quote">| { created = c, pop = headMay s, stack = tail s } |</span><span class="org-rainbow-delimiters-depth-1">]</span>
<span class="org-haskell-keyword">where</span>
c <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| created |</span><span class="org-rainbow-delimiters-depth-1">]</span> ctx
s <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| stack |</span><span class="org-rainbow-delimiters-depth-1">]</span> ctx
</pre>
</div>
<p>
(This definition assumes that the model satisfies the pre-conditions, as can be
seen in the use of <code>tail</code>.)
</p>
</div>
</div>
<div id="outline-container-org9eab783" class="outline-2">
<h2 id="org9eab783"><code>Arbitrary</code> for <code>Program Statement</code></h2>
<div class="outline-text-2" id="text-org9eab783">
<p>
With this in place I can define <code>Arbitrary</code> for <code>Program Statement</code> as
follows.
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-keyword">instance</span> <span class="org-haskell-type">Arbitrary</span> <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-type">Program</span> <span class="org-haskell-type">Statement</span><span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-keyword">where</span>
arbitrary <span class="org-haskell-operator">=</span> liftM <span class="org-haskell-constructor">P</span> <span class="org-haskell-operator">$</span> ar baseModelCtx
<span class="org-haskell-keyword">where</span>
ar m <span class="org-haskell-operator">=</span> <span class="org-haskell-keyword">do</span>
push <span class="org-haskell-operator"><-</span> liftM <span class="org-haskell-constructor">Push</span> arbitrary
<span class="org-haskell-keyword">let</span> possible <span class="org-haskell-operator">=</span> filter <span class="org-rainbow-delimiters-depth-1">(</span>preCond m<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-rainbow-delimiters-depth-1">[</span><span class="org-haskell-constructor">Create</span>, <span class="org-haskell-constructor">Pop</span>, push<span class="org-rainbow-delimiters-depth-1">]</span>
<span class="org-haskell-keyword">if</span> null possible
<span class="org-haskell-keyword">then</span> return <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-1">[]</span></span>
<span class="org-haskell-keyword">else</span> <span class="org-haskell-keyword">do</span>
s <span class="org-haskell-operator"><-</span> oneof <span class="org-rainbow-delimiters-depth-1">(</span>map return possible<span class="org-rainbow-delimiters-depth-1">)</span>
<span class="org-haskell-keyword">let</span> m' <span class="org-haskell-operator">=</span> modelRunStatement m s
frequency <span class="org-rainbow-delimiters-depth-1">[</span><span class="org-rainbow-delimiters-depth-2">(</span><span class="org-highlight-numbers-number">499</span>, liftM2 <span class="org-rainbow-delimiters-depth-3">(</span><span class="org-haskell-constructor">:</span><span class="org-rainbow-delimiters-depth-3">)</span> <span class="org-rainbow-delimiters-depth-3">(</span>return s<span class="org-rainbow-delimiters-depth-3">)</span> <span class="org-rainbow-delimiters-depth-3">(</span>ar m'<span class="org-rainbow-delimiters-depth-3">)</span><span class="org-rainbow-delimiters-depth-2">)</span>, <span class="org-rainbow-delimiters-depth-2">(</span><span class="org-highlight-numbers-number">1</span>, return <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-3">[]</span></span><span class="org-rainbow-delimiters-depth-2">)</span><span class="org-rainbow-delimiters-depth-1">]</span>
</pre>
</div>
<p>
The idea is to, in each step, choose a valid statement given the provided model
and cons it with the result of a recursive call with an updated model. The
constant 499 is just an arbitrary one I chose after running <code>arbitrary</code> a few
times to see how long the generated programs were.
</p>
<p>
For shrinking I take advantage of the already existing implementation for lists:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">shrink</span> <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">P</span> p<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator">=</span> filter allowed <span class="org-haskell-operator">$</span> map <span class="org-haskell-constructor">P</span> <span class="org-rainbow-delimiters-depth-1">(</span>shrink p<span class="org-rainbow-delimiters-depth-1">)</span>
<span class="org-haskell-keyword">where</span>
allowed <span class="org-haskell-operator">=</span> and <span class="org-haskell-operator">.</span> snd <span class="org-haskell-operator">.</span> mapAccumL go baseModelCtx
<span class="org-haskell-keyword">where</span>
go ctx s <span class="org-haskell-operator">=</span> <span class="org-rainbow-delimiters-depth-1">(</span>modelRunStatement ctx s, preCond ctx s<span class="org-rainbow-delimiters-depth-1">)</span>
</pre>
</div>
</div>
</div>
<div id="outline-container-org637962f" class="outline-2">
<h2 id="org637962f">Some thoughts so far</h2>
<div class="outline-text-2" id="text-org637962f">
<p>
I would love making an implementation of <code>Arbitrary s</code>, where <code>s</code> is something
that implements a type class that contains <code>preCond</code>, <code>modelRunStatement</code> and
anything else needed. I made an attempt using something like
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-keyword">class</span> <span class="org-haskell-type">S</span> a <span class="org-haskell-keyword">where</span>
<span class="org-haskell-keyword">type</span> <span class="org-haskell-type">Ctx</span> a <span class="org-haskell-operator">::</span> <span class="org-haskell-operator">*</span>
baseCtx <span class="org-haskell-operator">::</span> <span class="org-haskell-type">Ctx</span> a
preCond <span class="org-haskell-operator">::</span> <span class="org-haskell-type">Ctx</span> a <span class="org-haskell-operator">-></span> a <span class="org-haskell-operator">-></span> <span class="org-haskell-type">Bool</span>
<span class="org-haskell-operator">...</span>
</pre>
</div>
<p>
However, when trying to use <code>baseCtx</code> in an implementation of <code>arbitrary</code> I ran
into the issue of injectivity. I'm still not entirely sure what that means, or
if there is something I can do to work around it. Hopefully someone reading this
can offer a solution.
</p>
</div>
</div>
<div id="outline-container-orga64057c" class="outline-2">
<h2 id="orga64057c">Running the C code</h2>
<div class="outline-text-2" id="text-orga64057c">
<p>
When running the sequence of <code>Statement</code> against the C code I catch the results
in
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-keyword">type</span> <span class="org-haskell-type">RealContext</span> <span class="org-haskell-operator">=</span> <span class="org-rainbow-delimiters-depth-1">[</span>r<span class="org-haskell-quasi-quote">| { o :: Ptr (), pop :: Maybe Int } |</span><span class="org-rainbow-delimiters-depth-1">]</span>
</pre>
</div>
<p>
Actually running a statement and capturing the output in a <code>RealContext</code> is
easily done using <code>inline-c</code> and <code>record</code>:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">realRunStatement</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">RealContext</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">Statement</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">IO</span> <span class="org-haskell-type">RealContext</span>
<span class="org-haskell-definition">realRunStatement</span> ctx <span class="org-haskell-constructor">Create</span> <span class="org-haskell-operator">=</span> CApi.create <span class="org-haskell-operator">>>=</span> <span class="org-haskell-operator">\</span> ptr <span class="org-haskell-operator">-></span> return <span class="org-haskell-operator">$</span> RL.set <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| o |</span><span class="org-rainbow-delimiters-depth-1">]</span> ptr ctx
<span class="org-haskell-definition">realRunStatement</span> ctx <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">Push</span> i<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator">=</span> CApi.push o <span class="org-rainbow-delimiters-depth-1">(</span>toEnum i<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator">>></span> return ctx
<span class="org-haskell-keyword">where</span>
o <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| o |</span><span class="org-rainbow-delimiters-depth-1">]</span> ctx
<span class="org-haskell-definition">realRunStatement</span> ctx <span class="org-haskell-constructor">Pop</span> <span class="org-haskell-operator">=</span> CApi.pop o <span class="org-haskell-operator">>>=</span> <span class="org-haskell-operator">\</span> v <span class="org-haskell-operator">-></span> return <span class="org-haskell-operator">$</span> RL.set <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| pop |</span><span class="org-rainbow-delimiters-depth-1">]</span> <span class="org-rainbow-delimiters-depth-1">(</span><span class="org-haskell-constructor">Just</span> <span class="org-rainbow-delimiters-depth-2">(</span>fromEnum v<span class="org-rainbow-delimiters-depth-2">)</span><span class="org-rainbow-delimiters-depth-1">)</span> ctx
<span class="org-haskell-keyword">where</span>
o <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| o |</span><span class="org-rainbow-delimiters-depth-1">]</span> ctx
</pre>
</div>
</div>
</div>
<div id="outline-container-org8c5786b" class="outline-2">
<h2 id="org8c5786b">Comparing states</h2>
<div class="outline-text-2" id="text-org8c5786b">
<p>
Comparing a <code>ModelContext</code> and a <code>RealContext</code> is easily done:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">compCtx</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">ModelContext</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">RealContext</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">Bool</span>
<span class="org-haskell-definition">compCtx</span> mc rc <span class="org-haskell-operator">=</span> mcC <span class="org-haskell-operator">==</span> rcC <span class="org-haskell-operator">&&</span> mcP <span class="org-haskell-operator">==</span> rcP
<span class="org-haskell-keyword">where</span>
mcC <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| created |</span><span class="org-rainbow-delimiters-depth-1">]</span> mc
rcC <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| o |</span><span class="org-rainbow-delimiters-depth-1">]</span> rc <span class="org-haskell-operator">/=</span> nullPtr
mcP <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| pop|</span><span class="org-rainbow-delimiters-depth-1">]</span> mc
rcP <span class="org-haskell-operator">=</span> RL.view <span class="org-rainbow-delimiters-depth-1">[</span>R.l<span class="org-haskell-quasi-quote">| pop|</span><span class="org-rainbow-delimiters-depth-1">]</span> rc
</pre>
</div>
</div>
</div>
<div id="outline-container-org12af561" class="outline-2">
<h2 id="org12af561">Verifying a <code>Program Statement</code></h2>
<div class="outline-text-2" id="text-org12af561">
<p>
With all that in place I can finally write a function for checking the validity
of a program:
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">validProgram</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">Program</span> <span class="org-haskell-type">Statement</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">IO</span> <span class="org-haskell-type">Bool</span>
<span class="org-haskell-definition">validProgram</span> p <span class="org-haskell-operator">=</span> and <span class="org-haskell-operator"><$></span> snd <span class="org-haskell-operator"><$></span> mapAccumM go <span class="org-rainbow-delimiters-depth-1">(</span>baseModelCtx, baseRealContext<span class="org-rainbow-delimiters-depth-1">)</span> p
<span class="org-haskell-keyword">where</span>
runSingleStatement mc rc s <span class="org-haskell-operator">=</span> realRunStatement rc s <span class="org-haskell-operator">>>=</span> <span class="org-haskell-operator">\</span> rc' <span class="org-haskell-operator">-></span> return <span class="org-rainbow-delimiters-depth-1">(</span>modelRunStatement mc s, rc'<span class="org-rainbow-delimiters-depth-1">)</span>
go <span class="org-rainbow-delimiters-depth-1">(</span>mc, rc<span class="org-rainbow-delimiters-depth-1">)</span> s <span class="org-haskell-operator">=</span> <span class="org-haskell-keyword">do</span>
ctxs<span class="org-haskell-operator">@</span><span class="org-rainbow-delimiters-depth-1">(</span>mc', rc'<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator"><-</span> runSingleStatement mc rc s
return <span class="org-rainbow-delimiters-depth-1">(</span>ctxs, compCtx mc' rc'<span class="org-rainbow-delimiters-depth-1">)</span>
</pre>
</div>
<p>
(This uses <code>mapAccumM</code> from an <a href="2015-06-09-000-mapaccum-in-monad.html">earlier post of mine</a>.)
</p>
</div>
</div>
<div id="outline-container-org813eb63" class="outline-2">
<h2 id="org813eb63">The property, finally!</h2>
<div class="outline-text-2" id="text-org813eb63">
<p>
To wrap this all up I then define the property
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">prop_program</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">Program</span> <span class="org-haskell-type">Statement</span> <span class="org-haskell-operator">-></span> <span class="org-haskell-type">Property</span>
<span class="org-haskell-definition">prop_program</span> p <span class="org-haskell-operator">=</span> monadicIO <span class="org-haskell-operator">$</span> run <span class="org-rainbow-delimiters-depth-1">(</span>validProgram p<span class="org-rainbow-delimiters-depth-1">)</span> <span class="org-haskell-operator">>>=</span> assert
</pre>
</div>
<p>
and a main function
</p>
<div class="org-src-container">
<pre class="src src-haskell"><span class="org-haskell-definition">main</span> <span class="org-haskell-operator">::</span> <span class="org-haskell-type">IO</span> <span class="org-haskell-constructor"><span class="org-rainbow-delimiters-depth-1">()</span></span>
<span class="org-haskell-definition">main</span> <span class="org-haskell-operator">=</span> quickCheck prop_program
</pre>
</div>
<hr>
<p>
<i>Edit 2015-07-17</i>: Adjusted the description of the pre-conditions to match the
code.
</p>
</div>
</div>
<div class="taglist"><a href="https://magnus.therning.org/tags.html">Tags</a>: <a href="https://magnus.therning.org/tag-haskell.html">haskell</a> <a href="https://magnus.therning.org/tag-quickcheck.html">quickcheck</a> <a href="https://magnus.therning.org/tag-testing.html">testing</a> </div></div>
<div id="postamble" class="status"><!-- org-static-blog-page-postamble --></div>
</body>
</html>