seL4-l4v-10.1.1/graph-refine/check.py

31 	for (tag, fname) in pairing.funs.items ():
32 		p.add_entry_function (functions[fname], tag)
79 	[compare_tag] = [tag for tag in p.pairing.tags if tag != 'C']
130 def consider_inline (matched_funs, tag, force_inline, skip_underspec = False):
131 	return lambda (p, n): consider_inline1 (p, n, matched_funs, tag,
137 		tag_map = dict ([(tag, tag) for tag in p.tags ()])
175 			(self.point, self.tag) = args
189 			tag = p.node_tags[self.point][0]
191 				tag, kind, '%d' % x, '%d' % y])
193 			tag = p.node_tags[self.point][0]
196 				tag, '%d' % n, '%d' % len (eqs)])
213 			ss.extend (['CaseSplit', '%d' % self.point, self.tag])
277 		tag = ss[i + 2]
286 		tag = ss[i + 2]
306 		tag = ss[i + 2]
309 		return (i, ProofNode ('CaseSplit', (n, tag), [p1, p2]))
338 		(point, tag) = args
339 		visit = ((point, restrs), tag)
362 def split_visit_one_visit (tag, details, restrs, visit):
376 	visit = ((split, ((split, visit), ) + restrs), tag)
446 			# reachable from n (or on another tag)
568 def loop_eq_hyps_at_visit (tag, split, eqs, restrs, visit_num,
571 	visit = split_visit_one_visit (tag, details, restrs, visit_num)
572 	start = split_visit_one_visit (tag, details, restrs, vc_num (0))
584 	hyps = [(Hyp ('PCImp', visit, start), '%s pc imp' % tag)]
586 			(split, 0), use_if_at = use_if_at), '%s const' % tag)
593 	(tag, _) = p.node_tags[point]
594 	vis = ((point, restrs + tuple ([(point, vc_num (0))])), tag)
597 def single_loop_induct_base_checks (p, restrs, hyps, tag, split, n, eqs):
601 		reach = split_visit_one_visit (tag, details, restrs, vc_num (i))
606 			for (hyp, desc) in loop_eq_hyps_at_visit (tag, split,
610 def single_loop_induct_step_checks (p, restrs, hyps, tag, split, n,
615 	cont = split_visit_one_visit (tag, details, restrs, vc_offs (n))
618 		for (h, _) in loop_eq_hyps_at_visit (tag, split,
623 		for (hyp, desc) in loop_eq_hyps_at_visit (tag, split, eqs,
628 	(tag, _) = p.node_tags[split]
629 	visit = split_visit_one_visit (tag, details, restrs, vc_offs (0))
633 def single_loop_rev_induct_base_checks (p, restrs, hyps, tag, split,
636 	cont = split_visit_one_visit (tag, details, restrs, vc_offs (1))
643 		+ [h for (h, _) in loop_eq_hyps_at_visit (tag,
649 def single_loop_rev_induct_checks (p, restrs, hyps, tag, split,
652 	curr = split_visit_one_visit (tag, details, restrs, vc_offs (1))
653 	cont = split_visit_one_visit (tag, details, restrs, vc_offs (2))
660 		+ [h for (h, _) in loop_eq_hyps_at_visit (tag, split,
667 	(tag, _) = p.node_tags[point]
668         checks = (single_loop_induct_step_checks (p, restrs, hyps, tag,
670 		+ single_loop_induct_base_checks (p, restrs, hyps, tag,
672 		+ single_loop_rev_induct_checks (p, restrs, hyps, tag,
675 			tag, point, n_bound, eqs, pred))