!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

243 Members
The K Framework (kframework.org) and its applications to smart contracts.  EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics45 Servers

Load older messages


SenderMessageTime
16 Apr 2021
@kunwangyml:matrix.orgkunwangymlWhy it ask for a Statement😂07:02:06
@kunwangyml:matrix.orgkunwangymlimage.png
Download image.png
07:04:03
@kheradmand:matrix.orgAli *

Here is a small self-contained example that demonstrates the likely bug mentioned above in the java backend:

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts>
        <t multiplicity="*" type="Set">
            <name> .K </name>
        </t>
    </ts>

    syntax Y ::= "y1" | "y2"
    rule <k> _:X => y2 </k>
         <ts>
            (.Bag => <t> <name> y1 </name> </t>)
            (.Bag => <t> <name> y2 </name> </t>)
            ...
         </ts>

    syntax KItem ::= "SUCCESS"
    rule <k> I:Y => SUCCESS </k>
         <ts>
            <t> <name> I </name> </t>
            ...
         </ts>
endmodule

The execution gets stuck at:

<generatedTop>
  <k>
    y2
  </k>
  <ts>
    SetItem ( <t>
      <name>
        y1
      </name>
    </t> )
    SetItem ( <t>
      <name>
        y2
      </name>
    </t> )
  </ts>
</generatedTop>
07:52:55
@kheradmand:matrix.orgAliQuestion: is the java backend deprecated? I am encountering other bugs/problems even on simple examples. Was wondering if I should abandon that backend or not. 10:44:20
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Yes, we are not maintaining the Java backend at all anymore. 12:41:13
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt It will remain around while there are still large semantics working with it. 12:41:31
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But it will not receive anything but the simplest of updates. 12:41:44
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Please switch to the haskell backend. 12:41:51
17 Apr 2021
@kheradmand:matrix.orgAliFollowup: Are all the features supported by the java backend already implemented in the haskell backend, if not, I was wondering what is missing. E.g. seems like keq is only supported with the java backend.08:18:52
@kheradmand:matrix.orgAli * Followup: Are all the features supported by the java backend already implemented in the haskell backend, if not, I was wondering what is missing. E.g. seems like keq is only supported with the java backend.08:29:58
@kheradmand:matrix.orgAli

Can someone kindly explain the meaning of the output of search running with the haskel backend. Does it just say whether the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).

10:34:20
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }
10:34:53
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint.

10:44:30
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes show the condition on ?L and sometimes doesn't)

10:47:01
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't)

10:47:18
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain all conditions, it is kprint that picks what to display. So more concretely I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).

10:51:04
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output running in the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).

11:06:40
18 Apr 2021
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output of search running with the haskel backend. Does it just say the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).

07:00:32
19 Apr 2021
@kheradmand:matrix.orgAli *

Can someone kindly explain the meaning of the output of search running with the haskel backend. Does it just say whether the pattern is reachable or not or does it give the conditions for the pattern to be reachable. E.g. for the following

module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
    <k> $PGM:X </k>
    <ts> .K </ts>

    rule <k> _:X => .K </k>
         <ts> _ => ?L:List </ts>

    syntax KItem ::= "o1" | "o2" | "o3" | "o4"
    rule <k> .K => o1 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o2 </k>
         <ts> ListItem(10) </ts>

    rule <k> .K => o3 </k>
         <ts> ListItem(20) ListItem(30) </ts>


endmodule

if I run krun x --search --pattern "<k> o1 </k>” I get

#TOP

Now if I run krun x --search --pattern "<k> I:KItem </k>” I get

{
    I:KItem
  #Equals
    o3
  }
#Or
  {
    I:KItem
  #Equals
    o1
  }
#Or
  {
    I:KItem
  #Equals
    o2
  }

