kframework/X86-64-semantics

Failing to compile the semantics

andsanmar opened this issue · 13 comments

andsanmar commented

Hello, I'm trying to compile the semantics (actually using the suggested fork of the k framework), anyway, it gives me an exception when trying to compile:

➜  semantics git:(master) ../scripts/kompile.pl --backend java                                                             
	Merging UTInstructionsPath
On branch master
Your branch is up to date with 'origin/master'.

nothing to commit, working tree clean
time  kompile x86-semantics.k --syntax-module X86-SYNTAX --main-module \
    X86-SEMANTICS --debug -v --backend java -I ./ -I common/x86-config/ 
[NOTE] To make opam select /usr/lib/kframework/lib/opamroot as its root in the current shell, add --set-root or set OPAMROOT
Parse command line options                                   =  0.001s
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-semantics.k)
Importing: Source(/home/andsanmar/programs/k/k-distribution/target/release/k/include/builtin/prelude.k)
Importing: Source(/home/andsanmar/programs/k/k-distribution/target/release/k/include/builtin/kast.k)
Importing: Source(/home/andsanmar/programs/k/k-distribution/target/release/k/include/builtin/domains.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-semantics.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-loader.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-configuration.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-syntax.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-abstract-syntax.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-memory.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-mint-wrapper.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-float-conversions.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/common-memory.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-env-init.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-fetch-execute.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-abstract-semantics.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-flag-checks.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-flag-checks-syntax.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-verification-lemmas.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-instructions-semantics.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/common.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/verification-lemmas.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/x86-config/common-configuration.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/common-utils.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/common-error.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/library/common-c-library.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/library/common-c-library-configuration.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/library/common-c-library-utils.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/library/common-c-library-io.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/library/common-c-library-stdio.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/common/library/common-c-library-stdlib.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-builtin.k)
Importing: Source(/home/andsanmar/programs/X86-64-semantics/semantics/x86-c-library.k)
java.lang.StringIndexOutOfBoundsException: String index out of range: -1
	at java.lang.String.substring(String.java:1960)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.readSort(TypeInferencer.java:878)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.computeValue(TypeInferencer.java:869)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.computeModel(TypeInferencer.java:817)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferenceVisitor.apply(TypeInferenceVisitor.java:100)
	at org.kframework.parser.concrete2kore.ParseInModule.parseStringTerm(ParseInModule.java:265)
	at org.kframework.parser.concrete2kore.ParseInModule.parseString(ParseInModule.java:186)
	at org.kframework.kompile.DefinitionParsing.performParse(DefinitionParsing.java:423)
	at org.kframework.kompile.DefinitionParsing.parseBubble(DefinitionParsing.java:391)
	at org.kframework.kompile.ResolveConfig.lambda$apply$8(ResolveConfig.java:69)
	at java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:269)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.Spliterators$ArraySpliterator.forEachRemaining(Spliterators.java:948)
	at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:482)
	at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:472)
	at java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:747)
	at java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:721)
	at java.util.stream.AbstractTask.compute(AbstractTask.java:327)
	at java.util.concurrent.CountedCompleter.exec(CountedCompleter.java:731)
	at java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:289)
	at java.util.concurrent.ForkJoinPool.helpComplete(ForkJoinPool.java:1870)
	at java.util.concurrent.ForkJoinPool.externalHelpComplete(ForkJoinPool.java:2467)
	at java.util.concurrent.ForkJoinTask.externalAwaitDone(ForkJoinTask.java:324)
	at java.util.concurrent.ForkJoinTask.doInvoke(ForkJoinTask.java:405)
	at java.util.concurrent.ForkJoinTask.invoke(ForkJoinTask.java:734)
	at java.util.stream.ReduceOps$ReduceOp.evaluateParallel(ReduceOps.java:714)
	at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:233)
	at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:566)
	at org.kframework.kompile.ResolveConfig.apply(ResolveConfig.java:84)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:74)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.immutable.Set$Set3.foreach(Set.scala:167)
	at scala.collection.TraversableLike.map(TraversableLike.scala:234)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:227)
	at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
	at scala.collection.SetLike.map(SetLike.scala:101)
	at scala.collection.SetLike.map$(SetLike.scala:101)
	at scala.collection.AbstractSet.map(Set.scala:47)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:72)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.immutable.Set$Set4.foreach(Set.scala:206)
	at scala.collection.TraversableLike.map(TraversableLike.scala:234)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:227)
	at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
	at scala.collection.SetLike.map(SetLike.scala:101)
	at scala.collection.SetLike.map$(SetLike.scala:101)
	at scala.collection.AbstractSet.map(Set.scala:47)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:72)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.immutable.HashSet$HashSet1.foreach(HashSet.scala:320)
	at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
	at scala.collection.immutable.HashSet$HashTrieSet.foreach(HashSet.scala:976)
	at scala.collection.TraversableLike.map(TraversableLike.scala:234)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:227)
	at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
	at scala.collection.SetLike.map(SetLike.scala:101)
	at scala.collection.SetLike.map$(SetLike.scala:101)
	at scala.collection.AbstractSet.map(Set.scala:47)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:72)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at org.kframework.definition.DefinitionTransformer.apply(transformers.scala:110)
	at org.kframework.kompile.DefinitionParsing.resolveConfigBubbles(DefinitionParsing.java:229)
	at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:172)
	at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:165)
	at org.kframework.kompile.Kompile.run(Kompile.java:133)
	at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
	at org.kframework.main.Main.runApplication(Main.java:118)
	at org.kframework.kserver.KServerFrontEnd.run(KServerFrontEnd.java:160)
	at org.kframework.main.Main.nailMain(Main.java:79)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at com.martiansoftware.nailgun.NGSession.run(NGSession.java:331)
