From 72bc26acd2e5b0d4b3bec60e6f269602f61dce08 Mon Sep 17 00:00:00 2001 From: luongnt95 Date: Tue, 29 Aug 2017 19:25:51 +0700 Subject: [PATCH] Optimize symbolic expression --- oyente/symExec.py | 124 ++++++++++++++++++++++++++++++---------------- 1 file changed, 80 insertions(+), 44 deletions(-) diff --git a/oyente/symExec.py b/oyente/symExec.py index 2da35e77..3c6a2aab 100755 --- a/oyente/symExec.py +++ b/oyente/symExec.py @@ -702,6 +702,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path # both are real and we need to manually modulus with 2 ** 256 # if both are symbolic z3 takes care of modulus automatically computed = (first + second) % (2 ** 256) + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -715,6 +716,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path elif isSymbolic(first) and isReal(second): second = BitVecVal(second, 256) computed = first * second & UNSIGNED_BOUND_NUMBER + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -731,6 +733,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path computed = first - second else: computed = (first - second) % (2 ** 256) + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -751,11 +754,12 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = to_symbolic(second) solver.push() solver.add( Not (second == 0) ) - if solver.check() == unsat: + if check_solver() == unsat: computed = 0 else: computed = UDiv(first, second) solver.pop() + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -779,17 +783,17 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = to_symbolic(second) solver.push() solver.add(Not(second == 0)) - if solver.check() == unsat: + if check_solver() == unsat: computed = 0 else: solver.push() solver.add( Not( And(first == -2**255, second == -1 ) )) - if solver.check() == unsat: + if check_solver() == unsat: computed = -2**255 else: solver.push() solver.add(first / second < 0) - sign = -1 if solver.check() == sat else 1 + sign = -1 if check_solver() == sat else 1 z3_abs = lambda x: If(x >= 0, x, -x) first = z3_abs(first) second = z3_abs(second) @@ -797,6 +801,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path solver.pop() solver.pop() solver.pop() + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -819,13 +824,14 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path solver.push() solver.add(Not(second == 0)) - if solver.check() == unsat: + if check_solver() == unsat: # it is provable that second is indeed equal to zero computed = 0 else: computed = URem(first, second) solver.pop() + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -848,14 +854,14 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path solver.push() solver.add(Not(second == 0)) - if solver.check() == unsat: + if check_solver() == unsat: # it is provable that second is indeed equal to zero computed = 0 else: solver.push() solver.add(first < 0) # check sign of first element - sign = BitVecVal(-1, 256) if solver.check() == sat \ + sign = BitVecVal(-1, 256) if check_solver() == sat \ else BitVecVal(1, 256) solver.pop() @@ -866,6 +872,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path computed = sign * (first % second) solver.pop() + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -886,7 +893,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = to_symbolic(second) solver.push() solver.add( Not(third == 0) ) - if solver.check() == unsat: + if check_solver() == unsat: computed = 0 else: first = ZeroExt(256, first) @@ -895,6 +902,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path computed = (first + second) % third computed = Extract(255, 0, computed) solver.pop() + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -915,7 +923,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = to_symbolic(second) solver.push() solver.add( Not(third == 0) ) - if solver.check() == unsat: + if check_solver() == unsat: computed = 0 else: first = ZeroExt(256, first) @@ -924,6 +932,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path computed = URem(first * second, third) computed = Extract(255, 0, computed) solver.pop() + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -940,6 +949,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path # not supported in bit-vector theory new_var_name = gen.gen_arbitrary_var() computed = BitVec(new_var_name, 256) + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -962,18 +972,19 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = to_symbolic(second) solver.push() solver.add( Not( Or(first >= 32, first < 0 ) ) ) - if solver.check() == unsat: + if check_solver() == unsat: computed = second else: signbit_index_from_right = 8 * first + 7 solver.push() solver.add(second & (1 << signbit_index_from_right) == 0) - if solver.check() == unsat: + if check_solver() == unsat: computed = second | (2 ** 256 - (1 << signbit_index_from_right)) else: computed = second & ((1 << signbit_index_from_right) - 1) solver.pop() solver.pop() + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -989,12 +1000,13 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path first = to_unsigned(first) second = to_unsigned(second) if first < second: - stack.insert(0, 1) + computed = 1 else: - stack.insert(0, 0) + computed = 0 else: - sym_expression = If(ULT(first, second), BitVecVal(1, 256), BitVecVal(0, 256)) - stack.insert(0, sym_expression) + computed = If(ULT(first, second), BitVecVal(1, 256), BitVecVal(0, 256)) + computed = simplify(computed) if is_expr(computed) else computed + stack.insert(0, computed) else: raise ValueError('STACK underflow') elif instr_parts[0] == "GT": @@ -1006,12 +1018,13 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path first = to_unsigned(first) second = to_unsigned(second) if first > second: - stack.insert(0, 1) + computed = 1 else: - stack.insert(0, 0) + computed = 0 else: - sym_expression = If(UGT(first, second), BitVecVal(1, 256), BitVecVal(0, 256)) - stack.insert(0, sym_expression) + computed = If(UGT(first, second), BitVecVal(1, 256), BitVecVal(0, 256)) + computed = simplify(computed) if is_expr(computed) else computed + stack.insert(0, computed) else: raise ValueError('STACK underflow') elif instr_parts[0] == "SLT": # Not fully faithful to signed comparison @@ -1023,12 +1036,13 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path first = to_signed(first) second = to_signed(second) if first < second: - stack.insert(0, 1) + computed = 1 else: - stack.insert(0, 0) + computed = 0 else: - sym_expression = If(first < second, BitVecVal(1, 256), BitVecVal(0, 256)) - stack.insert(0, sym_expression) + computed = If(first < second, BitVecVal(1, 256), BitVecVal(0, 256)) + computed = simplify(computed) if is_expr(computed) else computed + stack.insert(0, computed) else: raise ValueError('STACK underflow') elif instr_parts[0] == "SGT": # Not fully faithful to signed comparison @@ -1040,12 +1054,13 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path first = to_signed(first) second = to_signed(second) if first > second: - stack.insert(0, 1) + computed = 1 else: - stack.insert(0, 0) + computed = 0 else: - sym_expression = If(first > second, BitVecVal(1, 256), BitVecVal(0, 256)) - stack.insert(0, sym_expression) + computed = If(first > second, BitVecVal(1, 256), BitVecVal(0, 256)) + computed = simplify(computed) if is_expr(computed) else computed + stack.insert(0, computed) else: raise ValueError('STACK underflow') elif instr_parts[0] == "EQ": @@ -1055,12 +1070,13 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = stack.pop(0) if isAllReal(first, second): if first == second: - stack.insert(0, 1) + computed = 1 else: - stack.insert(0, 0) + computed = 0 else: - sym_expression = If(first == second, BitVecVal(1, 256), BitVecVal(0, 256)) - stack.insert(0, sym_expression) + computed = If(first == second, BitVecVal(1, 256), BitVecVal(0, 256)) + computed = simplify(computed) if is_expr(computed) else computed + stack.insert(0, computed) else: raise ValueError('STACK underflow') elif instr_parts[0] == "ISZERO": @@ -1072,12 +1088,13 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path first = stack.pop(0) if isReal(first): if first == 0: - stack.insert(0, 1) + computed = 1 else: - stack.insert(0, 0) + computed = 0 else: - sym_expression = If(first == 0, BitVecVal(1, 256), BitVecVal(0, 256)) - stack.insert(0, sym_expression) + computed = If(first == 0, BitVecVal(1, 256), BitVecVal(0, 256)) + computed = simplify(computed) if is_expr(computed) else computed + stack.insert(0, computed) else: raise ValueError('STACK underflow') elif instr_parts[0] == "AND": @@ -1086,6 +1103,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path first = stack.pop(0) second = stack.pop(0) computed = first & second + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -1096,6 +1114,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = stack.pop(0) computed = first | second + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: @@ -1107,6 +1126,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = stack.pop(0) computed = first ^ second + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: @@ -1116,6 +1136,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path global_state["pc"] = global_state["pc"] + 1 first = stack.pop(0) computed = (~first) & UNSIGNED_BOUND_NUMBER + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -1137,11 +1158,12 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path second = to_symbolic(second) solver.push() solver.add( Not (Or( first >= 32, first < 0 ) ) ) - if solver.check() == unsat: + if check_solver() == unsat: computed = 0 else: computed = second & (255 << (8 * byte_index)) computed = computed >> (8 * byte_index) + computed = simplify(computed) if is_expr(computed) else computed stack.insert(0, computed) else: raise ValueError('STACK underflow') @@ -1300,7 +1322,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path expression = current_miu_i < temp solver.push() solver.add(expression) - if solver.check() != unsat: + if check_solver() != unsat: current_miu_i = If(expression, temp, current_miu_i) solver.pop() mem.clear() # very conservative @@ -1361,7 +1383,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path expression = current_miu_i < temp solver.push() solver.add(expression) - if solver.check() != unsat: + if check_solver() != unsat: current_miu_i = If(expression, temp, current_miu_i) solver.pop() mem.clear() # very conservative @@ -1428,7 +1450,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path expression = current_miu_i < temp solver.push() solver.add(expression) - if solver.check() != unsat: + if check_solver() != unsat: # this means that it is possibly that current_miu_i < temp current_miu_i = If(expression,temp,current_miu_i) solver.pop() @@ -1479,7 +1501,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path log.debug("Expression: " + str(expression)) solver.push() solver.add(expression) - if solver.check() != unsat: + if check_solver() != unsat: # this means that it is possibly that current_miu_i < temp current_miu_i = If(expression,temp,current_miu_i) solver.pop() @@ -1509,7 +1531,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path expression = current_miu_i < temp solver.push() solver.add(expression) - if solver.check() != unsat: + if check_solver() != unsat: # this means that it is possibly that current_miu_i < temp current_miu_i = If(expression,temp,current_miu_i) solver.pop() @@ -1689,7 +1711,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path solver.push() solver.add(is_enough_fund) - if solver.check() == unsat: + if check_solver() == unsat: # this means not enough fund, thus the execution will result in exception solver.pop() stack.insert(0, 0) # x = 0 @@ -1708,7 +1730,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path boolean_expression = (recipient != address_is) solver.push() solver.add(boolean_expression) - if solver.check() == unsat: + if check_solver() == unsat: solver.pop() new_balance_is = (global_state["balance"]["Is"] + transfer_amount) global_state["balance"]["Is"] = new_balance_is @@ -1753,7 +1775,7 @@ def sym_exec_ins(start, instr, stack, mem, memory, global_state, sha3_list, path solver.push() solver.add(is_enough_fund) - if solver.check() == unsat: + if check_solver() == unsat: # this means not enough fund, thus the execution will result in exception solver.pop() stack.insert(0, 0) # x = 0 @@ -2050,11 +2072,25 @@ def detect_bugs(): raise("Assertion checks need a Source Map") else: log.info("\t EVM code coverage: \t 0/0") + log.info("\t Callstack bug: \t False") + log.info("\t Money concurrency bug: False") + log.info("\t Time dependency bug: \t False") + log.info("\t Reentrancy bug: \t False") + if global_params.CHECK_ASSERTIONS: + log.info("\t Assertion failure: \t False") results["evm_code_coverage"] = "0/0" if global_params.WEB: results_for_web() +def check_solver(): + try: + ret = solver.check() + except Exception as e: + solver.pop() + raise e + return ret + def closing_message(): log.info("\t====== Analysis Completed ======") if global_params.STORE_RESULT: