dgpv / bsst

B'SST: Bitcoin-like Script Symbolic Tracer
Other
32 stars 5 forks source link

Add ability to explicitly specify possible values for data #15

Closed dgpv closed 10 months ago

dgpv commented 11 months ago

Like:

and use this to assist the analysis - it can reduce the solving times, and limit the scope of the analysis, if, for example, we specify possible values for dynamic stack index for PICK

While in case of placeholders, this would work as an explicit constraints ("will not be above ..."), in case of values on the stack and references it will be different

For values on the stack and references, we actually want to check if the "restriction" condition is true, and add a warning if it is not.

For dynamic indexes on the stack, such warning should be prominent, and tell that the analysis is incomplete. This is because for dynamic arguments, we will need to create a separate execution path for each possible value of dynamic stack index. If we use this "restriction" to limit the number of created/analyzed execution paths, and we know that the the condition can be false, we know that our analysis will be incomplete.

dgpv commented 10 months ago

18 fixes this

dgpv commented 10 months ago

18 was merged, closing