Skip to content

Commit

Permalink
isaspec: generate conditional selects (bytecodealliance#126)
Browse files Browse the repository at this point in the history 
Generate conditional select instructions `CSel` and `CSNeg`.

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

(spec
(MInst.CSel rd cond rn rm)
(provide
(match
cond
((Le)
(with
(t3 t5 t7)
(and
(=
t3
(not
(and
(= (:N (:flags_in result)) (:V (:flags_in result)))
(= (:Z (:flags_in result)) #b0))))
(if t3 (= t5 rn) (= t7 rm))
(= rd (if t3 t5 t7)))))
((Gt)
(with
(t3 t5 t7)
(and
(= t3 (and (= (:N (:flags_in result)) (:V (:flags_in result))) (= (:Z (:flags_in result)) #b0)))
(if t3 (= t5 rn) (= t7 rm))
(= rd (if t3 t5 t7)))))
((Lt)
(with
(t2 t4 t6)
(and
(= t2 (not (= (:N (:flags_in result)) (:V (:flags_in result)))))
(if t2 (= t4 rn) (= t6 rm))
(= rd (if t2 t4 t6)))))
((Ge)
(with
(t2 t4 t6)
(and
(= t2 (= (:N (:flags_in result)) (:V (:flags_in result))))
(if t2 (= t4 rn) (= t6 rm))
(= rd (if t2 t4 t6)))))
((Ls)
(with
(t2 t4 t6)
(and
(= t2 (not (and (= (:C (:flags_in result)) #b1) (= (:Z (:flags_in result)) #b0))))
(if t2 (= t4 rn) (= t6 rm))
(= rd (if t2 t4 t6)))))
((Hi)
(with
(t2 t4 t6)
(and
(= t2 (and (= (:C (:flags_in result)) #b1) (= (:Z (:flags_in result)) #b0)))
(if t2 (= t4 rn) (= t6 rm))
(= rd (if t2 t4 t6)))))
((Vc)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:V (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 rm))
(= rd (if t1 t3 t5)))))
((Vs)
(with
(t1 t3 t5)
(and (= t1 (= (:V (:flags_in result)) #b1)) (if t1 (= t3 rn) (= t5 rm)) (= rd (if t1 t3 t5)))))
((Pl)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:N (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 rm))
(= rd (if t1 t3 t5)))))
((Mi)
(with
(t1 t3 t5)
(and (= t1 (= (:N (:flags_in result)) #b1)) (if t1 (= t3 rn) (= t5 rm)) (= rd (if t1 t3 t5)))))
((Lo)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:C (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 rm))
(= rd (if t1 t3 t5)))))
((Hs)
(with
(t1 t3 t5)
(and (= t1 (= (:C (:flags_in result)) #b1)) (if t1 (= t3 rn) (= t5 rm)) (= rd (if t1 t3 t5)))))
((Ne)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:Z (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 rm))
(= rd (if t1 t3 t5)))))
((Eq)
(with
(t1 t3 t5)
(and (= t1 (= (:Z (:flags_in result)) #b1)) (if t1 (= t3 rn) (= t5 rm)) (= rd (if t1 t3 t5)))))))
(require
(match
cond
((Le) true)
((Gt) true)
((Lt) true)
((Ge) true)
((Ls) true)
((Hi) true)
((Vc) true)
((Vs) true)
((Pl) true)
((Mi) true)
((Lo) true)
((Hs) true)
((Ne) true)
((Eq) true))))

(spec
(MInst.CSNeg rd cond rn rm)
(provide
(match
cond
((Le)
(with
(t3 t5 t7)
(and
(=
t3
(not
(and
(= (:N (:flags_in result)) (:V (:flags_in result)))
(= (:Z (:flags_in result)) #b0))))
(if t3 (= t5 rn) (= t7 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t3 t5 t7)))))
((Gt)
(with
(t3 t5 t7)
(and
(= t3 (and (= (:N (:flags_in result)) (:V (:flags_in result))) (= (:Z (:flags_in result)) #b0)))
(if t3 (= t5 rn) (= t7 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t3 t5 t7)))))
((Lt)
(with
(t2 t4 t6)
(and
(= t2 (not (= (:N (:flags_in result)) (:V (:flags_in result)))))
(if t2 (= t4 rn) (= t6 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t2 t4 t6)))))
((Ge)
(with
(t2 t4 t6)
(and
(= t2 (= (:N (:flags_in result)) (:V (:flags_in result))))
(if t2 (= t4 rn) (= t6 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t2 t4 t6)))))
((Ls)
(with
(t2 t4 t6)
(and
(= t2 (not (and (= (:C (:flags_in result)) #b1) (= (:Z (:flags_in result)) #b0))))
(if t2 (= t4 rn) (= t6 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t2 t4 t6)))))
((Hi)
(with
(t2 t4 t6)
(and
(= t2 (and (= (:C (:flags_in result)) #b1) (= (:Z (:flags_in result)) #b0)))
(if t2 (= t4 rn) (= t6 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t2 t4 t6)))))
((Vc)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:V (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))
((Vs)
(with
(t1 t3 t5)
(and
(= t1 (= (:V (:flags_in result)) #b1))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))
((Pl)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:N (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))
((Mi)
(with
(t1 t3 t5)
(and
(= t1 (= (:N (:flags_in result)) #b1))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))
((Lo)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:C (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))
((Hs)
(with
(t1 t3 t5)
(and
(= t1 (= (:C (:flags_in result)) #b1))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))
((Ne)
(with
(t1 t3 t5)
(and
(= t1 (not (= (:Z (:flags_in result)) #b1)))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))
((Eq)
(with
(t1 t3 t5)
(and
(= t1 (= (:Z (:flags_in result)) #b1))
(if t1 (= t3 rn) (= t5 (bvadd (bvnot rm) #x0000000000000001)))
(= rd (if t1 t3 t5)))))))
(require
(match
cond
((Le) true)
((Gt) true)
((Lt) true)
((Ge) true)
((Ls) true)
((Hi) true)
((Vc) true)
((Vs) true)
((Pl) true)
((Mi) true)
((Lo) true)
((Hs) true)
((Ne) true)
((Eq) true))))
93 changes: 91 additions & 2 deletions cranelift/isle/veri/isaspec/src/bin/isaspec.rs
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
use std::collections::HashMap;
use std::io;
use std::io::Write;
use std::path::{Path, PathBuf};
use std::{io, vec};

use anyhow::{bail, Result};
use clap::Parser as ClapParser;
use cranelift_codegen::{
ir::MemFlags,
isa::aarch64::inst::{
writable_xreg, xreg, ALUOp, ALUOp3, AMode, BitOp, ExtendOp, Imm12, Inst, OperandSize,
writable_xreg, xreg, ALUOp, ALUOp3, AMode, BitOp, Cond, ExtendOp, Imm12, Inst, OperandSize,
ShiftOp, ShiftOpAndAmt, ShiftOpShiftImm,
},
Reg, Writable,
Expand Down Expand Up @@ -148,6 +148,10 @@ fn define() -> Result<Vec<FileConfig>> {
name: "extend.isle".into(),
specs: vec![define_extend()],
},
FileConfig {
name: "conds.isle".into(),
specs: define_conds(),
},
])
}

Expand Down Expand Up @@ -1114,6 +1118,91 @@ where
}
}

fn define_conds() -> Vec<SpecConfig> {
// CSel
let csel = define_csel("MInst.CSel", |rd, cond, rn, rm| Inst::CSel {
rd,
cond,
rn,
rm,
});

// CSNeg
let csneg = define_csel("MInst.CSNeg", |rd, cond, rn, rm| Inst::CSNeg {
rd,
cond,
rn,
rm,
});

vec![csel, csneg]
}

fn define_csel<F>(term: &str, inst: F) -> SpecConfig
where
F: Fn(Writable<Reg>, Cond, Reg, Reg) -> Inst,
{
// Cond
let conds = [
Cond::Eq,
Cond::Ne,
Cond::Hs,
Cond::Lo,
Cond::Mi,
Cond::Pl,
Cond::Vs,
Cond::Vc,
Cond::Hi,
Cond::Ls,
Cond::Ge,
Cond::Lt,
Cond::Gt,
Cond::Le,
];

// Flags and register mappings.
let mut mappings = flags_mappings();
mappings.writes.insert(
aarch64::gpreg(4),
Mapping::require(spec_var("rd".to_string())),
);
mappings.reads.insert(
aarch64::gpreg(5),
Mapping::require(spec_var("rn".to_string())),
);
mappings.reads.insert(
aarch64::gpreg(6),
Mapping::require(spec_var("rm".to_string())),
);

SpecConfig {
term: term.to_string(),
args: ["rd", "cond", "rn", "rm"].map(String::from).to_vec(),

cases: Cases::Match(Match {
on: spec_var("cond".to_string()),
arms: conds
.iter()
.rev()
.map(|cond| Arm {
variant: format!("{cond:?}"),
args: Vec::new(),
body: Cases::Instruction(InstConfig {
opcodes: Opcodes::Instruction(inst(
writable_xreg(4),
*cond,
xreg(5),
xreg(6),
)),
scope: aarch64::state(),
mappings: mappings.clone(),
}),
})
.collect(),
}),
}
}

fn flags_mappings() -> Mappings {
// Instruction model is the MInst value itself, which is considered the result of the variant term.
let inst = MappingBuilder::var("result").allow();
Expand Down

0 comments on commit f31bc1c

Please sign in to comment.