Add support for scalable vectors

[zhengyang92]

This patch adds the support for scalable vectors.

In this patch,

• Alive2 generates SMT terms for scalable vectors based on a global vscale factor declared in util/config.h. For example, a scalable vector of type <vscale x 2 x i2> creates eight i2 integers when vscale=4.
• The default vscale factor is set 2 and it can be adjusted by the command line arguments inalive and alive-tv.
• The elements of VectorType is set to vscale * min_elements at the time when the VectorType is created. The min_elements field in VectorType serves solely for IR printer.
• The llvm2alive is able to take scalable vector types.
• The parser of scalable vector types for alive is implemented, check the test cases.
• The llvm.vscale() returns the vscale factor.
• For the mask vectors of shufflevectors, replicate by vscale when the arguments are scalable vectors.

With this patch, Alive2 can validate non-trivial cases with loops as shown in tests/alive-tv/vector/scalable/insert-loop*.ll.

@nunoplopes please let me know what you think.

CC @regehr

[nunoplopes]

vscale needs to be an SMT variable.
If this can be set at run time (I don't know), then it goes to State. If the program can't change it, it goes to the type system.

[zhengyang92]

In the current semantics, vscale cannot be set at runtime, I’ll update the PR so that vscale is inferred as a type parameter. Get Outlook for iOS<https://aka.ms/o0ukef>

…

________________________________ From: Nuno Lopes ***@***.***> Sent: Tuesday, October 7, 2025 2:04:46 AM To: AliveToolkit/alive2 ***@***.***> Cc: ZHENGYANG LIU ***@***.***>; Author ***@***.***> Subject: Re: [AliveToolkit/alive2] Add support for scalable vectors (PR #1247) [https://avatars.githubusercontent.com/u/2998477?s=20&v=4]nunoplopes left a comment (AliveToolkit/alive2#1247)<#1247 (comment)> vscale needs to be an SMT variable. If this can be set at run time (I don't know), then it goes to State. If the program can't change it, it goes to the type system. — Reply to this email directly, view it on GitHub<#1247 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAPMVRKX6OYU6AQ3KZOV3KT3WN625AVCNFSM6AAAAACIPKJ25GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTGNZVHA4TKOJWHE>. You are receiving this because you authored the thread.Message ID: ***@***.***>