|
Revision tags: dev, v36.0.9, v44.0.1, v43.0.2, v36.0.8, v24.0.8, v44.0.0, v43.0.1, v42.0.2, v36.0.7, v24.0.7, v43.0.0 |
|
| #
198e34a2 |
| 16-Mar-2026 |
Bongjun Jang <[email protected]> |
[Cranelift] add type-aware rotate operations (#12764)
* [Cranelift] add type-aware rotate operations
* [Cranelift] add cprop rules for rotations
* [Cranlift] assert datatype assumptions
* add fil
[Cranelift] add type-aware rotate operations (#12764)
* [Cranelift] add type-aware rotate operations
* [Cranelift] add cprop rules for rotations
* [Cranlift] assert datatype assumptions
* add filetests for cprops
show more ...
|
|
Revision tags: v42.0.1, v41.0.4, v42.0.0, v40.0.4, v36.0.6, v24.0.6, v41.0.3, v41.0.2, v41.0.1, v36.0.5, v40.0.3, v41.0.0, v36.0.4, v39.0.2, v40.0.2, v40.0.1, v40.0.0, v39.0.1, v39.0.0, v38.0.4, v37.0.3, v36.0.3, v24.0.5, v38.0.3, v38.0.2, v38.0.1, v37.0.2 |
|
| #
7129b4b9 |
| 07-Oct-2025 |
Kirpal Grewal <[email protected]> |
Constant propagation opts (#11790)
* Add optimizations for leading / trailing zeros
* Add optimizations for srem
* Add optimizations for urem
* clean up
* fixes
* fixes
* nicer rust
* urem
Constant propagation opts (#11790)
* Add optimizations for leading / trailing zeros
* Add optimizations for srem
* Add optimizations for urem
* clean up
* fixes
* fixes
* nicer rust
* urem
* srem
* Remove srem special casing
iN::min % -1 = 0
* Remove unneeded variable shift
show more ...
|
| #
a21aba2d |
| 03-Oct-2025 |
Alex Crichton <[email protected]> |
Revert "Constant propagation opts (#11748)" (#11785)
* Revert "Constant propagation opts (#11748)"
This reverts commit 7cebfa206fe4a40ab54e9862f30b05c5fefb9043.
* Add regression test for revert
|
| #
7cebfa20 |
| 01-Oct-2025 |
Kirpal Grewal <[email protected]> |
Constant propagation opts (#11748)
* Add optimizations for leading / trailing zeros
* Add optimizations for srem
* Add optimizations for urem
* clean up
* fixes
|
|
Revision tags: v37.0.1, v37.0.0, v36.0.2, v36.0.1, v36.0.0, v35.0.0, v24.0.4, v33.0.2, v34.0.2, v34.0.1, v33.0.1, v24.0.3, v32.0.1, v34.0.0 |
|
| #
cfe17cb1 |
| 19-Jun-2025 |
Nick Fitzgerald <[email protected]> |
Cranelift: Generate integer numeric ops and conversions for ISLE in the meta crate (#11065)
* Cranelift: Generate integer numeric ops and conversions for ISLE in the meta crate
This automatically g
Cranelift: Generate integer numeric ops and conversions for ISLE in the meta crate (#11065)
* Cranelift: Generate integer numeric ops and conversions for ISLE in the meta crate
This automatically generates operations and conversions for integer types for use in ISLE.
Supported types are: `{i,u}{8,16,32,64,128}`
We generate
* Comparisons (eq, ne, lt, lt_eq, gt, gt_eq) * Arithmetic operations (add, sub, mul, div, neg) * These each have checked, wrapping, and unwrapping variants * Bitwise operations (and, or, xor, shifts, counting leading/trailing zeros/ones) * A variety of predicates (is_zero, is_power_of_two, is_odd, etc...) * These generate both partial constructors and a handful of extractors * Conversions * These come in a variety of flavors: fallible, infallible, truncating, unwrapping, sign-reinterpretation * Fallible conversions are also available as an extractor
* Fix copy paste
* Rename `x_reinterpret_as_y` to `x_cast_[un]signed`
* Collapse some fallible conversions in pulley lowering
* Clean up pulley iconst lowering, make sure narrowest `xconst*` instruction is always used
* Avoid an unnecessary truncation in riscv64 lowering
* Use extractor instead of partial constructor in x64 `imm` rule
* Clean up `op mem, imm` x64 lowering rules
* Use `(i64_eq a b)` instead of `(u64_eq (i64_cast_unsigned a) (i64_cast_unsigned b))`
* Rename `<ty>_unwrapping_<op>` to `<ty>_<op>`
show more ...
|
| #
a4f8f8f4 |
| 16-Jun-2025 |
Nick Fitzgerald <[email protected]> |
Add lowering rules for `{add,sub,or,and} mem, imm` on x64 (#11043)
* Add lowering rules for `{add,sub,or,and} mem, imm` on x64
* Fold `<op> reg, imm` lowering rules into existing `x64_op_mem` helpe
Add lowering rules for `{add,sub,or,and} mem, imm` on x64 (#11043)
* Add lowering rules for `{add,sub,or,and} mem, imm` on x64
* Fold `<op> reg, imm` lowering rules into existing `x64_op_mem` helpers
* Remove duplicate decl that got added elsewhere in a different commit on main
show more ...
|
| #
d6f72b56 |
| 16-Jun-2025 |
Alex Crichton <[email protected]> |
x64: Delete the `Imm` instruction variant (#11038)
* x64: Delete the `Imm` instruction variant
This commit deletes the `Imm` instruction variant in ISLE in favor of preexisting instructions already
x64: Delete the `Imm` instruction variant (#11038)
* x64: Delete the `Imm` instruction variant
This commit deletes the `Imm` instruction variant in ISLE in favor of preexisting instructions already added to the new assembler. This required rejiggering and refactoring the `imm` constructor in ISLE and refactoring the `Inst::imm` method as well.
One minor change in this PR is that the immediate `u64::from(u32::MAX)` was mistakenly classified previously as requiring `movabsq` but after this PR it's now classified as being able to use `movl` because the upper bits are zero'd with `movl`. This was an off-by-one mistake in the `nonzero_u64_fits_in_u32` extractor that was deleted in this PR.
This change also documents the preexisting behavior of the `imm` constructor and the `Inst::imm` helper which is to zero the upper bits of the 64-bit immediate passed in to those functions if the desired size is less than 64-bits. This is something I would prefer to avoid because it means the logical value of the immediate is not being preserved which could be a way to possibly subtly introduce bugs in the future. For now though more widespread changes would be needed to fix this so they're omitted.
* Remove emit tests
* Update winch test expectations
show more ...
|
| #
41bbc458 |
| 12-Jun-2025 |
Alex Crichton <[email protected]> |
x64: Remove `MovImmM` and `MovRM` (#11021)
This commit removes these two instruction variants although nothing new was added to the new assembler as all the necessary instructions were already suppo
x64: Remove `MovImmM` and `MovRM` (#11021)
This commit removes these two instruction variants although nothing new was added to the new assembler as all the necessary instructions were already supported.
show more ...
|
| #
94477009 |
| 10-Jun-2025 |
Bongjun Jang <[email protected]> |
Cranelift: `or(x, C) + (-C) --> and(x, ~C)` (#10979)
* add helper
* add rule and test
* update rule
* add rule summary
* update expectation test
|
| #
84477fc5 |
| 30-May-2025 |
Chris Fallin <[email protected]> |
Cranelift: properly reject unimplemented big-endian loads/stores. (#10863)
At some point during the development of the Cranelift backend infrastructure, to properly support big-endian architectures
Cranelift: properly reject unimplemented big-endian loads/stores. (#10863)
At some point during the development of the Cranelift backend infrastructure, to properly support big-endian architectures such as s390x, we added explicit endianness flags to `MemFlags`, which are given to all memory operations (e.g., loads, stores, and atomic ops). In s390x in particular, the backend carefully observes these flags, because a prominent use of Cranelift (as a Wasm backend) requires explicit little-endian behavior and the system is big-endian. However, all of our other supported ISAs are little-endian and so we did not implement explicit checks at the time, instead accepting all loads and stores as an artifact of our little-endian-only origins.
This PR adds explicit conditions to all ISLE rules that lower loads, stores, and atomic ops on x86-64, aarch64, and riscv64 to accept little or "native" (also little) endian operations only. Compilation of a big-endian operation will now result in a compilation error because no ISLE rule will match (no lowering exists). At some later point we could add these lowerings, but for now we at least do not miscompile.
Fixes #10861.
show more ...
|
| #
6abe3c44 |
| 20-May-2025 |
Alex Crichton <[email protected]> |
x64: Fix panic compiling 16-bit multiply-with-immediate (#10817)
* x64: Fix panic compiling 16-bit multiply-with-immediate
This commit fixes a minor regression from #10782 found via fuzzing. The re
x64: Fix panic compiling 16-bit multiply-with-immediate (#10817)
* x64: Fix panic compiling 16-bit multiply-with-immediate
This commit fixes a minor regression from #10782 found via fuzzing. The regression is 16-bit immediates were forced to fit from an `i32` value into a `u16` for 16-bit multiplication. This meant though that negative numbers failed this conversion which meant that ISLE would panic due to the value not being matched. This fixes the logic to first fit the i32 into an i16 and then cast that to a u16 where the first phase should hit all the constants that are possible in Cranelift.
* Add some more tests
show more ...
|
|
Revision tags: v33.0.0 |
|
| #
7ea7ebcc |
| 19-May-2025 |
Andrew Brown <[email protected]> |
x64: convert all multiplication-related instructions (#10782)
* asm: add SSE4.1 feature
* asm: refactor format constructors with expanding structs
* asm: add implicit operands
Implicit operands a
x64: convert all multiplication-related instructions (#10782)
* asm: add SSE4.1 feature
* asm: refactor format constructors with expanding structs
* asm: add implicit operands
Implicit operands are used by an instruction but not present in its disassembled output. Instructions like `mul`, e.g., will write to the `%rax` and `%rdx` registers, but this is all invisible in disassembly. Implicit operands are always fixed (i.e., the register is known), but not all fixed operands are implicit (i.e., some fixed registers _are_ disassembled).
* asm: add `mul*` instructions, vector and scalar
* asm: generate ISLE for multi-return constructors--`AssemblerOutputs::RetValueRegs`
Certain `mul*` instructions write to multiple registers. For register allocation, Cranelift needs to know about all of these registers. This change uses the pre-existing pattern of returning a `ValueRegs` type to indicate this. This change is limited to what is needed now: the only multi-return needed now uses two fixed registers.
* x64: convert SSE multiplications
* x64: convert scalar multiplications
* x64: remove old `Inst::Mul*` variants
* winch: convert multiplications
This does not include any special "small immediate resizing" rules for Winch, so the Winch disassembly tests gain a few bytes (e.g., some immediates that _could_ fit in 8 bits are emitted as the full 32 bits).
* refactor: move `i32`-related extractors to `prelude.isle`
* review: print the implicit registers as well
* fix: the instruction size has changed (again)
show more ...
|
| #
5ded0f4e |
| 06-May-2025 |
Ulrich Weigand <[email protected]> |
Refactor call ABI implementation (#10722)
This refactors implementation of call ABI handling across architectures with the goal of bringing s390x in line with other platforms.
The main idea is to -
Refactor call ABI implementation (#10722)
This refactors implementation of call ABI handling across architectures with the goal of bringing s390x in line with other platforms.
The main idea is to - handle main call instruction selection and generation in ISLE (like s390x but unlike other platforms today) - handle argument setup mostly outside of ISLE (like other platforms but unlike s390x today) - handle return value processing as part of the call instructio (like all platforms today)
All platforms now emit the main call instruction directly from ISLE, which e.g. handles selection of the correct ISA instruction depending on the call destination. This ISLE code calls out to helper routines to handle argument and return value processing. These helpers are mostly common code and provided by the Callee and/or Lower layers, with some platform-specific additions via ISLE Context routines.
The old CallSite abstraction is no longer needed; most of the differences between call and return_call handling disappear. (There is still a common-code CallInfo vs. a platform-specifc ReturnCallInfo. At this point, it should be relatively straight- forward to make CallInfo platform-specific as well if desired, but this is not done here.)
Some ISLE infrastructure for iterators / loops, which was only ever used by the s390x argument processing code, has been removed.
s390x now closely matches all other platforms, with only a few special cases (slightly different tail-call ABI requires some differences in stack offset computations; we still need to handle vector lane swaps for cross-ABI calls), which should simplify future maintenance.
show more ...
|
| #
d48b3856 |
| 29-Apr-2025 |
beetrees <[email protected]> |
Add support for loading, storing and bitcasting small vectors on x64 and aarch64 (#10693)
|
| #
e52ddbd3 |
| 29-Apr-2025 |
beetrees <[email protected]> |
Add initial `f16` and `f128` support to the s390x backend (#10691)
|
| #
494f5af2 |
| 24-Apr-2025 |
beetrees <[email protected]> |
Add inital support for `f16` without `Zfh` and `f128` to the riscv64 backend (#10652)
|
|
Revision tags: v32.0.0 |
|
| #
7bf31723 |
| 08-Apr-2025 |
Nick Fitzgerald <[email protected]> |
Cranelift: simplify some side-effectful instructions in ISLE (#10524)
* Cranelift: simplify some side-effectful instructions in ISLE
This commit adds a new top-level ISLE entrypoint specifically fo
Cranelift: simplify some side-effectful instructions in ISLE (#10524)
* Cranelift: simplify some side-effectful instructions in ISLE
This commit adds a new top-level ISLE entrypoint specifically for instructions in the side-effectful skeleton: `simplify_skeleton`. While these rewrites are processed during the egraph pass, values from skeleton instructions still do not get inserted into the egraph. Indeed, `simplify_skeleton` operates on *instructions* rather than *values* because we do not represent side effects as values; values do not have side effects in CLIF, instructions do. Therefore, rather than doing a whole dynamic-programming style extraction of the best candidate simplification like we do with the egraph, we take an eager and greedy approach.
Furthermore, `simplify_skeleton` is limited only to skeleton instructions that do not involve control-flow or terminators right now. This is because changing the control-flow graph can change whether a use is dominated by a def or not, and we do not currently have the machinery to track and fix up invalidated uses. Addressing this is left for future commits.
* fix `MIN / -1` cprop and add negative tests for things simplify_skeleton cannot handle yet
show more ...
|
|
Revision tags: v31.0.0, v30.0.2, v30.0.1, v30.0.0 |
|
| #
9260ce47 |
| 10-Feb-2025 |
Alex Crichton <[email protected]> |
pulley: Reimplement wasm loads/stores & memory opcodes (#10154)
* pulley: Reimplement wasm loads/stores & memory opcodes
This commit is a large refactoring to reimplement how WebAssembly loads/stor
pulley: Reimplement wasm loads/stores & memory opcodes (#10154)
* pulley: Reimplement wasm loads/stores & memory opcodes
This commit is a large refactoring to reimplement how WebAssembly loads/stores are translated to Pulley opcodes when using the interpreter. Additionally the functionality related to memory support has changed quite a bit with the interpreter as well. This is all based off comments on #10102 with the end goal of folding the two Pulley opcodes today of "do the bounds check" and "do the load" into one opcode. This is intended to reduce the number of opcodes and overall improve interpreter throughput by minimizing turns of the interpreter loop.
The basic idea behind this PR is that a new basic suite of loads/stores are added to Pulley which trap if the address is zero. This provides a route to translate trapping loads/stores in CLIF to Pulley bytecode without actually causing segfaults at runtime. WebAssembly translation to CLIF is then updated to use the `select` trick for wasm loads/stores where either 0 is loaded from or the actual address is loaded from. Basic support for translation and such is added for this everywhere, and this ensures that all loads/stores for wasm will be translated successfully with Pulley.
The next step was to extend the "g32" addressing mode preexisting in Pulley to support a bounds check as well. New pattern-matches were added to ISLE to search for a bounds check in the address of a trapping load/store. If found then the entire chain of operations necessary to compute the address are folded into a single "g32" opcode which ends up being a fallible load/store at runtime.
To fit all this into Pulley this commit contains a number of refactorings to shuffle around existing opcodes related to memory and extend various pieces of functionality here and there:
* Pulley now uses a `AddrFoo` types to represent addressing modes as a single immediate rather than splitting it up into pieces for each method. For example `AddrO32` represents "base + offset32". `AddrZ` represents the same thing but traps if the address is zero. The `AddrG32` mode represents a bounds-checked 32-bit linear memory access on behalf of wasm.
* Pulley loads/stores were reduced to always using an `AddrFoo` immediate. This means that the old `offset8` addressing mode was removed without replacement here (to be added in the future if necessary). Additionally the suite of sign-extension modes supported were trimmed down to remove 8-to-64, 16-to-64, and 32-to-64 extensions folded as part of the opcode. These can of course always be re-added later but probably want to be added just for the `G32` addressing mode as opposed to all addressing modes.
* The interpreter itself was refactored to have an `AddressingMode` trait to ensure that all memory accesses, regardless of addressing modes, are largely just copy/pastes of each other. In the future it might make sense to implement these methods with a macro, but for now it's copy/paste.
* In ISLE the `XLoad` generic instruction removed its `ext` field to have extensions handled exclusively in ISLE instead of partly in `emit.rs`.
* Float/vector loads/stores now have "g32" addressing (in addition to the "z" that's required for wasm) since it was easy to add them.
* Translation of 1-byte accesses on Pulley from WebAssembly to CLIF no longer has a special case for using `a >= b` instead of `a > b - 1` to ensure that the same bounds-check instruction can be used for all sizes of loads/stores.
* The bounds-check which folded a load-of-the-bound into the opcode is now present as a "g32bne" addressing mode. with its of suite of instructions to boo.
Overall this PR is not a 1:1 replacement of all previous opcodes with exactly one opcode. For example loading 8 bits sign-extended to 64-bits is now two opcodes instead of one. Additionally some previous opcodes have expanded in size where for example the 8-bit offset mode was remove in favor of only having 32-bit offsets. The goal of this PR is to reboot how memory is handled in Pulley. All loads/stores now use a specific addressing mode and currently all operations supported across addressing modes are consistently supported. In the future it's expected that some features will be added to some addressing modes and not others as necessary, for example extending the "g32" addressing mode only instead of all addressing modes.
For an evaluation of this PR:
* Code size: `spidermonkey.cwasm` file is reduced from 19M to 16M. * Sightglass: `pulldown-cmark` is improved by 15% * Sightglass: `bz2` is improved by 20% * Sightglass: `spidermonkey` is improved by 22% * Coremark: score improved by 40%
Overall this PR and new design looks to be a large win. This is all driven by the reduction in opcodes both for compiled code size and execution speed by minimizing turns of the interpreter loop. In the end I'm also pretty happy with how this turned out and I think the refactorings are well worth it.
* Use new `is_pulley` helper more
* Improve `addrz` helper, tighten up `memory-inbounds.wat` a bit
* Improve codegen in a few `memory-inbounds.wat` cases
* Fix test expectation
show more ...
|
|
Revision tags: v29.0.1, v29.0.0, v28.0.1 |
|
| #
a6a08570 |
| 13-Jan-2025 |
Alex Crichton <[email protected]> |
pulley: Add more addressing modes for loads/stores (#9994)
* pulley: Add more addressing modes for loads/stores
This commit adds a new "g32" addressing mode to Pulley that matches the pattern emitt
pulley: Add more addressing modes for loads/stores (#9994)
* pulley: Add more addressing modes for loads/stores
This commit adds a new "g32" addressing mode to Pulley that matches the pattern emitted by Cranelift for 32-bit wasm guests running on hosts. The general idea here is that this addressing mode encompasses an addition of a host-width value to a zero-extended (optionally) 32-bit value. On 32-bit hosts there's no zero-extension but on 64-bit hosts there's a zero-extension. The wasm address is always 32-bits though which enables using a single instruction for both 32 and 64-bit hosts.
New "g32" loads and stores are added to Pulley with varying sizes and options according to what seems to be common in wasm. The `disas` test suite was updated to showcase using these instructions for wasm loads/stores on 32 and 64-bit hosts.
An additional change in this commit is to deduplicate the 32/64-bit bounds-check macro-ops. The trick in this commit works for those as well meaning that only a single instruction is needed instead of one-per-host-pointer-width. Additionally the load of the bound from the `VMContext` is folded into the bounds check itself as it was found that this was always present anyway before the bounds check.
Overall this shrinks the size of `spidermonkey.cwasm` from 21M to 20M and the runtime of `pulldown-cmark`, `bz2`, and `spidermonkey` on Sightglass have all been reduced by 10%. Not as big wins as I was hoping for but alas.
* Fix debug assertions on 32-bit
show more ...
|
|
Revision tags: v28.0.0 |
|
| #
1e4c470a |
| 19-Dec-2024 |
Alex Crichton <[email protected]> |
pulley: Add immediate payloads to more opcodes (#9861)
* pulley: Add immediate payloads to more opcodes
This commit adds immediate payloads to the following instructions:
* `xmul32` - `xmul32_s8`
pulley: Add immediate payloads to more opcodes (#9861)
* pulley: Add immediate payloads to more opcodes
This commit adds immediate payloads to the following instructions:
* `xmul32` - `xmul32_s8` / `xmul32_s32` * `xmul64` - `xmul64_s8` / `xmul64_s32` * `xband32` - `xband32_s8` / `xband32_s32` * `xband64` - `xband64_s8` / `xband64_s32` * `xbor32` - `xbor32_s8` / `xbor32_s32` * `xbor64` - `xbor64_s8` / `xbor64_s32` * `xbxor32` - `xbxor32_s8` / `xbxor32_s32` * `xbxor64` - `xbxor64_s8` / `xbxor64_s32` * `xshl32` - `xshl32_u6` * `xshl64` - `xshl64_u6` * `xshr32_u` - `xshl32_u_u6` * `xshr64_u` - `xshl64_u_u6` * `xshr32_s` - `xshl32_s_u6` * `xshr64_s` - `xshl64_s_u6`
For shifts there's no need to have 32-bit immediates (or even 8-bit) since 6 bits is enough to encode all the immediates. This means that the 6-bit immediate is packed within `BinaryOperands` as a new `U6` type.
This commit unfortunately does not shrink `spidermonkey.cwasm` significantly beyond the prior 29M. This is nevertheless expected to be relatively important for performance.
* Fix test expectations
show more ...
|
| #
b3ac63ae |
| 18-Dec-2024 |
Alex Crichton <[email protected]> |
pulley: Add add/sub-with immediate opcodes (#9859)
This commit extends the pulley opcode space with integer addition/subtraction where `src2` is an immediate. The goal here is to be a "sort of macro
pulley: Add add/sub-with immediate opcodes (#9859)
This commit extends the pulley opcode space with integer addition/subtraction where `src2` is an immediate. The goal here is to be a "sort of macro instruction" despite it not being too too macro here. This cuts down on `xconstN` instructions which both saves space in the final binary and should be slightly more optimal perf-wise due to only one dispatch being needed.
In this commit the `xadd32` instruction is previously 3 bytes: one for an opcode and 2 bytes for the dst/src1/src2 binary operands. Adding a small constant to a register previously took 5 bytes where 2 bytes were needed for `xconst8 N` then 3 for the addition. Here the encoding size of the new instruction is 4 bytes: 1 for the opcode, 2 for dst/src1, and one for the immediate. This is currently chosen to mostly optimize dispatch in the interpreter loop as opposed to code size (as only a single byte is saved). In the future thought it would be possible to extend `BinaryOperands` to one operand being a 6-bit immediate to preserve the same code size.
This also notably adds, for addition/subtraction, only unsigned immediates. With addition/subtraction being inverses of one another supporting signed immediates isn't necessary and helps free up another bit for packing numbers into these opcodes.
This change reduces the size of `spidermonkey.cwasm` from 31M to 29M locally.
show more ...
|
| #
100e90bc |
| 01-Dec-2024 |
Karl Meakin <[email protected]> |
ISLE: built-in integer types (#9610)
Copyright (c) 2024, Arm Limited.
Signed-off-by: Karl Meakin <[email protected]>
|
|
Revision tags: v27.0.0 |
|
| #
bb886ffc |
| 14-Nov-2024 |
Karl Meakin <[email protected]> |
ISLE: Add proper bool type (#9593)
* ISLE: add proper booleans (expressions)
Copyright (c) 2024, Arm Limited.
Signed-off-by: Karl Meakin <[email protected]>
* ISLE: add proper booleans (pattern
ISLE: Add proper bool type (#9593)
* ISLE: add proper booleans (expressions)
Copyright (c) 2024, Arm Limited.
Signed-off-by: Karl Meakin <[email protected]>
* ISLE: add proper booleans (patterns)
Copyright (c) 2024, Arm Limited.
Signed-off-by: Karl Meakin <[email protected]>
* ISLE: add proper booleans (spec expressions)
Copyright (c) 2024, Arm Limited.
Signed-off-by: Karl Meakin <[email protected]>
* ISLE: replace opaque boolean constants
Copyright (c) 2024, Arm Limited.
Replace all occurences of `$true` and `$false` with `true` and `false`.
Signed-off-by: Karl Meakin <[email protected]>
* ISLE: remove `on_lhs` argument
Instead of threading `on_lhs` through all the calls to `translate_expr`, we can just set `is_partial` and `is_pure` on `root_flags` to true.
Copyright (c) 2024, Arm Limited.
Signed-off-by: Karl Meakin <[email protected]>
* ISLE: add proper booleans (language reference)
Copyright (c) 2024, Arm Limited.
Signed-off-by: Karl Meakin <[email protected]>
---------
Signed-off-by: Karl Meakin <[email protected]>
show more ...
|
|
Revision tags: v26.0.1, v25.0.3, v24.0.2, v26.0.0, v21.0.2, v22.0.1, v23.0.3, v25.0.2, v24.0.1 |
|
| #
e4980870 |
| 04-Oct-2024 |
Alexa VanHattum <[email protected]> |
ISLE: upstream prototype ISLE verifier (Crocus) (#9178)
* Squash of verification changes 2024-08-28
* Cleanup
* fmt
* More cleanup
* clippy
* update example spec
* fmt
* null
* clippy part 1
ISLE: upstream prototype ISLE verifier (Crocus) (#9178)
* Squash of verification changes 2024-08-28
* Cleanup
* fmt
* More cleanup
* clippy
* update example spec
* fmt
* null
* clippy part 1
* clippy fix, null
* clippy part 3
* fmt
* disable veri_engine tests in CI
* clap dependency
* remove strum
* use easy-smt version
* Get `cargo vet/deny` working and passing
Undoes a seeming `cargo update` that was performed previously and then adds a vet for the new crate added.
* Flag new crates as not published
* Revert "remove strum"
This reverts commit df7b540b51ebf14d45a7b9f9bbedeba018a53e9a.
* itertools
* Review feedback
* Future work comments for encodings
* fmt
* post merge Cargo.lock updates
* authors
---------
Co-authored-by: Alex Crichton <[email protected]>
show more ...
|
|
Revision tags: v25.0.1, v25.0.0 |
|
| #
b81ef46c |
| 22-Aug-2024 |
Nick Fitzgerald <[email protected]> |
Remove reference types (`r32` and `r64`) from Cranelift (#9164)
* Remove reference types (`r32` and `r64`) from Cranelift
* restore fuzz regression test
|