Goose  Artifact [d175cde7f1]

Artifact d175cde7f139b815d95df957ea86c62413ca0473c587234625743a535185c909:

• File bs/verify/func.cpp — part of check-in [54ef60956e] at 2020-06-05 18:57:03 on branch trunk — Verifier: loops: instead of tracking and havocing modified variables during loops, track modified addresses, so that modifying only some fields of a tuple will not result in forgetting everything about the other fields. (user: achavasse size: 5604)

#include "verify.h"
#include "builtins/builtins.h"
#include "diagnostics/diagnostics.h"
#include "helpers.inl"

using namespace goose::diagnostics;

namespace goose::verify
{
    bool Func::ms_TraceMode = false;
    bool Func::ms_DumpSolverOnFailure = false;
    bool Func::ms_DumpSolverOnSuccess = false;

    Func::Func( const sema::Context& c, const builtins::Func& func ) :
        m_func( &func ),
        m_cfg( func.llr()->body() ),
        m_solver( GetZ3Context() ),
        m_remapper( m_cfg->count() + 1 ),
        m_builder( c, m_solver, &m_remapper )
    {}

    Func::Func( const sema::Context& c, const ptr< llr::CFG >& cfg ) :
        m_cfg( cfg ),
        m_solver( GetZ3Context() ),
        m_remapper( m_cfg->count() + 1 ),
        m_builder( c, m_solver, &m_remapper )
    {}

    bool Func::verify()
    {
        ComputeLoops( m_cfg );
        ComputeLoopModifiedAddrs( m_cfg );

        try
        {
            // Enable the new z3 arith solver because the old one from recent versions of z3
            // is apparently shitting the bed in some tests. ¯\_(ツ)_/¯
            m_solver.set( "arith.solver", 6U );

            bool success = true;

            m_builder.setTraceMode( ms_TraceMode );
            if( ms_TraceMode )
                cout << "=== Begin function verification trace ===\n";

            m_builder.setAssertionHandler( [&]( auto&& expr, auto&& exprToCheck, uint32_t locationId )
            {
                return checkAssertion( expr, exprToCheck, locationId );
            } );

            m_builder.setCFG( m_cfg );

            if( m_func )
            {
                // Add assumptions of the function's parameter types predicates
                uint32_t varId = 0;

                ForEachInVectorTerm( m_func->type().params(), [&]( auto&& param )
                {
                    auto result = Decompose( param,
                        Vec(
                            Lit( "value"_sid ),
                            Lit( "param"_sid ),
                            SubTerm(),
                            SubTerm(),
                            Val< LocationId >()
                        )
                    );

                    if( !result )
                        return true;

                    auto&& [type, val, locId] = *result;
                    auto paramVal = BuildComputedValue( type, llr::Load( llr::VarAddress( varId ), type ) );

                    // Initialize every parameter containing variable with an freshly named constant of the right type.
                    if( auto paramInit = BuildZ3ConstantFromType( m_builder.context(), type, format( "p{}", varId ) ) )
                        m_builder.setVar( varId, move( *paramInit ) );

                    ++varId;

                    if( auto zv = BuildZ3ExprFromValue( m_builder, paramVal ) )
                    {
                        ForEachPredicate( m_builder, type, zv->expr, [&]( auto&& z3expr, auto locId )
                        {
                            m_builder.assume( z3expr );
                        } );
                    }

                    return true;
                } );

                // Add assumptions of the function's requirements
                const auto& reqs = m_func->type().verifInfos()->preConditions();
                ForEachInVectorTerm( reqs, [&]( auto&& t )
                {
                    // Don't do any error handling here, it should already have been taken care of
                    // by the condition verifier.
                    if( auto zv = BuildZ3ExprFromValue( m_builder, *ValueFromIRExpr( t ) ) )
                        m_builder.assume( zv->expr );

                    return true;
                } );
            }

            bool result = buildZ3Expressions( *m_cfg->entryBB(), nullptr );

            if( ms_TraceMode )
                cout << "=== End function verification trace ===\n\n";

            return result;
        }
        catch( z3::exception e )
        {
            cerr << "Func: z3 exception: " << e << endl;

            // rethrow so we get a stack trace dump to know where the error happened
            throw;
        }
    }

    bool Func::checkAssertion( const z3::expr& expr, const z3::expr& exprToCheck, uint32_t locationId )
    {
        if( ms_TraceMode )
            return true;

        z3::expr_vector exprVec( GetZ3Context() );
        exprVec.push_back( exprToCheck );

        switch( m_solver.check( exprVec ) )
        {
            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.

                if( ms_DumpSolverOnSuccess )
                    cout << "Solver dump:\n" << m_solver << "check_unsat: " << exprToCheck << endl << endl;

                return true;

            case z3::check_result::sat:
                DiagnosticsManager::GetInstance().emitErrorMessage( locationId, "assert"_sid,
                    "this condition may not be met." );

                if( ms_DumpSolverOnFailure )
                    cout << "Solver dump:\n" << m_solver << "check_unsat: " << exprToCheck << endl << endl;

                return false;

            default:
                DiagnosticsManager::GetInstance().emitErrorMessage( locationId, "assert"_sid,
                    "couldn't verify this condition." );

                if( ms_DumpSolverOnFailure )
                    cout << "Solver dump:\n" << m_solver << "check_unsat: " << exprToCheck << endl << endl;

                return false;
        }
    }
}