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

169 		tag = p.node_tags[n][0]
170 		hyp = rep_graph.pc_false_hyp ((default_n_vc (p, n), tag))
205 	for tag in set ([p.node_tags[n][0] for (n, _) in n_ptrs]):
206 		hyps = hyps + init_correctness_hyps (p, tag)
228 def init_correctness_hyps (p, tag):
229 	(_, fname, _) = p.get_entry_details (tag)
236 	if tag in pair.funs:
237 		true_tag = tag
238 	elif p.hook_tag_hints.get (tag, tag) in pair.funs:
239 		true_tag = p.hook_tag_hints.get (tag, tag)
246 	return check.inst_eqs (p, (), eqs, {true_tag: tag})
262 def get_extra_sp_defs (rep, tag):
271 		if rep.p.node_tags[n_vc[0]][0] == tag
285 def get_stack_sp (p, tag):
287 	entry = p.get_entry (tag)
288 	renames = p.entry_exit_renames (tags = [tag])
289 	r = renames[tag + '_IN']
312 	tag = p.node_tags[n][0]
313 	return tag == 'ASM' or p.hook_tag_hints.get (tag, None) == 'ASM'
327 def adjusted_var_dep_outputs_for_tag (p, tag):
328 	(ent, fname, _) = p.get_entry_details (tag)
335 			in azip (fun.outputs, p.outputs[tag])
342 	for tag in p.outputs:
343 		ent = p.get_entry (tag)
345 			outputs[tag] = adjusted_var_dep_outputs_for_tag (p, tag)
347 			outputs[tag] = p.outputs[tag]
349 		tag = p.node_tags[n][0]
350 		return outputs[tag]
471 def mk_get_local_offs (p, tag, sp_reps):
472 	(stack, _) = get_stack_sp (p, tag)
493 def get_loop_virtual_stack_analysis (p, tag):
496 	cache_key = ('loop_stack_analysis', tag)
500 	(ent, fname, _) = p.get_entry_details (tag)
501 	(_, sp) = get_stack_sp (p, tag)
506 	renames = p.entry_exit_renames (tags = [tag])
507 	r = renames[tag + '_OUT']
510 	ns = [n for n in p.nodes if p.node_tags[n][0] == tag]
536 	loc_offs = mk_get_local_offs (p, tag, rep_offs)
552 	preds['Ret'] = [n for n in preds['Ret'] if p.node_tags[n][0] == tag]
553 	preds['Err'] = [n for n in preds['Err'] if p.node_tags[n][0] == tag]
575 	tag = p.node_tags[split][0]
583 		upd_offsets, _) = get_loop_virtual_stack_analysis (p, tag)
589 	(stack, _) = get_stack_sp (p, tag)
875 def function_link_assns (p, call_site, tag):
877 	return rep_graph.mk_function_link_hyps (p, call_vis, tag)
883 	tag = 'fun0'
884 	p.add_entry_function (functions[f], tag)
890 		res = find_unknown_recursion (p, group, idents, tag, assns,
899 		tag = 'fun%d' % len (chain)
900 		(args, _, entry) = p.add_entry_function (functions[fname], tag)
902 		assns += function_link_assns (p, res, tag)
916 	if find_unknown_recursion (p, group, idents, tag, [], []) == None:
930 		entry_vis = ((entry, ()), tag)
932 		res = find_unknown_recursion (p, group, idents, tag,
945 def find_unknown_recursion (p, group, idents, tag, assns, extra_unfolds):
951 		if p.node_tags[n][0] != tag:
1085 		tag_set = [tag for tag in p.tags ()
1086 			if is_asm_node (p, p.get_entry (tag))]
1087 	frontier = [p.get_entry (tag) for tag in tag_set]
1172 def get_functions_with_tag (tag):
1173 	if tag in funs_with_tag:
1174 		return funs_with_tag[tag]
1175 	visit = set ([pre_pairings[f][tag] for f in pre_pairings
1176 		if tag in pre_pairings[f]])
1177 	visit.update ([pair.funs[tag] for f in pairings
1178 		for pair in pairings[f] if tag in pair.funs])
1184 	funs_with_tag[tag] = funs
1272 	tag = p.node_tags[n][0]
1273 	(_, sp) = get_stack_sp (p, tag)