| 15 Nov 2019 |
| 14:24:14 |  everett.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 |  Andreas Sthlbr | Yepp.. LLVM. I already used lldb for K. But it is not that convenient. |
| 14:24:35 | everett.hildenbrandt | That's because the Map sort comes with the implicit assumption that keys are distinct. |
| 14:24:57 | everett.hildenbrandt | It is a bit hard to use. |
| 14:25:02 | everett.hildenbrandt | Another option is to do krun, but pass in depth bounds. |
| 14:25:17 | everett.hildenbrandt | So krun --depth N |
| 14:25:20 | everett.hildenbrandt | And find the N where you think your rule should be applying. |
| 14:25:26 | everett.hildenbrandt | (then inspect the configuration) |
| 14:25:35 | Andreas Sthlbr | I already did that |
| 14:25:41 | Andreas Sthlbr | and the rule is not applied ;) |
| 14:25:49 | Andreas Sthlbr | I also tried it on a smaller program |
| 14:25:54 | Andreas Sthlbr | with a less complex config |
| 14:26:00 | Andreas Sthlbr | and there, the rule applied |
| 14:26:21 | Andreas Sthlbr | The rule was only rule .SomeList => . |
| 14:26:46 | Andreas Sthlbr | There is a cell <k> .SomeList </k>, but the rule is not applied |
| 14:27:05 | Andreas Sthlbr | I would have expected to get a final cell <k> . </k> |
| 14:27:49 | Andreas Sthlbr | Similar to the IMP++ example, there are several <k>-Cells in a Configuration |
| 14:29:05 | Andreas Sthlbr | This 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 | Andreas Sthlbr | Which backend would you recommend in terms of stability and testedness? |
| 15:20:44 | Andreas Sthlbr | I 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 | Andreas Sthlbr: I'm surprised that rule doesn't apply. |
| 16:13:17 | ehildenb | Can I see where .SomeList is defined? |
| 16:13:22 | ehildenb | (the syntax declarations) |
| 16:13:42 | ehildenb | Also, try rule <k> .SomeList => . ... </k> (instead of rule .SomeList => .) |
| 16:13:56 | ehildenb | In general, I personally consider it bad practice to omit the <k> ... </k> (even though K allows you to do this). |
| 16:26:04 |  demi | 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 | 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 | (basically so that the symbolic execution engine can just assume it, instead of having to learn it) |
| 19:13:55 | |  niels joined the room. |
| 16 Nov 2019 |
| 23:18:52 |  rikard.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
(0)
[Warning] Compiler: User specified configuration variable $PGM which does not
exist.
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
configuration
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] ]
endmodule
Kompiling with LLVM backend:
kompile --backend llvm polymer.k && krun input.ply --debug
The input file can be any sequence of letters. |
