Refactor production of initial terms, factor out method identification

[ehildenb]

This PR is pulled out of: #284.

This brings us closer to producing specifications that are usable for CSE when running individual functions directly. In particular:

• New methods {Method,Constructor}.{is_test,is_testfail} are added for binning Solidity methods by their type.
• The logic for deciding whether to have a more or less symbolic state is inverted. Instead, we start with the most general state (substituting the fewest number of cells), then if it's a test/testFail/setUp, the state is made more specific with it needs to be (behind guards about the type of function it is).
• Modifications are made to the produced initial states to make them compatible for use in CSE:
  • The ORIGIN_ID and CALLER_ID are made to be Int.
  • The OUTPUT_CELL is made to start as the empty buffer.
  • The cells [OUTPUT_CELL, CALLSTACK_CELL, CALLDEPTH_CELL, ID_CELL, LOG_CELL, ACCESSEDACCOUNTS_CELL, ACCESSEDSTORAGE_CELL, INTERIMSTATES_CELL, STATIC_CELL, ACCOUNTS_CELL] are left fully symbolic for normal function calls, only filled in for setUp and test methods.
  • Similar changes are made to the final term production.
• We make sure to add the KEVM invariant to terminal states in the setUp for producing initial states in the test methods.
• Adds pytest-timeout module for timing out individual tests.

[anvacaru]

Left some comments that should be addressed.

[anvacaru]

Approved! You might need to update the expected output again after 6d470cb .