cmdPlugin.c File Reference

#include <unistd.h>
#include "base/abc/abc.h"
#include "base/main/mainInt.h"
#include "cmd.h"
#include "cmdInt.h"
#include "misc/util/utilSignal.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START char *	Abc_GetBinaryName (Abc_Frame_t *pAbc, int argc, char **argv)
	DECLARATIONS ///. More...
Vec_Str_t *	Abc_ManReadFile (char *pFileName)
Vec_Int_t *	Abc_ManReadBinary (char *pFileName, char *pToken)
int	Abc_ManReadInteger (char *pFileName, char *pToken)
int	Abc_ManReadStatus (char *pFileName, char *pToken)
Vec_Int_t *	Abc_ManExpandCex (Gia_Man_t *pGia, Vec_Int_t *vCex)
static unsigned	textToBin (char *text, unsigned long text_sz)
Gia_Man_t *	Abc_ManReadAig (char *pFileName, char *pToken)
int	Cmd_CommandAbcPlugIn (Abc_Frame_t *pAbc, int argc, char **argv)
int	Cmd_CommandAbcLoadPlugIn (Abc_Frame_t *pAbc, int argc, char **argv)

Function Documentation

ABC_NAMESPACE_IMPL_START char* Abc_GetBinaryName	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [cmdPlugin.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Command processing package.]

Synopsis [Integrating external binary.]

Author [Alan Mishchenko, Niklas Een]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 29, 2010.]

Revision [

Id:

cmdPlugin.c,v 1.00 2010/09/29 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file cmdPlugin.c.

{
    char * pTemp;
    int i;
    Vec_PtrForEachEntry( char *, pAbc->vPlugInComBinPairs, pTemp, i )
    {
        i++;
        if ( strcmp( pTemp, argv[0] ) == 0 )
            return (char *)Vec_PtrEntry( pAbc->vPlugInComBinPairs, i );
    }
    assert( 0 );
    return NULL;
}

Vec_Int_t* Abc_ManExpandCex	(	Gia_Man_t *	pGia,
		Vec_Int_t *	vCex
	)

Function*************************************************************

Synopsis [Work-around to insert 0s for PIs without fanout.]

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file cmdPlugin.c.

{
    Vec_Int_t * vCexNew;
    Gia_Obj_t * pObj;
    int i, k;

    // start with register outputs
    vCexNew = Vec_IntAlloc( Vec_IntSize(vCex) );
    Gia_ManForEachRo( pGia, pObj, i )
        Vec_IntPush( vCexNew, 0 );

    ABC_FREE( pGia->pRefs );
    Gia_ManCreateRefs( pGia );
    k = Gia_ManRegNum( pGia );
    while ( 1 )
    {
        Gia_ManForEachPi( pGia, pObj, i )
        {
            if ( Gia_ObjRefNum(pGia, pObj) == 0 )
                Vec_IntPush( vCexNew, 0 );
            else
            {
                if ( k == Vec_IntSize(vCex) )
                    break;
                Vec_IntPush( vCexNew, Vec_IntEntry(vCex, k++) );
            }
        }
        if ( k == Vec_IntSize(vCex) )
            break;
    }
    return vCexNew;
}

Gia_Man_t* Abc_ManReadAig	(	char *	pFileName,
		char *	pToken
	)

Function*************************************************************

Synopsis [Derives AIG from the text string in the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file cmdPlugin.c.

{
    Gia_Man_t * pGia = NULL;
    unsigned nBinaryPart;
    Vec_Str_t * vStr;
    char * pStr, * pEnd;
    vStr = Abc_ManReadFile( pFileName );
    if ( vStr == NULL )
        return NULL;
    pStr = Vec_StrArray( vStr );
    pStr = strstr( pStr, pToken );
    if ( pStr != NULL )
    {
        // skip token
        pStr += strlen(pToken);
        // skip spaces
        while ( *pStr == ' ' )
            pStr++;
        // set the end at newline
        for ( pEnd = pStr; *pEnd; pEnd++ )
            if ( *pEnd == '\r' || *pEnd == '\n' )
            {
                *pEnd = 0;
                break;
            }
        // convert into binary AIGER
        nBinaryPart = textToBin( pStr, strlen(pStr) );
        // dump it into file
        if ( 0 )
        {
            FILE * pFile = fopen( "test.aig", "wb" );
            fwrite( pStr, 1, nBinaryPart, pFile );
            fclose( pFile );
        }
        // derive AIG
        pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0 ); 
    }
    Vec_StrFree( vStr );
    return pGia;

}

Vec_Int_t* Abc_ManReadBinary	(	char *	pFileName,
		char *	pToken
	)

Function*************************************************************

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file cmdPlugin.c.

{
    Vec_Int_t * vMap = NULL;
    Vec_Str_t * vStr;
    char * pStr;
    int i, Length;
    vStr = Abc_ManReadFile( pFileName );
    if ( vStr == NULL )
        return NULL;
    pStr = Vec_StrArray( vStr );
    pStr = strstr( pStr, pToken );
    if ( pStr != NULL )
    {
        pStr  += strlen( pToken );
        vMap   = Vec_IntAlloc( 100 );
        Length = strlen( pStr );
        for ( i = 0; i < Length; i++ )
        {
            if ( pStr[i] == '0' || pStr[i] == '?' )
                Vec_IntPush( vMap, 0 );
            else if ( pStr[i] == '1' )
                Vec_IntPush( vMap, 1 );
            if ( ('a' <= pStr[i] && pStr[i] <= 'z') || 
                 ('A' <= pStr[i] && pStr[i] <= 'Z') )
                break;
        }
    }
    Vec_StrFree( vStr );
    return vMap;
}

Vec_Str_t* Abc_ManReadFile

(

char *

pFileName

)

Function*************************************************************

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file cmdPlugin.c.

{
    FILE * pFile;
    Vec_Str_t * vStr;
    int c;
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Cannot open file \"%s\".\n", pFileName );
        return NULL;
    }
    vStr = Vec_StrAlloc( 100 );
    while ( (c = fgetc(pFile)) != EOF )
        Vec_StrPush( vStr, (char)c );
    Vec_StrPush( vStr, '\0' );
    fclose( pFile );
    return vStr;
}

