Skip to content

Commit 2605e46

Browse files
feliamfeliam
committed
merge
1 parent 2fa2561 commit 2605e46

File tree

12 files changed

+93
-149
lines changed

12 files changed

+93
-149
lines changed

‎manticore/core/manticore.py‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,6 @@
5959
description="The seed to use when randomly selecting states",
6060
)
6161

62-
6362
class ManticoreBase(Eventful):
6463
_published_events = {"solve"}
6564

‎manticore/core/state.py‎

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
import copy
22
import logging
3+
from typing import Optional
34

4-
from .smtlib import solver, Bool, issymbolic, BitVecConstant, MutableArray
5+
from .smtlib import Bool, issymbolic, BitVecConstant, MutableArray
56
from ..utils.event import Eventful
67
from ..utils.helpers import PickleSerializer
78
from ..utils import config
@@ -174,30 +175,30 @@ class StateBase(Eventful):
174175

175176
_published_events = {"execution_intermittent"}
176177

177-
def __init__(self, constraints, platform, **kwargs):
178+
def __init__(self, *, constraints: "Constraints", platform: "Platform", manticore: Optional["ManticoreBase"] = None, **kwargs):
178179
super().__init__(**kwargs)
180+
self._manticore = manticore
179181
self._platform = platform
180182
self._constraints = constraints
181-
self._platform.constraints = constraints
182-
self._input_symbols = list()
183183
self._child = None
184184
self._context = dict()
185+
185186
self._terminated_by = None
186187
self._solver = EventSolver()
187188
self._total_exec = 0
188189
self._own_exec = 0
189190
# 33
190191
# Events are lost in serialization and fork !!
191192
self.forward_events_from(self._solver)
192-
self.forward_events_from(platform)
193+
platform.set_state(self)
193194

194195
def __getstate__(self):
195196
state = super().__getstate__()
196197
state["platform"] = self._platform
197198
state["constraints"] = self._constraints
198-
state["input_symbols"] = self._input_symbols
199199
state["child"] = self._child
200200
state["context"] = self._context
201+
201202
state["terminated_by"] = self._terminated_by
202203
state["exec_counter"] = self._total_exec
203204
return state
@@ -206,17 +207,18 @@ def __setstate__(self, state):
206207
super().__setstate__(state)
207208
self._platform = state["platform"]
208209
self._constraints = state["constraints"]
209-
self._input_symbols = state["input_symbols"]
210210
self._child = state["child"]
211211
self._context = state["context"]
212+
self._manticore = None
213+
212214
self._terminated_by = state["terminated_by"]
213215
self._total_exec = state["exec_counter"]
214216
self._own_exec = 0
215217
self._solver = EventSolver()
216218
# 33
217219
# Events are lost in serialization and fork !!
218220
self.forward_events_from(self._solver)
219-
self.forward_events_from(self._platform)
221+
self.platform.set_state(self)
220222

221223
@property
222224
def id(self):
@@ -229,15 +231,16 @@ def __repr__(self):
229231
# This need to change. this is the center of ALL the problems. re. CoW
230232
def __enter__(self):
231233
assert self._child is None
232-
self._platform.constraints = None
233-
new_state = self.__class__(self._constraints.__enter__(), self._platform)
234-
self.platform.constraints = new_state.constraints
235-
new_state._input_symbols = list(self._input_symbols)
234+
self._platform._constraints = None
235+
new_state = self.__class__(constraints=self._constraints.__enter__(), platform=self._platform, manticore=self._manticore)
236+
#Keep the same constraint
237+
self.platform._constraints = new_state.constraints
238+
#backup copy of the context
236239
new_state._context = copy.copy(self._context)
237240
new_state._id = None
241+
238242
new_state._total_exec = self._total_exec
239243
self.copy_eventful_state(new_state)
240-
241244
self._child = new_state
242245
assert new_state.platform.constraints is new_state.constraints
243246

@@ -246,7 +249,6 @@ def __enter__(self):
246249
def __exit__(self, ty, value, traceback):
247250
self._constraints.__exit__(ty, value, traceback)
248251
self._child = None
249-
self.platform.constraints = self.constraints
250252

