In evm.v the function a_instr_sem misses the opcode EXTCODECOPY.

The analyzer does not remember what events are logged.

Especially for analyzing bamboo runtime code, it's crucial. Bamboo runtime first jumps into a program position indicated by the storage.

In evm.v, the function a_instr_sem misses these opcodes.

Currently the analyzer gives an error when the input does not start with "0x".

There is an optimized addition on abstract values Aadd' but it does not exist for

• multiplications
• signed division

According to #31. This is useful for choosing paths #28 .

geth has a method traceTransaction that prints a log of EVM execution. The log contains stack elements, but it is not immediate to know the origin of the numbers in the stack.

This issue keeps track of creating a command-line tool that enriches the log with more information.

Input has:

stack: ["00000000000000000000000000000000000000000000000000000000d67cbec9"],

The output should contain:

stack: [{val: "00000000000000000000000000000000000000000000000000000000d67cbec9",
            symbol: "blocknumber"
           }],

It should be possible to lookup the code and turn it into a byte sequence and then into a word.

A division instruction should produce two behaviors, one for divide by zero and the other for divide by non-zero. (When the divisor is known to be non-zero, only one behavior is fine.)

Instructions involving division return zero when the divisor is zero. This should be taken into account for *DIV and *MOD instructions.

For #28, it is necessary to classify abstract expressions according to if they are controllable by the caller.

This issue keeps track of creating a classification.

The opcode DELEGATECALL is missing from the evm.v.

when I make ,errors blow.Can you help me?

Error: The implementation CoqNat.ml does not match the interface CoqNat.cmi:
Values do not match:
val zero : int
is not included in
val zero : Decimal.int
File "CoqNat.mli", line 6, characters 0-14: Expected declaration
File "CoqNat.ml", line 8, characters 4-8: Actual declaration
Command exited with code 2.
Compilation unsuccessful after building 38 targets (0 cached) in 00:00:01.

make command as per the instruction in README failed with coqc compile error.

$ make
coqc evm.v
File "/home/dcsandr/software/dry-analyzer/evm.v", line 1263, characters 21-28:
Error: The reference Nat.ltb was not found in the current environment.
Makefile:15: recipe for target 'evm.vo' failed
make: *** [evm.vo] Error 1

Following is my version of coqc:

$ coqc --version
The Coq Proof Assistant, version 8.4pl4 (November 2015)
compiled on Nov 04 2015 12:56:53 with OCaml 4.02.3

I'm using Ubuntu 16.04.

The yellow paper now says the run-time stack has the limit of 1024 items. The stack has a maximum size of 1024. The analyzer should be made aware of this, and when the stack size exceeds the limit, the resulting state should be failure.

This issue keeps track of testing the analyzer against the blockchain data from the testnet or the mainnet.

This is maybe easier after #11.

Currently the analyzer stops at a CALL instruction. This issue keeps track of fixing this. After the call there would be three cases

1. the callee returns
2. the callee fails
3. the callee somehow calls back the original contract

exit criteria
Cases 1. and 2. should be implemented. A message should be shown for case 3. Also a github issue should be created for dealing with reentrancy in the analyzer.