Command exited with non-zero status 131
0.02user 0.00system 0:04.86elapsed 0%CPU (0avgtext+0avgdata 15008maxresident)k
0inputs+0outputs (0major+6318minor)pagefaults 0swaps

How may I solve this issue?

sdasgup3 commented

Hi @andsanmar, I tried reproducing the issue but I cannot. Just to be sure, you are using my fork for k clone.

The error seems to coming after the parsing of the x86 semantics files are done. I am curious to know how you build the k repo.
Also, can you try building the k repo using mvn package -DskipTests -DskipKTest -Dllvm.backend.skip -DskipDocs -Dhaskell.backend.skip. This is just to narrow down the build to only java backend.

Let me know.

andsanmar commented

Hello, by buildin the k repo (yes I'm using your fork) with the command you provide I still have the same error. I built the k rep by simply running mvn package and the command specified later in the README (to setting it up for the OCAML environment)

sdasgup3 commented

Thanks!
Can you quickly try out building this using kompile TEST.k --debug --backend java --main-module TEST and let me know if the build goes through?

I just updated the this link

andsanmar commented

I get the following output (seems similar to the one of compiling the semantics):

➜  TEST72 git:(master) kompile TEST.k --debug --backend java --main-module TEST
[NOTE] To make opam select /usr/lib/kframework/lib/opamroot as its root in the current shell, add --set-root or set OPAMROOT
java.lang.StringIndexOutOfBoundsException: String index out of range: -1
	at java.lang.String.substring(String.java:1960)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.readSort(TypeInferencer.java:878)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.computeValue(TypeInferencer.java:869)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.computeModel(TypeInferencer.java:817)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferenceVisitor.apply(TypeInferenceVisitor.java:100)
	at org.kframework.parser.concrete2kore.ParseInModule.parseStringTerm(ParseInModule.java:265)
	at org.kframework.parser.concrete2kore.ParseInModule.parseString(ParseInModule.java:186)
	at org.kframework.kompile.DefinitionParsing.performParse(DefinitionParsing.java:423)
	at org.kframework.kompile.DefinitionParsing.parseBubble(DefinitionParsing.java:391)
	at org.kframework.kompile.ResolveConfig.lambda$apply$8(ResolveConfig.java:69)
	at java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:269)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.Iterator.forEachRemaining(Iterator.java:116)
	at scala.collection.convert.Wrappers$IteratorWrapper.forEachRemaining(Wrappers.scala:26)
	at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1801)
	at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:482)
	at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:472)
	at java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:747)
	at java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:721)
	at java.util.stream.AbstractTask.compute(AbstractTask.java:327)
	at java.util.concurrent.CountedCompleter.exec(CountedCompleter.java:731)
	at java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:289)
	at java.util.concurrent.ForkJoinTask.doInvoke(ForkJoinTask.java:401)
	at java.util.concurrent.ForkJoinTask.invoke(ForkJoinTask.java:734)
	at java.util.stream.ReduceOps$ReduceOp.evaluateParallel(ReduceOps.java:714)
	at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:233)
	at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:566)
	at org.kframework.kompile.ResolveConfig.apply(ResolveConfig.java:84)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:76)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.immutable.Set$Set3.foreach(Set.scala:167)
	at scala.collection.TraversableLike.map(TraversableLike.scala:234)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:227)
	at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
	at scala.collection.SetLike.map(SetLike.scala:101)
	at scala.collection.SetLike.map$(SetLike.scala:101)
	at scala.collection.AbstractSet.map(Set.scala:47)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:72)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at org.kframework.definition.DefinitionTransformer.apply(transformers.scala:110)
	at org.kframework.kompile.DefinitionParsing.resolveConfigBubbles(DefinitionParsing.java:229)
	at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:172)
	at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:165)
	at org.kframework.kompile.Kompile.run(Kompile.java:133)
	at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
	at org.kframework.main.Main.runApplication(Main.java:118)
	at org.kframework.kserver.KServerFrontEnd.run(KServerFrontEnd.java:160)
	at org.kframework.main.Main.nailMain(Main.java:79)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at com.martiansoftware.nailgun.NGSession.run(NGSession.java:331)
