SMT Lemma not being added to solver

[dwightguth]

I am working on getting the C semantics working with the haskell backend and have run into a problem where a branch is not being pruned because it is unable to prove that a particular path constraint is unsatisfiable. It ought to be able to do this, but for some reason two of the four smt lemmas I wrote are not actually making it to the solver.

Here is part of the path constraint that ought to simplify to \bottom:

                                                                            /* Fl Fn D Sfa */
                                                                            LbladdressOfEntity'LParUndsCommUndsRParUnds'C-EXECUTION-ADDRESSES-SYNTAX'Unds'Int'Unds'EntityId'Unds'Int{}(
                                                                                /* Fl Fn D Sfa Cl */
                                                                                Lblexternal'LParUndsRParUnds'C-ENTITY-SYNTAX'Unds'EntityId'Unds'Identifier{}(
                                                                                    /* Fl Fn D Sfa Cli */
                                                                                    /* Inj: */ inj{SortId{}, SortIdentifier{}}(
                                                                                        /* Fl Fn D Sfa Cl */
                                                                                        \dv{SortId{}}(/* Fl Fn D Sfa Cl */
                                                                                        "main")
                                                                                    )
                                                                                ),
                                                                                /* Fl Fn D Sfa Cl */
                                                                                \dv{SortInt{}}("1")
                                                                            ),
                                                                            /* Fl Fn D Sfa */
                                                                            LbladdressOfEntity'LParUndsCommUndsRParUnds'C-EXECUTION-ADDRESSES-SYNTAX'Unds'Int'Unds'EntityId'Unds'Int{}(
                                                                                /* Fl Fn D Sfa Cl */
                                                                                Lblunique'LParUndsCommUndsCommUndsRParUnds'C-ENTITY-SYNTAX'Unds'EntityId'Unds'String'Unds'String'Unds'Int{}(
                                                                                    /* Fl Fn D Sfa Cl */
                                                                                    \dv{SortString{}}("2d6c80b9-afa9-4afd-bcb2-37c3db8fe6c5"),
                                                                                    /* Fl Fn D Sfa Cl */
                                                                                    \dv{SortString{}}(".str.6d61696e00"),
                                                                                    /* Fl Fn D Sfa Cl */
                                                                                    \dv{SortInt{}}("0")
                                                                                ),
                                                                                /* Fl Fn D Sfa Cl */
                                                                                \dv{SortInt{}}("5")
                                                                            )

Here is the lemma that ought to allow it to simplify:

  rule addressOfEntity(X, Len) ==K addressOfEntity(X', Len') => false
    requires X =/=K X' andBool Len >Int 0 andBool Len' >Int 0 [simplification, smt-lemma]

I have confirmed this axiom shows up in definition.kore with the smt-lemma attribute. However, it does not show up in the solver transcript.

Here is the relevant extract of the solver transcript:

(assert (forall ((<2> Int ) (<0> Int ) (<1> Int ) ) (=> (= (distinct <0> <1> ) true ) (= (= (+ <2> <0> ) (+ <2> <1> ) ) false ) ) ) )
; success

(assert (forall ((<1> Int ) (<0> Int ) ) (=> (= (distinct <0> 0 ) true ) (= (= (+ <1> <0> ) <1> ) false ) ) ) )
; success

(check-sat )
; sat

(push 1 )
; success

(declare-fun <0> () |HB_SortEntityId| )
; success

(declare-fun <1> () |HB_SortEntityId| )
; success

(assert (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (+ (addressOfEntity <0> 5 ) 2 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (+ (addressOfEntity <0> 5 ) 3 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (+ (addressOfEntity <0> 5 ) 4 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (addressOfEntity <0> 5 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (+ (addressOfEntity <0> 5 ) 3 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (+ (addressOfEntity <0> 5 ) 4 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (addressOfEntity <0> 5 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 3 ) (+ (addressOfEntity <0> 5 ) 4 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 3 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 3 ) (addressOfEntity <0> 5 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 4 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 4 ) (addressOfEntity <0> 5 ) ) ) (not (= (addressOfEntity <1> 1 ) (addressOfEntity <0> 5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
; success

(check-sat )
; sat

(pop 1 )
; success

(push 1 )
; success

(declare-fun <0> () |HB_SortEntityId| )
; success

(declare-fun <1> () |HB_SortEntityId| )
; success

(assert (not (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (+ (addressOfEntity <0> 5 ) 2 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (+ (addressOfEntity <0> 5 ) 3 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (+ (addressOfEntity <0> 5 ) 4 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 1 ) (addressOfEntity <0> 5 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (+ (addressOfEntity <0> 5 ) 3 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (+ (addressOfEntity <0> 5 ) 4 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 2 ) (addressOfEntity <0> 5 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 3 ) (+ (addressOfEntity <0> 5 ) 4 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 3 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 3 ) (addressOfEntity <0> 5 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 4 ) (addressOfEntity <1> 1 ) ) ) (and (not (= (+ (addressOfEntity <0> 5 ) 4 ) (addressOfEntity <0> 5 ) ) ) (not (= (addressOfEntity <1> 1 ) (addressOfEntity <0> 5 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
; success

(check-sat )
; sat

The second constraint ought to be unsatisfiable, but the lemmas that would allow it to disprove some of the disjuncts are missing.

Attached is the bug report archive for this invocation of kore-exec.

It would be really nice if an smt-lemma being unable to be translated was an error that told you why it was unable to be translated rather than the lemma just mysteriously not being used. kore-exec.tar.gz

[dwightguth]

This is the definition of addressOfEntity:

  syntax Int ::= addressOfEntity(EntityId, len: Int) [function, functional, smtlib(addressOfEntity), no-evaluators]

[dwightguth]

This turns out to be because of the presence of ==K, which the smt translator doesn't currently support. The best fix would be to modify the frontend and llvm backend so that ==K is parametric in its argument sort.

[ana-pantilie]

Look into if the backend supports ^.

[ana-pantilie]

@dwightguth The two LbladdressOfEntity seem to be the arguments of something. What exactly is that something? Why did you write the smt-lemma in that specific way, using ==K?

Also, is this issue still blocking/relevant?

[dwightguth]

This issue is no longer relevant.