Add x86 SIMD intrinsic models and generation tool by tautschnig · Pull Request #8939 · diffblue/cbmc

tautschnig · 2026-03-30T20:39:31Z

Depends-on: #9037
Depends-on: #9038
Depends-on: #9039

Add scripts/generate_intrinsic_models.py, which generates CBMC library models for x86 SIMD intrinsics. The tool:

Introspects CBMC's declared builtins vs existing models (--status)
Generates C library functions in src/ansi-c/library/ format
Covers 33 SSE2/SSSE3/SSE4.1 intrinsics: add, sub, min, max, abs, compare, average, and mullo operations for 8/16/32/64-bit elements
Is designed to be extended incrementally (add entries to the MODELS dict for more intrinsics)

The Intel Intrinsics Guide XML can be used with the tool to identify which intrinsics have parseable pseudocode for future auto-generation.

See: #7718

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Copilot

Pull request overview

Adds auto-generated CBMC library models for a set of x86 SIMD (SSE2/SSSE3/SSE4.1) intrinsics, plus a generator script and regression tests to validate the new models.

Changes:

Added scripts/generate_intrinsic_models.py to generate/check coverage of __builtin_ia32_* SIMD intrinsic models.
Added a generated CBMC library file implementing 33 intrinsic models (src/ansi-c/library/x86_intrinsics.c).
Added regression tests for each newly modeled intrinsic under regression/cbmc-library/.

Reviewed changes

Copilot reviewed 68 out of 68 changed files in this pull request and generated 7 comments.

Show a summary per file

