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