[Error] Internal: Uncaught exception thrown of type NoSuchElementException.

LaifsV1 commented 4 years ago

I was trying to compile a custom module that interacts with Z3 through system calls and encountered the error. This only happens in the llvm backend. The java backend compiles fine.

Any idea why this may happen?

Stack trace with the --debug option:

java.util.NoSuchElementException: None.get
    at scala.None$.get(Option.scala:349)
    at scala.None$.get(Option.scala:347)
    at org.kframework.backend.llvm.matching.Fringe.expand(Matrix.scala:248)
    at org.kframework.backend.llvm.matching.AHeuristic$.$anonfun$computeScoreForKey$4(Heuristics.scala:151)
    at org.kframework.backend.llvm.matching.AHeuristic$.$anonfun$computeScoreForKey$4$adapted(Heuristics.scala:150)
    at scala.collection.immutable.List.foreach(List.scala:389)
    at org.kframework.backend.llvm.matching.AHeuristic$.computeScoreForKey(Heuristics.scala:150)
    at org.kframework.backend.llvm.matching.AbstractColumn.computeScoreForKey(Matrix.scala:33)
    at org.kframework.backend.llvm.matching.AbstractColumn.computeScoreForKey$(Matrix.scala:17)
    at org.kframework.backend.llvm.matching.Column.computeScoreForKey(Matrix.scala:45)
    at org.kframework.backend.llvm.matching.Column.zeroOrHeuristic$2(Matrix.scala:79)
    at org.kframework.backend.llvm.matching.Column.$anonfun$computeScoreForKey$1(Matrix.scala:82)
    at org.kframework.backend.llvm.matching.Column.$anonfun$computeScoreForKey$1$adapted(Matrix.scala:82)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
    at scala.collection.immutable.List.foreach(List.scala:389)
    at scala.collection.TraversableLike.map(TraversableLike.scala:234)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:227)
    at scala.collection.immutable.List.map(List.scala:295)
    at org.kframework.backend.llvm.matching.Column.computeScoreForKey(Matrix.scala:82)
    at org.kframework.backend.llvm.matching.Column.computeScore(Matrix.scala:71)
    at org.kframework.backend.llvm.matching.Column.score$lzycompute(Matrix.scala:57)
    at org.kframework.backend.llvm.matching.Column.score(Matrix.scala:57)
    at org.kframework.backend.llvm.matching.Column.score(Matrix.scala:67)
    at org.kframework.backend.llvm.matching.MatrixColumn.score$lzycompute(Matrix.scala:42)
    at org.kframework.backend.llvm.matching.MatrixColumn.score(Matrix.scala:42)
    at org.kframework.backend.llvm.matching.Heuristic$.getBest(Heuristics.scala:27)
    at org.kframework.backend.llvm.matching.Matrix.bestColIx$lzycompute(Matrix.scala:447)
    at org.kframework.backend.llvm.matching.Matrix.bestColIx(Matrix.scala:442)
    at org.kframework.backend.llvm.matching.Matrix.compileInternal(Matrix.scala:623)
    at org.kframework.backend.llvm.matching.Matrix.compile(Matrix.scala:604)
    at org.kframework.backend.llvm.matching.Matching$.writeDecisionTreeToFile(Matching.scala:26)
    at org.kframework.backend.llvm.matching.Matching.writeDecisionTreeToFile(Matching.scala)
    at org.kframework.backend.llvm.LLVMBackend.accept(LLVMBackend.java:48)
    at org.kframework.kompile.KompileFrontEnd.run(KompileFrontEnd.java:74)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:62)
    at org.kframework.main.Main.runApplication(Main.java:118)
    at org.kframework.main.Main.runApplication(Main.java:108)
    at org.kframework.main.Main.main(Main.java:56)
[Error] Internal: Uncaught exception thrown of type NoSuchElementException
(NoSuchElementException: None.get)

dwightguth commented 4 years ago

Can you please run kore-parser $kompiledDir/definition.kore --no-print-definition and let me know if it reports any errors on the command line?

LaifsV1 commented 4 years ago

This reports the following error:

-bash: /Users/.../k/bin/kore-parser: cannot execute binary file

dwightguth commented 4 years ago

Can I see uname -a and file k/bin/kore-parser?

dwightguth commented 4 years ago

alternately, you can just share your definition.kore with me if you don't have any problem sharing the entire K definition you wrote publically. that file should be self contained enough for me to diagnose this issue, but it does contain a reversible representation of all the rules and syntax in your definition.

LaifsV1 commented 4 years ago

Sorry for the delayed response. Here's my K module:

require "substitution.k"

