# Copyright 2024 Apheleia
#
# Description:
# Apheleia Verification Library Variable Class
from __future__ import annotations
from collections.abc import Callable
from typing import Any
from z3 import And, Int
from .logic import Logic
[docs]
class Uint(Logic):
[docs]
def __init__(
self,
name: str,
value: int,
auto_random: bool = True,
fmt: Callable[..., int] = str,
width: int = 32
) -> None:
"""
Initialize an instance of the class.
:param name: The name of the instance.
:type name: str
:param value: The value to be assigned to the instance.
:type value: int
:param auto_random: Flag to enable automatic randomization, defaults to True.
:type auto_random: bool, optional
:param fmt: The format to be used, defaults to str.
:type fmt: function, optional
:param width: The width of the variable in bits, defaults to 32.
:type width: int, optional
:raises ValueError: If the width is not a positive integer.
"""
super().__init__(name, value, auto_random=auto_random, fmt=fmt, width=width)
def _z3_(self) -> Int:
"""
Get the Z3 representation of the variable.
Add a range constraint to ensure the value is within the specified limits.
:return: The Z3 BitVec representation of the variable.
:rtype: z3.BitVecRef
"""
(_min_, _max_) = self._range_()
self.add_constraint(
'_c_range_',
lambda x: And(x >= _min_, x <= _max_),
hard=True,
)
return Int(f"{self._idx_}")
[docs]
class Uint8(Uint):
[docs]
def __init__(
self, name: str, value: int, auto_random: bool = True, fmt: Callable[..., int] = str
) -> None:
"""
Initialize an instance of the class.
:param name: The name of the instance.
:type name: str
:param value: The value to be assigned to the instance.
:type value: int
:param auto_random: Flag to enable automatic randomization, defaults to True.
:type auto_random: bool, optional
:param fmt: The format to be used, defaults to str.
:type fmt: function, optional
"""
super().__init__(name, value, auto_random=auto_random, fmt=fmt, width=8)
def _wrap_(self, result : Any) -> Uint8:
"""
Wrap the result in an Logic instance.
:param result: The result to be wrapped.
:type result: Any
:return: An instance of Logic with the result.
:rtype: Logic
"""
return type(self)(self.name, result, auto_random=self._auto_random_, fmt=self._fmt_)
[docs]
class Uint16(Uint):
[docs]
def __init__(
self, name: str, value: int, auto_random: bool = True, fmt: Callable[..., int] = str
) -> None:
"""
Initialize an instance of the class.
:param name: The name of the instance.
:type name: str
:param value: The value to be assigned to the instance.
:type value: int
:param auto_random: Flag to enable automatic randomization, defaults to True.
:type auto_random: bool, optional
:param fmt: The format to be used, defaults to str.
:type fmt: function, optional
"""
super().__init__(name, value, auto_random=auto_random, fmt=fmt, width=16)
def _wrap_(self, result : Any) -> Uint16:
"""
Wrap the result in an Logic instance.
:param result: The result to be wrapped.
:type result: Any
:return: An instance of Logic with the result.
:rtype: Logic
"""
return type(self)(self.name, result, auto_random=self._auto_random_, fmt=self._fmt_)
[docs]
class Uint32(Logic):
[docs]
def __init__(
self, name: str, value: int, auto_random: bool = True, fmt: Callable[..., int] = str
) -> None:
"""
Initialize an instance of the class.
:param name: The name of the instance.
:type name: str
:param value: The value to be assigned to the instance.
:type value: int
:param auto_random: Flag to enable automatic randomization, defaults to True.
:type auto_random: bool, optional
:param fmt: The format to be used, defaults to str.
:type fmt: function, optional
"""
super().__init__(name, value, auto_random=auto_random, fmt=fmt, width=32)
def _wrap_(self, result : Any) -> Uint32:
"""
Wrap the result in an Logic instance.
:param result: The result to be wrapped.
:type result: Any
:return: An instance of Logic with the result.
:rtype: Logic
"""
return type(self)(self.name, result, auto_random=self._auto_random_, fmt=self._fmt_)
[docs]
class Uint64(Uint):
[docs]
def __init__(
self, name: str, value: int, auto_random: bool = True, fmt: Callable[..., int] = str
) -> None:
"""
Initialize an instance of the class.
:param name: The name of the instance.
:type name: str
:param value: The value to be assigned to the instance.
:type value: int
:param auto_random: Flag to enable automatic randomization, defaults to True.
:type auto_random: bool, optional
:param fmt: The format to be used, defaults to str.
:type fmt: function, optional
"""
super().__init__(name, value, auto_random=auto_random, fmt=fmt, width=64)
def _wrap_(self, result : Any) -> Uint64:
"""
Wrap the result in an Logic instance.
:param result: The result to be wrapped.
:type result: Any
:return: An instance of Logic with the result.
:rtype: Logic
"""
return type(self)(self.name, result, auto_random=self._auto_random_, fmt=self._fmt_)
__all__ = ["Uint", "Uint8", "Uint16", "Uint32", "Uint64"]