k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] how to kompile for java-symbolic backend?

From: Andrei Stefanescu <andreistef AT gmail.com>
To: Ömer Sinan Ağacan <omeragacan AT gmail.com>
Cc: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
Subject: Re: [K-user] how to kompile for java-symbolic backend?
Date: Mon, 23 Sep 2013 15:57:16 -0500
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

Yeah, that is correct (the description may need updating). As for the Exception, you have to give me more details (it is a feature that my backend does not support.

Andrei

On Mon, Sep 23, 2013 at 3:28 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

Interesting. in kompile --help ml parameter is described as:

-ml,--matching-logic generate support for matching logic
prover

Is this correct?

Also, kompilation fails with null pointer exception:

➜ lua-semantics git:(master) ✗ kompile -ml -v lua
Including file: /home/omer/K/lua-semantics/lua.k
Including file: /home/omer/K/lua-semantics/lua-configuration.k
Including file: /home/omer/K/lua-semantics/lua-syntax.k
Including file: /home/omer/K/lua-semantics/lua-binop.k
Including file: /home/omer/K/k/dist/include/autoinclude.k
Including file: /home/omer/K/k/dist/include/k-prelude.k
Including file: /home/omer/K/k/dist/include/builtins/builtins.k
Including file: /home/omer/K/k/dist/include/builtins/bool.k
Including file: /home/omer/K/k/dist/include/builtins/int.k
Including file: /home/omer/K/k/dist/include/builtins/k-equal.k
Including file: /home/omer/K/k/dist/include/builtins/array.k
Including file: /home/omer/K/k/dist/include/builtins/float.k
Including file: /home/omer/K/k/dist/include/builtins/string.k
Including file: /home/omer/K/k/dist/include/builtins/id.k
Including file: /home/omer/K/k/dist/include/io/tcp.k
Including file: /home/omer/K/k/dist/include/builtins/random.k
Including file: /home/omer/K/k/dist/include/builtins/counter.k
Including file: /home/omer/K/k/dist/include/builtins/symbolic-k.k
Including file: /home/omer/K/k/dist/include/modules/substitution.k
Including file: /home/omer/K/k/dist/include/modules/pattern-matching.k
Including file: /home/omer/K/k/dist/include/io/uris.k
Basic Parsing = 334
Preprocess = 164
Checks = 10
File Gen Pgm = 37
Generate TBLPgm = 241
File Gen Def = 209
Generate TBLDef = 9229
Importing Files = 1170
Parsing Configs = 519
Parsing Rules = 4113
Serialize Definition to XML = 492
Check that configuration cells have unique names = 16
Remove brackets = 5
Add empty lists = 6
Remove syntactic casts = 4
class org.kframework.compile.checks.CheckVariables = 6
class org.kframework.compile.checks.CheckRewrite = 7
Set the sort of each variable to the inferred sort = 8
Subsort syntactic lists = 33
Serialize Compiled Definition to XML = 116
Strict Ops To Context = 3
Freeze User Freezers = 1
Contexts to Heating Rules = 3
Generate Heating Conditions = 1
java.lang.NullPointerException
at org.kframework.compile.transformers.DesugarStreams.newListItem(DesugarStreams.java:127)
at org.kframework.compile.transformers.DesugarStreams.makeStreamList(DesugarStreams.java:88)
at org.kframework.compile.transformers.DesugarStreams.transform(DesugarStreams.java:42)
at org.kframework.kil.Cell.accept(Cell.java:266)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:365)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:390)
at org.kframework.kil.Bag.accept(Bag.java:55)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:112)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:161)
at org.kframework.kil.Configuration.accept(Configuration.java:51)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:75)
at org.kframework.kil.Module.accept(Module.java:102)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:42)
at org.kframework.kil.Definition.accept(Definition.java:121)
at org.kframework.compile.utils.CompilerTransformerStep.compile(CompilerTransformerStep.java:24)
at org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:37)
at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:294)
at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:250)
at org.kframework.main.Main.main(Main.java:69)
Total = 16730
Number of Modules = 4
Number of Sentences = 20
Number of Productions = 86
Number of Cells = 9
➜ lua-semantics git:(master) ✗

---
Ömer Sinan Ağacan
http://osa1.net

2013/9/23 Andrei Stefanescu <andreistef AT gmail.com>:

> kompile -ml
>
> Andrei
>
>
>
> On Mon, Sep 23, 2013 at 3:06 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com>
> wrote:
>>
>> Hi all,
>>
>> How can I compile my K apps for java-symbolic backend?
>>
>> Thanks,
>>
>> ---
>> Ömer Sinan Ağacan
>> http://osa1.net
>>
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>
>

[K-user] how to kompile for java-symbolic backend?, Ömer Sinan Ağacan, 09/23/2013
- Re: [K-user] how to kompile for java-symbolic backend?, Andrei Stefanescu, 09/23/2013
  - Re: [K-user] how to kompile for java-symbolic backend?, Ömer Sinan Ağacan, 09/23/2013
    - Re: [K-user] how to kompile for java-symbolic backend?, Andrei Stefanescu, 09/23/2013
      - Re: [K-user] how to kompile for java-symbolic backend?, Ömer Sinan Ağacan, 09/23/2013
        
        Re: [K-user] how to kompile for java-symbolic backend?, Andrei Stefanescu, 09/23/2013