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