Skip to content

Commit

Permalink
isaspec: generate AluRRImm12 spec (bytecodealliance#118)
Browse files Browse the repository at this point in the history 
Generate `AluRRImm12` spec from ASLp.

This is the first requiring symbolic opcodes, so there are substantial
changes to support it:

* Updates ASLp dependency to fork containing experimental symbolic
opcode support
mmcloughlin/aslp@e5190a0
* Introduces `Bits` type to `isaspec` for manipulating opcode bitvectors
with symbolic fields.
* Generating ASLp semantics from an opcode template
* Validating an assembly template against the Cranelift assembler
* Updating verification model of `Imm12` to a struct type, and updating
related specs.

Updates avanhatt#36 avanhatt#35
  • Loading branch information
@mmcloughlin
mmcloughlin authored Oct 5, 2024
1 parent 6f507bf commit 7a4a0d1
Show file tree
Hide file tree
Showing 13 changed files with 656 additions and 219 deletions.
90 changes: 40 additions & 50 deletions cranelift/codegen/src/isa/aarch64/inst.isle
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1072,43 +1072,6 @@
)
)

(spec (MInst.AluRRImm12 alu_op size rd rn imm12)
(provide
(=>
(and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size64)))
(= rd (bvadd rn (zero_ext 64 imm12)))
)
(=>
(and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size32)))
(= rd (conv_to 64 (bvadd (extract 31 0 rn) (zero_ext 32 imm12))))
)

(=>
(and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size64)))
(= rd (bvsub rn (zero_ext 64 imm12)))
)
(=>
(and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size32)))
(= rd (conv_to 64 (bvsub (extract 31 0 rn) (zero_ext 32 imm12))))
)
)
(require
; Implemented (opcode, size) combinations.
(or
(and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size64)))
(and (= alu_op (ALUOp.Add)) (= size (OperandSize.Size32)))

