!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

246 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
15 Apr 2021
@kheradmand:matrix.orgAli
In reply to @kheradmand:matrix.org

I have a K definition that gets stuck at:

 <k>
      @processDec ( metadata ingress_metadata_t ingress_metadata { .FieldValueAssignments } ) ~> ...
 </k>
…
 <headers>
      ...
      SetItem ( <header>
        <h-name>
          ingress_metadata_t
        </h-name>
        …      </header> )
        …
 </headers>

This happens with the java backend only (it does NOT get stuck with the llvm or haskell backend). The following rule should get applied (and gets applied with the llvm and haskell backends) but it does not get applied in the java backend:

rule <k> @processDec(metadata Type:Id Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

If I change <h-name> Type </h-name> to <h-name> Type2:Id </h-name>, the rule gets applied, suggesting the problem is with matching Type. But Type in the k cell and Type in the h-name cell seem to be the same thing (lines 43 and 84):

{
  "format": "KAST",
  "version": 1,
  "term": {
    "node": "KApply",
    "label": "<generatedTop>",
    "variable": false,
    "arity": 2,
    "args": [
      {
        "node": "KApply",
        "label": "<p4>",
        "variable": false,
        "arity": 29,
        "args": [
          {
            "node": "KApply",
            "label": "<k>",
            "variable": false,
            "arity": 1,
            "args": [
              {
                "node": "KApply",
                "label": "#KSequence",
                "variable": false,
                "arity": 2,
                "args": [
                  {
                    "node": "KApply",
                    "label": "@processDec(_)_P4-SEMANTICS",
                    "variable": false,
                    "arity": 1,
                    "args": [
                      {
                        "node": "KApply",
                        "label": "metadata____HEADER-SYNTAX",
                        "variable": false,
                        "arity": 3,
                        "args": [
                          {
                            "node": "KToken",
                            "sort": "Id",
                            "token": "ingress_metadata_t"
                          },
                          {
                            "node": "KToken",
                            "sort": "Id",
                            "token": "ingress_metadata"
                          },
                          {
                            "node": "KApply",
                            "label": "{_}_HEADER-SYNTAX",
                            "variable": false,
                            "arity": 1,
                            "args": [
                              {
                                "node": "KApply",
                                "label": ".List{\"'FieldValueAssignments\"}",
                                "variable": false,
                                "arity": 0,
                                "args": []
                              }
                            ]
                          }
                        ]
                      }
                    ]
                  },
…
                            "node": "KApply",
                            "label": "<header>",
                            "variable": false,
                            "arity": 3,
                            "args": [
                              {
                                "node": "KApply",
                                "label": "<h-name>",
                                "variable": false,
                                "arity": 1,
                                "args": [
                                  {
                                    "node": "KToken",
                                    "sort": "Id",
                                    "token": "ingress_metadata_t"
                                  }
                                ]
                              },

So I don’t know why it does not get applied. So far I have not managed to make a smaller example.

I am generally looking for a backend that can perform symbolic reasoning (although the above example is concrete). The haskell backend does not currently support some stuff e.g. String2Base(_, 2) and also crash during execution. My K definition used to work with k-legacy (with the java backend), that’s why I’m trying to see if I can make it work with the java backend. I was wondering if there are any other options besides these two?

Also with the java backed, what is the best way to find out why a particular rule does not get applied? E.g. any particular points in the source code that I can set a breakpoint on ?

Regarding this:
07:42:59
@kheradmand:matrix.orgAliimage.png
Download image.png
07:43:33
@kheradmand:matrix.orgAliRedacted or Malformed Event07:43:46
@kheradmand:matrix.orgAli

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, later in line 160 when it wants to evaluateConstraints, for simplifying the equality that is shown in the picture the leftHandSide (Set:choice(R__29:set)) is evaluated to a particular set item that is not equal to the rightHandSide, even though that set contains another element that is indeed equal to the rightHandSide.

Seems to me that this is a bug in the java backend, any ideas?
Not sure if the problem is using set choice (instead of say set membership) to implement the lookup in the headers cell in the following rule or it is in the implementation of set choice build in.

rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
    <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>
lookups:
1. Set:choice(R__29:Set) =? <header>(<h-name>(R_Type:HeaderTypeName),, R__0:K,, R__1:K)
2. Set:difference(R__29:Set,, HeaderCellSetItem(<header>(<h-name>(R_Type:HeaderTypeName),, R__0:K,, R__1:K))) =? R__DotVar3:Set
07:44:12
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that it picks the wrong <header> cell. I expected it to pick a header cell with <h-name>(Id(#”ingress_metadata_t”) but it picks a cell with <h-name>(Id(#"ethernet_t”). Remember the rule is:

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypename Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

07:45:48
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that it picks the wrong <header> cell. I expected it to pick a header cell with <h-name>(Id(#”ingress_metadata_t”) but it picks a cell with <h-name>(Id(#"ethernet_t”). Remember the rule is:

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

07:46:04
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that the substitution that matches the set inside <headers> (R__29:set) captures all headers except the

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

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

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that the substitution that matches the set inside <headers> (R__29:set) captures all headers except the one that needs to be considered. (i.e. the one with <h-name>(Id(#"ipv4_t")).

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

10:06:57
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that the substitution that matches the set inside <headers> (R__29:set) captures all headers except the one that needs to be considered. (i.e. the one with <h-name>(Id(#"ingress_metadata_t")).

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

10:13:21
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that the substitution that matches the set inside <headers> (R__29:set) captures all headers except the one that needs to be considered. (i.e. the one with <h-name>(Id(#"ingress_metadata_t")))

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

10:13:33
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that the substitution that matches the set inside <headers> (R__29:set) captures all headers except the one that needs to be considered (i.e. the one with <h-name>(Id(#"ingress_metadata_t"))).

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

10:13:39
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, the constraints for that match seem not to be correct. It seems that the substitution that matches the set inside <headers> (R__29:set) captures all set items except the one that needs to be considered (i.e. the one with <h-name>(Id(#"ingress_metadata_t"))).

syntax HeaderTypeName ::= Id
rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
     <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>

Seems to me that this is a bug in the java backend, any ideas?

10:16:09
@kheradmand:matrix.orgAliRedacted or Malformed Event10:23:03
@kheradmand:matrix.orgAliRedacted or Malformed Event10:23:12
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, later in line 160 when it wants to evaluateConstraints, for simplifying the equality that is shown in the picture the leftHandSide (Set:choice(R__29:set)) is evaluated to a particular set item that is not equal to the rightHandSide, even though that set contains another element that is indeed equal to the rightHandSide.

Seems to me that this is a bug in the java backend, any ideas?

10:39:11
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, later in line 160 when it wants to evaluateConstraints, for simplifying the equality that is shown in the picture the leftHandSide (Set:choice(R__29:set)) is evaluated to a particular set item that is not equal to the rightHandSide, even though that set contains another element that is indeed equal to the rightHandSide.

Seems to me that this is a bug in the java backend, any ideas?

10:40:58
@kheradmand:matrix.orgAliimage.png
Download image.png
10:41:53
@kheradmand:matrix.orgAliRedacted or Malformed Event10:47:09
@kheradmand:matrix.orgAliimage.png
Download image.png
10:49:50
@kheradmand:matrix.orgAli *

I have tried to debug the source code for the aforementioned problem.
So far it seems that the correct rule gets selected after the call to matchWithAutomaton in FastRuleMatcher.java:129, however, later in line 160 when it wants to evaluateConstraints, for simplifying the equality that is shown in the picture the leftHandSide (Set:choice(R__29:set)) is evaluated to a particular set item that is not equal to the rightHandSide, even though that set contains another element that is indeed equal to the rightHandSide.

Seems to me that this is a bug in the java backend, any ideas?
Not sure if the problem is using set choice (instead of say set membership) to implement the lookup in the headers cell in the following rule or it is in the implementation of set choice build in.

rule <k> @processDec(metadata Type:HeaderTypeName Name:InstanceName { Asgn:FieldValueAssignments } ) => @initInstance(Name,@getAssignmentsAsMap(Asgn, .Map)) ... </k>
    <headers>  <header>  <h-name> Type </h-name> ... </header> ... </headers>
lookups:
1. Set:choice(R__29:Set) =? <header>(<h-name>(R_Type:HeaderTypeName),, R__0:K,, R__1:K)
2. Set:difference(R__29:Set,, HeaderCellSetItem(<header>(<h-name>(R_Type:HeaderTypeName),, R__0:K,, R__1:K))) =? R__DotVar3:Set
12:19:47
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth For historical reasons, DOMAINS does not import FLOAT as I recall. 17:28:41
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth I mean, I don't think in practice anyone has been using any bases higher than 16 19:05:07
@_slack_runtimeverification_U5GE6G57G:matrix.orgdwight.guth so if you chose to only implement bases 2-16 at this time, it probably would suffice for anything currently being done in practice 19:05:28
16 Apr 2021
@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>
06:29:59
@kheradmand:matrix.orgAli *

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

<generatedTop>
  <k>
    y2
  </k>
  <ts>
    SetItem ( <t>
      <name>
        y1
      </name>
    </t> )
    SetItem ( <t>
      <name>
        y2
      </name>
    </t> )
  </ts>
</generatedTop>
06:31:23
@kheradmand:matrix.orgAli *

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

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 ::= "SUCESS"
    rule <k> I:Y => SUCESS </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>
06:32:27
@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 ::= "SUCESS"
    rule <k> I:Y => SUCESS </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>
06:32:41
@kunwangyml:matrix.orgkunwangymlRedacted or Malformed Event06:59:27
@kunwangyml:matrix.orgkunwangymlimage.png
Download image.png
07:00:22
@kunwangyml:matrix.orgkunwangymlimage.png
Download image.png
07:01:27

Show newer messages


Back to Room List