Simplify the pc whenever it is set.

[smoelius]

This pull request simplifies pc using simplify in visitor.py whenever pc is set. This gives a significant speed-up whenever DetectIntegerOverflow is enabled. I think this is because that detector's use of taint cause pc to become symbolic, but in a way that can be simplified.

To demonstrate the speed-up, I performed the following experiment. I introduced DetectIntegerOverflow to eight examples in examples/evm and timed them using both the master and simplify-pc branches. I performed ten runs of each, interleaved to even out load spikes, and summed the timings of the corresponding runs. Results appear below.

To repeat my experiment, perform the following steps.

1. Drop the four scripts in simplify-pc.zip into examples/evm.
2. Run ./patch.sh *.py.
3. Run ./loop.sh.

Here is sample output. Note that toward the end, I added the <== to draw your attention to where there were significant differences. But everything else is untouched.

Switched to branch 'master'
complete.py	2.94
coverage.py	28.90
minimal_bytecode_only.py	5.52
minimal-json.py	9.04
minimal.py	6.92
reentrancy_concrete.py	40.36
simple_mapping.py	8.46
use_def.py	3.61
Switched to branch 'simplify-pc'
complete.py	3.03
coverage.py	28.94
minimal_bytecode_only.py	3.78
minimal-json.py	9.19
minimal.py	5.42
reentrancy_concrete.py	21.41
simple_mapping.py	8.64
use_def.py	3.70
Switched to branch 'master'
complete.py	2.95
coverage.py	29.31
minimal_bytecode_only.py	5.23
minimal-json.py	8.99
minimal.py	6.80
reentrancy_concrete.py	40.22
simple_mapping.py	8.39
use_def.py	3.62
Switched to branch 'simplify-pc'
complete.py	3.05
coverage.py	28.20
minimal_bytecode_only.py	3.83
minimal-json.py	8.87
minimal.py	5.31
reentrancy_concrete.py	21.88
simple_mapping.py	8.40
use_def.py	3.51
Switched to branch 'master'
complete.py	2.89
coverage.py	27.84
minimal_bytecode_only.py	5.06
minimal-json.py	9.56
minimal.py	7.13
reentrancy_concrete.py	39.58
simple_mapping.py	8.74
use_def.py	3.66
Switched to branch 'simplify-pc'
complete.py	2.91
coverage.py	29.12
minimal_bytecode_only.py	3.61
minimal-json.py	9.06
minimal.py	5.07
reentrancy_concrete.py	22.35
simple_mapping.py	8.54
use_def.py	3.66
Switched to branch 'master'
complete.py	3.07
coverage.py	29.23
minimal_bytecode_only.py	4.95
minimal-json.py	9.17
minimal.py	7.27
reentrancy_concrete.py	39.38
simple_mapping.py	8.70
use_def.py	3.44
Switched to branch 'simplify-pc'
complete.py	2.83
coverage.py	29.76
minimal_bytecode_only.py	3.91
minimal-json.py	8.94
minimal.py	5.39
reentrancy_concrete.py	21.88
simple_mapping.py	8.63
use_def.py	3.73
Switched to branch 'master'
complete.py	3.10
coverage.py	28.68
minimal_bytecode_only.py	4.91
minimal-json.py	8.83
minimal.py	7.11
reentrancy_concrete.py	40.42
simple_mapping.py	8.84
use_def.py	3.67
Switched to branch 'simplify-pc'
complete.py	2.95
coverage.py	28.50
minimal_bytecode_only.py	3.77
minimal-json.py	9.17
minimal.py	5.30
reentrancy_concrete.py	21.78
simple_mapping.py	8.13
use_def.py	3.61
Switched to branch 'master'
complete.py	2.96
coverage.py	30.77
minimal_bytecode_only.py	4.99
minimal-json.py	9.46
minimal.py	7.27
reentrancy_concrete.py	39.46
simple_mapping.py	8.04
use_def.py	3.45
Switched to branch 'simplify-pc'
complete.py	3.26
coverage.py	29.08
minimal_bytecode_only.py	3.64
minimal-json.py	8.88
minimal.py	5.25
reentrancy_concrete.py	21.44
simple_mapping.py	8.61
use_def.py	3.85
Switched to branch 'master'
complete.py	3.08
coverage.py	29.19
minimal_bytecode_only.py	4.92
minimal-json.py	8.88
minimal.py	6.84
reentrancy_concrete.py	39.61
simple_mapping.py	8.33
use_def.py	3.66
Switched to branch 'simplify-pc'
complete.py	3.05
coverage.py	28.98
minimal_bytecode_only.py	3.71
minimal-json.py	9.17
minimal.py	5.02
reentrancy_concrete.py	21.66
simple_mapping.py	8.63
use_def.py	3.60
Switched to branch 'master'
complete.py	2.91
coverage.py	29.14
minimal_bytecode_only.py	4.88
minimal-json.py	9.05
minimal.py	6.90
reentrancy_concrete.py	40.33
simple_mapping.py	8.68
use_def.py	3.49
Switched to branch 'simplify-pc'
complete.py	3.01
coverage.py	28.80
minimal_bytecode_only.py	3.76
minimal-json.py	9.22
minimal.py	5.21
reentrancy_concrete.py	21.42
simple_mapping.py	8.37
use_def.py	3.70
Switched to branch 'master'
complete.py	2.98
coverage.py	28.10
minimal_bytecode_only.py	5.00
minimal-json.py	9.18
minimal.py	6.88
reentrancy_concrete.py	39.61
simple_mapping.py	8.27
use_def.py	3.94
Switched to branch 'simplify-pc'
complete.py	2.98
coverage.py	28.01
minimal_bytecode_only.py	3.76
minimal-json.py	9.27
minimal.py	5.21
reentrancy_concrete.py	22.00
simple_mapping.py	8.69
use_def.py	3.92
Switched to branch 'master'
complete.py	3.02
coverage.py	27.63
minimal_bytecode_only.py	4.99
minimal-json.py	9.24
minimal.py	6.97
reentrancy_concrete.py	40.30
simple_mapping.py	8.42
use_def.py	3.58
Switched to branch 'simplify-pc'
complete.py	2.89
coverage.py	28.92
minimal_bytecode_only.py	3.57
minimal-json.py	9.17
minimal.py	5.50
reentrancy_concrete.py	21.37
simple_mapping.py	8.40
use_def.py	3.71

