Dynamic buffers via SMT lists #500

MrChico · 2020-09-07T15:36:47Z

Replaces #491

tests passing

MrChico · 2020-09-16T14:35:58Z

getting annoying, mysterious errors in the communication with the solver and sbv

*** Data.SBV: Unexpected response from the solver, context: push:
***
***    Sent      : (push 1)
***    Expected  : success
***    Received  : (error "line 4036 column 7: canceled")
***
***    Executable: /nix/store/i0rqzy3avr6mdbggr28kk91igdripvnn-z3-4.8.8/bin/z3
***    Options   : -nw -in -smt2

d-xo · 2020-09-16T13:30:28Z

src/hevm/test/test.hs

+      -- testCase "calldata beyond length must be 0" $ runSMTWith z3
+      --   $ query $ do calldatalist <- freshVar_
+      --                -- works with length .< 10, but not 100...
+      --                constrain $ SL.length calldatalist .< 10
+      --                let cd = DynamicSymBuffer calldatalist
+      --                constrain $ 0 ./= readSWord (sw256 $ sFromIntegral $ len cd) cd
+      --                checkSat >>= \case
+      --                  Sat -> error "should be false"
+      --                  Unsat -> return ()
+      --                  Unk -> error "timed out!"


Did you mean to leave this commented?

I think I will remove this

d-xo · 2020-09-16T13:31:38Z

src/hevm/test/test.hs

+                       Unk -> error "timed out!"
+
+      ,
+        testCase "comparing function selector" $ runSMTWith z3{transcript=Just "sameno.smt2"} $ do


did you mean to leave the transcript here?

d-xo · 2020-09-16T13:33:07Z

src/hevm/test/test.hs

+                     constrain $ SL.length calldatalist .< 100
+                     constrain $ sw256 (sFromIntegral $ SL.length calldatalist) .< sw256 100


Why do we need both of these contraints?

it turned out to yield better performance in practice

d-xo · 2020-09-16T14:48:45Z

nix/hevm-tests/smt-checker.nix

+    # # OpCalldatacopy
+    # "loops/for_loop_array_assignment_memory_memory.sol"
+    # "loops/for_loop_array_assignment_memory_storage.sol"
+    # "loops/while_loop_array_assignment_memory_memory.sol"
+    # "loops/while_loop_array_assignment_memory_storage.sol"
+    # "types/address_call.sol"
+    # "types/address_delegatecall.sol"
+    # "types/address_staticcall.sol"
+    # "types/array_aliasing_storage_2.sol"
+    # "types/array_aliasing_storage_3.sol"
+    # "types/array_aliasing_storage_5.sol"
+    # "types/array_branch_1d.sol"
+    # "types/array_branches_1d.sol"
+    # "types/array_dynamic_parameter_1.sol"
+    # "types/array_dynamic_parameter_1_fail.sol"
+    # "types/bytes_1.sol"
+    # "types/bytes_2.sol"
+    # "types/bytes_2_fail.sol"
+    # "types/mapping_unsupported_key_type_1.sol"
+    # "types/function_type_array_as_reference_type.sol"


Did you mean to leave these commented?

d-xo · 2020-09-16T15:08:50Z

src/hevm/src/EVM.hs

@@ -1721,8 +1721,13 @@ notStatic continue = do
    then vmError StateChangeWhileStatic
    else continue

+burnSym :: SymWord -> EVM () -> EVM ()
+burnSym n continue = case maybeLitWord n of
+  Nothing -> continue -- smt query (TODO: no gas mode)


Does this mean no gas is deduced when dealing with symbolic values?

currently yes. But there should really be a query made here unless run in --no-gas mode.

MrChico force-pushed the slistbuffer branch 4 times, most recently from 5b104f4 to cb523e4 Compare September 14, 2020 13:20

MrChico added 26 commits September 16, 2020 16:33

dynamic buffers WIP

7d6db3c

using smt lists instead!

a0ffadb

WIP

c91ad37

more WIP

9053505

wip dynbuffer

2776c03

more wip

120376c

optimize as many static cases as possible

b1b9d43

things are getting better

3a36f12

correcter

029a003

callsemantics are back; more accurate SSTORE accounting; almost all

8d91c14

tests passing

all tests passing, things seem pretty good

d84f4cf

tests passing

6c37844

bump origstorage

0bd6a32

generalize EXP to admit symbolic args

3f8ed9c

clean up of test.hs, refactor EVM.Fetch.oracle

86a771f

fix

d5b070f

dynamic bytes testcase

1ed0233

fix readsWord

d16bc07

assumptions to improve smt performance

561d771

optimize concrete case

3f93f09

simplifications and more testing

c1376dc

update sbv

1149e7e

run only z3 tests for now

b4178a0

allow calldata to be either a buffer or pseudodynamic (old approach)

97ac686

put dynamic buffer test in dapp-test instead of hevm

0884f9c

fix rebase fuckups

f59a912

MrChico added 7 commits September 16, 2020 16:34

don't change which tests are run

90fb4f7

fix concrete RETURNDATA

35e8d51

simplify refunds

c124771

fix SSTORE accounting

b41dd3e

fix memory access accounting in concrete case

174f487

fix calldataload

248e232

turn on z3 dynamic tests

5472d0b

MrChico force-pushed the slistbuffer branch from 1ad0b38 to 5472d0b Compare September 16, 2020 14:34

d-xo approved these changes Sep 16, 2020

View reviewed changes

MrChico added 3 commits October 14, 2020 12:14

sketch of a new structure

39f4524

sketches of spain

6a88b66

wip

42c48a6

mds1 mentioned this pull request Jul 8, 2021

HEVM prove: Data.SBV: Unexpected response from the solver, context: push: #694

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Dynamic buffers via SMT lists #500

Dynamic buffers via SMT lists #500

		constrain $ SL.length calldatalist .< 100
		constrain $ sw256 (sFromIntegral $ SL.length calldatalist) .< sw256 100

Dynamic buffers via SMT lists #500

Are you sure you want to change the base?

Dynamic buffers via SMT lists #500

Conversation

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment