Skip to content

Actual assume vs assert distinction, named rules, move to aarch64 files #62

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

Merged
avanhatt merged 30 commits into from
Apr 12, 2023
Merged

Actual assume vs assert distinction, named rules, move to aarch64 files #62

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
a8fcbe4
add distinction for rhs assertions
avanhatt Apr 10, 2023
fae0d84
tests on named rules
avanhatt Apr 10, 2023
07bb0fc
more iadd
avanhatt Apr 11, 2023
2de1f49
kill moved files
avanhatt Apr 11, 2023
d35d5d4
more test movement
avanhatt Apr 11, 2023
7611976
broken_do_shift
avanhatt Apr 11, 2023
2e5ec5c
isub
avanhatt Apr 11, 2023
03cbbd6
ineg, div
avanhatt Apr 11, 2023
211dc84
rem
avanhatt Apr 11, 2023
4f9ff29
more b-logic
avanhatt Apr 11, 2023
42262c1
bnot
avanhatt Apr 11, 2023
e5dfc3f
move switch some match check to assertion, not assumption
avanhatt Apr 11, 2023
e83802f
start moving shifts
avanhatt Apr 11, 2023
3a41314
ishl
avanhatt Apr 11, 2023
ab4513b
ushr, sshr
avanhatt Apr 11, 2023
81844d0
do_shift
avanhatt Apr 11, 2023
fa43176
rotl
avanhatt Apr 11, 2023
65c3ff5
rotr
avanhatt Apr 11, 2023
f888708
rotr
avanhatt Apr 11, 2023
509c692
naming
avanhatt Apr 12, 2023
42a9a13
first 2 icmp
avanhatt Apr 12, 2023
d76e86f
more icmp
avanhatt Apr 12, 2023
1ce2ba2
more icmp
avanhatt Apr 12, 2023
23c902e
test_named_lower_icmp_8_16_signed
avanhatt Apr 12, 2023
26c3079
icmp
avanhatt Apr 12, 2023
f198f24
renaming
avanhatt Apr 12, 2023
775b577
rest of icmp
avanhatt Apr 12, 2023
29b8d62
fix test
avanhatt Apr 12, 2023
a663f52
fmt
avanhatt Apr 12, 2023
4f14be8
files
avanhatt Apr 12, 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
79 changes: 47 additions & 32 deletions cranelift/codegen/src/clif_lower.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,18 @@
)
)

;;@ (spec (sig (args) (r)) (assume (= (r) (2i8:bv8))))
;;decl IntCC.SignedGreaterThan

;;@ (spec (sig (args) (r)) (assume (= (r) (3i8:bv8))))
;;decl IntCC.SignedGreaterThanOrEqual

;;@ (spec (sig (args) (r)) (assume (= (r) (6i8:bv8))))
;;decl IntCC.UnsignedGreaterThan

;;@ (spec (sig (args) (r)) (assume (= (r) (7i8:bv8))))
;;decl IntCC.UnsignedGreaterThanOrEqual

;;;; Enumerated Immediate: TrapCode ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(type TrapCode extern
Expand Down Expand Up @@ -695,7 +707,7 @@
)

;;@ (spec (sig (args arg) (ret))
;;@ (assertions (= (arg) (zero_ext (64) (ret)))))
;;@ (assume (= (arg) (zero_ext (64) (ret)))))
(decl iconst (Imm64) Inst)
(extractor
(iconst N)
Expand Down Expand Up @@ -795,7 +807,7 @@
;; )
;; )
;;@ (spec (sig (args c, x, y) (ret))
;;@ (assertions
;;@ (assume
;;@ (= (ret)
;;@ (switch (c)
;;@ ((0i8:bv8) (if (= (x) (y)) (1i8:bv8) (0i8:bv8)))
Expand All @@ -808,8 +820,9 @@
;;@ ((7i8:bv8) (if (ugte (x) (y)) (1i8:bv8) (0i8:bv8)))
;;@ ((8i8:bv8) (if (ult (x) (y)) (1i8:bv8) (0i8:bv8)))
;;@ ((9i8:bv8) (if (ulte (x) (y)) (1i8:bv8) (0i8:bv8)))
;;@ )
;;@ )))
;;@ )),
;;@ (ulte (c) (9i8:bv8))
;;@ ))
(decl icmp (IntCC Value Value) Inst)
(extractor
(icmp Cond x y)
Expand All @@ -823,23 +836,23 @@
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (+ (x) (y)) (ret))))
;;@ (assume (= (+ (x) (y)) (ret))))
(decl iadd (Value Value) Inst)
(extractor
(iadd x y)
(inst_data (InstructionData.Binary (Opcode.Iadd) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (- (x) (y)) (ret))))
;;@ (assume (= (- (x) (y)) (ret))))
(decl isub (Value Value) Inst)
(extractor
(isub x y)
(inst_data (InstructionData.Binary (Opcode.Isub) (value_array_2 x y)))
)

