Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

WIP: ISLA-derived instruction specs #96

Draft
wants to merge 73 commits into
base: verify-main
Choose a base branch
from
Draft

WIP: ISLA-derived instruction specs #96

wants to merge 73 commits into from

Conversation

mmcloughlin
Copy link
Collaborator

@mmcloughlin mmcloughlin commented Feb 19, 2024 •
edited
Loading

No description provided.

@mmcloughlin
skeleton isla tool
5190aae
@mmcloughlin
integrate isla
1c8692a
@mmcloughlin
it builds
f4af432
@mmcloughlin
get smt out
25e85ba
@mmcloughlin
trying to get multiple opcodes to work
aa70c44
@mmcloughlin
emit Inst to opcodes
7c432e0
@mmcloughlin
Inst to ISLA trace
8a9082e
@mmcloughlin
anyhow::bail
943bd86
@mmcloughlin
veri: slight refactor isla emit
173bb50
@mmcloughlin
veri: isla emit tree shake
565f70f
@mmcloughlin
use todo!
6c1bebf
@mmcloughlin
start adhoc tool to experiment with x64 isla
ee2655c
@mmcloughlin
copypasta isla logic into x86
d44f3b1
@mmcloughlin
attempting to make x64 work
a0e811a
@mmcloughlin
first working trace output for x86
63d64e3
@mmcloughlin
write x64 traces to files
9358c6b
@mmcloughlin
linearization
2b24eb5
@mmcloughlin
disable simplify::hide_initialization
b68e55b 
This doesn't work the same on x64 as it does on arm, and ends up
deleting important parts of the trace.
@mmcloughlin
emit: add a selection of instructions
72fa499
@mmcloughlin
optionally show full traces
f379221
@mmcloughlin
update emit tool to use isla options
ba61ba7
@mmcloughlin
support filtering for ITE and struct reads
e7897da
@mmcloughlin
post-filter simplify
837e59b
@mmcloughlin
account for PSTATE register writes
447f355
@mmcloughlin
type inference: support "extra" spec variables
0c06bfd
@mmcloughlin
isle: printer skeleton
ad20e6e
@mmcloughlin
isle: type printing
d6ee519
@mmcloughlin
isle: printer supports more things
8ed0d01
@mmcloughlin
isle: more printing
81e1fb6
@mmcloughlin
isle: more spec printing
f491dfb
mmcloughlin and others added 29 commits February 18, 2024 20:12
@mmcloughlin
emit: print generated spec
814a67a
@mmcloughlin
emit: tolerate spec conversion failure
97e8582
@mmcloughlin
isaspec adhoc tool for building specs
73f231f
@mmcloughlin
expend spec config to produce a real spec
92c6ffd
@mmcloughlin
veriisle: specfunc experiment for executing single spec functions
8e3f5cf
@mmcloughlin
veriisle: exec add function
31e6ec7
@mmcloughlin
isaspec: provide cases
f26b486
@mmcloughlin
generate more alu ops
3e137e8
@mmcloughlin
keep debug output
46f554d
@mmcloughlin
elide no-op zext
f7decdd
@mmcloughlin
veriisle: isaspec option to write to file
79d673c
@mmcloughlin
isle: parse spec implication operator
b9da528
@mmcloughlin
codegen: add inst_specs.isle to aarch64 isle compilation
5281b49
@mmcloughlin
veriisle: generate instruction specs
176292f
@mmcloughlin
verify add lowering to alu_rrr
b5f2b68
@mmcloughlin
wip
2fe39d3
@mmcloughlin
x64 footprint
a49bfdf
@mmcloughlin
switch back to add rule
feaa688
@mmcloughlin
restore imp case in spec_op_to_expr
95f5c4a
@mmcloughlin
revert changes to aarch64/inst.isle
8c95834
@mmcloughlin
remove debug print in widen to register width
d1e50b0
@mmcloughlin
wip
cfd78d8
@mmcloughlin
fix build
eee9cff
@mmcloughlin
isaspec generates the (= result #b1) condition
2100e74
@mmcloughlin
use different prefixes for each instruction case
106d01e
@mmcloughlin
handle the 32-bit case
cbc0731
@mmcloughlin
extend sail spec to all bitwidths
5374323
@mmcloughlin
add more aluops
7bf9cc4
@mmcloughlin
define isla dependency with git
9eba5f6
avanhatt pushed a commit to wellesley-prog-sys/wasmtime that referenced this pull request Oct 9, 2024
@mmcloughlin
ci: upgrade actions/checkout to v4 (avanhatt#96)
192fffc 
Upgrade checkout action to resolve Node 20 warnings.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@mmcloughlin