K-user mailing list

[<daparpon AT dsic.upv.es>]

Hi, Dorel! I tried it but the term isBool(<my expression>) does not rewrite to
anything and gets stuck in that point. What might be happening? The pre-
processing that I apply to that <my expression> is to change all occurrences
of #symInt(X:Id) into another term defined in my language as:

syntax Int      ::= "smtIntVariable" "(" Id ")"

The purpose of this substitution is that I do not want those symbolic integers
to be declared in the call to Z3 as integer constants; instead, they should be
declared as existentially quantified variables in an "exists" clause. However,
all "#symInt" elements in a boolean expression are extracted and declared
automatically while building up the Z3 query. Is it possible that K does not
treat the "smtIntVariable" terms as actual Ints, and consequently cannot infer
a Bool type to the whole (supposed boolean) expression?

Best regards,
Daniel

--------------------------------------------------------------------------------------------------
2017-06-02 10:10 GMT+03:00 <dlucanu AT info.uaic.ro>:

Hi Daniel,

regarding the testing of sorts, did you try "is<sort>" predicate?
Here is a simple example using "isBool":

module TEST-SYNTAX
syntax Exp ::= "init" | "done"
| cfg(Exp, K)
endmodule

module TEST

imports TEST-SYNTAX
rule cfg(init, B) => done requires isBool(B)

endmodule

K 3.4 gives the following final configuration for the input "cfg(init,
false)":
$ ../bin/krun ex.text
<k>
done
</k>

I hope this help you.
Best regards,
Dorel

On 01/06/2017 14:28,
daparpon AT dsic.upv.es
wrote:

    Hi Christos, and thanks! I think I have already figured it out, though. As
you
    say, it works perfectly by dealing with Strings instead of SmtResponses,
but
    it seems that this happens because the whole infrastructure to communicate
    with Z3 is built-in and compiled in the prelude, at least in K 3.4. Which
    means that it is not necessary to require nor import the file "smt.k" and
the
    modules "SMT-HOOKS" or "SMT-SYNTAX-HOOKS". I tried it and performs as
    expected.

    However, you highlight an interesting issue in your Solution 2 (which I
also
    found while transferring to my setting), regarding sorts. As far as I
know,
    the subexpression (XXX):Sort is not a casting, but a restriction to the
    applicability of the rule; it means that the rule will only be applied if
the
    restricted term (usually a variable) belongs to that sort. I do not know
how
    to ask K for the actual sort of an expression, and it would be interesting
to
    me, since my language does not call Z3 correctly because one of its
arguments
    is not inferred to be Bool, although it should be. If anyone knows how to
    obtain or force the sort of an expression, can inform to us, please? It
would
    be really appreciated.

    Finally, I add myself to the claim regarding getModel. In my case it is
not
    just that getModel does not do anything, but I even get a syntax error
while
    compiling:

    [Error] Critical: Parse error: Syntax error near unexpected character 'M'

    I have a hypothesis for this. In your case it may compile because your
module
    imports "SMT-SYNTAX-HOOKS" in "smt.k", which declares both getModel and
    checkSat (the latter overloading the "checkSat(Bool) -> String" profile
    already defined), but gives no meaning to them. In my case I am purely
relying
    on the infrastructure compiled in the prelude, and most likely getModel
has
    not been defined there. There is indeed a rule for getModel in the "SMT-
HOOKS"
    module, but trying to import it takes us back to square one, getting some
    syntax errors during compilation. Can you please try to import "SMT-HOOKS"
and
    compile, to check whether it works for you or whether you get the same
errors?

    Best regards,
    Daniel


