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

6 files changed, 97 insertions, 30 deletions

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