runtimeverification / k Goto Github PK

K Framework Tools 7.0

License: BSD 3-Clause "New" or "Revised" License

Java 45.36% SMT 0.01% C 0.26% Shell 2.06% Standard ML 0.64% Scala 5.28% Python 42.28% Makefile 3.26% JavaScript 0.11% HTML 0.21% Nix 0.50% Pyret 0.01% Dockerfile 0.02% CSS 0.03%

k's People

Contributors

Stargazers

Watchers

Forkers

msaxena2 oscar-c shd101wyy virgil-serbanuta sdasgup3 uiuc-arc happyxzw mrchico mhhf luca590 traiansf variousforks ttuegel livnev asymmetric maya-rv denisadiaconescu radumereuta eviefp hjorthjort manhtv disisisid ana-pantilie jakerockland anvacaru franciscomelojr phillipharr1s andrew-miranti multiversx mewbak nishantjr icetan winnielin4 theo25 zawtom725 akihiro0710 joshpoll qianyangpeng iti satoshi-n galoisinc slowmistio djuanbei bitcalc pirapira https-github-com-goodman-ops hbourne sethpoulsen zhengyao-lin wenhaosu junkaicheng rts-2 5l1v3r1 andyclee likaioc joshs111 anda-amelia nice-aqiqi520 lemastero h0nzzik daqiann root-servers team-us-nsf zayadnimrod davidgtl mipasa haskell-monad plusxp babi1234567 stjordanis sashafrolov shubhamugare bnationsdev pleasecheckhere2021 alaref-codes kwannoel schmerik trtcoin kaii-zen 1974711560 mpetruska nrdxp vasil-sd fredericloulergue smirkybg c-vision allabadigarvita isabella232 ramaguru-forks agathaex ernestinaopum brandtfude yiyi-wang-rv byhoson thebluelizard lslightly dimplegrknyy jryans stevengre iq-scm

k's Issues

KORE Translation: functional/constructor attributes

Float arithmetic

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)

Exponential behavior when parsing shared term

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).

UnsupportedOperationException with --search in OCaml backend

Get Nightly build of K framework at commit 3af731f Prebuilt K binary
Open terminal and change into tutorial/1_k/1_lambda/lesson_1
Run kompile --backend ocaml lambda.k
Run 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)

K fails to build C/C++ semantics

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?.

java backend not mentioned in help

kompile --help

Result:

...
--backend
   Choose a backend. <backend> is one of [ocaml|coq]. Each creates the
...

"mvn package" is failing

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

No support for exponentials in rule requirements

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.

k-exercises not checked in

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

bad links in K Tutorial

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.

Cannot run program "ocamlfind" (in directory "."): error=2, No such file or directory

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?

KORE Translation: anywhere rules

KORE translation: comm, assoc, idem, unit axioms

KORE Translation: Attributes

KORE Translation: strategies

Error while compiling lambda.k

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.

KORE Translation: injection axioms

Unary + has higher precedence over binary + when both are applicable

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.

KORE Translation: as patterns

KORE Translation: KLabel variables

Debugging with krun

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

KORE Translation: owise rules

KORE Translation: fresh constants

flag for ignoring z3 symbols

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.

unparsing is slow after #110 fix

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

K Parser/Matching engine expects spaces between a cell and its content

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.

Wrong sort inference while parsing.

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?

kprove unsound when a spec rule leads to infinite loop

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:

https://github.com/kframework/k5/blob/7aa7d407a89ccb682729153f3808a239e0a7face/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java#L624-L625

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.

The commit 'fix array' breaks c-semantics

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)

Polymorphic sort inference failure

@dwightguth

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

Error while compiling c-semantics

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.

KORE Translation: contexts

Flex - an undocumented dependency

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.

Strange behaviour when invoking unification with definition that has strategies

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.

rename ocaml patchfile so as not to break users who have taken the highly insecure step of adding . to the front of their path

KORE Translation: impure functions

This is referring to things like doing IO as functions.

OCaml backend doesn't handle multiplicity *

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

Remove references to kdoc and --pdf

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?

Make an option to `krun` like `--suppress-cells` which suppresses outputting certain cells

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.

openjdk version confusion in checkJava

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.

@ehildenb

cached modules cause problems due to changed filepath

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.

krun AssertationError with java backend in nightly 023a4b6 prebuilt binary

Get Nightly build of K framework at commit 023a4b6 Prebuilt K binary
Open terminal and change into the directory containing the kool-untyped.k tutorial
Run ../../../../bin/kompile --backend java kool-untyped.k
Run ../../../../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)

how can i run use the symbolic way

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"?

missing documentation

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:

doesn't work with opam 2 beta (as installed by default on fedora) which takes a while to debug (symptom is ocamlc option from custom patch not working)

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

Cross-execution function caching/memoization

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?

KORE Translation: IMP

On the centos6.9,build fail

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.

Rule cannot match in Java backend

This is a minimal example originally taken from the Solidity semantics.
Please see below for the K definition, program to run and additional details.

K definition

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

Program to run

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).

K version and commit where it breaks

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

More details

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>

mvn install fails

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

kompile fails with simple lambda.k example

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.