module Z3-SYNTAX
  imports SUBSTITUTION
  imports DOMAINS-SYNTAX
  imports INT-SYNTAX
  imports STRING

  syntax SMTLib ::= "(" "declare-const" KVar "Int" ")"
                  | "(" "declare-const" KVar "String" ")"
          | "(" "check-sat" ")"
          | "(" "get-model" ")"
                  | "(" "assert" SMTProp ")"
          | SMTLib SMTLib                       [left]
  syntax SMTProp ::= Bool | SMTVal
                   | "(" "<" SMTVal SMTVal ")"              [left]
                   | "(" ">" SMTVal SMTVal ")"              [left]
                   | "(" "<=" SMTVal SMTVal ")"              [left]
                   | "(" ">=" SMTVal SMTVal ")"              [left]
                   | "(" "/" SMTVal SMTVal ")"              [left]
           | "(" "*" SMTVal SMTVal ")"              [left]
                   | "(" "+" SMTVal SMTVal ")"              [left]
                   | "(" "-" SMTVal SMTVal ")"              [left]
                   | "(" "="   SMTProp SMTProp ")"          [left]
                   | "(" "and" SMTProp SMTProp ")"          [left]
                   | "(" "or"  SMTProp SMTProp ")"          [left]
           | "(" "not" SMTProp ")"                  [right]
                   | "(" "ite"  SMTProp SMTProp SMTProp ")" [left]
  syntax SMTVal  ::= KVar | Int

  syntax String ::= PropToString(SMTProp) [function]
  syntax String ::= PropToString(Bool) [function, functional, hook(STRING.token2string)]
  syntax String ::= XToString(SMTVal)  [function, functional, hook(STRING.token2string)]
  syntax String ::= XToString(Int) [function]
  rule XToString(I:Int) => Int2String(I)
  syntax String ::= PropToString(Int) [function]
  rule PropToString(I:Int) => Int2String(I)

  rule PropToString( ( < V1 V2 ) ) => "( < " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( > V1 V2 ) ) => "( > " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( <= V1 V2 ) ) => "( <= " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( >= V1 V2 ) ) => "( >= " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( * V1 V2 ) ) => "( * " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( / V1 V2 ) ) => "( / " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( + V1 V2 ) ) => "( + " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( - V1 V2 ) ) => "( - " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( = P1 P2 ) ) => "( = " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( and P1 P2 ) ) => "( and " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( or P1 P2 ) ) => "( or " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( not P1 ) ) => "( not " +String PropToString(P1) +String " )"
  rule PropToString( ( ite P1 P2 P3 ) ) => "( ite " +String PropToString(P1) +String " " +String PropToString(P2) +String " " +String PropToString(P3) +String " )"
  rule PropToString( true ) => "true"
  rule PropToString( false ) => "false"

  syntax String ::= LibToString(SMTLib)  [function]
  rule LibToString( ( declare-const X Int) ) => "( declare-const " +String XToString(X) +String " Int )"
  rule LibToString( ( check-sat ) ) => "( check-sat )"
  rule LibToString( ( get-model ) ) => "( get-model )"
  rule LibToString( ( assert P ) ) => "( assert " +String PropToString(P) +String " )"
  rule LibToString( P1 P2 ) => LibToString(P1) +String LibToString(P2)
endmodule

