Goose  Artifact [a54919b03d]

Artifact a54919b03d09baef8114a824a3357646407852def3ea5aaf2aa282944c538ee6:

• File bs/verify/builder.h — part of check-in [bf81e30984] at 2021-09-18 17:00:20 on branch trunk —
  • Refactored LocationId into a separate class and actually use it everywhere instead of uint32_t, this makes it easier to make generic wrappers for APIs
  • g0 api: more work on the CIR api
  (user: achavasse size: 4304)

#ifndef GOOSE_VERIFY_BUILDER_H
#define GOOSE_VERIFY_BUILDER_H

namespace goose::builtins
{
    class Func;
}

namespace goose::verify
{
    using AssHandler = function< bool ( const z3::expr&, const z3::expr&, LocationId ) >;

    // Helper class that tracks the states of a few things
    // to build z3 expressions from a cfg.
    class Builder
    {
        friend class AssertionHandlerGuard;

        public:
            Builder( const sema::Context& c, z3::solver& solver, Remapper* remapper = nullptr ) :
                m_context( &c ),
                m_solver( &solver ),
                m_remapper( remapper )
            {}

            const auto& context() const { return *m_context; }
            auto* solver() { return m_solver; }
            auto* remapper() { return m_remapper; }
            uint32_t currentBBIndex() const { return m_currentBBIndex; }

            void setTraceMode( bool b ) { m_traceMode = b; }

            void setCFG( const ptr< cir::CFG >& cfg )
            {
                m_cfg = cfg;
            }

            void setCurrentBB( uint32_t index )
            {
                m_currentBBIndex = index;
            }

            void setCurrentPredicate( const optional< z3::expr >& predicate )
            {
                m_currentPredicate = predicate;
            }

            void add( const z3::expr& e );
            void assume( const z3::expr& e );
            bool checkAssertion( const z3::expr& e, LocationId locationId );

            optional< Z3Val > retrieveVar( uint32_t index, uint32_t bbIndex = ~0 );
            optional< Z3Val > setVar( uint32_t index, const Value& val );
            const Z3Val& setVar( uint32_t index, Z3Val&& v );

            const z3::expr* retrievePlaceholder( StringId sid ) const;
            void setPlaceholder( StringId sid, const z3::expr& expr );

            uint32_t newUniqueId() { return m_nextUniqueId++; }

            bool hasCheckFailed() const { return m_checkFailed; }

            template< typename F >
            void setAssertionHandler( F&& handler )
            {
                m_assertionHandler = forward< F >( handler );
            }

            Z3Val& setVarForBasicBlock( uint32_t bbIndex, uint32_t index, Z3Val&& v );

        private:
            optional< Z3Val > getVarForBasicBlock( uint32_t bbIndex, uint32_t index ) const;

            const sema::Context* m_context;
            z3::solver* m_solver = nullptr;
            Remapper* m_remapper = nullptr;

            ptr< cir::CFG > m_cfg;
            uint32_t m_currentBBIndex = 1;

            // All emitted assumptions and assertions are wrapped
            // with implications from this predicate.
            // This is used to model the control flow, where each
            // basic block gets a predicate that indicates that
            // the execution flow is going through that block.
            optional< z3::expr > m_currentPredicate;

            AssHandler m_assertionHandler;

            // For each variable and temporary, store its last value as a z3 expression.
            using VarState = llvm::SmallVector< optional< Z3Val >, 16 >;
            using VarStorage = cir::TempStorage< VarState >;

            VarStorage m_varStorage;
            unordered_map< StringId, z3::expr > m_placeholders;

            // TODO: investigate why this not being static breaks things, since it should
            // be saved and restored whenever the solver is, but apparently it causes name collisions
            // that invalidate the formulas. This works fine like this but it makes z3 formulas dumps
            // less readable (due to super large variable name indices) and dependent on function checking order.
            static uint32_t m_nextUniqueId;

            bool m_checkFailed = false;
            bool m_traceMode = false;
    };

    class AssertionHandlerGuard
    {
        public:
            AssertionHandlerGuard( Builder& b ) :
                m_builder( b ),
                m_savedAssHandler( b.m_assertionHandler )
            {}

            ~AssertionHandlerGuard()
            {
                m_builder.m_assertionHandler = m_savedAssHandler;
            }

        private:
            Builder&    m_builder;
            AssHandler  m_savedAssHandler;
    };
}

#endif