search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
210 stars 42 forks source link

Un-evaluated #if #then #else #1779

Closed ttuegel closed 4 years ago

ttuegel commented 4 years ago

This test exhibits a failure to evaluate #if #then #else using the solver.

The test needs, at least, the smtlib attribute replaced by smt-hook.

The final configuration reached is:

/* Created: Kore.Exec.toTermLike */
/* Spu */
\and{SortGeneratedTopCell{}}(
    /* Fn Sfc */
    Lbl'-LT-'generatedTop'-GT-'{}(
        /* Fn Sfc */
        Lbl'-LT-'k'-GT-'{}(
            /* Fn Sfc */
            append{}(
                /* Fn Sfc */
                Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortK{}}(
                    /* Fn Sfa */
                    Lbl'UndsEqlsEqls'Int'Unds'{}(
                        /* Fn Sfa */
                        Lblsign'LParUndsCommUndsRParUnds'A'Unds'Int'Unds'Int'Unds'Int{}(
                            /* Fl Fn D Sfa Cl */
                            /* builtin: */ \dv{SortInt{}}("7"),
                            /* Fn Sfa */
                            Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                                /* Fl Fn D Sfa Cl */
                                /* builtin: */ \dv{SortInt{}}("0")
                            )
                        ),
                        /* Fn Sfa */
                        Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                            /* Fl Fn D Sfa */ VarSignatures:SortIMap{},
                            /* Fl Fn D Sfa Cl */
                            /* builtin: */ \dv{SortInt{}}("0")
                        )
                    ),
                    /* Fl Fn D Sfa Cl */ dotk{}(),
                    /* Fl Fn D Sfa Cl */
                    kseq{}(
                        /* Fl Fn D Sfa Cl */
                        Lbl'Hash'bottom'Unds'A'Unds'KItem{}(),
                        /* Fl Fn D Sfa Cl */ dotk{}()
                    )
                ),
                /* Fl Fn D Sfa */
                kseq{}(
                    /* Fl Fn D Sfa */
                    LblvalidateSignatures'LParUndsCommUndsCommUndsCommUndsRParUnds'A'Unds'KItem'Unds'Int'Unds'Int'Unds'IMap'Unds'IMap{}(
                        /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1"),
                        /* Fl Fn D Sfa */ VarN:SortInt{},
                        /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                        /* Fl Fn D Sfa */ VarSignatures:SortIMap{}
                    ),
                    /* Fl Fn D Sfa */ VarDotVar1:SortK{}
                )
            )
        ),
        /* Fl Fn D Sfa */
        Lbl'-LT-'generatedCounter'-GT-'{}(
            /* Fl Fn D Sfa */ VarDotVar00:SortInt{}
        )
    ),
    /* Created: Kore.Internal.Predicate.makeAndPredicate */
    /* Sfc */
    \and{SortGeneratedTopCell{}}(
        /* Created: Kore.Internal.Predicate.makeAndPredicate */
        /* Sfc */
        \and{SortGeneratedTopCell{}}(
            /* Created: Kore.Internal.Predicate.makeAndPredicate */
            /* Sfa */
            \and{SortGeneratedTopCell{}}(
                /* Sfa */
                \equals{SortBool{}, SortGeneratedTopCell{}}(
                    /* Fl Fn D Sfa */
                    Lbl'Unds-LT-'Int'Unds'{}(
                        /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0"),
                        /* Fl Fn D Sfa */ VarN:SortInt{}
                    ),
                    /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true")
                ),
                /* Sfa */
                \equals{SortBool{}, SortGeneratedTopCell{}}(
                    /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true"),
                    /* Fl Fn D Sfa */
                    Lbl'Unds-GT-Eqls'Int'Unds'{}(
                        /* Fl Fn D Sfa */ VarN:SortInt{},
                        /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
                    )
                )
            ),
            /* Sfc */
            \equals{SortBool{}, SortGeneratedTopCell{}}(
                /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true"),
                /* Fn Sfc */
                Lblforall'LParUndsCommUndsCommUndsCommUndsRParUnds'A'Unds'Bool'Unds'KVar'Unds'Int'Unds'Int'Unds'Bool{}(
                    /* Fl Fn D Sfa Cl */
                    \dv{SortKVar{}}(/* Fl Fn D Sfa Cl */ "x"),
                    /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0"),
                    /* Fl Fn D Sfa */ VarN:SortInt{},
                    /* Fn Sfa */
                    Lbl'UndsEqlsEqls'Int'Unds'{}(
                        /* Fn Sfa */
                        Lblsign'LParUndsCommUndsRParUnds'A'Unds'Int'Unds'Int'Unds'Int{}(
                            /* Fl Fn D Sfa Cl */
                            /* builtin: */ \dv{SortInt{}}("7"),
                            /* Fn Sfa */
                            Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                                /* Fl Fn D Sfa Cli */
                                /* Inj: */ inj{SortKVar{}, SortInt{}}(
                                    /* Fl Fn D Sfa Cl */
                                    \dv{SortKVar{}}(/* Fl Fn D Sfa Cl */ "x")
                                )
                            )
                        ),
                        /* Fn Sfa */
                        Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                            /* Fl Fn D Sfa */ VarSignatures:SortIMap{},
                            /* Fl Fn D Sfa Cli */
                            /* Inj: */ inj{SortKVar{}, SortInt{}}(
                                /* Fl Fn D Sfa Cl */
                                \dv{SortKVar{}}(/* Fl Fn D Sfa Cl */ "x")
                            )
                        )
                    )
                )
            )
        ),
        /* Sfc */
        \not{SortGeneratedTopCell{}}(
            /* Created: Kore.Internal.Predicate.makeAndPredicate */
            /* Sfc */
            \and{SortGeneratedTopCell{}}(
                /* Created: Kore.Internal.Predicate.makeAndPredicate */
                /* Sfc */
                \and{SortGeneratedTopCell{}}(
                    /* Created: Kore.Internal.Predicate.makeAndPredicate */
                    /* Sfa */
                    \and{SortGeneratedTopCell{}}(
                        /* Created: Kore.Internal.Predicate.makeAndPredicate */
                        /* Sfa */
                        \and{SortGeneratedTopCell{}}(
                            /* Sfa */
                            \ceil{SortInt{}, SortGeneratedTopCell{}}(
                                /* Fn Sfa */
                                Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                    /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                                    /* Fl Fn D Sfa Cl */
                                    /* builtin: */ \dv{SortInt{}}("0")
                                )
                            ),
                            /* Sfa */
                            \ceil{SortInt{}, SortGeneratedTopCell{}}(
                                /* Fn Sfa */
                                Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                    /* Fl Fn D Sfa */ VarSignatures:SortIMap{},
                                    /* Fl Fn D Sfa Cl */
                                    /* builtin: */ \dv{SortInt{}}("0")
                                )
                            )
                        ),
                        /* Sfa */
                        \ceil{SortInt{}, SortGeneratedTopCell{}}(
                            /* Fn Sfa */
                            Lblsign'LParUndsCommUndsRParUnds'A'Unds'Int'Unds'Int'Unds'Int{}(
                                /* Fl Fn D Sfa Cl */
                                /* builtin: */ \dv{SortInt{}}("7"),
                                /* Fn Sfa */
                                Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                    /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                                    /* Fl Fn D Sfa Cl */
                                    /* builtin: */ \dv{SortInt{}}("0")
                                )
                            )
                        )
                    ),
                    /* Sfc */
                    \ceil{SortK{}, SortGeneratedTopCell{}}(
                        /* Fn Sfc */
                        append{}(
                            /* Fn Sfc */
                            Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortK{}}(
                                /* Fn Sfa */
                                Lbl'UndsEqlsEqls'Int'Unds'{}(
                                    /* Fn Sfa */
                                    Lblsign'LParUndsCommUndsRParUnds'A'Unds'Int'Unds'Int'Unds'Int{}(
                                        /* Fl Fn D Sfa Cl */
                                        /* builtin: */ \dv{SortInt{}}("7"),
                                        /* Fn Sfa */
                                        Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                            /* Fl Fn D Sfa */
                                            VarKeys:SortIMap{},
                                            /* Fl Fn D Sfa Cl */
                                            /* builtin: */ \dv{SortInt{}}("0")
                                        )
                                    ),
                                    /* Fn Sfa */
                                    Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                        /* Fl Fn D Sfa */
                                        VarSignatures:SortIMap{},
                                        /* Fl Fn D Sfa Cl */
                                        /* builtin: */ \dv{SortInt{}}("0")
                                    )
                                ),
                                /* Fl Fn D Sfa Cl */ dotk{}(),
                                /* Fl Fn D Sfa Cl */
                                kseq{}(
                                    /* Fl Fn D Sfa Cl */
                                    Lbl'Hash'bottom'Unds'A'Unds'KItem{}(),
                                    /* Fl Fn D Sfa Cl */ dotk{}()
                                )
                            ),
                            /* Fl Fn D Sfa */
                            kseq{}(
                                /* Fl Fn D Sfa */
                                LblvalidateSignatures'LParUndsCommUndsCommUndsCommUndsRParUnds'A'Unds'KItem'Unds'Int'Unds'Int'Unds'IMap'Unds'IMap{}(
                                    /* Fl Fn D Sfa Cl */
                                    /* builtin: */ \dv{SortInt{}}("1"),
                                    /* Fl Fn D Sfa */ VarN:SortInt{},
                                    /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                                    /* Fl Fn D Sfa */ VarSignatures:SortIMap{}
                                ),
                                /* Fl Fn D Sfa */ VarDotVar1:SortK{}
                            )
                        )
                    )
                ),
                /* Sfc */
                \equals{SortK{}, SortGeneratedTopCell{}}(
                    /* Fl Fn D Sfa */ VarDotVar1:SortK{},
                    /* Fn Sfc */
                    append{}(
                        /* Fn Sfc */
                        Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortK{}}(
                            /* Fn Sfa */
                            Lbl'UndsEqlsEqls'Int'Unds'{}(
                                /* Fn Sfa */
                                Lblsign'LParUndsCommUndsRParUnds'A'Unds'Int'Unds'Int'Unds'Int{}(
                                    /* Fl Fn D Sfa Cl */
                                    /* builtin: */ \dv{SortInt{}}("7"),
                                    /* Fn Sfa */
                                    Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                        /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                                        /* Fl Fn D Sfa Cl */
                                        /* builtin: */ \dv{SortInt{}}("0")
                                    )
                                ),
                                /* Fn Sfa */
                                Lbl'UndsLSqBUndsRSqBUnds'A'Unds'Int'Unds'IMap'Unds'Int{}(
                                    /* Fl Fn D Sfa */ VarSignatures:SortIMap{},
                                    /* Fl Fn D Sfa Cl */
                                    /* builtin: */ \dv{SortInt{}}("0")
                                )
                            ),
                            /* Fl Fn D Sfa Cl */ dotk{}(),
                            /* Fl Fn D Sfa Cl */
                            kseq{}(
                                /* Fl Fn D Sfa Cl */
                                Lbl'Hash'bottom'Unds'A'Unds'KItem{}(),
                                /* Fl Fn D Sfa Cl */ dotk{}()
                            )
                        ),
                        /* Fl Fn D Sfa */
                        kseq{}(
                            /* Fl Fn D Sfa */
                            LblvalidateSignatures'LParUndsCommUndsCommUndsCommUndsRParUnds'A'Unds'KItem'Unds'Int'Unds'Int'Unds'IMap'Unds'IMap{}(
                                /* Fl Fn D Sfa Cl */
                                /* builtin: */ \dv{SortInt{}}("1"),
                                /* Fl Fn D Sfa */ VarN:SortInt{},
                                /* Fl Fn D Sfa */ VarKeys:SortIMap{},
                                /* Fl Fn D Sfa */ VarSignatures:SortIMap{}
                            ),
                            /* Fl Fn D Sfa */ VarDotVar1:SortK{}
                        )
                    )
                )
            )
        )
    )
)

The solver transcript shows no indication that the quantified side condition is ever sent to the solver.

ttuegel commented 4 years ago

Duplicate of #1962.