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