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

241 				pc1 = rep.get_pc (visit1, tag = tag1)
245 				pc2 = rep.get_pc (visit2, tag = tag2)
253 			x_pc_env = rep.get_node_pc_env (xvis[0], tag = xvis[1])
254 			y_pc_env = rep.get_node_pc_env (yvis[0], tag = yvis[1])
263 				x_pc = rep.get_pc (xvis[0], tag = xvis[1])
264 				y_pc = rep.get_pc (yvis[0], tag = yvis[1])
271 def check_vis_is_vis (((n, vc), tag)):
341 	def get_tag_vcount (self, (n, vcount), tag):
342 		if tag == None:
343 			tag = self.p.node_tags[n][0]
346 			if self.p.node_tags[split][0] == tag]
349 				return (tag, None)
361 		return (tag, vcount)
363 	def get_node_pc_env (self, (n, vcount), tag = None, request = True):
364 		tag, vcount = self.get_tag_vcount ((n, vcount), tag)
368 		if (tag, n, vcount) in self.node_pc_envs:
369 			return self.node_pc_envs[(tag, n, vcount)]
372 			self.pc_env_requests.add (((n, vcount), tag))
374 		self.warm_pc_env_cache ((n, vcount), tag)
376 		pc_env = self.get_node_pc_env_raw ((n, vcount), tag)
379 				tag, pc_env)
381 		assert not (tag, n, vcount) in self.node_pc_envs
382 		self.node_pc_envs[(tag, n, vcount)] = pc_env
384 			self.node_pc_env_order.append ((tag, n, vcount))
388 	def warm_pc_env_cache (self, n_vc, tag):
395 					if (tag, p[0], p[1])
398 						== (tag, n_vc[1])]
412 			self.get_node_pc_env (n_vc, tag, request = False)
526 	def get_node_pc_env_raw (self, (n, vcount), tag):
535 			if self.p.node_tags[n_prev][0] == tag
553 			name = self.path_cond_name ((n, vcount), tag)
589 		tag, vcount = self.get_tag_vcount ((n, vcount), None)
646 		tag = self.p.node_tags[n[0]][0]
647 		app_eqs = self.apply_known_eqs_tm (n, tag)
731 	def fetch_known_eqs (self, n_vc, tag):
734 		eqs = self.p.known_eqs.get ((n_vc, tag))
747 	def apply_known_eqs_pc_env (self, n_vc, tag, (pc, env)):
748 		eqs = self.fetch_known_eqs (n_vc, tag)
761 	def apply_known_eqs_tm (self, n_vc, tag):
762 		eqs = self.fetch_known_eqs (n_vc, tag)
801 	def get_func (self, n_vc, tag = None):
804 		tag, vc = self.get_tag_vcount (n_vc, tag)
811 			self.get_node_pc_env (cont, tag = tag)
948 	def path_cond_name (self, n_vc, tag):
950 			self.node_count_name (n_vc), tag)
1044 	def get_pc (self, (n, vcount), tag = None):
1045 		pc_env = self.get_node_pc_env ((n, vcount), tag = tag)
1047 			trace ('Warning: unreachable n_vc, tag: %s, %s' % ((n, vcount), tag))
1052 	def to_smt_expr (self, expr, (n, vcount), tag = None):
1053 		pc_env = self.get_node_pc_env ((n, vcount), tag = tag)
1129 		for ((n, vc), tag) in reqs:
1130 			self.get_node_pc_env ((n, vc), tag = tag)
1233 	for (n_vc, tag) in requests:
1234 		if tag == 'InductVar':
1237 			rep.get_pc (n_vc, tag = tag)
1243 def mk_function_link_hyps (p, call_vis, tag, adjust_eq_seq = None):
1244 	(entry, _, args) = p.get_entry_details (tag)