Goose  Artifact [593cb45a4a]

Artifact 593cb45a4a534d162dde10e6b404f4b9bf86aa84e072e27cfbed16ba3c81ebb6:

• File bs/verify/verifyviz.cpp — part of check-in [0db147f117] at 2024-09-15 20:24:31 on branch cir-ssa-refactor — Add clang format settings, reformat everything (user: achavasse size: 4903)

#include "verify.h"
#include "codegen/codegen.h"

// If enabled, only dump dot files for functions where an assertion
// failure was detected
#define VERIFY_VIZ_FAIL_ONLY

#ifdef VERIFY_VIZ

using namespace goose;
using namespace goose::verify;

namespace
{
    ostream& indent( ostream& out, int indentation )
    {
        while( indentation-- )
            out << '\t';

        return out;
    }
} // namespace

VerifyViz::~VerifyViz()
{
    #ifdef VERIFY_VIZ_FAIL_ONLY
    if( !m_assertionFailed )
        return;
    #endif

    if( m_filename.empty() )
        m_filename = "anon_func.dot";

    ofstream out( m_filename );

    out << "digraph \"goose\"\n"
           "{\n"
           "\tcolor=\"#"
        << colors::base05
        << "\";\n"
           "\tfontcolor=\"#"
        << colors::base05
        << "\";\n"
           "\tbgcolor=\"#"
        << colors::base00
        << "\";\n"
           "\trankdir=TB;\n"
           "\tnode [\n"
           "\t\tcolor=\"#"
        << colors::base05
        << "\";\n"
           "\t\tfontcolor=\"#"
        << colors::base05
        << "\";\n"
           "\t];\n"
           "\tedge [\n"
           "\t\tcolor=\"#"
        << colors::base03
        << "\";\n"
           "\t];\n";

    if( m_assertionFailed )
        indent( out, 1 ) << *m_assertionFailed << "[color=\"#" << colors::base08 << "\"];\n";

    for( auto&& [id, oid] : m_root->m_blocks )
    {
        out << '\n';
        if( id != oid )
            indent( out, 1 ) << id << "[ label=\"" << id << ':' << oid << "\"];";
        else
            indent( out, 1 ) << id << ';';
    }

    for( auto&& x : m_root->m_children )
    {
        out << '\n';
        GenerateSubGraph( out, x, 1 );
    }

    for( auto&& [from, to] : m_edges )
        indent( out, 1 ) << from << "->" << to << ";\n";

    out << "}\n";
}

void VerifyViz::GenerateSubGraph( ostream& out, ptr< SubGraph > sg, int indentation ) const
{
    indent( out, indentation ) << "subgraph cluster_" << sg.get() << endl;
    indent( out, indentation ) << "{\n";
    indent( out, indentation + 1 ) << "color = \"#" << colors::base09 << "\";\n";

    for( auto&& [id, oid] : sg->m_blocks )
    {
        out << '\n';
        if( id != oid )
            indent( out, indentation + 1 ) << id << "[ label=\"" << id << ':' << oid << "\"];";
        else
            indent( out, indentation + 1 ) << id << ';';
    }

    for( auto&& x : sg->m_children )
    {
        out << '\n';
        GenerateSubGraph( out, x, indentation + 1 );
    }

    out << '\n';
    indent( out, indentation ) << "}" << endl;
}

void VerifyViz::setFunctionIdentity( const Term& id )
{
    m_filename = format( "{}.dot", *codegen::Mangle( id ) );
}

void VerifyViz::beginLoopVerification()
{
    if( m_assertionFailed )
        return;

    pushSubGraph();
}

void VerifyViz::beginLoopInduction()
{
    if( m_assertionFailed )
        return;

    popSubGraph();
    pushSubGraph();
}

void VerifyViz::endLoopVerification()
{
    if( m_assertionFailed )
        return;

    popSubGraph();
}

void VerifyViz::nextLoopIteration()
{
    if( m_assertionFailed )
        return;

    popSubGraph();
    pushSubGraph();
}

void VerifyViz::addBlock( uint32_t id, uint32_t originalId )
{
    if( m_assertionFailed )
        return;

    m_currentSubGraph->m_blocks.emplace_back( id, originalId );
    m_lastBlockId = id;
}

void VerifyViz::addEdge( uint32_t from, uint32_t to )
{
    if( m_assertionFailed )
        return;

    if( to == Remapper::InvalidEdgeId )
        return;

    m_edges.emplace_back( from, to );
}

void VerifyViz::pushSubGraph()
{
    if( m_assertionFailed )
        return;

    auto pNew = make_shared< SubGraph >();

    m_currentSubGraph->m_children.emplace_back( pNew );
    pNew->m_parent = m_currentSubGraph;

    m_currentSubGraph = pNew;
}

void VerifyViz::popSubGraph()
{
    if( m_assertionFailed )
        return;

    m_currentSubGraph = m_currentSubGraph->m_parent.lock();
    assert( m_currentSubGraph );
}

VerifyViz::Guard::Guard( VerifyViz& vv ) :
    m_vv( vv )
{
    m_savedRoot = deepCopyGraph( m_vv.m_root );
    m_savedEdges = vv.m_edges;
    m_savedLastBlockId = vv.m_lastBlockId;
}

VerifyViz::Guard::~Guard()
{
    if( m_commit )
        return;

    m_vv.m_root = move( m_savedRoot );
    m_vv.m_currentSubGraph = move( m_savedCurrentSubGraph );
    m_vv.m_edges = move( m_savedEdges );
    m_vv.m_lastBlockId = move( m_savedLastBlockId );
}

ptr< VerifyViz::SubGraph > VerifyViz::Guard::deepCopyGraph( const ptr< SubGraph >& pNode )
{
    auto pNew = make_shared< SubGraph >();
    pNew->m_blocks = pNode->m_blocks;

    for( const auto& x : pNode->m_children )
    {
        auto c = deepCopyGraph( x );
        c->m_parent = pNew;
        pNew->m_children.emplace_back( move( c ) );
    }

    if( m_vv.m_currentSubGraph == pNode )
        m_savedCurrentSubGraph = pNew;

    return pNew;
}

#endif