File	Description
src/ansi-c/library/x86_intrinsics.c	Adds 33 generated CBMC library models for x86 SIMD intrinsics.
scripts/generate_intrinsic_models.py	Adds a generator/status tool for intrinsic models.
regression/cbmc-library/__builtin_ia32_pabsb128/main.c	Regression test for `__builtin_ia32_pabsb128`.
regression/cbmc-library/__builtin_ia32_pabsb128/test.desc	Test descriptor for `__builtin_ia32_pabsb128`.
regression/cbmc-library/__builtin_ia32_pabsd128/main.c	Regression test for `__builtin_ia32_pabsd128`.
regression/cbmc-library/__builtin_ia32_pabsd128/test.desc	Test descriptor for `__builtin_ia32_pabsd128`.
regression/cbmc-library/__builtin_ia32_pabsw128/main.c	Regression test for `__builtin_ia32_pabsw128`.
regression/cbmc-library/__builtin_ia32_pabsw128/test.desc	Test descriptor for `__builtin_ia32_pabsw128`.
regression/cbmc-library/__builtin_ia32_paddb128/main.c	Regression test for `__builtin_ia32_paddb128`.
regression/cbmc-library/__builtin_ia32_paddb128/test.desc	Test descriptor for `__builtin_ia32_paddb128`.
regression/cbmc-library/__builtin_ia32_paddd128/main.c	Regression test for `__builtin_ia32_paddd128`.
regression/cbmc-library/__builtin_ia32_paddd128/test.desc	Test descriptor for `__builtin_ia32_paddd128`.
regression/cbmc-library/__builtin_ia32_paddq128/main.c	Regression test for `__builtin_ia32_paddq128`.
regression/cbmc-library/__builtin_ia32_paddq128/test.desc	Test descriptor for `__builtin_ia32_paddq128`.
regression/cbmc-library/__builtin_ia32_paddw128/main.c	Regression test for `__builtin_ia32_paddw128`.
regression/cbmc-library/__builtin_ia32_paddw128/test.desc	Test descriptor for `__builtin_ia32_paddw128`.
regression/cbmc-library/__builtin_ia32_pavgb128/main.c	Regression test for `__builtin_ia32_pavgb128`.
regression/cbmc-library/__builtin_ia32_pavgb128/test.desc	Test descriptor for `__builtin_ia32_pavgb128`.
regression/cbmc-library/__builtin_ia32_pavgw128/main.c	Regression test for `__builtin_ia32_pavgw128`.
regression/cbmc-library/__builtin_ia32_pavgw128/test.desc	Test descriptor for `__builtin_ia32_pavgw128`.
regression/cbmc-library/__builtin_ia32_pcmpeqb128/main.c	Regression test for `__builtin_ia32_pcmpeqb128`.
regression/cbmc-library/__builtin_ia32_pcmpeqb128/test.desc	Test descriptor for `__builtin_ia32_pcmpeqb128`.
regression/cbmc-library/__builtin_ia32_pcmpeqd128/main.c	Regression test for `__builtin_ia32_pcmpeqd128`.
regression/cbmc-library/__builtin_ia32_pcmpeqd128/test.desc	Test descriptor for `__builtin_ia32_pcmpeqd128`.
regression/cbmc-library/__builtin_ia32_pcmpeqw128/main.c	Regression test for `__builtin_ia32_pcmpeqw128`.
regression/cbmc-library/__builtin_ia32_pcmpeqw128/test.desc	Test descriptor for `__builtin_ia32_pcmpeqw128`.
regression/cbmc-library/__builtin_ia32_pcmpgtb128/main.c	Regression test for `__builtin_ia32_pcmpgtb128`.
regression/cbmc-library/__builtin_ia32_pcmpgtb128/test.desc	Test descriptor for `__builtin_ia32_pcmpgtb128`.
regression/cbmc-library/__builtin_ia32_pcmpgtd128/main.c	Regression test for `__builtin_ia32_pcmpgtd128`.
regression/cbmc-library/__builtin_ia32_pcmpgtd128/test.desc	Test descriptor for `__builtin_ia32_pcmpgtd128`.
regression/cbmc-library/__builtin_ia32_pcmpgtw128/main.c	Regression test for `__builtin_ia32_pcmpgtw128`.
regression/cbmc-library/__builtin_ia32_pcmpgtw128/test.desc	Test descriptor for `__builtin_ia32_pcmpgtw128`.
regression/cbmc-library/__builtin_ia32_pmaxsb128/main.c	Regression test for `__builtin_ia32_pmaxsb128`.
regression/cbmc-library/__builtin_ia32_pmaxsb128/test.desc	Test descriptor for `__builtin_ia32_pmaxsb128`.
regression/cbmc-library/__builtin_ia32_pmaxsd128/main.c	Regression test for `__builtin_ia32_pmaxsd128`.
regression/cbmc-library/__builtin_ia32_pmaxsd128/test.desc	Test descriptor for `__builtin_ia32_pmaxsd128`.
regression/cbmc-library/__builtin_ia32_pmaxsw128/main.c	Regression test for `__builtin_ia32_pmaxsw128`.
regression/cbmc-library/__builtin_ia32_pmaxsw128/test.desc	Test descriptor for `__builtin_ia32_pmaxsw128`.
regression/cbmc-library/__builtin_ia32_pmaxub128/main.c	Regression test for `__builtin_ia32_pmaxub128`.
regression/cbmc-library/__builtin_ia32_pmaxub128/test.desc	Test descriptor for `__builtin_ia32_pmaxub128`.
regression/cbmc-library/__builtin_ia32_pmaxud128/main.c	Regression test for `__builtin_ia32_pmaxud128`.
regression/cbmc-library/__builtin_ia32_pmaxud128/test.desc	Test descriptor for `__builtin_ia32_pmaxud128`.
regression/cbmc-library/__builtin_ia32_pmaxuw128/main.c	Regression test for `__builtin_ia32_pmaxuw128`.
regression/cbmc-library/__builtin_ia32_pmaxuw128/test.desc	Test descriptor for `__builtin_ia32_pmaxuw128`.
regression/cbmc-library/__builtin_ia32_pminsb128/main.c	Regression test for `__builtin_ia32_pminsb128`.
regression/cbmc-library/__builtin_ia32_pminsb128/test.desc	Test descriptor for `__builtin_ia32_pminsb128`.
regression/cbmc-library/__builtin_ia32_pminsd128/main.c	Regression test for `__builtin_ia32_pminsd128`.
regression/cbmc-library/__builtin_ia32_pminsd128/test.desc	Test descriptor for `__builtin_ia32_pminsd128`.
regression/cbmc-library/__builtin_ia32_pminsw128/main.c	Regression test for `__builtin_ia32_pminsw128`.
regression/cbmc-library/__builtin_ia32_pminsw128/test.desc	Test descriptor for `__builtin_ia32_pminsw128`.
regression/cbmc-library/__builtin_ia32_pminub128/main.c	Regression test for `__builtin_ia32_pminub128`.
regression/cbmc-library/__builtin_ia32_pminub128/test.desc	Test descriptor for `__builtin_ia32_pminub128`.
regression/cbmc-library/__builtin_ia32_pminud128/main.c	Regression test for `__builtin_ia32_pminud128`.
regression/cbmc-library/__builtin_ia32_pminud128/test.desc	Test descriptor for `__builtin_ia32_pminud128`.
regression/cbmc-library/__builtin_ia32_pminuw128/main.c	Regression test for `__builtin_ia32_pminuw128`.
regression/cbmc-library/__builtin_ia32_pminuw128/test.desc	Test descriptor for `__builtin_ia32_pminuw128`.
regression/cbmc-library/__builtin_ia32_pmulld128/main.c	Regression test for `__builtin_ia32_pmulld128`.
regression/cbmc-library/__builtin_ia32_pmulld128/test.desc	Test descriptor for `__builtin_ia32_pmulld128`.
regression/cbmc-library/__builtin_ia32_pmullw128/main.c	Regression test for `__builtin_ia32_pmullw128`.
regression/cbmc-library/__builtin_ia32_pmullw128/test.desc	Test descriptor for `__builtin_ia32_pmullw128`.
regression/cbmc-library/__builtin_ia32_psubb128/main.c	Regression test for `__builtin_ia32_psubb128`.
regression/cbmc-library/__builtin_ia32_psubb128/test.desc	Test descriptor for `__builtin_ia32_psubb128`.
regression/cbmc-library/__builtin_ia32_psubd128/main.c	Regression test for `__builtin_ia32_psubd128`.
regression/cbmc-library/__builtin_ia32_psubd128/test.desc	Test descriptor for `__builtin_ia32_psubd128`.
regression/cbmc-library/__builtin_ia32_psubq128/main.c	Regression test for `__builtin_ia32_psubq128`.
regression/cbmc-library/__builtin_ia32_psubq128/test.desc	Test descriptor for `__builtin_ia32_psubq128`.
regression/cbmc-library/__builtin_ia32_psubw128/main.c	Regression test for `__builtin_ia32_psubw128`.
regression/cbmc-library/__builtin_ia32_psubw128/test.desc	Test descriptor for `__builtin_ia32_psubw128`.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-03-30T20:58:46Z

