1import syntax
2import target_objects
3
4def get_cache (p):
5	k = 'c_rodata_hook_cache'
6	if k not in p.cached_analysis:
7		p.cached_analysis[k] = {}
8	return p.cached_analysis[k]
9
10def hook (rep, (n, vc)):
11	p = rep.p
12	tag = p.node_tags[n][0]
13	is_C = tag == 'C' or p.hook_tag_hints.get (tag, None) == 'C'
14	if not is_C:
15		return
16	upd_ps = [rep.to_smt_expr (ptr, (n, vc))
17		for (kind, ptr, v, m) in p.nodes[n].get_mem_accesses ()
18		if kind == 'MemUpdate']
19	if not upd_ps:
20		return
21	cache = get_cache (p)
22	for ptr in set (upd_ps):
23		pc = rep.get_pc ((n, vc))
24		eq_rodata = rep.solv.get_eq_rodata_witness (ptr)
25		hyp = rep.to_smt_expr (syntax.mk_implies (pc,
26			syntax.mk_not (eq_rodata)), (n, vc))
27		if ((n, vc), ptr) in cache:
28			res = cache[((n, vc), ptr)]
29		else:
30			res = rep.test_hyp_whyps (hyp, [], cache = cache)
31			cache[((n, vc), ptr)] = res
32		if res:
33			rep.solv.assert_fact (hyp, {})
34
35module_hook_k = 'c_rodata'
36target_objects.add_hook ('post_emit_node', module_hook_k, hook)
37target_objects.use_hooks.add (module_hook_k)
38
39