Goose  Check-in [98a85945f6]

    using namespace ir;
    using namespace llr;

    class Builder;

    extern z3::context& GetZ3Context();
    extern optional< z3::expr > BuildZ3ExprFromValue( Builder& b, const Value& val );
    extern optional< z3::expr > BuildZ3Op( Builder& b, const llr::Instruction& instr );
}

#include "builder.h"
#include "verifstmtvalidator.h"
#include "funcvalidator.h"

#endif

    }

    m_solver.add( z3::implies( *m_currentPredicate, e ) );
}

void Builder::addAssertion( const z3::expr e )
{
    m_haveAnyAssertion = true;

    if( !m_currentPredicate )
    {
        m_solver.add( !e );
        return;
    }

    m_solver.add( z3::implies( *m_currentPredicate, !e ) );

            Builder( z3::solver& solver ) :
                m_solver( solver )
            {}

            void addAssumption( const z3::expr e );
            void addAssertion( const z3::expr e );

            bool haveAnyAssertion() const { return m_haveAnyAssertion; }

        private:
            z3::solver& m_solver;

            // All emitted assumptions and assertions are wrapped
            // with implication 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;

            // Check if we actually emitted any assertion. If we didn't,
            // then we have no condition to prove, so just skip the checking.
            bool m_haveAnyAssertion = false;
    };
}

#endif

#include "analyze.h"
#include "builtins/builtins.h"
#include "diagnostics/diagnostics.h"

using namespace goose::analyze;
using namespace goose::diagnostics;

FuncValidator::FuncValidator( const builtins::Func& func ) :
    m_solver( GetZ3Context() ),
    m_builder( m_solver ),
    m_func( func )
{
    buildZ3Formula( func );
}

bool FuncValidator::validate()
{
    if( !m_builder.haveAnyAssertion() )
        return true;

    switch( m_solver.check() )
    {
        case z3::check_result::unsat:
            // We are using the solver to try and find a counter example,
            // so if it's unsat, it's good.
            return true;

        return true;
    } );

    const auto& llr = func.llr();
    const auto& cfg = llr->body();

    // For now, we assume that the BBs are already ordered so that each BB's dominating BB precedes it,
    // which should be the case due to the way if, while and shortcut eval operators are implemented.
    cfg->ForEachBB( [&]( auto&& bb )
    {
        buildFormulasForBB( bb );
    } );
}

void FuncValidator::buildFormulasForBB( const ptr< llr::BasicBlock >& bb )
{
    // TODO: setup the predicate for this basic block

    for( auto&& x : *bb )
        BuildZ3Op( m_builder, x );

    handleTerminator( *bb->terminator() );
}

void FuncValidator::handleTerminator( const llr::Terminator& t )
{
    return visit( [&]( auto&& t )
    {
        return handleTerminator( t );
    }, t.content() );
}

void FuncValidator::handleTerminator( const llr::Ret& t )
{
    // Emit the "ensures" expressions as assertions.
    const auto& reqs = m_func.type().verifInfos()->postAssertion();
    ForEachInVectorTerm( reqs, [&]( auto&& t )
    {
        // Don't do any error handling here, it should already have been taken care of
        // by VerifStmtValidator.
        if( auto z3expr = BuildZ3ExprFromValue( m_builder, *ValueFromIRExpr( t ) ) )
            m_builder.addAssertion( *z3expr );

        return true;
    } );
}

void FuncValidator::handleTerminator( const llr::Branch& t )
{
    // TODO - set the predicate of the target BB to be the same as the current BB's
}

void FuncValidator::handleTerminator( const llr::CondBranch& t )
{
    // TODO - set the predicate of the true BB to a z3expr generated from the condition,
    // and the predicate for the false BB to its negation
}

            FuncValidator( const builtins::Func& func );
            bool validate();

        private:
            void buildZ3Formula( const builtins::Func& func );
            void buildFormulasForBB( const ptr< llr::BasicBlock >& bb );

            void handleTerminator( const llr::Terminator& t );

            template< typename T >
            void handleTerminator( const T& t )
            {}

            void handleTerminator( const llr::Ret& t );
            void handleTerminator( const llr::Branch& t );
            void handleTerminator( const llr::CondBranch& t );

            z3::solver m_solver;
            Builder m_builder;

            const builtins::Func& m_func;

            // For now we don't attempt to handle loops. We only keep track
            // of which basic blocks we already converted to formulas to avoid
            // doing them again.
            unordered_set< uint32_t > m_convertedBBIndices;
    };
}

goose_analyze = library( 'goose-analyze',
    'analyze.cpp',
    'value.cpp',
    'builder.cpp',
    'verifstmtvalidator.cpp',
    'funcvalidator.cpp',

    include_directories: bsinc,
    dependencies: [fmt_dep, z3_dep]
)

            // calls to DestroyValue() may also have requirements to enforce, so we'll need to emit
            // the eventual implicit return first.
            p.destroyAllLiveValues();
            p.emitTerminator( llr::Ret() );
        }

        pFuncLLR->body() = cfg;

        analyze::FuncValidator fv( f );
        return fv.validate();
    }

    Term BuildArgListForCall( const FuncType& ft, const Term& unifiedArgs )
    {
        auto av = make_shared< Vector >();
        av->reserve( VecSize( ft.params() ) );