Dev fix solver getvalue (#739)

* Increment default gas

* Do not solve concrete values

* Do not solve concrete values

* Do not solve concrete values

* Remove comment

* Make solver get_value return concrete values untouched - wip

* Handle solver.get_value integers

* fix reporting

* Make solver.get_value return the expression untouched when concrete

* Remove hack; we know `c` can't be an int type

* Revert "Remove hack; we know `c` can't be an int type"

0849094525d7e4cea0295d4be13552dea9c8ad72

* Fix cli --data argument

Previously, it was being ignored :/

* Fix linux output generation

solve.get_value returns back an int, if it concretized the sym var

* Revert "Fix cli --data argument"

2ee740acb20a9d393e1a7984d7ec0e0fe64dbfaf

manticore/ethereum.py

@@ -1196,7 +1196,8 @@ class ManticoreEVM(Manticore):
                 tx_summary.write("From: 0x%x %s\n" % (state.solve_one(tx.caller), flagged(issymbolic(tx.caller))))
                 tx_summary.write("To: 0x%x %s\n" % (state.solve_one(tx.address), flagged(issymbolic(tx.address))))
                 tx_summary.write("Value: %d %s\n"% (state.solve_one(tx.value), flagged(issymbolic(tx.value))))
-                tx_summary.write("Data: %s %s\n"% (state.solve_one(tx.data).encode('hex'), flagged(issymbolic(tx.data))))
+                tx_data = ''.join(state.solve_one(tx.data))
+                tx_summary.write("Data: %s %s\n"% (tx_data.encode('hex'), flagged(issymbolic(tx.data))))
                 if tx.return_data is not None:
                     return_data = state.solve_one(tx.return_data)
                     tx_summary.write("Return_data: %s %s\n" % (''.join(return_data).encode('hex'), flagged(issymbolic(tx.return_data))))
@@ -1246,8 +1247,8 @@ class ManticoreEVM(Manticore):
                 logs_summary.write("Address: %x\n" % log_item.address)
                 logs_summary.write("Memlog: %s (%s) %s\n" % (solved_memlog.encode('hex'), printable_bytes, flagged(is_log_symbolic)))
                 logs_summary.write("Topics:\n")
-                for topic in log_item.topics:
-                    logs_summary.write("\t%d) %x %s" %(log_item.topics.index(topic), state.solve_one(topic), flagged(issymbolic(topic))))
+                for i, topic in enumerate(log_item.topics):
+                    logs_summary.write("\t%d) %x %s" %(i, state.solve_one(topic), flagged(issymbolic(topic))))
 
         with testcase.open_stream('constraints') as smt_summary:
             smt_summary.write(str(state.constraints))

manticore/platforms/evm.py

@@ -1195,7 +1195,6 @@ class EVM(Eventful):
         if isinstance(value, Constant) and not value.taint: 
             value = value.value
         self._publish('did_evm_read_memory', address, value)
-
         return value
 
     @staticmethod
@@ -1260,8 +1259,9 @@ class EVM(Eventful):
         return self.stack.pop()
 
     def _consume(self, fee):
-        assert fee>=0
+        assert fee >= 0
         if self._gas < fee:
+            logger.debug("Not enough gas for instruction")
             raise NotEnoughGas()
         self._gas -= fee
 
@@ -1774,11 +1774,10 @@ class EVM(Eventful):
     def read_buffer(self, offset, size):
         if size:
             self._allocate(offset+size)
-
         data = []
         for i in xrange(size):
-            data.append(Operators.CHR(self._load(offset+i)))
-
+            data.append(self._load(offset+i))
+        data = map(Operators.CHR, data)
         if any(map(issymbolic, data)):
             data_symb = self._constraints.new_array(index_bits=256, index_max=len(data))
             for i in range(len(data)):

manticore/platforms/linux.py

@@ -2584,13 +2584,11 @@ class SLinux(Linux):
 
     def generate_workspace_files(self):
         def solve_to_fd(data, fd):
-            def make_chr(c):
-                if isinstance(c, int):
-                    return chr(c)
-                return c
             try:
                 for c in data:
-                    fd.write(make_chr(solver.get_value(self.constraints, c)))
+                    if issymbolic(c):
+                        c = chr(solver.get_value(self.constraints, c))
+                    fd.write(c)
             except SolverException:
                 fd.write('{SolverException}')