Various fixes for running a Smart Contract (#135)

* Fix writing buffer to memory accross segments

* EVM: concretize concolic values for some of the operations

* Add simplification

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<Value> 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;
         }
@@ -708,18 +716,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<Value> 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);

src/expression/expression.cpp

@@ -2029,6 +2029,11 @@ bool operator<(Op op1, Op op2)
     return static_cast<int>(op1) < static_cast<int>(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 ||

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;

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);

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<Value>& 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<Value>& buf, bool ignore_flags)
 {
     int nb_bytes = 0;
+    std::vector<Value> tmp_buf;
+    std::vector<Value> next_buf;
+    std::vector<Value> 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<Value>& 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;
+            }
         }
     }
 

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;
 }
 

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<Value> 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; 
         }
     }

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; 
         }