kquery: versions. version-specifier and version labels

[Jonathan Koch]

Hallo everybody,

I am building a parser to reconstruct the AST for KQuery expressions.
However, I ran into 3 points in the language definition that are not
quite clear to me.

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

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?

On the KQuery reference page "version" is never used explicitly on any
RHS of a syntax-rule. Maybe this is already covered by the questions
above or maybe I just missed something.

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 ]

I would highly appreciate some help. Other than that: I really love
KLEE, it is a truly amazing tool you built.

Best regards,
Jonathan

[Cristian Cadar]

Hi Jonathan,

I only skimmed through your message, but may I first ask why you need to
build another parser for the KQuery language? We already have one, part
of the Kleaver tool. Couldn't you use/extend it in your work?

Best wishes,
Cristian

Post by Jonathan Koch
Hallo everybody,
I am building a parser to reconstruct the AST for KQuery expressions.
However, I ran into 3 points in the language definition that are not
quite clear to me.
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
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?
On the KQuery reference page "version" is never used explicitly on any
RHS of a syntax-rule. Maybe this is already covered by the questions
above or maybe I just missed something.
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 ]
I would highly appreciate some help. Other than that: I really love
KLEE, it is a truly amazing tool you built.
Best regards,
Jonathan
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Daniel Liew]

Post by Jonathan Koch
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

Post by Jonathan Koch
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.

Post by Jonathan Koch
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.

[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;)

Post by Jonathan Koch

Post by Jonathan Koch
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

version = identifier ":" version

Post by Jonathan Koch
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.

Post by Jonathan Koch
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.