diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2010-11-01 01:35:04 -0700 |
commit | 6130e39b18b5f53902e4eab14f6d5cdde5219563 (patch) | |
tree | 0db0628479a1b750e9af1f66cb8379ebd0913d31 /src/base/cmd/cmdPlugin.c | |
parent | f0e77f6797c0504b0da25a56152b707d3357f386 (diff) | |
download | abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.gz abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.tar.bz2 abc-6130e39b18b5f53902e4eab14f6d5cdde5219563.zip |
initial commit of public abc
Diffstat (limited to 'src/base/cmd/cmdPlugin.c')
-rw-r--r-- | src/base/cmd/cmdPlugin.c | 629 |
1 files changed, 629 insertions, 0 deletions
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c new file mode 100644 index 00000000..be7a9245 --- /dev/null +++ b/src/base/cmd/cmdPlugin.c @@ -0,0 +1,629 @@ +/**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 $] + +***********************************************************************/ + +#ifdef WIN32 +#include <io.h> +#include <process.h> +#else +#include <unistd.h> +#endif + +#include "abc.h" +#include "mainInt.h" +#include "cmd.h" +#include "cmdInt.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + +-------- Original Message -------- +Subject: ABC/ZZ integration +Date: Wed, 29 Sep 2010 00:34:32 -0700 +From: Niklas Een <niklas@een.se> +To: Alan Mishchenko <alanmi@EECS.Berkeley.EDU> + +Hi Alan, + +Since the interface is file-based, it is important that we generate +good, unique filenames (we may run multiple instances of ABC in the +same directory), so I have attached some portable code for doing that +(tmpFile.c). You can integrate it appropriately. + +This is how my interface is meant to work: + +(1) As part of your call to Bip, give it first argument "-abc". + This will alter Bip's behavior slightly. + +(2) To list the commands, call 'bip -list-commands'. + My commands begin with a comma (so that's my prefix). + +(3) All commands expect an input file and an output file. + The input file should be in AIGER format. + The output will be a text file. + Example: + bip -input=tmp.aig -output=tmp.out ,pdr -check -prop=5 + + So you just auto-generate the two temporary files (output file is + closed and left empty) and stitch the ABC command line at the end. + All you need to check for is if the ABC line begins with a comma. + +(4) The result written to the output file will contain a number + of object. Each object is on a separate line of the form: + + <object name>: <object data> + +That is: name, colon, space, data, newline. If you see a name you don't +recognize, just skip that line (so you will ignore future extensions by me). +I currently define the following objects: + + result: + counter-example: + proof-invariant: + bug-free-depth: + abstraction: + +"result:" is one of "proved", "failed", "undetermined" (=reached resource limit), "error" +(only used by the abstraction command, and only if resource limit was so tight that the +abstraction was still empty -- no abstraction is returned in this special case). + +"counter-example:" -- same format as before + +"proof-invariant:" contains an text-encoded single-output AIG. If you want +you can parse it and validate the invariant. + +"bug-free-depth:" the depth up to which the procedure has checked for counter-example. +Starts at -1 (not even the initial states have been verified). + +"abstraction:" -- same format as before + +(5) I propose that you add a command "load_plugin <path/binary>". That way Bob can put +Bip where ever he likes and just modify his abc_rc file. + +The intention is that ABC can read this file and act on it without knowing what +particular command was used. If there is an abstraction, you will always apply it. +If there is a "bug-free-depth" you will store that data somewhere so that Bob can query +it through the Python interface, and so on. If we need different actions for different +command, then we add a new object for the new action. + +// N. + +*/ + +extern int tmpFile(const char* prefix, const char* suffix, char** out_name); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_GetBinaryName( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + char * pTemp; + int i; + Vec_PtrForEachEntry( char *, pAbc->vPlugInComBinPairs, pTemp, i ) + { + i++; + if ( strcmp( pTemp, argv[0] ) == 0 ) + return Vec_PtrEntry( pAbc->vPlugInComBinPairs, i ); + } + assert( 0 ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Read flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Abc_ManReadFile( char * pFileName ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Read flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_ManReadBinary( char * pFileName, char * pToken ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Read flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ManReadInteger( char * pFileName, char * pToken ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Read flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ManReadStatus( char * pFileName, char * pToken ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Work-around to insert 0s for PIs without fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_ManExpandCex( Gia_Man_t * pGia, Vec_Int_t * vCex ) +{ + 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_ObjRefs(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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + char * pFileIn, * pFileOut; + char * pFileNameBinary; + Vec_Str_t * vCommand; + Vec_Int_t * vCex; + FILE * pFile; + int i, fd, 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 ) + { + 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 = tmpFile( "__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 = tmpFile( "__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_WriteAiger( 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 = clock(); + if ( system( 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 = 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 ) + { + // read program arguments + pAbc->Status = Abc_ManReadStatus( pFileOut, "result:" ); + pAbc->nFrames = Abc_ManReadInteger( pFileOut, "bug-free-depth:" ); + if ( pAbc->nFrames == -1 ) + printf( "Gia_ManCexAbstractionStartNew(): Cannot read the number of frames covered by BMC.\n" ); + pAbc->pGia->vFlopClasses = Abc_ManReadBinary( pFileOut, "abstraction:" ); + 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 + { + extern int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p ); + + 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 = Gia_ManDeriveCexFromArray( pAbc->pGia, vCex, 0, nFrames-1 ); + +// Gia_ManPrintCex( pAbc->pCex ); + +// if ( !Gia_ManVerifyCounterExample( 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_ManVerifyCounterExampleAllOuts( pAbc->pGia, pAbc->pCex ); + 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 ); + } + } + + + + // clean up + if ( !fLeaveFiles ) + { + remove( pFileIn ); + remove( pFileOut ); + } + ABC_FREE( pFileIn ); + ABC_FREE( pFileOut ); + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + 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 = tmpFile( "__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 = system( 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, strdup(pBuffer) ); + Vec_PtrPush( pAbc->vPlugInComBinPairs, strdup(pStrDirBin) ); + printf( "Creating command %s with binary %s\n", pBuffer, pStrDirBin ); + } + fclose( pFile ); + remove( pTempFile ); + 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; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |