search

Vector35 / binaryninja-api

Public API, examples, documentation and issues for Binary Ninja
https://binary.ninja/
MIT License
893 stars 199 forks source link

Enhanced Dataflow Solver #968

Open pmackinlay opened 6 years ago

pmackinlay commented 6 years ago

Binary Ninja Version: 1.1.1068-dev Personal, beb4a48f Platform: Windows 10 (10.0)

This is a very similar issue to #953, with the difference being that the flow condition is based on a copy of the value in question.

Referring to the screenshot below, BN correctly determines the range of values for r0 @ 6 is -0x8000..0x7fff, but fails to further constrain that range through the control flow @ 8, although it should be able to unambiguously do so due to the expression @ 7.

In this case, BN also fails to create the outward edges from @ 16, probably because the unconstrained range is too large.

image

joshwatson commented 6 years ago

This is probably related to #801

bpotchik commented 6 years ago

This will not be fixed by #801. We will have to add an algebraic solver for this pattern. I will look into this at some point.

bpotchik commented 6 years ago

Just an update. I have a working solver for this and will push pending some validation and performance tests. screen shot 2018-03-12 at 11 20 28 am