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

def get_target_info(dir_name):
    target_file = open(dir_name + 'target.info')

    content = target_file.readlines()

    target_info = []
    i = 0
    while i<len(content):
        target_file = content[i].strip()
        i += 1
        if i>=len(content):
            break
        target_line = content[i].strip()
        i += 1
        func_name = content[i].strip()
        i += 1

        unit_filename = target_file[:-2] + '_units/' + os.path.split(target_file)[1][:-2] + '_' + func_name + '.c.units.assert'
        print(unit_filename) # TODO: remove

        target_info.append((target_file.strip(), int(target_line.strip()), unit_filename))
        if i>=len(content):
            break
        dum_empty_line = content[i]
        i += 1

    return target_info

if __name__=='__main__':
    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()
    
    dir_name = opts.dir

    if not dir_name.endswith('/'):
        dir_name = dir_name + '/'

    klee_command = 'klee --simplify-sym-indices --write-cov --write-smt2s --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=%d. --max-time=%d. --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=targeted-search --use-batching-search --batch-instructions=10000 '%(10, 120)
    klee_sym_args = ' --sym-args 0 2 100 --sym-files 1 100'
    
    targets_info_file = open(dir_name + 'target.info')

    targets_info = targets_info_file.readlines()
    
    exec_name = opts.executable

    i = 0
    while i<len(targets_info):
        global_target_file = open('/mnt/ext-hdd/global_target.txt', 'w+')
        target_file = targets_info[i].strip()
        i += 1
        target_line = targets_info[i].strip()
        i += 1
        target_func = targets_info[i].strip()
        i += 2

        # Modify global target file
        global_target_file.write(target_file+'\n')
        global_target_file.write(target_line+'\n')
        global_target_file.close()

        # Copy and replace main file
        main_name = os.path.split(target_file)[1][:-2]
        os.system('mv %s%s.c %s%s.c.bkp'%(dir_name, main_name, dir_name, main_name))
        os.system('cp %s%s_units/%s_%s.c.units %s%s.c'%(dir_name, main_name, main_name, target_func, dir_name, main_name))
        
        # Compile
        os.system('make -C '+dir_name+' clean')
        make_ret = os.system('make -C '+dir_name)

        if not make_ret==0:
            print('Make error with %s_%s.c.units \nContinuing with the next unit file...\n'%(main_name, target_func))
            os.system('mv %s%s.c.bkp %s%s.c'%(dir_name, main_name, dir_name, main_name))
            time.sleep(3)
            continue

        # Run KLEE with --targeted-search
        os.system(klee_command + '--output-dir=' + dir_name + main_name + '_units/' + main_name + '_' + target_func + '_targeted/ ' + dir_name+exec_name + ' ' + klee_sym_args)
        
        # Replace main file again
        os.system('mv %s%s.c.bkp %s%s.c'%(dir_name, main_name, dir_name, main_name))