summary
29.90	29.96
288.79	288.31
50.45	37.34	<== minimal_bytecode_only.py
91.40	90.94
70.09	52.68	<== minimal.py
399.27	217.19	<== reentrancy_concrete.py
84.87	85.04
36.12	36.99

As you can see from the above, when DetectIntegerOverflow is enabled, simplify-pc significantly speeds up minimal_bytecode_only.py, minimal.py, and reentrancy_concrete.py, and has a negligible effect elsewhere.

[disconnect3d]

Can we move this to another PR and [possibly] add a unit test for that?

EDIT: Or if it is needed in here somehow then it should be in a different git commit at least ;F.

[smoelius]

It is needed for this PR in that, in some of my tests, the symbolic pc features an unsigned division.

I will move this into a separate commit and add a unit test as you suggested.

[ehennenfent]

#1526 has a different implementation of this:
https://github.com/trailofbits/manticore/pull/1526/files#diff-925668d298ca105732187a108baacbc7R294

@feliam Any thoughts?

[smoelius]

The implementation in #1526 looks Ethereum specific. But manticore/core/smtlib/visitors.py is not Ethereum specific, is it?

[disconnect3d]

This is weird as this PR does not include any additional uses of self.pc or self._pc.

We initialise self.pc in here:
https://github.com/trailofbits/manticore/blob/master/manticore/platforms/evm.py#L722-L723

And before this PR the only use of self._pc in this file is in:

• https://github.com/trailofbits/manticore/blob/master/manticore/platforms/evm.py#L1125

Either I am missing something or the latter is probably a bug and maybe should be a self.pc = ..., and the self.pc = 0 should be changed to self._pc = 0?

Also: are we sure this does not break anything? It passes the tests but do we have tests for everything, like tainting?

@feliam you might have some comment here too

[smoelius]

this PR does not include any additional uses of self.pc or self._pc.

Right. It is meant to influence the existing writes to self.pc.

...the latter is probably a bug...

I looked at this and thought it should be okay following this PR. But I agree with your sentiment that it should be self.pc = .... I will change it.

...the self.pc = 0 should be changed to self._pc = 0?

You're right. I'll make that change as well.

[feliam]

manticore/manticore/platforms/evm.py

Line 1126 in 19ba4b6

self._pc = last_pc

is probably a bug without this PR

[ehennenfent]

Agree that it's a bug as ._pc doesn't appear anywhere else in our code. This PR seems to be internally consistent and passes the tests, so I think we can give this change the green light.

[feliam]

Idk about the expressions being mutable. Maybe we can just do it for taint? But there are caches and other stuff that expects the expressions to be unmutable. This may be happening in other places anyway.

[smoelius]

Idk about the expressions being mutable.

I see your point. I will revise.

[smoelius]

I think I have addressed all of the comments. I was afraid that the most recent commit might negate the benefits, but new timing numbers suggest it's still a win:

summary
30.07	30.20
286.05	285.46
51.07	36.67	<== minimal_bytecode_only.py
91.51	91.25
69.27	54.44	<== minimal.py
394.87	211.79	<== reentrancy_concrete.py
83.32	84.10
36.97	36.88

I will be happy to address any additional concerns.

[ehennenfent]

Agree that it's a bug as ._pc doesn't appear anywhere else in our code. This PR seems to be internally consistent and passes the tests, so I think we can give this change the green light.

[ehennenfent]

Why not result = expressions.taint_with(result, expression.operands[0].taint) ? Looks to be almost exactly the same code.

[smoelius]

I considered that, but:

1. I wasn't sure what exactly is going on in that function, e.g., this:
   

   manticore/manticore/core/smtlib/expression.py

   Lines 95 to 96 in 19ba4b6

   	if isinstance(arg, BitVecVariable):
   	arg = arg + BitVecConstant(value_bits, 0, taint=tainted_fset)

2. taint_with makes a copy of the expression every time.

I am open to changing, though.

[ehennenfent]

During the dev meeting this morning, @feliam raised some good points:

• The reason we didn't explicitly simplify the PC in the past was that simplification didn't effectively propagate the taint.
• We don't have any tests that check whether taint propagation on the PC is effective.

However, I'm uncertain of this second point, based on this PR. @smoelius I'm guessing the reason you modified the BitVecITE visitor is that some test fails without that modification due to improperly propagated taints. Is that correct?

[smoelius]

No, not because a test fails.

Without the BitVecITE modification, Manticore will repeatedly throw Concretize exceptions from this point:

manticore/manticore/platforms/evm.py

Lines 1208 to 1210 in 612d40b

	raise Concretize(
	"Concretize PC", expression=expression, setstate=setstate, policy="ALL"
	)

My previous two pull requests were meant, in part, to help to expose this.

If you would like me to add some tests related to this issue, let me know. I would be happy to do so.