sdasgup3 commented

Thanks! This example is the minimal version of the x86 semantics, that should compile.
Now am more towards having a problem in the k build.

Anyway, I tried another test using kompile TEST.k --debug --backend java --main-module TEST, but this time the tool kompile comes from building the trunk of k repository (not my fork). The test using integer and map builtins only.

Can you please do that experiment? That will help me find out if the bug is in my k fork or is it in the mainline.

andsanmar commented

After compiling that test with your fork I get the same error:

➜  TEST73 git:(master) kompile TEST.k --debug --backend java --main-module TEST
[NOTE] To make opam select /usr/lib/kframework/lib/opamroot as its root in the current shell, add --set-root or set OPAMROOT
java.lang.StringIndexOutOfBoundsException: String index out of range: -1
	at java.lang.String.substring(String.java:1960)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.readSort(TypeInferencer.java:878)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.computeValue(TypeInferencer.java:869)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferencer.computeModel(TypeInferencer.java:817)
	at org.kframework.parser.concrete2kore.disambiguation.TypeInferenceVisitor.apply(TypeInferenceVisitor.java:100)
	at org.kframework.parser.concrete2kore.ParseInModule.parseStringTerm(ParseInModule.java:265)
	at org.kframework.parser.concrete2kore.ParseInModule.parseString(ParseInModule.java:186)
	at org.kframework.kompile.DefinitionParsing.performParse(DefinitionParsing.java:423)
	at org.kframework.kompile.DefinitionParsing.parseBubble(DefinitionParsing.java:391)
	at org.kframework.kompile.ResolveConfig.lambda$apply$8(ResolveConfig.java:69)
	at java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:269)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:193)
	at java.util.stream.ReferencePipeline$2$1.accept(ReferencePipeline.java:175)
	at java.util.Iterator.forEachRemaining(Iterator.java:116)
	at scala.collection.convert.Wrappers$IteratorWrapper.forEachRemaining(Wrappers.scala:26)
	at java.util.Spliterators$IteratorSpliterator.forEachRemaining(Spliterators.java:1801)
	at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:482)
	at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:472)
	at java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:747)
	at java.util.stream.ReduceOps$ReduceTask.doLeaf(ReduceOps.java:721)
	at java.util.stream.AbstractTask.compute(AbstractTask.java:327)
	at java.util.concurrent.CountedCompleter.exec(CountedCompleter.java:731)
	at java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:289)
	at java.util.concurrent.ForkJoinTask.doInvoke(ForkJoinTask.java:401)
	at java.util.concurrent.ForkJoinTask.invoke(ForkJoinTask.java:734)
	at java.util.stream.ReduceOps$ReduceOp.evaluateParallel(ReduceOps.java:714)
	at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:233)
	at java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:566)
	at org.kframework.kompile.ResolveConfig.apply(ResolveConfig.java:84)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:76)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.immutable.Set$Set3.foreach(Set.scala:167)
	at scala.collection.TraversableLike.map(TraversableLike.scala:234)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:227)
	at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
	at scala.collection.SetLike.map(SetLike.scala:101)
	at scala.collection.SetLike.map$(SetLike.scala:101)
	at scala.collection.AbstractSet.map(Set.scala:47)
	at org.kframework.definition.ModuleTransformer.$anonfun$apply$1(transformers.scala:72)
	at scala.collection.concurrent.TrieMap.getOrElseUpdate(TrieMap.scala:903)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:71)
	at org.kframework.definition.ModuleTransformer.apply(transformers.scala:67)
	at org.kframework.definition.DefinitionTransformer.apply(transformers.scala:110)
	at org.kframework.kompile.DefinitionParsing.resolveConfigBubbles(DefinitionParsing.java:229)
	at org.kframework.kompile.DefinitionParsing.parseDefinitionAndResolveBubbles(DefinitionParsing.java:172)
	at org.kframework.kompile.Kompile.parseDefinition(Kompile.java:165)
	at org.kframework.kompile.Kompile.run(Kompile.java:133)
	at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:70)
	at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
	at org.kframework.main.Main.runApplication(Main.java:118)
	at org.kframework.kserver.KServerFrontEnd.run(KServerFrontEnd.java:160)
	at org.kframework.main.Main.nailMain(Main.java:79)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at com.martiansoftware.nailgun.NGSession.run(NGSession.java:331)

