diff options
Diffstat (limited to 'test/Expr/Parser/Exprs.kquery')
| -rw-r--r-- | test/Expr/Parser/Exprs.kquery | 346 |
1 files changed, 346 insertions, 0 deletions
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] + |