isaspec: generate VecRRR spec for Addp opcode (bytecodealliance#187)

Generate the `VecRRR` `Addp` spec case. Updates avanhatt#34 avanhatt#35
wellesley-prog-sys · Oct 23, 2024 · 57fdabb · 57fdabb
1 parent 7b2b067
commit 57fdabb
Show file tree

Hide file tree

Showing 2 changed files with 148 additions and 2 deletions.
diff --git a/cranelift/codegen/src/isa/aarch64/spec/vec_rrr.isle b/cranelift/codegen/src/isa/aarch64/spec/vec_rrr.isle
@@ -0,0 +1,81 @@
+;; GENERATED BY `isaspec`. DO NOT EDIT!!!
+
+(spec
+    (MInst.VecRRR op rd rn rm size)
+    (provide
+        (match
+            size
+            ((Size8x16)
+                (match
+                    op
+                    ((Addp)
+                        (=
+                            rd
+                            (concat
+                                (bvadd (extract 119 112 rm) (extract 127 120 rm))
+                                (concat
+                                    (bvadd (extract 103 96 rm) (extract 111 104 rm))
+                                    (concat
+                                        (bvadd (extract 87 80 rm) (extract 95 88 rm))
+                                        (concat
+                                            (bvadd (extract 71 64 rm) (extract 79 72 rm))
+                                            (concat
+                                                (bvadd (extract 55 48 rm) (extract 63 56 rm))
+                                                (concat
+                                                    (bvadd (extract 39 32 rm) (extract 47 40 rm))
+                                                    (concat
+                                                        (bvadd (extract 23 16 rm) (extract 31 24 rm))
+                                                        (concat
+                                                            (bvadd (extract 7 0 rm) (extract 15 8 rm))
+                                                            (concat
+                                                                (bvadd (extract 119 112 rn) (extract 127 120 rn))
+                                                                (concat
+                                                                    (bvadd (extract 103 96 rn) (extract 111 104 rn))
+                                                                    (concat
+                                                                        (bvadd (extract 87 80 rn) (extract 95 88 rn))
+                                                                        (concat
+                                                                            (bvadd
+                                                                                (extract 71 64 rn)
+                                                                                (extract 79 72 rn))
+                                                                            (concat
+                                                                                (bvadd
+                                                                                    (extract 55 48 rn)
+                                                                                    (extract 63 56 rn))
+                                                                                (concat
+                                                                                    (bvadd
+                                                                                        (extract 39 32 rn)
+                                                                                        (extract 47 40 rn))
+                                                                                    (concat
+                                                                                        (bvadd
+                                                                                            (extract 23 16 rn)
+                                                                                            (extract 31 24 rn))
+                                                                                        (bvadd
+                                                                                            (extract 7 0 rn)
+                                                                                            (extract
+                                                                                                15
+                                                                                                8
+                                                                                                rn)))))))))))))))))))))
+            ((Size8x8)
+                (match
+                    op
+                    ((Addp)
+                        (=
+                            rd
+                            (zero_ext
+                                128
+                                (concat
+                                    (bvadd (extract 55 48 rm) (extract 63 56 rm))
+                                    (concat
+                                        (bvadd (extract 39 32 rm) (extract 47 40 rm))
+                                        (concat
+                                            (bvadd (extract 23 16 rm) (extract 31 24 rm))
+                                            (concat
+                                                (bvadd (extract 7 0 rm) (extract 15 8 rm))
+                                                (concat
+                                                    (bvadd (extract 55 48 rn) (extract 63 56 rn))
+                                                    (concat
+                                                        (bvadd (extract 39 32 rn) (extract 47 40 rn))
+                                                        (concat
+                                                            (bvadd (extract 23 16 rn) (extract 31 24 rn))
+                                                            (bvadd (extract 7 0 rn) (extract 15 8 rn))))))))))))))))
+    (require (match size ((Size8x16) (match op ((Addp) true))) ((Size8x8) (match op ((Addp) true))))))
diff --git a/cranelift/isle/veri/isaspec/src/bin/isaspec.rs b/cranelift/isle/veri/isaspec/src/bin/isaspec.rs
@@ -7,8 +7,8 @@ use anyhow::{bail, Result};
 use clap::Parser as ClapParser;
 use cranelift_codegen::ir::types::I8;
 use cranelift_codegen::isa::aarch64::inst::{
-    vreg, writable_vreg, MoveWideConst, MoveWideOp, SImm9, ScalarSize, UImm12Scaled, VecLanesOp,
-    VecMisc2, VectorSize, NZCV,
+    vreg, writable_vreg, MoveWideConst, MoveWideOp, SImm9, ScalarSize, UImm12Scaled, VecALUOp,
+    VecLanesOp, VecMisc2, VectorSize, NZCV,
 };
 use cranelift_codegen::{
     ir::MemFlags,
@@ -174,6 +174,10 @@ fn define() -> Result<Vec<FileConfig>> {
             name: "mov_from_vec.isle".into(),
             specs: vec![define_mov_from_vec()],
         },
+        FileConfig {
+            name: "vec_rrr.isle".into(),
+            specs: vec![define_vec_rrr()],
+        },
         FileConfig {
             name: "vec_misc.isle".into(),
             specs: vec![define_vec_misc()],
@@ -1844,6 +1848,67 @@ fn define_mov_from_vec() -> SpecConfig {
     }
 }
 
+// MInst.VecRRR specification configuration.
+fn define_vec_rrr() -> SpecConfig {
+    // VecALUOp
+    let vec_alu_ops = [VecALUOp::Addp];
+
+    // VectorSize
+    let sizes = [VectorSize::Size8x8, VectorSize::Size8x16];
+
+    // VecRRR
+    let mut mappings = Mappings::default();
+    mappings.writes.insert(
+        aarch64::vreg(4),
+        Mapping::require(spec_var("rd".to_string())),
+    );
+    mappings.reads.insert(
+        aarch64::vreg(5),
+        Mapping::require(spec_var("rn".to_string())),
+    );
+    mappings.reads.insert(
+        aarch64::vreg(6),
+        Mapping::require(spec_var("rm".to_string())),
+    );
+
+    SpecConfig {
+        term: "MInst.VecRRR".to_string(),
+        args: ["op", "rd", "rn", "rm", "size"].map(String::from).to_vec(),
+
+        cases: Cases::Match(Match {
+            on: spec_var("size".to_string()),
+            arms: sizes
+                .iter()
+                .rev()
+                .map(|size| Arm {
+                    variant: format!("{size:?}"),
+                    args: Vec::new(),
+                    body: Cases::Match(Match {
+                        on: spec_var("op".to_string()),
+                        arms: vec_alu_ops
+                            .iter()
+                            .map(|op| Arm {
+                                variant: format!("{op:?}"),
+                                args: Vec::new(),
+                                body: Cases::Instruction(InstConfig {
+                                    opcodes: Opcodes::Instruction(Inst::VecRRR {
+                                        alu_op: *op,
+                                        rd: writable_vreg(4),
+                                        rn: vreg(5),
+                                        rm: vreg(6),
+                                        size: *size,
+                                    }),
+                                    scope: aarch64::state(),
+                                    mappings: mappings.clone(),
+                                }),
+                            })
+                            .collect(),
+                    }),
+                })
+                .collect(),
+        }),
+    }
+}
 // MInst.VecMisc specification configuration.
 fn define_vec_misc() -> SpecConfig {
     // VecMisc2