Skip to content

Prototype LLVM 15 support#832

Open
shaobo-he wants to merge 4 commits into
developfrom
llvm15-develop-prototype
Open

Prototype LLVM 15 support#832
shaobo-he wants to merge 4 commits into
developfrom
llvm15-develop-prototype

Conversation

@shaobo-he

@shaobo-he shaobo-he commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

This prototypes SMACK support for LLVM 15 using the LLVM 15.0.6 binary distribution.

Changes include:

  • Bump SMACK LLVM version metadata to 15.0.6.
  • Update opaque-pointer-sensitive SMACK code paths to use value, global, GEP source/result, or inferred access types instead of pointer element types.
  • Update memory region sizing and static initializer handling for LLVM 15 opaque pointer IR.
  • Point the sea-dsa submodule at https://github.com/shaobo-he/sea-dsa.git commit 85ef2bd, which is based on upstream dev15 and adds SeaDsa-side opaque pointer field-type recovery.

SeaDsa fork change:

  • Stores recovered pointee evidence in FieldType, so type-aware link fields can distinguish opaque ptr values such as ptr<i32> and ptr<double>.
  • Infers that evidence in local analysis from globals, functions, allocas, GEP source/result types, load/store uses, PHI/select values, and indirect call uses.
  • Adds tests/opaque_ptr_field_types.ll to check recovered field labels in the generated graph.

Validation:

SMACK ./regtest.py
PASSED count: 197
FAILED count: 0
TIMEOUT count: 0
UNKNOWN count: 0

SeaDsa focused test
opaque_ptr_field_types.ll: OutputCheck passed for ptr<i32> and ptr<double>

Note: SeaDsa full lit target could not be run locally because the downloaded LLVM 15 binary package does not include the llvm-lit path referenced by LLVMConfig.cmake.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant