#!/usr/bin/env python """ # OpenWRT download directory cleanup utility. # Delete all but the very last version of the program tarballs. # # Copyright (c) 2010 Michael Buesch """ import sys import os import re import getopt # Commandline options opt_dryrun = False def parseVer_1234(match, filepath): progname = match.group(1) progversion = (int(match.group(2)) << 64) |\ (int(match.group(3)) << 48) |\ (int(match.group(4)) << 32) |\ (int(match.group(5)) << 16) return (progname, progversion) def parseVer_123(match, filepath): progname = match.group(1) try: patchlevel = match.group(5) except (IndexError), e: patchlevel = None if patchlevel: patchlevel = ord(patchlevel[0]) else: patchlevel = 0 progversion = (int(match.group(2)) << 64) |\ (int(match.group(3)) << 48) |\ (int(match.group(4)) << 32) |\ patchlevel return (progname, progversion) def parseVer_12(match, filepath): progname = match.group(1) try: patchlevel = match.group(4) except (IndexError), e: patchlevel = None if patchlevel: patchlevel = ord(patchlevel[0]) else: patchlevel = 0 progversion = (int(match.group(2)) << 64) |\ (int(match.group(3)) << 48) |\ patchlevel return (progname, progversion) def parseVer_r(match, filepath): progname = match.group(1) progversion = (int(match.group(2)) << 64) return (progname, progversion) def parseVer_ymd(match, filepath): progname = match.group(1) progversion = (int(match.group(2)) << 64) |\ (int(match.group(3)) << 48) |\ (int(match.group(4)) << 32) return (progname, progversion) def parseVer_GIT(match, filepath): progname = match.group(1) st = os.stat(filepath) progversion = int(st.st_mtime) << 64 return (progname, progversion) extensions = ( ".tar.gz", ".tar.bz2", ".orig.tar.gz", ".orig.tar.bz2", ".zip", ".tgz", ".tbz", ) versionRegex = ( (re.compile(r"(.+)[-_]([0-9a-fA-F]{40,40})"), parseVer_GIT), # xxx-GIT_SHASUM (re.compile(r"(.+)[-_](\d+)\.(\d+)\.(\d+)\.(\d+)"), parseVer_1234), # xxx-1.2.3.4 (re.compile(r"(.+)[-_](\d\d\d\d)-?(\d\d)-?(\d\d)"), parseVer_ymd), # xxx-YYYY-MM-DD (re.compile(r"(.+)[-_](\d+)\.(\d+)\.(\d+)(\w?)"), parseVer_123), # xxx-1.2.3a (re.compile(r"(.+)[-_](\d+)_(\d+)_(\d+)"), parseVer_123), # xxx-1_2_3 (re.compile(r"(.+)[-_](\d+)\.(\d+)(\w?)"), parseVer_12), # xxx-1.2a (re.compile(r"(.+)[-_]r?(\d+)"), parseVer_r), # xxx-r1111 ) blacklist = [ ("linux", re.compile(r"linux-.*")), ("gcc", re.compile(r"gcc-.*")), ("wl_apsta", re.compile(r"wl_apsta.*")), (".fw", re.compile(r".*\.fw")), (".arm", re.compile(r".*\.arm")), (".bin", re.compile(r".*\.bin")), ("rt-firmware", re.compile(r"RT[\d\w]+_Firmware.*")), ] class EntryParseError(Exception): pass class Entry: def __init__(self, directory, filename): self.directory = directory self.filename = filename self.progname = "" self.fileext = "" for ext in extensions: if filename.endswith(ext): filename = filename[0:0-len(ext)] self.fileext = ext break else: print self.filename, "has an unknown file-extension" raise EntryParseError("ext") for (regex, parseVersion) in versionRegex: match = regex.match(filename) if match: (self.progname, self.version) = parseVersion( match, directory + "/" + filename + self.fileext) break else: print self.filename, "has an unknown version pattern" raise EntryParseError("ver") def deleteFile(self): path = (self.directory + "/" + self.filename).replace("//", "/") print "Deleting", path if not opt_dryrun: os.unlink(path) def __eq__(self, y): return self.filename == y.filename def __ge__(self, y): return self.version >= y.version def usage(): print "OpenWRT download directory cleanup utility" print "Usage: " + sys.argv[0] + " [OPTIONS] " print "" print " -d|--dry-run Do a dry-run. Don't delete any files" print " -B|--show-blacklist Show the blacklist and exit" print " -w|--whitelist ITEM Remove ITEM from blacklist" def main(argv): global opt_dryrun try: (opts, args) = getopt.getopt(argv[1:], "hdBw:", [ "help", "dry-run", "show-blacklist", "whitelist=", ]) if len(args) != 1: usage() return 1 except getopt.GetoptError: usage() return 1 directory = args[0] for (o, v) in opts: if o in ("-h", "--help"): usage() return 0 if o in ("-d", "--dry-run"): opt_dryrun = True if o in ("-w", "--whitelist"): for i in range(0, len(blacklist)): (name, regex) = blacklist[i] if name == v: del blacklist[i] break else: print "Whitelist error: Item", v,\ "is not in blacklist" return 1 if o in ("-B", "--show-blacklist"): for (name, regex) in blacklist: print name return 0 # Create a directory listing and parse the file names. entries = [] for filename in os.listdir(directory): if filename == "." or filename == "..": continue for (name, regex) in blacklist: if regex.match(filename): if opt_dryrun: print filename, "is blacklisted" break else: try: entries.append(Entry(directory, filename)) except (EntryParseError), e: pass # Create a map of programs progmap = {} for entry in entries: if entry.progname in progmap.keys(): progmap[entry.progname].append(entry) else: progmap[entry.progname] = [entry,] # Traverse the program map and delete everything but the last version for prog in progmap: lastVersion = None versions = progmap[prog] for version in versions: if lastVersion is None or version >= lastVersion: lastVersion = version if lastVersion: for version in versions: if version != lastVersion: version.deleteFile() if opt_dryrun: print "Keeping", lastVersion.filename return 0 if __name__ == "__main__": sys.exit(main(sys.argv)) a> 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
/**CFile****************************************************************

  FileName    [mainMC.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [The main package.]

  Synopsis    [The main file for the model checker.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "mainInt.h"
#include "aig.h"
#include "saig.h"
#include "fra.h"
#include "ioa.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [The main() procedure.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int main( int argc, char * argv[] )
{
    int fEnableBmcOnly = 0;  // enable to make it BMC-only

    int fEnableCounter = 1;  // should be 1 in the final version
    int fEnableComment = 0;  // should be 0 in the final version

    Fra_Sec_t SecPar, * pSecPar = &SecPar;
    FILE * pFile;
    Aig_Man_t * pAig;
    int RetValue = -1;
    int Depth    = -1;
    // BMC parameters
    int nFrames  = 50;
    int nSizeMax = 500000;
    int nBTLimit = 10000;
    int fRewrite = 0;
    int fNewAlgo = 1;
    int fVerbose = 0;
    int clkTotal = clock();

    if ( argc != 2 )
    {
        printf( "  Expecting one command-line argument (an input file in AIGER format).\n" );
        printf( "  usage: %s <file.aig>\n", argv[0] );
        return 0;
    }
    pFile = fopen( argv[1], "r" );
    if ( pFile == NULL )
    {
        printf( "  Cannot open input AIGER file \"%s\".\n", argv[1] );
        printf( "  usage: %s <file.aig>\n", argv[0] );
        return 0;
    }
    fclose( pFile );
    pAig = Ioa_ReadAiger( argv[1], 1 );
    if ( pAig == NULL )
    {
        printf( "  Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
        printf( "  usage: %s <file.aig>\n", argv[0] );
        return 0;
    }

    Aig_ManSetRegNum( pAig, pAig->nRegs );
    if ( !fEnableBmcOnly )
    {
        // perform BMC
        if ( pAig->nRegs != 0 )
            RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0 );

        // perform full-blown SEC
        if ( RetValue != 0 )
        {
            extern void Dar_LibStart();
            extern void Dar_LibStop();
            extern void Cnf_ClearMemory();

            Fra_SecSetDefaultParams( pSecPar );
            pSecPar->TimeLimit       = 600;
            pSecPar->nFramesMax      =   4;  // the max number of frames used for induction
            pSecPar->fPhaseAbstract  =   0;  // disable phase-abstraction
            pSecPar->fSilent         =   1;  // disable phase-abstraction

            Dar_LibStart();
            RetValue = Fra_FraigSec( pAig, pSecPar, NULL );
            Dar_LibStop();
            Cnf_ClearMemory();
        }
    }

    // perform BMC again
    if ( RetValue == -1 && pAig->nRegs != 0 )
    {
        int nFrames  = 200;
        int nSizeMax = 500000;
        int nBTLimit = 10000000;
        int fRewrite = 0;
        RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0 );
        if ( RetValue != 0 )
            RetValue = -1;
    }

    // decide how to report the output
    pFile = stdout;

    // report the result
    if ( RetValue == 0 ) 
    {
//        fprintf(stdout, "s SATIFIABLE\n");
        fprintf( pFile, "1" );
        if ( fEnableCounter  )
        {
        printf( "\n" );
        if ( pAig->pSeqModel )
        Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
        }

        if ( fEnableComment )
        {
        printf( "  # File %10s.  ", argv[1] );
        PRT( "Time", clock() - clkTotal );
        }

        if ( pFile != stdout )
            fclose(pFile);
        Aig_ManStop( pAig );
        exit(10);
    } 
    else if ( RetValue == 1 ) 
    {
//    fprintf(stdout, "s UNSATISFIABLE\n");
        fprintf( pFile, "0" );

        if ( fEnableComment )
        {
        printf( "  # File %10s.  ", argv[1] );
        PRT( "Time", clock() - clkTotal );
        }
        printf( "\n" );

        if ( pFile != stdout )
            fclose(pFile);
        Aig_ManStop( pAig );
        exit(20);
    } 
    else // if ( RetValue == -1 ) 
    {
//    fprintf(stdout, "s UNKNOWN\n");
        fprintf( pFile, "2" );

        if ( fEnableComment )
        {
        printf( "  # File %10s.  ", argv[1] );
        PRT( "Time", clock() - clkTotal );
        }
        printf( "\n" );

        if ( pFile != stdout )
            fclose(pFile);
        Aig_ManStop( pAig );
        exit(0);
    }
    return 0;
}




////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END