251253
@property
252254
def input_symbols(self):
@@ -267,7 +269,6 @@ def constraints(self):
267269
@constraints.setter
268270
def constraints(self, constraints):
269271
self._constraints = constraints
270-
self.platform.constraints = constraints
271272

272273
def _update_state_descriptor(self, descriptor: StateDescriptor, *args, **kwargs):
273274
"""

‎manticore/core/workspace.py‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -602,10 +602,17 @@ def save_testcase(self, state: StateBase, testcase: Testcase, message: str = "")
602602
# The workspaces should override `save_testcase` method
603603
#
604604
# Below is native-only
605+
def save_input_symbols(testcase, state: StateBase):
606+
with testcase.open_stream("input") as f:
607+
for symbol in state.input_symbols:
608+
# TODO - constrain=False here, so the extra migration shouldn't cause problems, right?
609+
buf = state.solve_one(symbol)
610+
f.write(f"{symbol.name}: {buf!r}\n")
611+
605612
self.save_summary(testcase, state, message)
606613
self.save_trace(testcase, state)
607614
self.save_constraints(testcase, state)
608-
self.save_input_symbols(testcase, state)
615+
save_input_symbols(testcase, state)
609616

610617
for stream_name, data in state.platform.generate_workspace_files().items():
611618
with testcase.open_stream(stream_name, binary=True) as stream:
@@ -655,10 +662,3 @@ def save_constraints(testcase, state: StateBase):
655662
with testcase.open_stream("smt") as f:
656663
f.write(str(state.constraints))
657664

658-
@staticmethod
659-
def save_input_symbols(testcase, state: StateBase):
660-
with testcase.open_stream("input") as f:
661-
for symbol in state.input_symbols:
662-
# TODO - constrain=False here, so the extra migration shouldn't cause problems, right?
663-
buf = state.solve_one(symbol)
664-
f.write(f"{symbol.name}: {buf!r}\n")

‎manticore/ethereum/manticore.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -390,7 +390,7 @@ def __init__(self, plugins=None, **kwargs):
390390
constraints = ConstraintSet()
391391
# make the ethereum world state
392392
world = evm.EVMWorld(constraints)
393-
initial_state = State(constraints, world)
393+
initial_state = State(constraints=constraints, platform=world, maticore=self)
394394
super().__init__(initial_state, **kwargs)
395395
if plugins is not None:
396396
for p in plugins:

‎manticore/ethereum/parsetab.py‎

Lines changed: 34 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -1,111 +1,50 @@
1+
12
# parsetab.py
23
# This file is automatically generated. Do not edit.
34
# pylint: disable=W,C,R
4-
_tabversion = "3.10"
5-
6-
_lr_method = "LALR"
5+
_tabversion = '3.10'
76

8-
_lr_signature = "ADDRESS BOOL BYTES BYTESM COMMA FIXED FIXEDMN FUNCTION INT INTN LBRAKET LPAREN NUMBER RBRAKET RPAREN STRING UFIXED UFIXEDMN UINT UINTN\n T : UINTN\n T : UINT\n T : INTN\n T : INT\n T : ADDRESS\n T : BOOL\n T : FIXEDMN\n T : UFIXEDMN\n T : FIXED\n T : UFIXED\n T : BYTESM\n T : FUNCTION\n T : BYTES\n T : STRING\n\n \n TL : T\n \n TL : T COMMA TL\n \n T : LPAREN TL RPAREN\n \n T : LPAREN RPAREN\n \n T : T LBRAKET RBRAKET\n \n T : T LBRAKET NUMBER RBRAKET\n "
7+
_lr_method = 'LALR'
98

10-
_lr_action_items = {
11-
"UINTN": ([0, 16, 24,], [2, 2, 2,]),
12-
"UINT": ([0, 16, 24,], [3, 3, 3,]),
13-
"INTN": ([0, 16, 24,], [4, 4, 4,]),
14-
"INT": ([0, 16, 24,], [5, 5, 5,]),
15-
"ADDRESS": ([0, 16, 24,], [6, 6, 6,]),
16-
"BOOL": ([0, 16, 24,], [7, 7, 7,]),
17-
"FIXEDMN": ([0, 16, 24,], [8, 8, 8,]),
18-
"UFIXEDMN": ([0, 16, 24,], [9, 9, 9,]),
19-
"FIXED": ([0, 16, 24,], [10, 10, 10,]),
20-
"UFIXED": ([0, 16, 24,], [11, 11, 11,]),
21-
"BYTESM": ([0, 16, 24,], [12, 12, 12,]),
22-
"FUNCTION": ([0, 16, 24,], [13, 13, 13,]),
23-
"BYTES": ([0, 16, 24,], [14, 14, 14,]),
24-
"STRING": ([0, 16, 24,], [15, 15, 15,]),
25-
"LPAREN": ([0, 16, 24,], [16, 16, 16,]),
26-
"$end": (
27-
[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 19, 21, 23, 25,],
28-
[0, -1, -2, -3, -4, -5, -6, -7, -8, -9, -10, -11, -12, -13, -14, -18, -19, -17, -20,],
29-
),
30-
"LBRAKET": (
31-
[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 19, 20, 21, 23, 25,],
32-
[17, -1, -2, -3, -4, -5, -6, -7, -8, -9, -10, -11, -12, -13, -14, -18, 17, -19, -17, -20,],
33-
),
34-
"COMMA": (
35-
[2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 19, 20, 21, 23, 25,],
36-
[-1, -2, -3, -4, -5, -6, -7, -8, -9, -10, -11, -12, -13, -14, -18, 24, -19, -17, -20,],
37-
),
38-
"RPAREN": (
39-
[2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 18, 19, 20, 21, 23, 25, 26,],
40-
[
41-
-1,
42-
-2,
43-
-3,
44-
-4,
45-
-5,
46-
-6,
47-
-7,
48-
-8,
49-
-9,
50-
-10,
51-
-11,
52-
-12,
53-
-13,
54-
-14,
55-
19,
56-
23,
57-
-18,
58-
-15,
59-
-19,
60-
-17,
61-
-20,
62-
-16,
63-
],
64-
),
65-
"RBRAKET": ([17, 22,], [21, 25,]),
66-
"NUMBER": ([17,], [22,]),
67-
}
9+
_lr_signature = 'ADDRESS BOOL BYTES BYTESM COMMA FIXED FIXEDMN FUNCTION INT INTN LBRAKET LPAREN NUMBER RBRAKET RPAREN STRING UFIXED UFIXEDMN UINT UINTN\n T : UINTN\n T : UINT\n T : INTN\n T : INT\n T : ADDRESS\n T : BOOL\n T : FIXEDMN\n T : UFIXEDMN\n T : FIXED\n T : UFIXED\n T : BYTESM\n T : FUNCTION\n T : BYTES\n T : STRING\n\n \n TL : T\n \n TL : T COMMA TL\n \n T : LPAREN TL RPAREN\n \n T : LPAREN RPAREN\n \n T : T LBRAKET RBRAKET\n \n T : T LBRAKET NUMBER RBRAKET\n '
10+
11+
_lr_action_items = {'UINTN':([0,16,24,],[2,2,2,]),'UINT':([0,16,24,],[3,3,3,]),'INTN':([0,16,24,],[4,4,4,]),'INT':([0,16,24,],[5,5,5,]),'ADDRESS':([0,16,24,],[6,6,6,]),'BOOL':([0,16,24,],[7,7,7,]),'FIXEDMN':([0,16,24,],[8,8,8,]),'UFIXEDMN':([0,16,24,],[9,9,9,]),'FIXED':([0,16,24,],[10,10,10,]),'UFIXED':([0,16,24,],[11,11,11,]),'BYTESM':([0,16,24,],[12,12,12,]),'FUNCTION':([0,16,24,],[13,13,13,]),'BYTES':([0,16,24,],[14,14,14,]),'STRING':([0,16,24,],[15,15,15,]),'LPAREN':([0,16,24,],[16,16,16,]),'$end':([1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,19,21,23,25,],[0,-1,-2,-3,-4,-5,-6,-7,-8,-9,-10,-11,-12,-13,-14,-18,-19,-17,-20,]),'LBRAKET':([1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,19,20,21,23,25,],[17,-1,-2,-3,-4,-5,-6,-7,-8,-9,-10,-11,-12,-13,-14,-18,17,-19,-17,-20,]),'COMMA':([2,3,4,5,6,7,8,9,10,11,12,13,14,15,19,20,21,23,25,],[-1,-2,-3,-4,-5,-6,-7,-8,-9,-10,-11,-12,-13,-14,-18,24,-19,-17,-20,]),'RPAREN':([2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,18,19,20,21,23,25,26,],[-1,-2,-3,-4,-5,-6,-7,-8,-9,-10,-11,-12,-13,-14,19,23,-18,-15,-19,-17,-20,-16,]),'RBRAKET':([17,22,],[21,25,]),'NUMBER':([17,],[22,]),}
6812

6913
_lr_action = {}
7014
for _k, _v in _lr_action_items.items():
71-
for _x, _y in zip(_v[0], _v[1]):
72-
if not _x in _lr_action:
73-
_lr_action[_x] = {}
74-
_lr_action[_x][_k] = _y
15+
for _x,_y in zip(_v[0],_v[1]):
16+
if not _x in _lr_action: _lr_action[_x] = {}
17+
_lr_action[_x][_k] = _y
7518
del _lr_action_items
7619

77-
_lr_goto_items = {
78-
"T": ([0, 16, 24,], [1, 20, 20,]),
79-
"TL": ([16, 24,], [18, 26,]),
80-
}
20+
_lr_goto_items = {'T':([0,16,24,],[1,20,20,]),'TL':([16,24,],[18,26,]),}
8121

8222
_lr_goto = {}
8323
for _k, _v in _lr_goto_items.items():
84-
for _x, _y in zip(_v[0], _v[1]):
85-
if not _x in _lr_goto:
86-
_lr_goto[_x] = {}
87-
_lr_goto[_x][_k] = _y
24+
for _x, _y in zip(_v[0], _v[1]):
25+
if not _x in _lr_goto: _lr_goto[_x] = {}
26+
_lr_goto[_x][_k] = _y
8827
del _lr_goto_items
8928
_lr_productions = [
90-
("S' -> T", "S'", 1, None, None, None),
91-
("T -> UINTN", "T", 1, "p_basic_type", "abitypes.py", 154),
92-
("T -> UINT", "T", 1, "p_basic_type", "abitypes.py", 155),
93-
("T -> INTN", "T", 1, "p_basic_type", "abitypes.py", 156),
94-
("T -> INT", "T", 1, "p_basic_type", "abitypes.py", 157),
95-
("T -> ADDRESS", "T", 1, "p_basic_type", "abitypes.py", 158),
96-
("T -> BOOL", "T", 1, "p_basic_type", "abitypes.py", 159),
97-
("T -> FIXEDMN", "T", 1, "p_basic_type", "abitypes.py", 160),
98-
("T -> UFIXEDMN", "T", 1, "p_basic_type", "abitypes.py", 161),
99-
("T -> FIXED", "T", 1, "p_basic_type", "abitypes.py", 162),
100-
("T -> UFIXED", "T", 1, "p_basic_type", "abitypes.py", 163),
101-
("T -> BYTESM", "T", 1, "p_basic_type", "abitypes.py", 164),
102-
("T -> FUNCTION", "T", 1, "p_basic_type", "abitypes.py", 165),
103-
("T -> BYTES", "T", 1, "p_basic_type", "abitypes.py", 166),
104-
("T -> STRING", "T", 1, "p_basic_type", "abitypes.py", 167),
105-
("TL -> T", "TL", 1, "p_type_list_one", "abitypes.py", 175),
106-
("TL -> T COMMA TL", "TL", 3, "p_type_list", "abitypes.py", 182),
107-
("T -> LPAREN TL RPAREN", "T", 3, "p_tuple", "abitypes.py", 189),
108-
("T -> LPAREN RPAREN", "T", 2, "p_tuple_empty", "abitypes.py", 196),
109-
("T -> T LBRAKET RBRAKET", "T", 3, "p_dynamic_type", "abitypes.py", 203),
110-
("T -> T LBRAKET NUMBER RBRAKET", "T", 4, "p_dynamic_fixed_type", "abitypes.py", 212),
29+
("S' -> T","S'",1,None,None,None),
30+
('T -> UINTN','T',1,'p_basic_type','abitypes.py',154),
31+
('T -> UINT','T',1,'p_basic_type','abitypes.py',155),
32+
('T -> INTN','T',1,'p_basic_type','abitypes.py',156),
33+
('T -> INT','T',1,'p_basic_type','abitypes.py',157),
34+
('T -> ADDRESS','T',1,'p_basic_type','abitypes.py',158),
35+
('T -> BOOL','T',1,'p_basic_type','abitypes.py',159),
36+
('T -> FIXEDMN','T',1,'p_basic_type','abitypes.py',160),
37+
('T -> UFIXEDMN','T',1,'p_basic_type','abitypes.py',161),
38+
('T -> FIXED','T',1,'p_basic_type','abitypes.py',162),
39+
('T -> UFIXED','T',1,'p_basic_type','abitypes.py',163),
40+
('T -> BYTESM','T',1,'p_basic_type','abitypes.py',164),
41+
('T -> FUNCTION','T',1,'p_basic_type','abitypes.py',165),
42+
('T -> BYTES','T',1,'p_basic_type','abitypes.py',166),
43+
('T -> STRING','T',1,'p_basic_type','abitypes.py',167),
44+
('TL -> T','TL',1,'p_type_list_one','abitypes.py',175),
45+
('TL -> T COMMA TL','TL',3,'p_type_list','abitypes.py',182),
46+
('T -> LPAREN TL RPAREN','T',3,'p_tuple','abitypes.py',189),
47+
('T -> LPAREN RPAREN','T',2,'p_tuple_empty','abitypes.py',196),
48+
('T -> T LBRAKET RBRAKET','T',3,'p_dynamic_type','abitypes.py',203),
49+
('T -> T LBRAKET NUMBER RBRAKET','T',4,'p_dynamic_fixed_type','abitypes.py',212),
11150
]

‎manticore/native/manticore.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -422,7 +422,7 @@ def _make_linux(
422422
# TODO: use argv as arguments for function
423423
platform.set_entry(entry_pc)
424424

425-
initial_state = State(constraints, platform)
425+
initial_state = State(constraints=constraints, platform=platform)
426426

427427
if concrete_start != "":
428428
logger.info("Starting with concrete input: %s", concrete_start)

‎manticore/native/state.py‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,17 +20,20 @@ class CheckpointData(NamedTuple):
2020
class State(StateBase):
2121
def __init__(self, *args, **kwargs):
2222
super().__init__(*args, **kwargs)
23+
self._input_symbols = list()
2324
self._hooks: Dict[Optional[int], Set[HookCallback]] = {}
2425
self._after_hooks: Dict[Optional[int], Set[HookCallback]] = {}
2526

2627
def __getstate__(self) -> Dict[str, Any]:
2728
state = super().__getstate__()
29+
state["input_symbols"] = self._input_symbols
2830
state["hooks"] = self._hooks
2931
state["after_hooks"] = self._after_hooks
3032
return state
3133

3234
def __setstate__(self, state: Dict[str, Any]) -> None:
3335
super().__setstate__(state)
36+
self._input_symbols = state["input_symbols"]
3437
self._hooks = state["hooks"]
3538
self._after_hooks = state["after_hooks"]
3639
self._resub_hooks()

‎manticore/platforms/decree.py‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
from ..core.smtlib import *
88
from ..core.state import TerminateState
99
from ..binary import CGCElf
10-
from ..platforms.platform import Platform
10+
from ..platforms.platform import NativePlatform
1111
import logging
1212
import random
1313

@@ -76,7 +76,7 @@ def _transmit(self, buf):
7676
return len(buf)
7777

7878

79-
class Decree(Platform):
79+
class Decree(NativePlatform):
8080
"""
8181
A simple Decree Operating System.
8282
This class emulates the most common Decree system calls

0 commit comments

Comments
 (0)