Goose  Artifact [ace936b55b]

Artifact ace936b55bf3ec1703e2ed78b6342b5f842acfdee1a9b8042549cda4226bcef9:

• File bs/verify/call.cpp — part of check-in [c3f897359f] at 2020-06-20 14:32:02 on branch trunk —
  • Got rid of the gross system of performing unifications twice in all cases. It's only really needed when invoking template functions.
  • Since the above had the unexpected side effect of fixing the tuple Initialize() overloads not being called, fixed those (which were actually broken).
  (user: achavasse size: 3560)

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

using namespace goose::diagnostics;

namespace goose::verify
{
    optional< Z3Val > 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( b, 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.context(), *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 zv = BuildZ3ExprFromValue( b, arg ) )
                cb.setVar( index++, move( *zv ) );

            return true;
        } );

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

        ForEachInVectorTerm( ft.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 ) );

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

            return true;
        } );

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

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

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

            return true;
        } );

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

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

        return retExpr;
    }
}