(take (0x7ca) bytes at (0xc0) from
(codecopy mem: (0xc0), code: (0x23c), size: (0x7ca), on
(mem_write32 addr: (0x40) val: (0x88a) in ...

should be just

(take (0x7ca) bytes at (0xc0) from
(codecopy mem: (0xc0), code: (0x23c), size: (0x7ca), on (empty))

• design a url scheme for specifying a specific execution path (a sequence of booleans?)
• encode and decode such url scheme
• use the decode scheme to narrow down the execution path
• use the encode scheme to show links for "investigate this path."

Currently the analyzer tries to follow every possible execution path. There can be an option to filter out the execution paths that require a particular caller, or preimage of a hash function.

Thanks @kumavis for the idea.

The condition "(0x60) is not zero" should be simplified into "True".

After clicking the "Analyze" button on the web interface, I've got the following report. How do I read it? Thanks in advance.

Behaviors

2 behaviors cover the possibilities (assuming enough gas).

back fwd
Behavior 0

under conditions:

    (value of this call) is not zero.

hits an unimplemented instruction UNKNOWN fd in this analyzer.
Behavior 1

under conditions:

    (value of this call) is zero.

returns with output
(take (0x1bd6) bytes at (0x0) from
(codecopy mem: (0x0), code: (0xd4), size: (0x1bd6), on
(mem_write32 addr: (0x20) val: (0x1) in
(mem_write32 addr: (0x0) val: ((0xffffffffffffffffffffffffffffffffffffffff) and ((0xffffffffffffffffffffffffffffffffffffffff) and (address of caller))) in
(mem_write32 addr: (0x40) val: (0x60) in
(empty)
)
)
)
)
)
and state {
last instruction: PUSH_N0x00
stack: [(0x0), (0x1bd6)](size 2)
memory:
(codecopy mem: (0x0), code: (0xd4), size: (0x1bd6), on
(mem_write32 addr: (0x20) val: (0x1) in
(mem_write32 addr: (0x0) val: ((0xffffffffffffffffffffffffffffffffffffffff) and ((0xffffffffffffffffffffffffffffffffffffffff) and (address of caller))) in
(mem_write32 addr: (0x40) val: (0x60) in
(empty)
)
)
)
)

storage:
(storage_write at: (sha3 (concat ((0xffffffffffffffffffffffffffffffffffffffff) and ((0xffffffffffffffffffffffffffffffffffffffff) and (address of caller))) (0x1))), val: ((0x1dcd6500) * ((0xa) ** ((0xff) and (0x12))))
(storage_write at: (0x0), val: ((0x1dcd6500) * ((0xa) ** ((0xff) and (0x12))))
(storage_write at: (0x3), val: ((((0xffffffffffffffffffffffffffffffffffffffff) and (address of caller)) * (0x1)) or ((not ((0xffffffffffffffffffffffffffffffffffffffff) * (0x1))) and (((0x0) * (0x10000000000000000000000000000000000000000)) or ((not ((0xff) * (0x10000000000000000000000000000000000000000))) and (get_storage (0x3) (initial storage))))))
(storage_write at: (0x3), val: (((0x0) * (0x10000000000000000000000000000000000000000)) or ((not ((0xff) * (0x10000000000000000000000000000000000000000))) and (get_storage (0x3) (initial storage))))
(initial storage)
)
)
)
)

log: XXX
remaining_program: XXX
}. 

In evm.v, opcode CREATE is missing from a_instr_sem function`.

(take (0x40) bytes at (0x0) from (mem_write32 addr: (0x20) val: (0x0) in (mem_write32 addr: (0x0) val: (get32 (0x4) (input data)) in (empty)))

can be reduced into

(concat (get32 (0x4) (input data)) (0x0))

For example, http://dry.yoichihirai.com/?nsteps=150&contract=0x7f0000000000000000000000000000000000000000000000000000000000000000807f0000000000000000000000000000000000000000000000000000000000000040805180920190528180380382397f00000000000000000000000000000000000000000000000000000000000000025b82157f0000000000000000000000000000000000000000000000000000000000000126578181557f000000000000000000000000000000000000000000000000000000000000002090929003917f000000000000000000000000000000000000000000000000000000000000002001907f0000000000000000000000000000000000000000000000000000000000000020017f0000000000000000000000000000000000000000000000000000000000000071565b5050507f00000000000000000000000000000000000000000000000000000000000000237f0000000000000000000000000000000000000000000000000000000000000000557f0000000000000000000000000000000000000000000000000000000000000051807f000000000000000000000000000000000000000000000000000000000000004080518092019052817f00000000000000000000000000000000000000000000000000000000000001dc8239f37f000000000000000000000000000000000000000000000000000000000000000054565b7f00000000000000000000000000000000000000000000000000000000000000003560e060020a900450600256

into 0x2.

The expression "(get32 (0x40) (empty))" should be simplified to zero.

In evm.v, the function a_instr_sem misses the clauses for the opcodes in the title.

In evm.v, a_instr_sem misses clauses for these opcodes. These can be implemented in the same way as SWAP1 to SWAP10 that have already been implemented.

Would love to also help out here. Do you have a specific look/feel you're going for? Also, mention: @aupiff.

Currently, the results for long programs tend to be unreadable. Before improving this, we can already dissect the program into basic blocks and analyze each basic block separately.