History log of /wasmtime-44.0.1/cranelift/codegen/src/prelude.isle (Results 1 – 25 of 161)
Revision (<<< Hide revision tags) (Show revision tags >>>) Date Author Comments
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


1234567