https://github.com/zwegner/x86-sat Skip to content Toggle navigation Sign up * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions For + Enterprise + Teams + Startups + Education By Solution + CI/CD & Automation + DevOps + DevSecOps Case Studies + Customer Stories + Resources * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Pricing [ ] * # In this repository All GitHub | Jump to | * No suggested jump to results * # In this repository All GitHub | Jump to | * # In this user All GitHub | Jump to | * # In this repository All GitHub | Jump to | Sign in Sign up {{ message }} zwegner / x86-sat Public * Notifications * Fork 11 * Star 237 Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs 237 stars 11 forks Star Notifications * Code * Issues 1 * Pull requests 0 * Actions * Projects 0 * Security * Insights More * Code * Issues * Pull requests * Actions * Projects * Security * Insights zwegner/x86-sat This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master Switch branches/tags [ ] Branches Tags Could not load branches Nothing to show {{ refName }} default View all branches Could not load tags Nothing to show {{ refName }} default View all tags Name already in use A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch? Cancel Create 1 branch 0 tags Code * Local * Codespaces * Clone HTTPS GitHub CLI [https://github.com/z] Use Git or checkout with SVN using the web URL. [gh repo clone zwegne] Work fast with our official CLI. Learn more about the CLI. * Open with GitHub Desktop * Download ZIP Sign In Required Please sign in to use Codespaces. Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Launching GitHub Desktop If nothing happens, download GitHub Desktop and try again. Launching Xcode If nothing happens, download Xcode and try again. Launching Visual Studio Code Your codespace will open once ready. There was a problem preparing your codespace, please try again. Latest commit @zwegner zwegner Use data-latest.xml instead of a specific version in Intrinsics Guide... ... a1211ee Dec 1, 2021 Use data-latest.xml instead of a specific version in Intrinsics Guide... ... data URLs to future-proof it a bit a1211ee Git stats * 60 commits Files Permalink Failed to load latest commit information. Type Name Latest commit message Commit time screenshots x86_sat .gitmodules README.md optimize.py pos_popcnt.py test.py View code x86-sat Description Usage README.md x86-sat This is a rudimentary attempt to build an autogenerated formal-ish model of x86 intrinsics by interpreting Intel's instruction pseudocode, transforming it into a model for Z3. overview image Description Intel's Intrinsics Guide provides an interactive guide with data for each x86 intrinsic instruction, including a pseudocode that specifies the instruction's behavior. The intrinsics guide is backed by an XML file with all of this data in an easily parseable format, which we use here to build a Z3 model. So far, only these features of Intel's pseudocode are supported: * Basic unary/binary arithmetic/bitwise operations, and ternary conditionals * Bit slices, both reading and writing * IF/CASE conditionals (which are predicated when they can't be statically resolved) * FOR loops * Function definitions/calls See tokens/rules in parse.py for the most up-to-date information. There are many functions used in Intel's documentation that are not explicitly given in the XML. For now, these are almost all unsupported (see functions defined in intr_builtins.py for the current list). This method of generating models is inherently limited. The intrinsics only cover a subset of x86 instructions (presumably until a PDF reader is added), so this will mostly be useful for investigating hand-rolled SIMD code, etc. Handling memory might be possible but would certainly be very slow. Handling control flow is likely out of scope for now too. There are quite possibly bugs in this implementation, which can be pretty hard to find and fix. There are also definitely bugs in Intel's code (see below), so this shouldn't be relied on for anything serious. So far, this can do some interesting non-trivial things, like derive lookup tables for vpternlogd: check_print(_mm512_ternarylogic_epi32(_mm512_set1_epi8(0xAA), _mm512_set1_epi8(0xCC), _mm512_set1_epi8(0xF0), i) == _mm512_set1_epi8(0x57)) # -> [y = 0x1f] ...or find an index vector for vpermb that reverses its input: values = range(2, 3*64, 3) check(_mm512_set_epi8(*values) == _mm512_permutexvar_epi8(b, _mm512_set_epi8(*reversed(values)))) # <- [b = 0x000102030405060708090a0b0c0d0e0f1011...] ...or find a bug in Intel's pseudocode. Turns out that last one gives unsat, which didn't make sense. Investigating further, I noticed that I wasn't getting the right result for a _mm512_set_epi8(*range(64)), which led me to find this bug in the _mm512_set_epi8 pseudocode: dst[495:488] := e61 dst[503:496] := e62 -dst[511:503] := e63 +dst[511:504] := e63 dst[MAX:512] := 0 All of these intrinsic functions used in these examples (and the ones in test.py) are completely autogenerated from Intel's data; there's no manual intrinsics created whatsoever. Usage To use this, you must first download the latest XML from Intel's Intrinsics Guide (currently here: https://www.intel.com/content/dam/ develop/public/us/en/include/intrinsics-guide/data-latest.xml) and save it as data.xml in the current directory. I don't believe I can legally redistribute this file myself. This project requires Z3, and my sprdpl parsing library (included as a submodule). The library has two primary APIs for looking up and using intrinsics: * The parse_whitelist() function, which returns a dictionary of intrinsic objects, suitable for injecting directly into global scope: intrinsics = parse_whitelist('data.xml', regex='_mm256_set1_epi(8|32)') globals().update(intrinsics) check_print(_mm256_set1_epi8(0) == _mm256_set1_epi32(0)) * The parse_meta() function, which returns a magic object that lazily parses intrinsics pseudocode whenever attributes are accessed, like so: meta = parse_meta('data.xml') check_print(meta._mm256_xor_si256(0, 1) == 1) # .prefixed() allows reducing duplicated prefixes: avx = meta.prefixed('_mm256_') check_print(avx.set1_epi8(0) == 0) See test.py for various example use cases. About Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs Resources Readme Stars 237 stars Watchers 5 watching Forks 11 forks Report repository Releases No releases published Packages 0 No packages published Contributors 2 * @zwegner zwegner Zach Wegner * @markoshorro markoshorro Markos Horro Languages * Python 100.0% Footer (c) 2023 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact GitHub * Pricing * API * Training * Blog * About You can't perform that action at this time. You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.