(and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size64)))
(and (= alu_op (ALUOp.Sub)) (= size (OperandSize.Size32)))
)
; Imm12 immediate is well-formed.
(or
(= imm12 (bvand imm12 #x000fff))
(= imm12 (bvand imm12 #xfff000))
)
)
)

(spec (MInst.AluRRImmLogic alu_op size rd rn imml)
(provide
(=>
Expand Down Expand Up @@ -1298,8 +1261,17 @@
))

(type UImm5 (primitive UImm5))

(type Imm12 (primitive Imm12))
(model Imm12 (type (bv 24)))
(model Imm12
(type
(struct
(bits (bv 12))
(shift12 Bool)
)
)
)

(type ImmLogic (primitive ImmLogic))
; Note: ImmLogic values can be 32 or 64 bit.
; QUESTION(mbm): do we want to support "polymorphic" models: (model ImmLogic (type (poly (bv 32) (bv 64))))
Expand Down Expand Up @@ -2034,12 +2006,20 @@
(decl imm12_from_u64 (Imm12) u64)
(extern extractor imm12_from_u64 imm12_from_u64)
(spec (imm12_from_u64 imm12)
(provide (= result (zero_ext 64 imm12)))
(provide
(= result
(zero_ext 64
(if (:shift12 imm12)
(concat (:bits imm12) #x000)
(concat #x000 (:bits imm12))
)
)
)
)
(require
; REVIEW(mbm): correct formulation of imm12?
(or
(= imm12 (bvand imm12 #x000fff))
(= imm12 (bvand imm12 #xfff000))
(= result (bvand result (zero_ext 64 #x000fff)))
(= result (bvand result (zero_ext 64 #xfff000)))
)
)
)
Expand Down Expand Up @@ -2121,18 +2101,28 @@
(extern constructor is_zero_uimm12 is_zero_uimm12)

;; Helper to go directly from a `Value`, when it's an `iconst`, to an `Imm12`.
; REVIEW(mbm): is imm12_from_value spec correct?
; NOTE(mbm): compare with https://github.com/avanhatt/wasmtime/blob/94ccb9d4d55a479893cb04bc796ec620ed24cee2/cranelift/codegen/src/isa/aarch64/inst.isle#L1867-L1874
(spec (imm12_from_value imm12)
(provide
; REVIEW(mbm): zero_ext vs conv_to?
(= (zero_ext 128 result) (zero_ext 128 imm12))
(=
(zero_ext 128 result)
(zero_ext 128
(if (:shift12 imm12)
(concat (:bits imm12) #x000)
(concat #x000 (:bits imm12))
)
)
)
)
(require
; REVIEW(mbm): correct formulation of imm12?
(or
(= imm12 (bvand imm12 #x000fff))
(= imm12 (bvand imm12 #xfff000))
(let
(
(width 128)
(r (zero_ext width result))
)
(or
(= r (bvand r (zero_ext width #x000fff)))
(= r (bvand r (zero_ext width #xfff000)))
)
)
)
)
Expand Down
86 changes: 86 additions & 0 deletions cranelift/codegen/src/isa/aarch64/spec/alu_rr_imm12.isle
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
;; GENERATED BY `isaspec`. DO NOT EDIT!!!

(spec
(MInst.AluRRImm12 alu_op size rd rn imm12)
(provide
(match
size
((Size64)
(match
alu_op
((Add)
(and
(=> (not (:shift12 imm12)) (= rd (bvadd rn (zero_ext 64 (extract 11 0 (:bits imm12))))))
(=>
(:shift12 imm12)
(= rd (bvadd rn (zero_ext 64 (concat (extract 11 0 (:bits imm12)) #x000)))))))
((Sub)
(and
(=>
(not (:shift12 imm12))
(=
rd
(bvadd
(bvadd rn (bvnot (zero_ext 64 (extract 11 0 (:bits imm12)))))
#x0000000000000001)))
(=>
(:shift12 imm12)
(=
rd
(bvadd
(bvadd rn (bvnot (zero_ext 64 (concat (extract 11 0 (:bits imm12)) #x000))))
#x0000000000000001)))))))
((Size32)
(match
alu_op
((Add)
(and
(=>
(not (:shift12 imm12))
(=
rd
(zero_ext 64 (bvadd (extract 31 0 rn) (zero_ext 32 (extract 11 0 (:bits imm12)))))))
(=>
(:shift12 imm12)
(=
rd
(zero_ext
64
(bvadd
(extract 31 0 rn)
(zero_ext 32 (concat (extract 11 0 (:bits imm12)) #x000))))))))
((Sub)
(and
(=>
(not (:shift12 imm12))
(=
rd
(zero_ext
64
(bvadd
(bvadd (extract 31 0 rn) (bvnot (zero_ext 32 (extract 11 0 (:bits imm12)))))
#x00000001))))
(=>
(:shift12 imm12)
(=
rd
(zero_ext
64
(bvadd
(bvadd
(extract 31 0 rn)
(bvnot (zero_ext 32 (concat (extract 11 0 (:bits imm12)) #x000))))
#x00000001))))))))))
(require
(match
size
((Size64)
(match
alu_op
((Add) (or (not (:shift12 imm12)) (:shift12 imm12)))
((Sub) (or (not (:shift12 imm12)) (:shift12 imm12)))))
((Size32)
(match
alu_op
((Add) (or (not (:shift12 imm12)) (:shift12 imm12)))
((Sub) (or (not (:shift12 imm12)) (:shift12 imm12))))))))
126 changes: 0 additions & 126 deletions cranelift/isle/veri/aslp/src/bits.rs
View file

This file was deleted.

4 changes: 2 additions & 2 deletions cranelift/isle/veri/aslp/src/client.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use reqwest::IntoUrl;
use serde::Deserialize;
use tracing::debug;

use crate::{ast::Block, bits::Bits, parser};
use crate::{ast::Block, opcode::Opcode, parser};

pub struct Client<'a> {
client: &'a reqwest::blocking::Client,
Expand All @@ -18,7 +18,7 @@ impl<'a> Client<'a> {
})
}

pub fn opcode(&self, opcode: Bits) -> Result<Block> {
pub fn opcode(&self, opcode: Opcode) -> Result<Block> {
// Model for response JSON data.
#[derive(Deserialize, Debug)]
struct Response {
Expand Down
2 changes: 1 addition & 1 deletion cranelift/isle/veri/aslp/src/lib.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
pub mod ast;
pub mod bits;
pub mod client;
pub mod opcode;
pub mod parser;
Loading

0 comments on commit 7a4a0d1

Please sign in to comment.