Goose  Artifact [d524da943d]

Artifact d524da943d0101745793927c510c644370965d181e89d08c40daec62b956f42b:

• File bs/verify/call.cpp — part of check-in [9814f18b04] at 2022-06-29 21:39:39 on branch cir-stack-language —
  • Verifier: consider verification failed if we encountered anything funny that prevented us from translating the entire function cfg to z3, rather than silently ignoring it
  • Verifier: fixed a case where the verifier would improperly bail out and do the above
  • Verifier: fixed a nasty use-after-free caused by forgetting an ampersand. fucking c++
  (user: zlodo size: 4018) [more...]

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

using namespace goose::diagnostics;

namespace goose::verify
{
    bool BuildZ3Op( Builder& b, const Call& instr )
    {
        auto fVal = b.pop< Value >();
        if( !fVal )
            return false;

        auto rt = builtins::GetFuncRType( *fVal );
        if( !rt )
            return false;

        auto func = FromValue< builtins::Func >( *fVal );
        if( !func )
        {
            if( rt == GetValueType< void >() )
                return true;

            auto result = BuildZ3ConstantFromType( b, *rt, format( "r{}", b.newUniqueId() ) );
            b.push( move( result ) );
            return true;
        }

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

        optional< Z3Val > retExpr;
        if( rt != GetValueType< void >() )
            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;
        auto fcir = func->cir();
        if( fcir && fcir->body() )
            cb.resetVarStorage( fcir->body()->temporariesCount() );
        else
            cb.resetVarStorage( 0 );

        // 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();

        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( 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, VarAddr( varId++, type, 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;
        } );

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

        // 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->postConds();
        postConds->forEach( [&]( auto&& val )
        {
            if( auto zv = TryBuildZ3ExprFromValue( cb, val ) )
                b.assume( zv->expr );
        } );

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