Metadata-Version: 2.4
Name: micro-svm
Version: 1.0.1
Summary: Simple symbolic Virtual Machine in Python and Z3
Author: Mikhail Onischuck
License-Expression: MIT
Project-URL: Homepage, https://github.com/dog-m/micro-svm-engine
Project-URL: Issues, https://github.com/dog-m/micro-svm-engine/issues
Classifier: Programming Language :: Python :: 3
Classifier: Operating System :: OS Independent
Classifier: Intended Audience :: Developers
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: z3-solver>=4.0
Dynamic: license-file

# Micro-SVM

A simple and very basic symbolic virtual machine.

> [!IMPORTANT]
> This is a major piece for an ongoing research project.
> We are currently working hard on preparing our results for a publication.

## Overview

Micro-SVM is a standalone symbolic execution engine designed to:

- Explore program execution paths.
- Analyze control flow and state transitions.
- Validate program specifications against expected behaviors.
- Detect potential defects (e.g., unhandled exceptions, infinite loops).

This package provides the core symbolic execution engine used in research projects for defect discovery and path validation.
It is **not** a full programming language implementation but rather a tool for analyzing executable specifications.

## Supported features

- A range of primitive types: `boolean`, `int8/16/32/64`, `integer`, `real`, `char`, `string`.
- Symbolic primitive values.
- Built-in containers for primitives: `array<T>`, `set<T>`, `map<K,V>`, `transform<K,V>` (same as `map`, more limited but *sometimes* faster).
- Functions and/or static methods.
- Java/C#-like reference values (`ref<T>` for references of known type, plain `ref` for "opaque" cases).
- Structures and "classes" (i.e., structures with methods) with multiple inheritance.
- Handling of abstract methods and virtual calls.
- Intrinsics for specific operations.
- Basic library/program specification serialization (JSON).
- Ability to discover and validate both *normal* and *failing* execution paths (see [examples](examples/defect_detection)).
- Basic class-based user-defined exception handling (i.e. the usual `try-catch-finally` triplet and `throw`).
- Basic decoding of complex structures (containers and structures/classes) as Python objects (i.e. as a list, a list of pairs or a dictionary).

## Installation

```bash
pip install micro-svm
```

## Known limitations

- No function/method overload.
- No type checks. It is expected for a specification to be validated and type-checked by *external tools*.
- Little to no type conversion. The implementation relies heavily on Z3 in that aspect.
- No support for IEEE floats.
- Eager function/method execution. For every discovered program path, the machine checks if the whole path can be executed or not.
- Very crude fault handling for certain language- and runtime-specific edge-cases. It is only possible to:
  - not allowing any fault to occur during a path's execution (default),
  - check if they *might* have happened (i.e., using `CompilerContext.get_fault_status/clear_fault_status`),
  - ignore faulty operations.
- Exceptions regarding null-dereferencing, invalid array indexing and alike cannot be raised and caught automatically. It is advised to use `CompilerContext.get_fault_status` and `throw` to raise a suitable exception object. Note that `get_fault_status` is unhelpful unless `SymbolicStateMachine.fault_mode` is set to `STORE`.

## License

This project is licensed under the MIT License - see the [LICENSE](LICENSE) file for details.

---

*AI usage disclosure: 100% of code and ~50% of documentation were written by a <u>human</u> developer.*
