Goose  Artifact [17c5fefbc2]

Artifact 17c5fefbc2873aba7e02dab6ec9b41780df8cfd8bf369f81aa14be25941cc4de:

• File bs/verify/call.cpp — part of check-in [238df77134] at 2019-11-19 00:04:49 on branch trunk — cfg: now that we got rid of this crazy system where CFGs could "call" other CFGs that weren't really functions, removed that clumsy cfg index that was needed to identify temporaries everywhere. (user: achavasse size: 2265)

#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.
        // 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( 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;
    }
}