Skip to content

Shifts: ishr, sshr, ushr #49

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
avanhatt wants to merge 13 commits into from
Closed

Shifts: ishr, sshr, ushr #49

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
7009d8d
rebase
avanhatt Jan 23, 2023
06b347a
fix width extraction
avanhatt Jan 23, 2023
02284ee
fix extract
avanhatt Jan 23, 2023
5ab5643
more tests, some currently failing
avanhatt Jan 24, 2023
2bd6174
examples
avanhatt Jan 24, 2023
87767e6
more examples
avanhatt Jan 24, 2023
0728dcb
rest of examples
avanhatt Jan 24, 2023
f03b460
more tests
avanhatt Jan 24, 2023
ff5f5db
broken not whats expected
avanhatt Jan 24, 2023
a48b006
wip
avanhatt Jan 25, 2023
6688516
broken
avanhatt Jan 25, 2023
5a6e5fc
Merge branch 'verify-main' into shifts-rebase
avanhatt Jan 31, 2023
7e537f2
Merge branch 'verify-main' into shifts-rebase
avanhatt Mar 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1,917 changes: 0 additions & 1,917 deletions cranelift/codegen/isle_generated_code/clif_opt.isle
View file
Open in desktop

This file was deleted.

17,009 changes: 0 additions & 17,009 deletions cranelift/codegen/isle_generated_code/isle_aarch64.rs
View file
Open in desktop

This file was deleted.

5,544 changes: 0 additions & 5,544 deletions cranelift/codegen/isle_generated_code/isle_opt.rs
View file
Open in desktop

This file was deleted.

8,014 changes: 0 additions & 8,014 deletions cranelift/codegen/isle_generated_code/isle_riscv64.rs
View file
Open in desktop

This file was deleted.

30,872 changes: 0 additions & 30,872 deletions cranelift/codegen/isle_generated_code/isle_s390x.rs
View file
Open in desktop

This file was deleted.

18,835 changes: 0 additions & 18,835 deletions cranelift/codegen/isle_generated_code/isle_x64.rs
View file
Open in desktop

This file was deleted.

8 changes: 7 additions & 1 deletion cranelift/codegen/src/clif_lower.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -695,7 +695,7 @@
)

;;@ (spec (sig (args arg) (ret))
;;@ (assertions (= (zero_ext (widthof (arg)) (ret)) (arg))))
;;@ (assertions (= (zero_ext (widthof (arg)) (ret)) (arg))))
(decl iconst (Imm64) Inst)
(extractor
(iconst N)
Expand Down Expand Up @@ -1073,12 +1073,18 @@
(inst_data (InstructionData.Binary (Opcode.Ishl) (value_array_2 x y)))
)

;;@ (spec (sig (args a, b) (ret))
;;@ (assertions (<= (bv2int (b)) (widthof (a))),
;;@ (= (ret) (shr (a) (b)))))
(decl ushr (Value Value) Inst)
(extractor
(ushr x y)
(inst_data (InstructionData.Binary (Opcode.Ushr) (value_array_2 x y)))
)

;;@ (spec (sig (args a, b) (ret))
;;@ (assertions (<= (bv2int (b)) (widthof (a))),
;;@ (= (ret) (ashr (a) (b)))))
(decl sshr (Value Value) Inst)
(extractor
(sshr x y)
Expand Down
8 changes: 8 additions & 0 deletions cranelift/isle/veri/veri_annotation/tests/parser_test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,14 @@ fn test_expr() {
assert!(parser::ExprParser::new()
.parse("(if (a) {(+ (b) (c))} else {(d)})")
.is_ok());

// nested conditionals
assert!(parser::ExprParser::new()
.parse("(if (a) {(+ (if (x) {(+ (b) (c))} else {(d)}) (c))} else {(d)})")
.is_ok());
assert!(parser::ExprParser::new()
.parse("(if (<= (t) (32i8: isleType)) {(32i8: isleType)} else {(64i8: isleType)})")
.is_ok());
}

#[test]
Expand Down
104 changes: 104 additions & 0 deletions cranelift/isle/veri/veri_engine/examples/broken/shifts/broken_do_shift_32.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
;; Instruction formats.
(type MInst
(enum
))

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (0i64:bv) (ret))))
;;decl ALUOp.Lsl

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (1i64:bv) (ret))))
;;decl ALUOp.Lsr

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (2i64:bv) (ret))))
;;decl ALUOp.Asr

