[klee-dev] kquery: versions. version-specifier and version labels

[Daniel Liew]

> In the section "Expression and Version Labels" it says "Likewise,
> versions are frequently shared among reads and can be labelled in the
> same fashion." What does this mean exactly?
> Does it mean
>     version = identifier ":" version
> or does it mean
>     expression = identifier ":" version
>
I believe it means:

version = identifier ":" version

> In the definition of "Read", "ReadLSB" and "ReadMSB" a terminal-symbol
> "version-specifier" is used. At this point it is really not clear to me
> what is meant by this.
> At first I thought it is just an identifier/version but this contradicts
> "(Read w8 mem 0)" (given as an example in the "Query Commands"-Section).
> 0 can only be a numeric-literal, how does this fit into the definition?

The (Read w8 mem 0) is a mistake it should read (Read w8 0 mem) , 0 is
the "index-expression" and mem is the "version-specifier"

Similarly "version-specifier" is probably also a mistake. To be
consistent with the rest of the document it should say "version"
instead.


> Besides that I found one minor mistake:
> In the syntax-definition of array the following is stated:
>     array-initializer = "symbolic" | "[" { numeric-literal } "]"
> This does not match the example given in the same section (commas
> missing in the definition?)
>     array foo[] : w8 -> w1 = [ true, false, false, true ]

Nice catch. Another thing to fix in the documentation. I'll write a
patch for the documentation later today and submit it.

As Cristian mentioned though why do you need to build a KQuery parser?

1. KLEE already has a KQuery parser.

2. Constraints don't have to specified in the KQuery language. They
can also be specified in the SMT-LIBv2 langauge. Klee can produce
these by using options like --write-smt2s and
--user-query-log=solver:smt2. In Kleaver, the tool for parsing and
evaluating KQuery files (*.pc files) you can also convert KQuery to
SMT-LIBv2 by using --print-smtlib . There are already several
SMT-LIBv2 parsers in existance ( see http://www.smtlib.org/  and click
on Utilities)

Hope this helps,
Dan Liew.