Goose  call.cpp at [0db147f117]

File bs/verify/call.cpp artifact a001b6bb59 part of check-in 0db147f117

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

using namespace goose::diagnostics;

namespace goose::verify
{
    template< bool CheckResult, typename I > bool BuildZ3CallCheck( Builder& b, const I& instr )
    {
        Value ft;

        auto fVal = b.pop< Value >();
        if( fVal )
            ft = *EIRToValue( fVal->type() );
        else
        {
            auto zv = b.pop< Z3Val >();
            if( !zv )
                return false;
            ft = zv->type;
        }

        auto fvd = builtins::ExtractFuncVerifData( ft );
        if( !fvd )
            return false;

        optional< Z3Val > retExpr;

        if constexpr( CheckResult )
        {
            if( fvd->returnType != GetValueType< void >() )
                retExpr =
                    BuildZ3ConstantFromType( b, fvd->returnType, format( "r{}", b.newUniqueId() ) );
        }

        auto fvi = fvd->verifInfos;
        if( !fvi )
        {
            if( retExpr )
                b.push( move( *retExpr ) );
            return true;
        }

        // Create a temporary builder to construct the z3 expressions out of the
        // function's pre-conditions and postconditions, configured
        // to perform the necessary replacements for arguments and for the
        // return value placeholder.
        Builder cb = b;

        // Inject the arguments in the context.
        // They will be picked up by getVars instructions when refered to
        // by the verification conditions.
        uint32_t argCount = instr.numArgs();
        cb.resetVarStorage( argCount );

        for( uint32_t argIndex = 0; argIndex < argCount; ++argIndex )
        {
            auto zv = b.pop();
            if( !zv )
                return false;

            cb.setVar( argCount - argIndex - 1, move( *zv ) );
        }

        // Asserts the parameter types's predicates.
        uint32_t varId = 0;

        ForEachInVectorTerm( fvd->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, VarAddr( varId++, locId ), Load( type, locId ) );

                auto zv = BuildZ3ExprFromValue( cb, paramVal );
                ForEachPredicate( cb, type, zv.expr,
                    [&]( auto&& z3expr, auto locId )
                    {
                        DiagnosticsContext dc( fVal->locationId(), "At this call." );
                        b.checkAssertion( z3expr, locId );
                    } );

                return true;
            } );

        if constexpr( CheckResult )
        {
            // Setup the return value placeholder
            if( retExpr )
                cb.setPlaceholder( "@result"_sid, retExpr->expr );
        }

        // Check preconditions.
        const auto& preConds = fvi->preConds();
        preConds->forEach(
            [&]( auto&& val )
            {
                if( auto zv = TryBuildZ3ExprFromValue( cb, val ) )
                {
                    DiagnosticsContext dc( fVal->locationId(), "At this call." );
                    b.checkAssertion( zv->expr, val.locationId() );
                }
            } );

        if constexpr( CheckResult )
        {
            // Add the return type's predicates as assumptions.
            ForEachPredicate( cb, fvd->returnType, retExpr->expr,
                [&]( auto&& z3expr, auto locId ) { b.assume( z3expr ); } );

            // Add postconditions as assumptions.
            const auto& postConds = fvi->postConds();
            postConds->forEach(
                [&]( auto&& val )
                {
                    if( auto zv = TryBuildZ3ExprFromValue( cb, val ) )
                        b.assume( zv->expr );
                } );

            if( retExpr )
                b.push( move( *retExpr ) );
        }

        return true;
    }

    bool BuildZ3Op( Builder& b, const Call& instr )
    {
        return BuildZ3CallCheck< true >( b, instr );
    }

    bool BuildZ3Op( Builder& b, const CallCheck& instr )
    {
        return BuildZ3CallCheck< false >( b, instr );
    }
} // namespace goose::verify