The collect_mem_read_expr function is used to model assumptions about memory reads in comparative analysis. Here is the beginning of it:
let collect_mem_read_expr (env1 : Env.t) (env2 : Env.t) (exp : Exp.t)
(init_addrs : Addr.Set.t) (offset : Constr.z3_expr -> Constr.z3_expr)
: Constr.z3_expr list =
let ctx = Env.get_context env1 in
let bap_mem1 = Env.get_mem env1 in
let bap_mem2 = Env.get_mem env2 in
(* read_addr = init_addr1 \/ read_addr = init_addr2 \/ ... *)
let init_addrs read_addr =
Addr.Set.fold init_addrs ~init:[] ~f:(fun constr addr ->
let addr = word_to_z3 ctx addr in
let eq = Bool.mk_eq ctx read_addr addr in
eq :: constr) |>
Bool.mk_or ctx
in
...
The init_addrs property is used to check if the address we're reading from was initialized. But if the initialized data section is big, this is a massive conjunction. Probably we should take in ranges of initialized addresses and check if the address is in those ranges.
The
collect_mem_read_exprfunction is used to model assumptions about memory reads in comparative analysis. Here is the beginning of it:The
init_addrsproperty is used to check if the address we're reading from was initialized. But if the initialized data section is big, this is a massive conjunction. Probably we should take in ranges of initialized addresses and check if the address is in those ranges.