;; An ALU operation. This can be paired with several instruction formats
;; below (see `Inst`) in any combination.
(type ALUOp
(enum
(Add)
(Sub)
(Orr)
(OrrNot)
(And)
(AndS)
(AndNot)
;; XOR (AArch64 calls this "EOR")
(Eor)
;; XNOR (AArch64 calls this "EOR-NOT")
(EorNot)
;; Add, setting flags
(AddS)
;; Sub, setting flags
(SubS)
;; Signed multiply, high-word result
(SMulH)
;; Unsigned multiply, high-word result
(UMulH)
(SDiv)
(UDiv)
(RotR)
(Lsr)
(Asr)
(Lsl)
;; Add with carry
(Adc)
;; Add with carry, settings flags
(AdcS)
;; Subtract with carry
(Sbc)
;; Subtract with carry, settings flags
(SbcS)
))

;; BROKEN: no restriction on op in annotation
;;@ (spec (sig (args op, t, a, b) (ret))
;;@ (assertions (if (= (op) (0i64:bv)) {
;;@ (= (ret) (shl (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (1i64:bv)) {
;;@ (= (ret) (shr (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (2i64:bv)) {
;;@ (= (ret) (ashr (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (= (ret) (64i64:bv))
;;@ })
;;@ })
;;@ }),
;;@ (|| (= (t) (1i8: isleType))
;;@ (|| (= (t) (8i8: isleType))
;;@ (|| (= (t) (16i8: isleType))
;;@ (|| (= (t) (32i8: isleType))
;;@ (= (t) (64i8: isleType))))))
;;@ ))
(decl do_shift (ALUOp Type Reg Value) Reg)

;; BROKEN: no restriction on op in annotation
;;@ (spec (sig (args op, t, a, b) (ret))
;;@ (assertions (if (= (op) (0i64:bv)) {
;;@ (= (ret) (shl (conv_to (if (<= (t) (32i8: isleType)) {(32i8: isleType)} else {(64i8: isleType)}) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (1i64:bv)) {
;;@ (= (ret) (shr (conv_to (if (<= (t) (32i8: isleType)) {(32i8: isleType)} else {(64i8: isleType)}) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (2i64:bv)) {
;;@ (= (ret) (ashr (conv_to (if (<= (t) (32i8: isleType)) {(32i8: isleType)} else {(64i8: isleType)}) (a)) (b)))
;;@ } else {
;;@ (= (ret) (0i64:bv))
;;@ })
;;@ })
;;@ }),
;;@ (|| (= (t) (1i8: isleType))
;;@ (|| (= (t) (8i8: isleType))
;;@ (|| (= (t) (16i8: isleType))
;;@ (|| (= (t) (32i8: isleType))
;;@ (= (t) (64i8: isleType))))))
;;@ ))
(decl alu_rrr (ALUOp Type Reg Reg) Reg)
(extern constructor alu_rrr alu_rrr)

(rule (do_shift op $I32 x y) (alu_rrr op $I32 x (value_regs_get y 0)))
88 changes: 88 additions & 0 deletions cranelift/isle/veri/veri_engine/examples/broken/shifts/broken_ishl_to_do_shift_64.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
;;@ (spec (sig (args arg) (ret))
;;@ (assertions (= (arg) (ret))))
(decl lower (Inst) InstOutput)

;; Instruction formats.
(type MInst
(enum
))

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (0i64:bv) (ret))))
;;decl ALUOp.Lsl

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (1i64:bv) (ret))))
;;decl ALUOp.Lsr

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (2i64:bv) (ret))))
;;decl ALUOp.Asr

;; An ALU operation. This can be paired with several instruction formats
;; below (see `Inst`) in any combination.
(type ALUOp
(enum
(Add)
(Sub)
(Orr)
(OrrNot)
(And)
(AndS)
(AndNot)
;; XOR (AArch64 calls this "EOR")
(Eor)
;; XNOR (AArch64 calls this "EOR-NOT")
(EorNot)
;; Add, setting flags
(AddS)
;; Sub, setting flags
(SubS)
;; Signed multiply, high-word result
(SMulH)
;; Unsigned multiply, high-word result
(UMulH)
(SDiv)
(UDiv)
(RotR)
(Lsr)
(Asr)
(Lsl)
;; Add with carry
(Adc)
;; Add with carry, settings flags
(AdcS)
;; Subtract with carry
(Sbc)
;; Subtract with carry, settings flags
(SbcS)
))

