Add signed checks to the cvc3 overflow detector. (40b543ad) · Commits · tables / jtet

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

+33 −2

Original line number	Diff line number	Diff line
		@@ -173,7 +173,37 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec
		m_output += "PUSH;\n";

		String query = null;
		//@todo: Handle signed integers.
		if (((FixedPointVariableType) binaryOp.usedType).isSigned()) {
		switch (binaryOp.op) {
		case Addition:
		// Verify the sign bit doesn't change as appropriate. Only on the sign bits being equal can an error occur, and only if the output sign differs.
		query = "QUERY ((x[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin0 AND y[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin0) " +
		"=> BVPLUS(" + type.digits() + ",x,y)[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin0) AND " +
		"((x[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin1 AND y[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin1) " +
		"=> BVPLUS(" + type.digits() + ",x,y)[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin1);";
		break;
		case Minus:
		// Verify the sign bit doesn't change as appropriate. Only on the sign bits being equal can an error occur, and only if the output sign differs.
		query = "QUERY ((x[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin0 AND y[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin1) " +
		"=> BVPLUS(" + type.digits() + ",x,y)[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin0) AND " +
		"((x[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin1 AND y[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin0) " +
		"=> BVPLUS(" + type.digits() + ",x,y)[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = 0bin1);";
		break;
		case Multiplication:
		// Same as unsigned, sign extend and verify the extra bits don't change to the wrong value. Same signs is all 0, different signs are all 1.
		query = "QUERY ((x[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] = y[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "]) => BVMULT(" +
		(type.digits() * 2) + ",SX(" + binaryOp.lhsExp + "," + (type.digits() * 2) + "),SX(" + binaryOp.rhsExp + "," + (type.digits() * 2) + "))[" +
		(type.digits() * 2 - 1) + ":" + (type.digits() - 1) + "] = 0bin" + StringUtils.repeat('0', type.digits() + 1) + ") AND " +
		"((x[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "] /= y[" + (type.digits() - 1) + ":" + (type.digits() - 1) + "]) => BVMULT(" +
		(type.digits() * 2) + ",SX(" + binaryOp.lhsExp + "," + (type.digits() * 2) + "),SX(" + binaryOp.rhsExp + "," + (type.digits() * 2) + "))[" +
		(type.digits() * 2 - 1) + ":" + (type.digits() - 1) + "] = 0bin" + StringUtils.repeat('1', type.digits() + 1) + ");";
		break;
		case Division:
		// Overflow only happens when the smallest negative is multiplied by -1, as that can't be represented in the positive.
		query = "QUERY NOT (x = 0bin1" + StringUtils.repeat('0', type.digits() - 1) + " AND y = 0bin" + StringUtils.repeat('1', type.digits()) + ");";
		break;
		}
		} else {
		switch (binaryOp.op) {
		case Addition:
		// Extend the addition and verify the extra bit remains unchanged.
		@@ -193,6 +223,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec
		// 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";

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

+60 −1

Original line number	Diff line number	Diff line
		@@ -104,7 +104,7 @@ public class HierarchicalGridCVC3GeneratorTest {

		// Exercise the cvc3 generator's overflow protection
		@Test
		public void testCVC3GeneratorOverflow() {
		public void testCVC3GeneratorUnsignedOverflow() {
		HierarchicalGrid grid = new HierarchicalGrid();
		List<HierarchicalCell> topCells = grid.getSubHierarchy();

		@@ -157,5 +157,64 @@ public class HierarchicalGridCVC3GeneratorTest {
		assertEquals(expected, out);
		}

		@Test
		public void testCVC3GeneratorSignedOverflow() {
		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(1,8,0),y:fixedt(1,8,0)"), 1));

		String expected = "ECHO \"begin1\";\n" +
		"PUSH;\n" +
		"QUERY ((x[7:7] = 0bin0 AND y[7:7] = 0bin0) => BVPLUS(8,x,y)[7:7] = 0bin0) AND ((x[7:7] = 0bin1 AND y[7:7] = 0bin1) => BVPLUS(8,x,y)[7:7] = 0bin1);\n" +
		"POP;\n" +
		"ECHO \"end1\";\n" +
		"ECHO \"begin2\";\n" +
		"PUSH;\n" +
		"QUERY ((x[7:7] = y[7:7]) => BVMULT(16,SX(x,16),SX(y,16))[15:7] = 0bin000000000) AND ((x[7:7] /= y[7:7]) => BVMULT(16,SX(x,16),SX(y,16))[15:7] = 0bin111111111);\n" +
		"POP;\n" +
		"ECHO \"end2\";\n" +
		"ECHO \"begin3\";\n" +
		"PUSH;\n" +
		"QUERY NOT (x = 0bin10000000 AND y = 0bin11111111);\n" +
		"POP;\n" +
		"ECHO \"end3\";\n" +
		"ECHO \"begin4\";\n" +
		"PUSH;\n" +
		"QUERY (NOT ( BVSGT(BVPLUS(8,x,y),0bin00000000) AND (BVMULT(8,x,y) = 0bin00000000) ) AND\n" +
		"NOT ( BVSGT(BVPLUS(8,x,y),0bin00000000) AND BVSGT(BVSDIV(x,y),0bin00000000) ) AND\n" +
		"NOT ( (BVMULT(8,x,y) = 0bin00000000) AND BVSGT(BVSDIV(x,y),0bin00000000) ));\n" +
		"POP;\n" +
		"ECHO \"end4\";\n" +
		"ECHO \"begin5\";\n" +
		"PUSH;\n" +
		"QUERY (BVSGT(BVPLUS(8,x,y),0bin00000000) OR (BVMULT(8,x,y) = 0bin00000000) OR BVSGT(BVSDIV(x,y),0bin00000000));\n" +
		"POP;\n" +
		"ECHO \"end5\";\n" +
		"ECHO \"begin6\";\n" +
		"PUSH;\n" +
		"QUERY ((x[7:7] = 0bin0 AND y[7:7] = 0bin1) => BVPLUS(8,x,y)[7:7] = 0bin0) AND ((x[7:7] = 0bin1 AND y[7:7] = 0bin0) => BVPLUS(8,x,y)[7:7] = 0bin1);\n" +
		"POP;\n" +
		"ECHO \"end6\";\n" +
		"ECHO \"begin7\";\n" +
		"PUSH;\n" +
		"QUERY ((BVMULT(8,x,y) = 0bin00000000)) => ();\n" +
		"POP;\n" +
		"ECHO \"end7\";\n" +
		"ECHO \"begin8\";\n" +
		"PUSH;\n" +
		"QUERY ((BVMULT(8,x,y) = 0bin00000000)) => (BVSGT(BVSUB(8,x,y),0bin00000000));\n" +
		"POP;\n" +
		"ECHO \"end8\";\n";
		assertEquals(expected, out);
		}

		VariableParser variableParser = new VariableParser();
		}