From cd95368ea4f74b09e30725ba04cc84ede6b24fcf Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 21 May 2009 04:48:03 +0000 Subject: Missed a couple tests git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72206 91177308-0d34-0410-b5e6-96231b3b80d8 --- test/Expr/Lexer/Numbers.pc | 74 +++++++++ test/Expr/Lexer/dg.exp | 3 + test/Expr/Parser/Exprs.pc | 390 +++++++++++++++++++++++++++++++++++++++++++++ test/Expr/Parser/dg.exp | 3 + 4 files changed, 470 insertions(+) create mode 100644 test/Expr/Lexer/Numbers.pc create mode 100644 test/Expr/Lexer/dg.exp create mode 100644 test/Expr/Parser/Exprs.pc create mode 100644 test/Expr/Parser/dg.exp (limited to 'test/Expr') diff --git a/test/Expr/Lexer/Numbers.pc b/test/Expr/Lexer/Numbers.pc new file mode 100644 index 00000000..6af40133 --- /dev/null +++ b/test/Expr/Lexer/Numbers.pc @@ -0,0 +1,74 @@ +# RUN: %kleaver -print-tokens %s | grep -v Comment > %t1 +# RUN: grep "(Token .Number. .0b0101_0110. 11 40 0)" %t1 +# RUN: grep "(Token .Number. .0o0703. 6 41 0)" %t1 +# RUN: grep "(Token .Number. .0xABC0_0024. 11 42 0)" %t1 +# RUN: grep "(Token .Number. .-0x10. 5 43 0)" %t1 +# RUN: grep "(Token .Number. .+10. 3 44 0)" %t1 +# RUN: grep "(Token .Comma. .,. 1 47 0)" %t1 +# RUN: grep "(Token .Arrow. .->. 2 48 0)" %t1 +# RUN: grep "(Token .Colon. .:. 1 49 0)" %t1 +# RUN: grep "(Token .Semicolon. .;. 1 50 0)" %t1 +# RUN: grep "(Token .Equals. .=. 1 51 0)" %t1 +# RUN: grep "(Token .At. .@. 1 52 0)" %t1 +# RUN: grep "(Token .LParen. .(. 1 54 0)" %t1 +# RUN: grep "(Token .RParen. .). 1 54 2)" %t1 +# RUN: grep "(Token .LSquare. .\[. 1 55 0)" %t1 +# RUN: grep "(Token .RSquare. .\]. 1 55 2)" %t1 +# RUN: grep "(Token .LBrace. .{. 1 56 0)" %t1 +# RUN: grep "(Token .RBrace. .}. 1 56 2)" %t1 +# RUN: grep "(Token .Identifier. ._hello_world. 12 58 0)" %t1 +# RUN: grep "(Token .KWReserved. .array. 5 62 0)" %t1 +# RUN: grep "(Token .KWReserved. .declare. 7 63 0)" %t1 +# RUN: grep "(Token .KWReserved. .def. 3 64 0)" %t1 +# RUN: grep "(Token .KWReserved. .define. 6 65 0)" %t1 +# RUN: grep "(Token .KWFalse. .false. 5 66 0)" %t1 +# RUN: grep "(Token .KWQuery. .query. 5 67 0)" %t1 +# RUN: grep "(Token .KWTrue. .true. 4 68 0)" %t1 +# RUN: grep "(Token .KWReserved. .var. 3 69 0)" %t1 +# RUN: grep "(Token .KWReserved. .i32. 3 73 0)" %t1 +# RUN: grep "(Token .KWReserved. .fp10.3. 6 74 0)" %t1 +# RUN: grep "(Token .EndOfFile. .. 0 75 0)" %t1 + +# This is just some random filler space which can be erased in order +# to add more run lines without having to adjust the token locations. + + + + +# This comment should be on line 38. + +0b0101_0110 +0o0703 +0xABC0_0024 +-0x10 ++10 + +# Various punctuation +, +-> +: +; += +@ + +( ) +[ ] +{ } + +_hello_world + +# Keywords + +array +declare +def +define +false +query +true +var + +# Reserved keywords + +i32 +fp10.3 diff --git a/test/Expr/Lexer/dg.exp b/test/Expr/Lexer/dg.exp new file mode 100644 index 00000000..94fc4df8 --- /dev/null +++ b/test/Expr/Lexer/dg.exp @@ -0,0 +1,3 @@ +load_lib llvm.exp + +RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]] diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.pc new file mode 100644 index 00000000..3d37bf9b --- /dev/null +++ b/test/Expr/Parser/Exprs.pc @@ -0,0 +1,390 @@ +# FIXME: Make this test actual check for something (other than +# crashing/errors). + +# RUN: %kleaver -print-ast %s + +# Query 0 -- Type: Truth, Instructions: 33 +(query [] (Not (Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16))) +# OK -- Elapsed: 0.000977993 +# Is Valid: false + +# Query 1 -- Type: Value, Instructions: 41 +(query [(Ult N0:(Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16)] + (Add w32 174331008 (Mul w32 4 N0))) +# OK -- Elapsed: 3.38554e-05 +# Result: 174331008 + +# Query 2 -- Type: Truth, Instructions: 41 +(query [(Ult N0:(Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16)] + (Ult (Mul w32 4 N0) 61)) +# OK -- Elapsed: 0.00113606 +# Is Valid: true + +# Query 3 -- Type: Truth, Instructions: 57 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16)] + (Not (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16))) +# OK -- Elapsed: 0.000864983 +# Is Valid: false + +# Query 4 -- Type: Value, Instructions: 62 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult N0:(Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16)] + (Add w32 174331008 (Mul w32 4 N0))) +# OK -- Elapsed: 3.60012e-05 +# Result: 174331008 + +# Query 5 -- Type: Truth, Instructions: 62 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult N0:(Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16)] + (Ult (Mul w32 4 N0) 61)) +# OK -- Elapsed: 0.00109196 +# Is Valid: true + +# Query 6 -- Type: Truth, Instructions: 79 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16)] + (Not (Ult (Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16))) +# OK -- Elapsed: 0.00089097 +# Is Valid: false + +# Query 7 -- Type: Value, Instructions: 87 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult N0:(Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16)] + (Add w32 174331008 (Mul w32 4 N0))) +# OK -- Elapsed: 4.41074e-05 +# Result: 174331008 + +# Query 8 -- Type: Truth, Instructions: 87 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult N0:(Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16)] + (Ult (Mul w32 4 N0) 61)) +# OK -- Elapsed: 0.00111794 +# Is Valid: true + +# Query 9 -- Type: Truth, Instructions: 103 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult (Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16)] + (And (Not (Eq 3 + N0:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0)))))) +# OK -- Elapsed: 0.00117898 +# Is Valid: false + +# Query 10 -- Type: Value, Instructions: 108 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult (Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16) + (Not (And (Not (Eq 3 + N0:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0))))))] + (Add w32 174291904 N0)) +# OK -- Elapsed: 5.91278e-05 +# Result: 174291907 + +# Query 11 -- Type: Truth, Instructions: 108 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult (Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16) + (Not (And (Not N0:(Eq 3 + N1:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (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.00145888 +# Is Valid: true + +# Query 12 -- Type: Truth, Instructions: 114 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult (Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16) + (Not (And (Not (Eq 3 + N0:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0))))))] + (Not (Eq 104 + (Read w8 0 [N0=0, + 1=97] @ arr60)))) +# OK -- Elapsed: 0.00247502 +# Is Valid: false + +# Query 13 -- Type: Truth, Instructions: 124 +(query [(Ult (Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult (Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16) + (Not (And (Not (Eq 3 + N0:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (And (Not (Eq 2 N0)) + (And (Not (Eq 1 N0)) + (Not (Eq 0 N0)))))) + (Eq 104 + (Read w8 0 U0:[N0=0, + 1=97] @ arr60))] + (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.000127077 +# Is Valid: false + +# Query 14 -- Type: Truth, Instructions: 130 +(query [(Ult N0:(Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult (Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult N1:(Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16) + (Not (And (Not (Eq 3 + N2:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (And (Not (Eq 2 N2)) + (And (Not (Eq 1 N2)) + (Not (Eq 0 N2)))))) + (Eq 104 + (Read w8 0 U0:[N2=0, + 1=97] @ arr60)) + (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 (Concat w32 (Read w8 51 U1:[N4:(Mul w32 4 N1)=(Extract w8 0 N5:(SExt w32 (Read w8 3 arr60))), + (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 arr60))), + (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]) + (Concat w24 (Read w8 50 U1) + (ReadLSB w16 48 U1))) + N3))) +# OK -- Elapsed: 0.0158381 +# Is Valid: false + +# Query 15 -- Type: Truth, Instructions: 135 +(query [(Ult N0:(Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult N1:(Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult N2:(Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16) + (Not (And (Not (Eq 3 + N3:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (And (Not (Eq 2 N3)) + (And (Not (Eq 1 N3)) + (Not (Eq 0 N3)))))) + (Eq 104 + (Read w8 0 U0:[N3=0, + 1=97] @ arr60)) + (Slt 2 + N4:(Concat w32 (Read w8 3 U0) + (Concat w24 (Read w8 2 U0) + (Concat w16 (Read w8 1 U0) (w8 104))))) + (Eq (Concat w32 (Read w8 51 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr60))), + (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 arr60))), + (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]) + (Concat w24 (Read w8 50 U1) + (ReadLSB w16 48 U1))) + N4)] + (Eq 32 + (Concat w32 (Read w8 (Add w32 3 N9:(Mul w32 4 N1)) + U2) + (Concat w24 (Read w8 (Add w32 2 N9) + U2) + (ReadLSB w16 N9 U2))))) +# OK -- Elapsed: 0.000321865 +# Is Valid: false + +# Query 16 -- Type: InitialValues, Instructions: 137 +(query [(Ult N0:(Concat w32 (Read w8 3 arr65) + (Concat w24 (Read w8 2 arr65) + (ReadLSB w16 0 arr65))) + 16) + (Ult N1:(Concat w32 (Read w8 3 arr72) + (Concat w24 (Read w8 2 arr72) + (ReadLSB w16 0 arr72))) + 16) + (Ult N2:(Concat w32 (Read w8 3 arr79) + (Concat w24 (Read w8 2 arr79) + (ReadLSB w16 0 arr79))) + 16) + (Not (And (Not (Eq 3 + N3:(Concat w32 (Read w8 3 arr86) + (Concat w24 (Read w8 2 arr86) + (ReadLSB w16 0 arr86))))) + (And (Not (Eq 2 N3)) + (And (Not (Eq 1 N3)) + (Not (Eq 0 N3)))))) + (Eq 104 + (Read w8 0 U0:[N3=0, + 1=97] @ arr60)) + (Slt 2 + N4:(Concat w32 (Read w8 3 U0) + (Concat w24 (Read w8 2 U0) + (Concat w16 (Read w8 1 U0) (w8 104))))) + (Eq (Concat w32 (Read w8 51 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr60))), + (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 arr60))), + (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]) + (Concat w24 (Read w8 50 U1) + (ReadLSB w16 48 U1))) + N4) + (Not (Eq 32 + (Concat w32 (Read w8 (Add w32 3 N9:(Mul w32 4 N1)) + U2) + (Concat w24 (Read w8 (Add w32 2 N9) + U2) + (ReadLSB w16 N9 U2)))))] + false) +# OK -- Elapsed: 0.000178814 +# Solvable: true +# arr60 = [104,0,0,0] +# arr65 = [12,0,0,0] +# arr72 = [0,0,0,0] +# arr79 = [0,0,0,0] +# arr86 = [1,0,0,0] diff --git a/test/Expr/Parser/dg.exp b/test/Expr/Parser/dg.exp new file mode 100644 index 00000000..94fc4df8 --- /dev/null +++ b/test/Expr/Parser/dg.exp @@ -0,0 +1,3 @@ +load_lib llvm.exp + +RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]] -- cgit 1.4.1