SECO

Simulink Equivalent Code Optimizer uses Simulink subsystem semantics to help identify equivalent C code segments, then checks candidate shared functions with local deterministic tools before applying size-reducing rewrites.

The maintained implementation is in SECO_Implementation/. A program generates the structured task, Codex supplies candidate JSON, and local tools perform validation, compilation, harness generation, CBMC verification, counterexample feedback, and size screening. This offline workflow does not read .env or call an LLM API.

Repository layout

Path	Contents
SECO_Implementation/	Python implementation, MATLAB scripts, solver adapters, tests, and toolchain example.
Model/	Original paper benchmark models, retained from the existing repository.
Experiment/	Original benchmark sources/results and additional benchmark sources.
Experiment/Model/	Models and generated C/header fixtures used by the current workflow and tests.
Codebase/, Example/, Example_Standalone/	C inputs and prompt examples for the legacy API workflow.
CodeCompletion/, CostModel/, Testcase/, TestVerifier/	Input fixtures for retained legacy entry points.
Output/	Generated on demand; not versioned.

Requirements

• Python 3.10 or newer; the offline Python pipeline uses the standard library.
• MATLAB, Simulink, and Embedded Coder for fresh code generation and trace export. Existing generated C can also be used without MATLAB.
• A C compiler and size utility. Clang with -Oz and llvm-size are suitable for the default size-screening path; target compilers are configured separately.
• CBMC and Z3. The local workflow was tested with CBMC 6.10.0 and Z3 5.1.0.

Solver binaries, credentials, machine caches, and cleanup backups are not published. Install tools on PATH, pass paths explicitly, or use the optional local layout in tools/README.md.

Offline workflow

Run commands from the repository root.

1. Generate a task using MATLAB and Embedded Coder:

   python -m SECO_Implementation prepare --model Experiment/Model/ABS.slx --run-dir Output/abs

   Without MATLAB, use the checked-in generated source:

   python -m SECO_Implementation prepare --model Experiment/Model/ABS.slx --source Experiment/Model/ABS_ert_rtw/ABS.c --skip-matlab --run-dir Output/abs

   Without trace metadata, the source-only path does not infer Simulink Constant-to-literal parameter mappings.

2. Give Output/abs/CODEX_TASK.md, task.json, and augmented.c to Codex and save its candidates as Output/abs/candidates.json. Subsystem boundaries provide context, not restrictions: candidates use start/end statement IDs and may span part of one subsystem or multiple subsystems.

3. Validate, prove, and screen candidates:

   python -m SECO_Implementation continue --run-dir Output/abs --candidates Output/abs/candidates.json --compiler clang --cbmc-solver z3-fpa-qffpbv --timeout 0

   --cbmc and --cbmc-external-solver override tool discovery. --timeout 0 leaves solver time unbounded. Failed candidates produce feedback for another Codex JSON revision; this is not an automatic API call.

4. Inspect validation/, verification/, profitability/, summary.json, and optimized_verified.c, or run:

   python -m SECO_Implementation status --run-dir Output/abs

See the detailed guide for candidate JSON, mapping, floating-point comparison, feedback limits, and target toolchains. C analysis is conservative, not a general C parser; this implementation is not a claim of full paper benchmark reproduction. Floating-point checks use exact value equality with NaN-to-NaN equivalence, not bitwise identity.

Tests and legacy entry points

python -m unittest discover -s SECO_Implementation/tests -v

Tests do not depend on old runs or downloaded solvers. Compiler-dependent tests are skipped if no C compiler is installed.

The original API-based modules are retained under SECO_Implementation:

python -m pip install -r SECO_Implementation/requirements-legacy.txt
python -m SECO_Implementation.code_optimizer --run-experiments --help

These legacy entry points still require API configuration and are separate from the offline workflow. Never commit .env or API keys.

Benchmarks and references

The original benchmarks include ABS (anti-lock braking), AN (auditory system), Bacteria, DoorLock, HybridPass, BC (bionic cochlea), OHC (hearing-aid DSP), and RAC (robot-arm control). Original experiments include Embedded Coder, Frodo, and SECO.

• Shrestha, Chowdhury, and Csallner. SLNET: a redistributable corpus of 3rd-party Simulink models. MSR 2022. DOI.
• Kroening and Tautschnig. CBMC — C Bounded Model Checker. TACAS 2014. Project.
• MathWorks. Embedded Coder.
• Yu et al. Efficient Code Generation for Data-Intensive Simulink Models via Redundancy Elimination. DAC 2024. DOI.
• Rocha et al. Effective function merging in the SSA form. PLDI 2020. DOI.