diff --git a/cranelift/codegen/src/isa/aarch64/spec/conds.isle b/cranelift/codegen/src/isa/aarch64/spec/conds.isle new file mode 100644 index 000000000000..d080ae4e0515 --- /dev/null +++ b/cranelift/codegen/src/isa/aarch64/spec/conds.isle @@ -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)))) diff --git a/cranelift/isle/veri/isaspec/src/bin/isaspec.rs b/cranelift/isle/veri/isaspec/src/bin/isaspec.rs index e79210e1af3c..9ff309facb81 100644 --- a/cranelift/isle/veri/isaspec/src/bin/isaspec.rs +++ b/cranelift/isle/veri/isaspec/src/bin/isaspec.rs @@ -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, @@ -148,6 +148,10 @@ fn define() -> Result> { name: "extend.isle".into(), specs: vec![define_extend()], }, + FileConfig { + name: "conds.isle".into(), + specs: define_conds(), + }, ]) } @@ -1114,6 +1118,91 @@ where } } +fn define_conds() -> Vec { + // 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(term: &str, inst: F) -> SpecConfig +where + F: Fn(Writable, 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();