Skip to content

Integrate type inf - #1

Open
yelhsams wants to merge 88 commits into
wellesley-prog-sys:verify-mainfrom
yelhsams:integrate-type-inf
Open

Integrate type inf#1
yelhsams wants to merge 88 commits into
wellesley-prog-sys:verify-mainfrom
yelhsams:integrate-type-inf

Conversation

@yelhsams

@yelhsams yelhsams commented May 6, 2024

Copy link
Copy Markdown
Collaborator

No description provided.

mmcloughlin and others added 30 commits February 2, 2024 10:49
This PR restores the Github actions workflow from the verify-main-2023-01-10 branch.

In addition, we fixup some Cranelift warnings since the Rust setup step from the Wasmtime CI runs with warnings treated as errors.
This PR fixes a bug in the Solver in dynamic width mode and onlywidths true,
where the y operand of a BVShr expression will not be visited. This can
cause type inference to fail. This problem came up when trying to use a
Sail-generated specification that contained a concat expression in the
right-hand-side operand.
This doesn't work the same on x64 as it does on arm, and ends up
deleting important parts of the trace.
avanhatt pushed a commit that referenced this pull request Apr 8, 2026
* Debugging: add builtin gdbstub component.

This adds a debug component that makes use of the debug-main world
defined in bytecodealliance#12756 and serves the gdbstub protocol, with Wasm
extensions, compatible with LLDB.

This component is built and included inside the Wasmtime binary, and
is loaded using the lower-level `-D debugger=...` debug-main option;
the user doesn't need to specify the `.wasm` adapter
component. Instead, the user simply runs `wasmtime run -g <PORT>
program.wasm ...` and Wasmtime will load and prepare to run
`program.wasm` as the debuggee, waiting for a gdbstub connection on
the given TCP port before continuing.

The workflow is:

```
$ wasmtime run -g 1234 program.wasm
[ wasmtime starts and waits for connection ]

$ /opt/wasi-sdk/bin/lldb  # use LLDB from wasi-sdk release 32 or later
(lldb) process connect --plugin wasm connect://localhost:1234
Process 1 stopped
* thread #1, stop reason = signal SIGTRAP
    frame #0: 0x40000000000001cc
->  0x40000000000001cc: unreachable
    0x40000000000001cd: end
    0x40000000000001ce: local.get 0
    0x40000000000001d0: call   13
(lldb) si
Process 1 stopped
* thread #1, stop reason = instruction step into
    frame #0: 0x4000000000000184
->  0x4000000000000184: block
    0x4000000000000186: block
    0x4000000000000188: global.get 1
    0x400000000000018e: i32.const 3664
[ ... ]
```

This makes use of the `gdbstub` third-party crate, into which I've
upstreamed support for the Wasm extensions in daniel5151/gdbstub#188,
daniel5151/gdbstub#189, daniel5151/gdbstub#190, and
daniel5151/gdbstub#192. (I'll add vets as part of this PR.)

* cargo vets.

* Handle Trap events as well as breakpoints.

* Review feedback.

* Fix gdbstub artifact build to make it publishable (by disabling it when isolated crates are used).

* Review feedback.

* fix published-crates list

* For now, empty gdbstub data but no compile error when artifact crate is published.

* add some more Cargo metadata: version for artifact crate dep
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants