[K-Bug] Internal error for nested private imports

[virgil-serbanuta]

What component is the issue in?

Front-End

Which command

• [X] kompile
• [ ] kast
• [ ] krun
• [ ] kprove
• [ ] kprovex
• [ ] ksearch

What K Version?

v5.5.40-0-g98574f12a2-dirty

Operating System

Linux

K Definitions (If Possible)

c.k:

module A
  syntax A ::= "a"
endmodule

module B
  imports private A

  syntax C ::= B
             | A
  syntax B ::= "b"

  syntax B ::= f(C)  [function, total]

endmodule

module C
  imports private B

  rule f(V:B) => V
  rule f(_) => "a" [owise]
endmodule

Steps to Reproduce

kompile c.k --backend haskell

Will display:

[Error] Internal: Unexpected result from z3: (error "line 44 column 13: unknown
constant SortA")
        Source(/.../c.k)
        Location(19,8,19,19)
        19 |      rule f(V:B) => V
           .           ^~~~~~~~~~~

Expected Results

Kompile be able to compile that file. Or, in the worst case, it should provide a decent error message.

[radumereuta]

I did a timeboxed investigation and there seems to be a problem in the way we calculate the sentences in a module. Should probably be something like this:

  private lazy val importedSentences = fullImports flatMap {_.publicSentences}

  lazy val publicSentences: Set[Sentence] = publicLocalSentences | imports.filter(_.isPublic).flatMap(_.module.publicSentences)
  lazy val sentences: Set[Sentence] = localSentences | importedSentences

But then there is also another issue in RuleGrammarGenerator since by the time we get to the end of the generator we have way too many sentences.

[ehildenb]

A couple weird things:

• Original definition uses "a" on the RHS of a rule, it should be just a?
• Why are we seeing SortA being sent to the SMT solver when it's not involved in the rule in question?
• Why is SortA being sent to the SMT solver without being declared?

[virgil-serbanuta]

Yes, "a" was a mistake. You get the same error if you remove the last rule or if you change it to

  rule f(_) => b [owise]

[ehildenb]

@virgil-serbanuta is this blocking?

[virgil-serbanuta]

No.