--------------------------------------------------------------------------------------------------
    2017-05-31 19:26 GMT+03:00 <c.kloukinas AT gmail.com>:

    Hi, here are two ways I managed to get it to work (at least what I _think_
you
    were trying to achieve).
    I think the problem has something to do with sorts (I'm total new to K, so
I'm
    not very sure of what's going on).
    I also think that you should avoid SmtResponse and use String directly.

    - Solution 1:

    module TEMP
    imports SMT-SYNTAX-HOOKS
    syntax String ::= "SMTR2String" "(" String ")" // [function]
    rule SMTR2String("sat") => "SATISFIABLE" [structural]
    rule SMTR2String("unsat") => "NOT SATISFIABLE" [structural]
    configuration <k> SMTR2String(checkSat(#symInt(1) >Int #symInt(2))) </k>
    endmodule

    - Solution 2:

    module TEMP
    imports SMT-SYNTAX-HOOKS
    // configuration <k> checkSat(notBool(notBool(#symInt(1) >Int
#symInt(2)))) </
    k> // alternative configuration
    configuration <k> checkSat((#symInt(1) >Int #symInt(2)):Bool) </k> // Is
    (XXX):Bool casting XXX as Bool? Not sure...
    rule "sat" => "SATISFIABLE"
    rule "unsat" => "NOT SATISFIABLE"
    endmodule


    Now, if someone knows how to get a model out from the SMT solver, that'd
be
    great!
    I've tried to use getModel instead of checkSat but it doesn't seem to be
doing
    anything:

    require "builtins/smt.k"
    module TEMP-MODEL
    imports SMT-SYNTAX-HOOKS
    // configuration <k> checkSat( 10 <=Int #symInt(1) andBool #symInt(1)
<=Int
    12 ) </k> // reduces to "sat"
    configuration <k> getModel( 10 <=Int #symInt(1) andBool #symInt(1) <=Int
12 )
    </k>
    endmodule

    Best,
    Christos

    On 15/05/2017 11:53,
    daparpon AT dsic.upv.es
    wrote:

    I tried, but the result remains the same:

    require "builtins/smt.k"

    module TEMP
    imports SMT-SYNTAX-HOOKS

    syntax String ::= SMTR2String(SmtResponse)

    rule SMTR2String(sat) => "SATISFIABLE"
    [structural]
    rule SMTR2String(unsat) => "NOT SATISFIABLE"
    [structural]

    configuration <k> SMTR2String(checkSat(#symInt(1) >Int #symInt(2))) </k>

    endmodule

    wifialu34-51:SMT Test ELP$ kompile temp.k --backend symbolic
    wifialu34-51:SMT Test ELP$ krun -cPC=true --search
    Search results:

    Solution 1:
    <k>
    SMTR2String ( checkSat ( #symInt(1) >Int #symInt(2) ) )
    </k>
    <path-condition>
    true
    </path-condition>

    Daniel



--------------------------------------------------------------------------------------------------
    2017-05-15 11:09 GMT+03:00 <andrei.arusoaie AT gmail.com>:

    I believe that K finds the rules in the SMT-HOOKS but the other rules
    imported
    from K builtins apply first and reduce the _expression_ "4 >Int 4" before
    sending it to the solver.
    Can you try to use a symbolic value instead of 4?

    Andrei

    2017-05-15 10:40 GMT+03:00 <daparpon AT dsic.upv.es>:

    Yes, it does, but then functions and non-terminals from SMT-HOOKS such as
    "checkSat" stop working. For instance, kompiling and krunning the same
    example
    K spec as before...

    require "builtins/smt.k"

    module TEMP
    imports SMT-SYNTAX-HOOKS

    syntax String ::= SMTR2String(SmtResponse)

    rule SMTR2String(sat) =>
    "SATISFIABLE" [structural]
    rule SMTR2String(unsat) => "NOT
    SATISFIABLE" [structural]

    configuration <k> SMTR2String(checkSat(4 >Int 4)) </k>

    endmodule

    ... results in the following output:

    wifialu34-51:SMT Test ELP$ krun
    <k>
    SMTR2String ( checkSat ( false ) )
    </k>

    To test further cases, I tried making "SMTR2String" a [strict]
    construction,
    and then I got the following result:

    wifialu34-51:SMT Test ELP$ krun
    <k>
    checkSat ( false ) ~> SMTR2String ( HOLE )
    </k>

    So it seems that the execution gets stuck because K cannot find any rules
    that
    give semantics to "checkSat", which are in the file SMT-HOOKS...




--------------------------------------------------------------------------------------------------
    2017-05-15 07:57 GMT+03:00 <andrei.arusoaie AT gmail.com>:

    I think you should import SMT-SYTNAX-HOOKS. Does it compile?
    Andrei

    2017-05-12 11:39 GMT+03:00 <daparpon AT dsic.upv.es>:

    Thanks! I tried your example and works for me as well. However, it
    seems
    that
    the problem arises when explicitly manipulating elements of sort
    SmtResponse.
    For instance, I modified the example introducing a function that
    takes
    a
    SmtResponse parameter, and now I get an error saying that the
    SmtResponse
    sort
    is undefined:

    require "builtins/smt.k"

    module TEMP

    syntax String ::= SMTR2String(SmtResponse)

    rule SMTR2String(sat) =>
    "SATISFIABLE" [structural]
    rule SMTR2String(unsat) => "NOT
    SATISFIABLE" [structural]

    configuration <k> SMTR2String(checkSat(4 >Int 4)) </k>

    endmodule

    wifialu32-238:SMT Test ELP$ kompile temp.k
    [Error] Compiler: Undefined sort SmtResponse
    File: /Users/ELP/Desktop/KTests/SMT Test/temp.k
    Location: (5,33,5,43)
    Compilation Phase: class
    org.kframework.compile.checks.CheckSyntaxDecl

    I tried to solve it by adding "imports SMT-HOOKS" below the "module
    TEMP"
    declaration, but then the error that I reported in previous messages
    returned:

    wifialu32-238:SMT Test ELP$ kompile temp.k
    [Warning] Compiler: Associativity attribute should only be assigned
    to
    binary
    infix production.

    File: /Users/ELP/Documents/k/include/builtins/fol.k
    Location: (14,18,14,57)
    Compilation Phase: class
    org.kframework.compile.checks.CheckSyntaxDecl
    [Warning] Compiler: Associativity attribute should only be assigned
    to
    binary
    infix production.

    File: /Users/ELP/Documents/k/include/builtins/fol.k
    Location: (15,18,15,57)
    Compilation Phase: class
    org.kframework.compile.checks.CheckSyntaxDecl
    [Error] Critical: Parse error: Syntax error near unexpected character
    'y'
    File: /Users/ELP/Documents/k/include/builtins/smt.k
    Location: (17,16,17,16)

    Thanks again and sorry for the inconveniencies,
    Daniel





--------------------------------------------------------------------------------------------------
    2017-05-11 16:00 GMT+03:00 <andrei.arusoaie AT gmail.com>:

    I’ve done the following experiment (please note the commented line no
    4 in
    smt.k) and it works for me:

    [andrei]-$ cat /home/andrei/Downloads/k/include/builtins/smt.k
    // Copyright (c) 2012-2014 K Team. All Rights Reserved.
    require "builtins/builtins.k"
    require "builtins/fol.k"
    // require "builtins/array-symbolic.k"

    module SMTLIB-CONVERSION
    imports BUILTIN-HOOKS
    imports FOL
    ...


    [andrei]-$ cat temp.k
    require "builtins/smt.k"

    module TEMP

    configuration <k> checkSat(4 >Int 4) </k>

    endmodule
    [andrei]-$ ./kompile --version
    K-framework version 3.4.
    Git Revision: 08c9271
    Build date: Tue Aug 26 13:56:56 PDT 2014

    [andrei]-$ ./kompile temp.k

    [andrei]-$ ./krun
    <k>
    "unsat"
    </k>

    Andrei
    ​

    2017-05-11 15:19 GMT+03:00 Andrei Arusoaie <andrei.arusoaie AT
    gmail.com>:

    Hi,

    Can you attach a simple K file which can reproduce the bug?
    Andrei

    2017-05-11 10:27 GMT+03:00 <daparpon AT dsic.upv.es>:

    Hi, Andrei.

    Please can you give me any recommendations regarding this
    problem?
    Since I'm
    not able to make K interact with the SMT solver, I'm stuck in
    this
    phase of my
    research.

    Thanks in advance,
    Daniel






--------------------------------------------------------------------------------------------------
    2017-04-28 13:25 GMT+03:00 <daparpon AT dsic.upv.es>:

    Nope, it does not. I tried commenting the "require array-
    symbolic.k"
    clause
    and I obtained other kompiling errors and warnings,
    specifically
    the
    following
    ones:

    [Warning] Compiler: Associativity attribute should only be
    assigned to
    binary
    infix production.

    File: /Users/ELP/Documents/k/include/builtins/fol.k
    Location: (14,18,14,57)
    Compilation Phase: class
    org.kframework.compile.checks.CheckSyntaxDecl

    [Warning] Compiler: Associativity attribute should only be
    assigned to
    binary
    infix production.

    File: /Users/ELP/Documents/k/include/builtins/fol.k
    Location: (15,18,15,57)
    Compilation Phase: class
    org.kframework.compile.checks.CheckSyntaxDecl

    [Error] Critical: Parse error: Syntax error near unexpected
    character
    'y'
    File: /Users/ELP/Documents/k/include/builtins/smt.k
    Location: (17,16,17,16)

    To be more precise, the line which the error refers to is:

    rule Smtlib(symBool(I:Int)) => "var" +String Int2String(I)

    and the location reference points to the 'y' in
    "symBool(I:Int)".

    Daniel






--------------------------------------------------------------------------------------------------
    2017-04-28 13:16 GMT+03:00 <andrei.arusoaie AT gmail.com>:

    That's weird...
    Anyway, I think you can comment the line which include array-
    symbolic.k from /
    k/include/builtins/smt.k.
    Does it work if you do that?


    2017-04-28 13:12 GMT+03:00 <daparpon AT dsic.upv.es>:

    Hi! I tried to import the module you refer to (and insert the
    proper "
    require
    "builtins/smt.k" " clause) in order to use the checkSat
    function
    in my
    language. However, when I kompile the resulting
    specification,
    I
    get
    the
    following error message:

    [Error] Critical: Could not find 'required' file: builtins/
    array-
    symbolic.k
    File: <filepath to K>/k/include/builtins/smt.k
    Location: (4,1,4,35)

    I have looked for the "array-symbolic.k" file in both my file
    system
    and
    previous distributions of the K Framework, but I could not
    find it
    anywhere.
    How can I solve this dependency and work with the "smt.k"
    file?

    Thanks in advance,
    Daniel

    From: Andrei Arusoaie <andrei.arusoaie AT gmail.com>
    Date: 2017-04-12 19:47 GMT+03:00
    Subject: Re: [[K-user] ] Calling SMT Solver from K
    specification
    To: daparpon AT dsic.upv.es


    Hi Daniel,

    If you’re using K-3.4 then you can take a look at k/include/
    builtins/
    smt.k,
    specifically in module:

    module SMT-SYNTAX-HOOKS

    syntax SmtResponse ::= "sat"
    | "unsat"
    | "unknown"
    | "model" "(" Map ")"

    syntax SmtResponse ::= "checkSat" "(" K ")" [function]
    | "getModel" "(" K ")" [function]

    syntax Bool ::= SmtResponse "=/=" SmtResponse
    | SmtResponse "==" SmtResponse
    endmodule

    I think checkSat is what you’re looking for. Make sure you
    pass a
    Bool
    to
    it.
    If you need more, you can extend the module to translate
    whatever
    exp
    to
    SMTLib as we implicitly did for ints and bools (check the
    entire
    smt.k
    file
    for details).

    Andrei A.
    ​

    2017-04-12 17:07 GMT+03:00 <daparpon AT dsic.upv.es>:

    What I need to do is to compare two symbolic execution
    states,
    S1
    and
    S2,
    which respectively contain the path conditions PC1 and PC2.
    The
    comparison
    is
    simply done by checking whether the implication PC1 => PC2
    holds.
    For
    instance, this is a valid implication, where each ?vi is a
    symbolic
    value

    (?v1 < ?v3 ^ ?v3 < ?v2) => (?v1 <= ?v2)

    Since path conditions are logical expressions involving
    symbolic
    data,
    the
    implication cannot be solved by means of K's boolean
    operators
    but
    I
    need
    to
    delegate this problem to a SAT/SMT Solver.

    How can I send the constraint to the SAT solver and get the
    solver
    verdict
    in
    return?

    I am still using K 3.4 since I need to read the
    path-condition
    cell
    during
    symbolic execution, while K 4.0 does not have this capability
    available
    yet.

    Thanks a lot and sorry for the inconveniencies. Best regards,
    Daniel
    ________________________________________
    From:
    yzhng173 AT illinois.edu

    [yzhng173 AT illinois.edu]
    Sent: Tuesday, April 11, 2017 9:16 AM
    To:
    k-user AT lists.cs.illinois.edu
    Subject: RE: [[K-user] ] Calling SMT Solver from K
    specification

    Hi Daniel,

    The current Java backend is using Z3 in the symbolic
    execution
    engine
    internally and it is not exposed to the user. Could you
    please
    tell us
    more
    specifically about your use cases?

    Best,

    Yi
    ________________________________________
    From:
    daparpon AT dsic.upv.es

    [daparpon AT dsic.upv.es]
    Sent: Tuesday, April 11, 2017 4:01 AM
    To:
    k-user AT lists.cs.illinois.edu
    Subject: [[K-user] ] Calling SMT Solver from K specification

    Hi! I am implementing a part of my K language specification
    which
    needs to
    check a boolean formula for satisfiability/validity. How can
    I
    do
    that
    in
    K?
    Are there any built-in commands or terms that allow K rules
    to
    communicate
    with an SMT Solver, for instance Z3? In that case, which are
    they
    (or
    where
    can I find more information about them)?

    Thanks in advance,
    Daniel