diff --git a/src/engine/callother.cpp b/src/engine/callother.cpp index 8459109b..e09bb8b9 100644 --- a/src/engine/callother.cpp +++ b/src/engine/callother.cpp @@ -614,22 +614,30 @@ void EVM_ENV_INFO_handler(MaatEngine& engine, const ir::Inst& inst, ir::Processe case 0x3d: // RETURNDATASIZE { if (not contract->result_from_last_call.has_value()) - throw callother_exception("RETURNDATASIZE: contract runtime doesn't have any transaction result set"); - pinst.res = Value(256, contract->result_from_last_call->return_data_size()); + pinst.res = Value(256, 0); + else + pinst.res = Value(256, contract->result_from_last_call->return_data_size()); break; } case 0x3e: // RETURNDATACOPY { - if (not contract->result_from_last_call.has_value()) - throw callother_exception("RETURNDATACOPY: contract runtime doesn't have any transaction result set"); Value addr = contract->stack.get(0); addr_t offset = contract->stack.get(1).as_uint(*engine.vars); unsigned int size = contract->stack.get(2).as_uint(*engine.vars); contract->stack.pop(3); - for (const auto& val : contract->result_from_last_call->return_data_load_bytes(offset, size)) + if (not contract->result_from_last_call.has_value()) { - contract->memory.write(addr, val); - addr = addr + val.size()/8; + // Write zeroes + std::vector zeroes (size, Value(8,0)); + contract->memory.write(addr, zeroes); + } + else + { + for (const auto& val : contract->result_from_last_call->return_data_load_bytes(offset, size)) + { + contract->memory.write(addr, val); + addr = addr + val.size()/8; + } } break; } @@ -703,18 +711,24 @@ void _set_return_data(MaatEngine& engine, const Value& addr, const Value& len, e { env::EVM::contract_t contract = env::EVM::get_contract_for_engine(engine); - if (not len.is_concrete(*engine.vars)) - throw callother_exception("Getting transaction return data: not supported with symbolic length"); - if (not addr.is_concrete(*engine.vars)) - throw callother_exception("Getting transaction return data: not supported with symbolic address"); + if (len.is_symbolic(*engine.vars)) + throw callother_exception("Setting transaction return data: not supported with symbolic length"); + else if (len.is_concolic(*engine.vars)) + engine.log.warning("Setting transaction return data: concretizing concolic length"); + + if (addr.is_symbolic(*engine.vars)) + throw callother_exception("Setting transaction return data: not supported with symbolic address"); + else if (addr.is_concolic(*engine.vars)) + engine.log.warning("Setting transaction return data: concretizing concolic address"); std::vector return_data; _check_transaction_exists(contract); - if (len.as_uint(*engine.vars) != 0) + ucst_t concrete_len = len.as_number(*engine.vars).get_ucst(); + if (concrete_len != 0) { return_data = contract->memory.mem()._read_optimised_buffer( - addr.as_uint(*engine.vars), - len.as_uint(*engine.vars) + addr.as_number(*engine.vars).get_ucst(), + concrete_len ); } contract->transaction->result = env::EVM::TransactionResult(type, return_data); diff --git a/src/expression/expression.cpp b/src/expression/expression.cpp index ea3e7e06..33950c04 100644 --- a/src/expression/expression.cpp +++ b/src/expression/expression.cpp @@ -2029,6 +2029,11 @@ bool operator<(Op op1, Op op2) return static_cast(op1) < static_cast(op2); } +bool op_is_bitwise(Op op) +{ + return (op == Op::AND || op == Op::OR || op == Op::XOR || op == Op::NOT); +} + bool op_is_symetric(Op op) { return (op == Op::ADD || op == Op::AND || op == Op::MUL || op == Op::MULH || diff --git a/src/expression/simplification.cpp b/src/expression/simplification.cpp index aff8c2bc..a5be2242 100644 --- a/src/expression/simplification.cpp +++ b/src/expression/simplification.cpp @@ -324,9 +324,28 @@ Expr es_extract_patterns(Expr e) // extract(concat(X,Y), a, b) --> extract(Y, a', b') else if( e->args[1]->cst() < e->args[0]->args[1]->size ) { - return extract( e->args[0]->args[1], - e->args[1]->cst(), - e->args[2]->cst()); + return extract( + e->args[0]->args[1], + e->args[1]->cst(), + e->args[2]->cst() + ); + } + // extract overlaps X and Y components: + // extract(concat(X,Y), a, b) --> concat(extract(X, a', 0), extract(Y, sizeof(Y)-1, b')) + else + { + return concat( + extract( + e->args[0]->args[0], + e->args[1]->cst() - e->args[0]->args[1]->size, // a-sizeof(Y) + 0 + ), + extract( + e->args[0]->args[1], + e->args[0]->args[1]->size-1, + e->args[2]->cst() // b + ) + ); } } // extract(extract(X,a,b),c,d) --> extract(X, c+b,d+b) @@ -541,6 +560,35 @@ Expr es_concat_patterns(Expr e) ); } + // X &|^ concat(A,B) = concat(X' &|^ A, X'' &|^ B) + if ( + e->is_type(ExprType::BINOP) && + op_is_bitwise(e->op()) && + e->args[0]->is_type(ExprType::CST) && + e->args[1]->is_type(ExprType::CONCAT) + ){ + return concat( + exprbinop( + e->op(), + extract( + e->args[0], + e->args[0]->size-1, + e->args[1]->args[1]->size // sizeof(B) + ), + e->args[1]->args[0] // A + ), + exprbinop( + e->op(), + extract( + e->args[0], + e->args[1]->args[1]->size-1, // sizeof(B) + 0 + ), + e->args[1]->args[1] // B + ) + ); + } + // TODO: support the below simplifications for expressions > 64bits also if (e->size > 64) return e; diff --git a/src/include/maat/expression.hpp b/src/include/maat/expression.hpp index 96e8cad9..a0b80ef9 100644 --- a/src/include/maat/expression.hpp +++ b/src/include/maat/expression.hpp @@ -93,6 +93,7 @@ enum class Op : uint8_t std::string op_to_str(Op op); bool operator<(Op op1, Op op2); +bool op_is_bitwise(Op op); bool op_is_symetric(Op op); bool op_is_associative(Op op); bool op_is_left_associative(Op op); diff --git a/src/memory/memory.cpp b/src/memory/memory.cpp index 4e7fdd2b..ded1658a 100644 --- a/src/memory/memory.cpp +++ b/src/memory/memory.cpp @@ -1196,6 +1196,26 @@ static inline void concat_endian( res.set_concat(first, second); } +// Extract bytes to be written according to endianness +// For big endian extract left-most bytes, for little endian +// extract right-most bytes +static inline Value extract_endian( + const Value& val, + int high_byte, + int low_byte, + Endian endian +) +{ + if (endian == Endian::LITTLE) + return extract(val, high_byte*8-1, low_byte*8); + else + return extract( + val, + val.size()-1-(low_byte*8), + val.size()-(high_byte+1)*8 + ); +} + void MemSegment::read(Value& res, addr_t addr, unsigned int nb_bytes) { offset_t off = addr - start; @@ -1402,7 +1422,7 @@ void MemSegment::write(addr_t addr, const std::vector& buf, VarContext& c for (const Value& val : buf) { if (addr + val.size()/8 -1 > end) - throw mem_exception("MemSegment: buffer copy: nb_bytes exceeds segment"); + throw mem_exception("MemSegment: buffer write: nb_bytes exceeds segment"); write(addr, val, ctx); addr += val.size()/8; off += val.size()/8; @@ -1414,7 +1434,7 @@ void MemSegment::write(addr_t addr, uint8_t* src, int nb_bytes) offset_t off = addr-start; if( addr + nb_bytes -1 > end) { - throw mem_exception("MemSegment: buffer copy: nb_bytes exceeds segment"); + throw mem_exception("MemSegment:: buffer write: nb_bytes exceeds segment"); } _concrete.write_buffer(off, src, nb_bytes); _bitmap.mark_as_concrete(off, off+nb_bytes-1); @@ -1957,7 +1977,7 @@ ValueSet MemEngine::limit_symptr_range(Expr addr, const ValueSet& range, const S ValueSet res(range.size); // Adjust the value set min - tmp_addr_min = addr->as_uint(*_varctx) - settings.symptr_max_range/2; + tmp_addr_min = addr->as_number(*_varctx).get_ucst() - settings.symptr_max_range/2; tmp_addr_min -= tmp_addr_min % range.stride; // Adjust lower bound on stride if (tmp_addr_min < range.min) { @@ -2361,6 +2381,9 @@ void MemEngine::write_buffer(addr_t addr, uint8_t* src, int nb_bytes, bool ignor void MemEngine::write_buffer(addr_t addr, const std::vector& buf, bool ignore_flags) { int nb_bytes = 0; + std::vector tmp_buf; + std::vector next_buf; + std::vector tmp_buf2; for (const Value& val : buf) nb_bytes += val.size()/8; @@ -2389,8 +2412,55 @@ void MemEngine::write_buffer(addr_t addr, const std::vector& buf, bool ig ); } - segment->write(addr, buf, *_varctx); - return; + // If buffer exceeds segment size, adjust the number of bytes to write + int tmp_nb_bytes = nb_bytes; + tmp_buf.clear(); + next_buf.clear(); + if (tmp_buf2.empty()) + tmp_buf2 = buf; // copy buf + if (addr + nb_bytes > segment->end) + { + tmp_nb_bytes = segment->end - addr+1; + int tmp_size = 0; + // Truncate the buffer to write + for (const auto& val : tmp_buf2) + { + if (tmp_size + val.size()/8 <= tmp_nb_bytes) + { + tmp_buf.push_back(val); + tmp_size += val.size()/8; + } + else if (tmp_size < tmp_nb_bytes) + { + tmp_buf.push_back( + extract_endian(val, tmp_nb_bytes-tmp_size-1, 0, _endianness) + ); + next_buf.push_back( + extract_endian( + val, val.size()/8 -1, tmp_nb_bytes-tmp_size, _endianness + ) + ); + tmp_size = tmp_nb_bytes; + } + else + { + next_buf.push_back(val); + tmp_size += val.size()/8; + } + } + // Write partial buffer + segment->write(addr, tmp_buf, *_varctx); + // Update data to write + nb_bytes -= tmp_nb_bytes; + addr += tmp_nb_bytes; + tmp_buf2 = std::move(next_buf); // OK to move because we clear() we using it + } + // Else if buffer fits in the segment, just write everyting + else + { + segment->write(addr, tmp_buf2.empty()? buf : tmp_buf2, *_varctx); + return; + } } } diff --git a/src/memory/symbolic_memory.cpp b/src/memory/symbolic_memory.cpp index 989c1269..340a1efd 100644 --- a/src/memory/symbolic_memory.cpp +++ b/src/memory/symbolic_memory.cpp @@ -350,6 +350,13 @@ Expr SymbolicMemEngine::concrete_ptr_read(Expr addr, int nb_bytes, Expr base_exp for( int count = 0; count < write_count; count++ ) { SymbolicMemWrite& write = writes[count]; + // If read address and write address sizes don't match, adjust read address + // This can happen when reading from a constant on archs that have addresses + // on more than 64 bits (e.g EVM). The MemEngine will create 64 bits + // addresses by default, so we need to adjust their size here manually + if (write.addr->size > addr->size and addr->is_type(ExprType::CST)) + addr = exprcst(write.addr->size, addr->cst()); + if( write.refined_value_set.is_cst()) { // Only update value if concrete write falls into the range of the read @@ -398,6 +405,7 @@ Expr SymbolicMemEngine::concrete_ptr_read(Expr addr, int nb_bytes, Expr base_exp } } } + return res; } diff --git a/tests/unit-tests/test_memory.cpp b/tests/unit-tests/test_memory.cpp index 7e1757a5..48811f9d 100644 --- a/tests/unit-tests/test_memory.cpp +++ b/tests/unit-tests/test_memory.cpp @@ -369,7 +369,7 @@ namespace test{ nb += _assert(mem.read(0x10000, 4).as_expr()->eq(concat(concat(extract(e5, 7, 0), e3), e1)), "MemSegment symbolic simple overlapping read failed"); nb += _assert(mem.read(0x10001, 4).as_expr()->eq(concat(extract(e5, 15, 0), e3)), "MemSegment symbolic simple overlapping read failed"); nb += _assert(mem.read(0x10006, 8).as_expr()->eq(concat(extract(e7, 55, 0), extract(e5, 31, 24))), "MemSegment symbolic simple overlapping read failed"); - + /* Overwrite */ mem.write(0x10100, e7, ctx); mem.write(0x10104, e6, ctx); @@ -687,6 +687,12 @@ namespace test{ ctx->set("var1", 0x12345678abababab); nb += _assert(e2->as_uint(*ctx) == 0x12345678abababab, "MemEngine: read/write accross segments failed"); + // With abstract buffer + ctx->set("var1", 0x12345678abababff); + std::vector buf{648, e}; + mem2.write_buffer(0x1001, buf); + nb += _assert(mem2.read(0x2000, 1).as_uint(*ctx) == 0xff, "MemEngine: failed to correctly write buffer accross segments"); + return nb; } } diff --git a/tests/unit-tests/test_simplification.cpp b/tests/unit-tests/test_simplification.cpp index e0cf1d30..6c292bff 100644 --- a/tests/unit-tests/test_simplification.cpp +++ b/tests/unit-tests/test_simplification.cpp @@ -209,6 +209,10 @@ namespace test e1 = concat(e, e2) >> 64; nb += _assert_simplify(e1, concat(exprcst(64, 0), e), s); + + e1 = 0xff & concat(v1, v2); + nb += _assert_simplify(e1, concat(exprcst(8, 0), 0xff & v2), s); + return nb; }