Skip to content

Commit

Permalink
isaspec: generate MovWide spec (bytecodealliance#127)
Browse files Browse the repository at this point in the history
Generate `MovWide` spec.

Updates avanhatt#36 avanhatt#35
  • Loading branch information
mmcloughlin authored Oct 9, 2024
1 parent f31bc1c commit 7659774
Show file tree
Hide file tree
Showing 3 changed files with 204 additions and 1 deletion.
60 changes: 60 additions & 0 deletions cranelift/codegen/src/isa/aarch64/spec/mov_wide.isle
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
;; GENERATED BY `isaspec`. DO NOT EDIT!!!

(spec
(MInst.MovWide op rd imm size)
(provide
(match
size
((Size64)
(match
op
((MovZ)
(and
(=> (= (:shift imm) #b00) (= rd (zero_ext 64 (extract 15 0 (:bits imm)))))
(=> (= (:shift imm) #b01) (= rd (zero_ext 64 (concat (extract 15 0 (:bits imm)) #x0000))))
(=>
(= (:shift imm) #b10)
(= rd (zero_ext 64 (concat (extract 15 0 (:bits imm)) #x00000000))))
(=> (= (:shift imm) #b11) (= rd (concat (extract 15 0 (:bits imm)) #x000000000000)))))
((MovN)
(and
(=> (= (:shift imm) #b00) (= rd (bvnot (zero_ext 64 (extract 15 0 (:bits imm))))))
(=>
(= (:shift imm) #b01)
(= rd (bvnot (zero_ext 64 (concat (extract 15 0 (:bits imm)) #x0000)))))
(=>
(= (:shift imm) #b10)
(= rd (bvnot (zero_ext 64 (concat (extract 15 0 (:bits imm)) #x00000000)))))
(=>
(= (:shift imm) #b11)
(= rd (bvnot (concat (extract 15 0 (:bits imm)) #x000000000000))))))))
((Size32)
(match
op
((MovZ)
(and
(=> (= (:shift imm) #b00) (= rd (zero_ext 64 (extract 15 0 (:bits imm)))))
(=> (= (:shift imm) #b01) (= rd (zero_ext 64 (concat (extract 15 0 (:bits imm)) #x0000))))))
((MovN)
(and
(=>
(= (:shift imm) #b00)
(= rd (zero_ext 64 (bvnot (zero_ext 32 (extract 15 0 (:bits imm)))))))
(=>
(= (:shift imm) #b01)
(= rd (zero_ext 64 (bvnot (concat (extract 15 0 (:bits imm)) #x0000)))))))))))
(require
(match
size
((Size64)
(match
op
((MovZ)
(or (= (:shift imm) #b00) (= (:shift imm) #b01) (= (:shift imm) #b10) (= (:shift imm) #b11)))
((MovN)
(or (= (:shift imm) #b00) (= (:shift imm) #b01) (= (:shift imm) #b10) (= (:shift imm) #b11)))))
((Size32)
(match
op
((MovZ) (or (= (:shift imm) #b00) (= (:shift imm) #b01)))
((MovN) (or (= (:shift imm) #b00) (= (:shift imm) #b01))))))))
22 changes: 21 additions & 1 deletion cranelift/isle/veri/isaspec/src/bin/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ use clap::Parser as ClapParser;
use cranelift_codegen::ir::types::I64;
use cranelift_codegen::isa::aarch64::inst::{
vreg, writable_vreg, writable_xreg, xreg, ALUOp, ALUOp3, BitOp, Cond, Imm12, ImmLogic,
ImmShift, Inst, OperandSize, ShiftOp, ShiftOpAndAmt, ShiftOpShiftImm, VecALUOp, VectorSize,
ImmShift, Inst, MoveWideConst, MoveWideOp, OperandSize, ShiftOp, ShiftOpAndAmt,
ShiftOpShiftImm, VecALUOp, VectorSize,
};
use cranelift_isle::printer;
use cranelift_isle_veri_aslp::ast::Block;
Expand Down Expand Up @@ -68,6 +69,9 @@ fn main() -> Result<()> {
fn define_insts() -> Vec<Inst> {
let mut insts = Vec::new();

// OperandSize
let sizes = [OperandSize::Size32, OperandSize::Size64];

// AluRRR
let alu_ops = vec![
ALUOp::Add,
Expand Down Expand Up @@ -203,6 +207,22 @@ fn define_insts() -> Vec<Inst> {
});
}

// MovWide
let mov_wide_ops = [MoveWideOp::MovN, MoveWideOp::MovZ];
let values = [0x00001234u64, 0x12340000u64];
for mov_wide_op in mov_wide_ops {
for size in sizes {
for value in values {
insts.push(Inst::MovWide {
op: mov_wide_op,
rd: writable_xreg(4),
imm: MoveWideConst::maybe_from_u64(value).unwrap(),
size,
});
}
}
}

// CSel
let conds = vec![
Cond::Eq,
Expand Down
123 changes: 123 additions & 0 deletions cranelift/isle/veri/isaspec/src/bin/isaspec.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ use std::{io, vec};

use anyhow::{bail, Result};
use clap::Parser as ClapParser;
use cranelift_codegen::isa::aarch64::inst::{MoveWideConst, MoveWideOp};
use cranelift_codegen::{
ir::MemFlags,
isa::aarch64::inst::{
Expand Down Expand Up @@ -144,6 +145,10 @@ fn define() -> Result<Vec<FileConfig>> {
name: "loads.isle".into(),
specs: define_loads(),
},
FileConfig {
name: "mov_wide.isle".into(),
specs: vec![define_mov_wide()?],
},
FileConfig {
name: "extend.isle".into(),
specs: vec![define_extend()],
Expand Down Expand Up @@ -821,6 +826,124 @@ fn define_bit_rr() -> SpecConfig {
}
}

// MInst.MovWide specification configuration.
fn define_mov_wide() -> Result<SpecConfig> {
// MovWideOps
let mov_wide_ops = [MoveWideOp::MovZ, MoveWideOp::MovN];

// OperandSize
let sizes = [OperandSize::Size32, OperandSize::Size64];

// Execution scope: define opcode template fields.
let mut scope = aarch64::state();
let mov_wide_const_bits = Target::Var("bits".to_string());
scope.global(mov_wide_const_bits.clone());

// Mappings
let mut mappings = Mappings::default();
mappings.writes.insert(
aarch64::gpreg(4),
Mapping::require(spec_var("rd".to_string())),
);
mappings.reads.insert(
mov_wide_const_bits.clone(),
MappingBuilder::var("imm").field("bits").build(),
);

Ok(SpecConfig {
term: "MInst.MovWide".to_string(),
args: ["op", "rd", "imm", "size"].map(String::from).to_vec(),
cases: Cases::Match(Match {
on: spec_var("size".to_string()),
arms: sizes
.iter()
.rev()
.map(|size| {
let max_shift = size.bits() / 16;
Ok(Arm {
variant: format!("{size:?}"),
args: Vec::new(),
body: Cases::Match(Match {
on: spec_var("op".to_string()),
arms: mov_wide_ops
.iter()
.map(|mov_wide_op| {
Ok(Arm {
variant: format!("{mov_wide_op:?}"),
args: Vec::new(),
body: Cases::Cases(
(0..max_shift)
.map(|shift| {
let template = mov_wide_template(
*mov_wide_op,
writable_xreg(4),
shift,
*size,
)?;
Ok(Case {
conds: vec![spec_eq(
spec_field(
"shift".to_string(),
spec_var("imm".to_string()),
),
spec_const_bit_vector(shift.into(), 2),
)],
cases: Cases::Instruction(InstConfig {
opcodes: Opcodes::Template(template),
scope: scope.clone(),
mappings: mappings.clone(),
}),
})
})
.collect::<Result<_>>()?,
),
})
})
.collect::<Result<_>>()?,
}),
})
})
.collect::<Result<_>>()?,
}),
})
}

fn mov_wide_template(
op: MoveWideOp,
rd: Writable<Reg>,
shift: u8,
size: OperandSize,
) -> Result<Bits> {
// Assemble a base instruction with a placeholder for the immediate bits field.
let placeholder = MoveWideConst { bits: 0, shift };
let base = Inst::MovWide {
op,
rd,
imm: placeholder,
size,
};
let opcode = aarch64::opcode(&base);
let bits = Bits::from_u32(opcode);

// Splice in symbolic immediate fields.
let imm = Bits {
segments: vec![Segment::Symbolic("bits".to_string(), 16)],
};
let template = Bits::splice(&bits, &imm, 5)?;

// Verify template against the assembler.
verify_opcode_template(&template, |assignment: &HashMap<String, u32>| {
let bits = assignment.get("bits").unwrap();
let imm = MoveWideConst {
bits: (*bits).try_into().unwrap(),
shift,
};
Ok(Inst::MovWide { op, rd, imm, size })
})?;

Ok(template)
}

fn define_extend() -> SpecConfig {
// Extend
let signed = [false, true];
Expand Down

0 comments on commit 7659774

Please sign in to comment.