From 2757315ee9cd1e943ea1650300d9664f312e94bb Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 28 Jul 2009 11:14:04 +0000 Subject: [PATCH] Fixes defects in how arrays, especially writes over ITE expressions work. I generated 25,000 problems with the attached array generator. All files pass if optimisations are disabled. There are still defects in the array simplification code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@94 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.cpp | 17 +++- AST/ToSAT.cpp | 34 ++++++- AST/Transform.cpp | 65 ++++++++----- generated_tests/ArrayGenerator.java | 141 ++++++++++++++++++++++++++++ 4 files changed, 228 insertions(+), 29 deletions(-) create mode 100644 generated_tests/ArrayGenerator.java diff --git a/AST/AST.cpp b/AST/AST.cpp index 9c97d6d..7f44c35 100644 --- 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 bbee194..7a4aa1b 100644 --- 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 72f607a..080ee70 100644 --- 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 index 0000000..539c706 --- /dev/null +++ b/generated_tests/ArrayGenerator.java @@ -0,0 +1,141 @@ +import java.util.ArrayList; +import java.util.List; +import java.util.Random; + +/* Randomly generates problem instances that contain nested array operations */ + +// Both Indexes and values have the same bitwidth, potentially missing some errors. + +// Doesn't generate extensional problems yet.. + +public class ArrayGenerator +{ + public static List bits = new ArrayList(); + public static List arrays = new ArrayList(); + static Random r = new Random(); + + // When we get to a nesting of 5, start to return leaf nodes (like symbols). + static int MAX_DEPTH = 8; + + public static void main(String[] args) + { + bits.add("b1"); + bits.add("b2"); + bits.add("b3"); // Some case statements depend on there being 3 bitvectors. + + arrays.add("a1"); + arrays.add("a2"); + arrays.add("a3"); + + randomGenerate(); + } + + static void randomGenerate() + { + StringBuilder output = new StringBuilder(); + output.append("(\n"); + output.append("benchmark t.smt\n"); + output.append(":source {automatically generated}\n"); + output.append(":status unknown\n"); + output.append(":logic QF_BV\n"); + + for (String s : bits) + { + output.append(":extrafuns (( " + s + " BitVec[10]))\n"); + } + + for (String s : arrays) + { + output.append(":extrafuns (( " + s + " Array[10:10]))\n"); + } + + for (int i = 0; i < 10; i++) + output.append(":assumption " + generateProp(0) + "\n"); + + output.append(":formula true \n )\n"); + System.out.println(output); + } + + // Arrays are either array symbols, ites, or stores. + static String generateArray(int depth) + { + int next =r.nextInt(5); + if (depth > MAX_DEPTH) + next = next %3; + + depth++; + + switch (next) + { + case 0: + case 1: + case 2: + return arrays.get(next); + case 3: + return "(ite " + generateProp(depth) + " " + generateArray(depth) + " " + generateArray(depth) + " )"; + case 4: + return "(store " + generateArray(depth) + " " + generateBit(depth) + " " + generateBit(depth) + " )"; + } + + throw new RuntimeException("Never here"); + } + + // BitVectors. + static String generateBit(int depth) + { + + int next =r.nextInt(6); + if (depth > MAX_DEPTH) + next = next %3; + + depth++; + + switch (next) + { + case 0: + case 1: + case 2: + return bits.get(next); + + case 3: + return "(select " + generateArray(depth) + " " + generateBit(depth) + " )"; + + case 4: + return "(ite " + generateProp(depth) + " " + generateBit(depth) + " " + generateBit(depth) + " )"; + + case 5: + return "(bvadd " + generateBit(depth) + " " + generateBit(depth) + " )"; + + } + + throw new RuntimeException("Never here"); + + } + + static String generateProp(int depth) + { + int next =r.nextInt(6); + if (depth > MAX_DEPTH) + next = next %2; + + depth++; + + switch (next) + { + case 0: + return "true"; + case 1: + return "(= " + generateBit(depth) + " " + generateBit(depth) + " )"; + case 2: + return "(and " + generateProp(depth) + " " + generateProp(depth) + " )"; + case 3: + return "(bvslt " + generateBit(depth) + " " + generateBit(depth) + " )"; + case 4: + return "(iff " + generateProp(depth) + " " + generateProp(depth) + " )"; + case 5: + return "(ite " + generateProp(depth) + " " + generateProp(depth) + " " + generateProp(depth) + " )"; + } + throw new RuntimeException("Never here"); + } + +} -- 2.47.3