module Z3
  imports SUBSTITUTION
  imports Z3-SYNTAX
  imports DOMAINS
  imports STRING

  configuration <T>
          <k> $PGM:SMTLib </k>
        </T>

  syntax KResult ::= Bool  
  syntax Bool ::= CheckSAT(SMTLib)  [function]
  syntax Bool ::= SystemSAT(KItem)  [function,strict(1)]

  rule P:SMTLib => CheckSAT(P)

  rule CheckSAT(P) => SystemSAT(#system("echo \"" +String LibToString(P) +String "(check-sat)\" | z3 -in"))
  rule SystemSAT(#systemResult ( 0 , "sat\n" , "" )) => true
  rule SystemSAT(#systemResult ( 0 , "unsat\n" , "" )) => false
endmodule

It's called z3.k

dwightguth commented 4 years ago

I see a couple problems with this definition that make it ill formed. It should probably report a compiler error here, but some of these checks were not explicitly written and as a result, things just silently fail later on in the compilation pipeline. While you may be able to get this definition to work in the Java backend, it's still not correct K and writing things like this will eventually result in an error from the frontend preventing your code from being compiled at some point in the future:

It looks like you are trying to define overloaded functions in the form of Prop2String and XToString, but overloaded functions are not currently supported. You should define one production that takes the entire domain of the function, and if you need to declare a second production in order to implement the first function, treat it as an entirely separate function and call it explicitly where necessary.
It looks like you are trying to invoke the STRING.token2string hook with productions that have a sort as the argument that doesn't represent a token. For example, Bool and SMTVal. You should probably use #if to convert from a Bool to a String and explicitly call Int2String and KVar2String. I'm not sure we have implemented that last in the standard library, but if you define such a production and give it an argument sort of KVar and give it the token2string hook and it doesn't work, that is definitely something I can figure something out for.

dwightguth commented 4 years ago

Incidentally, associativity declarations do nothing when applied to a production that starts and ends with a terminal. Moreover, declaring associativity is not in any way necessary for disambiguation on such productions.

LaifsV1 commented 4 years ago

Thanks for the information. This is very helpful!

After making the changes to not use overloaded functions, I am still having trouble compiling. I get the same error reported as before.

I updated my syntax module accordingly, but I might not know what to look for. If it is convenient, could you point me in the right direction on what I might need to correct in it?

module Z3-SYNTAX
  imports SUBSTITUTION
  imports DOMAINS-SYNTAX
  imports INT-SYNTAX
  imports STRING

  syntax SMTLib ::= "(" "declare-const" KVar "Int" ")"
                  | "(" "declare-const" KVar "String" ")"
          | "(" "check-sat" ")"
          | "(" "get-model" ")"
                  | "(" "assert" SMTProp ")"
          | SMTLib SMTLib                       [left]
  syntax SMTProp ::= Bool | SMTVal
                   | "(" "<" SMTVal SMTVal ")"              
                   | "(" ">" SMTVal SMTVal ")"              
                   | "(" "<=" SMTVal SMTVal ")"              
                   | "(" ">=" SMTVal SMTVal ")"              
                   | "(" "/" SMTVal SMTVal ")"              
           | "(" "*" SMTVal SMTVal ")"              
                   | "(" "+" SMTVal SMTVal ")"              
                   | "(" "-" SMTVal SMTVal ")"              
                   | "(" "="   SMTProp SMTProp ")"          
                   | "(" "and" SMTProp SMTProp ")"          
                   | "(" "or"  SMTProp SMTProp ")"          
           | "(" "not" SMTProp ")"                  
                   | "(" "ite"  SMTProp SMTProp SMTProp ")" 
  syntax SMTVal  ::= KVar | Int

  syntax String ::= PropToString(SMTProp) [function]
  syntax String ::= BoolToString(Bool) [function, functional]
  syntax String ::= XToString(SMTVal)  [function, functional, hook(STRING.token2string)]

  rule XToString(I:Int) => Int2String(I)
  rule PropToString(I:Int) => Int2String(I)

  rule PropToString( ( < V1 V2 ) ) => "( < " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( > V1 V2 ) ) => "( > " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( <= V1 V2 ) ) => "( <= " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( >= V1 V2 ) ) => "( >= " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( * V1 V2 ) ) => "( * " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( / V1 V2 ) ) => "( / " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( + V1 V2 ) ) => "( + " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( - V1 V2 ) ) => "( - " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( = P1 P2 ) ) => "( = " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( and P1 P2 ) ) => "( and " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( or P1 P2 ) ) => "( or " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( not P1 ) ) => "( not " +String PropToString(P1) +String " )"
  rule PropToString( ( ite P1 P2 P3 ) ) => "( ite " +String PropToString(P1) +String " " +String PropToString(P2) +String " " +String PropToString(P3) +String " )"
  rule PropToString( B:Bool ) => BoolToString(B)

  rule BoolToString( true ) => "true"
  rule BoolToString( false ) => "false"

  syntax String ::= LibToString(SMTLib)  [function]
  rule LibToString( ( declare-const X Int) ) => "( declare-const " +String XToString(X) +String " Int )"
  rule LibToString( ( check-sat ) ) => "( check-sat )"
  rule LibToString( ( get-model ) ) => "( get-model )"
  rule LibToString( ( assert P ) ) => "( assert " +String PropToString(P) +String " )"
  rule LibToString( P1 P2 ) => LibToString(P1) +String LibToString(P2)
endmodule

dwightguth commented 4 years ago

I'm not sure if this is the source of the error or not, but offhand, I notice you're still setting the STRING.token2string hook on the SMTVal sort, which is not allowed.

dwightguth commented 4 years ago

I found a definition that works:

require "substitution.k"

