Closed zhanghongce closed 4 years ago
Agree, we should address this issue. I feel like lexically checking/sharing may be very limited, and we should at least have some sort of the semantic checks (like FRAIG in logic synthesis).
Two possible approaches in my mind:
I suggest we don't do hashing/sharing at model construct time, and to have a pass (one-time effort) that can be called optionally afterward.
I already have a pass PassSimplifyInstrUpdate
in my branch plainc
that uses SMT to simplify the state update functions. It's still an early-stage feature, which only looks for its own sub-trees and find equivalent (modulo decode) ones to replace. Perhaps can be reused/adapted for the model-wise pruning.
I was thinking about updating
ExprMngr
a bit, using the hash collision handling ofstd::unordered_map
. As we earlier experimented, in some cases (e.g., AES's AST), hash collisions are very likely to occur, instead of designing the hash to avoid collision, maybe we can target handling such collisions? Previously, intmpl-synth
, Pramod used Z3 to (semantically) check and distinguish expressions if they have the same hash. What do you think about lexically checking instead? In that case, we could create a function/class that converts ASTs to strings, for example. (Vars to their names, constants to the constant, OPs to the opname) And compare the strings for lexical matching. Do you think if it (either semantically or lexically) will work?