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
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
"http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
<title>KLEE - KQuery Language Reference Manul</title>
<link type="text/css" rel="stylesheet" href="menu.css" />
<link type="text/css" rel="stylesheet" href="content.css" />
</head>
<body>
<!--#include virtual="menu.html.incl"-->
<div id="content">
<h1>KQuery Language Reference Manual</h1>
<h2>Table Of Contents</h2>
<ol>
<li><a href="#intro">Introduction</a></li>
<li><a href="#notation">Notation</a></li>
<li><a href="#structure">Structure</a></li>
<ol type="a">
<li><a href="#expr_labels">Expression and Version Labels</a>
</ol>
<li><a href="#literals">Literals</a>
<ol type="a">
<li><a href="#ident_literal">Identifiers</a></li>
<li><a href="#ident_number">Numbers</a></li>
<li><a href="#ident_types">Numbers</a></li>
</ol>
</li>
<li><a href="#decls">Declarations</a>
<ol type="a">
<li><a href="#array_decls">Arrays</a></li>
<li><a href="#query_commands">Query Commands</a></li>
</ol>
</li>
<li><a href="#versions">Versions</a></li>
<li><a href="#exprs">Expressions</a>
<ol type="a">
<li><a href="#primitive_expr">Primitive Expressions</a>
<ol type="i">
<li><a href="#ref_primitive_expr">Expression References</a></li>
<li><a href="#const_primitive_expr">Constants</a></li>
</ol>
</li>
<li><a href="#arith_expr">Arithmetic Operations</a>
<ol type="i">
<li><a href="#Add_expr">Add</a></li>
<li><a href="#Sub_expr">Sub</a></li>
<li><a href="#Mul_expr">Mul</a></li>
<li><a href="#UDiv_expr">UDiv</a></li>
<li><a href="#SDiv_expr">SDiv</a></li>
<li><a href="#URem_expr">URem</a></li>
<li><a href="#SRem_expr">SRem</a></li>
</ol>
</li>
<li><a href="#bit_expr">Bitwise Operations</a>
<ol type="i">
<li><a href="#And_expr">And</a></li>
<li><a href="#Or_expr">Or</a></li>
<li><a href="#Xor_expr">Xor</a></li>
<li><a href="#Shl_expr">Shl</a></li>
<li><a href="#LShr_expr">LShr</a></li>
<li><a href="#AShr_expr">AShr</a></li>
</ol>
</li>
<li><a href="#comp_expr">Comparisons</a>
<ol type="i">
<li><a href="#Eq_expr">Eq</a></li>
<li><a href="#Ne_expr">Ne</a></li>
<li><a href="#Ult_expr">Ult</a></li>
<li><a href="#Ule_expr">Ule</a></li>
<li><a href="#Ugt_expr">Ugt</a></li>
<li><a href="#Uge_expr">Uge</a></li>
<li><a href="#Slt_expr">Slt</a></li>
<li><a href="#Sle_expr">Sle</a></li>
<li><a href="#Sgt_expr">Sgt</a></li>
<li><a href="#Sge_expr">Sge</a></li>
</ol>
</li>
<li><a href="#bv_expr">Bitvector Manipulation</a>
<ol type="i">
<li><a href="#Concat_expr">Concat</a></li>
<li><a href="#Extract_expr">Extract</a></li>
<li><a href="#ZExt_expr">ZExt</a></li>
<li><a href="#SExt_expr">SExt</a></li>
</ol>
</li>
<li><a href="#special_expr">Special Expressions</a>
<ol type="i">
<li><a href="#Read_expr">Read</a></li>
<li><a href="#Select_expr">Select</a></li>
</ol>
</li>
<li><a href="#macro_expr">Macro Expressions</a>
<ol type="i">
<li><a href="#Neg_expr">Not</a></li>
<li><a href="#Not_expr">Not</a></li>
<li><a href="#ReadLSB_expr">ReadLSB</a></li>
<li><a href="#ReadMSB_expr">ReadMSB</a></li>
</ol>
</li>
</ol>
</li>
</ol>
<h2><a name="intro">Introduction</a></h2>
<p>The KQuery language is the textual representation of constraint
expressions and queries which is used as input to the Kleaver
constraint solver.</p>
<p>Currently the language is capable of representing quantifier free
formulas over bitvectors and arrays, with direct support for all
standard operations on bitvectors. The language has been designed to
be compact and easy to read and write.</p>
<p>The KQuery language is closely related to the C++ API for Exprs, see
also the
doxygen <a href="http://t1.minormatter.com/~ddunbar/klee-doxygen/classklee_1_1Expr.html">Expr</a>
documentation.</p>
<h2><a name="notation">Notation</a></h2>
<p>In this document, syntax is given in Extended Backus-Naur Form and appears as:</p>
<div class="syntax">
"(" "Eq" [ type ] LHS RHS ")"
</div>
<p>Unless noted, the rules are described in terms of tokens not characters,
and tokens can be separate by white space and comments.</p>
<p>In some case, a production like <i>child-expression</i> is used as an alias
for the <i>expression</i> production, when subsequent text needs to
differentiate the expression.</p>
<p>Examples are shown using:</p>
<div class="example">
(Eq w32 a b)
</div>
<h2><a name="structure">Structure</a></h2>
<p>A KQuery source file consists of a sequence of declarations.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
kquery = { array-declaration | query-command }
</div>
<p>Currently, the language supports two kinds of declarations:</p>
<ul>
<li><i><a href="#array_decls">Array Declarations</a></i>: Use to
declare an array of bitvectors for use in subsequent
expressions.</li>
<li><i><a href="#query_commands">Query Commands</a></i>: Used to
define queries which should be executed by the constraint solver. A
query consists of a set of constraints (assumptions), a query
expression, and optionally expressions and arrays to compute values
for if the query expression is invalid.</li>
</ul>
<p>Comments begin with "#" and continue until the end of line. For example:</p>
<div class="example">
(Add w32 1 1) <font color="Red"># Two, hopefully</font>
</div>
<h3><a name="expr_labels">Expression and Version Labels</a></h3>
<p>Expressions are frequently shared among constraints and query
expressions. In order to keep the output succinct and readable,
expression labels can be used to introduce a lexical binding which can
be used in subsequent expressions.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = identifier ":" expression<br>
</div>
<p>Likewise, versions are frequently shared among reads and can be labelled in
the same fashion.</p>
<p><b>Examples:</b></p>
<div class="example">
(Add w32 N0:(Add w32 1 1) N0) <font color="Red"># Four</font>
</div>
<h2><a name="literals">Literals</a></h2>
<h3><a name="ident_literal">Identifiers</a></h3>
<p>Identifiers are used for specifying array names and
for <a href="#expr_labels">expression labels</a>.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
identifier = "[a-zA-Z_][a-zA-Z0-9._]*"<br>
</div>
<p><b>Examples:</b></p>
<div class="example">
_foo<br>
arr10_20<br>
</div>
<p>Note that in order to keep open the possibility to introduce explicit
integral and floating-point types, the following identifiers are treated
as reserved keywords:</p>
<div class="syntax">
floating-point-type = "fp[0-9]+([.].*)?"<br>
integer-type = "i[0-9]+"<br>
</div>
<h3><a name="ident_number">Numbers</a></h3>
<p>Numeric constants can be specified as follows.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
number = "true" | "false" | signed-constant<br>
signed-constant = [ "+" | "-" ] ( dec-constant | bin-constant | oct-constant | hex-constant )<br>
dec-constant = "[0-9_]+"<br>
bin-constant = "0b[01_]+"<br>
oct-constant = "0o[0-7_]+"<br>
hex-constant = "0x[0-9a-fA-F_]+"<br>
</div>
<p><b>Examples:</b></p>
<div class="example">
false<br>
-10<br>
0b1000_0001 <font color="Red"># 129 </font><br>
</div>
<p>Non-decimal constants can be signed. The '_' character is ignored when
evaluating constants, but is available for use as a separator. </p>
<h3><a name="ident_type">Types</a></h3>
<p>Types are explicit operands to most expressions, and indicate the
bit-width of the type.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
type = "w[0-9]+"<br>
</div>
<p><b>Example:</b></p>
<div class="example">
w32<br>
</div>
<p>The numeric portion of the token is taken to be a decimal integer
specifying the bit-width of the type.</p>
<h2><a name="decls">Declarations</a></h2>
<h3><a name="array_decls">Arrays</a></h3>
<p>Arrays are the basic type for defining symbolic variables (the
language does not currently support simple variables).</p>
<p><b>Syntax:</b></p>
<div class="syntax">
array-declaration = "array" name "[" [ size ] "]" ":" domain "->" range "=" array-initializer<br>
array-initializer = "symbolic" | "{" { numeric-literal } "}"<br>
</div>
<p><b>Examples:</b></p>
<div class="example">
array foo[10] : w32 -> w8 = symbolic <font color="Red"># A ten element symbolic array</font><br>
array foo[4] : w8 -> w1 = { true, false, false, true } <font color="Red"># A constant array of four booleans</font><br>
</div>
<h3><a name="query_commands">Query Commands</a></h3>
<p>Query declarations describe the queries that the constraint solver
should run, along with optional additional arguments to specify
expressions and arrays for which counterexamples should be provided.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
query-command = "(" "query" constraint-list query-expression [ eval-expr-list [ eval-array-list ] ] ")" <br>
query-expression = expression<br>
constraint-list = "[" { expression } "]" <br>
eval-expr-list = "[" { expression } "]" <br>
eval-array-list = "[" { identifier } "]" <br>
</div>
<p><b>Examples:</b></p>
<div class="example">
(query [] false)<br>
(query [(Eq w8 (Read w8 mem 0) 10)] false [] [ mem ])<br>
</div>
<p>A query command consists a query, consisting of a constraint list and
a query expression, and two optional lists for use when a counterexample is desired.</p>
<p>The <i>constraint-list</i> is a list of expressions (with boolean
type) which are assumed to hold. Although not required in the language,
many solvers require that this set of constraints be
consistent. The <i>query-expression</i> is the expression to determine
the validity of.</p>
<p>If a counterexample is desired for invalid
queries, <i>eval-expr-list</i> is a list of expressions for which a
possible value should be constructed, and <i>eval-array-list</i> is a
list of arrays for which values for the entire array should be
provided. All counterexamples results must be simultaneously
feasible.</p>
<h2><a name="versions">Versions</a></h2>
<p>Versions are used to refer to an array with an ordered sequence of writes to it.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
version = identifier<br>
version = "[" [ update-list ] "]" [ "@" version "]"<br>
update-list = lhs-expression "=" rhs-expression [ "," update-list ]<br>
</div>
<p>A version can be specified either by an identifier, which can refer to an
array or a <a href="#expr_labels">labelled version</a>, or by an explicit list
of writes which are to be concatenated to another version (the most recent
writes are first).</p>
<p>FIXME: Get rid of anonymous arrays.</p>
<h2><a name="exprs">Expressions</a></h2>
<p>Expressions are strongly typed, and have the following general
form:</p>
<div class="syntax">
"(" EXPR_NAME EXPR_TYPE ... arguments ... ")"
</div>
<p>where <i>EXPR_NAME</i> is the expression name, <i>EXPR_TYPE</i> is the
expression type (which may be optional), followed by any additional
arguments.</p>
<h3><a name="primitive_expr">Primitive Expressions</a></h3>
<h4><a name="ref_primitive_expr">Expression References</a></h4>
<p>An expression reference can be used to refer to a
previously <a href="#expr_labels">labelled expression</a>.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = identifier<br>
</div>
<p>Expression and version labels are in separate namespaces, it is the users
responsibility to use separate labels to preserve readability.</p>
<h4><a name="const_primitive_expr">Constants</a></h4>
<p>Constants are specified by a numeric token or a type and numeric
token.</p>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = number | "(" type number ")"<br>
</div>
<p>When a constant is specified without a type, the resulting expression
is only well-formed if its type can be inferred from the enclosing
context. The <b>true</b> and <b>false</b> constants always have
type <b>w1</b>.
<p><b>Examples:</b></p>
<div class="example">
true<br>
(w32 0)<br>
(Add w32 10 20) <font color="Red"># The type for 10 and 20 is inferred to be w32.</font><br>
</div>
<h3><a name="arith_expr">Arithmetic Operations</a></h3>
<h4><a name="Add_expr">Add</a>,
<a name="Sub_expr">Sub</a>,
<a name="Mul_expr">Mul</a>,
<a name="UDiv_expr">UDiv</a>,
<a name="SDiv_expr">SDiv</a>,
<a name="URem_expr">URem</a>,
<a name="SRem_expr">SRem</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
arithmetic-expr-kind = ( "Add" | "Sub" | "Mul" | "UDiv" | "SDiv" | "URem" )<br>
expression = "(" arithmetic-expr-kind type expression expression ")"<br>
</div>
<p>Arithmetic operations are always binary and the types of the left-
and right-hand side expressions must match the expression type.</p>
<h3><a name="bit_expr">Bitwise Operations</a></h3>
<h4><a name="And_expr">And</a>,
<a name="Or_expr">Or</a>,
<a name="Xor_expr">Xor</a>,
<a name="Shl_expr">Shl</a>,
<a name="LShr_expr">LShr</a>,
<a name="AShr_expr">AShr</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
bitwise-expr-kind = ( "And" | "Or" | "Xor" | "Shl" | "LShr" | "AShr" )<br>
expression = "(" bitwise-expr-kind type expression expression ")"<br>
</div>
<p>Bitwise operations are always binary and the types of the left-
and right-hand side expressions must match the expression type.</p>
<p>FIXME: Pin down semantics of Shl, LShr, and AShr.</p>
<h3><a name="comp_expr">Comparisons</a></h3>
<h4><a name="Eq_expr">Eq</a>,
<a name="Ne_expr">Ne</a>,
<a name="Ult_expr">Ult</a>,
<a name="Ule_expr">Ule</a>,
<a name="Ugt_expr">Ugt</a>,
<a name="Uge_expr">Uge</a>,
<a name="Slt_expr">Slt</a>,
<a name="Sle_expr">Sle</a>,
<a name="Sgt_expr">Sgt</a>,
<a name="Sge_expr">Sge</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
comparison-expr-kind = ( "Eq" | "Ne" | "Ult" | "Ule" | "Ugt" | "Uge" | "Slt" | "Sle" | "Sgt" | "Sge" )<br>
expression = "(" comparison-expr-kind [ type ] expression expression ")"<br>
</div>
<p>Comparison operations are always binary and the types of the left-
and right-hand side expression must match. If the type is specified, it
must be <b>w1</b>.</p>
<h3><a name="bv_expr">Bitvector Manipulation</a></h3>
<h4><a name="Concat_expr">Concat</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "Concat" [type] msb-expression lsb-expression ")"
</div>
<p><b>Concat</b> evaluates to a <i>type</i> bits formed by
concatenating <i>lsb-expression</i> to <i>msb-expression</i>.</p>
<h4><a name="Extract_expr">Extract</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "Extract" type offset-number child-expression ")"
</div>
<p><b>Extract</b> evaluates to <i>type</i> bits from <i>child-expression</i>
taken from <i>offset-number</i>, where <i>offset-number</i> is the index of
the least-significant bit in <i>child-expression</i> which should be
extracted.
<h4><a name="ZExt_expr">ZExt</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "ZExt" type child-expression ")"
</div>
<p><b>ZExt</b> evaluates to the lowest <i>type</i> bits
of <i>child-expression</i>, with undefined bits set to zero.</p>
<h4><a name="SExt_expr">SExt</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "SExt" type input-expression ")"
</div>
<p><b>SExt</b> evaluates to the lowest <i>type</i> bits
of <i>child-expression</i>, with undefined bits set to the most-significant
bit of <i>input-expression</i>.</p>
<h3><a name="special_expr">Special Expressions</a></h3>
<h4><a name="Read_expr">Read</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "Read" type index-expression version-specifier ")"<br>
</div>
<p>The <b>Read</b> expression evaluates to the first write
in <i>version-specifier</i> for which <i>index-expression</i> is equivalent to
the index in the write. The type of the expression must match the range of the
root array in <i>version-specifier</i>, and the type
of <i>index-expression</i> must match the domain.</p>
<h4><a name="Select_expr">Select</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "Select" type cond-expression true-expression false-expression ")"<br>
</div>
<p>The <b>Select</b> expression evalues to <i>true-expression</i> if the
condition evaluates to true, and to <i>false-expression</i> if the condition
evaluates to false. The <i>cond-expression</i> must have type <b>w1</b>.</p>
<p>Both the true and false expressions must be well-formed, regardless of the
condition expression. In particular, it is not legal for one of the
expressions to cause a division-by-zero during evaluation, even if
the <b>Select</b> expression will never evaluate to that expression.</p>
<h3><a name="macro_expr">Macro Expressions</a></h3>
<p>Several common expressions are not implemented directly in the Expr
library, but can be expressed in terms of other operations. A number of these
are implemented as "macros". The pretty printer recognizes and prints the
appropriate Expr forms as the macro, and the parser recognizes them and turns
them into the underlying representation.</p>
<h4><a name="Neg_expr">Neg</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "Neg" [ type ] expression ")"
</div>
<p>This macro form can be used to generate a <b>Sub</b> from zero.</p>
<h4><a name="Not_expr">Not</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "Not" [ type ] expression ")"
</div>
<p>This macro form can be used to generate an <b>Eq</b> comparison to zero. If
the type is specified, it must be <b>w1</b>.</p>
<h4><a name="ReadLSB_expr">ReadLSB</a>,
<a name="ReadMSB_expr">ReadMSB</a></h4>
<p><b>Syntax:</b></p>
<div class="syntax">
expression = "(" "ReadLSB" type index-expression version-specifier ")"<br>
expression = "(" "ReadMSB" type index-expression version-specifier ")"<br>
</div>
<p><b>ReadLSB</b> and <b>ReadMSB</b> can be used to simplify contiguous array
accesses. The type of the expression must be a multiple <i>N</i> of the array
range type. The expression expands to a concatenation of <i>N</i> read
expressions, where each read is done at a subsequent offset from
the <i>index-expression</i>. For <b>ReadLSB</b> (<b>ReadMSB</b>), the
concatentation is done such that the read at <i>index-expression</i> forms the
least- (most-) significant bits.</p>
</div>
</body>
</html>
|
