From 20aebfdb32657e9427c6a2567516dc8fd8843bdb Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Sun, 7 Jun 2009 09:57:01 +0000 Subject: Implement array declarations. - Printing current prints all declarations, and we allow redefinition, since the printer doesn't know what has already been printed. - Names don't print right yet, since the Array* object doesn't have the name. - Various things are unsupported. o Array domain/range must be w32/w8. o Concrete initializers for arrays are unsupported. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73026 91177308-0d34-0410-b5e6-96231b3b80d8 --- test/Expr/Evaluate.pc | 5 +- test/Expr/Lexer/Numbers.pc | 2 +- test/Expr/Parser/Concat64.pc | 1 + test/Expr/Parser/Exprs.pc | 106 ++++++++++++++++++++++++++++--------- test/Expr/Parser/MultiByteReads.pc | 3 ++ test/Expr/Parser/TypeChecking.pc | 10 ++-- 6 files changed, 97 insertions(+), 30 deletions(-) (limited to 'test/Expr') diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.pc index 354b0489..0dac0cc8 100644 --- a/test/Expr/Evaluate.pc +++ b/test/Expr/Evaluate.pc @@ -1,8 +1,11 @@ # RUN: %kleaver -evaluate %s > %t.log +array arr0[4] : w32 -> w8 = symbolic +array arr1[8] : w32 -> w8 = symbolic + # RUN: grep "Query 0: INVALID" %t.log # Query 0 -(query [] (Not (Ult (ReadLSB w32 0 arr65) +(query [] (Not (Ult (ReadLSB w32 0 arr0) 16))) # RUN: grep "Query 1: VALID" %t.log diff --git a/test/Expr/Lexer/Numbers.pc b/test/Expr/Lexer/Numbers.pc index 6af40133..6b8e2e37 100644 --- a/test/Expr/Lexer/Numbers.pc +++ b/test/Expr/Lexer/Numbers.pc @@ -17,7 +17,7 @@ # 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 .KWArray. .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 diff --git a/test/Expr/Parser/Concat64.pc b/test/Expr/Parser/Concat64.pc index e57e9760..0b1479d4 100644 --- a/test/Expr/Parser/Concat64.pc +++ b/test/Expr/Parser/Concat64.pc @@ -1,5 +1,6 @@ # 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) diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.pc index 742a0185..4a6adf7e 100644 --- a/test/Expr/Parser/Exprs.pc +++ b/test/Expr/Parser/Exprs.pc @@ -6,64 +6,79 @@ # 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.00128889 +# 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 31543472 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000106812 -# Result: 31543472 + [(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.0014112 +# 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.00128603 +# 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 31543472 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000141144 -# Result: 31543472 + [(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.00145102 +# 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.00127888 +# 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) @@ -71,11 +86,14 @@ (Ult N0:(ReadLSB w32 0 arr67) 16)] false - [(Add w32 31543472 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000179052 -# Result: 31543472 + [(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) @@ -87,6 +105,10 @@ # 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) @@ -98,10 +120,14 @@ (And (Not (Eq 2 N0)) (And (Not (Eq 1 N0)) (Not (Eq 0 N0)))))) -# OK -- Elapsed: 0.00163794 +# 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) @@ -114,11 +140,15 @@ (And (Not (Eq 1 N0)) (Not (Eq 0 N0))))))] false - [(Add w32 31583216 N0)]) -# OK -- Elapsed: 0.000283003 -# Result: 31583219 + [(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) @@ -132,10 +162,15 @@ (Not N4:(Eq 0 N1))))))] (Or N0 (Or N2 (Or N3 N4)))) -# OK -- Elapsed: 0.00217485 +# 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) @@ -150,10 +185,15 @@ (Not (Eq 104 (Read w8 0 [N0=0, 1=97] @ arr49)))) -# OK -- Elapsed: 0.00330305 +# 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) @@ -172,10 +212,16 @@ (Concat w32 (Read w8 3 U0) (Concat w24 (Read w8 2 U0) (Concat w16 (Read w8 1 U0) (w8 104))))))) -# OK -- Elapsed: 0.00039506 +# 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) @@ -204,10 +250,16 @@ (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.018568 +# 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) @@ -238,10 +290,16 @@ N4)] (Eq 32 (ReadLSB w32 N9:(Mul w32 4 N1) U2))) -# OK -- Elapsed: 0.00105405 +# 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) @@ -278,7 +336,7 @@ arr60 arr67 arr74]) -# OK -- Elapsed: 0.00058198 +# OK -- Elapsed: 0.000574112 # Solvable: true # arr49 = [104,0,0,0] # arr53 = [12,0,0,0] diff --git a/test/Expr/Parser/MultiByteReads.pc b/test/Expr/Parser/MultiByteReads.pc index af94b516..ea2e7a5d 100644 --- a/test/Expr/Parser/MultiByteReads.pc +++ b/test/Expr/Parser/MultiByteReads.pc @@ -2,6 +2,9 @@ # RUN: grep -q "(ReadLSB w32 4 arr1)" log # RUN: grep -q "(ReadMSB w32 2 arr2)" 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) diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc index 9e29d0db..66991c20 100644 --- a/test/Expr/Parser/TypeChecking.pc +++ b/test/Expr/Parser/TypeChecking.pc @@ -2,13 +2,15 @@ -# RUN: grep "TypeChecking.pc:6:9: error: type widths do not match in binary expression" %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:12:25: error: invalid write index (doesn't match array domain)" %t.log -# RUN: grep "TypeChecking.pc:12:35: error: invalid write value (doesn't match array range)" %t.log +# 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 -(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr0) 0)] false) +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