Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
73 commits
Select commit Hold shift + click to select a range
5190aae
skeleton isla tool
mmcloughlin Nov 30, 2023
1c8692a
integrate isla
mmcloughlin Nov 30, 2023
f4af432
it builds
mmcloughlin Nov 30, 2023
25e85ba
get smt out
mmcloughlin Nov 30, 2023
aa70c44
trying to get multiple opcodes to work
mmcloughlin Nov 30, 2023
7c432e0
emit Inst to opcodes
mmcloughlin Nov 30, 2023
8a9082e
Inst to ISLA trace
mmcloughlin Dec 1, 2023
943bd86
anyhow::bail
mmcloughlin Dec 1, 2023
173bb50
veri: slight refactor isla emit
mmcloughlin Dec 10, 2023
565f70f
veri: isla emit tree shake
mmcloughlin Dec 14, 2023
6c1bebf
use todo!
mmcloughlin Dec 14, 2023
ee2655c
start adhoc tool to experiment with x64 isla
mmcloughlin Dec 15, 2023
d44f3b1
copypasta isla logic into x86
mmcloughlin Dec 15, 2023
a0e811a
attempting to make x64 work
mmcloughlin Dec 19, 2023
63d64e3
first working trace output for x86
mmcloughlin Dec 24, 2023
9358c6b
write x64 traces to files
mmcloughlin Dec 24, 2023
2b24eb5
linearization
mmcloughlin Dec 24, 2023
b68e55b
disable simplify::hide_initialization
mmcloughlin Dec 24, 2023
72fa499
emit: add a selection of instructions
mmcloughlin Dec 27, 2023
f379221
optionally show full traces
mmcloughlin Dec 27, 2023
ba61ba7
update emit tool to use isla options
mmcloughlin Dec 29, 2023
e7897da
support filtering for ITE and struct reads
mmcloughlin Dec 29, 2023
837e59b
post-filter simplify
mmcloughlin Dec 29, 2023
447f355
account for PSTATE register writes
mmcloughlin Dec 29, 2023
0c06bfd
type inference: support "extra" spec variables
mmcloughlin Dec 30, 2023
ad20e6e
isle: printer skeleton
mmcloughlin Dec 30, 2023
d6ee519
isle: type printing
mmcloughlin Dec 30, 2023
8ed0d01
isle: printer supports more things
mmcloughlin Dec 30, 2023
81e1fb6
isle: more printing
mmcloughlin Dec 30, 2023
f491dfb
isle: more spec printing
mmcloughlin Dec 30, 2023
1ff75fc
isle: more printing
mmcloughlin Dec 30, 2023
ba0a01a
isle: print if-let
mmcloughlin Dec 30, 2023
df71a75
basic printer tests
mmcloughlin Dec 30, 2023
1e70a2f
ensure printed isle parses
mmcloughlin Dec 30, 2023
2876e90
alow position tagging to be disabled
mmcloughlin Dec 30, 2023
cda22d8
fix roundtrip errors
mmcloughlin Dec 30, 2023
dc155ce
test against full isle files
mmcloughlin Dec 30, 2023
227989e
start trace to spec translation
mmcloughlin Jan 1, 2024
8745a04
more spec translation
mmcloughlin Jan 1, 2024
493aa3d
even more spec translation
mmcloughlin Jan 1, 2024
475328c
use concat to support arbitrary length bitvectors
mmcloughlin Jan 1, 2024
6ef5e50
handle more spec translation
mmcloughlin Jan 1, 2024
e85162d
isle: support printing of any Printable nodes
mmcloughlin Jan 3, 2024
02a46a7
isle: Errors implement std::error::Error
mmcloughlin Jan 3, 2024
814a67a
emit: print generated spec
mmcloughlin Jan 3, 2024
97e8582
emit: tolerate spec conversion failure
mmcloughlin Jan 3, 2024
73f231f
isaspec adhoc tool for building specs
mmcloughlin Jan 12, 2024
92c6ffd
expend spec config to produce a real spec
mmcloughlin Jan 12, 2024
8e3f5cf
veriisle: specfunc experiment for executing single spec functions
mmcloughlin Jan 17, 2024
31e6ec7
veriisle: exec add function
mmcloughlin Jan 17, 2024
f26b486
isaspec: provide cases
mmcloughlin Jan 26, 2024
3e137e8
generate more alu ops
mmcloughlin Jan 26, 2024
46f554d
keep debug output
mmcloughlin Jan 26, 2024
f7decdd
elide no-op zext
mmcloughlin Jan 26, 2024
79d673c
veriisle: isaspec option to write to file
mmcloughlin Jan 26, 2024
b9da528
isle: parse spec implication operator
mmcloughlin Jan 26, 2024
5281b49
codegen: add inst_specs.isle to aarch64 isle compilation
mmcloughlin Jan 26, 2024
176292f
veriisle: generate instruction specs
mmcloughlin Jan 30, 2024
b5f2b68
verify add lowering to alu_rrr
mmcloughlin Jan 31, 2024
2fe39d3
wip
mmcloughlin Jan 31, 2024
a49bfdf
x64 footprint
mmcloughlin Jan 31, 2024
feaa688
switch back to add rule
mmcloughlin Feb 2, 2024
95f5c4a
restore imp case in spec_op_to_expr
mmcloughlin Feb 18, 2024
8c95834
revert changes to aarch64/inst.isle
mmcloughlin Feb 18, 2024
d1e50b0
remove debug print in widen to register width
mmcloughlin Feb 18, 2024
cfd78d8
wip
mmcloughlin Feb 18, 2024
eee9cff
fix build
mmcloughlin Feb 18, 2024
2100e74
isaspec generates the (= result #b1) condition
mmcloughlin Feb 19, 2024
106d01e
use different prefixes for each instruction case
mmcloughlin Feb 19, 2024
cbc0731
handle the 32-bit case
mmcloughlin Feb 19, 2024
5374323
extend sail spec to all bitwidths
mmcloughlin Feb 19, 2024
7bf9cc4
add more aluops
mmcloughlin Feb 19, 2024
9eba5f6
define isla dependency with git
mmcloughlin Feb 19, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
688 changes: 647 additions & 41 deletions Cargo.lock

Large diffs are not rendered by default.

4 changes: 3 additions & 1 deletion cranelift/codegen/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,8 @@ fn get_isle_compilations(
make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("prelude_opt.isle"));
let prelude_lower_isle =
make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("prelude_lower.isle"));
let inst_specs = make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("inst_specs.isle"));
let inst_specs =
make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("inst_specs.isle"));

