runtimeverification / k Goto Github PK
View Code? Open in Web Editor NEWK Framework Tools 7.0
License: BSD 3-Clause "New" or "Revised" License
K Framework Tools 7.0
License: BSD 3-Clause "New" or "Revised" License
Compiled 6e240f3 on debian stretch:
Trying to kompile
a simple lambda definition gives an error.
lambda.k
module LAMBDA
imports DOMAINS
syntax Val ::= Id
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [left]
| "(" Exp ")" [bracket]
endmodule
kompile -v --debug lambda.k
gives:
Parse command line options = 41
Importing: Source(/home/dev/Lambda/./lambda.k)
Importing: Source(/home/dev/k5/k-distribution/target/release/k/include/builtin/prelude.k)
Importing: Source(/home/dev/k5/k-distribution/target/release/k/include/builtin/kast.k)
Importing: Source(/home/dev/k5/k-distribution/target/release/k/include/builtin/domains.k)
Importing: Source(/home/dev/Lambda/./lambda.k)
org.kframework.utils.errorsystem.KEMException: [Error] Compiler: Had 1 parsing errors.
at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:117)
at org.kframework.utils.errorsystem.KEMException.compilerError(KEMException.java:75)
at org.kframework.kompile.DefinitionParsing.throwExceptionIfThereAreErrors(DefinitionParsing.java:168)
at org.kframework.kompile.DefinitionParsing.resolveConfigBubbles(DefinitionParsing.java:225)
at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:158)
at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:123)
at org.kframework.kompile.Kompile.run(Kompile.java:107)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:114)
at org.kframework.main.Main.runApplication(Main.java:104)
at org.kframework.main.Main.main(Main.java:53)
[Error] Compiler: Had 1 parsing errors.
[Error] Internal: gcc returned nonzero exit code. See output for details.
[Warning] Compiler: Could not find main syntax module with name LAMBDA-SYNTAX
in definition. Use --syntax-module to specify one. Using LAMBDA as default.
Centos6.9
gcc version 7.1.0 (GCC)
When using K after commit 0c6be56 , it fails to build the newest c-semantics (0c6be5696ee8c522ac42eab9a09c95d8b111df2b
). Output:
[root@localhost src]# export CC=gcc
[root@localhost src]# cd /root/src/c-semantics/c-semantics/x86-gcc-limited-libc/src && /root/src/c-semantics/c-semantics/dist/kcc -nodefaultlibs -Xbuiltins -fno-native-compilation -shared -o /root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/lib/libc.so *.c -I .
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)
Error: Could not find or load main class org.kframework.main.BinaryToText
Translation failed (config dumped). Run kcc -d -nodefaultlibs -Xbuiltins -fno-native-compilation -shared -o /root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/lib/libc.so builtintypes.c ctype.c math.c stdlib.c string.c -I . to see commands run.
The output of running kcc -d is following:
[root@localhost src]# kcc -d -nodefaultlibs -Xbuiltins -fno-native-compilation -shared -o /root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/lib/libc.so builtintypes.c ctype.c math.c stdlib.c string.c -I .
'/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/pp' '-I' '.' '-pedantic' 'builtintypes.c' '-o' 'tmp-kcc-iyvSr1L'
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
/root/src/c-semantics/c-semantics/dist/cparser tmp-kcc-iyvSr1L --trueName 'builtintypes.c' > tmp-kcc-ld9RIal
'krun' '--output' 'binary' '--output-file' 'tmp-kcc-tZv7NuZ' '-d' '/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/c11-translation-kompiled' '-w' 'none' '--smt' 'none' '--argv' 'dummy' '--debug' '-cOPTIONS=`_Set_`(`SetItem`(`NoLink`(.KList)), `_Set_`(`SetItem`(`XBuiltins`(.KList)), `.Set`(.KList)))' '-pOPTIONS=printf %s' '-cJSON=#token("\"{\\\"suppressions\\\"\\x3a [],\\\"message_length\\\"\\x3a 80,\\\"format\\\"\\x3a \\\"Console\\\",\\\"previous_errors\\\"\\x3a [],\\\"fatal_errors\\\"\\x3a false,\\\"rv_error\\\"\\x3a \\\"\\\"}\"", "String")' '-pJSON=printf %s' '-cOBJS=.K' '-pOBJS=printf %s' '-cPGM=tmp-kcc-ld9RIal' '-pPGM=cat'
'/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/pp' '-I' '.' '-pedantic' '-pedantic' 'ctype.c' '-o' 'tmp-kcc-hLzLQA2'
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
/root/src/c-semantics/c-semantics/dist/cparser tmp-kcc-hLzLQA2 --trueName 'ctype.c' > tmp-kcc-OZa6_Dk
'krun' '--output' 'binary' '--output-file' 'tmp-kcc-GxaIDlM' '-d' '/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/c11-translation-kompiled' '-w' 'none' '--smt' 'none' '--argv' 'dummy' '--debug' '-cOPTIONS=`_Set_`(`SetItem`(`NoLink`(.KList)), `.Set`(.KList))' '-pOPTIONS=printf %s' '-cJSON=#token("\"{\\\"suppressions\\\"\\x3a [],\\\"message_length\\\"\\x3a 80,\\\"format\\\"\\x3a \\\"Console\\\",\\\"previous_errors\\\"\\x3a [],\\\"fatal_errors\\\"\\x3a false,\\\"rv_error\\\"\\x3a \\\"\\\"}\"", "String")' '-pJSON=printf %s' '-cOBJS=.K' '-pOBJS=printf %s' '-cPGM=tmp-kcc-OZa6_Dk' '-pPGM=cat'
'/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/pp' '-I' '.' '-pedantic' '-pedantic' '-pedantic' 'math.c' '-o' 'tmp-kcc-klxSZ4V'
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
/root/src/c-semantics/c-semantics/dist/cparser tmp-kcc-klxSZ4V --trueName 'math.c' > tmp-kcc-KCS3YEy
'krun' '--output' 'binary' '--output-file' 'tmp-kcc-XLsk6YR' '-d' '/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/c11-translation-kompiled' '-w' 'none' '--smt' 'none' '--argv' 'dummy' '--debug' '-cOPTIONS=`_Set_`(`SetItem`(`NoLink`(.KList)), `.Set`(.KList))' '-pOPTIONS=printf %s' '-cJSON=#token("\"{\\\"suppressions\\\"\\x3a [],\\\"message_length\\\"\\x3a 80,\\\"format\\\"\\x3a \\\"Console\\\",\\\"previous_errors\\\"\\x3a [],\\\"fatal_errors\\\"\\x3a false,\\\"rv_error\\\"\\x3a \\\"\\\"}\"", "String")' '-pJSON=printf %s' '-cOBJS=.K' '-pOBJS=printf %s' '-cPGM=tmp-kcc-KCS3YEy' '-pPGM=cat'
'/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/pp' '-I' '.' '-pedantic' '-pedantic' '-pedantic' '-pedantic' 'stdlib.c' '-o' 'tmp-kcc-SMR00CY'
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
/root/src/c-semantics/c-semantics/dist/cparser tmp-kcc-SMR00CY --trueName 'stdlib.c' > tmp-kcc-2qy23T6
'krun' '--output' 'binary' '--output-file' 'tmp-kcc-Szsntkq' '-d' '/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/c11-translation-kompiled' '-w' 'none' '--smt' 'none' '--argv' 'dummy' '--debug' '-cOPTIONS=`_Set_`(`SetItem`(`NoLink`(.KList)), `.Set`(.KList))' '-pOPTIONS=printf %s' '-cJSON=#token("\"{\\\"suppressions\\\"\\x3a [],\\\"message_length\\\"\\x3a 80,\\\"format\\\"\\x3a \\\"Console\\\",\\\"previous_errors\\\"\\x3a [],\\\"fatal_errors\\\"\\x3a false,\\\"rv_error\\\"\\x3a \\\"\\\"}\"", "String")' '-pJSON=printf %s' '-cOBJS=.K' '-pOBJS=printf %s' '-cPGM=tmp-kcc-2qy23T6' '-pPGM=cat'
'/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/pp' '-I' '.' '-pedantic' '-pedantic' '-pedantic' '-pedantic' '-pedantic' 'string.c' '-o' 'tmp-kcc-S0q37gB'
Can't exec "rv-ifdefclear": No such file or directory at /root/src/c-semantics/c-semantics/dist/kcc line 4002.
/root/src/c-semantics/c-semantics/dist/cparser tmp-kcc-S0q37gB --trueName 'string.c' > tmp-kcc-CijZE9J
'krun' '--output' 'binary' '--output-file' 'tmp-kcc-zvLmw2d' '-d' '/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/c11-translation-kompiled' '-w' 'none' '--smt' 'none' '--argv' 'dummy' '--debug' '-cOPTIONS=`_Set_`(`SetItem`(`NoLink`(.KList)), `.Set`(.KList))' '-pOPTIONS=printf %s' '-cJSON=#token("\"{\\\"suppressions\\\"\\x3a [],\\\"message_length\\\"\\x3a 80,\\\"format\\\"\\x3a \\\"Console\\\",\\\"previous_errors\\\"\\x3a [],\\\"fatal_errors\\\"\\x3a false,\\\"rv_error\\\"\\x3a \\\"\\\"}\"", "String")' '-pJSON=printf %s' '-cOBJS=.K' '-pOBJS=printf %s' '-cPGM=tmp-kcc-CijZE9J' '-pPGM=cat'
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
substr outside of string at /root/src/c-semantics/c-semantics/dist/kcc line 3940.
Use of uninitialized value $thisObj in concatenation (.) or string at /root/src/c-semantics/c-semantics/dist/kcc line 3942.
'krun' '--output' 'binary' '--output-file' 'tmp-kcc-Lw8SIuq' '-d' '/root/src/c-semantics/c-semantics/dist/x86-gcc-limited-libc/cpp14-translation-kompiled' '-w' 'none' '--smt' 'none' '--argv' 'dummy' '--debug' '-cOPTIONS=`_Set_`(`SetItem`(`NoLink`(.KList)), `.Set`(.KList))' '-pOPTIONS=printf %s' '-cJSON=#token("\"{\\\"suppressions\\\"\\x3a [],\\\"message_length\\\"\\x3a 80,\\\"format\\\"\\x3a \\\"Console\\\",\\\"previous_errors\\\"\\x3a [],\\\"fatal_errors\\\"\\x3a false,\\\"rv_error\\\"\\x3a \\\"\\\"}\"", "String")' '-pJSON=printf %s' '-cOBJS=tmp-kcc-ALGtF4J' '-pOBJS=cat' '-cPGM=.K' '-pPGM=printf %s'
java.util.NoSuchElementException
at java.util.ArrayDeque.removeFirst(ArrayDeque.java:280)
at java.util.ArrayDeque.pop(ArrayDeque.java:517)
at org.kframework.parser.binary.BinaryParser.read400(BinaryParser.java:104)
at org.kframework.parser.binary.BinaryParser.parse(BinaryParser.java:198)
at org.kframework.parser.binary.BinaryParser.parse(BinaryParser.java:182)
at org.kframework.krun.KRun.externalParse(KRun.java:385)
at org.kframework.krun.KRun.parseConfigVars(KRun.java:302)
at org.kframework.krun.KRun.run(KRun.java:84)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
java.util.NoSuchElementException
at java.util.ArrayDeque.removeFirst(ArrayDeque.java:280)
at java.util.ArrayDeque.pop(ArrayDeque.java:517)
at org.kframework.parser.binary.BinaryParser.read400(BinaryParser.java:104)
at org.kframework.parser.binary.BinaryParser.parse(BinaryParser.java:198)
at org.kframework.parser.binary.BinaryParser.parse(BinaryParser.java:182)
at org.kframework.krun.KRun.externalParse(KRun.java:385)
at org.kframework.krun.KRun.parseConfigVars(KRun.java:302)
at org.kframework.krun.KRun.run(KRun.java:84)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
[Error] Internal: Uncaught exception thrown of type NoSuchElementException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)
Error: Could not find or load main class org.kframework.main.BinaryToText
Translation failed (config dumped). Refer to last command run for details.
If in the configuration, a cell contains large data, it would take long time to print the whole configuration. Especially when debugging the kprover in intellij, nearly in each step, the intellij will print the whole configuration. It would be great if there is an option to krun
and kprove
to suppress printing certain cells in the configuration.
To improve the run-time of the KEVM and KEVM proofs, we've been discussing ways to avoid re-parsing the byte-code on every proof run.
Three solutions were proposed:
Add a feature to cache the results of krun
, and use the resulting configuration as defaults for filling the LHS of cells in the proof when told to do so.
Cache the results of simplifying the LHS of certain cells in proofs using only function
rules.
Add cross-execution memoization of marked function
symbols in the semantics. We can start out with a simple cache which has a finite number of cache slots and randomly selects which slot to discard on new calls to the function, and eventually implement more sensible least-recently-used logic. For the purposes of running the proofs, it should be enough to have a small number of cache slots as most of the proofs which re-use the same code are usually run together at the same time.
After discussion, @dwightguth and @ehildenb think that option (3) is good. @daejunpark what do you think?
I'm seeing strange behavior when invoking the unification engine on a definition which also uses strategies. Before commit 7b4f03095 - Add parameters to Sort and KLabel (#69)
this seems to work fine, but afterward the Java backend throws "Array out of bounds" exceptions.
Here is an example definition (file test.k
):
module TEST
imports DOMAINS
imports STRATEGY
imports BASIC-STRATEGY
configuration
<TEST>
initSCell(Init)
<k> $INIT:Foo </k>
</TEST>
syntax Foo ::= "symbolicFoo" [function]
| "foo" | "bar"
rule <s> ~ S => . ... </s>
rule <k> symbolicFoo => ?X:Foo ... </k>
rule <k> foo => bar ... </k> [tag(F2B)]
rule <k> bar => foo ... </k> [tag(B2F)]
endmodule
Kompiled with the following command:
kompile --backend java test.k
And invoked with the following command (no input file needed):
krun -cSTRATEGY='^ F2B' -cINIT=symbolicFoo --debug
This is blocking https://github.com/kframework/kat from updating to the newest K submodule.
Pretty printing cells k and the constraint inside a proof took <0.1s before, ~40s after.
Consider supporting 2 versions of unparsing: the old and the new one.
This script illustrates the issue. It runs a relatively short proof from casper project, on 2 versions of K gnosis
branch. One before the rebase on latest master, one after. Run the script below inside an empty dir, go to verified-smart-contracts
and compare the two .out
files. Compare the latest 2 logged times: STEP 2724 v1
and TOTAL TIME:
.
#!/usr/bin/env bash
git clone --recurse-submodules https://github.com/runtimeverification/verified-smart-contracts.git
cd verified-smart-contracts/.build/evm-semantics/.build/k
git fetch
git checkout gnosis_slow_pp
mvn package -Dmaven.test.skip=true
cd ../..
make defn
.build/k/k-distribution/target/release/k/bin/kompile --debug --backend java -I .build/java -d .build/java --main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION .build/java/driver.k
cd ../..
make casper
.build/evm-semantics/.build/k/k-distribution/target/release/k/bin/kprove specs/casper/total_curdyn_deposits_scaled-success-spec.k -d .build/evm-semantics/.build/java -m VERIFICATION \
--z3-executable --log-basic> pretty-print-k-and-contraint-slow.out 2>&1
cd .build/evm-semantics/.build/k
git checkout gnosis_before_rebase
mvn package -Dmaven.test.skip=true
cd ../..
.build/k/k-distribution/target/release/k/bin/kompile --debug --backend java -I .build/java -d .build/java --main-module ETHEREUM-SIMULATION --syntax-module ETHEREUM-SIMULATION .build/java/driver.k
cd ../..
.build/evm-semantics/.build/k/k-distribution/target/release/k/bin/kprove specs/casper/total_curdyn_deposits_scaled-success-spec.k -d .build/evm-semantics/.build/java -m VERIFICATION \
--z3-executable --log-basic> pretty-print-k-and-contraint-fast.out 2>&1
This is already an issue on the legacy repo, but are there any plans to get KDoc working in K5, or at least to print out rules in that nice lego-block format, used e.g. on page 13 in the SIMPLE paper?
kool-untyped.k
tutorial../../../../bin/kompile --backend java kool-untyped.k
../../../../bin/krun --debug tests/field.kool
Issue does not occur with default backend.
I'm using Java 1.8.0_151 on Ubuntu 16.04
java.lang.AssertionError: unexpected class at matching: class org.kframework.backend.java.kil.KSequence
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:321)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:307)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:299)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:299)
at org.kframework.backend.java.symbolic.FastRuleMatcher.unifyEquality(FastRuleMatcher.java:173)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:375)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:331)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.addAndSimplify(ConjunctiveFormula.java:149)
at org.kframework.backend.java.kil.ConstrainedTerm.lambda$evaluateConstraints$0(ConstrainedTerm.java:208)
at org.kframework.backend.java.kil.ConstrainedTerm$$Lambda$248.000000009D2C5F20.apply(Unknown Source)
at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:204)
at java.util.Iterator.forEachRemaining(Iterator.java:127)
at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1812)
at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:523)
at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:513)
at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:719)
at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:245)
at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:510)
at org.kframework.backend.java.kil.ConstrainedTerm.evaluateConstraints(ConstrainedTerm.java:216)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:111)
at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:154)
at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:95)
at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:82)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:168)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
at org.kframework.krun.KRun.run(KRun.java:99)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:90)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:114)
at org.kframework.main.Main.runApplication(Main.java:104)
at org.kframework.main.Main.main(Main.java:53)
java.lang.AssertionError: unexpected class at matching: class org.kframework.backend.java.kil.KSequence
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:321)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:390)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:307)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:299)
at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:299)
at org.kframework.backend.java.symbolic.FastRuleMatcher.unifyEquality(FastRuleMatcher.java:173)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:375)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:331)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.addAndSimplify(ConjunctiveFormula.java:149)
at org.kframework.backend.java.kil.ConstrainedTerm.lambda$evaluateConstraints$0(ConstrainedTerm.java:208)
at org.kframework.backend.java.kil.ConstrainedTerm$$Lambda$248.000000009D2C5F20.apply(Unknown Source)
at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:204)
at java.util.Iterator.forEachRemaining(Iterator.java:127)
at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1812)
at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:523)
at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:513)
at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:719)
at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:245)
at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:510)
at org.kframework.backend.java.kil.ConstrainedTerm.evaluateConstraints(ConstrainedTerm.java:216)
at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:111)
at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:154)
at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:95)
at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:82)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:168)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:70)
at org.kframework.krun.KRun.run(KRun.java:99)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:90)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:114)
at org.kframework.main.Main.runApplication(Main.java:104)
at org.kframework.main.Main.main(Main.java:53)
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (unexpected class
at matching: class org.kframework.backend.java.kil.KSequence)
mvn package:
...........................
Tests run: 23, Failures: 0, Errors: 21, Skipped: 0, Time elapsed: 32.021 sec <<< FAILURE! - in org.kframework.parser.concrete2kore.RuleGrammarTest
test10(org.kframework.parser.concrete2kore.RuleGrammarTest) Time elapsed: 1.531 sec <<< ERROR!
org.kframework.utils.errorsystem.KEMException: [Error] Internal: gcc returned nonzero exit code. See output for details.
at org.kframework.utils.errorsystem.KEMException.create(KEMException.java:113)
at org.kframework.utils.errorsystem.KEMException.internalError(KEMException.java:59)
at org.kframework.parser.concrete2kore.kernel.Scanner.getScanner(Scanner.java:123)
at org.kframework.parser.concrete2kore.kernel.Scanner.(Scanner.java:38)
at org.kframework.parser.concrete2kore.ParseInModule.getScanner(ParseInModule.java:115)
at org.kframework.parser.concrete2kore.ParseInModule.getGrammar(ParseInModule.java:104)
at org.kframework.parser.concrete2kore.ParseInModule.parseStringTerm(ParseInModule.java:147)
at org.kframework.parser.concrete2kore.ParseInModule.parseString(ParseInModule.java:121)
at org.kframework.parser.concrete2kore.ParseInModule.parseString(ParseInModule.java:99)
at org.kframework.parser.concrete2kore.RuleGrammarTest.parseRule(RuleGrammarTest.java:63)
at org.kframework.parser.concrete2kore.RuleGrammarTest.test10(RuleGrammarTest.java:237)
gcc 7.1.0 Self compiled;
There will be no problem executing the “mvn package -DskipTests” command.
when supplying a custom z3 prelude file, axioms have to be stated about "known" symbols, so they have to be defined in the prelude file as well. However, currently there is no way to prevent them here to be exported a second time, which leads to a crash. I currently modify the file myself and recompile k in order to prevent a crash due tue a z3 prelude file. It would be great to have a flag which i can pass the symbols i customely defined in the prelude.
When using K after commit 097e611 with newest rv-match backend, it fails to build the newest C/C++ semantics (91161bdb21b1cf86fb3398b2d0b299b84ceda442). Output:
Kompiling the static C++ semantics...
kompile -O2 --backend ocaml --non-strict --opaque-klabels c11/c11-translation.k --smt none cpp14/cpp14-translation.k -d "x86-gcc-limited-libc/cpp14-translation-kompiled" --no-prelude -w all -v --debug -I /path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics -I /path/to/c-semantics/x86-gcc-limited-libc/semantics
Parse command line options = 37
Importing: Source(/path/to/c-semantics/semantics/./cpp14/cpp14-translation.k)
Importing: Source(/path/to/runtimeverification/k/k-distribution/target/release/k/include/builtin/kast.k)
Importing: Source(/path/to/runtimeverification/k/k-distribution/target/release/k/include/builtin/domains.k)
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/translation/translation.k)
... (a lot of stuff) ...
Importing: Source(/path/to/c-semantics/semantics/cpp14/language/linking/resolution.k)
Importing: Source(/path/to/c-semantics/x86-gcc-limited-libc/cpp-semantics/cpp-settings.k)
/tmp/tmp-kompile-8536276429347807810.l:2385: warning, rule cannot be matched
/tmp/tmp-kompile-4446192371551866502.l:18280: warning, rule cannot be matched
/tmp/tmp-kompile-5378504171804408025.l:49003: warning, rule cannot be matched
Parse definition [3182/3183 rules] = 113186
Apply compile pipeline = 5356
java.lang.NoSuchMethodError: org.kframework.definition.Module.unresolvedLocalSentences()Lscala/collection/Set;
at org.kframework.backend.ocaml.DefinitionToOcaml.lambda$initialize$9756c910$1(DefinitionToOcaml.java:245)
at org.kframework.backend.ocaml.DefinitionToOcaml$$Lambda$279/860222046.apply(Unknown Source)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at org.kframework.backend.ocaml.DefinitionToOcaml.initialize(DefinitionToOcaml.java:252)
at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:50)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
java.lang.NoSuchMethodError: org.kframework.definition.Module.unresolvedLocalSentences()Lscala/collection/Set;
at org.kframework.backend.ocaml.DefinitionToOcaml.lambda$initialize$9756c910$1(DefinitionToOcaml.java:245)
at org.kframework.backend.ocaml.DefinitionToOcaml$$Lambda$279/860222046.apply(Unknown Source)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at org.kframework.backend.ocaml.DefinitionToOcaml.initialize(DefinitionToOcaml.java:252)
at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:50)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
[Error] Internal: Uncaught exception thrown of type NoSuchMethodError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
(org.kframework.definition.Module.unresolvedLocalSentences()Lscala/collection/Set;)
With the previous version of K (2ba519f), the output is a bit different:
...
Importing: Source(/home/jenda/Documents/School/DP/c-semantics/x86-gcc-limited-libc/semantics/c-settings.k)
40 states, 1247 transitions, table size 5228 bytes
File "constants.ml", line 16601, characters 21-2993:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(ThreadLocal|Thread (_, _, _, _))
File "constants.ml", line 16638, characters
...
Warning 58: no cmx file was found in path for module Gmp, and its interface was not compiled with -opaque
java.lang.NullPointerException
at org.kframework.backend.ocaml.ConvertDataStructureToLookup.convert(ConvertDataStructureToLookup.java:581)
at org.kframework.backend.ocaml.DefinitionToOcaml$$Lambda$351/550194951.apply(Unknown Source)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at org.kframework.backend.ocaml.DefinitionToOcaml.convert(DefinitionToOcaml.java:279)
at org.kframework.backend.ocaml.DefinitionToOcaml.ocamlMatchPattern(DefinitionToOcaml.java:379)
at org.kframework.backend.ocaml.DefinitionToOcaml.interpreter(DefinitionToOcaml.java:550)
at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:134)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
java.lang.NullPointerException
at org.kframework.backend.ocaml.ConvertDataStructureToLookup.convert(ConvertDataStructureToLookup.java:581)
at org.kframework.backend.ocaml.DefinitionToOcaml$$Lambda$351/550194951.apply(Unknown Source)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at org.kframework.backend.ocaml.DefinitionToOcaml.convert(DefinitionToOcaml.java:279)
at org.kframework.backend.ocaml.DefinitionToOcaml.ocamlMatchPattern(DefinitionToOcaml.java:379)
at org.kframework.backend.ocaml.DefinitionToOcaml.interpreter(DefinitionToOcaml.java:550)
at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:134)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
[Error] Internal: Uncaught exception thrown of type NullPointerException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)
[Warning] Compiler: missing entry for hook C_SEMANTICS.error
[Warning] Compiler: missing entry for hook C_SEMANTICS.nativeFunctions
K version 2ba519f together with the semantics version d2f2c3584fbc980e8748738577e14f797a91c8e8 gives similar (the same?) error:
Step (Thread (_, _, _, [])::_, _)|
Step
((ThreadLocal|Bottom|KToken (_, _)|InjectedKLabel _|Map (_, _, _)|
List (_, _, _)|Set (_, _, _)|Array (_, _)|Int _|Float (_, _, _)|String _|
Bool _|KApply0 _|KApply1 (_, _)|KApply2 (_, _, _)|KApply3 (_, _, _, _)|
KApply4 (_, _, _, _, _)|KApply5 (_, _, _, _, _, _)|
KApply6 (_, _, _, _, _, _, _)|KApply7 (_, _, _, _, _, _, _, _)|
KApply8 (_, _, _, _, _, _, _, _, _)|
KApply9 (_, _, _, _, _, _, _, _, _, _)|
KApply10 (_, _, _, _, _, _, _, _, _, _, _)|
KApply12 (_, _, _, _, _, _, _, _, _, _, _, _, _)|
KApply15 (_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _))::_,
_)|
Step ([], _))
File "run.ml", line 33, characters 9-1066:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
[]
File "_none_", line 1:
Warning 58: no cmx file was found in path for module Gmp, and its interface was not compiled with -opaque
java.lang.NullPointerException
at org.kframework.backend.ocaml.ConvertDataStructureToLookup.convert(ConvertDataStructureToLookup.java:581)
at org.kframework.backend.ocaml.DefinitionToOcaml$$Lambda$352/1381237406.apply(Unknown Source)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at org.kframework.backend.ocaml.DefinitionToOcaml.convert(DefinitionToOcaml.java:279)
at org.kframework.backend.ocaml.DefinitionToOcaml.ocamlMatchPattern(DefinitionToOcaml.java:379)
at org.kframework.backend.ocaml.DefinitionToOcaml.interpreter(DefinitionToOcaml.java:550)
at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:134)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
java.lang.NullPointerException
at org.kframework.backend.ocaml.ConvertDataStructureToLookup.convert(ConvertDataStructureToLookup.java:581)
at org.kframework.backend.ocaml.DefinitionToOcaml$$Lambda$352/1381237406.apply(Unknown Source)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at scala.Function1$$anonfun$andThen$1.apply(Function1.scala:52)
at org.kframework.backend.ocaml.DefinitionToOcaml.convert(DefinitionToOcaml.java:279)
at org.kframework.backend.ocaml.DefinitionToOcaml.ocamlMatchPattern(DefinitionToOcaml.java:379)
at org.kframework.backend.ocaml.DefinitionToOcaml.interpreter(DefinitionToOcaml.java:550)
at org.kframework.backend.ocaml.OcamlBackend.accept(OcamlBackend.java:134)
at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:71)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:113)
at org.kframework.main.Main.runApplication(Main.java:103)
at org.kframework.main.Main.main(Main.java:52)
[Error] Internal: Uncaught exception thrown of type NullPointerException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)
[Warning] Compiler: missing entry for hook C_SEMANTICS.error
[Warning] Compiler: missing entry for hook C_SEMANTICS.nativeFunctions
K version 2ba519f together with the semantics version 8c2641ba528f7082b5197896e4ce0e57193a8540 works fine. K version 097e611 with the same semantics fails on '--exit-code' being passed to 'kompile'.
In all cases I had the latest ocaml backend (ocaml-backend-1.0-20170405.020916-316.jar), but I am not sure whether K used it every time - does it simply use the last accessible version?.
kompile --help
Result:
...
--backend
Choose a backend. <backend> is one of [ocaml|coq]. Each creates the
...
Sorry if this is a duplicate, as I'm aware some bugs with this are already known. Compiling the code below on my machine has the following output:
File "realdef.ml", line 1713, characters 79-80:
Error: Syntax error: ')' expected
File "realdef.ml", line 1713, characters 60-61:
Error: This '(' might be unmatched
[Error] Critical: ocamlopt returned nonzero exit code: 2
Examine output to see errors.
[Warning] Compiler: missing entry for hook BAG.concat
[Warning] Compiler: missing entry for hook BAG.element
[Warning] Compiler: missing entry for hook BAG.unit
Oddly enough, removing the Exp
category gets rid of the OCaml syntax errors but not the warnings:
[Warning] Compiler: missing entry for hook BAG.concat
[Warning] Compiler: missing entry for hook BAG.element
[Warning] Compiler: missing entry for hook BAG.unit
Minimal-ish example:
module FOO-SYNTAX
imports DOMAINS-SYNTAX
syntax Id ::= "main" [token]
syntax Exp ::= Int | Bool | String
| "(" Exp ")" [bracket]
| "-" Exp
> Exp "(" Exp ")"
| Exp "/" Exp [left, strict]
| Exp "*" Exp [left, strict]
| Exp "%" Exp [strict, left]
> Exp "+" Exp [left, strict]
| Exp "-" Exp [left, strict]
> Exp "<" Exp [strict, non-assoc]
| Exp "<=" Exp [strict, non-assoc]
| Exp ">" Exp [strict, non-assoc]
| Exp ">=" Exp [strict, non-assoc]
| Exp "=" Exp [strict, non-assoc]
| Exp "!=" Exp [strict, non-assoc]
> "!" Exp [strict]
> Exp "&&" Exp [left, strict(1)]
| Exp "||" Exp [left, strict(1)]
| "(" Exp ")" [bracket]
syntax Pgm ::= Id
endmodule
module FOO
imports FOO-SYNTAX
imports DOMAINS
syntax KResult ::= Int | Bool | String
configuration <T color="yellow">
<actors color="orange">
<actor multiplicity="*" color="yellow">
<k color="green"> $PGM:Pgm </k>
<env color="violet"> .Map </env>
<store color="red"> .Map </store>
<nextLoc color="gray"> 0 </nextLoc>
</actor>
</actors>
</T>
endmodule
I see, in the old version 3.4.we can symbolic a variate use the backend "symbolic" and run it with cIN="ListItem(#symInt(n))" but there is no backend "symbolic" in k5,does it mean that backend "java" already do this work?and how can i run just use the symbolic way now to symbolic a "int n"?
This is referring to things like doing IO as functions.
Look at this (incorrect) rule:
rule A => false
requires chop( 1 &Int bool2Word ( A ) ) ==K 0 [trusted]
It will be compiled into a spec rule, not a function rule, e.g.: <k> A => false ...</k>...
Now if this rule applies once, it will normally continue to apply indefinitely, rewriting the spec to itself. kprove has a mechanism to prevent this:
If a a configuration is encountered the 2nd time, the respective path will be considered proven. Thus, in our case kprove will report that spec is proved, while in fact it would execute indefinitely. I propose considering looping path "not proven" and print an appropriate message. Will submit a fix ASAP.
I've problems with ^Int
expressions in an evm-semantics proof. They can't be translated into z3 and therefore the impliesSMT
function crashes: this blocks from having expressions with ^Int
in require statements of lemmas:
e.g. I've a precondition a the circularity rule looking like this:
X ^Int (2 +Int N) <Int pow256
1 <=Int X
X <Int pow256
...
at one point in the proof I multiply X*X which leaves chop(X *Int X)
on the stack
in order to reason about it i have the following lemma:
rule chop(X *Int X) => X *Int X
requires X ^Int (2 +Int N) <Int pow256
Since the actual proof is for an implementation of fixed-point exponentiation by squaring I don't see how omitting ^Int
expressions in requirements is possible.
Tried to build from k-distribution and also k-master folder. Both are failing with the following message.
[INFO] Scanning for projects...
Downloading from runtime-verification.snapshots: http://office.runtimeverificati
on.com:8888/repository/snapshots/com/runtimeverification/rv_match/parent/1.0-SNA
PSHOT/maven-metadata.xml
[WARNING] Could not transfer metadata com.runtimeverification.rv_match:parent:1.
0-SNAPSHOT/maven-metadata.xml from/to runtime-verification.snapshots (http://off
ice.runtimeverification.com:8888/repository/snapshots): Connect to office.runtim
everification.com:8888 [office.runtimeverification.com/76.191.23.163] failed: Co
nnection timed out: connect
Downloading from runtime-verification.snapshots: http://office.runtimeverificati
on.com:8888/repository/snapshots/com/runtimeverification/rv_match/parent/1.0-SNA
PSHOT/parent-1.0-SNAPSHOT.pom
[ERROR] [ERROR] Some problems were encountered while processing the POMs:
[FATAL] Non-resolvable parent POM for com.runtimeverification.k:parent:[unknown-
version]: Could not transfer artifact com.runtimeverification.rv_match:parent:po
m:1.0-SNAPSHOT from/to runtime-verification.snapshots (http://office.runtimeveri
fication.com:8888/repository/snapshots): Connect to office.runtimeverification.c
om:8888 [office.runtimeverification.com/76.191.23.163] failed: Connection timed
out: connect and 'parent.relativePath' points at wrong local POM @ line 5, colum
n 11
@
[ERROR] The build could not read 1 project -> [Help 1]
[ERROR]
[ERROR] The project com.runtimeverification.k:parent:[unknown-version] (C:\kfr
amework\k-master\k-master\pom.xml) has 1 error
[ERROR] Non-resolvable parent POM for com.runtimeverification.k:parent:[unkn
own-version]: Could not transfer artifact com.runtimeverification.rv_match:paren
t:pom:1.0-SNAPSHOT from/to runtime-verification.snapshots (http://office.runtime
verification.com:8888/repository/snapshots): Connect to office.runtimeverificati
on.com:8888 [office.runtimeverification.com/76.191.23.163] failed: Connection ti
med out: connect and 'parent.relativePath' points at wrong local POM @ line 5, c
olumn 11 -> [Help 2]
[ERROR]
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e swit
ch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR]
[ERROR] For more information about the errors and possible solutions, please rea
d the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/ProjectBuildin
gException
[ERROR] [Help 2] http://cwiki.apache.org/confluence/display/MAVEN/UnresolvableMo
delException
The README file for the K Tutorial says "Some of the languages defined so far using the K framework can be found in the tutorial/2_languages directory, and many others in the samples directory." When I clink on the links for these two directories, I get a "file not found" error.
When using kompile, it fails to compile the lambda.k(a very simple example).
cat lambda.k
[root@localhost hello]# cat lambda.k
// Copyright (c) 2012-2016 K Team. All Rights Reserved.
module LAMBDA-SYNTAX
syntax Val ::= Id
| "lambda" Id "." Exp
syntax Exp ::= Val
| Exp Exp [left]
| "(" Exp ")" [bracket]
endmodule
(1) kompile --no-prelude lambda.k. Output:
[root@localhost hello]# kompile --no-prelude lambda.k
[Error] Compiler: Could not find sorts: [Id]
Source(/root/src/c-semantics/hello/./lambda.k)
Location(4,18,4,19)
(2) kompile lambda.k. Output:
[root@localhost hello]# kompile lambda.k
[Error] Compiler: Could not find main module with name LAMBDA in definition.
Use --main-module to specify one.
I don't know what the reason is.
Who has the latest K manual?
Thank you.
mvn verify
fails because k-exercises
is missing. It seems like it is not checked into runtimeverification (https://github.com/runtimeverification).
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-antrun-plugin:1.7:run (exec-ktest) on project k-distribution: An Ant BuildException has occured: The directory /Users/danielsf/runtimeverification/k-exercises does not exist
[ERROR] around Ant part ...<exec dir="/Users/danielsf/runtimeverification/k/k-distribution/../../k-exercises" executable="make">... @ 4:104 in /Users/danielsf/runtimeverification/k/k-distribution/target/antrun/build-main.xml
Is there a way to step through each rule application procedure or something of similar granularity? I tried using --debug
and -v
flags, but i don't get enough info to understand what is wrong with my semantics
I have this kore file: https://github.com/radumereuta/k-light/blob/evenLighter/src/test/k/unparametric_examples/imp/imp-rules.kore.info (about 300kB - the result of parsing IMP rules, with lots of sharing in them).
Sometime between June 6 and July 7 there has been a change which makes kore-parser take a HUGE amount of time to run (stopped it after 10 minutes).
Tried rendering using kdoc, realized that it requires an older version, installed k3.6 and still doesn't work. Is there a prerendered pdf somewhere? K seems to have some rough edges to get up and running with :/
The tutorials also seem out of date, I'm having trouble getting them to run properly in k5.
People that aren't familiar with ocaml would also need to know the following:
EDIT: it looks like the ocaml backend was the issue. The kdoc is known not to work. It might be a good idea to keep the java backend the default for now
Hi, is there a reason I get a (parse) error on any float arithmetic i try to do:
rule I1:Float + I2:Float => I1 +Float I2
[Error] Critical: Rewrite is not allowed to be an immediate child of #cells
Use parentheses: (x)=>(y) to set the proper scope of the operations.
Source(./test.k)
Location(19,10,19,43)
k's java-backend caches compiled modules including the filepath to that module across executions. If now the module is compiled again from a different location without being changed the old filepath is used through the execution. Which causes problems if the old file is deleted.
A solution could be an additional flag which prevents k from caching compiled modules across executions or k rebuilding modules if its path changed.
When I try to make
I get a complaint that I don't have a java
of the required version:
~/src/k/latest/evm-semantics(dapphub/stable) » make build-java
== kompile: .build/java/driver-kompiled/timestamp
/home/lev/src/k/latest/evm-semantics/.build/k/k-distribution/target/release/k/bin/kompile --debug --main-module ETHEREUM-SIMULATION --backend java \
--syntax-module ETHEREUM-SIMULATION .build/java/driver.k --directory .build/java -I .build/java
Error: K requires Java 1.8 to run but the detected version is 10.0.1.
Please either add Java 1.8 bin directory to the PATH or set the JAVA_HOME
environment variable accordingly.
Makefile:131: recipe for target '.build/java/driver-kompiled/timestamp' failed
make: *** [.build/java/driver-kompiled/timestamp] Error 2
Indeed, the version reported by $ java -version
is:
~ » java -version
openjdk version "10.0.1" 2018-04-17
OpenJDK Runtime Environment (build 10.0.1+10-Debian-4)
OpenJDK 64-Bit Server VM (build 10.0.1+10-Debian-4, mixed mode)
So this appears to be some confusion in the Java version number convention. By the way, I am using openjdk-10-jre 10.0.1+10-4
provided by debian testing. I can only assume that anyone else using debian would have the same problem. The problem is resolved by adjusting MIN_VERSION
in k-distribution/src/main/scripts/lib/checkJava
, after that everything builds as expected.
I kompiled simple-typed-static.k and kran the programs manually, the resulting type of a function contains .Params
in its argument Types
instead of .Types
.
For example, krun exceptions_01.simple
gives following results:
<T>
<tasks>
.TaskCellBag
</tasks>
<gtenv>
main |-> void , .Params -> void
</gtenv>
</T>
Something similar happened when I tried to put Types
sort entry into a cell with default item .Types
.
syntax Decl ::= Type Exps ";"
| Type Id "(" Params ")" Block
| Type Id "(" Params ")" "throws" Types Block
...
configuration <T color="yellow">
<tasks color="orange">
<task multiplicity="*" color="yellow">
<k color="green"> $PGM:Stmts </k>
<tenv multiplicity="?" color="cyan"> .Map </tenv>
<returnType multiplicity="?" color="black"> void </returnType>
<mayThrow multiplicity="?" color="grey"> .Types </mayThrow>
</task>
</tasks>
<gtenv color="blue"> .Map </gtenv>
</T>
...
rule
<task> <k> T:Type F:Id(Ps:Params) throws Ts:Types S:Block => getTypes(Ps)->T F; ...</k> </task>
(.Bag => <task>
<k> mkDecls(Ps) S </k>
<tenv> .Map </tenv>
<returnType> T </returnType>
<mayThrow> Ts </mayThrow> /////////////////// Line 146
</task>)
[structural]
Kompiling simple-typed-static.k
with some rules and syntax added as above gives following result:
[Error] Compiler: Had 1 parsing errors.
[Error] Critical: Unexpected sort Types for term Ts. Expected Params.
Source(/some/random/directory/simple-typed-static.k)
Location(146,29,146,31)
Error disappeared when I put .
or .Params
in Line 146.
If I put .Types
in the Line 146, kompile fails with the following message:
[Error] Compiler: Had 1 parsing errors.
[Error] Inner Parser: Parse error: unexpected token '</throwsType>'.
Source(/some/random/directory/simple-typed-static.k)
Location(146,36,146,49)
I should I deal with it?
tutorial/1_k/1_lambda/lesson_1
kompile --backend ocaml lambda.k
krun --search --debug tests/identity.lambda
This occurs with Kool untyped as well. Running without --search
is fine, though.
I'm running OCaml 4.03.1+dev0-2016-04-25 on Linux Mint 18.3.
java.lang.UnsupportedOperationException
at org.kframework.backend.ocaml.OcamlRewriter$1.search(OcamlRewriter.java:116)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:55)
at org.kframework.krun.KRun.run(KRun.java:99)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:90)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:114)
at org.kframework.main.Main.runApplication(Main.java:104)
at org.kframework.main.Main.main(Main.java:53)
java.lang.UnsupportedOperationException
at org.kframework.backend.ocaml.OcamlRewriter$1.search(OcamlRewriter.java:116)
at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:55)
at org.kframework.krun.KRun.run(KRun.java:99)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:90)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:114)
at org.kframework.main.Main.runApplication(Main.java:104)
at org.kframework.main.Main.main(Main.java:53)
[Error] Internal: Uncaught exception thrown of type
UnsupportedOperationException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)
From commit c6f34a2,
when I try to build the c-semantics, it fails with error:
File "prelude.ml", line 136, characters 10-27:
Error: The constructor Array expects 2 argument(s),
but is applied here to 3 argument(s)
Version: Nightly build of K framework at commit babeea3
Consider lesson 8 of the lambda
tutorial. Here are two simple programs:
1 + 2
1+2
The first gives the expected result 3
. The second gives the unexpected result 1 2
. This might to be due to the second +
being interpreted as a unary +
operating on the 2
. In the definition, Exp Exp
and Exp "+" Exp
are both valid.
This problem is not seen with imp
. Both of the above inputs give the expected result 3
. This might be due to only Exp "+" Exp
being present in imp
.
Rearranging the two conflicting definitions in lambda
and/or giving one of them higher precedence does not seem to make any difference.
The following code does not give me any errors on compiling but fails to match when run:
rule <thread>... <k> test E => !T:Int ... </k> <env>Env</env> ...</thread>
(.Bag => <thread>... <k>E</k> <env>Env</env> <id>!T</id> ...</thread>)
But this works (Note the spaces):
rule <thread>... <k> test E => !T:Int ... </k> <env> Env </env> ...</thread>
(.Bag => <thread>... <k> E </k> <env> Env </env> <id> !T </id> ...</thread>)
Is that expected? This makes it very difficult to debug.
I'm getting this message about ocamlfind when trying to run K through intelliJ. In the terminal it all seems to work fine. Any idea what causes this?
This is a minimal example originally taken from the Solidity semantics.
Please see below for the K definition, program to run and additional details.
module IMP-SYNTAX
imports DOMAINS-SYNTAX
syntax Stmt ::= "addContract" "(" Id ")" ";"
| "addFunction" "(" Id "," Id ")" ";"
| "testFunction" "(" Id "," Id ")" ";"
| "testFunction1" "(" Int ")" ";"
> Stmt Stmt [left, format(%1%n%2)]
syntax Pgm ::= Stmt [format(%1 %2%3%n%4), colors(yellow,pink)]
endmodule
module IMP
imports IMP-SYNTAX
imports DOMAINS
configuration <T color="yellow">
<k color="green"> $PGM:Pgm </k>
<functions color="blue">
<nextFunction> 0:Int </nextFunction> // It works again if we move this outside of <functions>
<function multiplicity = "*">
<fId> 0:Int </fId>
</function>
</functions>
<contracts color="orange">
<contract multiplicity = "*">
<cName> . </cName>
<cFunctions> .Map </cFunctions>
</contract>
</contracts>
</T>
rule
<k> addContract(ContractName:Id); => . ... </k>
<contracts>
...
(.Bag =>
<contract>
<cName> ContractName </cName>
<cFunctions> .Map </cFunctions>
</contract>)
...
</contracts>
rule
<k> addFunction(ContractName:Id, FunctionName:Id); => . ... </k>
<contracts>
...
<contract>
<cName> ContractName </cName>
<cFunctions> ... .Map => FunctionName |-> N ... </cFunctions>
</contract>
...
</contracts>
<functions>
<nextFunction> N => N +Int 1 </nextFunction>
(.Bag => <function> <fId> N </fId> </function>)
...
</functions>
rule
<k> testFunction(ContractName:Id, FunctionName:Id); => "done" ... </k>
<contract>
<cName> ContractName </cName>
<cFunctions> ... FunctionName |-> N:Int ... </cFunctions>
</contract>
<function> <fId> N </fId> </function>
rule
S1:Stmt S2:Stmt => S1 ~> S2 [structural]
endmodule
addContract(foo);
addFunction(foo, f1);
addFunction(foo, f2);
addFunction(foo, f3);
testFunction(foo, f2); // but it works with f1 or f3 (first or last element)
This currently gets stuck as the match is unsuccessfull. However, it works if we use f1
or f3
instead (seems like it can match the first and last elements but fails otherwise).
I am currently using the latest sources of K5 (git revision a3adf21
according to kompile --version
)
It seems to work in commit d7a851c
, but fails in the next commit
If we do a little modification, it seems to work. This is the modification: in the configuration, move the <nextFunction>
outside of the <functions>
cell, and update the addFunction
rule accordingly. After this step, the matching is successful.
This is the updated configuration:
configuration <T color="yellow">
<k color="green"> $PGM:Pgm </k>
<nextFunction> 0:Int </nextFunction>
<functions color="blue">
<function multiplicity = "*">
<fId> 0:Int </fId>
</function>
</functions>
<contracts color="orange">
<contract multiplicity = "*">
<cName> . </cName>
<cFunctions> .Map </cFunctions>
</contract>
</contracts>
</T>
and rule
rule
<k> addFunction(ContractName:Id, FunctionName:Id); => . ... </k>
<contracts>
...
<contract>
<cName> ContractName </cName>
<cFunctions> ... .Map => FunctionName |-> N ... </cFunctions>
</contract>
...
</contracts>
<nextFunction> N => N +Int 1 </nextFunction>
<functions>
(.Bag => <function> <fId> N </fId> </function>)
...
</functions>
Class 'Scanner' runs gcc and assumes that flex library is installed. However, this dependency is not documented anywhere. Imho it should be documented in README.md.
I am trying to build k5 up to date to about 10 min ago.
mvn package succeeds, but sudo mvn install fails.
[INFO] ------------------------------------------------------------------------
[INFO] Reactor Summary:
[INFO]
[INFO] K Framework Tool Parent ............................ SUCCESS [01:58 min]
[INFO] K Framework KORE ................................... SUCCESS [01:30 min]
[INFO] K Framework Tool Kernel ............................ SUCCESS [01:07 min]
[INFO] K Framework KTree .................................. SUCCESS [ 0.522 s]
[INFO] K Framework Ocaml Backend .......................... SUCCESS [ 0.489 s]
[INFO] K Framework Java Backend ........................... SUCCESS [ 29.130 s]
[INFO] K Framework Tool Distribution ...................... FAILURE [02:08 min]
[INFO] K Framework API .................................... SKIPPED
[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 07:54 min
[INFO] Finished at: 2018-02-26T12:23:09-04:00
[INFO] Final Memory: 39M/343M
[INFO] ------------------------------------------------------------------------
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-antrun-plugin:1.7:run (exec-ktest) on project k-distribution: An Ant BuildException has occured: exec returned: 2
[ERROR] around Ant part ...<exec failonerror="true" dir="/home/marko/src/k5/k-distribution/tutorial" executable="make">... @ 4:95 in /home/marko/src/k5/k-distribution/target/antrun/build-main.xml
The sort inference algorithm fails (is not robust) to infer the precise sort of a term with the polymorphic sorted production symbol, especially for #if_#then_#else_#fi
:
https://github.com/kframework/k/blob/a3adf2120bde353b7cd89f2d31662ff2c24c6631/k-distribution/include/builtin/domains.k#L730
A minimal example.
Suppose we have:
a.k:
module A
imports DOMAINS
configuration <k> $PGM:K </k>
syntax Foo ::= "foo" | "bar"
rule foo => #if ?B:Bool #then 0 #else 1 #fi
rule I:Int => bar
endmodule
1.a:
foo
Then, when we run the following:
$ kompile --backend java a.k
$ krun --smt none 1.a
<k>
#if V0 #then 0 #else 1 #fi
</k>
we expect it outputs bar
, but it got stuck without the second rule being applied.
Currently, the sort of the #if_#then_#else_#fi
term is inferred as K
, while it should be Int
.
See the small difference between the above example and the regression test:
https://github.com/kframework/k/blob/a3adf2120bde353b7cd89f2d31662ff2c24c6631/k-distribution/tests/regression-new/poly-sort/test.k
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.