Goose  Artifact [052bf428c2]

Artifact 052bf428c20f6839b91ff49dd429884ad7a4dd35172a58249129ac8572e9bade:

• File bs/parse/bracketblock.cpp — part of check-in [68260b65f2] at 2022-03-14 19:23:09 on branch trunk —
  • bracket blocks inlined in the code are no longer proposition lists but a new type of block to contain "ghost code" (ie a verification specific cfg)
  • added a GhostBranch instruction to insert the above in the middle of regular code
  • removed a bunch of hacks to ignore load/stores involving ghost funcs during execution and codegen since they are now separated from normal code using the above
  • miscellaneous other refactorings and improvements
  • as a result ghost code is now more flexible and can use idiomatic tuple assignments to exchange the values of two ghost function closures
  (user: zlodo size: 4875)

#include "parse.h"
#include "builtins/builtins.h"
#include "precedence.h"

using namespace goose;
using namespace goose::parse;
using namespace goose::builtins;

namespace
{
    auto TokenizeBracketBlock( Parser& p )
    {
        // Create a nested verbosity context to restrict the scope of
        // error silencing caused by syntax errors to the block.
        VerbosityContext vc( Verbosity::Normal );

        auto props = make_shared< Propositions >();
        props->setIdentity( p.context().identity() );

        props->unparsed().emplace_back();
        auto& toks = props->unparsed().back();

        auto g = p.resolver()->consumeUnit();

        auto beg = g.begin();

        auto startLoc = beg->second;
        advance( beg, 1 );

        move( beg, g.end(), back_inserter( toks ) );
        auto loc = Location::CreateSpanningLocation( startLoc, toks.back().second );
        toks.resize( toks.size() - 1 );

        return make_tuple( props, loc );
    }
}

Value Parser::parseBracketBlock()
{
    if( m_lastValue )
    {
        // Maybe a bit hackish: if there's currently a left value,
        // this bracket block is part of an expression (ie "requires" and such)
        // and should be parsed as a proposition list.
        auto [props, loc] = TokenizeBracketBlock( *this );
        return ToValue( TypeWrapper< ptr< Propositions > >( props ) )
            .setLocationId( loc );
    }

    auto cfg = GetCFG( context() );
    if( !cfg )
    {
        DiagnosticsManager::GetInstance().emitSyntaxErrorMessage(
            resolver()->currentLocation(), "ghost code blocks aren't allowed here.", 0 );
        PoisonBuilder( context() );
        return PoisonValue();
    }

    CurrentContextGuard ccg( *this );

    auto currentBB = cfg->currentBB();

    // Create a nested verbosity context to restrict the scope of
    // error silencing caused by syntax errors to the block.
    VerbosityContext vc( Verbosity::Normal );

    m_resolver->consume();

    auto ghostCode = make_shared< GhostCode >( cfg );

    Context localContext( context().env(), context().identity() );
    localContext.setBuilder( ToValue( TypeWrapper< ptr< GhostCode > >( ghostCode ) ) );

    auto p = makeNestedParser( Delimiter::OpenBracket );
    p.context() = localContext;

    cfg->setCurrentBB( ghostCode->entryBB() );
    p.parseSequence();
    cfg->setCurrentBB( currentBB );

    auto next = m_resolver->consumeUnresolved();
    if( !next )
    {
        DiagnosticsManager::GetInstance().emitSyntaxErrorMessage(
            resolver()->currentLocation(), "']' expected.", 0 );
        PoisonBuilder( context() );
        return PoisonValue();
    }

    auto decomp = Decompose( next->first, Val< Delimiter >() );
    if( !decomp || *decomp != Delimiter::CloseBracket )
    {
        DiagnosticsManager::GetInstance().emitSyntaxErrorMessage(
            next->second, "']' expected.", 0 );
        PoisonBuilder( context() );
        return PoisonValue();
    }

    return localContext.builder();
}

optional< uint32_t > Parser::getPostfixBracketBlockPrecedence()
{
    auto lastVal = peekLastValue();
    if( !lastVal )
        return nullopt;

    if( !IsType( context(), *lastVal ) )
        return nullopt;

    if( !GetTypePredicates( *lastVal ) )
        return nullopt;

    return precedence::ContractOp;
}

bool Parser::parsePostfixBracketBlock( uint32_t prec )
{
    auto type = *popValue();
    auto preds = *GetTypePredicates( type );
    if( preds )
        preds = make_shared< Propositions >( *preds );
    else
    {
        preds = make_shared< Propositions >();
        auto& c = context();

        // Create a new identity for the predicates, which imports everything from the parent identity
        // and also makes @val visible as a placeholder for the type's value.
        preds->setIdentity( VEC( Env::NewUniqueId() ) );
        c.env()->addVisibilityRule( c.identity(), preds->identity() );

        auto name = "@val"_sid;
        auto typeTerm = ValueToEIR( type );
        auto phVal = ValueToEIR( BuildComputedValue( typeTerm, cir::Placeholder( typeTerm, name ) ) );

        auto valuePlaceholderIdentity = AppendToVectorTerm( preds->identity(), TERM( name ) );
        c.env()->storeValue( valuePlaceholderIdentity, ANYTERM( _ ), phVal );

        // The placeholder is also available as the default lhs value, so "@val" can be omitted in many cases
        auto defLhsIdentity = AppendToVectorTerm( preds->identity(), TSID( 0_def_lhs ) );
        c.env()->storeValue( defLhsIdentity, ANYTERM( _ ), move( phVal ) );
    }

    auto [props, loc] = TokenizeBracketBlock( *this );
    preds->append( move( *props ) );

    loc = Location::CreateSpanningLocation( type.locationId(), loc );

    pushValue( Value( type.type(), InjectPredicatesIntoStdType( type.val(), preds ) )
        .setLocationId( loc ) );
    return true;
}