// Directory for mid-end optimizations.
let src_opts = make_isle_source_path_relative(&cur_dir, crate_dir.join("src").join("opts"));
Expand Down Expand Up @@ -253,6 +254,7 @@ fn get_isle_compilations(
prelude_lower_isle.clone(),
src_isa_aarch64.join("inst.isle"),
src_isa_aarch64.join("inst_neon.isle"),
src_isa_aarch64.join("inst_specs.isle"),
inst_specs.clone(),
src_isa_aarch64.join("lower.isle"),
src_isa_aarch64.join("lower_dynamic_neon.isle"),
Expand Down
31 changes: 22 additions & 9 deletions cranelift/codegen/src/isa/aarch64/inst.isle
Original file line number Diff line number Diff line change
Expand Up @@ -2018,23 +2018,32 @@
(spec (alu_rrr op t a b)
(provide
(= result (switch op
((ALUOp.Add)
(if (<= t 32)
(zero_ext 64 (bvadd (extract 31 0 a) (extract 31 0 b)))
(bvadd a b)))
((ALUOp.Lsr)
(if (<= t 32)
(conv_to 64 (bvlshr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b))))
(zero_ext 64 (bvlshr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b))))
(bvlshr a (bvand (bvsub (int2bv 64 64) #x0000000000000001) b))))
((ALUOp.Asr)
(if (<= t 32)
(conv_to 64 (bvashr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b))))
(zero_ext 64 (bvashr (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b))))
(bvashr a (bvand (bvsub (int2bv 64 64) #x0000000000000001) b))))
((ALUOp.Lsl)
(if (<= t 32)
(conv_to 64 (bvshl (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b))))
(zero_ext 64 (bvshl (extract 31 0 a) (bvand (bvsub (int2bv 32 32) #x00000001) (extract 31 0 b))))
(bvshl a (bvand (bvsub (int2bv 64 64) #x0000000000000001) b)))))))
(require
(or (= op (ALUOp.Lsr)) (= op (ALUOp.Asr)) (= op (ALUOp.Lsl)))
(or (= t 8) (= t 16) (= t 32) (= t 64))))
(or (= op (ALUOp.Add)) (= op (ALUOp.Lsr)) (= op (ALUOp.Asr)) (= op (ALUOp.Lsl)))
(or (= t 8) (= t 16) (= t 32) (= t 64)))
;(or (= t 32) (= t 64)))
)
(decl alu_rrr (ALUOp Type Reg Reg) Reg)
(rule (alu_rrr op ty src1 src2)
(instantiate alu_rrr
((args (bv 8) Int (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
)
(rule alu_rrr_emit (alu_rrr op ty src1 src2)
(let ((dst WritableReg (temp_writable_reg $I64))
(_ Unit (emit (MInst.AluRRR op (operand_size ty) dst src1 src2))))
dst))
Expand Down Expand Up @@ -2633,10 +2642,14 @@
(provide
(= result
(if (<= ty 32)
(conv_to 64 (bvadd (extract 31 0 a) (extract 31 0 b)))
(bvadd a b)))))
(zero_ext 64 (bvadd (extract 31 0 a) (extract 31 0 b)))
(bvadd a b))))
(require (or (= ty 8) (= ty 16) (= ty 32) (= ty 64))))
(decl add (Type Reg Reg) Reg)
(rule (add ty x y) (alu_rrr (ALUOp.Add) ty x y))
(instantiate add
((args Int (bv 64) (bv 64)) (ret (bv 64)) (canon (bv 64)))
)
(rule add_alu_rrr (add ty x y) (alu_rrr (ALUOp.Add) ty x y))

(spec (add_imm ty a b)
(provide
Expand Down
12 changes: 8 additions & 4 deletions cranelift/codegen/src/isa/aarch64/inst/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,14 +15,14 @@ use smallvec::{smallvec, SmallVec};
use std::fmt::Write;
use std::string::{String, ToString};

pub(crate) mod regs;
pub(crate) use self::regs::*;
pub mod regs;
pub use self::regs::*;
pub mod imms;
pub use self::imms::*;
pub mod args;
pub use self::args::*;
pub mod emit;
pub(crate) use self::emit::*;
pub use self::emit::*;
use crate::isa::aarch64::abi::AArch64MachineDeps;

pub(crate) mod unwind;
Expand Down Expand Up @@ -1191,7 +1191,11 @@ fn mem_finalize_for_show(mem: &AMode, state: &EmitState) -> (String, AMode) {
}

impl Inst {
fn print_with_state(&self, state: &mut EmitState, allocs: &mut AllocationConsumer) -> String {
pub fn print_with_state(
&self,
state: &mut EmitState,
allocs: &mut AllocationConsumer,
) -> String {
let mut empty_allocs = AllocationConsumer::default();

fn op_name(alu_op: ALUOp) -> &'static str {
Expand Down
Loading