Repository navigation
Conversation
isla-sail hadn't been updated for two Sail API changes since this commit was last tested against a current Sail release: - Sail_file.to_path / Sail_file.Path.to_string don't exist. The value being passed through them (file_map's entries) was never a Sail_file handle to begin with -- it's collected from Lexing.position.pos_fname in file_number above, which is a plain string. Print it directly. - Preprocess.add_default_symbol was removed; add_symbol is now the only registration mechanism. Since this call still runs before any user-provided symbols are processed, add_symbol has the same effect. Verified by building the plugin and running it against a real Sail RISC-V model (riscv/sail-riscv, as vendored in external/sail-riscv), not just compiling: `isla-sail --all-modules riscv.sail_project -o out` produces a complete .ir file. Isla's own symbolic execution then hits a separate, deeper incompatibility with that specific model's current physical-memory validation logic (unrelated to these two fixes) -- tracked separately, not fixed here. These two fixes are self-contained and upstreamable as-is.
isla-footprint failed during model initialization against a current sail-riscv build (specifically postlude/validate_config.sail's check_pma_regions/check_mem_layout, evaluating `2 ^ physaddr_bits`) with "Type error: %i64->%i I128(4)". i64_to_i128 is the primop backing Sail's %i64->%i conversion, and only handled Val::I64 and Val::Symbolic inputs; it had no case for an operand that arrives already as Val::I128. That's a real, reachable case: exponentiation with a dependently-typed exponent (as in `2 ^ physaddr_bits`) can produce an I128 value on a path that's statically typed %i64, before it reaches this conversion. Since I128 is what this function widens *to*, an already-I128 input just needs to pass through unchanged -- the same reasoning already applied to the existing Val::I64 and Val::Symbolic cases, just missing this one. Verified against a snapshot built (via isla-sail, see the prior two commits on this branch) from riscv/sail-riscv HEAD (external/sail-riscv's pinned commit in the formal-c repo, 29e6158f): isla-footprint now correctly derives ADD's semantics as a genuine symbolic SMT-LIB formula (x12 := x11 + x10 for free variables v408/v409) from that exact model, where it previously failed before any instruction-level execution began.
Contributor
|
The API issue has happened because isla-sail has been updated for the development version of Sail (which should be released shortly), although there's another small tweak I need to make. The |
Alasdair
pushed a commit
to rems-project/sail
that referenced
this pull request
Oct 21, 2026
Otherwise isla-sail attempts to use large integers in some places where a small one is expected, e.g. structs. Fixes rems-project/isla#105.
bacam
added a commit
to bacam/sail
that referenced
this pull request
Oct 22, 2026
Otherwise isla-sail attempts to use large integers in some places where a small one is expected, e.g. structs. Fixes rems-project/isla#105.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two small, independent compatibility fixes found while getting isla-sail
and isla-footprint working against a current Sail release (0.20.2) and
a recent riscv/sail-riscv commit.
isla-sail against current Sail 0.20.2 API (342231a)
jib_ir.ml:Sail_file.to_path/Path.to_stringno longer exist.The values being passed through them were always plain filename
strings (collected from
Lexing.position.pos_fname), never realSail_filehandles -- printed directly instead.sail_plugin_isla.ml:Preprocess.add_default_symbolwas removed;add_symbolis now the only registration mechanism, with the sameeffect at this call site (still runs before any user-provided
symbols are processed).
Verified by building the plugin and running it against a real Sail
RISC-V model (riscv/sail-riscv):
isla-sail --all-modules riscv.sail_project -o outnow produces a complete.irfile.i64_to_i128 accepting an already-widened I128 operand (70d2085)
i64_to_i128(backing Sail's%i64->%iconversion) only handledVal::I64andVal::Symbolicinputs. A real, reachable path incurrent sail-riscv -- exponentiation with a dependently-typed exponent,
as in
2 ^ physaddr_bits-- produces an already-Val::I128value on apath statically typed
%i64before it reaches this conversion. SinceI128 is what this function widens to, an already-I128 input just
needs to pass through unchanged.
Verified against a snapshot built from riscv/sail-riscv HEAD:
isla-footprint now correctly derives instruction semantics as symbolic
SMT-LIB (confirmed with ADD) from that model, where it previously
failed with a type error before any instruction-level execution began.