The K Framework User Group

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

Load older messages

Timestamp Message
15 Nov 2019
14:24:14@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt @demi if you have a rule which does this rule k doSomething KEY1 KEY2 => doneSomething ... /k map ... KEY1 ,-> VALUE1 KEY2 ,-> VALUE2 ... /map and run it on doSomething 4 4, for example, it will not apply the rule.
14:24:18@asteel:matrix.orgAndreas SthlbrYepp.. LLVM. I already used lldb for K. But it is not that convenient.
14:24:35@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt That's because the Map sort comes with the implicit assumption that keys are distinct.
14:24:57@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt It is a bit hard to use.
14:25:02@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Another option is to do krun, but pass in depth bounds.
14:25:17@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt So krun --depth N
14:25:20@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt And find the N where you think your rule should be applying.
14:25:26@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt (then inspect the configuration)
14:25:35@asteel:matrix.orgAndreas SthlbrI already did that
14:25:41@asteel:matrix.orgAndreas Sthlbrand the rule is not applied ;)
14:25:49@asteel:matrix.orgAndreas SthlbrI also tried it on a smaller program
14:25:54@asteel:matrix.orgAndreas Sthlbrwith a less complex config
14:26:00@asteel:matrix.orgAndreas Sthlbrand there, the rule applied
14:26:21@asteel:matrix.orgAndreas Sthlbr The rule was only rule .SomeList => .
14:26:46@asteel:matrix.orgAndreas Sthlbr There is a cell <k> .SomeList </k>, but the rule is not applied
14:27:05@asteel:matrix.orgAndreas Sthlbr I would have expected to get a final cell <k> . </k>
14:27:49@asteel:matrix.orgAndreas Sthlbr Similar to the IMP++ example, there are several <k>-Cells in a Configuration
14:29:05@asteel:matrix.orgAndreas SthlbrThis list construct is only one example. The rewriting is also stopped for other k-cells, where still some rules would be applicable
14:36:51@asteel:matrix.orgAndreas SthlbrWhich backend would you recommend in terms of stability and testedness?
15:20:44@asteel:matrix.orgAndreas SthlbrI am open for any hints to investigate the reason why the rewrite stops for certain cells while there still would be applicable rules.
16:13:11@ehildenb:matrix.orgehildenb Andreas Sthlbr: I'm surprised that rule doesn't apply.
16:13:17@ehildenb:matrix.orgehildenb Can I see where .SomeList is defined?
16:13:22@ehildenb:matrix.orgehildenb(the syntax declarations)
16:13:42@ehildenb:matrix.orgehildenb Also, try rule <k> .SomeList => . ... </k> (instead of rule .SomeList => .)
16:13:56@ehildenb:matrix.orgehildenb In general, I personally consider it bad practice to omit the <k> ... </k> (even though K allows you to do this).
In reply to @_slack_runtimeverification_U8T2RJ802:matrix.org
@demi if you have a rule which does this rule k doSomething KEY1 KEY2 => doneSomething ... /k map ... KEY1 ,-> VALUE1 KEY2 ,-> VALUE2 ... /map and run it on doSomething 4 4, for example, it will not apply the rule.
Is it okay to rely on this?
17:11:46@ehildenb:matrix.orgehildenb Yes. the syntax KEY1 |-> VALUE1 KEY2 |-> VALUE2 comes with the assumption that KEY1 =/=K KEY2. But I would still add that assumption to your requires clause for explicitness.
17:12:04@ehildenb:matrix.orgehildenb(basically so that the symbolic execution engine can just assume it, instead of having to learn it)
19:13:55@niels:chat.datenburg.orgniels joined the room.
16 Nov 2019
23:18:52@_slack_runtimeverification_UFTN1UV4H:matrix.orgrikard.hjort I'm playing around with some general purpose programming in K and I ran into the following error:
java.lang.IndexOutOfBoundsException: 0
        at scala.collection.LinearSeqOptimized.apply(LinearSeqOptimized.scala:63)
        at scala.collection.LinearSeqOptimized.apply$(LinearSeqOptimized.scala:61)
        at scala.collection.immutable.List.apply(List.scala:86)
        at org.kframework.definition.Production.nonterminal(outer.scala:479)
        at org.kframework.compile.AddSortInjections.visitChildren(AddSortInjections.java:197)
        at org.kframework.compile.AddSortInjections.internalAddSortInjections(AddSortInjections.java:125)
        at org.kframework.compile.AddSortInjections.addSortInjections(AddSortInjections.java:86)
        at org.kframework.compile.AddSortInjections.addInjections(AddSortInjections.java:80)
        at org.kframework.backend.llvm.LLVMRewriter$1.execute(LLVMRewriter.java:79)
        at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:69)
        at org.kframework.krun.KRun.run(KRun.java:87)
        at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:93)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:59)
        at org.kframework.main.Main.runApplication(Main.java:119)
        at org.kframework.main.Main.runApplication(Main.java:108)
        at org.kframework.main.Main.main(Main.java:54)
[Error] Internal: Uncaught exception thrown of type IndexOutOfBoundsException
[Warning] Compiler: User specified configuration variable $PGM which does not
I would assume the error is caused by the warning: I just don't get under which circumstances $PGM wouldn't exist. Minimal example:
module POLYMER
   imports DOMAINS
   imports BYTES-HOOKED

     k  $PGM:Polymer  /k 
     result  String2Bytes("")  /result 

   syntax Polymer ::= r"\\$[a-zA-Z]+" [token]
   rule  k  BYTES => substrBytes(BYTES, 1, lengthBytes(BYTES)) ...  /k 
         result  RES => RES[ lengthBytes(RES)  - BYTES[0] ] 

Kompiling with LLVM backend:
kompile --backend llvm polymer.k && krun input.ply --debug
The input file can be any sequence of letters.

There are no newer messages yet.

Back to Room List