From e202ebab04e6e244a57e217e1698520cf6f4e5f4 Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Tue, 13 Jan 2026 23:19:24 +0100 Subject: [PATCH 01/56] Add compilation to intermediate binary --- Cargo.toml | 2 + hycore/Cargo.toml | 5 +- hycore/src/base/api.rs | 46 ++++++- hycore/src/compiler.rs | 207 +++++++++++++++++++++++++++++ hycore/src/lib.rs | 1 + hycore/src/utils/error.rs | 3 + hyinstr/Cargo.toml | 1 + hyinstr/src/analysis.rs | 2 + hyinstr/src/modules/mod.rs | 3 + python/examples/sample.py | 35 +++++ python/python/hypi/api/__init__.py | 39 +++++- python/src/lib.rs | 25 +++- 12 files changed, 363 insertions(+), 6 deletions(-) create mode 100644 hycore/src/compiler.rs diff --git a/Cargo.toml b/Cargo.toml index ea8a55e..ac2d797 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -44,6 +44,8 @@ ariadne = "0.6" pyo3 = "0.27.0" once_cell = "^1" inventory = "^0.3" +serde_cbor = "=0.11.2" +borsh = "^1" criterion = "0.5" rand = "0.9.2" diff --git a/hycore/Cargo.toml b/hycore/Cargo.toml index 180b093..0e876df 100644 --- a/hycore/Cargo.toml +++ b/hycore/Cargo.toml @@ -4,7 +4,7 @@ version = "0.1.1" edition = "2024" [dependencies] -hyinstr.workspace = true +hyinstr = { workspace = true, features = ["serde", "chumsky"] } uuid = { workspace = true, features = ["v4", "serde"] } petgraph.workspace = true smallvec.workspace = true @@ -31,14 +31,13 @@ pyo3 = { workspace = true, features = [ ], optional = true } chrono = { workspace = true } inventory = { workspace = true } +serde_cbor.workspace = true [build-dependencies] build-info-build.workspace = true [features] default = [] - - pyo3 = ["dep:pyo3"] ext_hylog = [] diff --git a/hycore/src/base/api.rs b/hycore/src/base/api.rs index a4ff478..7a3b6ae 100644 --- a/hycore/src/base/api.rs +++ b/hycore/src/base/api.rs @@ -1,7 +1,8 @@ use std::sync::Arc; #[cfg(feature = "pyo3")] -use pyo3::FromPyObject; +use pyo3::{Borrowed, FromPyObject, PyAny, PyErr}; +use strum::FromRepr; use crate::{ base::InstanceContext, @@ -49,7 +50,50 @@ pub struct InstanceCreateInfo { pub ext: OpaqueList, } +/// Enumeration of the different sources from which a module can be compiled. +#[derive(Debug, Clone, Copy, PartialEq, Eq, FromRepr)] +#[repr(u32)] +pub enum ModuleSourceType { + /// Contains assembly code + Assembly, +} + +#[cfg(feature = "pyo3")] +impl<'a, 'py> FromPyObject<'a, 'py> for ModuleSourceType { + type Error = PyErr; + + fn extract(obj: Borrowed<'a, 'py, PyAny>) -> Result { + let level_int: u32 = obj.extract()?; + if let Some(level) = ModuleSourceType::from_repr(level_int) { + Ok(level) + } else { + Err(PyErr::new::(format!( + "Invalid LogLevelEXT value: {}", + level_int + ))) + } + } +} + +/// Information about the source of a module. +#[repr(C)] +#[cfg_attr(feature = "pyo3", derive(FromPyObject))] +pub struct ModuleSourceInfo { + pub source_type: ModuleSourceType, + pub filename: Option, + pub data: String, +} + +/// Structure containing information about how to compile a list of source files +#[repr(C)] +#[cfg_attr(feature = "pyo3", derive(FromPyObject))] +pub struct ModuleCompileInfo { + pub sources: Vec, +} + /// Creates and initializes a new [`InstanceContext`] from the provided metadata. pub unsafe fn create_instance(create_info: InstanceCreateInfo) -> HyResult> { unsafe { InstanceContext::create(create_info) } } + +pub use crate::compiler::compile_sources; diff --git a/hycore/src/compiler.rs b/hycore/src/compiler.rs new file mode 100644 index 0000000..a34f26b --- /dev/null +++ b/hycore/src/compiler.rs @@ -0,0 +1,207 @@ +use hyinstr::{ + modules::{Module, parser::extend_module_from_string}, + types::TypeRegistry, +}; +use log::info; +use serde::{Deserialize, Serialize}; + +use crate::{ + base::{ + InstanceContext, + api::{ModuleCompileInfo, ModuleSourceType}, + }, + hyerror, hytrace, + utils::error::{HyError, HyResult}, +}; + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct CompiledModuleStorageInternal { + pub filenames: Vec, + pub module: Module, +} + +impl CompiledModuleStorageInternal { + pub fn encode(&self, instance: &InstanceContext) -> HyResult> { + // Serialize inner using dlhn + let mut buf = Vec::new(); + let mut serializer = serde_cbor::Serializer::new(&mut buf); + self.serialize(&mut serializer).map_err(|e| { + hyerror!( + instance, + "Failed to serialize compiled module storage: {}", + e + ); + HyError::Unknown(format!( + "Failed to serialize compiled module storage: {}", + e + )) + })?; + + // Secondly, wrap in CompiledModuleStorage + let storage = CompiledModuleStorage { + magic: CompiledModuleStorage::MAGIC_BYTES, + version_req: semver::VersionReq { + comparators: vec![semver::Comparator { + op: semver::Op::Exact, + major: instance.version.major, + minor: Some(instance.version.minor), + patch: Some(instance.version.patch), + pre: instance.version.pre.clone(), + }], + }, + data: buf, + }; + + // Serialize the storage using serde_cbor for stability + hytrace!( + instance, + "Serializing compiled module storage wrapper with version requirement {}", + storage.version_req + ); + let mut buf = Vec::new(); + serde_cbor::to_writer(&mut buf, &storage).map_err(|e| { + hyerror!( + instance, + "Failed to serialize compiled module storage wrapper: {}", + e + ); + HyError::Unknown(format!( + "Failed to serialize compiled module storage wrapper: {}", + e + )) + })?; + + Ok(buf) + } + + pub fn decode(&self, instance: &InstanceContext, data: &[u8]) -> HyResult { + hytrace!( + instance, + "Deserializing compiled module storage ({} bytes)", + data.len() + ); + + // Deserialize the storage using serde_cbor + let storage: CompiledModuleStorage = serde_cbor::from_slice(data).map_err(|e| { + hyerror!( + instance, + "Failed to deserialize compiled module storage wrapper: {}", + e + ); + HyError::Unknown(format!( + "Failed to deserialize compiled module storage wrapper: {}", + e + )) + })?; + + // Check magic bytes + if storage.magic != CompiledModuleStorage::MAGIC_BYTES { + hyerror!(instance, "Invalid magic bytes in compiled module storage"); + return Err(HyError::Unknown( + "Invalid magic bytes in compiled module storage".to_string(), + )); + } + + // Check version compatibility + if !storage.version_req.matches(&instance.version) { + hyerror!( + instance, + "Incompatible compiled module storage version: required {}, found {}", + storage.version_req, + instance.version + ); + return Err(HyError::Unknown(format!( + "Incompatible compiled module storage version: required {}, found {}", + storage.version_req, instance.version + ))); + } + + // Deserialize inner using dlhn + let compiled_module: Self = + serde_cbor::from_slice(storage.data.as_slice()).map_err(|e| { + hyerror!( + instance, + "Failed to deserialize compiled module storage: {}", + e + ); + HyError::Unknown(format!( + "Failed to deserialize compiled module storage: {}", + e + )) + })?; + + Ok(compiled_module) + } +} + +/// Compiled IR module storage format. +/// +/// This is used to store compiled-module metadata alongside the serialized module data. +/// This should be kept stable across all versions of Hyperion. No modifications should be made +/// to this structure that would break compatibility with previously stored modules. +/// +/// See [`CompiledModuleStorage::MAGIC_BYTES`] for the magic bytes used to identify compiled module storage files. +/// See [`CompiledModuleStorageInternal`] for the internal representation used during (de)serialization. +/// +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct CompiledModuleStorage { + pub magic: [u8; 8], + pub version_req: semver::VersionReq, + pub data: Vec, +} + +impl CompiledModuleStorage { + /// Magic bytes used to identify compiled module storage files. + pub const MAGIC_BYTES: [u8; 8] = *b"\0HYCOMP\0"; +} + +pub fn compile_sources( + instance: &InstanceContext, + compile_info: ModuleCompileInfo, +) -> HyResult> { + let mut module = Module::default(); + let type_registry = TypeRegistry::new([0u8; 6]); + let mut filenames = Vec::new(); + + // Compile each source in the compile_info + for source_info in compile_info.sources { + hytrace!( + instance, + "Compiling source \"{}\"", + source_info.filename.as_deref().unwrap_or("") + ); + + if let Some(filename) = source_info.filename { + filenames.push(filename); + } + + match source_info.source_type { + ModuleSourceType::Assembly => { + // Compile assembly source code into the module + extend_module_from_string(&mut module, &type_registry, &source_info.data)?; + } + } + } + + // Produce compiled module storage or further processing here + let storage = CompiledModuleStorageInternal { module, filenames }; + let encoded_storage = storage.encode(instance)?; + + // Information about the compiled module can be used here + info!( + "Compiled successful, module has {} functions: {:?}", + storage.module.functions.len(), + storage + .module + .functions + .values() + .map(|x| x.name.clone().unwrap_or_else(|| format!("@{}", x.uuid))) + .collect::>() + ); + info!( + "Produced {} bytes of compiled module storage", + encoded_storage.len() + ); + + Ok(encoded_storage) +} diff --git a/hycore/src/lib.rs b/hycore/src/lib.rs index 0329122..f53b489 100644 --- a/hycore/src/lib.rs +++ b/hycore/src/lib.rs @@ -6,6 +6,7 @@ //! exported below. pub mod base; +pub mod compiler; pub mod ext; pub mod magic; pub mod provers; diff --git a/hycore/src/utils/error.rs b/hycore/src/utils/error.rs index 824f1bf..9b50e20 100644 --- a/hycore/src/utils/error.rs +++ b/hycore/src/utils/error.rs @@ -24,6 +24,9 @@ pub enum HyError { #[error("UTF-8 conversion error: {0}")] #[from(std::str::Utf8Error)] Utf8Error(std::str::Utf8Error), + + #[error("{0}")] + HyInstrError(#[from] hyinstr::utils::Error), } /// Convenience alias for fallible operations returning [`HyError`]. diff --git a/hyinstr/Cargo.toml b/hyinstr/Cargo.toml index 86eb1ab..f83029b 100644 --- a/hyinstr/Cargo.toml +++ b/hyinstr/Cargo.toml @@ -19,6 +19,7 @@ either.workspace = true enum-map.workspace = true bitflags.workspace = true chumsky = { workspace = true, optional = true } +borsh = { workspace = true, optional = true } [features] default = ["chumsky", "chumsky/either"] diff --git a/hyinstr/src/analysis.rs b/hyinstr/src/analysis.rs index 12f32d6..1bed5b7 100644 --- a/hyinstr/src/analysis.rs +++ b/hyinstr/src/analysis.rs @@ -1,4 +1,6 @@ use enum_map::Enum; +#[cfg(feature = "serde")] +use serde::{Deserialize, Serialize}; use strum::{EnumDiscriminants, EnumIs, EnumIter, EnumTryAs, IntoEnumIterator}; use crate::modules::instructions::InstructionFlags; diff --git a/hyinstr/src/modules/mod.rs b/hyinstr/src/modules/mod.rs index 20121d7..84ae43f 100644 --- a/hyinstr/src/modules/mod.rs +++ b/hyinstr/src/modules/mod.rs @@ -290,6 +290,7 @@ impl From for (Label, usize) { /// the next block to execute. This structure allows for the representation /// of complex control flow within functions. #[derive(Debug, Clone, Hash)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] pub struct BasicBlock { /// Unique block label. pub label: Label, @@ -332,6 +333,7 @@ impl BasicBlock { /// contain arbitrary control flow, including loops and recursion. /// #[derive(Debug, Clone, Hash)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] pub struct Function { /// The unique identifier (UUID) of the function. pub uuid: Uuid, @@ -815,6 +817,7 @@ pub struct FunctionAnalysisContext<'a> { /// Functions defined here appear in `functions`; references to symbols not /// defined locally are listed in `external_functions`. #[derive(Debug, Default, Clone, Hash)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] pub struct Module { /// Defined functions keyed by their UUID. pub functions: BTreeMap, diff --git a/python/examples/sample.py b/python/examples/sample.py index cf0eef8..5b7a614 100644 --- a/python/examples/sample.py +++ b/python/examples/sample.py @@ -29,4 +29,39 @@ def log_callback(log_message): ) instance = api.create_instance(instance_create_info) +source_code = api.compile_module( + instance, + api.ModuleCompileInfo( + sources=[ + api.ModuleSourceInfo( + source_type=api.ModuleSourceType.ASSEMBLY, + filename="example_module.hyasm", + data=""" + ; Example Hyperion assembly module + define i32 pow(%a: i32, %b: i32) { + entry: + jump loop_check + + loop_check: + %current.b: i32 = phi [%b, entry], [%next.b, loop_body] + %current.acc: i32 = phi [i32 0, entry], [%next.acc, loop_body] + %is_zero: i1 = icmp.eq %current.b, i32 0 + branch %is_zero, loop_end, loop_body + + loop_body: + %next.acc: i32 = imul.wrap %current.acc, %a + %next.b: i32 = isub.wrap %current.b, i32 1 + jump loop_check + + loop_end: + ret %current.acc + } + """, + ) + ] + ) +) + +print(source_code) + del instance diff --git a/python/python/hypi/api/__init__.py b/python/python/hypi/api/__init__.py index 07b00db..ead8c17 100644 --- a/python/python/hypi/api/__init__.py +++ b/python/python/hypi/api/__init__.py @@ -9,7 +9,8 @@ from hypi.api.ext.hylog import LogCreateInfoEXT, LogLevelEXT, LogMessageEXT from pydantic.dataclasses import dataclass from pydantic import Field -from enum import StrEnum +from typing import Optional +from enum import StrEnum, IntEnum class InstanceEXT(StrEnum): """Enumeration of built-in extensions that can be enabled on an instance.""" @@ -53,6 +54,22 @@ class InstanceCreateInfo: enabled_extensions: list[str] ext: list[object] = Field(default_factory=list) +class ModuleSourceType(IntEnum): + """Enumeration of source module types.""" + ASSEMBLY = 0 + +@dataclass +class ModuleSourceInfo: + """Information about a source module to be loaded into the instance.""" + source_type: ModuleSourceType + data: str + filename: Optional[str] = None + +@dataclass +class ModuleCompileInfo: + """Information about how to compile a source module.""" + sources: list[ModuleSourceInfo] + def create_instance(create_info: InstanceCreateInfo) -> lib.Instance: """Create an instance with the given creation info. @@ -71,6 +88,26 @@ def create_instance(create_info: InstanceCreateInfo) -> lib.Instance: assert isinstance(create_info, InstanceCreateInfo), "create_info must be an InstanceCreateInfo" return lib._hy_create_instance(create_info) +def compile_module(instance: lib.Instance, compile_info: ModuleCompileInfo) -> bytes: + """Compile a source module within the context of the given instance. + + Parameters + ---------- + instance: + Handle to a running Hyperion instance. + compile_info: + A fully populated :class:`ModuleCompileInfo` describing the source + module to be compiled. + + Returns + ------- + bytes + The compiled module as a byte array. + """ + assert isinstance(instance, lib.Instance), "instance must be a lib.Instance" + assert isinstance(compile_info, ModuleCompileInfo), "compile_info must be a ModuleCompileInfo" + return lib._hy_compile_module(instance, compile_info) + # Exported names __all__ = [ "InstanceCreateInfo", diff --git a/python/src/lib.rs b/python/src/lib.rs index 357155a..f6903a6 100644 --- a/python/src/lib.rs +++ b/python/src/lib.rs @@ -1,7 +1,7 @@ use std::sync::Arc; use hycore::base::{InstanceContext, api}; -use pyo3::prelude::*; +use pyo3::{prelude::*, types::PyBytes}; /// Opaque handle to a running Hyperion instance exposed to Python callers. #[pyclass] @@ -26,6 +26,28 @@ fn _hy_create_instance<'py>(instance_create_info: &Bound<'py, PyAny>) -> PyResul Ok(Instance(instance_context)) } +/// Compiles a list of source modules into a compiled module. +#[pyfunction] +fn _hy_compile_module<'py>( + instance: &Instance, + compile_info: &Bound<'py, PyAny>, +) -> PyResult> { + let py = compile_info.py(); + + let compile_info: api::ModuleCompileInfo = compile_info.extract().map_err(|e| { + PyErr::new::(format!("Invalid ModuleCompileInfo: {}", e)) + })?; + + let compiled_module = api::compile_sources(&instance.0, compile_info).map_err(|e| { + PyErr::new::(format!( + "Failed to compile module: {}", + e + )) + })?; + + Ok(PyBytes::new(py, &compiled_module).into()) +} + /// Computes the factorial of a number. #[pyfunction] fn factorial(n: u64) -> PyResult { @@ -61,6 +83,7 @@ fn hypi_sys(m: &Bound<'_, PyModule>) -> PyResult<()> { m.add_class::()?; m.add_function(wrap_pyfunction!(_hy_create_instance, m)?)?; + m.add_function(wrap_pyfunction!(_hy_compile_module, m)?)?; m.add_function(wrap_pyfunction!(factorial, m)?)?; m.add_function(wrap_pyfunction!(fibonacci, m)?)?; From 13bc85fa8ca55bf12223cdaa2acb53c73a07194c Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Wed, 14 Jan 2026 01:46:17 +0100 Subject: [PATCH 02/56] Transition to borsh for source storage and add zstd --- .vscode/settings.json | 2 +- Cargo.toml | 2 +- hycore/Cargo.toml | 11 +- hycore/src/compiler.rs | 232 ++++++++++++----------- hyinstr/Cargo.toml | 1 + hyinstr/src/analysis.rs | 11 +- hyinstr/src/consts/fp.rs | 27 +++ hyinstr/src/consts/int.rs | 35 ++++ hyinstr/src/consts/mod.rs | 4 + hyinstr/src/modules/instructions/fp.rs | 32 ++++ hyinstr/src/modules/instructions/int.rs | 76 ++++++++ hyinstr/src/modules/instructions/mem.rs | 20 ++ hyinstr/src/modules/instructions/meta.rs | 24 +++ hyinstr/src/modules/instructions/misc.rs | 28 +++ hyinstr/src/modules/instructions/mod.rs | 19 ++ hyinstr/src/modules/mod.rs | 28 +++ hyinstr/src/modules/operand.rs | 16 ++ hyinstr/src/modules/symbol.rs | 8 + hyinstr/src/modules/terminator.rs | 24 +++ hyinstr/src/types/mod.rs | 4 + hyinstr/src/types/primary.rs | 12 ++ 21 files changed, 497 insertions(+), 119 deletions(-) diff --git a/.vscode/settings.json b/.vscode/settings.json index 3a89c71..99d44c5 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -16,6 +16,6 @@ "stdint.h": "c" }, "rust-analyzer.cargo.features": [ - "ext_all" + "ext_all", ] } \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index ac2d797..948f7d2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -44,7 +44,7 @@ ariadne = "0.6" pyo3 = "0.27.0" once_cell = "^1" inventory = "^0.3" -serde_cbor = "=0.11.2" +zstd = "=0.13.3" borsh = "^1" criterion = "0.5" diff --git a/hycore/Cargo.toml b/hycore/Cargo.toml index 0e876df..8042539 100644 --- a/hycore/Cargo.toml +++ b/hycore/Cargo.toml @@ -4,8 +4,10 @@ version = "0.1.1" edition = "2024" [dependencies] -hyinstr = { workspace = true, features = ["serde", "chumsky"] } +hyinstr = { workspace = true, features = ["serde", "chumsky", "borsh"] } uuid = { workspace = true, features = ["v4", "serde"] } +borsh = { workspace = true, features = ["derive"] } +serde = { workspace = true, features = ["derive"] } petgraph.workspace = true smallvec.workspace = true semver.workspace = true @@ -20,18 +22,17 @@ enum-map = { workspace = true } log = { workspace = true } either.workspace = true bit-set = { workspace = true } -serde = { workspace = true, features = ["derive"] } toml.workspace = true downcast-rs.workspace = true +chrono.workspace = true +inventory.workspace = true +zstd.workspace = true pyo3 = { workspace = true, features = [ "uuid", "extension-module", "abi3", "chrono", ], optional = true } -chrono = { workspace = true } -inventory = { workspace = true } -serde_cbor.workspace = true [build-dependencies] build-info-build.workspace = true diff --git a/hycore/src/compiler.rs b/hycore/src/compiler.rs index a34f26b..aadc786 100644 --- a/hycore/src/compiler.rs +++ b/hycore/src/compiler.rs @@ -1,9 +1,9 @@ +use borsh::{BorshDeserialize, BorshSerialize}; use hyinstr::{ modules::{Module, parser::extend_module_from_string}, types::TypeRegistry, }; use log::info; -use serde::{Deserialize, Serialize}; use crate::{ base::{ @@ -14,62 +14,126 @@ use crate::{ utils::error::{HyError, HyResult}, }; -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct CompiledModuleStorageInternal { +#[derive(Debug, Clone, BorshSerialize, BorshDeserialize)] +pub struct CompiledModuleStorage { pub filenames: Vec, pub module: Module, } -impl CompiledModuleStorageInternal { - pub fn encode(&self, instance: &InstanceContext) -> HyResult> { - // Serialize inner using dlhn - let mut buf = Vec::new(); - let mut serializer = serde_cbor::Serializer::new(&mut buf); - self.serialize(&mut serializer).map_err(|e| { - hyerror!( - instance, - "Failed to serialize compiled module storage: {}", - e - ); - HyError::Unknown(format!( - "Failed to serialize compiled module storage: {}", - e - )) +impl CompiledModuleStorage { + pub const MAGIC_BYTES: [u8; 8] = *b"\x7FHYMODIR"; + + fn writer_header( + &self, + instance: &InstanceContext, + writer: &mut W, + ) -> std::io::Result<()> { + // Write magic bytes + writer.write_all(&Self::MAGIC_BYTES)?; + + // Write version requirement (using semver format) + let version_req = semver::VersionReq { + comparators: vec![semver::Comparator { + op: semver::Op::Exact, + major: instance.version.major, + minor: Some(instance.version.minor), + patch: Some(instance.version.patch), + pre: instance.version.pre.clone(), + }], + }; + let mut version_req_str = version_req.to_string(); + + // Write null-terminated version requirement string + version_req_str.push('\0'); + let version_req_bytes = version_req_str.as_bytes(); + + // Write version requirement string bytes + writer.write_all(version_req_bytes)?; + + Ok(()) + } + + fn read_header( + instance: &InstanceContext, + reader: &mut R, + ) -> std::io::Result<()> { + // Read and verify magic bytes + let mut magic = [0u8; 8]; + reader.read_exact(&mut magic)?; + if magic != Self::MAGIC_BYTES { + return Err(std::io::Error::new( + std::io::ErrorKind::InvalidData, + "Invalid magic bytes in compiled module storage", + )); + } + + // Read version requirement string until null terminator + let mut version_req_bytes = Vec::new(); + loop { + let mut byte = [0u8; 1]; + reader.read_exact(&mut byte)?; + if byte[0] == 0 { + break; + } + version_req_bytes.push(byte[0]); + } + + // Parse version requirement + let version_req_str = String::from_utf8(version_req_bytes).map_err(|e| { + std::io::Error::new( + std::io::ErrorKind::InvalidData, + format!("Invalid UTF-8 in version requirement: {}", e), + ) + })?; + let version_req = semver::VersionReq::parse(&version_req_str).map_err(|e| { + std::io::Error::new( + std::io::ErrorKind::InvalidData, + format!("Invalid version requirement format: {}", e), + ) })?; - // Secondly, wrap in CompiledModuleStorage - let storage = CompiledModuleStorage { - magic: CompiledModuleStorage::MAGIC_BYTES, - version_req: semver::VersionReq { - comparators: vec![semver::Comparator { - op: semver::Op::Exact, - major: instance.version.major, - minor: Some(instance.version.minor), - patch: Some(instance.version.patch), - pre: instance.version.pre.clone(), - }], - }, - data: buf, - }; + // Check version compatibility + if !version_req.matches(&instance.version) { + return Err(std::io::Error::new( + std::io::ErrorKind::InvalidData, + format!( + "Incompatible compiled module storage version: required {}, found {}", + version_req, instance.version + ), + )); + } + + Ok(()) + } - // Serialize the storage using serde_cbor for stability + pub fn encode(&self, instance: &InstanceContext) -> HyResult> { + // Serialize inner using borsh hytrace!( instance, - "Serializing compiled module storage wrapper with version requirement {}", - storage.version_req + "Serializing compiled module storage (module has {} functions)", + self.module.functions.len() ); let mut buf = Vec::new(); - serde_cbor::to_writer(&mut buf, &storage).map_err(|e| { - hyerror!( - instance, - "Failed to serialize compiled module storage wrapper: {}", - e - ); - HyError::Unknown(format!( - "Failed to serialize compiled module storage wrapper: {}", - e - )) - })?; + let mut writer = &mut buf; + + self.writer_header(instance, &mut writer) + .and_then(|_| { + let mut zstd_writer = zstd::stream::write::Encoder::new(writer, 3).unwrap(); + borsh::BorshSerialize::serialize(&self, &mut zstd_writer)?; + zstd_writer.finish()?; + Ok(()) + }) + .map_err(|e| { + hyerror!( + instance, + "Failed to serialize compiled module storage header: {}", + e + ); + HyError::Unknown(format!( + "Failed to serialize compiled module storage header: {}", + e + )) + })?; Ok(buf) } @@ -81,80 +145,26 @@ impl CompiledModuleStorageInternal { data.len() ); - // Deserialize the storage using serde_cbor - let storage: CompiledModuleStorage = serde_cbor::from_slice(data).map_err(|e| { - hyerror!( - instance, - "Failed to deserialize compiled module storage wrapper: {}", - e - ); - HyError::Unknown(format!( - "Failed to deserialize compiled module storage wrapper: {}", - e - )) - })?; - - // Check magic bytes - if storage.magic != CompiledModuleStorage::MAGIC_BYTES { - hyerror!(instance, "Invalid magic bytes in compiled module storage"); - return Err(HyError::Unknown( - "Invalid magic bytes in compiled module storage".to_string(), - )); - } - - // Check version compatibility - if !storage.version_req.matches(&instance.version) { - hyerror!( - instance, - "Incompatible compiled module storage version: required {}, found {}", - storage.version_req, - instance.version - ); - return Err(HyError::Unknown(format!( - "Incompatible compiled module storage version: required {}, found {}", - storage.version_req, instance.version - ))); - } - - // Deserialize inner using dlhn - let compiled_module: Self = - serde_cbor::from_slice(storage.data.as_slice()).map_err(|e| { + let mut reader = &data[..]; + Self::read_header(instance, &mut reader) + .and_then(|_| { + let mut zstd_reader = zstd::stream::read::Decoder::new(reader).unwrap(); + borsh::BorshDeserialize::deserialize_reader(&mut zstd_reader) + }) + .map_err(|e| { hyerror!( instance, - "Failed to deserialize compiled module storage: {}", + "Failed to read compiled module storage header: {}", e ); HyError::Unknown(format!( - "Failed to deserialize compiled module storage: {}", + "Failed to read compiled module storage header: {}", e )) - })?; - - Ok(compiled_module) + }) } } -/// Compiled IR module storage format. -/// -/// This is used to store compiled-module metadata alongside the serialized module data. -/// This should be kept stable across all versions of Hyperion. No modifications should be made -/// to this structure that would break compatibility with previously stored modules. -/// -/// See [`CompiledModuleStorage::MAGIC_BYTES`] for the magic bytes used to identify compiled module storage files. -/// See [`CompiledModuleStorageInternal`] for the internal representation used during (de)serialization. -/// -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct CompiledModuleStorage { - pub magic: [u8; 8], - pub version_req: semver::VersionReq, - pub data: Vec, -} - -impl CompiledModuleStorage { - /// Magic bytes used to identify compiled module storage files. - pub const MAGIC_BYTES: [u8; 8] = *b"\0HYCOMP\0"; -} - pub fn compile_sources( instance: &InstanceContext, compile_info: ModuleCompileInfo, @@ -184,7 +194,7 @@ pub fn compile_sources( } // Produce compiled module storage or further processing here - let storage = CompiledModuleStorageInternal { module, filenames }; + let storage = CompiledModuleStorage { module, filenames }; let encoded_storage = storage.encode(instance)?; // Information about the compiled module can be used here diff --git a/hyinstr/Cargo.toml b/hyinstr/Cargo.toml index f83029b..75ab871 100644 --- a/hyinstr/Cargo.toml +++ b/hyinstr/Cargo.toml @@ -33,3 +33,4 @@ serde = [ "bitflags/serde", ] chumsky = ["dep:chumsky"] +borsh = ["dep:borsh", "borsh/derive", "uuid/borsh"] diff --git a/hyinstr/src/analysis.rs b/hyinstr/src/analysis.rs index 1bed5b7..7d632ed 100644 --- a/hyinstr/src/analysis.rs +++ b/hyinstr/src/analysis.rs @@ -55,9 +55,18 @@ impl TerminationBehavior { /// an block of instructions/function during execution or simulation. /// #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, EnumIs, EnumTryAs, EnumDiscriminants)] -#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] #[strum_discriminants(name(AnalysisStatisticOp))] #[strum_discriminants(derive(EnumIter))] +#[cfg_attr(feature = "serde", strum_discriminants(derive(Serialize, Deserialize)))] +#[cfg_attr( + feature = "borsh", + strum_discriminants(derive(borsh::BorshSerialize, borsh::BorshDeserialize)) +)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum AnalysisStatistic { /// Count of instructions executed containing any of the specified flags. /// diff --git a/hyinstr/src/consts/fp.rs b/hyinstr/src/consts/fp.rs index de629c2..6337121 100644 --- a/hyinstr/src/consts/fp.rs +++ b/hyinstr/src/consts/fp.rs @@ -16,6 +16,33 @@ pub struct FConst { pub value: BigDecimal, } +#[cfg(feature = "borsh")] +impl borsh::BorshSerialize for FConst { + fn serialize(&self, writer: &mut W) -> std::io::Result<()> { + use crate::consts::int::serialize_bigint_borsh; + + borsh::BorshSerialize::serialize(&self.ty, writer)?; + let (bigint, exponent) = self.value.as_bigint_and_scale(); + serialize_bigint_borsh(&bigint, writer)?; + borsh::BorshSerialize::serialize(&exponent, writer)?; + + Ok(()) + } +} + +#[cfg(feature = "borsh")] +impl borsh::BorshDeserialize for FConst { + fn deserialize_reader(reader: &mut R) -> std::io::Result { + use crate::consts::int::deserialize_bigint_borsh; + + let ty = borsh::BorshDeserialize::deserialize_reader(reader)?; + let bigint = deserialize_bigint_borsh(reader)?; + let exponent = borsh::BorshDeserialize::deserialize_reader(reader)?; + let value = BigDecimal::new(bigint, exponent); + Ok(Self { ty, value }) + } +} + impl FConst { /// Create a new `FConst` from its type and value. pub fn new(ty: FType, value: BigDecimal) -> Self { diff --git a/hyinstr/src/consts/int.rs b/hyinstr/src/consts/int.rs index 4e1ecf3..a2f166b 100644 --- a/hyinstr/src/consts/int.rs +++ b/hyinstr/src/consts/int.rs @@ -15,6 +15,41 @@ pub struct IConst { pub value: BigInt, } +/// Serialize a [`BigInt`] using Borsh +#[cfg(feature = "borsh")] +pub fn serialize_bigint_borsh( + value: &BigInt, + writer: &mut W, +) -> std::io::Result<()> { + let bytes = value.to_signed_bytes_le(); + borsh::BorshSerialize::serialize(&bytes, writer) +} + +/// Deserialize a [`BigInt`] using Borsh +#[cfg(feature = "borsh")] +pub fn deserialize_bigint_borsh(reader: &mut R) -> std::io::Result { + let bytes: Vec = borsh::BorshDeserialize::deserialize_reader(reader)?; + Ok(BigInt::from_signed_bytes_le(&bytes)) +} + +#[cfg(feature = "borsh")] +impl borsh::BorshSerialize for IConst { + fn serialize(&self, writer: &mut W) -> std::io::Result<()> { + borsh::BorshSerialize::serialize(&self.ty, writer)?; + serialize_bigint_borsh(&self.value, writer)?; + Ok(()) + } +} + +#[cfg(feature = "borsh")] +impl borsh::BorshDeserialize for IConst { + fn deserialize_reader(reader: &mut R) -> std::io::Result { + let ty = borsh::BorshDeserialize::deserialize_reader(reader)?; + let value = deserialize_bigint_borsh(reader)?; + Ok(Self { ty, value }) + } +} + impl std::fmt::Display for IConst { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "{} {}", self.ty, self.value) diff --git a/hyinstr/src/consts/mod.rs b/hyinstr/src/consts/mod.rs index d528e41..fa63d2a 100644 --- a/hyinstr/src/consts/mod.rs +++ b/hyinstr/src/consts/mod.rs @@ -17,6 +17,10 @@ pub mod int; /// A constant value (integer or floating‑point) usable as an immediate. #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, EnumIs, EnumTryAs)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum AnyConst { /// Integer constant Int(IConst), diff --git a/hyinstr/src/modules/instructions/fp.rs b/hyinstr/src/modules/instructions/fp.rs index 4d88cd2..2ca54f4 100644 --- a/hyinstr/src/modules/instructions/fp.rs +++ b/hyinstr/src/modules/instructions/fp.rs @@ -18,6 +18,10 @@ use crate::{ /// Floating-point comparison operations #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum FCmpVariant { /// Ordered and equal (i.e., neither operand is NaN and lhs == rhs) Oeq, @@ -76,6 +80,10 @@ impl FCmpVariant { /// Floating-point addition instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct FAdd { /// Destination SSA name receiving the sum. pub dest: Name, @@ -120,6 +128,10 @@ impl Instruction for FAdd { /// Floating-point subtraction instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct FSub { /// Destination SSA name receiving the difference. pub dest: Name, @@ -164,6 +176,10 @@ impl Instruction for FSub { /// Floating-point multiplication instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct FMul { /// Destination SSA name receiving the product. pub dest: Name, @@ -208,6 +224,10 @@ impl Instruction for FMul { /// Floating-point division instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct FDiv { /// Destination SSA name receiving the quotient. pub dest: Name, @@ -252,6 +272,10 @@ impl Instruction for FDiv { /// Floating-point remainder instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct FRem { /// Destination SSA name receiving the remainder. pub dest: Name, @@ -296,6 +320,10 @@ impl Instruction for FRem { /// Floating-point negation instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct FNeg { /// Destination SSA name receiving the negated value. pub dest: Name, @@ -338,6 +366,10 @@ impl Instruction for FNeg { /// Floating-point comparison instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct FCmp { /// Destination SSA name receiving the comparison result. pub dest: Name, diff --git a/hyinstr/src/modules/instructions/int.rs b/hyinstr/src/modules/instructions/int.rs index dc8afa8..ebfff0b 100644 --- a/hyinstr/src/modules/instructions/int.rs +++ b/hyinstr/src/modules/instructions/int.rs @@ -19,6 +19,10 @@ use crate::{ /// Overflow policies for integer operations #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum OverflowPolicy { /// Wrap around on overflow Wrap, @@ -32,6 +36,10 @@ pub enum OverflowPolicy { /// Additional signedness policy for overflow handling #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum OverflowSignednessPolicy { /// Wrap (signedness does not matter for wrap) Wrap, @@ -83,6 +91,10 @@ impl OverflowSignednessPolicy { /// Signedness for integer operations #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum IntegerSignedness { Signed, Unsigned, @@ -106,6 +118,10 @@ impl IntegerSignedness { /// Integer comparison operations #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum ICmpVariant { /// Equal Eq, @@ -181,6 +197,10 @@ impl ICmpVariant { /// Integer shift operations disambiguation #[derive(Debug, Clone, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum IShiftVariant { /// Logical left shift Lsl, @@ -215,6 +235,10 @@ impl IShiftVariant { /// Integer addition instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IAdd { /// Destination SSA name receiving the sum. pub dest: Name, @@ -261,6 +285,10 @@ impl Instruction for IAdd { /// Integer substraction instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct ISub { /// Destination SSA name receiving the difference. pub dest: Name, @@ -307,6 +335,10 @@ impl Instruction for ISub { /// Integer multiplication instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IMul { /// Destination SSA name receiving the product. pub dest: Name, @@ -353,6 +385,10 @@ impl Instruction for IMul { /// Integer division instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IDiv { /// Destination SSA name receiving the quotient. pub dest: Name, @@ -399,6 +435,10 @@ impl Instruction for IDiv { /// Integer remainder instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IRem { /// Destination SSA name receiving the remainder. pub dest: Name, @@ -445,6 +485,10 @@ impl Instruction for IRem { /// Integer comparison instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct ICmp { /// Destination SSA name receiving the predicate result. pub dest: Name, @@ -493,6 +537,10 @@ impl Instruction for ICmp { /// Integer shift instruction #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct ISht { /// Destination SSA name receiving the shifted value. pub dest: Name, @@ -540,6 +588,10 @@ impl Instruction for ISht { /// (Negates the value of the operand) #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct INeg { /// Destination SSA name receiving the negated value. pub dest: Name, @@ -583,6 +635,10 @@ impl Instruction for INeg { /// (Flips all bits of the operand) #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct INot { /// Destination SSA name receiving the inverted value. pub dest: Name, @@ -625,6 +681,10 @@ impl Instruction for INot { /// Integer AND instruction (bitwise AND, logical is equivalent when working on type i1) #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IAnd { /// Destination SSA name receiving the bitwise conjunction. pub dest: Name, @@ -669,6 +729,10 @@ impl Instruction for IAnd { /// Integer OR instruction (bitwise OR, logical is equivalent when working on type i1) #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IOr { /// Destination SSA name receiving the bitwise disjunction. pub dest: Name, @@ -713,6 +777,10 @@ impl Instruction for IOr { /// Integer XOR instruction (bitwise XOR, logical is equivalent when working on type i1) #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IXor { /// Destination SSA name receiving the bitwise exclusive-or. pub dest: Name, @@ -757,6 +825,10 @@ impl Instruction for IXor { /// Implies instruction (logical implication, works on type i1) #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IImplies { /// Destination SSA name receiving the implication result. pub dest: Name, @@ -801,6 +873,10 @@ impl Instruction for IImplies { /// Equivalence instruction (logical equivalence, works on type i1) #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct IEquiv { /// Destination SSA name receiving the equivalence result. pub dest: Name, diff --git a/hyinstr/src/modules/instructions/mem.rs b/hyinstr/src/modules/instructions/mem.rs index 4c04b23..dac0285 100644 --- a/hyinstr/src/modules/instructions/mem.rs +++ b/hyinstr/src/modules/instructions/mem.rs @@ -26,6 +26,10 @@ use crate::{ /// You can also check LLVM's documentation on [Ordering](https://llvm.org/docs/LangRef.html#atomic-memory-ordering) for more details. #[derive(Debug, Clone, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum MemoryOrdering { Unordered, Monotonic, @@ -61,6 +65,10 @@ impl MemoryOrdering { /// is specified, the load is considered atomic with the given ordering. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MLoad { /// Destination SSA name receiving the loaded value. pub dest: Name, @@ -118,6 +126,10 @@ impl Instruction for MLoad { /// is specified, the store is considered atomic with the given ordering. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MStore { /// Pointer operand describing the destination address. pub addr: Operand, @@ -167,6 +179,10 @@ impl Instruction for MStore { /// on the stack and let the optimizer handle promoting to registers if possible. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MAlloca { /// Destination SSA name receiving the pointer to the allocated storage. pub dest: Name, @@ -214,6 +230,10 @@ impl Instruction for MAlloca { /// instruction can also be used to calculate a vector of such addresses #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MGetElementPtr { /// Destination SSA name receiving the computed address. pub dest: Name, diff --git a/hyinstr/src/modules/instructions/meta.rs b/hyinstr/src/modules/instructions/meta.rs index e1b4533..bfdfe6b 100644 --- a/hyinstr/src/modules/instructions/meta.rs +++ b/hyinstr/src/modules/instructions/meta.rs @@ -23,6 +23,10 @@ use strum::{EnumDiscriminants, EnumIs, EnumIter, EnumTryAs, IntoEnumIterator}; /// be provided by the derivation engine or external tools. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MetaAssert { /// The condition to assert. This should evaluate to a boolean value. pub condition: Operand, @@ -80,6 +84,10 @@ impl Instruction for MetaAssert { /// while `assert %cond` signifies that ∵ `%cond` is true. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MetaAssume { /// The condition to assume. This should evaluate to a boolean value. pub condition: Operand, @@ -128,6 +136,10 @@ impl Instruction for MetaAssume { /// Check whether an operand is fully defined (no undef/poison content). #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MetaIsDef { /// Destination SSA name holding the boolean result. pub dest: Name, @@ -189,6 +201,10 @@ impl Instruction for MetaIsDef { #[strum_discriminants(name(MetaProbVariant))] #[strum_discriminants(derive(EnumIter))] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum MetaProbOperand { /// Operand (boolean) value, this is the probability that the given operand is true. Input /// should be a boolean value. @@ -244,6 +260,10 @@ impl MetaProbVariant { /// for modeling and reasoning about probabilistic computations. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MetaProb { /// The destination SSA name for the result of the probability function. pub dest: Name, @@ -303,6 +323,10 @@ impl Instruction for MetaProb { /// #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MetaAnalysisStat { /// The destination SSA name for the result of the analysis statistic instruction. pub dest: Name, diff --git a/hyinstr/src/modules/instructions/misc.rs b/hyinstr/src/modules/instructions/misc.rs index f9f05f6..2115391 100644 --- a/hyinstr/src/modules/instructions/misc.rs +++ b/hyinstr/src/modules/instructions/misc.rs @@ -20,6 +20,10 @@ use strum::{EnumIter, IntoEnumIterator}; /// a return code or never return from the function (e.g., abort). #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Invoke { /// Should be a reference to a function pointer (either internal or external). We /// describe it as an `Operand` to allow dynamic function calls to achieve virtualization @@ -80,6 +84,10 @@ impl Instruction for Invoke { /// beginning of a basic block. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Phi { /// The destination SSA name for the result of the phi instruction. pub dest: Name, @@ -126,6 +134,10 @@ impl Instruction for Phi { /// This instruction selects one of two values based on a condition. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Select { /// The destination SSA name for the result of the select instruction. pub dest: Name, @@ -179,6 +191,10 @@ impl Instruction for Select { /// details. #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum CastVariant { /// Truncate integer /// @@ -275,6 +291,10 @@ impl CastVariant { /// This instruction casts a value from one type to another using the specified cast operation. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Cast { /// The destination SSA name for the casted result. pub dest: Name, @@ -325,6 +345,10 @@ impl Instruction for Cast { /// This is purely a value transform; no memory is touched. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct InsertValue { /// Destination SSA name receiving the updated aggregate. pub dest: Name, @@ -375,6 +399,10 @@ impl Instruction for InsertValue { /// all indices must be constant integers. This is a pure value operation (no memory access). #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct ExtractValue { /// Destination SSA name receiving the extracted element. pub dest: Name, diff --git a/hyinstr/src/modules/instructions/mod.rs b/hyinstr/src/modules/instructions/mod.rs index 3acef69..d820e79 100644 --- a/hyinstr/src/modules/instructions/mod.rs +++ b/hyinstr/src/modules/instructions/mod.rs @@ -78,6 +78,21 @@ bitflags! { } } +#[cfg(feature = "borsh")] +impl borsh::BorshSerialize for InstructionFlags { + fn serialize(&self, writer: &mut W) -> std::io::Result<()> { + borsh::BorshSerialize::serialize(&self.bits(), writer) + } +} + +#[cfg(feature = "borsh")] +impl borsh::BorshDeserialize for InstructionFlags { + fn deserialize_reader(reader: &mut R) -> std::io::Result { + let bits = borsh::BorshDeserialize::deserialize_reader(reader)?; + Ok(InstructionFlags::from_bits_truncate(bits)) + } +} + /// Common interface implemented by every instruction node. /// /// This trait provides lightweight, zero‑allocation iteration over an @@ -158,6 +173,10 @@ pub trait Instruction { #[derive(Debug, Clone, Hash, PartialEq, Eq, EnumIs, EnumTryAs, EnumDiscriminants)] #[strum_discriminants(name(HyInstrOp), derive(EnumIter))] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum HyInstr { // Integer instructions IAdd(int::IAdd), diff --git a/hyinstr/src/modules/mod.rs b/hyinstr/src/modules/mod.rs index 84ae43f..3f354ed 100644 --- a/hyinstr/src/modules/mod.rs +++ b/hyinstr/src/modules/mod.rs @@ -44,6 +44,10 @@ pub mod terminator; /// All Global Variables and Functions have one of the following types of linkage: #[derive(Debug, Default, Clone, Copy, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum Linkage { /// Global values with `Linkage::private` linkage are only directly accessible by objects in the current module. /// @@ -70,6 +74,10 @@ pub enum Linkage { /// Note: A symbol with internal or private linkage must have default visibility. #[derive(Debug, Default, Clone, Copy, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum Visibility { /// Default visibility /// @@ -114,6 +122,10 @@ impl Visibility { /// and more may be added in the future: #[derive(Debug, Default, Clone, Copy, Hash, PartialEq, Eq, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum CallingConvention { /// The C calling convention /// @@ -261,6 +273,10 @@ impl CallingConvention { /// This structure identifies an instruction by the basic block label it resides in /// and the index of the instruction within that block. #[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct InstructionRef { /// Label of the basic block containing the instruction. pub block: Label, @@ -291,6 +307,10 @@ impl From for (Label, usize) { /// of complex control flow within functions. #[derive(Debug, Clone, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct BasicBlock { /// Unique block label. pub label: Label, @@ -334,6 +354,10 @@ impl BasicBlock { /// #[derive(Debug, Clone, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Function { /// The unique identifier (UUID) of the function. pub uuid: Uuid, @@ -818,6 +842,10 @@ pub struct FunctionAnalysisContext<'a> { /// defined locally are listed in `external_functions`. #[derive(Debug, Default, Clone, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Module { /// Defined functions keyed by their UUID. pub functions: BTreeMap, diff --git a/hyinstr/src/modules/operand.rs b/hyinstr/src/modules/operand.rs index 1cb181b..780b5db 100644 --- a/hyinstr/src/modules/operand.rs +++ b/hyinstr/src/modules/operand.rs @@ -15,6 +15,10 @@ use strum::{EnumIs, EnumTryAs}; /// instruction's result. #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Name(pub u32); impl std::ops::Add for Name { @@ -46,6 +50,10 @@ impl Debug for Name { /// Represents a meta operand used internally in attributes and properties. #[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct MetaLabel(pub u32); /// Represents a code label used as a target for control‑flow instructions (besides invokes). @@ -54,6 +62,10 @@ pub struct MetaLabel(pub u32); /// labels are only valid within the function they are defined in. #[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Label(pub u32); impl Label { @@ -70,6 +82,10 @@ impl Label { /// Instruction operand. #[derive(Clone, Debug, PartialEq, Eq, Hash, EnumIs, EnumTryAs)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum Operand { /// Reference to a previously defined SSA value. Reg(Name), diff --git a/hyinstr/src/modules/symbol.rs b/hyinstr/src/modules/symbol.rs index 11b0c33..02d093f 100644 --- a/hyinstr/src/modules/symbol.rs +++ b/hyinstr/src/modules/symbol.rs @@ -16,6 +16,10 @@ use crate::{modules::CallingConvention, types::Typeref}; /// This struct represents a function that is defined outside the current module, #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct ExternalFunction { /// Unique identifier for the external function. This is used internally to /// reference the function within the module. @@ -41,6 +45,10 @@ pub struct ExternalFunction { #[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord, EnumDiscriminants)] #[strum_discriminants(name(FunctionPointerType))] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum FunctionPointer { /// Reference to a function defined within the current module Internal(Uuid), diff --git a/hyinstr/src/modules/terminator.rs b/hyinstr/src/modules/terminator.rs index 8e7c21f..22dc938 100644 --- a/hyinstr/src/modules/terminator.rs +++ b/hyinstr/src/modules/terminator.rs @@ -30,6 +30,10 @@ pub trait Terminator: Instruction { /// See `Label` in `operand.rs` for more information about code labels. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Branch { /// The condition operand; should evaluate to a boolean value. /// @@ -83,6 +87,10 @@ impl Terminator for Branch { /// See `Label` in `operand.rs` for more information about code labels. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Jump { /// The label to jump to. pub target: Label, @@ -125,6 +133,10 @@ impl Terminator for Jump { /// If `value` is `None`, it indicates a `void` return. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Ret { pub value: Option, } @@ -164,6 +176,10 @@ impl Terminator for Ret { /// Trap instruction to indicate an unrecoverable error or exceptional condition. #[derive(Debug, Clone, Hash, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Trap; impl Instruction for Trap { @@ -203,7 +219,15 @@ impl Terminator for Trap { #[strum_discriminants(name(HyTerminatorOp))] #[strum_discriminants(derive(EnumIter))] #[cfg_attr(feature = "serde", strum_discriminants(derive(Serialize, Deserialize)))] +#[cfg_attr( + feature = "borsh", + strum_discriminants(derive(borsh::BorshSerialize, borsh::BorshDeserialize)) +)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum HyTerminator { Branch(Branch), Jump(Jump), diff --git a/hyinstr/src/types/mod.rs b/hyinstr/src/types/mod.rs index a620862..056a179 100644 --- a/hyinstr/src/types/mod.rs +++ b/hyinstr/src/types/mod.rs @@ -35,6 +35,10 @@ pub mod primary; /// A stable reference to a type stored inside a `TypeRegistry`. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct Typeref(Uuid); impl Typeref { diff --git a/hyinstr/src/types/primary.rs b/hyinstr/src/types/primary.rs index 5d19ce5..6a3f237 100644 --- a/hyinstr/src/types/primary.rs +++ b/hyinstr/src/types/primary.rs @@ -28,6 +28,10 @@ use uuid::Uuid; /// #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] #[repr(transparent)] pub struct IType { num_bits: u32, @@ -120,6 +124,10 @@ impl std::fmt::Display for IType { /// formats. Not all floating-point types may be supported on all targets. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, EnumIter)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub enum FType { /// 16-bit floating point value (IEEE-754 binary16) /// Also known as "half precision". @@ -239,6 +247,10 @@ impl std::fmt::Display for ExtType { /// to coexist in the same function or module. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] pub struct WType { /// Ordinal identifier used to distinguish wildcard placeholders. pub id: u16, From b3229a500ac97bdcc7ae2c3f2c9dc91021d40a9b Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Sun, 18 Jan 2026 16:35:08 +0100 Subject: [PATCH 03/56] Refactor plugin registration macros and add formal verification module --- hycore/src/ext/hylog/impl.rs | 4 +- hycore/src/ext/mod.rs | 2 +- hycore/src/formal/mod.rs | 93 ++++++++++++++++++++++++++++++++++++ hycore/src/lib.rs | 12 ++++- hycore/src/provers/mod.rs | 3 -- hycore/src/utils/error.rs | 3 ++ 6 files changed, 110 insertions(+), 7 deletions(-) create mode 100644 hycore/src/formal/mod.rs delete mode 100644 hycore/src/provers/mod.rs diff --git a/hycore/src/ext/hylog/impl.rs b/hycore/src/ext/hylog/impl.rs index 6bfb947..fef535b 100644 --- a/hycore/src/ext/hylog/impl.rs +++ b/hycore/src/ext/hylog/impl.rs @@ -1,11 +1,11 @@ use crate::{ base::InstanceContext, - define_plugin, ext::{ PluginEXT, StaticPluginEXT, hylog::{LogCallbackEXT, LogCreateInfoEXT, LogLevelEXT, LogMessageEXT}, }, magic::{HYPERION_LOGGER_NAME_EXT, HYPERION_LOGGER_UUID_EXT}, + register, utils::{error::HyResult, opaque::OpaqueList}, }; use std::sync::Weak; @@ -18,7 +18,7 @@ pub struct LogPluginEXT { callback: Option, min_level: LogLevelEXT, } -define_plugin!(LogPluginEXT); +register!(plugin LogPluginEXT); impl StaticPluginEXT for LogPluginEXT { const UUID: Uuid = HYPERION_LOGGER_UUID_EXT; diff --git a/hycore/src/ext/mod.rs b/hycore/src/ext/mod.rs index 7a764fc..c246fc0 100644 --- a/hycore/src/ext/mod.rs +++ b/hycore/src/ext/mod.rs @@ -41,7 +41,7 @@ inventory::collect!(PluginRegistry); /// Macro to define and register a Hyperion plugin. #[macro_export] -macro_rules! define_plugin { +macro_rules! register_plugin { ( $plugin:ty ) => { diff --git a/hycore/src/formal/mod.rs b/hycore/src/formal/mod.rs new file mode 100644 index 0000000..fb2927a --- /dev/null +++ b/hycore/src/formal/mod.rs @@ -0,0 +1,93 @@ +//! Entry point for formal verification functionalities. + +use std::{collections::BTreeMap, sync::Weak}; + +use uuid::Uuid; + +use crate::{ + base::InstanceContext, + utils::error::{HyError, HyResult}, +}; + +/// Base trait for dynamic theorem inference strategies. Should not be +/// implemented directly, instead prefer implementing [`TheoremInferenceStrategy`]. +pub trait DynTheoremInferenceStrategyBase: Send + Sync { + // Returns the unique identifier for the theorem inference strategy. + fn uuid(&self) -> Uuid; +} + +pub trait DynTheoremInferenceStrategy: DynTheoremInferenceStrategyBase { + fn derive(&self); +} + +/// Static, non-dynamic trait for theorem inference strategies. +pub trait TheoremInferenceStrategy: Sized + Send + Sync { + /// Unique identifier for the theorem inference strategy. + const UUID: Uuid; + + /// Constructs a new instance of the theorem inference strategy. + fn new(instance: Weak) -> HyResult; +} + +impl DynTheoremInferenceStrategyBase for T { + fn uuid(&self) -> Uuid { + ::UUID + } +} + +/// Inventory containing theorem inference strategy registrations. +pub struct TheoremInferenceStrategyRegistry { + pub uuid: Uuid, + pub loader: fn(Weak) -> HyResult>, +} +inventory::collect!(TheoremInferenceStrategyRegistry); + +#[macro_export] +macro_rules! register_theorem_inference_strategy { + ( + $strategy:ty + ) => { + $crate::inventory::submit! { + $crate::formal::TheoremInferenceStrategyRegistry { + uuid: <$strategy as $crate::formal::TheoremInferenceStrategy>::UUID, + loader: |instance: std::sync::Weak<$crate::base::InstanceContext>| -> $crate::utils::error::HyResult> { + let strategy = <$strategy as $crate::formal::TheoremInferenceStrategy>::new(instance)?; + Ok(Box::new(strategy)) + }, + } + } + }; + () => {}; +} + +/// Library managing registered theorem inference strategies. +pub struct TheoremInferenceStrategyLibrary { + strategies: BTreeMap>, +} + +impl TheoremInferenceStrategyLibrary { + /// Adds a new theorem inference strategy to the library by its UUID. + pub fn add_strategy_by_uuid( + &mut self, + uuid: Uuid, + instance: Weak, + ) -> HyResult<()> { + for registry in inventory::iter:: { + if registry.uuid == uuid { + let strategy = (registry.loader)(instance)?; + self.strategies.insert(uuid, strategy); + return Ok(()); + } + } + + Err(HyError::KeyNotFound { + key: uuid.to_string(), + context: "theorem inference strategy".to_string(), + }) + } + + /// Retrieves a reference to a registered theorem inference strategy by its UUID. + pub fn get_strategy(&self, uuid: &Uuid) -> Option<&Box> { + self.strategies.get(uuid) + } +} diff --git a/hycore/src/lib.rs b/hycore/src/lib.rs index f53b489..1319458 100644 --- a/hycore/src/lib.rs +++ b/hycore/src/lib.rs @@ -8,10 +8,20 @@ pub mod base; pub mod compiler; pub mod ext; +pub mod formal; pub mod magic; -pub mod provers; pub mod specifications; pub mod utils; pub extern crate chrono; pub extern crate inventory; + +#[macro_export] +macro_rules! register { + (plugin $ty:ty) => { + crate::register_plugin!($ty); + }; + (theorem_inference_strategy $ty:ty) => { + $crate::register_theorem_inference_strategy!($ty); + }; +} diff --git a/hycore/src/provers/mod.rs b/hycore/src/provers/mod.rs deleted file mode 100644 index b6ed8e8..0000000 --- a/hycore/src/provers/mod.rs +++ /dev/null @@ -1,3 +0,0 @@ -//! Entry point for future theorem-prover integrations. -//! -//! The module intentionally stays empty until solver backends are stabilized. diff --git a/hycore/src/utils/error.rs b/hycore/src/utils/error.rs index 9b50e20..a876c70 100644 --- a/hycore/src/utils/error.rs +++ b/hycore/src/utils/error.rs @@ -27,6 +27,9 @@ pub enum HyError { #[error("{0}")] HyInstrError(#[from] hyinstr::utils::Error), + + #[error("Failed to find {context} with key '{key}'")] + KeyNotFound { key: String, context: String }, } /// Convenience alias for fallible operations returning [`HyError`]. From 193ea6b20aeca150f9cd25bfbb63f9db211a29db Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Sun, 18 Jan 2026 16:39:33 +0100 Subject: [PATCH 04/56] Rename specification -> theorems for consistency --- examples/hycore-examples/src/main.rs | 2 +- hycore/src/base/module.rs | 4 +- hycore/src/lib.rs | 2 +- hycore/src/specifications/library.rs | 43 ------------------- .../src/{specifications => theorems}/base.rs | 24 +++++------ hycore/src/theorems/library.rs | 43 +++++++++++++++++++ .../src/{specifications => theorems}/mod.rs | 2 +- .../src/{specifications => theorems}/utils.rs | 2 +- 8 files changed, 61 insertions(+), 61 deletions(-) delete mode 100644 hycore/src/specifications/library.rs rename hycore/src/{specifications => theorems}/base.rs (84%) create mode 100644 hycore/src/theorems/library.rs rename hycore/src/{specifications => theorems}/mod.rs (86%) rename hycore/src/{specifications => theorems}/utils.rs (98%) diff --git a/examples/hycore-examples/src/main.rs b/examples/hycore-examples/src/main.rs index 0d685aa..ebb4c02 100644 --- a/examples/hycore-examples/src/main.rs +++ b/examples/hycore-examples/src/main.rs @@ -1,4 +1,4 @@ -use hycore::specifications::utils::{remove_unused_op, simple_simplify_function}; +use hycore::theorems::utils::{remove_unused_op, simple_simplify_function}; use hyinstr::{ modules::{Module, parser::extend_module_from_string}, types::TypeRegistry, diff --git a/hycore/src/base/module.rs b/hycore/src/base/module.rs index e2b160e..2d798b7 100644 --- a/hycore/src/base/module.rs +++ b/hycore/src/base/module.rs @@ -7,7 +7,7 @@ use hyinstr::modules::{ use petgraph::prelude::DiGraphMap; use uuid::Uuid; -use crate::specifications::library::SpecificationLibrary; +use crate::theorems::library::TheoremLibrary; /// Contextual information about a [`Function`] within a module. pub struct FunctionContext { @@ -32,5 +32,5 @@ pub struct ModuleContext { /// Library of properties and specifications (can be used to derive additional /// specifications). - pub library: SpecificationLibrary, + pub library: TheoremLibrary, } diff --git a/hycore/src/lib.rs b/hycore/src/lib.rs index 1319458..c2df146 100644 --- a/hycore/src/lib.rs +++ b/hycore/src/lib.rs @@ -10,7 +10,7 @@ pub mod compiler; pub mod ext; pub mod formal; pub mod magic; -pub mod specifications; +pub mod theorems; pub mod utils; pub extern crate chrono; diff --git a/hycore/src/specifications/library.rs b/hycore/src/specifications/library.rs deleted file mode 100644 index 90ad50e..0000000 --- a/hycore/src/specifications/library.rs +++ /dev/null @@ -1,43 +0,0 @@ -use std::collections::BTreeMap; - -use uuid::Uuid; - -use crate::specifications::base::Specification; - -/// A library for managing multiple [`Specification`]s. -#[derive(Default)] -pub struct SpecificationLibrary { - specifications: BTreeMap, -} - -impl SpecificationLibrary { - /// Creates a new, empty [`SpecificationLibrary`]. - pub fn new() -> Self { - Self::default() - } - - /// Inserts a new [`Specification`] into the library. - pub fn insert(&mut self, spec: Specification) { - self.specifications.insert(spec.uuid(), spec); - } - - /// Retrieves a reference to a [`Specification`] by its UUID. - pub fn get(&self, uuid: &Uuid) -> Option<&Specification> { - self.specifications.get(uuid) - } - - /// Retrieves a mutable reference to a [`Specification`] by its UUID. - pub fn get_mut(&mut self, uuid: &Uuid) -> Option<&mut Specification> { - self.specifications.get_mut(uuid) - } - - /// Removes a [`Specification`] from the library by its UUID. - pub fn remove(&mut self, uuid: &Uuid) -> Option { - self.specifications.remove(uuid) - } - - /// Returns an iterator over all [`Specification`]s in the library. - pub fn iter(&self) -> impl Iterator { - self.specifications.values() - } -} diff --git a/hycore/src/specifications/base.rs b/hycore/src/theorems/base.rs similarity index 84% rename from hycore/src/specifications/base.rs rename to hycore/src/theorems/base.rs index ca4afaa..0efab26 100644 --- a/hycore/src/specifications/base.rs +++ b/hycore/src/theorems/base.rs @@ -8,7 +8,7 @@ use uuid::Uuid; use crate::utils::lazy::{LazyContainer, LazyDirtifierGuard, LazyGuard}; -struct SpecificationAccelerationStructures { +struct TheoremAccelerationStructures { /// Collected references to all assert-style meta-instructions found in `function`. list_asserts: Vec, @@ -19,21 +19,21 @@ struct SpecificationAccelerationStructures { list_referenced_functions: BTreeSet, } -impl SpecificationAccelerationStructures { - /// Scan the specification function and update [`Specification::list_asserts`] with all +impl TheoremAccelerationStructures { + /// Scan the theorems function and update [`Theorem::list_asserts`] with all /// instructions that represent meta-assertions. fn derive_meta_asserts(&mut self, func: &Function) { self.list_asserts = func.gather_instructions_by_predicate(|instr| instr.is_meta_assert()); } - /// Scan the specification function and update [`Specification::list_assumptions`] with all + /// Scan the theorems function and update [`Theorem::list_assumptions`] with all /// instructions that represent meta-assumptions (preconditions). fn derive_meta_assumptions(&mut self, func: &Function) { self.list_assumptions = func.gather_instructions_by_predicate(|instr| instr.is_meta_assume()); } - /// Scan the function body and populate [`Specification::list_referenced_functions`] with every + /// Scan the function body and populate [`Theorem::list_referenced_functions`] with every /// directly referenced function pointer. fn derive_referenced_functions(&mut self, func: &Function) { self.list_referenced_functions = func @@ -76,7 +76,7 @@ impl SpecificationAccelerationStructures { } } -/// Specification are a set of external properties attached to functions, expressed as meta-functions. +/// Theorems are a set of external properties attached to functions, expressed as meta-functions. /// /// These meta-functions can contain meta-instructions such as assertions and assumptions, /// which can be used by provers to verify that the target function adheres to its specification. @@ -84,7 +84,7 @@ impl SpecificationAccelerationStructures { /// They are external as they do not provide information about the internal workings of the function, /// only about its external state and behavior. /// -pub struct Specification { +pub struct Theorem { /// Uuid (should stay static after creation) uuid: Uuid, @@ -92,10 +92,10 @@ pub struct Specification { function: Function, /// Acceleration structures derived from the specification function. - acceleration: LazyContainer, + acceleration: LazyContainer, } -impl Specification { +impl Theorem { /// Unique identifier associated with both the specification and the backing meta-function. pub fn uuid(&self) -> Uuid { debug_assert!(self.uuid == self.function.uuid); @@ -126,7 +126,7 @@ impl Specification { // pub fn list_asserts(&self) -> &[InstructionRef] {} pub fn list_asserts(&self) -> LazyGuard<'_, [InstructionRef]> { self.acceleration.get( - |x| SpecificationAccelerationStructures::compute(x, &self.function), + |x| TheoremAccelerationStructures::compute(x, &self.function), |x| x.list_asserts.as_slice(), ) } @@ -134,7 +134,7 @@ impl Specification { /// Get a reference to the list of meta-assumption instructions pub fn list_assumptions(&self) -> LazyGuard<'_, [InstructionRef]> { self.acceleration.get( - |x| SpecificationAccelerationStructures::compute(x, &self.function), + |x| TheoremAccelerationStructures::compute(x, &self.function), |x| x.list_assumptions.as_slice(), ) } @@ -142,7 +142,7 @@ impl Specification { /// Get a reference to the set of directly referenced function pointers. pub fn list_referenced_functions(&self) -> LazyGuard<'_, BTreeSet> { self.acceleration.get( - |x| SpecificationAccelerationStructures::compute(x, &self.function), + |x| TheoremAccelerationStructures::compute(x, &self.function), |x| &x.list_referenced_functions, ) } diff --git a/hycore/src/theorems/library.rs b/hycore/src/theorems/library.rs new file mode 100644 index 0000000..a6291ac --- /dev/null +++ b/hycore/src/theorems/library.rs @@ -0,0 +1,43 @@ +use std::collections::BTreeMap; + +use uuid::Uuid; + +use crate::theorems::base::Theorem; + +/// A library for managing multiple [`Theorem`]s. +#[derive(Default)] +pub struct TheoremLibrary { + specifications: BTreeMap, +} + +impl TheoremLibrary { + /// Creates a new, empty [`TheoremLibrary`]. + pub fn new() -> Self { + Self::default() + } + + /// Inserts a new [`Theorem`] into the library. + pub fn insert(&mut self, spec: Theorem) { + self.specifications.insert(spec.uuid(), spec); + } + + /// Retrieves a reference to a [`Theorem`] by its UUID. + pub fn get(&self, uuid: &Uuid) -> Option<&Theorem> { + self.specifications.get(uuid) + } + + /// Retrieves a mutable reference to a [`Theorem`] by its UUID. + pub fn get_mut(&mut self, uuid: &Uuid) -> Option<&mut Theorem> { + self.specifications.get_mut(uuid) + } + + /// Removes a [`Theorem`] from the library by its UUID. + pub fn remove(&mut self, uuid: &Uuid) -> Option { + self.specifications.remove(uuid) + } + + /// Returns an iterator over all [`Theorem`]s in the library. + pub fn iter(&self) -> impl Iterator { + self.specifications.values() + } +} diff --git a/hycore/src/specifications/mod.rs b/hycore/src/theorems/mod.rs similarity index 86% rename from hycore/src/specifications/mod.rs rename to hycore/src/theorems/mod.rs index 4b79aa4..ceaf16a 100644 --- a/hycore/src/specifications/mod.rs +++ b/hycore/src/theorems/mod.rs @@ -1,4 +1,4 @@ -//! Utilities for describing, storing, and manipulating Hyperion specifications. +//! Utilities for describing, storing, and manipulating Hyperion theorem. pub mod base; pub mod library; diff --git a/hycore/src/specifications/utils.rs b/hycore/src/theorems/utils.rs similarity index 98% rename from hycore/src/specifications/utils.rs rename to hycore/src/theorems/utils.rs index eb68a1c..faa7c2c 100644 --- a/hycore/src/specifications/utils.rs +++ b/hycore/src/theorems/utils.rs @@ -1,4 +1,4 @@ -//! Lightweight optimization passes shared by specification tooling and provers. +//! Lightweight optimization passes shared by theorems tooling and provers. use std::collections::HashMap; From 3c6ad0d3231997642eb51214d4f964bab8cc3e60 Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Sun, 18 Jan 2026 17:09:52 +0100 Subject: [PATCH 05/56] Add design decisions: ProofView and TerminationScope for future refernece --- docs/Roadmap.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/docs/Roadmap.md b/docs/Roadmap.md index 91cb44f..04b2a43 100644 --- a/docs/Roadmap.md +++ b/docs/Roadmap.md @@ -15,3 +15,20 @@ - [ ] Develop derivers for simple specifications (find loop invariants, preconditions, postconditions). - [ ] Implement a verification engine that can check function equivalence based on provided specifications. - [ ] Implement searching of target conditions for equivalence using SMT solvers. + +## Design Decisions: ProofView and TerminationScope + +- Construct: ProofView (aka TheoremDerivationView) overlays an original function, keeps an explicit reference to it, and adds reasoning without mutating the source. +- Reasoning model: + - Use existing IR ops (e.g., iadd, icmp) in side-effect-free PreBlock and PostBlocks. + - Employ !assume and !assert to express preconditions, invariants, and postconditions. + - Order is governed by SSA dependencies; values must be defined before use. +- Termination analysis: + - Introduce TerminationScope for MetaAnalysisStat::TerminationBehavior: + - BlockExit: termination of the current block. + - FunctionExit: termination of the entire function. + - ReachPoint(label): termination defined as reaching a specific label. + - ReachAny(labels): termination if any label in the set is reached. + - ReachAll(labels): termination if all labels in the set are reached. +- Quantified reasoning: + - Encode ∀ by treating ProofView PreBlock parameters as bound variables; constrain with !assume in PreBlock and conclude with !assert in PostBlocks. From a95575ebe51471a51d302a018df10526f317f4c4 Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Mon, 19 Jan 2026 19:07:50 +0100 Subject: [PATCH 06/56] Convert Function to Arc in module for external ref --- hyinstr/Cargo.toml | 3 ++- hyinstr/src/modules/mod.rs | 19 +++++++++++-------- hyinstr/src/modules/parser.rs | 5 +++-- hyinstr/tests/modules_tests.rs | 5 +++-- 4 files changed, 19 insertions(+), 13 deletions(-) diff --git a/hyinstr/Cargo.toml b/hyinstr/Cargo.toml index 75ab871..d6c5ed4 100644 --- a/hyinstr/Cargo.toml +++ b/hyinstr/Cargo.toml @@ -26,6 +26,7 @@ default = ["chumsky", "chumsky/either"] serde = [ "dep:serde", "serde/serde_derive", + "serde/rc", "uuid/serde", "num-bigint/serde", "bigdecimal/serde", @@ -33,4 +34,4 @@ serde = [ "bitflags/serde", ] chumsky = ["dep:chumsky"] -borsh = ["dep:borsh", "borsh/derive", "uuid/borsh"] +borsh = ["dep:borsh", "borsh/derive", "borsh/rc", "uuid/borsh"] diff --git a/hyinstr/src/modules/mod.rs b/hyinstr/src/modules/mod.rs index 3f354ed..0ad790b 100644 --- a/hyinstr/src/modules/mod.rs +++ b/hyinstr/src/modules/mod.rs @@ -848,7 +848,7 @@ pub struct FunctionAnalysisContext<'a> { )] pub struct Module { /// Defined functions keyed by their UUID. - pub functions: BTreeMap, + pub functions: BTreeMap>, /// Declared external functions keyed by their UUID. pub external_functions: BTreeMap, } @@ -914,8 +914,8 @@ impl Module { FunctionPointerType::Internal => self .functions .values() - .find(|f| f.name.as_deref() == Some(name)) - .map(|f| FunctionPointer::Internal(f.uuid)), + .find(|f| f.as_ref().name.as_deref() == Some(name)) + .map(|f| FunctionPointer::Internal(f.as_ref().uuid)), FunctionPointerType::External => self .external_functions .values() @@ -932,23 +932,26 @@ impl Module { pub fn find_internal_function_uuid_by_name(&self, name: &str) -> Option { self.functions .values() - .find(|f| f.name.as_deref() == Some(name)) - .map(|f| f.uuid) + .find(|f| f.as_ref().name.as_deref() == Some(name)) + .map(|f| f.as_ref().uuid) } /// Retrieve a particular function from its Uuid pub fn get_internal_function_by_uuid(&self, uuid: Uuid) -> Option<&Function> { - self.functions.get(&uuid) + self.functions.get(&uuid).map(|f| f.as_ref()) } /// Retrieve a particular function from its Uuid (mutable) pub fn get_internal_function_by_uuid_mut(&mut self, uuid: Uuid) -> Option<&mut Function> { - self.functions.get_mut(&uuid) + self.functions + .get_mut(&uuid) + .and_then(|arc| std::sync::Arc::get_mut(arc)) } /// Check each function in the module for SSA validity. pub fn verify(&self) -> Result<(), Error> { - for function in self.functions.values() { + for func in self.functions.values() { + let function = func.as_ref(); function.verify()?; self.verify_func(function)?; } diff --git a/hyinstr/src/modules/parser.rs b/hyinstr/src/modules/parser.rs index b7894d0..a29a6c7 100644 --- a/hyinstr/src/modules/parser.rs +++ b/hyinstr/src/modules/parser.rs @@ -3,6 +3,7 @@ use std::{ collections::{BTreeMap, HashMap}, path::Path, rc::Rc, + sync::Arc, u16, }; @@ -2035,7 +2036,7 @@ pub fn extend_module_from_path( } // Add it to the module - module.functions.insert(func.uuid, func); + module.functions.insert(func.uuid, Arc::new(func)); } // Verify module @@ -2256,7 +2257,7 @@ pub fn extend_module_from_string( } } - module.functions.insert(func.uuid, func.clone()); + module.functions.insert(func.uuid, Arc::new(func)); } // Verify module integrity diff --git a/hyinstr/tests/modules_tests.rs b/hyinstr/tests/modules_tests.rs index 7407c51..a5814f6 100644 --- a/hyinstr/tests/modules_tests.rs +++ b/hyinstr/tests/modules_tests.rs @@ -1,3 +1,4 @@ +use std::sync::Arc; use std::{ collections::{BTreeMap, BTreeSet}, fs, @@ -541,7 +542,7 @@ fn module_verify_succeeds_when_functions_resolved() { wildcard_types: BTreeSet::new(), meta_function: false, }; - module.functions.insert(callee_uuid, callee.clone()); + module.functions.insert(callee_uuid, Arc::new(callee)); // Caller referencing callee let call_instr = HyInstr::from(Invoke { @@ -565,7 +566,7 @@ fn module_verify_succeeds_when_functions_resolved() { BTreeSet::new(), false, ); - module.functions.insert(caller.uuid, caller); + module.functions.insert(caller.uuid, Arc::new(caller)); module.verify().unwrap(); } From 88913505f0a9c2f254931d147e8b0cd04d82213c Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Mon, 19 Jan 2026 19:09:19 +0100 Subject: [PATCH 07/56] Add default to Function and derived_from field --- hyinstr/src/modules/mod.rs | 29 +++++++++++++++++++++++++++++ hyinstr/src/modules/parser.rs | 2 +- hyinstr/tests/modules_tests.rs | 9 ++------- 3 files changed, 32 insertions(+), 8 deletions(-) diff --git a/hyinstr/src/modules/mod.rs b/hyinstr/src/modules/mod.rs index 0ad790b..5ec38b6 100644 --- a/hyinstr/src/modules/mod.rs +++ b/hyinstr/src/modules/mod.rs @@ -23,6 +23,7 @@ use crate::{ instructions::{HyInstr, Instruction}, operand::{Label, Name, Operand}, symbol::{ExternalFunction, FunctionPointer, FunctionPointerType}, + terminator::Trap, }, types::{Typeref, primary::WType}, utils::Error, @@ -377,6 +378,34 @@ pub struct Function { pub wildcard_types: BTreeSet, /// Indicates whether this function is a meta-function (i.e., used for verification or analysis purposes). pub meta_function: bool, + /// If this function was derived from another, holds the source function UUID. + pub derived_from: Option, +} + +impl Default for Function { + fn default() -> Self { + Self { + uuid: Uuid::new_v4(), + name: None, + params: vec![], + return_type: None, + body: [( + Label::NIL, + BasicBlock { + label: Label::NIL, + instructions: vec![], + terminator: terminator::HyTerminator::Trap(Trap), + }, + )] + .into_iter() + .collect(), + visibility: None, + cconv: None, + wildcard_types: Default::default(), + meta_function: false, + derived_from: Default::default(), + } + } } impl Function { diff --git a/hyinstr/src/modules/parser.rs b/hyinstr/src/modules/parser.rs index a29a6c7..6529b87 100644 --- a/hyinstr/src/modules/parser.rs +++ b/hyinstr/src/modules/parser.rs @@ -1757,8 +1757,8 @@ where body: blocks.into_iter().map(|block| (block.label, block)).collect(), visibility: visibility, cconv: cconv, - wildcard_types: Default::default(), meta_function: is_meta_func, + ..Default::default() }; // Check if function should be meta-function diff --git a/hyinstr/tests/modules_tests.rs b/hyinstr/tests/modules_tests.rs index a5814f6..d9f71f5 100644 --- a/hyinstr/tests/modules_tests.rs +++ b/hyinstr/tests/modules_tests.rs @@ -55,15 +55,13 @@ fn function( meta_function: bool, ) -> Function { Function { - uuid: Uuid::new_v4(), name: Some(name.to_string()), params, return_type, body: blocks.into_iter().map(|bb| (bb.label, bb)).collect(), - visibility: None, - cconv: None, wildcard_types, meta_function, + ..Default::default() } } @@ -537,10 +535,7 @@ fn module_verify_succeeds_when_functions_resolved() { }), ), )]), - visibility: None, - cconv: None, - wildcard_types: BTreeSet::new(), - meta_function: false, + ..Default::default() }; module.functions.insert(callee_uuid, Arc::new(callee)); From 4cc5309fb8f14d58234359ad4f4d95e5315332ee Mon Sep 17 00:00:00 2001 From: BoyeGuillaume Date: Mon, 19 Jan 2026 22:44:24 +0100 Subject: [PATCH 08/56] Starting working on introduction of new meta-analysis instruction --- hyinstr/src/analysis.rs | 30 ++++- hyinstr/src/lib.rs | 1 + hyinstr/src/modules/instructions/meta.rs | 48 ++++++++ hyinstr/src/modules/instructions/mod.rs | 11 ++ hyinstr/src/modules/parser.rs | 142 ++++++++++++++++++++++- hyinstr/src/proof.rs | 22 ++++ hyinstr/tests/modules_tests.rs | 116 ++++++++++++++++++ 7 files changed, 363 insertions(+), 7 deletions(-) create mode 100644 hyinstr/src/proof.rs diff --git a/hyinstr/src/analysis.rs b/hyinstr/src/analysis.rs index 7d632ed..d382594 100644 --- a/hyinstr/src/analysis.rs +++ b/hyinstr/src/analysis.rs @@ -4,6 +4,7 @@ use serde::{Deserialize, Serialize}; use strum::{EnumDiscriminants, EnumIs, EnumIter, EnumTryAs, IntoEnumIterator}; use crate::modules::instructions::InstructionFlags; +use crate::modules::operand::Label; /// Possible termination behaviors of a block of instructions/function. /// @@ -51,10 +52,28 @@ impl TerminationBehavior { } } +/// Scope over which termination behavior is evaluated. +/// +/// Selects the region of interest for the termination query. +#[derive(Debug, Clone, Hash, PartialEq, Eq)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr( + feature = "borsh", + derive(borsh::BorshSerialize, borsh::BorshDeserialize) +)] +pub enum TerminationScope { + /// Termination is defined as reaching the end of the current block. + BlockExit, + /// Termination of the entire function (any return/trap or completion of all paths). + FunctionExit, + /// Termination if any label in the set is reached. + ReachAny(Vec