+/* FUNCTION: __builtin_ia32_paddb128 */
+
+typedef char __gcc_v16qi __attribute__((__vector_size__(16)));
+
+__gcc_v16qi __builtin_ia32_paddb128(__gcc_v16qi a, __gcc_v16qi b)


This file repeats the same typedef declarations for __gcc_v16qi/__gcc_v4si/__gcc_v8hi/__gcc_v2di (and unsigned variants) before many models. That works for CBMC’s per-/* FUNCTION: */ extraction, but it will fail src/ansi-c/library_check.sh (which compiles the whole .c file) due to typedef redefinition errors under -Werror -pedantic. Consider guarding each typedef with a dedicated #ifndef/#define macro (or moving common typedefs into a shared header included by each extracted model).

Copilot · 2026-03-30T20:58:47Z

+  __gcc_v2di b_ = b;
+  __gcc_v2di dst;
+  for(int j = 0; j < 2; j++)
+    dst[j] = a_[j] + b_[j];
+  return dst;


Several models use signed arithmetic directly on int/long long elements (e.g., a_[j] + b_[j]). For these intrinsics the hardware behavior is modulo 2^n wraparound, but in C signed overflow is undefined behavior, which can make the model unsound for edge cases (and may interact badly with overflow checking options). Prefer performing the operation in the corresponding unsigned type (or wider unsigned + truncation) and then casting back to the vector element type so wraparound is well-defined.

Copilot · 2026-03-30T20:58:47Z

+  __gcc_v4si a_ = a;
+  __gcc_v4si dst;
+  for(int j = 0; j < 4; j++)
+    dst[j] = a_[j] < 0 ? -a_[j] : a_[j];
+  return dst;


pabsd on x86 defines abs(INT_MIN) as INT_MIN (bitpattern preserved), but -a_[j] is undefined behavior in C when a_[j] is INT_MIN. To model the intrinsic precisely, compute the negation via unsigned modular arithmetic (or another UB-free formulation) and then cast back to the destination element type.

