Fixes defects in how arrays, especially writes over ITE expressions work. I generate...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@94 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/AST/AST.cpp b/AST/AST.cpp
index 9c97d6dd2cbeabe4ce11fa7ac06325e09b28d455..7f44c3516caf2188a0cc1dd17ca8e863156d0066 100644 (file)
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -1271,7 +1271,7 @@ bool BeevMgr::BVTypeCheckRecursive(const ASTNode& n)
  * typecheck as you go along. It is not suitable as a general
  * typechecker.
  *
- * This ALWAYS returns true. If there is an error it will call
+ * If this returns, this ALWAYS returns true. If there is an error it will call
  * FatalError() and abort.
  */
 
@@ -1300,18 +1300,33 @@ bool BeevMgr::BVTypeCheck(const ASTNode& n)
                                        FatalError("BVTypeCheck: length of THENbranch != length of ELSEbranch in the term t = \n", n);
                                break;
                        case READ:
+                               if (n.GetChildren().size() !=2)
+                                       FatalError("2 params to read.");
                                if (n[0].GetIndexWidth() != n[1].GetValueWidth())
                                {
                                        cerr << "Length of indexwidth of array: " << n[0] << " is : " << n[0].GetIndexWidth() << endl;
                                        cerr << "Length of the actual index is: " << n[1] << " is : " << n[1].GetValueWidth() << endl;
                                        FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n", n);
                                }
+                               if (ARRAY_TYPE != n[0].GetType())
+                                       FatalError("First parameter to read should be an array", n[0]);
+                               if (BITVECTOR_TYPE != n[1].GetType())
+                                       FatalError("Second parameter to read should be a bitvector", n[1]);
                                break;
                        case WRITE:
+                               if (n.GetChildren().size() !=3)
+                                       FatalError("3 params to write.");
                                if (n[0].GetIndexWidth() != n[1].GetValueWidth())
                                        FatalError("BVTypeCheck: length of indexwidth of array != length of actual index in the term t = \n", n);
                                if (n[0].GetValueWidth() != n[2].GetValueWidth())
                                        FatalError("BVTypeCheck: valuewidth of array != length of actual value in the term t = \n", n);
+                               if (ARRAY_TYPE != n[0].GetType())
+                                       FatalError("First parameter to read should be an array", n[0]);
+                               if (BITVECTOR_TYPE != n[1].GetType())
+                                       FatalError("Second parameter to read should be a bitvector", n[1]);
+                               if (BITVECTOR_TYPE != n[2].GetType())
+                                       FatalError("Third parameter to read should be a bitvector", n[2]);
+
                                break;
                        case BVOR:
                        case BVAND:

diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp
index bbee194d4824f8ec6b1127449ff24ec7a541a8d3..7a4aa1b6acadd6b07d54dd46872b7912ee35e07b 100644 (file)
--- a/AST/ToSAT.cpp
+++ b/AST/ToSAT.cpp
@@ -431,6 +431,7 @@ void BeevMgr::ConstructCounterExample(MINISAT::Solver& newS)
        }
 } //End of ConstructCounterExample
 
+
 // FUNCTION: accepts a non-constant term, and returns the
 // corresponding constant term with respect to a model.
 //
@@ -531,8 +532,8 @@ ASTNode BeevMgr::TermToConstTermUsingModel(const ASTNode& t, bool ArrayReadFlag)
                                FatalError("TermToConstTermUsingModel: array has 0 index width: ", arrName);
                        }
 
-                       //READ over a WRITE
-                       if (WRITE == arrName.GetKind())
+
+                       if (WRITE == arrName.GetKind()) //READ over a WRITE
                        {
                                ASTNode wrtterm = Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag);
                                if (wrtterm == term)
@@ -540,12 +541,33 @@ ASTNode BeevMgr::TermToConstTermUsingModel(const ASTNode& t, bool ArrayReadFlag)
                                        FatalError("TermToConstTermUsingModel: Read_Over_Write term must be expanded into an ITE", term);
                                }
                                ASTNode rtterm = TermToConstTermUsingModel(wrtterm, ArrayReadFlag);
