1# * Copyright 2015, NICTA 2# * 3# * This software may be distributed and modified according to the terms of 4# * the BSD 2-Clause license. Note that NO WARRANTY is provided. 5# * See "LICENSE_BSD2.txt" for details. 6# * 7# * @TAG(NICTA_BSD) 8 9# trace_refute: refutations of traces, useful for WCET 10 11import syntax 12import solver 13import problem 14import rep_graph 15import search 16import logic 17import check 18import stack_logic 19 20from target_objects import functions, trace, pairings, symbols, printout 21import target_objects 22 23from logic import azip 24import sys 25 26def parse_num_list (s): 27 s = s.strip() 28 assert s[0] == '[', s 29 assert s[-1] == ']', s 30 inner = s[1:-1].strip () 31 if not inner: 32 return [] 33 return map (int, inner.split(',')) 34 35def parse_num_arrow_list (s): 36 s = s.strip() 37 assert s[0] == '[', s 38 assert s[-1] == ']', s 39 inner = s[1:-1].strip () 40 if not inner: 41 return [] 42 bits = inner.split(',') 43 res = [] 44 for bit in bits: 45 if '<-' in bit: 46 [l, r] = bit.split('<-') 47 res.append ((int (l), int(r))) 48 else: 49 res.append ((int (bit), 0)) 50 return res 51 52def parse_ctxt_arcs (f): 53 ctxt = None 54 fc_len = len ('Funcall context') 55 arcs = {} 56 for line in f: 57 if line.startswith('Funcall context'): 58 line = line.strip() 59 assert line[-1] == '{' 60 context = line[fc_len:-1].strip() 61 ctxt = tuple (parse_num_list (context)) 62 arcs.setdefault (ctxt, []) 63 elif line.startswith('}'): 64 ctxt = None 65 elif line.startswith('Arc:'): 66 assert ctxt, line 67 arc = parse_num_list (line[4:]) 68 arcs[ctxt].append (arc) 69 assert not ctxt, ctxt 70 return arcs 71 72body_addrs = {} 73fun_addrs_counts = {} 74 75def is_addr (n): 76 return n % 4 == 0 77 78def setup_body_addrs (): 79 for f in stack_logic.get_functions_with_tag ('ASM'): 80 count = 0 81 for n in functions[f].nodes: 82 if is_addr (n): 83 body_addrs[n] = f 84 count += 1 85 fun_addrs_counts[f] = count 86 # just in case there aren't any 87 body_addrs['Loaded'] = True 88 89def get_body_addrs_fun (n): 90 """get the function a given body address is within.""" 91 if not body_addrs: 92 setup_body_addrs () 93 return body_addrs.get (n) 94 95def addrs_covered (fs): 96 """get the fraction of instructions covered by some functions""" 97 if not body_addrs: 98 setup_body_addrs () 99 covered = sum ([fun_addrs_counts.get (f, 0) for f in fs]) 100 total = len (body_addrs) - 1 101 return (covered * 1.0 / total) 102 103def funs_sort_by_num_addrs (fs): 104 """sort a list of function names into increasing order 105 of the number of instruction addresses, skipping functions 106 with no instructions in their body.""" 107 if not body_addrs: 108 setup_body_addrs () 109 fun_addrs = [(fun_addrs_counts[f], f) for f in fs 110 if f in fun_addrs_counts] 111 fun_addrs.sort () 112 return [f for (n, f) in fun_addrs] 113 114problem_inline_scripts = {} 115 116def get_problem_inline_scripts (pair): 117 if pair.name in problem_inline_scripts: 118 return problem_inline_scripts[pair.name] 119 p = check.build_problem (pair, avoid_abort = True) 120 scripts = p.inline_scripts 121 problem_inline_scripts[pair.name] = scripts 122 return scripts 123 124last_compound_problem_req = [0] 125 126def build_compound_problem (fnames): 127 """mirrors build_problem from check for multiple functions""" 128 printout ('Building compound problem for %s' % fnames) 129 last_compound_problem_req[0] = list (fnames) 130 p = problem.Problem (None, name = ', '.join(fnames)) 131 fun_tag_pairs = [] 132 133 all_tags = {} 134 for (i, fn) in enumerate (fnames): 135 i = len (fnames) - i 136 [pair] = pairings[fn] 137 next_tags = {} 138 scripts = get_problem_inline_scripts (pair) 139 for (pair_tag, fname) in pair.funs.items (): 140 tag = '%s_%d_%s' % (fname, i, pair_tag) 141 tag = syntax.fresh_name (tag, all_tags) 142 next_tags[pair_tag] = tag 143 p.add_entry_function (functions[fname], tag) 144 p.hook_tag_hints[tag] = pair_tag 145 p.replay_inline_script (tag, scripts[pair_tag]) 146 fun_tag_pairs.append ((next_tags, pair)) 147 148 p.pad_merge_points () 149 p.do_analysis () 150 151 free_hyps = [] 152 for (tags, pair) in fun_tag_pairs: 153 (inp_eqs, _) = pair.eqs 154 free_hyps += check.inst_eqs (p, (), inp_eqs, tags) 155 err_vis_opts = rep_graph.vc_options ([0, 1, 2], [1]) 156 err_vis_vc = tuple ([(n, err_vis_opts) for n in p.loop_heads () 157 if p.node_tags[n][0] == tags['C']]) 158 err_vis = (('Err', err_vis_vc), tags['C']) 159 free_hyps.append (rep_graph.pc_false_hyp (err_vis)) 160 161 addr_map = {} 162 for n in p.nodes: 163 if not p.node_tags[n][0].endswith ('_ASM'): 164 continue 165 if type (p.node_tags[n][1]) == tuple: 166 (fname, data) = p.node_tags[n][1] 167 if (logic.is_int (data) and is_addr (data) 168 and not fname.startswith ("instruction'")): 169 assert data not in addr_map, data 170 addr_map[data] = n 171 172 return (p, free_hyps, addr_map, fun_tag_pairs) 173 174def get_uniform_loop_vc (p, n): 175 l_id = p.loop_id (n) 176 assert l_id != None, n 177 if n == l_id: 178 restrs = tuple ([(l_id, rep_graph.vc_offs (0))]) 179 else: 180 restrs = tuple ([(l_id, rep_graph.vc_offs (1))]) 181 restrs = search.restr_others_both (p, restrs, 2, 2) 182 return restrs 183 184def get_vis (p, n, tag = None, focused_loops = None): 185 # not well configured for loops except in the 'uniform' case 186 if not tag: 187 tag = p.node_tags[n][0] 188 if focused_loops and tag in focused_loops: 189 l_id = focused_loops[tag] 190 assert p.loop_id (n) == l_id, (n, tag, l_id) 191 vc = get_uniform_loop_vc (p, n) 192 else: 193 (n, vc) = stack_logic.default_n_vc (p, n) 194 return ((n, vc), tag) 195 196def get_pc_hyp_local (rep, n, focused_loops = None): 197 return rep_graph.pc_true_hyp (get_vis (rep.p, n, 198 focused_loops = focused_loops)) 199 200def find_actual_call_node (p, n): 201 """we're getting call addresses from the binary trace, and using the 202 node naming convention to find a relevant graph node, but it might not 203 be the actual call node. a short breadth-first-search should hopefully 204 find it.""" 205 stack = [(n, 3)] 206 init_n = n 207 while stack: 208 (n, limit) = stack.pop (0) 209 if limit < 0: 210 continue 211 if p.nodes[n].kind == 'Call': 212 return n 213 else: 214 for c in p.nodes[n].get_conts (): 215 stack.append ((c, limit -1)) 216 trace ('failed to find Call node near %s' % init_n) 217 return None 218 219def adj_eq_seq_for_asm_fun_link (fname): 220 cc = stack_logic.get_asm_calling_convention (fname) 221 if not cc: 222 return None 223 addrs = [(p, v.typ) for arg in cc['args'] 224 for (_, p, v, _) in arg.get_mem_accesses ()] 225 inps = functions[fname].inputs 226 [stack_idx] = [i for (i, (nm, _)) in enumerate (inps) 227 if nm == 'stack'] 228 def adj (seq): 229 (x_stack, y_stack) = seq[stack_idx] 230 xsub = dict ([(v, xv) for (v, (xv, _)) in azip (inps, seq)]) 231 ysub = dict ([(v, yv) for (v, (_, yv)) in azip (inps, seq)]) 232 from logic import var_subst 233 stk_eqs = [(syntax.mk_memacc (x_stack, var_subst (p, xsub), t), 234 syntax.mk_memacc (y_stack, var_subst (p, ysub), t)) 235 for (p, t) in addrs] 236 return seq[:stack_idx] + seq[stack_idx + 1:] + stk_eqs 237 return adj 238 239def get_unique_call_site (p, fname, tag): 240 ns = [n for n in p.nodes if p.nodes[n].kind == 'Call' 241 if p.nodes[n].fname == fname 242 if p.node_tags[n][0] == tag] 243 if len (ns) == 1: 244 [n] = ns 245 return n 246 else: 247 return None 248 249def get_call_link_hyps (p, n, (from_tags, from_pair), (to_tags, to_pair), 250 focused_loops = None): 251 n = find_actual_call_node (p, n) 252 fname = p.nodes[n].fname 253 assert fname == to_pair.funs['ASM'] 254 vis = get_vis (p, n, focused_loops = focused_loops) 255 hyps = rep_graph.mk_function_link_hyps (p, vis, to_tags['ASM'], 256 adjust_eq_seq = adj_eq_seq_for_asm_fun_link (fname)) 257 258 c_fname = to_pair.funs['C'] 259 cn = get_unique_call_site (p, c_fname, from_tags['C']) 260 if cn != None: 261 vis = get_vis (p, cn, focused_loops = focused_loops) 262 hyps += rep_graph.mk_function_link_hyps (p, vis, to_tags['C']) 263 return hyps 264 265def refute_minimise_vis_hyps (rep, free_hyps, call_hyps, vis_pcs): 266 def test (call_hyps, vis_pcs): 267 hs = [h for grp in call_hyps for h in grp] + [ 268 h for (h, _) in vis_pcs] + free_hyps 269 return rep.test_hyp_whyps (syntax.false_term, hs) 270 271 if not test (call_hyps, vis_pcs): 272 return None 273 for i in range (1, len (call_hyps)): 274 vis_pcs2 = [(h, (addr, j)) for (h, (addr, j)) in vis_pcs 275 if j < i] 276 if test (call_hyps [ - i : ], vis_pcs2): 277 call_hyps = call_hyps [ - i : ] 278 vis_pcs = vis_pcs2 279 break 280 281 vis_pcs.sort (cmp = lambda (h, (addr, i)), (h2, (addr2, j)): j - i) 282 kept = [] 283 for i in range (len (vis_pcs)): 284 if not test (call_hyps, kept + vis_pcs[i + 1 :]): 285 kept.append (vis_pcs[i]) 286 287 return (call_hyps, kept) 288 289verdicts = {} 290 291new_refutes = {} 292 293def previous_verdict (call_stack, f, arc): 294 for (stack, points, verdict) in verdicts.get (f, []): 295 suffix = call_stack[len (call_stack) - len (stack) : ] 296 if tuple (suffix) == tuple (stack): 297 if verdict in ('impossible', 'impossible_in_loop'): 298 if set (points) <= set (arc): 299 return True 300 if verdict == 'possible': 301 if set (arc) <= set (points): 302 return False 303 return None 304 305def identify_function (call_stack, addrs): 306 fs = set ([get_body_addrs_fun (addr) for addr in addrs]) - set ([None]) 307 assert len (fs) <= 1, (fs, addrs) 308 if fs: 309 [f] = list (fs) 310 return f 311 call = call_stack[-1] 312 prev_fn = get_body_addrs_fun (call) 313 cn = find_actual_call_node (functions[prev_fn], call) 314 fn = functions[prev_fn].nodes[cn].fname 315 return fn 316 317def build_compound_problem_with_links (call_stack, f): 318 funs = [get_body_addrs_fun (addr) for addr in call_stack] + [f] 319 (p, hyps, addr_map, tag_pairs) = build_compound_problem (funs) 320 call_tags = zip (tag_pairs[:-1], tag_pairs[1:]) 321 call_hyps = [get_call_link_hyps (p, addr_map[n], from_tp, to_tp) 322 for (n, (from_tp, to_tp)) in zip (call_stack, call_tags)] 323 wcet_hyps = [] 324 from rep_graph import eq_hyp 325 for (entry, tag, _, inputs) in p.entries: 326 entry_vis = ((entry, ()), tag) 327 for f in target_objects.hooks ('extra_wcet_assertions'): 328 for assn in f (inputs): 329 wcet_hyps.append (eq_hyp ((assn, entry_vis), 330 (syntax.true_term, entry_vis))) 331 return (p, hyps + [h for hs in call_hyps for h in hs] 332 + wcet_hyps, addr_map) 333 334def all_reachable (p, addrs): 335 assert set (addrs) <= set (p.nodes) 336 return all ([p.is_reachable_from (addrs[i], addrs[j]) or 337 p.is_reachable_from (addrs[j], addrs[i]) 338 for i in range (len (addrs)) 339 for j in range (i + 1, len (addrs))]) 340 341parent_ctxt_limit = 3 342 343def call_stack_parent_arc_extras (stack, ctxt_arcs, max_length, top_loop): 344 rng = range (1, len (stack))[ - parent_ctxt_limit : ][ - max_length : ] 345 arc_extras = [] 346 for i in rng: 347 prev_stack = stack[:i] 348 f = body_addrs[stack[i]] 349 p = functions[f].as_problem (problem.Problem) 350 arcs = ctxt_arcs[tuple (prev_stack)] 351 if top_loop != None and i == rng[0]: 352 assert uniform_loop_id (stack[i]) == top_loop, (stack, i) 353 arcs = [[x for x in a if uniform_loop_id (x) == top_loop] 354 for a in arcs] 355 arcs = [a for a in arcs if a] 356 arcs = [a for a in arcs if all_reachable (p, a + [stack[i]])] 357 arcs = sorted ([(len (a), a) for a in arcs]) 358 if arcs: 359 (_, arc) = arcs[-1] 360 arc_extras.extend ([(addr, len (stack) - i) 361 for addr in arc]) 362 return arc_extras 363 364def add_arc_extras (arc, extras): 365 return [(addr, 0) for addr in arc] + extras 366 367last_refute_attempt = [None] 368 369has_complex_loop_cache = {} 370 371def has_complex_loop (fname): 372 if fname in has_complex_loop_cache: 373 return has_complex_loop_cache[fname] 374 p = functions[fname].as_problem (problem.Problem) 375 p.do_analysis () 376 result = bool ([h for h in p.loop_heads () 377 if problem.has_inner_loop (p, h)]) 378 has_complex_loop_cache[fname] = result 379 return result 380 381def pick_stack_setup (call_stack): 382 # how much stack to use? 383 stack = list (call_stack [ - parent_ctxt_limit : ]) 384 for (i, addr) in reversed (list (enumerate (stack))): 385 f2 = get_body_addrs_fun (addr) 386 if should_avoid_fun (f2) or has_complex_loop (f2): 387 return (None, stack [ i + 1 : ]) 388 if uniform_loop_id (addr) != None: 389 return (uniform_loop_id (addr), stack [ i : ]) 390 elif addr_in_loop (addr): 391 return (None, stack [ i + 1 : ]) 392 return (None, stack) 393 394loops_info_cache = {} 395 396def fun_loops_info (fname): 397 if fname in loops_info_cache: 398 return loops_info_cache[fname] 399 p = functions[fname].as_problem (problem.Problem) 400 p.do_analysis () 401 info = {} 402 for l_id in p.loop_heads (): 403 ext_reachable = [n for n in p.loop_body (l_id) 404 if [n2 for n2 in p.preds[n] if p.loop_id (n2) != l_id]] 405 if ext_reachable != [l_id]: 406 trace ("Loop in %s non-uniform, additional entries %s." 407 % (fname, ext_reachable)) 408 uniform = False 409 elif problem.has_inner_loop (p, l_id): 410 trace ("Loop in %s non-uniform, inner loop." % fname) 411 uniform = False 412 else: 413 assert is_addr (l_id), (fname, l_id) 414 uniform = True 415 for n in p.loop_body (l_id): 416 info[n] = (l_id, uniform) 417 loops_info_cache[fname] = info 418 return info 419 420def addr_in_loop (addr): 421 fname = get_body_addrs_fun (addr) 422 info = fun_loops_info (fname) 423 if addr not in info: 424 return None 425 (l_id, uniform) = info[addr] 426 return (l_id != None) 427 428def uniform_loop_id (addr): 429 fname = get_body_addrs_fun (addr) 430 info = fun_loops_info (fname) 431 if addr not in info: 432 return None 433 (l_id, uniform) = info[addr] 434 if not uniform: 435 return None 436 return l_id 437 438def refute_function_arcs (call_stack, arcs, ctxt_arcs): 439 last_refute_attempt[0] = (call_stack, arcs, ctxt_arcs) 440 f = identify_function (call_stack, 441 [(addr, 0) for arc in arcs for addr in arc]) 442 443 # easy function limit refutations 444 if not (ctxt_within_function_limits (call_stack) 445 and function_reachable_within_limits (f)): 446 verdicts.setdefault (f, []) 447 if call_stack: 448 vdct = (call_stack, [], 'impossible') 449 else: 450 min_addr = min ([addr for arc in arcs for addr in arc]) 451 vdct = ([], [min_addr], 'impossible') 452 verdicts[f].append (vdct) 453 new_refutes[f] = True 454 print 'added %s refutation %s: %s' % (f, vdct[0], vdct[1]) 455 return 456 457 # ignore complex loops 458 if has_complex_loop (f): 459 print 'has complex loop: %s, skipping' % f 460 return 461 462 (top_loop, stack) = pick_stack_setup (call_stack) 463 arc_extras = call_stack_parent_arc_extras (call_stack, ctxt_arcs, 464 len (stack), top_loop) 465 466 arcs = [arc for arc in arcs 467 if previous_verdict (stack, f, 468 add_arc_extras (arc, arc_extras)) == None] 469 if not arcs: 470 return 471 472 funs = [body_addrs[addr] for addr in stack] + [f] 473 (p, hyps, addr_map, tag_pairs) = build_compound_problem (funs) 474 475 focused_loops = {} 476 if top_loop != None: 477 top_loop_split = p.loop_id (addr_map[top_loop]) 478 top_loop_tag = p.node_tags[top_loop_split][0] 479 assert top_loop_tag in tag_pairs[0][0].values () 480 focused_loops[top_loop_tag] = top_loop_split 481 482 rep = rep_graph.mk_graph_slice (p) 483 call_tags = zip (tag_pairs[:-1], tag_pairs[1:]) 484 call_hyps = [get_call_link_hyps (p, addr_map[n], from_tp, to_tp, 485 focused_loops = focused_loops) 486 for (n, (from_tp, to_tp)) in zip (stack, call_tags)] 487 488 for arc in arcs: 489 arc2 = add_arc_extras (arc, arc_extras) 490 if previous_verdict (stack, f, arc2) != None: 491 continue 492 print 'fresh %s arc %s: %s' % (f, stack, arc) 493 vis_pcs = [(get_pc_hyp_local (rep, addr_map[addr], 494 focused_loops = focused_loops), (addr, i)) 495 for (addr, i) in arc2] 496 vis_pcs = dict (vis_pcs).items () 497 498 res = refute_minimise_vis_hyps (rep, hyps, call_hyps, vis_pcs) 499 if res == None: 500 verdicts.setdefault (f, []) 501 verdicts[f].append ((stack, list (arc2), 'possible')) 502 continue 503 504 (used_call_hyps, used_vis_pcs) = res 505 stack2 = stack [ - len (used_call_hyps) : ] 506 used_vis = [(addr, i) for (_, (addr, i)) in used_vis_pcs] 507 verdicts.setdefault (f, []) 508 if len (stack2) == len (stack) and top_loop != None: 509 vdct = 'impossible_in_loop' 510 else: 511 vdct = 'impossible' 512 verdicts[f].append ((stack2, used_vis, vdct)) 513 new_refutes[f] = True 514 print 'added %s refutation %s: %s' % (f, stack, used_vis) 515 516# function limits. mostly used by loop_bounds, but also present here 517def function_limit (fname): 518 for hook in target_objects.hooks ('wcet_function_limits'): 519 if fname in hook: 520 return hook[fname] 521 return None 522 523# functions to avoid. won't ever include these in parent contexts for 524# arc refutations 525def should_avoid_fun (fname): 526 for hook in target_objects.hooks ('wcet_functions_to_avoid'): 527 if fname in hook: 528 return True 529 return False 530 531reachable_functions = {} 532 533def build_reachable_functions (): 534 fcall_graph = dict ([(fname, functions[fname].function_calls ()) 535 for fname in functions]) 536 is_reachable = dict ([(fname, False) for fname in functions]) 537 called = set ([f for fs in fcall_graph.itervalues () for f in fs]) 538 uncalled = set (fcall_graph) - called 539 frontier = uncalled 540 while frontier: 541 f = frontier.pop () 542 if is_reachable[f]: 543 continue 544 elif function_limit (f) == 0: 545 continue 546 else: 547 is_reachable[f] = True 548 frontier.update (fcall_graph[f]) 549 reachable_functions.update (is_reachable) 550 reachable_functions[('IsLoaded', None)] = True 551 552def function_reachable_within_limits (fname): 553 if fname not in reachable_functions: 554 build_reachable_functions () 555 return reachable_functions[fname] 556 557def ctxt_within_function_limits (call_ctxt): 558 for (i, addr) in enumerate (call_ctxt): 559 fname = identify_function (call_ctxt[:i], [addr]) 560 if not function_reachable_within_limits (fname): 561 return False 562 return True 563 564def serialise_verdicts (fname): 565 f = open (fname, 'w') 566 for (_, vs) in verdicts.iteritems (): 567 for (stack, visits, verdict) in vs: 568 visit_str = '[%s]' % (','.join (['%d<-%d' % (addr, i) 569 for (addr, i) in visits])) 570 f.write ('%s: %s: %s\n' % (list (stack), visit_str, 571 verdict)) 572 f.close () 573 574def load_verdicts (fname): 575 f = open (fname) 576 for l in f: 577 bits = l.split(':') 578 if len (bits) < 3: 579 bits = set ([bit for bit in bits if bit.strip()]) 580 assert not bits, bits 581 [stack, visits, verdict] = bits 582 stack = parse_num_list (stack) 583 visits = parse_num_arrow_list (visits) 584 verdict = verdict.strip () 585 assert verdict in ('possible', 'impossible', 586 'impossible_in_loop'), verdict 587 fn = identify_function (stack, visits) 588 verdicts.setdefault (fn, []) 589 verdicts[fn].append ((stack, visits, verdict)) 590 f.close () 591 592last_report = [0] 593exceptions = [] 594 595def refute (inp_fname, out_fname, prev_fnames, instance = None): 596 f = open (inp_fname) 597 ctxt_arcs = parse_ctxt_arcs (f) 598 f.close () 599 body_addrs.clear () 600 setup_body_addrs () 601 verdicts.clear () 602 new_refutes.clear () 603 for fn in prev_fnames: 604 load_verdicts (fn) 605 report = {} 606 last_report[0] = report 607 for (ctxt, arcs) in ctxt_arcs.iteritems (): 608 if instance: 609 (a, b) = instance 610 if hash (('foo', tuple (ctxt))) % b != a: 611 continue 612 try: 613 refute_function_arcs (ctxt, arcs, ctxt_arcs) 614 report[ctxt] = 'Success' 615 except problem.Abort: 616 report[ctxt] = 'ProofAbort' 617 except Exception, e: 618 import sys, traceback 619 exceptions.append ((ctxt, arcs, ctxt_arcs)) 620 exception = sys.exc_info () 621 (etype, evalue, tb) = exception 622 ss = traceback.format_exception (etype, evalue, tb) 623 report[ctxt] = '\n'.join (['EXCEPTION'] + ss) 624 print 'EXCEPTION in handling %s, %s' % (ctxt, arcs) 625 for s in ss[:3]: 626 print s 627 if len (ss) > 3: 628 print '...' 629 serialise_verdicts (out_fname) 630 print 'Found new refutations: %s' % bool (new_refutes) 631 return (bool (new_refutes), report) 632 633if __name__ == '__main__': 634 args = target_objects.load_target_args () 635 prevs = [arg[5:] for arg in args if arg.startswith ('prev:')] 636 args = [arg for arg in args if not arg.startswith ('prev:')] 637 insts = [arg for arg in args if arg.startswith ('instance:')] 638 if insts: 639 args = [arg for arg in args if not arg.startswith ('instance:')] 640 assert len (insts) == 1, insts 641 [inst] = insts 642 bits = inst.split(':') 643 assert len (bits) == 3, (insts, bits) 644 [_, a, b] = bits 645 instance = (int (a), int (b)) 646 else: 647 instance = None 648 if len (args) < 2: 649 print 'Usage: python trace_refute <target> <refutables> [prev:output] <output>' 650 print 'where <target> as per graph-refine, <refutables> from reconstruct.py' 651 print 'and <output> is output filename.' 652 print 'Optional previous output may be loaded.' 653 print 'e.g. python trace_refute new-gcc-O2 new-gcc-O2/ctxt_arcs.txt prev:refutes.txt refutes.txt' 654 sys.exit (1) 655 else: 656 (new, _) = refute (args[0], args[1], prevs, 657 instance = instance) 658 import sys 659 if new: 660 sys.exit (127) 661 else: 662 sys.exit (0) 663 664 665