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

[Jonathan Koch]

Thanks a lot for the clarification.

Regarding the KQuery-parser: I will probably use the one delivered with
KLEE in the end. Building one of my own was just the result of my
excitement about parsers and getting used to the language;)

Am 11.04.13 16:44, schrieb 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.
>