+                               assert(ArrayReadFlag || (BVCONST == rtterm.GetKind()));
                                return rtterm;
                        }
-                       //READ over an ITE
-                       if (ITE == arrName.GetKind())
+                       else if (ITE == arrName.GetKind()) //READ over an ITE
                        {
-                               arrName = TermToConstTermUsingModel(arrName, ArrayReadFlag);
+                               // The "then" and "else" branch are arrays.
+                               ASTNode indexVal = TermToConstTermUsingModel(index, ArrayReadFlag);
+
+                               ASTNode condcompute = ComputeFormulaUsingModel(arrName[0]); // Get the truth value.
+                               if (ASTTrue == condcompute)
+                               {
+                                       const ASTNode & result = TermToConstTermUsingModel(CreateTerm(READ, arrName.GetValueWidth(), arrName[1], indexVal), ArrayReadFlag);
+                                       assert(ArrayReadFlag || (BVCONST == result.GetKind()));
+                                       return result;
+                               }
+                               else if (ASTFalse == condcompute)
+                               {
+                                       const ASTNode & result =  TermToConstTermUsingModel(CreateTerm(READ, arrName.GetValueWidth(), arrName[2], indexVal), ArrayReadFlag);
+                                       assert(ArrayReadFlag || (BVCONST == result.GetKind()));
+                                       return result;
+                               }
+                               else
+                               {
+                                       cerr << "TermToConstTermUsingModel: termITE: value of conditional is wrong: " << condcompute << endl;
+                                       FatalError(" TermToConstTermUsingModel: termITE: cannot compute ITE conditional against model: ", term);
+                               }
+                               FatalError("bn23143 Never Here");
                        }
 
                        ASTNode modelentry;
@@ -624,6 +646,8 @@ ASTNode BeevMgr::TermToConstTermUsingModel(const ASTNode& t, bool ArrayReadFlag)
                }
        }
 
+       assert(ArrayReadFlag || (BVCONST == output.GetKind()));
+
        //when this flag is false, we should compute the arrayread to a
        //constant. this constant is stored in the counter_example
        //datastructure

diff --git a/AST/Transform.cpp b/AST/Transform.cpp
index 72f607a54a0ad949aecf658bc4a432e4e7233366..080ee7050e61f03b893be98ba052f65ab26216fb 100644 (file)
--- a/AST/Transform.cpp
+++ b/AST/Transform.cpp
@@ -145,13 +145,13 @@ void BeevMgr::assertTransformPostConditions(const ASTNode & term)
        const Kind k = term.GetKind();
 
        // Check the signed operations have been removed.
-       assert(  SBVDIV != k);
-       assert(  SBVMOD != k);
-       assert(  SBVREM !=k);
+       assert( SBVDIV != k);
+       assert( SBVMOD != k);
+       assert( SBVREM !=k);
 
        // Check the array reads / writes have been removed
-       assert(  READ !=k );
-       assert(  WRITE !=k);
+       assert( READ !=k );
+       assert( WRITE !=k);
 
        // There should be no nodes left of type array.
        assert(0 == term.GetIndexWidth());
@@ -501,25 +501,44 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term)
                                        ASTNode writeIndex = TransformTerm(arrName[1]);
                                        ASTNode writeVal = TransformTerm(arrName[2]);
 
-                                       if (!(SYMBOL == arrName[0].GetKind() || WRITE == arrName[0].GetKind()))
-                                               FatalError("TransformArray: An array write is being attempted on a non-array:", term);
                                        if (ARRAY_TYPE != arrName[0].GetType())
                                                FatalError("TransformArray: An array write is being attempted on a non-array:", term);
 
