Register initialization

[r4dr3fr4d]

It seems Maat initializes all registers to 0...is this intentional and is there a simple way to blanket initialize all registers to symbolic values instead? I would think that would be the default...

[Boyan-MILANOV]

We intentionally initialize all registers to concrete values. Using 0 as a default seems to make a lot of sense.

Initializing registers with symbolic variables by default could have some wanted side-effects. For instance, on X64, let's assume that we initialize all ZMM registers with symbolic variables. If we then set sub-registers like XMM or YMM to concrete values, the whole ZMM registers will still hold symbolic expressions (because the upper bits are still symbolic). And then it is likely that the more instructions we run that modify those sub-registers, the more complex the symbolic expressions become. Hence, we would propagate useless symbolic data even though the program is doing purely concrete stuff. We definitely want to avoid this as the default behaviour.

Is there something that prevents you from manually symbolizing the desired registers?

[r4dr3fr4d]

No, there isn't, it's just a small pain. I can't help but think there may be a way to circumvent that problem though - maybe treat non-overlapping parts of registers as distinct, and then when updating an outer one, automatically update the inner ones?

[Boyan-MILANOV]

treat non-overlapping parts of registers as distinct, and then when updating an outer one, automatically update the inner ones

Doing this will add a lot of complexity to Maat's architecture descriptions and symbolic CPU. That would be more code, more possible mistakes and oversights when specifying the subregister map, and make the codebase harder to maintain. I really don't think it would be a reasonable design decision.

Assigning registers manually is the way to go. It should be pretty easy to do from Python, like

for reg in ['rax', 'rbx', ...]:
    setattr(engine.cpu, reg, Var(64,reg))

In case people want to really make every single register symbolic, it might be worth exposing the Arch class in the bindings so that they can do Var(engine.arch.reg_size(reg), reg) to generate a symbolic expression with the correct size for every register.

[r4dr3fr4d]

Definitely agree that simpler is better.