nevillegrech / gigahorse-toolchain

A binary lifter and analysis framework for Ethereum smart contracts
Other
290 stars 59 forks source link

small bugfixes in memory modeling #107

Closed sifislag closed 1 year ago

snf commented 1 year ago

I think this may bring issues later as values won't be classified as NumericValues? Also last time I checked the values saturated to 0x7fffffff.

Still have this PR here which is probably not the correct solution either: https://github.com/nevillegrech/gigahorse-toolchain/pull/42/files . The reason I went for it is because most of the ones I observed were negative.

github-actions[bot] commented 1 year ago

Test Results (Souffle 2.3)

43 tests  ±0   43 :heavy_check_mark: ±0   22m 37s :stopwatch: + 3m 48s   1 suites ±0     0 :zzz: ±0    1 files   ±0     0 :x: ±0 

Results for commit e8e3ec33. ± Comparison against base commit 44086dd3.

:recycle: This comment has been updated with latest results.

github-actions[bot] commented 1 year ago

Test Results (Souffle 2.4)

43 tests  ±0   43 :heavy_check_mark: ±0   19m 25s :stopwatch: - 1m 34s   1 suites ±0     0 :zzz: ±0    1 files   ±0     0 :x: ±0 

Results for commit e8e3ec33. ± Comparison against base commit 44086dd3.

:recycle: This comment has been updated with latest results.

sifislag commented 1 year ago

Hi @snf, my reasoning is that Variable_NumericValue() will contain the subset of Variable_Value() that we can model with souffle's arithmetic. I had a quick look through the uses and it looked consistent with what I had in mind. In all other cases we can use Variable_Value() directly. Do you want us to revisit your PR based on an example? You're right about 0x7fffffff, changing it.

sifislag commented 1 year ago

Went with a different approach to solving the problem you've identified in my latest commit. Check it out and let me know what you think.

snf commented 1 year ago

I cannot try til next week but it looks good to me. Thanks for the change

sifislag commented 1 year ago

Thanks for your input! Let me know when you're able to check it.