-                                       ASTNode cond = CreateSimplifiedEQ(writeIndex, readIndex);
-                                       //TypeCheck internally created node
-                                       BVTypeCheck(cond);
-                                       ASTNode readTerm = CreateTerm(READ, width, arrName[0], readIndex);
-                                       //TypeCheck internally created node
-                                       BVTypeCheck(readTerm);
-                                       ASTNode readPushedIn = TransformArray(readTerm);
-                                       //TypeCheck internally created node
-                                       BVTypeCheck(readPushedIn);
-                                       //result = CreateTerm(ITE, arrName[0].GetValueWidth(),cond,writeVal,readPushedIn);
-                                       result = CreateSimplifiedTermITE(cond, writeVal, readPushedIn);
-
-                                       //Good idea to typecheck terms created inside the system
-                                       BVTypeCheck(result);
+                                       if ((SYMBOL == arrName[0].GetKind() || WRITE == arrName[0].GetKind()))
+                                       {
+                                               ASTNode cond = CreateSimplifiedEQ(writeIndex, readIndex);
+                                               BVTypeCheck(cond);
+
+                                               ASTNode readTerm = CreateTerm(READ, width, arrName[0], readIndex);
+                                               BVTypeCheck(readTerm);
+
+                                               ASTNode readPushedIn = TransformArray(readTerm);
+                                               BVTypeCheck(readPushedIn);
+
+                                               result = CreateSimplifiedTermITE(cond, writeVal, readPushedIn);
+
+                                               BVTypeCheck(result);
+                                       }
+                                       else if (ITE == arrName[0].GetKind())
+                                       {
+                                               // pull out the ite from the write.
+                                               ASTNode writeTrue = CreateNode(WRITE, (arrName[0][1]), writeIndex, writeVal);
+                                               writeTrue.SetIndexWidth(writeIndex.GetValueWidth());
+                                               writeTrue.SetValueWidth(writeVal.GetValueWidth());
+                                               assert(ARRAY_TYPE == writeTrue.GetType());
+
+                                               ASTNode writeFalse = CreateNode(WRITE, (arrName[0][2]), writeIndex, writeVal);
+                                               writeFalse.SetIndexWidth(writeIndex.GetValueWidth());
+                                               writeFalse.SetValueWidth(writeVal.GetValueWidth());
+                                               assert(ARRAY_TYPE == writeFalse.GetType());
+
+                                               result = CreateSimplifiedTermITE(TransformFormula(arrName[0][0]), (writeTrue), (writeFalse));
+                                               result = CreateTerm(READ, writeVal.GetValueWidth(), result, readIndex);
+                                               BVTypeCheck(result);
+                                               result = TransformArray(result);
+                                       }
+                                       else
+                                               FatalError("TransformArray: Write over bad type.");
                                        break;
                                } //end of READ over a WRITE
                                case ITE:
@@ -543,8 +562,8 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term)
                                        ASTNode t02 = term0[2];
 
                                        cond = TransformFormula(cond);
-                                       ASTNode thn = TransformTerm(t01);
-                                       ASTNode els = TransformTerm(t02);
+                                       ASTNode& thn = t01;
+                                       ASTNode& els = t02;
 
                                        if (!(t01.GetValueWidth() == t02.GetValueWidth() && t01.GetValueWidth() == thn.GetValueWidth() && t01.GetValueWidth()
                                                        == els.GetValueWidth()))

