WIP: ISLA-derived instruction specs#96

Draft

mmcloughlin wants to merge 73 commits intoverify-mainfrom

mbm/compile-to-isla

Commits on Feb 19, 2024

skeleton isla tool
mmcloughlin
committed
integrate isla
mmcloughlin
committed
it builds
mmcloughlin
committed
get smt out
mmcloughlin
committed
trying to get multiple opcodes to work
mmcloughlin
committed
emit Inst to opcodes
mmcloughlin
committed
Inst to ISLA trace
mmcloughlin
committed
anyhow::bail
mmcloughlin
committed
veri: slight refactor isla emit
mmcloughlin
committed
veri: isla emit tree shake
mmcloughlin
committed
use todo!
mmcloughlin
committed
start adhoc tool to experiment with x64 isla
mmcloughlin
committed
copypasta isla logic into x86
mmcloughlin
committed
attempting to make x64 work
mmcloughlin
committed
first working trace output for x86
mmcloughlin
committed
write x64 traces to files
mmcloughlin
committed
linearization
mmcloughlin
committed
disable simplify::hide_initialization
mmcloughlin
committed
emit: add a selection of instructions
mmcloughlin
committed
optionally show full traces
mmcloughlin
committed
update emit tool to use isla options
mmcloughlin
committed
support filtering for ITE and struct reads
mmcloughlin
committed
post-filter simplify
mmcloughlin
committed
account for PSTATE register writes
mmcloughlin
committed
type inference: support "extra" spec variables
mmcloughlin
committed
isle: printer skeleton
mmcloughlin
committed
isle: type printing
mmcloughlin
committed
isle: printer supports more things
mmcloughlin
committed
isle: more printing
mmcloughlin
committed
isle: more spec printing
mmcloughlin
committed
isle: more printing
mmcloughlin
committed
isle: print if-let
mmcloughlin
committed
basic printer tests
mmcloughlin
committed
ensure printed isle parses
mmcloughlin
committed
alow position tagging to be disabled
mmcloughlin
committed
fix roundtrip errors
mmcloughlin
committed
test against full isle files
mmcloughlin
committed
start trace to spec translation
mmcloughlin
committed
more spec translation
mmcloughlin
committed
even more spec translation
mmcloughlin
committed
use concat to support arbitrary length bitvectors
mmcloughlin
committed
handle more spec translation
mmcloughlin
committed
isle: support printing of any Printable nodes
mmcloughlin
committed
isle: Errors implement std::error::Error
mmcloughlin
committed
emit: print generated spec
mmcloughlin
committed
emit: tolerate spec conversion failure
mmcloughlin
committed
isaspec adhoc tool for building specs
mmcloughlin
committed
expend spec config to produce a real spec
mmcloughlin
committed
veriisle: specfunc experiment for executing single spec functions
mmcloughlin
committed
veriisle: exec add function
mmcloughlin
committed
isaspec: provide cases
mmcloughlin
committed
generate more alu ops
mmcloughlin
committed
keep debug output
mmcloughlin
committed
elide no-op zext
mmcloughlin
committed
veriisle: isaspec option to write to file
mmcloughlin
committed
isle: parse spec implication operator
mmcloughlin
committed
codegen: add inst_specs.isle to aarch64 isle compilation
mmcloughlin
committed
veriisle: generate instruction specs
mmcloughlin
committed
verify add lowering to alu_rrr
mmcloughlin
committed
wip
mmcloughlin
committed
x64 footprint
mmcloughlin
committed
switch back to add rule
mmcloughlin
committed
restore imp case in spec_op_to_expr
mmcloughlin
committed
revert changes to aarch64/inst.isle
mmcloughlin
committed
remove debug print in widen to register width
mmcloughlin
committed
wip
mmcloughlin
committed
fix build
mmcloughlin
committed
isaspec generates the (= result #b1) condition
mmcloughlin
committed
use different prefixes for each instruction case
mmcloughlin
committed
handle the 32-bit case
mmcloughlin
committed
extend sail spec to all bitwidths
mmcloughlin
committed
add more aluops
mmcloughlin
committed
define isla dependency with git
mmcloughlin
committed