Add unsigned overflow checks to the system. (02810adb) · Commits · tables / jtet

src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java

+62 −3

Original line number	Diff line number	Diff line
		@@ -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) {

src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java

+55 −0

Original line number	Diff line number	Diff line
		@@ -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<HierarchicalCell> 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<HierarchicalCell> 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();
		}