From f27cf86466d75c71a302abe5e0a3ffcad1670373 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 14 Sep 2015 14:32:37 -0400 Subject: Renamed .pc to .kquery (kleaver query) --- test/Expr/Parser/Concat64.kquery | 12 ++ test/Expr/Parser/Concat64.pc | 12 -- test/Expr/Parser/ConstantFolding.kquery | 197 ++++++++++++++++++ test/Expr/Parser/ConstantFolding.pc | 197 ------------------ test/Expr/Parser/Exprs.kquery | 346 ++++++++++++++++++++++++++++++++ test/Expr/Parser/Exprs.pc | 346 -------------------------------- test/Expr/Parser/MultiByteReads.kquery | 20 ++ test/Expr/Parser/MultiByteReads.pc | 20 -- test/Expr/Parser/Simplify.kquery | 40 ++++ test/Expr/Parser/Simplify.pc | 40 ---- test/Expr/Parser/TypeChecking.kquery | 16 ++ test/Expr/Parser/TypeChecking.pc | 16 -- 12 files changed, 631 insertions(+), 631 deletions(-) create mode 100644 test/Expr/Parser/Concat64.kquery delete mode 100644 test/Expr/Parser/Concat64.pc create mode 100644 test/Expr/Parser/ConstantFolding.kquery delete mode 100644 test/Expr/Parser/ConstantFolding.pc create mode 100644 test/Expr/Parser/Exprs.kquery delete mode 100644 test/Expr/Parser/Exprs.pc create mode 100644 test/Expr/Parser/MultiByteReads.kquery delete mode 100644 test/Expr/Parser/MultiByteReads.pc create mode 100644 test/Expr/Parser/Simplify.kquery delete mode 100644 test/Expr/Parser/Simplify.pc create mode 100644 test/Expr/Parser/TypeChecking.kquery delete mode 100644 test/Expr/Parser/TypeChecking.pc (limited to 'test/Expr/Parser') diff --git a/test/Expr/Parser/Concat64.kquery b/test/Expr/Parser/Concat64.kquery new file mode 100644 index 00000000..0b1479d4 --- /dev/null +++ b/test/Expr/Parser/Concat64.kquery @@ -0,0 +1,12 @@ +# RUN: kleaver --print-ast %s + +array arr1[8] : w32 -> w8 = symbolic +(query [(Eq 0 + (Concat w64 (Read w8 7 arr1) + (Concat w56 (Read w8 6 arr1) + (Concat w48 (Read w8 5 arr1) + (Concat w40 (Read w8 4 arr1) + (Concat w32 (Read w8 3 arr1) + (Concat w24 (Read w8 2 arr1) + (Concat w16 (Read w8 1 arr1) (Read w8 0 arr1)))))))))] + false) diff --git a/test/Expr/Parser/Concat64.pc b/test/Expr/Parser/Concat64.pc deleted file mode 100644 index 0b1479d4..00000000 --- a/test/Expr/Parser/Concat64.pc +++ /dev/null @@ -1,12 +0,0 @@ -# RUN: kleaver --print-ast %s - -array arr1[8] : w32 -> w8 = symbolic -(query [(Eq 0 - (Concat w64 (Read w8 7 arr1) - (Concat w56 (Read w8 6 arr1) - (Concat w48 (Read w8 5 arr1) - (Concat w40 (Read w8 4 arr1) - (Concat w32 (Read w8 3 arr1) - (Concat w24 (Read w8 2 arr1) - (Concat w16 (Read w8 1 arr1) (Read w8 0 arr1)))))))))] - false) diff --git a/test/Expr/Parser/ConstantFolding.kquery b/test/Expr/Parser/ConstantFolding.kquery new file mode 100644 index 00000000..a02920db --- /dev/null +++ b/test/Expr/Parser/ConstantFolding.kquery @@ -0,0 +1,197 @@ +# RUN: %kleaver --builder=constant-folding -print-ast %s > %t + +array a[64] : w32 -> w8 = symbolic + +# RUN: grep -A 2 "# Query 1$" %t > %t2 +# RUN: grep "(query .. false)" %t2 +(query [] (Not (Ult (w32 0) (w32 1)))) + +# Check -- 0 + X ==> X +# RUN: grep -A 2 "# Query 2$" %t > %t2 +# RUN: grep "(query .. false .(Read w8 0 a).)" %t2 +(query [] false [(Add w8 0 (Read w8 0 a))]) +# RUN: grep -A 2 "# Query 3$" %t > %t2 +# RUN: grep "(query .. false .(Read w8 0 a).)" %t2 +(query [] false [(Add w8 (Read w8 0 a) 0)]) + +# Check -- C_0 + (C_1 + X) ==> (C_0 + C_1) + X +# RUN: grep -A 2 "# Query 4$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 30 (Read w8 0 a)).)" %t2 +(query [] false [(Add w8 10 (Add w8 20 (Read w8 0 a)))]) + +# Check -- C_0 + (X + C_1) ==> (C_0 + C_1) + X +# RUN: grep -A 2 "# Query 5$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 30 (Read w8 0 a)).)" %t2 +(query [] false [(Add w8 10 (Add w8 (Read w8 0 a) 20))]) + +# Check -- C_0 + (C_1 - X) ==> (C_0 + C_1) - X +# RUN: grep -A 2 "# Query 6$" %t > %t2 +# RUN: grep "(query .. false .(Sub w8 30 (Read w8 0 a)).)" %t2 +(query [] false [(Add w8 10 (Sub w8 20 (Read w8 0 a)))]) + +# Check -- C_0 + (X - C_1) ==> (C_0 - C_1) + X +# RUN: grep -A 2 "# Query 7$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a)).)" %t2 +(query [] false [(Add w8 10 (Sub w8 (Read w8 0 a) 20))]) + +# Check -- (X + Y) + Z ==> X + (Y + Z) +# RUN: grep -A 3 "# Query 8$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2 +# RUN: grep "(Add w8 (Read w8 1 a) (Read w8 2 a)" %t2 +(query [] false [(Add w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) + +# Check -- (X - Y) + Z ==> X + (Z - Y) +# RUN: grep -A 3 "# Query 9$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2 +# RUN: grep "(Sub w8 (Read w8 2 a) (Read w8 1 a)" %t2 +(query [] false [(Add w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) + +# Check -- X + (C + Y) ==> C + (X + Y) +# RUN: grep -A 3 "# Query 10$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 10" %t2 +# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))]) + +# Check -- X + (Y + C) ==> C + (X + Y) +# RUN: grep -A 3 "# Query 11$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 10" %t2 +# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))]) + +# Check -- X + (C - Y) ==> C + (X - Y) +# RUN: grep -A 3 "# Query 12$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 10" %t2 +# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))]) + +# Check -- X + (Y - C) ==> -C + (X + Y) +# RUN: grep -A 3 "# Query 13$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 246" %t2 +# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Add w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))]) + +# Check -- C_0 - (C_1 + X) ==> (C_0 - C1) - X +# RUN: grep -A 2 "# Query 14$" %t > %t2 +# RUN: grep "(query .. false .(Sub w8 10 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 20 (Add w8 10 (Read w8 0 a)))]) + +# Check -- C_0 - (X + C_1) ==> (C_0 + C1) + X +# RUN: grep -A 2 "# Query 15$" %t > %t2 +# RUN: grep "(query .. false .(Sub w8 10 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 20 (Add w8 (Read w8 0 a) 10))]) + +# Check -- C_0 - (C_1 - X) ==> (C_0 - C1) + X +# RUN: grep -A 2 "# Query 16$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 10 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 20 (Sub w8 10 (Read w8 0 a)))]) + +# Check -- C_0 - (X - C_1) ==> (C_0 + C1) - X +# RUN: grep -A 2 "# Query 17$" %t > %t2 +# RUN: grep "(query .. false .(Sub w8 30 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 20 (Sub w8 (Read w8 0 a) 10))]) + +# Check -- (C_0 + X) - C_1 ==> (C_0 - C1) + X +# RUN: grep -A 2 "# Query 18$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 (Add w8 10 (Read w8 0 a)) 20)]) + +# Check -- (X + C_0) - C_1 ==> (C_0 - C1) + X +# RUN: grep -A 2 "# Query 19$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 (Add w8 (Read w8 0 a) 10) 20)]) + +# Check -- (C_0 - X) - C_1 ==> (C_0 - C1) - X +# RUN: grep -A 2 "# Query 20$" %t > %t2 +# RUN: grep "(query .. false .(Sub w8 246 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 (Sub w8 10 (Read w8 0 a)) 20)]) + +# Check -- (X - C_0) - C_1 ==> -(C_0 + C1) + X +# RUN: grep -A 2 "# Query 21$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 226 (Read w8 0 a))" %t2 +(query [] false [(Sub w8 (Sub w8 (Read w8 0 a) 10) 20)]) + +# Check -- (X + Y) - Z ==> X + (Y - Z) +# RUN: grep -A 3 "# Query 22$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2 +# RUN: grep "(Sub w8 (Read w8 1 a) (Read w8 2 a)" %t2 +(query [] false [(Sub w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) + +# Check -- (X - Y) - Z ==> X - (Y + Z) +# RUN: grep -A 3 "# Query 23$" %t > %t2 +# RUN: grep "(query .. false .(Sub w8 (Read w8 0 a)" %t2 +# RUN: grep "(Add w8 (Read w8 1 a) (Read w8 2 a)" %t2 +(query [] false [(Sub w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) + +# Check -- X - (C + Y) ==> -C + (X - Y) +# RUN: grep -A 3 "# Query 24$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 246" %t2 +# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Sub w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))]) + +# Check -- X - (Y + C) ==> -C + (X - Y) +# RUN: grep -A 3 "# Query 25$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 246" %t2 +# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Sub w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))]) + +# Check -- X - (C - Y) ==> -C + (X + Y) +# RUN: grep -A 3 "# Query 26$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 246" %t2 +# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Sub w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))]) + +# Check -- X - (Y - C) ==> C + (X - Y) +# RUN: grep -A 3 "# Query 27$" %t > %t2 +# RUN: grep "(query .. false .(Add w8 10" %t2 +# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 +(query [] false [(Sub w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))]) + +# Check -- X * 0 ==> 0 +# RUN: grep -A 2 "# Query 28$" %t > %t2 +# RUN: grep "(query .. false .(w8 0)." %t2 +(query [] false [(Mul w8 0 (Read w8 0 a))]) + +# Check -- X * 1 ==> X +# RUN: grep -A 2 "# Query 29$" %t > %t2 +# RUN: grep "(query .. false .(Read w8 0 a)." %t2 +(query [] false [(Mul w8 1 (Read w8 0 a))]) + +# Check -- X & 0 ==> 0 +# RUN: grep -A 2 "# Query 30$" %t > %t2 +# RUN: grep "(query .. false .(w8 0)." %t2 +(query [] false [(And w8 0 (Read w8 0 a))]) + +# Check -- X & 0b1...1 ==> X +# RUN: grep -A 2 "# Query 31$" %t > %t2 +# RUN: grep "(query .. false .(Read w8 0 a)." %t2 +(query [] false [(And w8 255 (Read w8 0 a))]) + +# Check -- X | 0 ==> X +# RUN: grep -A 2 "# Query 32$" %t > %t2 +# RUN: grep "(query .. false .(Read w8 0 a)." %t2 +(query [] false [(Or w8 0 (Read w8 0 a))]) + +# Check -- X | 0b1...1 ==> X +# RUN: grep -A 2 "# Query 33$" %t > %t2 +# RUN: grep "(query .. false .(w8 255)." %t2 +(query [] false [(Or w8 255 (Read w8 0 a))]) + +# Check -- X ^ 0b1...1 ==> X +# RUN: grep -A 2 "# Query 34$" %t > %t2 +# RUN: grep "(query .. false .(Read w8 0 a)." %t2 +(query [] false [(Xor w8 0 (Read w8 0 a))]) + +# Check -- true == X ==> X +# RUN: grep -A 2 "# Query 35$" %t > %t2 +# RUN: grep "(query .. false .(Eq 0 (Read w8 0 a))." %t2 +(query [] false [(Eq true (Eq 0 (Read w8 0 a)))]) + +# Check -- !!X ==> X +# RUN: grep -A 2 "# Query 36$" %t > %t2 +# RUN: grep "(query .. false .(Eq 0 (Read w8 0 a))." %t2 +(query [] false [(Not (Not (Eq 0 (Read w8 0 a))))]) + +# Check -- !Const +# RUN: grep -A 2 "# Query 37$" %t > %t2 +# RUN: grep "(query .. false .true." %t2 +(query [] false [(Eq (Not w32 0xdeadbeef) 0x21524110)]) diff --git a/test/Expr/Parser/ConstantFolding.pc b/test/Expr/Parser/ConstantFolding.pc deleted file mode 100644 index a02920db..00000000 --- a/test/Expr/Parser/ConstantFolding.pc +++ /dev/null @@ -1,197 +0,0 @@ -# RUN: %kleaver --builder=constant-folding -print-ast %s > %t - -array a[64] : w32 -> w8 = symbolic - -# RUN: grep -A 2 "# Query 1$" %t > %t2 -# RUN: grep "(query .. false)" %t2 -(query [] (Not (Ult (w32 0) (w32 1)))) - -# Check -- 0 + X ==> X -# RUN: grep -A 2 "# Query 2$" %t > %t2 -# RUN: grep "(query .. false .(Read w8 0 a).)" %t2 -(query [] false [(Add w8 0 (Read w8 0 a))]) -# RUN: grep -A 2 "# Query 3$" %t > %t2 -# RUN: grep "(query .. false .(Read w8 0 a).)" %t2 -(query [] false [(Add w8 (Read w8 0 a) 0)]) - -# Check -- C_0 + (C_1 + X) ==> (C_0 + C_1) + X -# RUN: grep -A 2 "# Query 4$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 30 (Read w8 0 a)).)" %t2 -(query [] false [(Add w8 10 (Add w8 20 (Read w8 0 a)))]) - -# Check -- C_0 + (X + C_1) ==> (C_0 + C_1) + X -# RUN: grep -A 2 "# Query 5$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 30 (Read w8 0 a)).)" %t2 -(query [] false [(Add w8 10 (Add w8 (Read w8 0 a) 20))]) - -# Check -- C_0 + (C_1 - X) ==> (C_0 + C_1) - X -# RUN: grep -A 2 "# Query 6$" %t > %t2 -# RUN: grep "(query .. false .(Sub w8 30 (Read w8 0 a)).)" %t2 -(query [] false [(Add w8 10 (Sub w8 20 (Read w8 0 a)))]) - -# Check -- C_0 + (X - C_1) ==> (C_0 - C_1) + X -# RUN: grep -A 2 "# Query 7$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a)).)" %t2 -(query [] false [(Add w8 10 (Sub w8 (Read w8 0 a) 20))]) - -# Check -- (X + Y) + Z ==> X + (Y + Z) -# RUN: grep -A 3 "# Query 8$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2 -# RUN: grep "(Add w8 (Read w8 1 a) (Read w8 2 a)" %t2 -(query [] false [(Add w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) - -# Check -- (X - Y) + Z ==> X + (Z - Y) -# RUN: grep -A 3 "# Query 9$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2 -# RUN: grep "(Sub w8 (Read w8 2 a) (Read w8 1 a)" %t2 -(query [] false [(Add w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) - -# Check -- X + (C + Y) ==> C + (X + Y) -# RUN: grep -A 3 "# Query 10$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 10" %t2 -# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Add w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))]) - -# Check -- X + (Y + C) ==> C + (X + Y) -# RUN: grep -A 3 "# Query 11$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 10" %t2 -# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Add w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))]) - -# Check -- X + (C - Y) ==> C + (X - Y) -# RUN: grep -A 3 "# Query 12$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 10" %t2 -# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Add w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))]) - -# Check -- X + (Y - C) ==> -C + (X + Y) -# RUN: grep -A 3 "# Query 13$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 246" %t2 -# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Add w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))]) - -# Check -- C_0 - (C_1 + X) ==> (C_0 - C1) - X -# RUN: grep -A 2 "# Query 14$" %t > %t2 -# RUN: grep "(query .. false .(Sub w8 10 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 20 (Add w8 10 (Read w8 0 a)))]) - -# Check -- C_0 - (X + C_1) ==> (C_0 + C1) + X -# RUN: grep -A 2 "# Query 15$" %t > %t2 -# RUN: grep "(query .. false .(Sub w8 10 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 20 (Add w8 (Read w8 0 a) 10))]) - -# Check -- C_0 - (C_1 - X) ==> (C_0 - C1) + X -# RUN: grep -A 2 "# Query 16$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 10 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 20 (Sub w8 10 (Read w8 0 a)))]) - -# Check -- C_0 - (X - C_1) ==> (C_0 + C1) - X -# RUN: grep -A 2 "# Query 17$" %t > %t2 -# RUN: grep "(query .. false .(Sub w8 30 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 20 (Sub w8 (Read w8 0 a) 10))]) - -# Check -- (C_0 + X) - C_1 ==> (C_0 - C1) + X -# RUN: grep -A 2 "# Query 18$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 (Add w8 10 (Read w8 0 a)) 20)]) - -# Check -- (X + C_0) - C_1 ==> (C_0 - C1) + X -# RUN: grep -A 2 "# Query 19$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 246 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 (Add w8 (Read w8 0 a) 10) 20)]) - -# Check -- (C_0 - X) - C_1 ==> (C_0 - C1) - X -# RUN: grep -A 2 "# Query 20$" %t > %t2 -# RUN: grep "(query .. false .(Sub w8 246 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 (Sub w8 10 (Read w8 0 a)) 20)]) - -# Check -- (X - C_0) - C_1 ==> -(C_0 + C1) + X -# RUN: grep -A 2 "# Query 21$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 226 (Read w8 0 a))" %t2 -(query [] false [(Sub w8 (Sub w8 (Read w8 0 a) 10) 20)]) - -# Check -- (X + Y) - Z ==> X + (Y - Z) -# RUN: grep -A 3 "# Query 22$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 (Read w8 0 a)" %t2 -# RUN: grep "(Sub w8 (Read w8 1 a) (Read w8 2 a)" %t2 -(query [] false [(Sub w8 (Add w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) - -# Check -- (X - Y) - Z ==> X - (Y + Z) -# RUN: grep -A 3 "# Query 23$" %t > %t2 -# RUN: grep "(query .. false .(Sub w8 (Read w8 0 a)" %t2 -# RUN: grep "(Add w8 (Read w8 1 a) (Read w8 2 a)" %t2 -(query [] false [(Sub w8 (Sub w8 (Read w8 0 a) (Read w8 1 a)) (Read w8 2 a))]) - -# Check -- X - (C + Y) ==> -C + (X - Y) -# RUN: grep -A 3 "# Query 24$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 246" %t2 -# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Sub w8 (Read w8 0 a) (Add w8 10 (Read w8 1 a)))]) - -# Check -- X - (Y + C) ==> -C + (X - Y) -# RUN: grep -A 3 "# Query 25$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 246" %t2 -# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Sub w8 (Read w8 0 a) (Add w8 (Read w8 1 a) 10))]) - -# Check -- X - (C - Y) ==> -C + (X + Y) -# RUN: grep -A 3 "# Query 26$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 246" %t2 -# RUN: grep "(Add w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Sub w8 (Read w8 0 a) (Sub w8 10 (Read w8 1 a)))]) - -# Check -- X - (Y - C) ==> C + (X - Y) -# RUN: grep -A 3 "# Query 27$" %t > %t2 -# RUN: grep "(query .. false .(Add w8 10" %t2 -# RUN: grep "(Sub w8 (Read w8 0 a) (Read w8 1 a)" %t2 -(query [] false [(Sub w8 (Read w8 0 a) (Sub w8 (Read w8 1 a) 10))]) - -# Check -- X * 0 ==> 0 -# RUN: grep -A 2 "# Query 28$" %t > %t2 -# RUN: grep "(query .. false .(w8 0)." %t2 -(query [] false [(Mul w8 0 (Read w8 0 a))]) - -# Check -- X * 1 ==> X -# RUN: grep -A 2 "# Query 29$" %t > %t2 -# RUN: grep "(query .. false .(Read w8 0 a)." %t2 -(query [] false [(Mul w8 1 (Read w8 0 a))]) - -# Check -- X & 0 ==> 0 -# RUN: grep -A 2 "# Query 30$" %t > %t2 -# RUN: grep "(query .. false .(w8 0)." %t2 -(query [] false [(And w8 0 (Read w8 0 a))]) - -# Check -- X & 0b1...1 ==> X -# RUN: grep -A 2 "# Query 31$" %t > %t2 -# RUN: grep "(query .. false .(Read w8 0 a)." %t2 -(query [] false [(And w8 255 (Read w8 0 a))]) - -# Check -- X | 0 ==> X -# RUN: grep -A 2 "# Query 32$" %t > %t2 -# RUN: grep "(query .. false .(Read w8 0 a)." %t2 -(query [] false [(Or w8 0 (Read w8 0 a))]) - -# Check -- X | 0b1...1 ==> X -# RUN: grep -A 2 "# Query 33$" %t > %t2 -# RUN: grep "(query .. false .(w8 255)." %t2 -(query [] false [(Or w8 255 (Read w8 0 a))]) - -# Check -- X ^ 0b1...1 ==> X -# RUN: grep -A 2 "# Query 34$" %t > %t2 -# RUN: grep "(query .. false .(Read w8 0 a)." %t2 -(query [] false [(Xor w8 0 (Read w8 0 a))]) - -# Check -- true == X ==> X -# RUN: grep -A 2 "# Query 35$" %t > %t2 -# RUN: grep "(query .. false .(Eq 0 (Read w8 0 a))." %t2 -(query [] false [(Eq true (Eq 0 (Read w8 0 a)))]) - -# Check -- !!X ==> X -# RUN: grep -A 2 "# Query 36$" %t > %t2 -# RUN: grep "(query .. false .(Eq 0 (Read w8 0 a))." %t2 -(query [] false [(Not (Not (Eq 0 (Read w8 0 a))))]) - -# Check -- !Const -# RUN: grep -A 2 "# Query 37$" %t > %t2 -# RUN: grep "(query .. false .true." %t2 -(query [] false [(Eq (Not w32 0xdeadbeef) 0x21524110)]) diff --git a/test/Expr/Parser/Exprs.kquery b/test/Expr/Parser/Exprs.kquery new file mode 100644 index 00000000..4a6adf7e --- /dev/null +++ b/test/Expr/Parser/Exprs.kquery @@ -0,0 +1,346 @@ +# Taken from Features/ExprLogging.c + +# FIXME: Make this test actual check for something (other than +# crashing/errors). + +# RUN: %kleaver -print-ast %s + +# Query 0 -- Type: Truth, Instructions: 31 +array arr53[4] : w32 -> w8 = symbolic +(query [] (Not (Ult (ReadLSB w32 0 arr53) + 16))) +# OK -- Elapsed: 0.00137401 +# Is Valid: false + +# Query 1 -- Type: Value, Instructions: 39 +array arr53[4] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 arr53) + 16)] + false + [(Add w32 31543488 (Mul w32 4 N0))]) +# OK -- Elapsed: 0.000108004 +# Result: 31543488 + +# Query 2 -- Type: Truth, Instructions: 39 +array arr53[4] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 arr53) + 16)] + (Ult (Mul w32 4 N0) 61)) +# OK -- Elapsed: 0.00140095 +# Is Valid: true + +# Query 3 -- Type: Truth, Instructions: 55 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16)] + (Not (Ult (ReadLSB w32 0 arr60) + 16))) +# OK -- Elapsed: 0.00106597 +# Is Valid: false + +# Query 4 -- Type: Value, Instructions: 60 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult N0:(ReadLSB w32 0 arr60) + 16)] + false + [(Add w32 31543488 (Mul w32 4 N0))]) +# OK -- Elapsed: 0.000138998 +# Result: 31543488 + +# Query 5 -- Type: Truth, Instructions: 60 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult N0:(ReadLSB w32 0 arr60) + 16)] + (Ult (Mul w32 4 N0) 61)) +# OK -- Elapsed: 0.00137782 +# Is Valid: true + +# Query 6 -- Type: Truth, Instructions: 77 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16)] + (Not (Ult (ReadLSB w32 0 arr67) + 16))) +# OK -- Elapsed: 0.001127 +# Is Valid: false + +# Query 7 -- Type: Value, Instructions: 85 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult N0:(ReadLSB w32 0 arr67) + 16)] + false + [(Add w32 31543488 (Mul w32 4 N0))]) +# OK -- Elapsed: 0.000175953 +# Result: 31543488 + +# Query 8 -- Type: Truth, Instructions: 85 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult N0:(ReadLSB w32 0 arr67) + 16)] + (Ult (Mul w32 4 N0) 61)) +# OK -- Elapsed: 0.00141382 +# Is Valid: true + +# Query 9 -- Type: Truth, Instructions: 101 +array arr53[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult (ReadLSB w32 0 arr67) + 16)] + (And (Not (Eq 3 + N0:(ReadLSB w32 0 arr74))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0)))))) +# OK -- Elapsed: 0.00157499 +# Is Valid: false + +# Query 10 -- Type: Value, Instructions: 106 +array arr53[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult (ReadLSB w32 0 arr67) + 16) + (Not (And (Not (Eq 3 + N0:(ReadLSB w32 0 arr74))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0))))))] + false + [(Add w32 31583232 N0)]) +# OK -- Elapsed: 0.000259876 +# Result: 31583235 + +# Query 11 -- Type: Truth, Instructions: 106 +array arr53[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult (ReadLSB w32 0 arr67) + 16) + (Not (And (Not N0:(Eq 3 + N1:(ReadLSB w32 0 arr74))) + (And (Not N2:(Eq 2 N1)) + (And (Not N3:(Eq 1 N1)) + (Not N4:(Eq 0 N1))))))] + (Or N0 + (Or N2 (Or N3 N4)))) +# OK -- Elapsed: 0.00194788 +# Is Valid: true + +# Query 12 -- Type: Truth, Instructions: 112 +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult (ReadLSB w32 0 arr67) + 16) + (Not (And (Not (Eq 3 + N0:(ReadLSB w32 0 arr74))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0))))))] + (Not (Eq 104 + (Read w8 0 [N0=0, + 1=97] @ arr49)))) +# OK -- Elapsed: 0.0030148 +# Is Valid: false + +# Query 13 -- Type: Truth, Instructions: 122 +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult (ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult (ReadLSB w32 0 arr67) + 16) + (Not (And (Not (Eq 3 + N0:(ReadLSB w32 0 arr74))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0)))))) + (Eq 104 + (Read w8 0 U0:[N0=0, + 1=97] @ arr49))] + (Not (Slt 2 + (Concat w32 (Read w8 3 U0) + (Concat w24 (Read w8 2 U0) + (Concat w16 (Read w8 1 U0) (w8 104))))))) +# OK -- Elapsed: 0.000394106 +# Is Valid: false + +# Query 14 -- Type: Truth, Instructions: 128 +array arr5[64] : w32 -> w8 = symbolic +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 arr53) + 16) + (Ult (ReadLSB w32 0 arr60) + 16) + (Ult N1:(ReadLSB w32 0 arr67) + 16) + (Not (And (Not (Eq 3 + N2:(ReadLSB w32 0 arr74))) + (And (Not (Eq 2 N2)) + (And (Not (Eq 1 N2)) + (Not (Eq 0 N2)))))) + (Eq 104 + (Read w8 0 U0:[N2=0, + 1=97] @ arr49)) + (Slt 2 + N3:(Concat w32 (Read w8 3 U0) + (Concat w24 (Read w8 2 U0) + (Concat w16 (Read w8 1 U0) (w8 104)))))] + (Not (Eq (ReadLSB w32 48 U1:[N4:(Mul w32 4 N1)=(Extract w8 0 N5:(SExt w32 (Read w8 3 arr49))), + (Add w32 1 N4)=(Extract w8 8 N5), + (Add w32 2 N4)=(Extract w8 16 N5), + (Add w32 3 N4)=(Extract w8 24 N5), + N6:(Mul w32 4 N0)=(Extract w8 0 N7:(SExt w32 (Read w8 0 arr49))), + (Add w32 1 N6)=(Extract w8 8 N7), + (Add w32 2 N6)=(Extract w8 16 N7), + (Add w32 3 N6)=(Extract w8 24 N7), + 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1] @ arr5) + N3))) +# OK -- Elapsed: 0.0180621 +# Is Valid: false + +# Query 15 -- Type: Truth, Instructions: 133 +array arr5[64] : w32 -> w8 = symbolic +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 arr53) + 16) + (Ult N1:(ReadLSB w32 0 arr60) + 16) + (Ult N2:(ReadLSB w32 0 arr67) + 16) + (Not (And (Not (Eq 3 + N3:(ReadLSB w32 0 arr74))) + (And (Not (Eq 2 N3)) + (And (Not (Eq 1 N3)) + (Not (Eq 0 N3)))))) + (Eq 104 + (Read w8 0 U0:[N3=0, + 1=97] @ arr49)) + (Slt 2 + N4:(Concat w32 (Read w8 3 U0) + (Concat w24 (Read w8 2 U0) + (Concat w16 (Read w8 1 U0) (w8 104))))) + (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr49))), + (Add w32 1 N5)=(Extract w8 8 N6), + (Add w32 2 N5)=(Extract w8 16 N6), + (Add w32 3 N5)=(Extract w8 24 N6)] @ + U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr49))), + (Add w32 1 N7)=(Extract w8 8 N8), + (Add w32 2 N7)=(Extract w8 16 N8), + (Add w32 3 N7)=(Extract w8 24 N8), + 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1] @ arr5) + N4)] + (Eq 32 + (ReadLSB w32 N9:(Mul w32 4 N1) U2))) +# OK -- Elapsed: 0.00104594 +# Is Valid: false + +# Query 16 -- Type: InitialValues, Instructions: 135 +array arr5[64] : w32 -> w8 = symbolic +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic +(query [(Ult N0:(ReadLSB w32 0 arr53) + 16) + (Ult N1:(ReadLSB w32 0 arr60) + 16) + (Ult N2:(ReadLSB w32 0 arr67) + 16) + (Not (And (Not (Eq 3 + N3:(ReadLSB w32 0 arr74))) + (And (Not (Eq 2 N3)) + (And (Not (Eq 1 N3)) + (Not (Eq 0 N3)))))) + (Eq 104 + (Read w8 0 U0:[N3=0, + 1=97] @ arr49)) + (Slt 2 + N4:(Concat w32 (Read w8 3 U0) + (Concat w24 (Read w8 2 U0) + (Concat w16 (Read w8 1 U0) (w8 104))))) + (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr49))), + (Add w32 1 N5)=(Extract w8 8 N6), + (Add w32 2 N5)=(Extract w8 16 N6), + (Add w32 3 N5)=(Extract w8 24 N6)] @ + U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr49))), + (Add w32 1 N7)=(Extract w8 8 N8), + (Add w32 2 N7)=(Extract w8 16 N8), + (Add w32 3 N7)=(Extract w8 24 N8), + 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1] @ arr5) + N4) + (Not (Eq 32 + (ReadLSB w32 N9:(Mul w32 4 N1) U2)))] + false [] + [arr49 + arr53 + arr60 + arr67 + arr74]) +# OK -- Elapsed: 0.000574112 +# Solvable: true +# arr49 = [104,0,0,0] +# arr53 = [12,0,0,0] +# arr60 = [0,0,0,0] +# arr67 = [0,0,0,0] +# arr74 = [1,0,0,0] + diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.pc deleted file mode 100644 index 4a6adf7e..00000000 --- a/test/Expr/Parser/Exprs.pc +++ /dev/null @@ -1,346 +0,0 @@ -# Taken from Features/ExprLogging.c - -# FIXME: Make this test actual check for something (other than -# crashing/errors). - -# RUN: %kleaver -print-ast %s - -# Query 0 -- Type: Truth, Instructions: 31 -array arr53[4] : w32 -> w8 = symbolic -(query [] (Not (Ult (ReadLSB w32 0 arr53) - 16))) -# OK -- Elapsed: 0.00137401 -# Is Valid: false - -# Query 1 -- Type: Value, Instructions: 39 -array arr53[4] : w32 -> w8 = symbolic -(query [(Ult N0:(ReadLSB w32 0 arr53) - 16)] - false - [(Add w32 31543488 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000108004 -# Result: 31543488 - -# Query 2 -- Type: Truth, Instructions: 39 -array arr53[4] : w32 -> w8 = symbolic -(query [(Ult N0:(ReadLSB w32 0 arr53) - 16)] - (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.00140095 -# Is Valid: true - -# Query 3 -- Type: Truth, Instructions: 55 -array arr53[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16)] - (Not (Ult (ReadLSB w32 0 arr60) - 16))) -# OK -- Elapsed: 0.00106597 -# Is Valid: false - -# Query 4 -- Type: Value, Instructions: 60 -array arr53[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult N0:(ReadLSB w32 0 arr60) - 16)] - false - [(Add w32 31543488 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000138998 -# Result: 31543488 - -# Query 5 -- Type: Truth, Instructions: 60 -array arr53[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult N0:(ReadLSB w32 0 arr60) - 16)] - (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.00137782 -# Is Valid: true - -# Query 6 -- Type: Truth, Instructions: 77 -array arr53[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16)] - (Not (Ult (ReadLSB w32 0 arr67) - 16))) -# OK -- Elapsed: 0.001127 -# Is Valid: false - -# Query 7 -- Type: Value, Instructions: 85 -array arr53[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult N0:(ReadLSB w32 0 arr67) - 16)] - false - [(Add w32 31543488 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000175953 -# Result: 31543488 - -# Query 8 -- Type: Truth, Instructions: 85 -array arr53[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult N0:(ReadLSB w32 0 arr67) - 16)] - (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.00141382 -# Is Valid: true - -# Query 9 -- Type: Truth, Instructions: 101 -array arr53[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult (ReadLSB w32 0 arr67) - 16)] - (And (Not (Eq 3 - N0:(ReadLSB w32 0 arr74))) - (And (Not (Eq 2 N0)) - (And (Not (Eq 1 N0)) - (Not (Eq 0 N0)))))) -# OK -- Elapsed: 0.00157499 -# Is Valid: false - -# Query 10 -- Type: Value, Instructions: 106 -array arr53[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult (ReadLSB w32 0 arr67) - 16) - (Not (And (Not (Eq 3 - N0:(ReadLSB w32 0 arr74))) - (And (Not (Eq 2 N0)) - (And (Not (Eq 1 N0)) - (Not (Eq 0 N0))))))] - false - [(Add w32 31583232 N0)]) -# OK -- Elapsed: 0.000259876 -# Result: 31583235 - -# Query 11 -- Type: Truth, Instructions: 106 -array arr53[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult (ReadLSB w32 0 arr67) - 16) - (Not (And (Not N0:(Eq 3 - N1:(ReadLSB w32 0 arr74))) - (And (Not N2:(Eq 2 N1)) - (And (Not N3:(Eq 1 N1)) - (Not N4:(Eq 0 N1))))))] - (Or N0 - (Or N2 (Or N3 N4)))) -# OK -- Elapsed: 0.00194788 -# Is Valid: true - -# Query 12 -- Type: Truth, Instructions: 112 -array arr53[4] : w32 -> w8 = symbolic -array arr49[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult (ReadLSB w32 0 arr67) - 16) - (Not (And (Not (Eq 3 - N0:(ReadLSB w32 0 arr74))) - (And (Not (Eq 2 N0)) - (And (Not (Eq 1 N0)) - (Not (Eq 0 N0))))))] - (Not (Eq 104 - (Read w8 0 [N0=0, - 1=97] @ arr49)))) -# OK -- Elapsed: 0.0030148 -# Is Valid: false - -# Query 13 -- Type: Truth, Instructions: 122 -array arr53[4] : w32 -> w8 = symbolic -array arr49[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult (ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult (ReadLSB w32 0 arr67) - 16) - (Not (And (Not (Eq 3 - N0:(ReadLSB w32 0 arr74))) - (And (Not (Eq 2 N0)) - (And (Not (Eq 1 N0)) - (Not (Eq 0 N0)))))) - (Eq 104 - (Read w8 0 U0:[N0=0, - 1=97] @ arr49))] - (Not (Slt 2 - (Concat w32 (Read w8 3 U0) - (Concat w24 (Read w8 2 U0) - (Concat w16 (Read w8 1 U0) (w8 104))))))) -# OK -- Elapsed: 0.000394106 -# Is Valid: false - -# Query 14 -- Type: Truth, Instructions: 128 -array arr5[64] : w32 -> w8 = symbolic -array arr53[4] : w32 -> w8 = symbolic -array arr49[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult N0:(ReadLSB w32 0 arr53) - 16) - (Ult (ReadLSB w32 0 arr60) - 16) - (Ult N1:(ReadLSB w32 0 arr67) - 16) - (Not (And (Not (Eq 3 - N2:(ReadLSB w32 0 arr74))) - (And (Not (Eq 2 N2)) - (And (Not (Eq 1 N2)) - (Not (Eq 0 N2)))))) - (Eq 104 - (Read w8 0 U0:[N2=0, - 1=97] @ arr49)) - (Slt 2 - N3:(Concat w32 (Read w8 3 U0) - (Concat w24 (Read w8 2 U0) - (Concat w16 (Read w8 1 U0) (w8 104)))))] - (Not (Eq (ReadLSB w32 48 U1:[N4:(Mul w32 4 N1)=(Extract w8 0 N5:(SExt w32 (Read w8 3 arr49))), - (Add w32 1 N4)=(Extract w8 8 N5), - (Add w32 2 N4)=(Extract w8 16 N5), - (Add w32 3 N4)=(Extract w8 24 N5), - N6:(Mul w32 4 N0)=(Extract w8 0 N7:(SExt w32 (Read w8 0 arr49))), - (Add w32 1 N6)=(Extract w8 8 N7), - (Add w32 2 N6)=(Extract w8 16 N7), - (Add w32 3 N6)=(Extract w8 24 N7), - 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1] @ arr5) - N3))) -# OK -- Elapsed: 0.0180621 -# Is Valid: false - -# Query 15 -- Type: Truth, Instructions: 133 -array arr5[64] : w32 -> w8 = symbolic -array arr53[4] : w32 -> w8 = symbolic -array arr49[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult N0:(ReadLSB w32 0 arr53) - 16) - (Ult N1:(ReadLSB w32 0 arr60) - 16) - (Ult N2:(ReadLSB w32 0 arr67) - 16) - (Not (And (Not (Eq 3 - N3:(ReadLSB w32 0 arr74))) - (And (Not (Eq 2 N3)) - (And (Not (Eq 1 N3)) - (Not (Eq 0 N3)))))) - (Eq 104 - (Read w8 0 U0:[N3=0, - 1=97] @ arr49)) - (Slt 2 - N4:(Concat w32 (Read w8 3 U0) - (Concat w24 (Read w8 2 U0) - (Concat w16 (Read w8 1 U0) (w8 104))))) - (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr49))), - (Add w32 1 N5)=(Extract w8 8 N6), - (Add w32 2 N5)=(Extract w8 16 N6), - (Add w32 3 N5)=(Extract w8 24 N6)] @ - U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr49))), - (Add w32 1 N7)=(Extract w8 8 N8), - (Add w32 2 N7)=(Extract w8 16 N8), - (Add w32 3 N7)=(Extract w8 24 N8), - 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1] @ arr5) - N4)] - (Eq 32 - (ReadLSB w32 N9:(Mul w32 4 N1) U2))) -# OK -- Elapsed: 0.00104594 -# Is Valid: false - -# Query 16 -- Type: InitialValues, Instructions: 135 -array arr5[64] : w32 -> w8 = symbolic -array arr53[4] : w32 -> w8 = symbolic -array arr49[4] : w32 -> w8 = symbolic -array arr74[4] : w32 -> w8 = symbolic -array arr60[4] : w32 -> w8 = symbolic -array arr67[4] : w32 -> w8 = symbolic -(query [(Ult N0:(ReadLSB w32 0 arr53) - 16) - (Ult N1:(ReadLSB w32 0 arr60) - 16) - (Ult N2:(ReadLSB w32 0 arr67) - 16) - (Not (And (Not (Eq 3 - N3:(ReadLSB w32 0 arr74))) - (And (Not (Eq 2 N3)) - (And (Not (Eq 1 N3)) - (Not (Eq 0 N3)))))) - (Eq 104 - (Read w8 0 U0:[N3=0, - 1=97] @ arr49)) - (Slt 2 - N4:(Concat w32 (Read w8 3 U0) - (Concat w24 (Read w8 2 U0) - (Concat w16 (Read w8 1 U0) (w8 104))))) - (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr49))), - (Add w32 1 N5)=(Extract w8 8 N6), - (Add w32 2 N5)=(Extract w8 16 N6), - (Add w32 3 N5)=(Extract w8 24 N6)] @ - U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr49))), - (Add w32 1 N7)=(Extract w8 8 N8), - (Add w32 2 N7)=(Extract w8 16 N8), - (Add w32 3 N7)=(Extract w8 24 N8), - 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1] @ arr5) - N4) - (Not (Eq 32 - (ReadLSB w32 N9:(Mul w32 4 N1) U2)))] - false [] - [arr49 - arr53 - arr60 - arr67 - arr74]) -# OK -- Elapsed: 0.000574112 -# Solvable: true -# arr49 = [104,0,0,0] -# arr53 = [12,0,0,0] -# arr60 = [0,0,0,0] -# arr67 = [0,0,0,0] -# arr74 = [1,0,0,0] - diff --git a/test/Expr/Parser/MultiByteReads.kquery b/test/Expr/Parser/MultiByteReads.kquery new file mode 100644 index 00000000..71f0288f --- /dev/null +++ b/test/Expr/Parser/MultiByteReads.kquery @@ -0,0 +1,20 @@ +# RUN: %kleaver -print-ast -pc-multibyte-reads=true %s > %t.log +# RUN: grep -q "(ReadLSB w32 4 arr1)" %t.log +# RUN: grep -q "(ReadMSB w32 2 arr2)" %t.log + +array arr1[8] : w32 -> w8 = symbolic +array arr2[8] : w32 -> w8 = symbolic + +(query [(Not (Slt 100 + (Concat w32 (Read w8 7 arr1) + (Concat w24 (Read w8 6 arr1) + (Concat w16 (Read w8 5 arr1) (Read w8 4 arr1))))))] + false) + + +(query [(Not (Slt 100 + (Concat w32 (Read w8 2 arr2) + (Concat w24 (Read w8 3 arr2) + (Concat w16 (Read w8 4 arr2) (Read w8 5 arr2))))))] + false) + diff --git a/test/Expr/Parser/MultiByteReads.pc b/test/Expr/Parser/MultiByteReads.pc deleted file mode 100644 index 71f0288f..00000000 --- a/test/Expr/Parser/MultiByteReads.pc +++ /dev/null @@ -1,20 +0,0 @@ -# RUN: %kleaver -print-ast -pc-multibyte-reads=true %s > %t.log -# RUN: grep -q "(ReadLSB w32 4 arr1)" %t.log -# RUN: grep -q "(ReadMSB w32 2 arr2)" %t.log - -array arr1[8] : w32 -> w8 = symbolic -array arr2[8] : w32 -> w8 = symbolic - -(query [(Not (Slt 100 - (Concat w32 (Read w8 7 arr1) - (Concat w24 (Read w8 6 arr1) - (Concat w16 (Read w8 5 arr1) (Read w8 4 arr1))))))] - false) - - -(query [(Not (Slt 100 - (Concat w32 (Read w8 2 arr2) - (Concat w24 (Read w8 3 arr2) - (Concat w16 (Read w8 4 arr2) (Read w8 5 arr2))))))] - false) - diff --git a/test/Expr/Parser/Simplify.kquery b/test/Expr/Parser/Simplify.kquery new file mode 100644 index 00000000..6d817b6f --- /dev/null +++ b/test/Expr/Parser/Simplify.kquery @@ -0,0 +1,40 @@ +# RUN: %kleaver --builder=simplify -print-ast %s > %t + +array a[64] : w32 -> w8 = symbolic + +# Check -- X u> Y ==> Y u< X +# RUN: grep -A 2 "# Query 1" %t > %t2 +# RUN: grep "(query .. false .(Ult (Read w8 1 a) (Read w8 0 a)).)" %t2 +(query [] false [(Ugt (Read w8 0 a) (Read w8 1 a))]) + +# Check -- X u>= Y ==> Y u<= X +# RUN: grep -A 2 "# Query 2" %t > %t2 +# RUN: grep "(query .. false .(Ule (Read w8 1 a) (Read w8 0 a)).)" %t2 +(query [] false [(Uge (Read w8 0 a) (Read w8 1 a))]) + +# Check -- X u> Y ==> Y u< X +# RUN: grep -A 2 "# Query 3" %t > %t2 +# RUN: grep "(query .. false .(Slt (Read w8 1 a) (Read w8 0 a)).)" %t2 +(query [] false [(Sgt (Read w8 0 a) (Read w8 1 a))]) + +# Check -- X u>= Y ==> Y u<= X +# RUN: grep -A 2 "# Query 4" %t > %t2 +# RUN: grep "(query .. false .(Sle (Read w8 1 a) (Read w8 0 a)).)" %t2 +(query [] false [(Sge (Read w8 0 a) (Read w8 1 a))]) + +# Check -- X != Y ==> !(X == Y) +# RUN: grep -A 2 "# Query 5" %t > %t2 +# RUN: grep "(query .. false .(Not (Eq (Read w8 0 a) (Read w8 1 a))).)" %t2 +(query [] false [(Ne (Read w8 0 a) (Read w8 1 a))]) + +# Check -- !(X or Y) ==> !X and !Y +# RUN: grep -A 3 "# Query 6$" %t > %t2 +# RUN: grep "(query .. false .(And (Not (Eq 0 (Read w8 0 a)))" %t2 +# RUN: grep "(Not (Eq 1 (Read w8 1 a))))" %t2 +(query [] false [(Not (Or (Eq 0 (Read w8 0 a)) + (Eq 1 (Read w8 1 a))))]) + +# Check -- false == X ==> !X +# RUN: grep -A 2 "# Query 7" %t > %t2 +# RUN: grep "(query .. false .(Not (Extract 1 (Read w8 0 a))).)" %t2 +(query [] false [(Eq (Extract w1 1 (Read w8 0 a)) false)]) diff --git a/test/Expr/Parser/Simplify.pc b/test/Expr/Parser/Simplify.pc deleted file mode 100644 index 6d817b6f..00000000 --- a/test/Expr/Parser/Simplify.pc +++ /dev/null @@ -1,40 +0,0 @@ -# RUN: %kleaver --builder=simplify -print-ast %s > %t - -array a[64] : w32 -> w8 = symbolic - -# Check -- X u> Y ==> Y u< X -# RUN: grep -A 2 "# Query 1" %t > %t2 -# RUN: grep "(query .. false .(Ult (Read w8 1 a) (Read w8 0 a)).)" %t2 -(query [] false [(Ugt (Read w8 0 a) (Read w8 1 a))]) - -# Check -- X u>= Y ==> Y u<= X -# RUN: grep -A 2 "# Query 2" %t > %t2 -# RUN: grep "(query .. false .(Ule (Read w8 1 a) (Read w8 0 a)).)" %t2 -(query [] false [(Uge (Read w8 0 a) (Read w8 1 a))]) - -# Check -- X u> Y ==> Y u< X -# RUN: grep -A 2 "# Query 3" %t > %t2 -# RUN: grep "(query .. false .(Slt (Read w8 1 a) (Read w8 0 a)).)" %t2 -(query [] false [(Sgt (Read w8 0 a) (Read w8 1 a))]) - -# Check -- X u>= Y ==> Y u<= X -# RUN: grep -A 2 "# Query 4" %t > %t2 -# RUN: grep "(query .. false .(Sle (Read w8 1 a) (Read w8 0 a)).)" %t2 -(query [] false [(Sge (Read w8 0 a) (Read w8 1 a))]) - -# Check -- X != Y ==> !(X == Y) -# RUN: grep -A 2 "# Query 5" %t > %t2 -# RUN: grep "(query .. false .(Not (Eq (Read w8 0 a) (Read w8 1 a))).)" %t2 -(query [] false [(Ne (Read w8 0 a) (Read w8 1 a))]) - -# Check -- !(X or Y) ==> !X and !Y -# RUN: grep -A 3 "# Query 6$" %t > %t2 -# RUN: grep "(query .. false .(And (Not (Eq 0 (Read w8 0 a)))" %t2 -# RUN: grep "(Not (Eq 1 (Read w8 1 a))))" %t2 -(query [] false [(Not (Or (Eq 0 (Read w8 0 a)) - (Eq 1 (Read w8 1 a))))]) - -# Check -- false == X ==> !X -# RUN: grep -A 2 "# Query 7" %t > %t2 -# RUN: grep "(query .. false .(Not (Extract 1 (Read w8 0 a))).)" %t2 -(query [] false [(Eq (Extract w1 1 (Read w8 0 a)) false)]) diff --git a/test/Expr/Parser/TypeChecking.kquery b/test/Expr/Parser/TypeChecking.kquery new file mode 100644 index 00000000..d9685b70 --- /dev/null +++ b/test/Expr/Parser/TypeChecking.kquery @@ -0,0 +1,16 @@ +# RUN: not %kleaver %s 2> %t.log + + + +# RUN: grep "TypeChecking.kquery:7:9: error: type widths do not match in binary expression" %t.log +array arr1[8] : w32 -> w8 = symbolic +(query [(Eq (ReadLSB w32 0 arr1) true)] + false) + +# RUN: grep "TypeChecking.kquery:14:25: error: invalid write index (doesn't match array domain)" %t.log +# RUN: grep "TypeChecking.kquery:14:35: error: invalid write value (doesn't match array range)" %t.log +# FIXME: Add array declarations +array arr2[8] : w32 -> w8 = symbolic +(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false) + +# RUN: grep "TypeChecking.kquery: parse failure: 3 errors." %t.log diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc deleted file mode 100644 index 66991c20..00000000 --- a/test/Expr/Parser/TypeChecking.pc +++ /dev/null @@ -1,16 +0,0 @@ -# RUN: not %kleaver %s 2> %t.log - - - -# RUN: grep "TypeChecking.pc:7:9: error: type widths do not match in binary expression" %t.log -array arr1[8] : w32 -> w8 = symbolic -(query [(Eq (ReadLSB w32 0 arr1) true)] - false) - -# RUN: grep "TypeChecking.pc:14:25: error: invalid write index (doesn't match array domain)" %t.log -# RUN: grep "TypeChecking.pc:14:35: error: invalid write value (doesn't match array range)" %t.log -# FIXME: Add array declarations -array arr2[8] : w32 -> w8 = symbolic -(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false) - -# RUN: grep "TypeChecking.pc: parse failure: 3 errors." %t.log -- cgit 1.4.1