diff --git a/generated_tests/ArrayGenerator.java b/generated_tests/ArrayGenerator.java
new file mode 100644 (file)
index 0000000..539c706
--- /dev/null
+++ b/generated_tests/ArrayGenerator.java
@@ -0,0 +1,141 @@
+import java.util.ArrayList;\r
+import java.util.List;\r
+import java.util.Random;\r
+\r
+/* Randomly generates problem instances that contain nested array operations */\r
+\r
+// Both Indexes and values have the same bitwidth, potentially missing some errors.\r
+\r
+// Doesn't generate extensional problems yet..\r
+\r
+public class ArrayGenerator\r
+{\r
+    public static List<String> bits = new ArrayList<String>();\r
+    public static List<String> arrays = new ArrayList<String>();\r
+    static Random r = new Random();\r
+\r
+    // When we get to a nesting of 5, start to return leaf nodes (like symbols).\r
+    static int MAX_DEPTH = 8;\r
+    \r
+    public static void main(String[] args)\r
+    {\r
+       bits.add("b1");\r
+       bits.add("b2");\r
+       bits.add("b3"); // Some case statements depend on there being 3 bitvectors.\r
+\r
+       arrays.add("a1");\r
+       arrays.add("a2");\r
+       arrays.add("a3");\r
+\r
+       randomGenerate();\r
+    }\r
+\r
+    static void randomGenerate()\r
+    {\r
+       StringBuilder output = new StringBuilder();\r
+       output.append("(\n");\r
+       output.append("benchmark t.smt\n");\r
+       output.append(":source {automatically generated}\n");\r
+       output.append(":status unknown\n");\r
+       output.append(":logic QF_BV\n");\r
+\r
+       for (String s : bits)\r
+       {\r
+           output.append(":extrafuns (( " + s + " BitVec[10]))\n");\r
+       }\r
+\r
+       for (String s : arrays)\r
+       {\r
+           output.append(":extrafuns (( " + s + " Array[10:10]))\n");\r
+       }\r
+\r
+       for (int i = 0; i < 10; i++)\r
+           output.append(":assumption " + generateProp(0) + "\n");\r
+\r
+       output.append(":formula true \n )\n");\r
+       System.out.println(output);\r
+    }\r
+\r
+    // Arrays are either array symbols, ites, or stores.\r
+    static String generateArray(int depth)\r
+    {\r
+       int next =r.nextInt(5);\r
+       if (depth > MAX_DEPTH)\r
+           next  = next %3;\r
+\r
+       depth++;\r
+       \r
+       switch (next)\r
+       {\r
+       case 0:\r
+       case 1:\r
+       case 2:\r
+           return arrays.get(next);\r
+       case 3:\r
+           return "(ite " + generateProp(depth) + " " + generateArray(depth) + " " + generateArray(depth) + " )";\r
+       case 4:\r
+           return "(store " + generateArray(depth) + " " + generateBit(depth) + " " + generateBit(depth) + " )";\r
+       }\r
+\r
+       throw new RuntimeException("Never here");\r
+    }\r
+\r
+    // BitVectors.\r
+    static String generateBit(int depth)\r
+    {\r
+\r
+       int next =r.nextInt(6);\r
+       if (depth > MAX_DEPTH)\r
+           next  = next %3;\r
+       \r
+       depth++;\r
+       \r
+       switch (next)\r
+       {\r
+       case 0:\r
+       case 1:\r
+       case 2:\r
+           return bits.get(next);\r
+\r
+       case 3:\r
+           return "(select " + generateArray(depth) + " " + generateBit(depth) + " )";\r
+\r
+       case 4:\r
+           return "(ite " + generateProp(depth) + " " + generateBit(depth) + " " + generateBit(depth) + " )";\r
+\r
+       case 5:\r
+           return "(bvadd " + generateBit(depth) + " " + generateBit(depth) + " )";\r
+\r
+       }\r
+\r
+       throw new RuntimeException("Never here");\r
+\r
+    }\r
+\r
+    static String generateProp(int depth)\r
+    {\r
+       int next =r.nextInt(6);\r
+       if (depth > MAX_DEPTH)\r
+           next  = next %2;\r
+       \r
+       depth++;\r
+       \r
+       switch (next)\r
+       {\r
+       case 0: \r
+           return "true";\r
+       case 1:\r
+           return "(= " + generateBit(depth) + " " + generateBit(depth) + " )";\r
+       case 2: \r
+           return "(and " + generateProp(depth) + " " + generateProp(depth) + " )";\r
+       case 3: \r
+           return "(bvslt " + generateBit(depth) + " " + generateBit(depth) + " )";\r
+       case 4: \r
+           return "(iff " + generateProp(depth) + " " + generateProp(depth) + " )";\r
+       case 5: \r
+           return "(ite " + generateProp(depth) + " " + generateProp(depth) + " " + generateProp(depth) + " )";\r
+       }\r
+       throw new RuntimeException("Never here");\r
+       }\r
+\r
+}\r