;;@ (spec (sig (args x) (ret))
;;@ (assertions (= (-(x)) (ret))))
;;@ (assume (= (-(x)) (ret))))
(decl ineg (Value) Inst)
(extractor
(ineg x)
Expand All @@ -853,23 +866,23 @@
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (* (x) (y)) (ret))))
;;@ (assume (= (* (x) (y)) (ret))))
(decl imul (Value Value) Inst)
(extractor
(imul x y)
(inst_data (InstructionData.Binary (Opcode.Imul) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (extract 127 64 (* (zero_ext (128) (x)) (zero_ext (128) (y)))) (ret))))
;;@ (assume (= (extract 127 64 (* (zero_ext (128) (x)) (zero_ext (128) (y)))) (ret))))
(decl umulhi (Value Value) Inst)
(extractor
(umulhi x y)
(inst_data (InstructionData.Binary (Opcode.Umulhi) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (extract 127 64 (* (sign_ext (128) (x)) (sign_ext (128) (y)))) (ret))))
;;@ (assume (= (extract 127 64 (* (sign_ext (128) (x)) (sign_ext (128) (y)))) (ret))))
(decl smulhi (Value Value) Inst)
(extractor
(smulhi x y)
Expand All @@ -883,23 +896,23 @@
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (/ (x) (y)) (ret))))
;;@ (assume (= (/ (x) (y)) (ret))))
(decl udiv (Value Value) Inst)
(extractor
(udiv x y)
(inst_data (InstructionData.Binary (Opcode.Udiv) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (sdiv (x) (y)) (ret))))
;;@ (assume (= (sdiv (x) (y)) (ret))))
(decl sdiv (Value Value) Inst)
(extractor
(sdiv x y)
(inst_data (InstructionData.Binary (Opcode.Sdiv) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (urem (x) (y)) (ret)),
;;@ (assume (= (urem (x) (y)) (ret)),
;;@ (! (= (bv2int (ret)) (0i0:isleType)))
;;@ ))
(decl urem (Value Value) Inst)
Expand All @@ -909,7 +922,7 @@
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (srem (x) (y)) (ret)),
;;@ (assume (= (srem (x) (y)) (ret)),
;;@ (! (= (bv2int (ret)) (0i0:isleType)))
;;@ ))
(decl srem (Value Value) Inst)
Expand All @@ -918,16 +931,14 @@
(inst_data (InstructionData.Binary (Opcode.Srem) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (+ (sign_ext (64) (x)) (y)) (ret))))
(decl iadd_imm (Value Imm64) Inst)
(extractor
(iadd_imm x Y)
(inst_data (InstructionData.BinaryImm64 (Opcode.IaddImm) x Y))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (* (sign_ext (64) (x)) (y)) (ret))))
;;@ (assume (= (* (sign_ext (64) (x)) (y)) (ret))))
(decl imul_imm (Value Imm64) Inst)
(extractor
(imul_imm x Y)
Expand Down Expand Up @@ -965,7 +976,7 @@
)

;;@ (spec (sig (args x, y, cin) (ret))
;;@ (assertions (= (+ (+ (x) (y)) (cin)) (ret))))
;;@ (assume (= (+ (+ (x) (y)) (cin)) (ret))))
(decl iadd_cin (Value Value Value) Inst)
(extractor
(iadd_cin x y c_in)
Expand All @@ -991,7 +1002,7 @@
)

;;@ (spec (sig (args x, y, bin) (ret))
;;@ (assertions (= (- (x) (+ (y) (bin))) (ret))))
;;@ (assume (= (- (x) (+ (y) (bin))) (ret))))
(decl isub_bin (Value Value Value) Inst)
(extractor
(isub_bin x y b_in)
Expand All @@ -1011,35 +1022,39 @@
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (& (x) (y)) (ret))))
;;@ (assume (= (& (x) (y)) (ret))))
(decl band (Value Value) Inst)
(extractor
(band x y)
(inst_data (InstructionData.Binary (Opcode.Band) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (| (x) (y)) (ret))))
;;@ (assume (= (| (x) (y)) (ret))))
(decl bor (Value Value) Inst)
(extractor
(bor x y)
(inst_data (InstructionData.Binary (Opcode.Bor) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (xor (x) (y)) (ret))))
;;@ (assume (= (xor (x) (y)) (ret))))
(decl bxor (Value Value) Inst)
(extractor
(bxor x y)
(inst_data (InstructionData.Binary (Opcode.Bxor) (value_array_2 x y)))
)

