Fix operators.ORD for BitVecs of size > 8 (#1512)

* Fix operators.ORD for BitVecs of size > 8

TLDR: `ORD(s)` should return something that has 8 bits instead of 7, which it incorrectly did for BitVecs with size>8.

Note that the `ORD` still does not support `BitVec`s with size<8, but I am not sure if we need that support for now. To be clear, such situation ends up as an assertion failure that is being done in `BitVecExtract`, so when assertions are gone (for optimized launches) we might want to extend `ORD` to support it.

* Add proper ORD fix testcase

manticore/core/smtlib/operators.py

@@ -19,7 +19,7 @@ def ORD(s):
         if s.size == 8:
             return s
         else:
-            return BitVecExtract(s, 0, 7)
+            return BitVecExtract(s, 0, 8)
     elif isinstance(s, int):
         return s & 0xFF
     else:

tests/other/test_smtlibv2.py

@@ -681,6 +681,15 @@ def test_ORD(self):
         self.assertTrue(solver.check(cs))
         self.assertEqual(solver.get_value(cs, a), ord("Z"))
 
+    def test_ORD_proper_extract(self):
+        solver = Z3Solver.instance()
+        cs = ConstraintSet()
+        a = cs.new_bitvec(32)
+        cs.add(Operators.ORD(a) == Operators.ORD("\xff"))
+
+        self.assertTrue(solver.check(cs))
+        self.assertEqual(solver.get_value(cs, a), ord("\xff"))
+
     def test_CHR(self):
         solver = Z3Solver.instance()
         cs = ConstraintSet()