1# * Copyright 2016, NICTA
2# *
3# * This software may be distributed and modified according to the terms
4# of
5# * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6# * See "LICENSE_BSD2.txt" for details.
7# *
8# * @TAG(NICTA_BSD)
9
10import os, sys, time
11from subprocess import Popen, PIPE
12import graph_refine.trace_refute as trace_refute
13import conflict
14import cplex
15
16def silence():
17    '''
18    Silence all outputs to stdout and stderr
19    '''
20    #open 2 fds
21    saved_fds = None
22    null_fds = None
23    null_fds = [os.open(os.devnull, os.O_RDWR) for x in xrange(2)]
24    #save the current file descriptors to a tuple
25    saved_fds = os.dup(1), os.dup(2)
26    #put /dev/null fds on 1 and 2
27    os.dup2(null_fds[0], 1)
28    os.dup2(null_fds[1], 2)
29    return (saved_fds, null_fds)
30
31def unsilence(save_fds, null_fds):
32    '''
33    Un-silence outputs to stdout and stderr
34    '''
35    #restore stdin and stderr
36    os.dup2(save_fds[0], 1)
37    os.dup2(save_fds[1], 2)
38    os.close(null_fds[0])
39    os.close(null_fds[1])
40    return (save_fds, null_fds)
41
42def auto_infea(dir_name, entry_point_function, manual_conflicts_file, results_dir, initial_case_iteration, preemption_limit):
43    kernel_elf_file = dir_name+'/kernel.elf'
44    tcfg_map = dir_name + '/%s.imm.map' % entry_point_function
45    kernel_elf_file = dir_name+'/kernel.elf'
46    ilp_nofooter = cplex.stripFooter(dir_name + '/%s.imm.ilp' % entry_point_function)
47
48    auto_refutes_file = results_dir+'/refutes.txt'
49
50    p = Popen(['touch', auto_refutes_file])
51    p.communicate()
52    assert not p.returncode
53
54    results_file = results_dir+ '/results.txt'
55#we want to see results as we go, set bufsize to 0
56    results_f = open(results_file,'w',0)
57
58#setup trace_refute's environment
59    from graph_refine.target_objects import target_dir, target_args
60    target = '%s/target.py' % dir_name
61    target_dir.set_dir(dir_name)
62
63    case_i = initial_i
64    while True:
65        sol_file = results_dir+'/case_%d.sol' % case_i
66        ilp_file = results_dir+'/case_%d.ilp' % case_i
67        print 'case_i = %d' % case_i
68        print 'calling conflict.conflict'
69#silence()
70#get the wcet with existing conflicts
71        conflict.cleanGlobalStates()
72
73        #FIXME: un-hardcode the entry function
74        wcet = conflict.conflict(entry_point_function, tcfg_map, [manual_conflicts_file,auto_refutes_file],ilp_nofooter,ilp_file,dir_name, sol_file, emit_conflicts=True, do_cplex=True, silent_cplex=True, preempt_limit=preemption_limit)
75#unsilence()
76
77        print 'conflict.main returned'
78
79        results_f.write('case %d\n' % case_i)
80        results_f.write('   wcet: %s\n' % wcet)
81
82#reconstruct the worst case
83        refutables_fname = results_dir + '/refutables_%d' % case_i
84        f_refutables = open(refutables_fname,'w')
85        print 'reconstructing the worst case for case %d' % case_i
86        p = Popen(['python', 'reconstruct.py', '--refutable', dir_name, sol_file, tcfg_map, kernel_elf_file], stdout=f_refutables)
87        p.communicate()
88        ret = p.returncode
89        print 'ret: %d'% ret
90        assert ret == 0
91
92        f_refutables.close()
93        #now call trace_refute
94        t = time.asctime()
95        c1 = time.time()
96        print 'calling trace_refute, time is: %s' % t
97        results_f.write(' trace_refute called at: %s\n' % t)
98        silence_all = False
99        if silence_all:
100            #but before we do, supress output.
101            (saved_fds, null_fds) = silence()
102        new_refutes,_ = trace_refute.refute(refutables_fname, auto_refutes_file, [auto_refutes_file])
103        if silence_all:
104            #restore stdin and stderr
105            unsilence(saved_fds, null_fds)
106        c2 = time.time()
107        t = time.asctime()
108        print 'trace_refute returned, time is: %s' % t
109        results_f.write(' trace_refute returned at: %s\n' % t)
110
111        results_f.write('   this took %f seconds\n' % (c2-c1))
112
113        if not new_refutes:
114            print 'At case %d, trace_refute cannot find any more refutations' % case_i
115            results_f.write('terminated normally: trace_refute cannot find any more refutations\n')
116            break
117
118#cp the auto_refutes_file to keep a copy
119        p = Popen(['cp', auto_refutes_file, results_dir+'/refutes_%d.txt'% case_i])
120        p.communicate()
121        assert not p.returncode
122        case_i += 1
123
124    results_f.close()
125
126if __name__ == '__main__':
127    if len(sys.argv) != 5:
128        print 'Usage: python auto_infea.py <dir_name> <entry point function> <results directory> <initial i>'
129        print 'results direcotry should already exists and be empty'
130        print 'initial i determine which iterations to start at, use 0 for fresh runs'
131        print len(sys.argv)
132        sys.exit(0)
133    dir_name = sys.argv[1]
134    entry_point_function = sys.argv[2]
135    from convert_loop_bounds import phantomPreemptsAnnoFileName
136    preempt_conflicts_file = phantomPreemptsAnnoFileName(dir_name)
137    results_dir = sys.argv[3]
138    initial_i = int(sys.argv[4])
139    auto_infea(dir_name, entry_point_function,preempt_conflicts_file, results_dir, initial_i, preemption_limit = 5)
140
141