diff --git a/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java b/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java index 315534eac4cd53e670dce36aa6ad3854adf7033a..c58728a27700094071b9274e882e6110ec58b367 100644 --- a/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java +++ b/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java @@ -28,6 +28,9 @@ */ package ca.mcscert.jtet.cvc3generator; +import ca.mcscert.jtet.expression.BinaryOperation; +import ca.mcscert.jtet.expression.CheckerGeneratorSpy; +import ca.mcscert.jtet.expression.FixedPointVariableType; import ca.mcscert.jtet.expression.VariableCollection; import ca.mcscert.jtet.parsers.MatlabParser; import ca.mcscert.jtet.expression.BooleanVariableType; @@ -129,8 +132,16 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec @Override public void handleLeafCell(Cell cell) { - // First get the appropriate CVC3 code from matlab. - String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type); + // First get the appropriate CVC3 code from matlab. Capture generation for further processing. + CheckerGeneratorSpy spy = new CheckerGeneratorSpy(m_CVC3Generator); + String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(spy, BooleanVariableType.Type); + + // Next, find all the fixed point expressions and handle them. + for(CheckerGeneratorSpy.SpiedBinaryOp op : spy.getBinaryOps()) { + if (op.usedType instanceof FixedPointVariableType) { + generateOverflowTCC(op); + } + } // Next form the disjoint queries and add to the list. for(String otherCellCode : m_currentCompleteQueries) { @@ -142,6 +153,54 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec m_currentCompleteQueries.add(newCellCode); } + private void generateOverflowTCC(CheckerGeneratorSpy.SpiedBinaryOp binaryOp) { + // Comparisons never overflow, so ignore them. + switch (binaryOp.op) { + case GreaterThen: + case GreaterThenEqual: + case LessThen: + case LessThenEqual: + case Equals: + case NotEquals: + return; + } + FixedPointVariableType type = (FixedPointVariableType) binaryOp.usedType; + if (!type.isSigned() && binaryOp.op == BinaryOperation.Division) { + return ; // Skip this generation. Unsigned division requires no checks, since it never over/under flows. + } + + m_output += "ECHO \"begin" + m_currentTCC + "\";\n"; + m_output += "PUSH;\n"; + + String query = null; + //@todo: Handle signed integers. + switch (binaryOp.op) { + case Addition: + // Extend the addition and verify the extra bit remains unchanged. + query = "QUERY BVPLUS(" + (type.digits() + 1) + "," + binaryOp.lhsExp + "," + binaryOp.rhsExp + ")[" + + (type.digits() + 1) + ":" + type.digits() + "] = 0bin0;"; + break; + case Minus: + // Test rhs <= lhs, which guarantees this case as (lhs >= rhs => lhs - rhs > 0). + query = "QUERY BVLE(" + binaryOp.rhsExp + "," + binaryOp.lhsExp + ");"; + break; + case Multiplication: + // Extend the addition and test extra bits remain zero, like addition. + query = "QUERY BVMULT(" + (type.digits() * 2) + "," + binaryOp.lhsExp + "," + binaryOp.rhsExp + ")[" + + (type.digits() * 2 - 1) + ":" + type.digits() + "] = 0bin" + StringUtils.repeat('0', type.digits()) + ";"; + break; + case Division: + // Unsigned never overflows, as the result never grows. We skip any generation, so we should never come here. + throw new IllegalStateException("No check necessary for unsigned division! Should never get here!"); + } + m_queries.add(query); + m_output += query + "\n"; + + m_output += "POP;\n"; + m_output += "ECHO \"end" + m_currentTCC + "\";\n"; + m_currentTCC++; // For now, just screw up the TCC counting. + } + @Override public String getFinalString() { if (m_currentlyRunning) { @@ -161,7 +220,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec List m_currentDisjointQueries = new ArrayList(); List m_currentCompleteQueries = new ArrayList(); - + boolean m_currentlyRunning = true; int m_currentTCC = 1; diff --git a/src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java b/src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java index 289a0046d03589f48b10b88f3cfe0d0535b3131f..dc730e618c38539c80d604a1950f8738f10ae111 100644 --- a/src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java +++ b/src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java @@ -102,5 +102,60 @@ public class HierarchicalGridCVC3GeneratorTest { assertEquals(expected, out); } + // Exercise the cvc3 generator's overflow protection + @Test + public void testCVC3GeneratorOverflow() { + HierarchicalGrid grid = new HierarchicalGrid(); + List topCells = grid.getSubHierarchy(); + + topCells.add(new HierarchicalCell("(x + y) > 0")); + topCells.add(new HierarchicalCell("(x * y) == 0")); + topCells.add(new HierarchicalCell("(x / y) > 0")); + + List nextGrid = topCells.get(1).getSubHierarchy(); + nextGrid.add(new HierarchicalCell("(x - y) > 0")); + + String out = HierarchicalGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridCVC3Generator(variableParser.parseVariables("x:fixedt(0,8,0),y:fixedt(0,8,0)"), 1)); + + String expected = "ECHO \"begin1\";\n" + + "PUSH;\n" + + "QUERY BVPLUS(9,x,y)[9:8] = 0bin0;\n" + + "POP;\n" + + "ECHO \"end1\";\n" + + "ECHO \"begin2\";\n" + + "PUSH;\n" + + "QUERY BVMULT(16,x,y)[15:8] = 0bin00000000;\n" + + "POP;\n" + + "ECHO \"end2\";\n" + + "ECHO \"begin3\";\n" + + "PUSH;\n" + + "QUERY (NOT ( BVGT(BVPLUS(8,x,y),0bin00000000) AND (BVMULT(8,x,y) = 0bin00000000) ) AND\n" + + "NOT ( BVGT(BVPLUS(8,x,y),0bin00000000) AND BVGT(BVUDIV(x,y),0bin00000000) ) AND\n" + + "NOT ( (BVMULT(8,x,y) = 0bin00000000) AND BVGT(BVUDIV(x,y),0bin00000000) ));\n" + + "POP;\n" + + "ECHO \"end3\";\n" + + "ECHO \"begin4\";\n" + + "PUSH;\n" + + "QUERY (BVGT(BVPLUS(8,x,y),0bin00000000) OR (BVMULT(8,x,y) = 0bin00000000) OR BVGT(BVUDIV(x,y),0bin00000000));\n" + + "POP;\n" + + "ECHO \"end4\";\n" + + "ECHO \"begin5\";\n" + + "PUSH;\n" + + "QUERY BVLE(y,x);\n" + + "POP;\n" + + "ECHO \"end5\";\n" + + "ECHO \"begin6\";\n" + + "PUSH;\n" + + "QUERY ((BVMULT(8,x,y) = 0bin00000000)) => ();\n" + + "POP;\n" + + "ECHO \"end6\";\n" + + "ECHO \"begin7\";\n" + + "PUSH;\n" + + "QUERY ((BVMULT(8,x,y) = 0bin00000000)) => (BVGT(BVSUB(8,x,y),0bin00000000));\n" + + "POP;\n" + + "ECHO \"end7\";\n"; + assertEquals(expected, out); + } + VariableParser variableParser = new VariableParser(); }