module Z3-SYNTAX
  imports SUBSTITUTION
  imports DOMAINS-SYNTAX
  imports INT-SYNTAX
  imports STRING

  syntax SMTLib ::= "(" "declare-const" KVar "Int" ")"
                  | "(" "declare-const" KVar "String" ")"
                  | "(" "check-sat" ")"
                  | "(" "get-model" ")"
                  | "(" "assert" SMTProp ")"
                  | SMTLib SMTLib                           [left]
  syntax SMTProp ::= Bool | SMTVal
                   | "(" "<" SMTVal SMTVal ")"
                   | "(" ">" SMTVal SMTVal ")"
                   | "(" "<=" SMTVal SMTVal ")"
                   | "(" ">=" SMTVal SMTVal ")"
                   | "(" "/" SMTVal SMTVal ")"
                   | "(" "*" SMTVal SMTVal ")"
                   | "(" "+" SMTVal SMTVal ")"
                   | "(" "-" SMTVal SMTVal ")"
                   | "(" "="   SMTProp SMTProp ")"
                   | "(" "and" SMTProp SMTProp ")"
                   | "(" "or"  SMTProp SMTProp ")"
                   | "(" "not" SMTProp ")"
                   | "(" "ite"  SMTProp SMTProp SMTProp ")"
  syntax SMTVal  ::= KVar | Int

  syntax String ::= PropToString(SMTProp) [function]
  syntax String ::= BoolToString(Bool) [function, functional]
  syntax String ::= XToString(SMTVal)  [function, functional]
  syntax String ::= KVar2String(KVar) [function, functional, hook(STRING.token2string)]

  rule XToString(I:Int) => Int2String(I)
  rule XToString(K:KVar) => KVar2String(K)
  rule PropToString(I:Int) => Int2String(I)

  rule PropToString( ( < V1 V2 ) ) => "( < " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( > V1 V2 ) ) => "( > " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( <= V1 V2 ) ) => "( <= " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( >= V1 V2 ) ) => "( >= " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( * V1 V2 ) ) => "( * " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( / V1 V2 ) ) => "( / " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( + V1 V2 ) ) => "( + " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( - V1 V2 ) ) => "( - " +String XToString(V1) +String " " +String XToString(V2) +String " )"
  rule PropToString( ( = P1 P2 ) ) => "( = " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( and P1 P2 ) ) => "( and " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( or P1 P2 ) ) => "( or " +String PropToString(P1) +String " " +String PropToString(P2) +String " )"
  rule PropToString( ( not P1 ) ) => "( not " +String PropToString(P1) +String " )"
  rule PropToString( ( ite P1 P2 P3 ) ) => "( ite " +String PropToString(P1) +String " " +String PropToString(P2) +String " " +String PropToString(P3) +String " )"
  rule PropToString( B:Bool ) => BoolToString(B)

  rule BoolToString( true ) => "true"
  rule BoolToString( false ) => "false"

  syntax String ::= LibToString(SMTLib)  [function]
  rule LibToString( ( declare-const X Int) ) => "( declare-const " +String XToString(X) +String " Int )"
  rule LibToString( ( check-sat ) ) => "( check-sat )"
  rule LibToString( ( get-model ) ) => "( get-model )"
  rule LibToString( ( assert P ) ) => "( assert " +String PropToString(P) +String " )"
  rule LibToString( P1 P2 ) => LibToString(P1) +String LibToString(P2)
endmodule

module Z3
  imports SUBSTITUTION
  imports Z3-SYNTAX
  imports DOMAINS
  imports STRING

  configuration <T>
                  <k> $PGM:SMTLib </k>
                </T>

  syntax KResult ::= Bool
  syntax Bool ::= CheckSAT(SMTLib)  [function]
  syntax Bool ::= SystemSAT(KItem)  [function]

  rule P:SMTLib => CheckSAT(P)

  rule CheckSAT(P) => SystemSAT(#system("echo \"" +String LibToString(P) +String "(check-sat)\" | z3 -in"))
  rule SystemSAT(#systemResult ( _ , "sat\n" , _ )) => true
  rule SystemSAT(#systemResult ( _ , "unsat\n" , _ )) => false
endmodule

dwightguth commented 4 years ago

Esssentially, you had declared SystemSAT as strict, which is not allowed because it is a function.

LaifsV1 commented 4 years ago

Aaah. Thanks!

I thought I had to define it to be strict to evaluate the argument first. Are functions call by value and can't have their evaluation strategy changed?

dwightguth commented 4 years ago

Strictness is a way of transforming terms over a sequence of rewrite steps in order to evaluate expressions. Functions cannot be strict because they evaluate immediately rather than as a rewrite step, so the term that you pass to the function is what the function sees. If you have some expression you want to evaluate using strictness prior to calling a function on it, you need to first evaluate the expression using strictness, and /then/ call the function.

One common pattern you can use if you have a function that you want to call at the top of the k cell on an evaluated expression on the rhs of a rule is to define two symbols and make one strict and the other a function, like so:

syntax KItem ::= fooStrict(KItem) [strict]
syntax Foo ::= foo(Bar) [function]
rule fooStrict(B:Bar) => foo(B)

However, this is not necessary in your example. #system is a function and thus does not need to be evaluated via strictness in order for its result to be passed to SystemSat.

runtimeverification / k

[Error] Internal: Uncaught exception thrown of type NoSuchElementException. #1190