Copilot · 2026-03-30T20:58:47Z

+  __gcc_v16qi a_ = a;
+  __gcc_v16qi b_ = b;
+  __gcc_v16qi dst;
+  for(int j = 0; j < 16; j++)
+    dst[j] = a_[j] > b_[j] ? -1 : 0;


These byte-based models rely on char being signed (e.g., signed compare for pcmpgtb). char signedness is implementation-defined, so on configurations with unsigned char the comparison semantics would be wrong. Consider casting lane values to signed char for signed-byte operations (abs/min/max/cmpgt/cmpeq on epi8) to make the model independent of the target’s default char signedness.

Copilot · 2026-03-30T20:58:47Z

+    for hdr_name in ("gcc_builtin_headers_ia32.h",
+                     "gcc_builtin_headers_ia32-2.h",
+                     "gcc_builtin_headers_ia32-3.h"):
+        hdr = os.path.join(cbmc_root, "src", "ansi-c", "compiler_headers", hdr_name)
+        if not os.path.exists(hdr):


get_declared_builtins only scans gcc_builtin_headers_ia32.h through gcc_builtin_headers_ia32-3.h, but this repo also has gcc_builtin_headers_ia32-4.h … -9.h (see src/ansi-c/compiler_headers/). This makes --status and generation decisions incomplete. Consider globbing gcc_builtin_headers_ia32*.h (or iterating -2..-9) so the tool reflects all declared x86 builtins.

Copilot · 2026-03-30T20:58:47Z

+def emit_model(builtin, elem_type_str, count, body_tpl, n_params):
+    """Emit a CBMC library model function."""
+    unsigned = elem_type_str.startswith("u:")
+    base_type = elem_type_str.removeprefix("u:")
+    vec_type = VEC_TYPES.get((base_type, count))


emit_model uses str.removeprefix, which requires Python >= 3.9. If the repo’s tooling still targets older Python 3 versions, this will break. Consider replacing with a backwards-compatible expression (e.g., slicing after a startswith check) or documenting/enforcing the minimum Python version for scripts.

Copilot · 2026-03-30T20:58:48Z

+"""
+Generate CBMC library models for x86 SIMD intrinsics from Intel's XML.
+
+Usage:
+    scripts/generate_intrinsic_models.py --status
+    scripts/generate_intrinsic_models.py --xml data-latest.xml \
+        -o src/ansi-c/library/x86_intrinsics.c
+
+Download the XML from:
+  https://www.intel.com/content/dam/develop/public/us/en/include/intrinsics-guide/data-latest.xml
+"""
+
+import argparse, os, re, sys, xml.etree.ElementTree as ET


The script advertises XML-driven generation and accepts --xml, but the XML is not currently parsed/used (and xml.etree.ElementTree as ET is unused). Either implement the XML-based introspection/detail intended here, or remove the unused flag/import and adjust the docstring so the tool’s behavior matches its interface/documentation.

codecov · 2026-03-30T21:29:43Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.60%. Comparing base (01ebe42) to head (f838785).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8939   +/-   ##
========================================
  Coverage    80.59%   80.60%           
========================================
  Files         1711     1711           
  Lines       189454   189454           
  Branches        73       73           
========================================
+ Hits        152697   152700    +3     
+ Misses       36757    36754    -3

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

