import sys
import os
import glob
from optparse import OptionParser, OptionGroup

if __name__=='__main__':
    klee_command = 'klee --simplify-sym-indices --write-cvcs --write-cov --write-smt2 --output-module --max-memory=1000 --disable-inlining --optimize --use-forked-solver --use-cex-cache --libc=uclibc --posix-runtime --allow-external-sym-calls --only-output-states-covering-new --max-sym-array-size=4096 --max-instruction-time=60. --max-time=300. --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --randomize-fork --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 '
    klee_executable = ' ./ngircd '
    klee_sym_args = '' #' --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 '
    decl_vars = []
    func_nodes = []

    inj_code = []
    func_names = []

    parser = OptionParser("usage: %prog -d {directory containing source files} -e {executable name}")
    parser.add_option('-d', '--dir', action='store', type='string', dest='dir', help='Source file directory path')
    parser.add_option('-e', '--exec', action='store', type='string', dest='executable', help='Name of executable generated by Makefile')

    (opts, args) = parser.parse_args()

    # pprint(('diags', map(get_diag_info, tu.diagnostics)))

    dir_name = opts.dir
    exec_name = opts.executable

    if not os.path.isdir(dir_name):
        print('Could not find the specified directory.\nExiting.')
        sys.exit(-1)

    if not dir_name.endswith('/'):
        dir_name = dir_name+'/'
    
    for f in glob.glob(dir_name+'src/*.c'):
        if not os.path.exists(dir_name+'src/ngircd/*.c.units.mod'):
            os.system('python generate_unit.py -f '+f+' -a')
    
    for f in glob.glob(dir_name+'src/ngircd/*.c.units.mod'):    
        fl_name_noext = f[:-12]
        # user_response = raw_input('Do you want to run klee for '+fl_name_noext)
        if True:
        #if user_response == 'Y':
            os.system('mv '+fl_name_noext+'.c '+fl_name_noext+'.c.bkp')
            os.system('cp '+f+' '+fl_name_noext+'.c')
            os.system('make -C '+dir_name+' clean')
            os.system('make -C '+dir_name)

            os.system('llvm-link-3.4 -o '+dir_name+'src/ngircd/'+exec_name+' '+dir_name+'src/ngircd/*.o')
            os.system(klee_command + ' --output-dir='+fl_name_noext+'/ '+dir_name+'src/ngircd/'+exec_name+klee_sym_args)
            os.system('mv '+fl_name_noext+'.c '+fl_name_noext+'.c.units.finished')
            os.system('mv '+fl_name_noext+'.c.bkp '+fl_name_noext+'.c')
