[Bug] [kompile] - kompile -E crashes on everything I tested.

virgil-serbanuta commented 3 years ago

K Version

$ kompile --version
K version:    v5.1.180-0-g75d680ef7e-dirty
Build date:   Mon Sep 13 18:00:49 EEST 2021

(this is commit 75d680ef7e98589e161fdce1154428dd6706303b , the current master)

Description

Running kompile with -E crashes with ProvisionException, Error injecting constructor.

Input Files

Examples:

File: tmp.k

module TMP
endmodule

Reproduction Steps

$ kompile -E tmp.k --backend haskell

[Error] Internal: Uncaught exception thrown of type ProvisionException.
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
(ProvisionException: Unable to provision, see the following errors:

1) Error injecting constructor, java.lang.Error: Unresolved compilation
problems: 
        The type org.kframework.definition.Module cannot be resolved. It is indirectly
referenced from required .class files
        The import org.kframework.backend.llvm.matching.Matching cannot be resolved
        Matching cannot be resolved
        Matching cannot be resolved

  at org.kframework.backend.llvm.LLVMBackend.<init>(Unknown Source)
  while locating org.kframework.backend.llvm.LLVMBackend
  while locating org.kframework.compile.Backend annotated with
@com.google.inject.multibindings.Element(setName=,uniqueId=7, type=MAPBINDER,
keyType=java.lang.String)
  at org.kframework.kompile.BackendModule.configure(BackendModule.java:17) (via
modules: org.kframework.kompile.KompileModule ->
org.kframework.kompile.BackendModule ->
com.google.inject.multibindings.MapBinder$RealMapBinder)
  while locating java.util.Map<java.lang.String,
org.kframework.compile.Backend>
  at org.kframework.kompile.BackendModule.getKoreBackend(Unknown Source) (via
modules: org.kframework.kompile.KompileModule ->
org.kframework.kompile.BackendModule)
  while locating org.kframework.compile.Backend

1 error)

Expected Behavior

kompile -E should not crash, it should just output the K code with all requires statements resolved.

virgil-serbanuta commented 3 years ago

Actually, this is weirder: the first time I checkout a specific commit and do mvn clean && mvn package -DskipTests, kompile fails with this error, however, the second time I do the same mvn clean && mvn package -DskipTests, kompile -E works.

SchmErik commented 3 years ago

I did what you wrote in the report and I cannot reproduce the behavior that you're seeing... Here's the output that I get from fetching, checking out the current head at commit 75d680ef7e98589e161fdce1154428dd6706303b and running mvn clean && mvn package -DskipTests and kompile -E tmp.k

output.txt

virgil-serbanuta commented 3 years ago

Yeah, as I mentioned, I can't always reproduce it. For me the following steps work, I'm not sure what to do to make it more reliable:

git checkout <some-commit-in-the-past-e-g-c3d02667a57385b91065d33287d73df075609fcc>
mvn clean && mvn package -DskipTests
git checkout master
mvn clean && mvn package -DskipTests
kompile -E tmp.k --backend haskell

virgil-serbanuta commented 3 years ago

Could you try this tmp.k file?

module TMP
  imports BOOL
  imports INT
  imports K-EQUAL

  syntax KItem ::= a(Int)
  syntax Int ::= f(Int)  [function, functional, smtlib(asdf)]

  rule f(0) => 0
  rule f(_) => 1  [owise]

  rule f(_) >Int -1 => true  [simplification, smt-lemma]

  rule a(X) => .K requires f(X) >=Int -1

endmodule

SchmErik commented 3 years ago

I did

git fetch --all --prune
git checkout master
mvn clean && mvn package -DskipTests

and kompile -E tmp.k --backend haskell > output1.txt with the modified tmp.k here is the output: output1.txt

Here's my version:

$ kompile --version
K version:    v5.1.180-0-g75d680ef7e
Build date:   Mon Sep 13 10:15:33 PDT 2021

SchmErik commented 3 years ago

what happens when you do this on a9099b2882407fefa2104f3a488089c2759300e9?

SchmErik commented 3 years ago

another thing to try is to do git stash on your changes and build from a clean build...

virgil-serbanuta commented 3 years ago

$ git checkout a9099b2882407fefa2104f3a488089c2759300e9
$ mvn clean && mvn package -DskipTests
...
$ kompile -E tmp.k
[Error] Internal: Uncaught exception thrown of type ProvisionException.
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
(ProvisionException: Unable to provision, see the following errors:

1) Error injecting constructor, java.lang.Error: Unresolved compilation
problems: 
        The type org.kframework.definition.Module cannot be resolved. It is indirectly
referenced from required .class files
        The import org.kframework.backend.llvm.matching.Matching cannot be resolved
        Matching cannot be resolved
        Matching cannot be resolved

  at org.kframework.backend.llvm.LLVMBackend.<init>(Unknown Source)
  while locating org.kframework.backend.llvm.LLVMBackend
  while locating org.kframework.compile.Backend annotated with
@com.google.inject.multibindings.Element(setName=,uniqueId=7, type=MAPBINDER,
keyType=java.lang.String)
  at org.kframework.kompile.BackendModule.configure(BackendModule.java:17) (via
modules: org.kframework.kompile.KompileModule ->
org.kframework.kompile.BackendModule ->
com.google.inject.multibindings.MapBinder$RealMapBinder)
  while locating java.util.Map<java.lang.String,
org.kframework.compile.Backend>
  at org.kframework.kompile.BackendModule.getKoreBackend(Unknown Source) (via
modules: org.kframework.kompile.KompileModule ->
org.kframework.kompile.BackendModule)
  while locating org.kframework.compile.Backend

1 error)

FWIW, I just noticed that kompile does the same even without -E.

virgil-serbanuta commented 3 years ago

After updating all submodules, the problem went away.

Sorry for the trouble, I didn't think that updating the modules would make a difference.

radumereuta commented 3 years ago

Can this be closed then? If yes, can you also mark it as invalid?

runtimeverification / k