;;@ (spec (sig (args x) (ret))
;;@ (assume (= (~ (x)) (ret))))
(decl bnot (Value) Inst)
(extractor
(bnot x)
(inst_data (InstructionData.Unary (Opcode.Bnot) x))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assume (= (& (x) (~ (y))) (ret))))
(decl band_not (Value Value) Inst)
(extractor
(band_not x y)
Expand Down Expand Up @@ -1077,15 +1092,15 @@
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (rotl (x) (y)) (ret))))
;;@ (assume (= (rotl (x) (y)) (ret))))
(decl rotl (Value Value) Inst)
(extractor
(rotl x y)
(inst_data (InstructionData.Binary (Opcode.Rotl) (value_array_2 x y)))
)

;;@ (spec (sig (args x, y) (ret))
;;@ (assertions (= (rotr (x) (y)) (ret))))
;;@ (assume (= (rotr (x) (y)) (ret))))
(decl rotr (Value Value) Inst)
(extractor
(rotr x y)
Expand All @@ -1112,23 +1127,23 @@
;; }

;;@ (spec (sig (args a, b) (ret))
;;@ (assertions (= (ret) (shl (a) (& (conv_to (widthof (b)) (- (int2bv 64 (widthof (b))) (1i64:bv))) (b))))))
;;@ (assume (= (ret) (shl (a) (& (conv_to (widthof (b)) (- (int2bv 64 (widthof (b))) (1i64:bv))) (b))))))
(decl ishl (Value Value) Inst)
(extractor
(ishl x y)
(inst_data (InstructionData.Binary (Opcode.Ishl) (value_array_2 x y)))
)

;;@ (spec (sig (args a, b) (ret))
;;@ (assertions (= (ret) (shr (a) (& (conv_to (widthof (b)) (- (int2bv 64 (widthof (b))) (1i64:bv))) (b))))))
;;@ (assume (= (ret) (shr (a) (& (conv_to (widthof (b)) (- (int2bv 64 (widthof (b))) (1i64:bv))) (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 (= (ret) (ashr (a) (& (conv_to (widthof (b)) (- (int2bv 64 (widthof (b))) (1i64:bv))) (b))))))
;;@ (assume (= (ret) (ashr (a) (& (conv_to (widthof (b)) (- (int2bv 64 (widthof (b))) (1i64:bv))) (b))))))
(decl sshr (Value Value) Inst)
(extractor
(sshr x y)
Expand Down Expand Up @@ -1160,23 +1175,23 @@
)

;;@ (spec (sig (args a) (ret))
;;@ (assertions (= (ret) (clz (a)))))
;;@ (assume (= (ret) (clz (a)))))
(decl clz (Value) Inst)
(extractor
(clz x)
(inst_data (InstructionData.Unary (Opcode.Clz) x))
)

;;@ (spec (sig (args a) (ret))
;;@ (assertions (= (ret) (cls (a)))))
;;@ (assume (= (ret) (cls (a)))))
(decl cls (Value) Inst)
(extractor
(cls x)
(inst_data (InstructionData.Unary (Opcode.Cls) x))
)

;;@ (spec (sig (args a) (ret))
;;@ (assertions (= (ret) (clz (rev (a))))))
;;@ (assume (= (ret) (clz (rev (a))))))
(decl ctz (Value) Inst)
(extractor
(ctz x)
Expand Down Expand Up @@ -1394,15 +1409,15 @@
)

;;@ (spec (sig (args arg) (ret))
;;@ (assertions (= (ret) (zero_ext (widthof (ret)) (arg)))))
;;@ (assume (= (ret) (zero_ext (widthof (ret)) (arg)))))
(decl uextend (Value) Inst)
(extractor
(uextend x)
(inst_data (InstructionData.Unary (Opcode.Uextend) x))
)

;;@ (spec (sig (args arg) (ret))
;;@ (assertions (= (ret) (sign_ext (widthof (ret)) (arg)))))
;;@ (assume (= (ret) (sign_ext (widthof (ret)) (arg)))))
(decl sextend (Value) Inst)
(extractor
(sextend x)
Expand Down
Loading