;;@ (spec (sig (args op, t, a, b) (ret))
;;@ (assertions (if (= (op) (0i64:bv)) {
;;@ (= (ret) (shl (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (1i64:bv)) {
;;@ (= (ret) (shr (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (2i64:bv)) {
;;@ (= (ret) (ashr (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (= (ret) (64i64:bv))
;;@ })
;;@ })
;;@ }),
;;@ (|| (= (op) (0i64:bv)) (|| (= (op) (1i64:bv)) (= (op) (2i64:bv)))),
;;@ (|| (= (t) (1i8: isleType))
;;@ (|| (= (t) (8i8: isleType))
;;@ (|| (= (t) (16i8: isleType))
;;@ (|| (= (t) (32i8: isleType))
;;@ (= (t) (64i8: isleType))))))
;;@ ))
(decl do_shift (ALUOp Type Reg Value) Reg)
(extern constructor do_shift do_shift)

;; BROKEN: Asr instead of Lsl
;; Shift for i64.
(rule (lower (has_type $I64 (ishl x y)))
(do_shift (ALUOp.Asr) $I64 x y))
98 changes: 98 additions & 0 deletions ...lift/isle/veri/veri_engine/examples/broken/shifts/broken_sshr_to_do_shift_fits_in_32.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,98 @@
;;@ (spec (sig (args arg) (ret))
;;@ (assertions (= (arg) (ret))))
(decl lower (Inst) InstOutput)

;; Instruction formats.
(type MInst
(enum
))

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (0i64:bv) (ret))))
;;decl ALUOp.Lsl

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (1i64:bv) (ret))))
;;decl ALUOp.Lsr

;;@ (spec (sig (args) (ret))
;;@ (assertions (= (2i64:bv) (ret))))
;;decl ALUOp.Asr

;; An ALU operation. This can be paired with several instruction formats
;; below (see `Inst`) in any combination.
(type ALUOp
(enum
(Add)
(Sub)
(Orr)
(OrrNot)
(And)
(AndS)
(AndNot)
;; XOR (AArch64 calls this "EOR")
(Eor)
;; XNOR (AArch64 calls this "EOR-NOT")
(EorNot)
;; Add, setting flags
(AddS)
;; Sub, setting flags
(SubS)
;; Signed multiply, high-word result
(SMulH)
;; Unsigned multiply, high-word result
(UMulH)
(SDiv)
(UDiv)
(RotR)
(Lsr)
(Asr)
(Lsl)
;; Add with carry
(Adc)
;; Add with carry, settings flags
(AdcS)
;; Subtract with carry
(Sbc)
;; Subtract with carry, settings flags
(SbcS)
))

;;@ (spec (sig (args op, t, a, b) (ret))
;;@ (assertions (if (= (op) (0i64:bv)) {
;;@ (= (ret) (shl (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (1i64:bv)) {
;;@ (= (ret) (shr (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (if (= (op) (2i64:bv)) {
;;@ (= (ret) (ashr (conv_to (t) (a)) (b)))
;;@ } else {
;;@ (= (ret) (64i64:bv))
;;@ })
;;@ })
;;@ }),
;;@ (|| (= (op) (0i64:bv)) (|| (= (op) (1i64:bv)) (= (op) (2i64:bv)))),
;;@ (|| (= (t) (1i8: isleType))
;;@ (|| (= (t) (8i8: isleType))
;;@ (|| (= (t) (16i8: isleType))
;;@ (|| (= (t) (32i8: isleType))
;;@ (= (t) (64i8: isleType))))))
;;@ ))
(decl do_shift (ALUOp Type Reg Value) Reg)
(extern constructor do_shift do_shift)

;;@ (spec (sig (args x) (ret))
;;@ (assertions (= (sign_ext (32) (x)) (ret))))
(decl put_in_reg_sext32 (Value) Reg)
(extern constructor put_in_reg_sext32 put_in_reg_sext32)

;;@ (spec (sig (args x) (ret))
;;@ (assertions (= (zero_ext (32) (x)) (ret))))
(decl put_in_reg_zext32 (Value) Reg)
(extern constructor put_in_reg_zext32 put_in_reg_zext32)

;; BROKEN: zext32 instead of sext32
;; Shift for i64.
(rule -2 (lower (has_type (fits_in_32 ty) (sshr x y)))
(do_shift (ALUOp.Asr) ty (put_in_reg_zext32 x) y))
Loading