As of LLVM 20 the per-target builtin databases were migrated from the X-macro ".def" files to TableGen ".td", and NEON/SVE builtins are emitted by clang-tblgen into a "..._BUILTIN_INFOS" form using the classic compact type encoding. Rewrite clang_builtins.py to parse the TableGen .td databases directly, and add a --inc PREFIX:PATH mode that parses clang-tblgen-generated .inc files (e.g. NEON from -gen-arm-neon-sema), prepending PREFIX to each spelling. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add scripts/generate_intrinsic_models.py and the library it produces, src/ansi-c/library/x86_intrinsics.c (204 __builtin_ia32_* models: pointwise arithmetic, saturating add/sub, min/max, abs, shifts, bitwise, compares, MMX/SSE/AVX2/AVX-512 widths and AVX-512 merge-masking). The generator is driven by a curated MODELS table, cross-checks against CBMC's __builtin_ia32_* declarations, can survey/translate Intel Intrinsics Guide pseudocode for maintainers (--status/--xml/--emit-drafts), and emits equivalence tests (--emit-tests). scripts/check_intrinsic_models_sync.sh + a syntax-checks CI job keep the committed library in sync with the generator. cbmc-library tests are consolidated into a single regression/cbmc-library/__builtin_ia32/ directory (one .c per individually tested function, including the pre-existing l/m/sfence tests); the rest are exercised by an aggregate regression/cbmc/SIMD_ia32_models smoke test produced by scripts/generate_simd_smoke_test.py. library_check.sh is generalised to derive coverage by scanning the .c files under the consolidated directory and to treat functions exercised by regression/cbmc/SIMD* as covered. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Clang's <arm_neon.h> declares the NEON vector typedefs (int8x16_t, ...) with __attribute__((neon_vector_type(N))), where N is a lane count rather than a size in bytes as for vector_size. Recognise it in the scanner, add a grammar rule mirroring vector_size that marks the frontend vector as lane-counted (ID_C_vector_lanes), carry that marker through ansi_c_convert_typet, and skip the byte-size/base-size division in typecheck_vector_type for lane-counted vectors. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add gcc_builtin_headers_aarch64.h (Clang __builtin_neon_* declarations, generated by clang_builtins.py from clang-tblgen -gen-arm-neon-sema) and wire it into the front-end like the other per-target builtin headers: extern + string constant in ansi_c_internal_additions, a find_pattern() lookup in the ARM branch of builtin_factory, and the .inc generation rules in the Makefile and CMakeLists. The NEON builtins are polymorphic (arm_neon.h casts operands to the representative lane type and passes a NeonTypeFlags code), so each has a single concrete __gcc_v* signature. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add scripts/generate_neon_models.py and src/ansi-c/library/arm_neon.c, modelling the mechanically-translatable integer NEON families (absolute difference, min/max, saturating/halving/rounding add-sub, pairwise reductions, test-bits, bitwise select). Structure comes from Clang's arm_neon.td; per-instruction semantics are keyed on the ACLE instruction mnemonic (advsimd.md). doc/neon-intrinsic-models.md documents the design and the ARM-JSON vs ARM-ASL trade-off. Individually-tested builtins live in regression/cbmc-library/__builtin_neon/; the rest are exercised by the aggregate regression/cbmc/SIMD_neon_models smoke test (--arch arm64). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig self-assigned this Mar 30, 2026

tautschnig requested a review from a team as a code owner March 30, 2026 20:39

Copilot AI review requested due to automatic review settings March 30, 2026 20:39

tautschnig requested review from kroening, peterschrammel and remi-delmas-3000 as code owners March 30, 2026 20:39

Copilot started reviewing on behalf of tautschnig March 30, 2026 20:52 View session

Copilot AI reviewed Mar 30, 2026

View reviewed changes

tautschnig force-pushed the fix-7718-simd-intrinsics branch 2 times, most recently from 083c04e to f838785 Compare May 29, 2026 10:15

tautschnig marked this pull request as draft June 15, 2026 18:32

tautschnig force-pushed the fix-7718-simd-intrinsics branch from f838785 to fa397c3 Compare June 15, 2026 18:34

tautschnig and others added 5 commits June 15, 2026 18:34

tautschnig force-pushed the fix-7718-simd-intrinsics branch from fa397c3 to 052a8a4 Compare June 15, 2026 18:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add x86 SIMD intrinsic models and generation tool#8939

Add x86 SIMD intrinsic models and generation tool#8939
tautschnig wants to merge 5 commits into
diffblue:developfrom
tautschnig:fix-7718-simd-intrinsics

tautschnig commented Mar 30, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 30, 2026

Uh oh!

Copilot AI Mar 30, 2026

Uh oh!

Copilot AI Mar 30, 2026

Uh oh!

Copilot AI Mar 30, 2026

Uh oh!

Copilot AI Mar 30, 2026

Uh oh!

Copilot AI Mar 30, 2026

Uh oh!

Copilot AI Mar 30, 2026

Uh oh!

codecov Bot commented Mar 30, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

tautschnig commented Mar 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

codecov Bot commented Mar 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

tautschnig commented Mar 30, 2026 •

edited

Loading

codecov Bot commented Mar 30, 2026 •

edited

Loading