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