And for krun x --search --pattern "<k> I:K </k>” ,

    #Not ( {
      ?L:List
    #Equals
      ListItem ( 10 )
    } )
  #And
    #Not ( {
      ?L:List
    #Equals
      ListItem ( 20 )
      ListItem ( 30 )
    } )
  #And
    {
      I:K
    #Equals
      .
    }
#Or
  {
    I:K
  #Equals
    o1 ~> .
  }
#Or
  {
    I:K
  #Equals
    o2 ~> .
  }
#Or
  {
    I:K
  #Equals
    o3 ~> .
  }

In any case result.kore seems to contain some conditions, it is kprint that picks what to display. So I was wondering what is the logic behind selecting what to display in kprint (e.g. why it sometimes shows the condition on ?L and sometimes doesn't).

07:33:50
@kheradmand:matrix.orgAli

Question: is the following a bug or an expected behavior? :


module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
        <k> $PGM:X </k>
        <ts> .K </ts>

    syntax A ::= "a1" | "a2" | "a3"
    rule <k> _:X => .K </k>
         <ts> _ => ?I:A </ts>

    syntax O ::= "o1" | "o2" | "o3" | "o4"

    rule <k> .K => #check(Ts) </k>
         <ts> Ts:A </ts>

    syntax O ::= #check(A) [function, functional, smtlib(check)]
    rule #check(a1) => o1 [smt-lemma]
    rule #check(a2) => o2 [smt-lemma]
    rule #check(a3) => o3 [smt-lemma]


endmodule
$ kompile --backend haskell test.k --syntax-module TEST-SYNTAX --main-module TEST
$ krun x —search —pattern “<k> o4 </k> 
{
  o4
#Equals
  #check ( ?I:A )
}

Shouldn’t it give “#Bottom” as output ?

11:22:47
@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort 5GE6G57G Is it safe to do reverse lookups on maps through matching? As in: ``` k foo(VAL) => KEY ... /k m ... KEY |-> VAL ... /m 12:23:37
@kheradmand:matrix.orgAli *

Question: is the following a bug or an expected behavior? :


module TEST-SYNTAX
imports ID
    syntax X ::= "x"
endmodule

module TEST
imports DOMAINS
imports TEST-SYNTAX

    configuration
        <k> $PGM:X </k>
        <ts> .K </ts>

    syntax A ::= "a1" | "a2" | "a3"
    rule <k> _:X => .K </k>
         <ts> _ => ?I:A </ts>

    syntax O ::= "o1" | "o2" | "o3" | "o4"

    rule <k> .K => #check(Ts) </k>
         <ts> Ts:A </ts>

    syntax O ::= #check(A) [function, functional, smtlib(check)]
    rule #check(a1) => o1 [smt-lemma]
    rule #check(a2) => o2 [smt-lemma]
    rule #check(a3) => o3 [smt-lemma]


endmodule
$ kompile --backend haskell test.k --syntax-module TEST-SYNTAX --main-module TEST
$ krun x —search —pattern “<k> o4 </k> 
{
  o4
#Equals
  #check ( ?I:A )
}

Shouldn’t it give “#Bottom” as output ?

12:24:05
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth I mean, in theory it's allowed, but you're going to be paying the price for a map choice rather than a deterministic lookup 14:28:59
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth It's much better to just maintain two maps if you need something like that 14:29:29
@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort In this case maintaining two maps would be a big hassle, (we are extending an existing semantics) and the maps won't be all that big. Is the map choice a very slow operation compared to direct lookup? Or is it more like the difference of iterating over the elements in a hashmap vs direct lookup? 14:49:53
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth I mean, two map lookups are 2*log(n), whereas two map choices are n^2 14:53:22
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth three map lookups are 3*log(n), 3 map choices are n^3 14:53:53
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth so it's a pretty significant difference if you nest them 14:53:59
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth if you don't nest them, then yeah, it's about what you would expect from iterating through the elements rather than a direct lookup 14:54:16
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth and by "nest" I mean they both appear in the same rule 14:55:16

There are no newer messages yet.


Back to Room List