Goose  call.cpp at [477ef5b3d4]

File bs/verify/call.cpp artifact a8013dbf65 part of check-in 477ef5b3d4

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

using namespace goose::diagnostics;

namespace goose::verify
{
    optional< z3::expr > BuildZ3Op( Builder& b, const Call& instr )
    {
        auto func = FromValue< builtins::Func >( instr.func() );
        if( !func )
            return nullopt;

        const auto& ft = func->type();
        const auto& fvi = ft.verifInfos();
        if( !fvi )
            return nullopt;

        auto retExpr = BuildZ3ConstantFromType( ft.returnType(), format( "r{}", b.newUniqueId() ) );

        // 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.solver(), b.remapper() );

        // Inject the arguments in the context as variables of cfgId "0".
        // They will be picked up by getVars instructions when refered to
        // by the verification conditions.
        uint32_t index = 0;

        ForEachInVectorTerm( instr.args(), [&]( auto&& t )
        {
            auto arg = *ValueFromIRExpr( t );

            if( auto expr = BuildZ3ExprFromValue( b, arg ) )
                cb.setVar( 0, index++, move( *expr ) );

            return true;
        } );

        // Setup the return value placeholder
        if( retExpr )
            cb.setPlaceholder( "@"_sid, *retExpr );

        // Check preconditions.
        const auto& preConds = fvi->preConditions();
        ForEachInVectorTerm( preConds, [&]( auto&& t )
        {
            auto val = *ValueFromIRExpr( t );

            if( auto z3expr = BuildZ3ExprFromValue( cb, val ) )
            {
                DiagnosticsContext dc( instr.func().locationId(), "At this call." );
                b.checkAssertion( *z3expr, val.locationId() );
            }

            return true;
        } );

        // Add postconditions as assumptions.
        const auto& postConds = fvi->postConditions();
        ForEachInVectorTerm( postConds, [&]( auto&& t )
        {
            if( auto z3expr = BuildZ3ExprFromValue( cb, *ValueFromIRExpr( t ) ) )
                b.assume( *z3expr );
            return true;
        } );

        return retExpr;
    }
}