DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Fix z3 oddity: reset vs optimization (#627)

Browse Source 
* Fixes symbolic reentrancy example

* Fix coverage Issue# 527

* Remove  debug unused code

* New solidity biased API and reporting

* Updated examples to new api WIP

* simple_mapping FIXED. new api

* Simple transaction example added. msg.value can be symbolic now

* Reentrancy symbolic now updated to new API + bugfixes

* Doc and cleanups in evm assembler

* EVMInstruction -> Instruction

* cleanups

* typo

* deepcopy in Constant

* Better EVM-asm api and doc

* some docs

* More evm asm docs

* Initial seth in place refactor

* Fix import *

* typo

* newline between text and param

* similar phrasing to all the other flags

* typo

* typo

* fix function name in comment

* sphinx newline

* documentation fixes

* documentation fixes

* refactors

* EVMAssembler to EVMAsm

* Fix evm @hook signature

* EVMAsm

* WIP seth doc

* WIP move seth

* seth moved to manticore module

* Fixed DUP and typo

* Slightly better evm reporting

* review

* review

* Removed unfinished refactor

* Mitigates the wrong objectives print in z3 4.4.x

* Exception to SolveException
This commit is contained in:
feliam 2017-12-15 16:45:30 -03:00 committed by Mark Mossberg
parent aabfecfe77
commit 9839cbdbb0
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
manticore/core/smtlib/solver.py
View File

@ -126,9 +126,14 @@ class Z3Solver(Solver):
self.support_reset = True
logger.debug('Z3 version: %s', self.version)
if self.version >= Version(4, 4, 1):
if self.version >= Version(4, 5, 0):
self.support_maximize = False
self.support_minimize = False
self.support_reset = True
elif self.version >= Version(4, 4, 1):
self.support_maximize = True
self.support_minimize = True
self.support_reset = False
else:
logger.debug(' Please install Z3 4.4.1 or newer to get optimization support')
@ -390,7 +395,7 @@ class Z3Solver(Solver):
with constraints as temp_cs:
X = temp_cs.new_bitvec(x.size)
temp_cs.add(X == x)
aux = temp_cs.new_bitvec(X.size)
aux = temp_cs.new_bitvec(X.size, name='optimized_')
self._reset(temp_cs)
self._send(aux.declaration)
@ -499,7 +504,8 @@ class Z3Solver(Solver):
self._send('(get-value (%s))'%var.name)
ret = self._recv()
assert ret.startswith('((') and ret.endswith('))')
if not ( ret.startswith('((') and ret.endswith('))') ):
raise SolverException('SMTLIB error parsing response: %s' % ret)
if isinstance(expression, Bool):
return {'true':True, 'false':False}[ret[2:-2].split(' ')[1]]