types: fixed width integers

typpete/src/annotation_resolver.py

@@ -11,6 +11,14 @@ def __init__(self, z3_types):
         self.primitives = {
             "object": z3_types.object,
             "int": z3_types.int,
+            "i8": z3_types.i8,
+            "i16": z3_types.i16,
+            "i32": z3_types.i32,
+            "i64": z3_types.i64,
+            "u8": z3_types.u8,
+            "u16": z3_types.u16,
+            "u32": z3_types.u32,
+            "u64": z3_types.u64,
             "bool": z3_types.bool,
             "float": z3_types.float,
             "complex": z3_types.complex,

typpete/src/z3_types.py

@@ -103,6 +103,7 @@ def init_axioms(self):
         for st in self.z3_types.subtyping:
             self.add(st, fail_message="Subtyping error")
         self.add(self.z3_types.subst_axioms, fail_message="Subst definition")
+        self.add(self.z3_types.int_limits_axioms(), fail_message="Int limits")
 
     def infer_stubs(self, context, infer_func):
         self.stubs_handler.infer_all_files(
@@ -157,6 +158,12 @@ def __init__(self, config, solver):
         self.complex = type_sort.complex
         self.float = type_sort.float
         self.int = type_sort.int
+        # fixed width
+        for w in (64, 32, 16, 8):
+            attr = f"u{w}"
+            setattr(self, attr, getattr(type_sort, attr))
+            attr = f"i{w}"
+            setattr(self, attr, getattr(type_sort, attr))
         self.bool = type_sort.bool
         # sequences
         self.seq = type_sort.sequence
@@ -551,6 +558,19 @@ def create_subtype_axioms(self, tree):
             axioms.append(axiom)
         return axioms
 
+    def int_limits_axioms(self):
+        axioms = []
+        # unsigned
+        for w in (64, 32, 16, 8):
+            t = getattr(self, f"u{w}")
+            a = And(t < (1 << w), t > 0)
+            axioms.append(a)
+        # signed
+        for w in (64, 32, 16, 8):
+            t = getattr(self, f"i{w}")
+            a = And(t < (1 << (w-1)), t >= -(1 << w))
+            axioms.append(a)
+        return axioms
 
 def declare_type_sort(max_tuple_length, max_function_args, classes_to_base, type_vars):
     """Declare the type data type and all its constructors and accessors."""
@@ -564,6 +584,10 @@ def declare_type_sort(max_tuple_length, max_function_args, classes_to_base, type
     type_sort.declare("complex")
     type_sort.declare("float")
     type_sort.declare("int")
+    # fixed width
+    for w in (64, 32, 16, 8):
+        type_sort.declare(f"u{w}")
+        type_sort.declare(f"i{w}")
     type_sort.declare("bool")
 
     for tp in type_vars.values():