Feat/shedskin fprime support

Dockerfile

@@ -0,0 +1,69 @@
+
+FROM ubuntu:22.04
+
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Install base dependencies and Python 3
+RUN apt-get update && \
+    apt-get install -y --no-install-recommends \
+        build-essential \
+        git \
+        wget \
+        curl \
+        python3 \
+        python3-dev \
+        python3-pip \
+        g++ \
+        flex \
+        bison \
+        ca-certificates \
+        unzip \
+        libgc-dev \
+        libpcre3-dev \
+    && rm -rf /var/lib/apt/lists/*
+
+# Provide compatibility symlinks for Shedskin's expected libgctba
+RUN if [ -f /usr/lib/x86_64-linux-gnu/libgccpp.so ]; then \
+        ln -sf /usr/lib/x86_64-linux-gnu/libgccpp.so /usr/lib/x86_64-linux-gnu/libgctba.so; \
+    fi && \
+    if [ -f /usr/lib/x86_64-linux-gnu/libgccpp.a ]; then \
+        ln -sf /usr/lib/x86_64-linux-gnu/libgccpp.a /usr/lib/x86_64-linux-gnu/libgctba.a; \
+    fi
+
+# Install Shedskin (latest version via pip3)
+# Shedskin now works with Python 3 (versions 0.9.8+)
+RUN python3 -m pip install --upgrade pip setuptools wheel && \
+    SHEDSKIN_LATEST=$(curl -s https://api.github.com/repos/shedskin/shedskin/releases/latest | grep '"tag_name"' | cut -d'"' -f4) && \
+    echo "Installing Shedskin version: $SHEDSKIN_LATEST" && \
+    python3 -m pip install "shedskin@git+https://github.com/shedskin/shedskin.git@${SHEDSKIN_LATEST}#egg=shedskin" || \
+    (echo "Warning: Shedskin git installation failed. Attempting pip fallback..." && \
+     python3 -m pip install shedskin || \
+     echo "Warning: Shedskin installation failed completely." && true)
+
+WORKDIR /workspace
+VOLUME ["/workspace"]
+
+# Install additional dependencies for ESBMC
+RUN apt-get update && \
+    apt-get install -y --no-install-recommends \
+        libboost-all-dev \
+        libz3-dev \
+        libc6 \
+        libstdc++6 \
+    && rm -rf /var/lib/apt/lists/*
+
+# Download and install latest ESBMC release (esbmc-linux.zip)
+# Always fetches the latest release from GitHub
+RUN ESBMC_DOWNLOAD_URL=$(curl -s https://api.github.com/repos/esbmc/esbmc/releases/latest | \
+    grep -o 'https://github.com/esbmc/esbmc/releases/download/[^"]*esbmc-linux.zip' | head -n 1) && \
+    echo "Downloading ESBMC from: $ESBMC_DOWNLOAD_URL" && \
+    curl -L "$ESBMC_DOWNLOAD_URL" -o esbmc-linux.zip && \
+    unzip -q esbmc-linux.zip && \
+    mv bin/* /usr/local/bin/ && \
+    mv lib/* /usr/local/lib/ && \
+    mv include/* /usr/local/include/ 2>/dev/null || true && \
+    rm -rf esbmc-linux.zip bin lib include license README release-notes.txt && \
+    ldconfig && \
+    which esbmc && esbmc --version
+
+ENTRYPOINT ["/bin/bash"]

Makefile

@@ -0,0 +1,14 @@
+DOCKER_IMAGE ?= esbmc-shedskin
+
+.PHONY: docker-build docker-shell docker-run-example
+
+docker-build:
+	docker build -t $(DOCKER_IMAGE) .
+
+docker-shell: docker-build
+	docker run --rm -it -v "$(PWD)":/workspace -w /workspace $(DOCKER_IMAGE)
+
+# Smoke: convert, compile, and run the Shedskin runtime example inside Docker
+docker-run-example: docker-build
+	docker run --rm -it -v "$(PWD)":/workspace -w /workspace $(DOCKER_IMAGE) \
+		-lc "set -e; rm -rf /tmp/shedskin-smoke; mkdir -p /tmp/shedskin-smoke; cp -r /workspace/examples /tmp/shedskin-smoke/; cd /tmp/shedskin-smoke/examples; exec bash"

README.md

@@ -2,13 +2,15 @@
 
 **ESBMC-Python-CPP** is a work-in-progress toolkit that bridges Python code and C/++ verification through the [ESBMC](https://esbmc.org/) model checker. It supports three primary approaches for converting and analyzing Python code:
 
-1. **Static Conversion via Shedskin**  
+1. **Static Conversion via Shedskin**
    Converts Python to C++ code using [Shedskin](https://github.com/shedskin/shedskin).
+   - See [`docs/shedskin.md`](docs/shedskin.md) for a reproducible Docker setup and usage examples.
+   - See [`docs/hybrid-flow.md`](docs/hybrid-flow.md) for a detailed explanation of the hybrid verification flow.
 
-2. **LLM-Based Conversion from Python to C**  
+2. **LLM-Based Conversion from Python to C**
    Uses local or remote LLMs to directly convert Python code to verifiable C code.
 
-3. **Dynamic Tracing**  
+3. **Dynamic Tracing**
    Traces a specific execution path to analyze behavior during runtime.
 
 ---
@@ -241,8 +243,30 @@ export OPENAI_API_BASE=http://localhost:8080/v1
 
 ---
 
+## 🐳 Using Docker with Shedskin
+
+For a fully reproducible environment with Shedskin and ESBMC, you can use the provided Dockerfile:
+
+```bash
+# 1. Rebuild the image (force refresh of dependencies)
+docker build --no-cache -t esbmc-shedskin .
+# or
+make docker-build
+
+# 2. Open an interactive shell with examples copied to /tmp/shedskin-smoke/examples
+make docker-run-example
+
+# 3. Inside the container (already in /tmp/shedskin-smoke/examples):
+shedskin shedskin_runtime_smoke.py
+make
+./shedskin_runtime_smoke
+```
+
+You can replace `shedskin_runtime_smoke.py` with any other Python example that is compatible with Shedskin.
+
+---
+
 ## 📬 Contact & Contributions
 
 This project is under active development. Feedback, issues, and contributions are welcome!
 
-

dict.hpp

@@ -158,7 +158,63 @@ class dict {
     __ss_int __len__() const {
         return size_;
     }
+
+    // Get value or default
+    V get(const K& key, const V& default_val) const {
+        for (__ss_int i = 0; i < SIZE; i++) {
+            if (used[i] && keys[i] == key) {
+                return values[i];
+            }
+        }
+        return default_val;
+    }
+
+    // Return list of keys
+    list<K>* keys_list() const {
+        list<K>* out = new list<K>();
+        for (__ss_int i = 0; i < SIZE; i++) {
+            if (used[i]) {
+                out->append(keys[i]);
+            }
+        }
+        return out;
+    }
+
+    // Return list of values
+    list<V>* values_list() const {
+        list<V>* out = new list<V>();
+        for (__ss_int i = 0; i < SIZE; i++) {
+            if (used[i]) {
+                out->append(values[i]);
+            }
+        }
+        return out;
+    }
+
+    // Return list of (key, value) tuples
+    list<tuple2<K,V>*>* items_list() const {
+        list<tuple2<K,V>*>* out = new list<tuple2<K,V>*>();
+        for (__ss_int i = 0; i < SIZE; i++) {
+            if (used[i]) {
+                tuple2<K,V>* t = new tuple2<K,V>(2, keys[i], values[i]);
+                out->append(t);
+            }
+        }
+        return out;
+    }
+
+    list<K>* keys() const {
+        return keys_list();
+    }
+
+    list<V>* values() const {
+        return values_list();
+    }
+
+    list<tuple2<K,V>*>* items() const {
+        return items_list();
+    }
 };
 
 } // namespace shedskin
-#endif
+#endif

examples/fprime_threading_smoke.py

@@ -0,0 +1,165 @@
+#!/usr/bin/env python3
+"""F' threading-inspired smoke test for Shedskin (no method passing)."""
+
+from typing import Any, Dict, List, Optional
+
+
+class TaskContext:
+    """Deterministic task runner mimicking an F' rate group."""
+
+    def __init__(self, name: str):
+        self.name = name
+        self._tasks: List[Any] = []
+        self._queue: List[Any] = []
+
+    def add_task(self, task: Any):
+        self._tasks.append(task)
+
+    def schedule_async(self, task: Any):
+        self._queue.append(task)
+
+    def run_once(self):
+        for task in self._tasks:
+            task.run()
+        while self._queue:
+            job = self._queue.pop(0)
+            job.run()
+
+
+class AsyncJob:
+    def __init__(self, handler: Any, data: Any):
+        self.handler = handler
+        self.data = data
+
+    def run(self):
+        self.handler.handle(self.data)
+
+
+class InputPort:
+    """Simplified F' input port com contexto opcional."""
+
+    def __init__(self, name: str, data_type: str):
+        self.name = name
+        self.data_type = data_type
+        self._handler: Optional[Any] = None
+        self._context: Optional[TaskContext] = None
+
+    def register_handler(self, handler: Any, context: Optional[TaskContext] = None):
+        self._handler = handler
+        self._context = context
+
+    def invoke(self, data: Any):
+        if not self._handler:
+            return
+        if self._context:
+            job = AsyncJob(self._handler, data)
+            self._context.schedule_async(job)
+        else:
+            self._handler.handle(data)
+
+
+class OutputPort:
+    """Simplified F' output port that fans out to multiple inputs."""
+
+    def __init__(self, name: str, data_type: str):
+        self.name = name
+        self.data_type = data_type
+        self._connections: List[InputPort] = []
+
+    def connect(self, input_port: InputPort):
+        if input_port.data_type == self.data_type:
+            self._connections.append(input_port)
+
+    def emit(self, data: Any):
+        for connection in self._connections:
+            connection.invoke(data)
+
+
+class CommandMessage:
+    def __init__(self, command_id: int, args: Dict[str, int]):
+        self.command_id = command_id
+        self.args = args
+
+
+class CommandComponent:
+    """Produces command messages for downstream components."""
+
+    def __init__(self):
+        self.command_out = OutputPort("command_out", "CommandMessage")
+
+    def issue(self, command_id: int, payload: Dict[str, int]):
+        msg = CommandMessage(command_id, payload)
+        self.command_out.emit(msg)
+        return msg
+
+
+class TickTask:
+    def __init__(self, component: "ExecutionComponent"):
+        self.component = component
+
+    def run(self):
+        self.component.event_log.append("tick")
+
+
+class CommandHandler:
+    def __init__(self, component: "ExecutionComponent"):
+        self.component = component
+
+    def handle(self, message: CommandMessage):
+        keys = sorted(list(message.args.keys()))
+        parts: List[str] = []
+        for key in keys:
+            value = message.args[key]
+            parts.append(f"{key}={value}")
+        description = f"cmd:{message.command_id}|" + ",".join(parts)
+        self.component.event_log.append(description)
+
+
+class ExecutionComponent:
+    """Consumes commands and logs execution order."""
+
+    def __init__(self):
+        self.command_in = InputPort("command_in", "CommandMessage")
+        self.context = TaskContext("exec")
+        self.event_log: List[str] = []
+        self.tick_task = TickTask(self)
+        self.handler = CommandHandler(self)
+        self.context.add_task(self.tick_task)
+
+    def register(self):
+        self.command_in.register_handler(self.handler, self.context)
+
+
+def run_smoke() -> List[str]:
+    commander = CommandComponent()
+    executor = ExecutionComponent()
+    executor.register()
+    commander.command_out.connect(executor.command_in)
+
+    # Set operations exercise the runtime helpers
+    targets = set(["nav", "nav", "science"])
+    assert len(targets) == 2
+    targets.discard("nav")
+    assert "nav" not in targets
+
+    commander.issue(1, {"speed": 3, "heading": 90})
+    executor.context.run_once()
+
+    commander.issue(2, {"speed": 1})
+    commander.issue(3, {"speed": 2})
+    executor.context.run_once()
+
+    expected = [
+        "tick",
+        "cmd:1|heading=90,speed=3",
+        "tick",
+        "cmd:2|speed=1",
+        "cmd:3|speed=2",
+    ]
+    assert executor.event_log == expected
+    return executor.event_log
+
+
+if __name__ == "__main__":
+    log = run_smoke()
+    print("F' threading smoke log:", log)

examples/shedskin_example_simple.py

@@ -0,0 +1,10 @@
+def inc(x):
+    return x + 1
+
+def main():
+    a = 0
+    a = inc(a)
+    assert a == 1
+
+if __name__ == '__main__':
+    main()