int Abc_ManReadInteger	(	char *	pFileName,
		char *	pToken
	)

Function*************************************************************

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file cmdPlugin.c.

{
    int Result = -1;
    Vec_Str_t * vStr;
    char * pStr;
    vStr = Abc_ManReadFile( pFileName );
    if ( vStr == NULL )
        return -1;
    pStr = Vec_StrArray( vStr );
    pStr = strstr( pStr, pToken );
    if ( pStr != NULL )
        Result = atoi( pStr + strlen(pToken) );
    Vec_StrFree( vStr );
    return Result;
}

int Abc_ManReadStatus	(	char *	pFileName,
		char *	pToken
	)

Function*************************************************************

Synopsis [Read flop map.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file cmdPlugin.c.

{
    int Result = -1;
    Vec_Str_t * vStr;
    char * pStr;
    vStr = Abc_ManReadFile( pFileName );
    if ( vStr == NULL )
        return -1;
    pStr = Vec_StrArray( vStr );
    pStr = strstr( pStr, pToken );
    if ( pStr != NULL )
    {
        if ( strncmp(pStr+8, "proved", 6) == 0 )
            Result = 1; 
        else if ( strncmp(pStr+8, "failed", 6) == 0 )
            Result = 0; 
    }
    Vec_StrFree( vStr );
    return Result;
}

int Cmd_CommandAbcLoadPlugIn	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 642 of file cmdPlugin.c.

{
    FILE * pFile;
    char pBuffer[1000];
    char * pCommandLine;
    char * pTempFile;
    char * pStrDirBin, * pStrSection;
    int fd, RetValue;

    if ( argc != 3 )
    {
        Abc_Print( -1, "Wrong number of arguments.\n" );
        goto usage;
    }
    // collect arguments
    pStrDirBin  = argv[argc-2];
    pStrSection = argv[argc-1];

    // check if the file exists
    if ( (pFile = fopen( pStrDirBin, "r" )) == NULL )
    {
//        Abc_Print( -1, "Cannot run the binary \"%s\".\n", pStrDirBin );
//        goto usage;
        return 0;
    }
    fclose( pFile );

    // create temp file
    fd = Util_SignalTmpFile( "__abctmp_", ".txt", &pTempFile );
    if ( fd == -1 )
    {
        Abc_Print( -1, "Cannot create a temporary file.\n" );
        goto usage;
    }
#ifdef WIN32
    _close( fd );
#else
    close( fd );
#endif

    // get command list
    pCommandLine = ABC_ALLOC( char, 100 + strlen(pStrDirBin) + strlen(pTempFile) );
//    sprintf( pCommandLine, "%s -abc -list-commands > %s", pStrDirBin, pTempFile );
    sprintf( pCommandLine, "%s -abc -list-commands > %s", pStrDirBin, pTempFile );
    RetValue = Util_SignalSystem( pCommandLine );
    if ( RetValue == -1 )
    {
        Abc_Print( -1, "Command \"%s\" did not succeed.\n", pCommandLine );
        ABC_FREE( pCommandLine );
        ABC_FREE( pTempFile );
        goto usage;
    }
    ABC_FREE( pCommandLine );

    // create commands
    pFile = fopen( pTempFile, "r" );
    if ( pFile == NULL )
    {
        Abc_Print( -1, "Cannot open file with the list of commands.\n" );
        ABC_FREE( pTempFile );
        goto usage;
    }
    while ( fgets( pBuffer, 1000, pFile ) != NULL )
    {
        if ( pBuffer[strlen(pBuffer)-1] == '\n' )
            pBuffer[strlen(pBuffer)-1] = 0;
        Cmd_CommandAdd( pAbc, pStrSection, pBuffer, Cmd_CommandAbcPlugIn, 1 );
//        plugin_commands.push(Pair(cmd_name, binary_name));
        Vec_PtrPush( pAbc->vPlugInComBinPairs, Extra_UtilStrsav(pBuffer) );
        Vec_PtrPush( pAbc->vPlugInComBinPairs, Extra_UtilStrsav(pStrDirBin) );
//        printf( "Creating command %s with binary %s\n", pBuffer, pStrDirBin );
    }
    fclose( pFile );
    Util_SignalTmpFileRemove( pTempFile, 0 );
    ABC_FREE( pTempFile );
    return 0;
usage:
    Abc_Print( -2, "usage: load_plugin <plugin_dir\\binary_name> <section_name>\n" );
    Abc_Print( -2, "\t        loads external binary as a plugin\n" );
    Abc_Print( -2, "\t-h    : print the command usage\n");
    return 1;
}

int Cmd_CommandAbcPlugIn	(	Abc_Frame_t *	pAbc,
		int	argc,
		char **	argv
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 412 of file cmdPlugin.c.

{
    char * pFileIn, * pFileOut;
    char * pFileNameBinary;
    Vec_Str_t * vCommand;
    Vec_Int_t * vCex;
    FILE * pFile;
    Gia_Man_t * pGia;
    int i, fd;
    abctime clk;
    int fLeaveFiles;
/*
    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
    if ( pNtk == NULL )
    {
        Abc_Print( -1, "Current network does not exist\n" );
        return 1;
    }
    if ( !Abc_NtkIsStrash( pNtk) )
    {
        Abc_Print( -1, "The current network is not an AIG. Cannot continue.\n" );
        return 1;
    }
*/

    if ( pAbc->pGia == NULL )
    {
        if (argc == 2 && strcmp(argv[1], "-h") == 0)
        {
            // Run command to produce help string:
            vCommand = Vec_StrAlloc( 100 );
            pFileNameBinary = Abc_GetBinaryName( pAbc, argc, argv );
            Vec_StrAppend( vCommand, pFileNameBinary );
            Vec_StrAppend( vCommand, " -abc " );
            Vec_StrAppend( vCommand, argv[0] );
            Vec_StrAppend( vCommand, " -h" );
            Vec_StrPush( vCommand, 0 );
            Util_SignalSystem( Vec_StrArray(vCommand) );
            Vec_StrFree( vCommand );
        }
        else
        {
            Abc_Print( -1, "Current AIG does not exist (try command &ps).\n" );
        }
        return 1;
    }

    // check if there is the binary
    pFileNameBinary = Abc_GetBinaryName( pAbc, argc, argv );
    if ( (pFile = fopen( pFileNameBinary, "r" )) == NULL )
    {
        Abc_Print( -1, "Cannot run the binary \"%s\".\n\n", pFileNameBinary );
        return 1;
    }
    fclose( pFile );

    // create temp file
    fd = Util_SignalTmpFile( "__abctmp_", ".aig", &pFileIn );
    if ( fd == -1 )
    {
        Abc_Print( -1, "Cannot create a temporary file.\n" );
        return 1;
    }
#ifdef WIN32
    _close( fd );
#else
    close( fd );
#endif

    // create temp file
    fd = Util_SignalTmpFile( "__abctmp_", ".out", &pFileOut );
    if ( fd == -1 )
    {
        ABC_FREE( pFileIn );
        Abc_Print( -1, "Cannot create a temporary file.\n" );
        return 1;
    }
#ifdef WIN32
    _close( fd );
#else
    close( fd );
#endif


    // write current network into a file
/*
    {
        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
        Aig_Man_t * pAig;
        pAig = Abc_NtkToDar( pNtk, 0, 1 );
        Ioa_WriteAiger( pAig, pFileIn, 0, 0 );
        Aig_ManStop( pAig );
    }
*/ 
    // check what to do with the files
    fLeaveFiles = 0;
    if ( strcmp( argv[argc-1], "!" ) == 0 )
    {
        Abc_Print( 0, "Input file \"%s\" and output file \"%s\" are not deleted.\n", pFileIn, pFileOut );
        fLeaveFiles = 1;
        argc--;
    }

    // create input file
    Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0 );

    // create command line
    vCommand = Vec_StrAlloc( 100 );
    Vec_StrAppend( vCommand, pFileNameBinary );
    // add input/output file
    Vec_StrAppend( vCommand, " -abc" );
//    Vec_StrAppend( vCommand, " -input=C:/_projects/abc/_TEST/hwmcc/139442p0.aig" );
    Vec_StrAppend( vCommand, " -input=" );
    Vec_StrAppend( vCommand, pFileIn );
    Vec_StrAppend( vCommand, " -output=" );
    Vec_StrAppend( vCommand, pFileOut );
    // add other arguments
    for ( i = 0; i < argc; i++ )
    {
        Vec_StrAppend( vCommand, " " );
        Vec_StrAppend( vCommand, argv[i] );
    }
    Vec_StrPush( vCommand, 0 );

    // run the command line
//printf( "Running command line: %s\n", Vec_StrArray(vCommand) ); 

    clk = Abc_Clock();
    if ( Util_SignalSystem( Vec_StrArray(vCommand) ) )
    {
        Abc_Print( -1, "The following command has returned non-zero exit status:\n" );
        Abc_Print( -1, "\"%s\"\n", Vec_StrArray(vCommand) );
        return 1;
    }
    clk = Abc_Clock() - clk;
    Vec_StrFree( vCommand );

    // check if the output file exists
    if ( (pFile = fopen( pFileOut, "r" )) == NULL )
    {
        Abc_Print( -1, "There is no output file \"%s\".\n", pFileOut );
        return 1;
    }
    fclose( pFile );

    // process the output
    if ( Extra_FileSize(pFileOut) > 0 )
    {
        // get status
        pAbc->Status  = Abc_ManReadStatus( pFileOut, "result:" );
        // get bug-free depth
        pAbc->nFrames = Abc_ManReadInteger( pFileOut, "bug-free-depth:" );
        // get abstraction
        pAbc->pGia->vFlopClasses = Abc_ManReadBinary( pFileOut, "abstraction:" );
        // get counter-example
        vCex = Abc_ManReadBinary( pFileOut, "counter-example:" );
        if ( vCex ) 
        {
            int nFrames, nRemain;

            nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) / Gia_ManPiNum(pAbc->pGia);
            nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) % Gia_ManPiNum(pAbc->pGia);
            if ( nRemain != 0 )
            {   
                Vec_Int_t * vTemp;
                Abc_Print( 1, "Adjusting counter-example by adding zeros for PIs without fanout.\n" );
                // expand the counter-example to include PIs without fanout
                vCex = Abc_ManExpandCex( pAbc->pGia, vTemp = vCex );
                Vec_IntFree( vTemp );
            }

            nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) / Gia_ManPiNum(pAbc->pGia);
            nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pAbc->pGia)) % Gia_ManPiNum(pAbc->pGia);
            if ( nRemain != 0 )
                Abc_Print( 1, "Counter example has a wrong length.\n" );
            else
            {
                Abc_Print( 1, "Problem is satisfiable. Found counter-example in frame %d.  ", nFrames-1 );
                Abc_PrintTime( 1, "Time", clk );
                ABC_FREE( pAbc->pCex );
                pAbc->pCex = Abc_CexCreate( Gia_ManRegNum(pAbc->pGia), Gia_ManPiNum(pAbc->pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );

//                Abc_CexPrint( pAbc->pCex );

//                if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
//                    Abc_Print( 1, "Generated counter-example is INVALID.\n" );

                // remporary work-around to detect the output number - October 18, 2010
                pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex, 0 );
                if ( pAbc->pCex->iPo == -1 )
                {
                    Abc_Print( 1, "Generated counter-example is INVALID.\n" );
                    ABC_FREE( pAbc->pCex );
                }
                else
                {
                    Abc_Print( 1, "Returned counter-example successfully verified in ABC.\n" );
                }
            }
            Vec_IntFreeP( &vCex );
        }
        // get AIG if present
        pGia = Abc_ManReadAig( pFileOut, "aig:" );
        if ( pGia != NULL )
        {
            Gia_ManStopP( &pAbc->pGia );
            pAbc->pGia = pGia;                
        }
    }    

    // clean up
    Util_SignalTmpFileRemove( pFileIn, fLeaveFiles );
    Util_SignalTmpFileRemove( pFileOut, fLeaveFiles );
    
    ABC_FREE( pFileIn );
    ABC_FREE( pFileOut );
    return 0;
}

static unsigned textToBin ( char *  text, unsigned long  text_sz  )

static

Function*************************************************************

Synopsis [Procedure to convert the AIG from text into binary form.]

Description []

SideEffects []

SeeAlso []

Definition at line 330 of file cmdPlugin.c.

{
    char*       dst = text;
    const char* src = text;
    unsigned sz, i;
    sscanf(src, "%u ", &sz);
    while(*src++ != ' ');
    for ( i = 0; i < sz; i += 3 )
    {
        dst[0] = (char)( (unsigned)src[0] - '0')       | (((unsigned)src[1] - '0') << 6);
        dst[1] = (char)(((unsigned)src[1] - '0') >> 2) | (((unsigned)src[2] - '0') << 4);
        dst[2] = (char)(((unsigned)src[2] - '0') >> 4) | (((unsigned)src[3] - '0') << 2);
        src += 4;
        dst += 3;
    }
    return sz;
}