From 6896c227ef1d015ae15b67755efd3942d1c6853c Mon Sep 17 00:00:00 2001 From: Yan Ivnitskiy Date: Thu, 21 Dec 2017 17:02:44 -0500 Subject: [PATCH] Initial implementation of concolic algorithm (#653) * WIP New Policy class * WIP pubsub * Update Signal tests * small fixes from github comments * Fix event decode_instruction signature * Good merge * Good good merge * WIP manticore refactor * Fix default old-style initial state * add -> enqueue * @m.init * Fix workspace url * Some test skipped * Ad Fixme to platform specific stuff in State * add -> enqueue * Enqueue created state * Fix m.init Use a messy hack to adhere to the spec (callback func receive 1 state argument) * Add _coverage_file ivar to Manticore * Fix symbolic files * remove extra enqueue * Fixing __main__ * comments * Experimental plugin system * tests fixed * Fix plugins * Some reporting moved to plugin * Fix assertions test * Add published events to classes that publish them * Update how we verify callbacks * Update Eventful._publish * Yet another flavor for event name checking * really it's a bunch of minimal bugfixes * Remove get_all_event_names from Plugin * Update where we get all events * Use new metaclass-based event registry * Initial concrete trace follower * Add extended (json) trace support * More stubs for condition gather * Update trace saving to new format * Produce trace regardless of contents * Record register deltas in trace * Move initialization to _start_run so we can call run() multiple times * Re-fix multiple workspace bug * Fix it correctly * Add extended trace and accessors * make sure did_execute_instruction is always published * Produce a consistent version * move extended tracing to separate class * Reorg of extended tracing plugins * Add concolic tracing script * Clean up old hooks * Sync memory as well; cleanups * Revert binary tests * simplify concolic follower * Move trace follower to plugin.py * Simplify follower * Add skip ranges to Follower * Update concolic.py * Remove redundant state init * Clean up driver script * Update header line * Move trace follower * Move Follower to follow_trace.py * rm unused import * Remove unnecessary property * rm ConcreteTraceFollower * Revert start_run behavior * Initial implementation of concolic algorithm (#574) * Fix coverage calculation vs. metadata (#529) * Fixes symbolic reentrancy example * Fix coverage Issue# 527 * Remove debug unused code * Various bug fixes. (#530) * Fixes #503 * Fixes #515 * Fixes 272. Concretize data written to a fd. * Revert debug hack and fix overly broad exception * Update did/will_exec_instr semantics * Clean up imports * Update logging and improve sys_open return * Update variable names+doc for consistency * Remove win32 support (#535) * Remove Windows support files * Remove Windows test files * Localize log formatting changes (#547) * Don't add custom format string to root logger * Fix handler propagation * Move inline function definitions out of the AbstractCPU's execute method (#538) * This change moves from inline function definitions out of the critical path of AbstractCpu's execute method. * Raise a mcore exception if we fail at emulation * Fix all integral type checks that forget long (#555) * [fix] Issue #550: generates extra workspace folder (#557) * [fix] Issue #550: generates extra workspace folder Signed-off-by: Cole Lightfighter * Slight workspace and store refactor * Handle file.tell() error, which will happen for special files (/dev/tty) (#559) * Fix SLOAD invalid memory access (#562) Check global_storage includes an entry at address before trying to load storage. * New API for EVM analysis (#551) * 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 * Add PCMPXSTRX Instructions (#507) * Add PCMPXSTRX Instructions * bug fixes * unittest related fixes * Full test of pcmpxstrx * Move tests * Fix typo per issue #552 - s/arm64/amd64/ (#561) * Added missing syscalls in decree syscall trace (#545) * added missing syscalls in decree syscall trace * added missing parameter in callback of BranchLimited policy * progress * can flip constraint set * hack around double decl issue * can gen input * what is this, a coding interview? * did it? * clean * finish * pretty log messages * comment, clean * more cleaning * cmt * Only really fork when there's multiple solutions (#569) * Update comment and path * Add UMD simple assert example (#573) * Manticore prints linux ret code as uint instead of int (#578) * Fixing raise issue #435 * syncing git * Fix Bug #570 * syncing * removed all binaries * missed one file * Updates travis cache to python 2.7.13 (#576) * Updating README with solc binary requirements (#575) * Updating README with solc binary requirements * Update README.md * Assert valid operand length (#558) * Assert valid bytecode and operand length EVM bytecode comes in 32-byte chunks, and contracts require at least one segment to be created. An example, originally written by @ggrieco-tob in issue #546, is included. Unsure what expected behavior should be, but initial state has a problem when a contract is created with a single byte. Also added some exception handling in `parse_operand()` to catch invalid instructions, e.g. a PUSH1 instruction followed by no bytes. Signed-off-by: Cole Lightfighter * Fix SLOAD invalid memory access Simple check to ensure address storage is in global_storage before attempting to load data. * Remove invalid assertions * Fix for issue 556 and 591 (#590) * version argument in manticore * Fix 591 - Exception Handler * Fix Issue: 597 - Remove unused policy argument in function State.solve_n (#598) * version argument in manticore * Fix 591 - Exception Handler * Issue 597 - Remove the unused policy argument * Fixes to thumb mode instruction implementations * Thumb specific fixes to the SUB, BX, and MOV instruction implementations * implemented hardcoded result for gettid syscall * Trace following mode (#513) * WIP New Policy class * WIP pubsub * Update Signal tests * small fixes from github comments * Fix event decode_instruction signature * Good merge * Good good merge * WIP manticore refactor * Fix default old-style initial state * add -> enqueue * @m.init * Fix workspace url * Some test skipped * Ad Fixme to platform specific stuff in State * add -> enqueue * Enqueue created state * Fix m.init Use a messy hack to adhere to the spec (callback func receive 1 state argument) * Add _coverage_file ivar to Manticore * Fix symbolic files * remove extra enqueue * Fixing __main__ * comments * Experimental plugin system * tests fixed * Fix plugins * Some reporting moved to plugin * Fix assertions test * Add published events to classes that publish them * Update how we verify callbacks * Update Eventful._publish * Yet another flavor for event name checking * really it's a bunch of minimal bugfixes * Remove get_all_event_names from Plugin * Update where we get all events * Use new metaclass-based event registry * Initial concrete trace follower * Add extended (json) trace support * More stubs for condition gather * Update trace saving to new format * Produce trace regardless of contents * Record register deltas in trace * Move initialization to _start_run so we can call run() multiple times * Re-fix multiple workspace bug * Fix it correctly * Add extended trace and accessors * make sure did_execute_instruction is always published * Produce a consistent version * move extended tracing to separate class * Reorg of extended tracing plugins * Add concolic tracing script * Clean up old hooks * Sync memory as well; cleanups * Revert binary tests * simplify concolic follower * Move trace follower to plugin.py * Simplify follower * Add skip ranges to Follower * Update concolic.py * Remove redundant state init * Clean up driver script * Update header line * Move trace follower * Move Follower to follow_trace.py * rm unused import * Remove unnecessary property * rm ConcreteTraceFollower * Revert start_run behavior * Centralize system call logging (#602) * Remove per-syscall logging * Make Cpu.read_string() stop reading at first symbolic byte * Centralize syscall logging * Update helper docstring * Update arg/ret expansion * Check for issymbolic first * Tiny hex format change * Log unimplemented instructions (issue 163) (#599) * Remove double printing of exception. * Pretty print the unimplemented instruction raised by unicorn (UcError). * Raise exception after unimplemented instruction error logging. * Ensure the raised exception is actually a unicorn invalid instruction error. * Resolve conflict * EVM assembler/disassembler doc and cleanup (#563) * 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 * 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 * EVMAssembler to EVMAsm * Fix evm @hook signature * EVMAsm * EVMasm refactor * EVM api refactor (#589) * 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 * Fixed Issue #533 (#606) * Remove Platform._path * Amend pr guidelines (#615) * Fixed Issue #619 (#623) Add newlines in .trace file generation * Hide legacy cli flags from cli help (#622) * Fixed Issue #533 * Removed --replay argument from cli help. Issue #617 * Update help description * Remove unused --size flag * Emit .input instead of .txt files in workspace (#625) Related: #612 * Update workspace.py Changed extension to .input * Update test_workspace.py * changed key value pair in test_workspace bc of change of extension to .input in workspace.py, fixed issue #618 * removed unwanted directories * Update seth.py * Update seth.py Change in Documentation issue #612 * EVM refactor and simple UI (#629) * 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 * Various refactors. Auxiliar for calculating % coverage * Change report in examples * Detailed transactions and reporting accessible to the user2 * Fix on Expression Array * Some documentation * Get full ABI from solc compiler * evm/examples -> bugfixes * Clarify try/except blocks * Code review * Code review * Initial eth cli based on solidse.py (#633) * 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 * Various refactors. Auxiliar for calculating % coverage * Change report in examples * Detailed transactions and reporting accessible to the user2 * Fix on Expression Array * Some documentation * Get full ABI from solc compiler * evm/examples -> bugfixes * Clarify try/except blocks * Code review * Code review * initially evm cli from solidse.py * rm prints, make import work it's just `import seth` because this file runs from the perspective of being inside the package. `from manticore.seth` doesn't work because manticore.py gets priority over the manticore package, and there is no seth entity inside manticore.py * rm wip cli file * add excess printing as a big comment * print minimal report * require .sol only * rm solidse again * rm fluff * evm: Make 'not enough funds' states finalized states (#636) * print on every * terminate not enough fund states * Better check * revert debug change * Implement initial evm workspace, fix small bugs (#638) * print on every * save the bytecode to look at later * update tuple * wip workspace files * wip * generate tx files * rm unused event handler * clean up solving for tx.data * Revert "print on every" 0caaae3658a169c9763c51544aa3c79a4e3940ca * Detectors () (#637) * 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 * Various refactors. Auxiliar for calculating % coverage * Change report in examples * Detailed transactions and reporting accessible to the user2 * Fix on Expression Array * Some documentation * Get full ABI from solc compiler * evm/examples -> bugfixes * Clarify try/except blocks * Code review * Code review * Code review * Code review * Code review * Initial detector plugin. integer overflow and unitialized mem * Better metadata handling and new events for detectors * detectors wip * Better name for internal findings context * Explicit detector register * review * Refactor concolic implementation (#601) * Refactor concolic.py * make arg name more descriptive * A few cleanups * Keep track of traces * Added perm() description * Rm meaningless paths variable * little comment * rm bug comment trace set is the correct solution; we need to filter out satisfiable but redundant paths that are generated by the dumb permuter * clean comments, debug stuff * Better EVM workspace output (#641) * 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 * Various refactors. Auxiliar for calculating % coverage * Change report in examples * Detailed transactions and reporting accessible to the user2 * Fix on Expression Array * Some documentation * Get full ABI from solc compiler * evm/examples -> bugfixes * Clarify try/except blocks * Code review * Code review * Code review * Code review * Code review * Initial detector plugin. integer overflow and unitialized mem * Better metadata handling and new events for detectors * detectors wip * Better name for internal findings context * Explicit detector register * review * New workspace output * Fix examples * wrog merge fix * Fix examples/new api * Fix examples/new api/output * More output * More doc * Broken examples deleted * Debug code removed * Wrong docstring * Update evm __main__ * Update evm __main__ * Update evm __main__ * Update evm __main__ * Update evm __main__ * Fix TODO * Fix for issue #642 (#643) * version argument in manticore * Fix 591 - Exception Handler * Issue 597 - Remove the unused policy argument * fix issue 642 * Fix z3 oddity: reset vs optimization (#627) * 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 * Fix compilation bug (#645) * fix for #608 using a local definition (#644) * refactor logs files content (#646) - if no logs just print nothing - output any printable bytes in the memlog as a convenience in case they logged strings --- examples/script/concolic.py | 281 +++++++++++++++++++++++++++ manticore/core/plugin.py | 69 +++++++ manticore/core/smtlib/constraints.py | 6 +- 3 files changed, 355 insertions(+), 1 deletion(-) create mode 100755 examples/script/concolic.py diff --git a/examples/script/concolic.py b/examples/script/concolic.py new file mode 100755 index 0000000..8fcb137 --- /dev/null +++ b/examples/script/concolic.py @@ -0,0 +1,281 @@ +#!/usr/bin/env python + +''' +Rough concolic execution implementation + +Limitations +- tested only on the simpleassert example program in examples/ +- only works for 3 ints of stdin + +Bugs +- Will probably break if a newly discovered branch gets more input/does another read(2) +- possibly unnecessary deepcopies + +''' + +import Queue +import struct +import itertools + +from manticore import Manticore +from manticore.core.plugin import ExtendedTracer, Follower, Plugin +from manticore.core.smtlib.constraints import ConstraintSet +from manticore.core.smtlib import Z3Solver, solver +from manticore.core.smtlib.visitors import pretty_print as pp + +import copy +from manticore.core.smtlib.expression import * + +prog = '../linux/simpleassert' +endd = 0x400ae9 +VERBOSITY = 0 + +def _partition(pred, iterable): + t1, t2 = itertools.tee(iterable) + return (list(itertools.ifilterfalse(pred, t1)), filter(pred, t2)) + +def log(s): + print '[+]', s + +class TraceReceiver(Plugin): + def __init__(self, tracer): + self._trace = None + self._tracer = tracer + super(self.__class__, self).__init__() + + @property + def trace(self): + return self._trace + + def will_generate_testcase_callback(self, state, test_id, msg): + self._trace = state.context[self._tracer.context_key] + + instructions, writes = _partition(lambda x: x['type'] == 'regs', self._trace) + total = len(self._trace) + log('Recorded concrete trace: {}/{} instructions, {}/{} writes'.format( + len(instructions), total, len(writes), total)) + +def flip(constraint): + ''' + flips a constraint (Equal) + + (Equal (BitVecITE Cond IfC ElseC) IfC) + -> + (Equal (BitVecITE Cond IfC ElseC) ElseC) + ''' + equal = copy.deepcopy(constraint) + + assert len(equal.operands) == 2 + # assume they are the equal -> ite form that we produce on standard branches + ite, forcepc = equal.operands + assert isinstance(ite, BitVecITE) and isinstance(forcepc, BitVecConstant) + assert len(ite.operands) == 3 + cond, iifpc, eelsepc = ite.operands + assert isinstance(iifpc, BitVecConstant) and isinstance(eelsepc, BitVecConstant) + + equal.operands[1] = eelsepc if forcepc.value == iifpc.value else iifpc + + return equal + +def eq(a, b): + # this ignores checking the conditions, only checks the 2 possible pcs + # the one that it is forced to + + ite1, force1 = a.operands + ite2, force2 = b.operands + + if force1.value != force2.value: + return False + + _, first1, second1 = ite1.operands + _, first2, second2 = ite1.operands + + if first1.value != first2.value: + return False + if second1.value != second2.value: + return False + + return True + +def perm(lst, func): + ''' Produce permutations of `lst`, where permutations are mutated by `func`. Used for flipping constraints. highly + possible that returned constraints can be unsat this does it blindly, without any attention to the constraints + themselves + + Considering lst as a list of constraints, e.g. + + [ C1, C2, C3 ] + + we'd like to consider scenarios of all possible permutations of flipped constraints, excluding the original list. + So we'd like to generate: + + [ func(C1), C2 , C3 ], + [ C1 , func(C2), C3 ], + [ func(C1), func(C2), C3 ], + [ C1 , C2 , func(C3)], + .. etc + + This is effectively treating the list of constraints as a bitmask of width len(lst) and counting up, skipping the + 0th element (unmodified array). + + The code below yields lists of constraints permuted as above by treating list indeces as bitmasks from 1 to + 2**len(lst) and applying func to all the set bit offsets. + + ''' + for i in range(1, 2**len(lst)): + yield [func(item) if (1< 0: + datas = new_datas + + for each in to_queue: + q.put(each) + + log('paths found: {}'.format(len(traces))) + +if __name__=='__main__': + main() diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py index 9c5122b..bfd3d0e 100644 --- a/manticore/core/plugin.py +++ b/manticore/core/plugin.py @@ -98,6 +98,47 @@ class ExtendedTracer(Plugin): } state.context[self.context_key].append(entry) +class Follower(Plugin): + def __init__(self, trace): + self.index = 0 + self.trace = trace + self.last_instruction = None + self.symbolic_ranges = [] + self.active = True + super(self.__class__, self).__init__() + + def add_symbolic_range(self, pc_start, pc_end): + self.symbolic_ranges.append((pc_start,pc_end)) + + def get_next(self, type): + event = self.trace[self.index] + assert event['type'] == type + self.index += 1 + return event + + def did_write_memory_callback(self, state, where, value, size): + if not self.active: + return + write = self.get_next('mem_write') + + if not issymbolic(value): + return + + assert write['where'] == where and write['size'] == size + # state.constrain(value == write['value']) + + def did_execute_instruction_callback(self, state, last_pc, pc, insn): + if not self.active: + return + event = self.get_next('regs') + self.last_instruction = event['values'] + if issymbolic(pc): + state.constrain(state.cpu.RIP == self.last_instruction['RIP']) + else: + for start, stop in self.symbolic_ranges: + if start <= pc <= stop: + self.active = False + class RecordSymbolicBranches(Plugin): def will_start_run_callback(self, state): state.context['branches'] = {} @@ -173,6 +214,34 @@ class Visited(Plugin): f.write(fmt.format(m)) logger.info('Coverage: %d different instructions executed', len(executor_visited)) +class ConcreteTraceFollower(Plugin): + def __init__(self, source=None): + ''' + :param iterable source: Iterator producing instruction pointers to be followed + ''' + super(ConcreteTraceFollower, self).__init__() + self.source = source + + def will_start_run_callback(self, state): + self.saved_flags = None + + def will_execute_instruction_callback(self, state, pc, instruction): + if not instruction.group(CS_GRP_JUMP): + self.saved_flags = None + return + + # Likely unconditional + if not instruction.regs_read: + self.saved_flags = None + return + + self.saved_flags = state.cpu.RFLAGS + state.cpu.RFLAGS = state.new_symbolic_value(state.cpu.address_bit_size) + + def did_execute_instruction_callback(self, state, pc, target_pc, instruction): + # Should direct execution via trace + if self.saved_flags: + state.cpu.RFLAGS = self.saved_flags #TODO document all callbacks class ExamplePlugin(Plugin): diff --git a/manticore/core/smtlib/constraints.py b/manticore/core/smtlib/constraints.py index 477ccf6..15361fa 100644 --- a/manticore/core/smtlib/constraints.py +++ b/manticore/core/smtlib/constraints.py @@ -150,8 +150,12 @@ class ConstraintSet(object): for expression in self.constraints: translator.visit(expression) + # band aid hack around the fact that we are double declaring stuff :( :( + tmp = set() for d in self.declarations: - result += d.declaration + '\n' + tmp.add(d.declaration) + for d in tmp: + result += d + '\n' for name, exp, smtlib in translator.bindings: if isinstance(exp, BitVec):