Fix sha3 (#703)

* the fix

* Add default example sha3 when unknown

* Review

* Remove IF statement on potentially symbolic value

manticore/ethereum.py

@@ -361,6 +361,7 @@ class ABI(object):
             padding = 32 - byte_size # for 160
             value = arithmetic_simplifier(Operators.CONCAT(size, *map(Operators.ORD, data[offset+padding:offset+padding+byte_size])))
             return simplify(value)
+
         if ty == u'uint256':
             return get_uint(256, offset), offset+32
         elif ty in (u'bool', u'uint8'):
@@ -1155,6 +1156,11 @@ class ManticoreEVM(Manticore):
                 summary.write("\n")
 
 
+            if blockchain._sha3:
+                summary.write("Known hashes:\n")
+                for key, value in blockchain._sha3.items():
+                    summary.write('%s::%x\n'%(key.encode('hex'), value))
+
             if is_something_symbolic:
                 summary.write('\n\n(*) Example solution given. Value is symbolic and may take other values\n')
 

manticore/platforms/evm.py

@@ -1504,7 +1504,7 @@ class EVM(Eventful):
         value = sha3.keccak_256(buf).hexdigest()
         value = int('0x'+value,0)
         self._publish('on_concrete_sha3', buf, value)
-        logger.info("Found new SHA3 example %r -> %x", buf, value)
+        logger.info("Found a concrete SHA3 example %r -> %x", buf, value)
         return value
 
 
@@ -1924,7 +1924,7 @@ class EVMWorld(Platform):
             self.forward_events_from(self.current)
             self.subscribe('on_concrete_sha3', self._concrete_sha3_callback)
 
-    def _concrete_sha3_callback(self,buf, value):
+    def _concrete_sha3_callback(self, buf, value):
         if buf in self._sha3:
             assert self._sha3[buf] == value
         self._sha3[buf] = value
@@ -2444,27 +2444,49 @@ class EVMWorld(Platform):
         self._publish('on_symbolic_sha3', data, self._sha3.items())
 
         results = []
+
+        #If know_hashes is true then there is a _known_ solution for the hash
         known_hashes = False
         for key, value in self._sha3.items():
+            assert not any( map(issymbolic, key))
             cond = compare_buffers(key, data)
             if solver.can_be_true(self._constraints, cond):
                 results.append((cond, value))  
                 known_hashes = Operators.OR(cond, known_hashes)
+        #results contains all the possible and known solutions
 
+
+        #If known_hashes can be False then data can take at least one concrete 
+        #value of which we do not know a hash for.
+
+        #Calculate the sha3 of one extra example solution and add this as a 
+        #potential result
+        #This is an incomplete result:
+        # Intead of choosing one single extra concrete solution we should save 
+        # the state and when a new sha3 example is found load it back and try 
+        #the new concretization for sha3.
+        
         with self._constraints as temp_cs:
             if solver.can_be_true(temp_cs, Operators.NOT(known_hashes)):
                 temp_cs.add(Operators.NOT(known_hashes))
+                #a_buffer is different from all strings we know a hash for 
                 a_buffer = solver.get_value(temp_cs, data)
                 cond = compare_buffers(a_buffer, data)
+                #Get the sha3 for a_buffer
+                a_value = int(sha3.keccak_256(a_buffer).hexdigest(), 16)
+                #add the new sha3 pair to the known_hashes and result
+                self._publish('on_concrete_sha3', a_buffer, a_value)
+                results.append((cond, a_value))
                 known_hashes = Operators.OR(cond, known_hashes)
-
+        
         if solver.can_be_true(self._constraints, known_hashes):
             self._constraints.add(known_hashes)
             value = 0 #never used
             for cond, sha in results:
                 value = Operators.ITEBV(256, cond, sha, value)
         else:
-            raise TerminateState()
+            raise TerminateState("Unknown hash")
             
         self.current._push(value)
         self.current.pc += self.current.instruction.size
+