Should I try with the trunk of the k repository?

sdasgup3 commented

The TEST73 is using only integer and map sorts and the truck k repository should compile that. In order to compile the X86 semantics, which uses MInt sort (for bitvectors), the truck will not work and hence you should use my fork only.

So far it seems that irrespective of which K repo you are using, you are not able to compile a simple (using basic K builtins) program. It should get compiled using either of the two repos, which implies that the problem could be in the k build itself.

Let me get back to you after talking with the k tool experts here. In the meanwhile, I would encourage you to file an issue in the mainline k repository (they are pretty responsive) using the test example. I think they can infer what the problem is from the error message (incase they also cannot reproduce it)

  • 👍1
sdasgup3 commented

Can you please let us know the z3 --version that you are using?

andsanmar commented

I'm running Z3 version 4.5.1 - 64 bit

sdasgup3 commented

@andsanmar Can you please try out a newer version? The one I am using is Z3 version 4.8.6 - 64 bit. You may get the latest source from https://github.com/Z3Prover/z3.git.

sdasgup3 commented

Also, make sure that you tried https://github.com/sdasgup3/learning-K/tree/master/TEST73, other than https://github.com/sdasgup3/learning-K/tree/master/TEST72. As the names of the k files are exactly the same TEST.k, so it might happen that we are running only the TEST72/* twice and not the newer one TEST73/*. As I said, they use different operators and the output of kompile on both them is very informative.

dwightguth commented

I am unable to reproduce this error with z3 4.5.1 because such a version of z3 does not exist. Z3 went directly from 4.5.0 to 4.6.0.

  • 👍1
andsanmar commented

No idea where this z3 binary came from, I've compiled version 4.8.5 from sources and achieved to do the compilation of the semantics. Thanks!

  • 👍1