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