Fix translation of __builtin_*_overflow functions

trunk/examples/programs/regression/c/builtin_sadd_overflow.c

@@ -0,0 +1,13 @@
+//#Safe
+/*
+ * Author: Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Date: 2024-07-02
+ */
+
+int main(){
+  int r;
+  int x = __VERIFIER_nondet_int();
+  if (x < 2) return;
+  _Bool overflow = __builtin_sadd_overflow(2147483647, x, &r);
+  //@ assert overflow;
+}

trunk/examples/programs/regression/c/builtin_sadd_overflow2.c

@@ -0,0 +1,14 @@
+//#Safe
+/*
+ * Author: Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Date: 2024-07-02
+ */
+
+int main(){
+  int r;
+  int x = __VERIFIER_nondet_short();
+  int y = __VERIFIER_nondet_short();
+  _Bool overflow = __builtin_sadd_overflow(x, y, &r);
+  //@ assert !overflow;
+  //@ assert r == x + y;
+}

trunk/examples/programs/regression/c/builtin_smul_overflow.c

@@ -0,0 +1,13 @@
+//#Safe
+/*
+ * Author: Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Date: 2024-07-02
+ */
+
+int main(){
+  int r;
+  __builtin_smul_overflow(-2147483647, 3, &r);
+  //@ assert r == -2147483645;
+  __builtin_smul_overflow(-2147483647, 6, &r);
+  //@ assert r == 6;
+}

trunk/examples/programs/regression/c/builtin_ssub_overflow.c

@@ -0,0 +1,12 @@
+//#Safe
+/*
+ * Author: Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Date: 2024-07-02
+ */
+
+int main(){
+  int r;
+  _Bool overflow = __builtin_ssub_overflow(-2147483647, 2147483647, &r);
+  //@ assert overflow;
+  //@ assert r == 2;
+}

trunk/examples/programs/regression/c/builtin_umul_overflow.c

@@ -0,0 +1,12 @@
+//#Safe
+/*
+ * Author: Frank Schüssele (schuessf@informatik.uni-freiburg.de)
+ * Date: 2024-07-02
+ */
+
+int main(){
+  int r;
+  _Bool overflow = __builtin_umul_overflow(2147483647, 3, &r);
+  //@ assert overflow;
+  //@ assert r == 2147483645;
+}

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorTranslation.java

@@ -436,6 +436,39 @@ public Expression constructArithmeticIntegerExpression(final ILocation loc, fina
 		return BitvectorFactory.constructBinaryBitvectorOperation(loc, bvop, new Expression[] { exp1, exp2 });
 	}
 
+	@Override
+	public Pair<Expression, ASTType> constructInfinitePrecisionOperation(final ILocation loc, final int operator,
+			final Expression exp1, final Expression exp2, final CPrimitive type) {
+		final int inputBitsize = computeBitsize(type);
+		final int resultBitsize;
+		final BvOp bvop;
+		if (operator == IASTBinaryExpression.op_plus) {
+			resultBitsize = inputBitsize + 1;
+			bvop = BvOp.bvadd;
+		} else if (operator == IASTBinaryExpression.op_minus) {
+			resultBitsize = inputBitsize + 1;
+			bvop = BvOp.bvsub;
+		} else if (operator == IASTBinaryExpression.op_divide) {
+			resultBitsize = inputBitsize + 1;
+			bvop = BvOp.bvsdiv;
+		} else if (operator == IASTBinaryExpression.op_multiply) {
+			resultBitsize = 2 * inputBitsize;
+			bvop = BvOp.bvmul;
+		} else {
+			throw new AssertionError("Unsupported operator for infinite precision operation: " + operator);
+		}
+		final ExtendOperation extendOp =
+				mTypeSizes.isUnsigned(type) ? ExtendOperation.zero_extend : ExtendOperation.sign_extend;
+		final Expression exp1Extended = extend(loc, exp1, extendOp, inputBitsize, resultBitsize);
+		final Expression exp2Extended = extend(loc, exp2, extendOp, inputBitsize, resultBitsize);
+		declareBitvectorFunctionForArithmeticOperation(loc, bvop, resultBitsize);
+		final Expression resultExpr =
+				BitvectorFactory.constructBinaryBitvectorOperation(loc, bvop, exp1Extended, exp2Extended);
+		final ASTType resultType =
+				new PrimitiveType(loc, BoogieType.createBitvectorType(resultBitsize), "bv" + resultBitsize);
+		return new Pair<>(resultExpr, resultType);
+	}
+
 	public void declareBitvectorFunction(final ILocation loc, final BvOp smtFunctionName,
 			final String boogieFunctionName, final boolean boogieResultTypeBool, final CPrimitive resultCType,
 			final int[] indices, final CPrimitive... paramCType) {
@@ -613,6 +646,12 @@ protected ExpressionResult convertIntToIntNonBool(final ILocation loc, final Exp
 		return new ExpressionResultBuilder().addAllExceptLrValue(operand).setLrValue(rVal).build();
 	}
 
+	@Override
+	public Expression convertInfinitePrecisionExpression(final ILocation loc, final Expression exp,
+			final CPrimitive type) {
+		return extractBits(loc, exp, computeBitsize(type), 0);
+	}
+
 	@Override
 	protected ExpressionResult convertFloatToIntNonBool(final ILocation loc, final ExpressionResult rexp,
 			final CPrimitive newType) {
@@ -1506,23 +1545,45 @@ public Pair<Expression, Expression> constructOverflowCheckForArithmeticExpressio
 
 	private Expression constructSmallerMaxIntConstraint(final ILocation loc, final CPrimitive resultType,
 			final int requiredBitsize, final Expression opResult) {
+		final BvOp operator = mTypeSizes.isUnsigned(resultType) ? BvOp.bvule : BvOp.bvsle;
 		final BigInteger maxValueAsInt = mTypeSizes.getMaxValueOfPrimitiveType(resultType);
 		final Expression maxValueAsExpr = ExpressionFactory.createBitvecLiteral(loc, maxValueAsInt, requiredBitsize);
-		final Expression smallerMaxInt = BitvectorFactory.constructBinaryBitvectorOperation(loc, BvOp.bvsle,
+		final Expression smallerMaxInt = BitvectorFactory.constructBinaryBitvectorOperation(loc, operator,
 				new Expression[] { opResult, maxValueAsExpr });
 		return smallerMaxInt;
 	}
 
 	private Expression constructBiggerMinIntConstraint(final ILocation loc, final CPrimitive resultType,
 			final int requiredBitsize, final Expression opResult) {
-		declareBitvectorFunctionForComparisonOperation(loc, BvOp.bvsle, requiredBitsize);
+		final BvOp operator = mTypeSizes.isUnsigned(resultType) ? BvOp.bvule : BvOp.bvsle;
+		declareBitvectorFunctionForComparisonOperation(loc, operator, requiredBitsize);
 		final BigInteger minValueAsInt = mTypeSizes.getMinValueOfPrimitiveType(resultType);
 		final Expression minValueAsExpr = ExpressionFactory.createBitvecLiteral(loc, minValueAsInt, requiredBitsize);
-		final Expression biggerMinInt = BitvectorFactory.constructBinaryBitvectorOperation(loc, BvOp.bvsle,
+		final Expression biggerMinInt = BitvectorFactory.constructBinaryBitvectorOperation(loc, operator,
 				new Expression[] { minValueAsExpr, opResult });
 		return biggerMinInt;
 	}
 
+	private static int computeBitsize(final ASTType type) {
+		if (!(type instanceof PrimitiveType)) {
+			throw new AssertionError("Cannot extract bitsize from type " + type);
+		}
+		final String typeName = ((PrimitiveType) type).getName();
+		if (!typeName.startsWith("bv")) {
+			throw new AssertionError("Cannot extract bitsize from type with name " + typeName);
+		}
+		return Integer.parseInt(typeName.substring(2));
+	}
+
+	@Override
+	public Expression checkInRangeInfinitePrecision(final ILocation loc, final Expression expr, final ASTType inputType,
+			final CPrimitive resultType) {
+		final int bitsize = computeBitsize(inputType);
+		final Expression greaterMin = constructBiggerMinIntConstraint(loc, resultType, bitsize, expr);
+		final Expression smallerMax = constructSmallerMaxIntConstraint(loc, resultType, bitsize, expr);
+		return ExpressionFactory.and(loc, List.of(greaterMin, smallerMax));
+	}
+
 	@Override
 	public Pair<Expression, Expression> constructOverflowCheckForUnaryExpression(final ILocation loc,
 			final int operation, final CPrimitive resultType, final Expression operand) {

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java

@@ -575,4 +575,23 @@ public abstract Pair<Expression, Expression> constructOverflowCheckForArithmetic
 
 	public abstract Pair<Expression, Expression> constructOverflowCheckForUnaryExpression(ILocation loc, int operation,
 			CPrimitive resultType, Expression operand);
+
+	/**
+	 * Construct an expression for an arithmetic expression with infinite precision. Returns a pair of the resulting
+	 * expression and a matching ASTType.
+	 */
+	public abstract Pair<Expression, ASTType> constructInfinitePrecisionOperation(ILocation loc, int operator,
+			Expression exp1, Expression exp2, CPrimitive type);
+
+	/**
+	 * Returns an expression to check whether the given expression with infinite precision fits in the resultType.
+	 */
+	public abstract Expression checkInRangeInfinitePrecision(ILocation loc, Expression expr, ASTType inputType,
+			CPrimitive resultType);
+
+	/**
+	 * Converts the given expression with infinite precision to the given type. This conversion should extract the
+	 * lowest bits that fit in type.
+	 */
+	public abstract Expression convertInfinitePrecisionExpression(ILocation loc, Expression exp, CPrimitive type);
 }

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java

@@ -242,6 +242,13 @@ public Expression constructArithmeticIntegerExpression(final ILocation loc, fina
 		}
 	}
 
+	@Override
+	public Pair<Expression, ASTType> constructInfinitePrecisionOperation(final ILocation loc, final int operator,
+			final Expression exp1, final Expression exp2, final CPrimitive type) {
+		return new Pair<>(constructArithmeticExpression(loc, operator, exp1, exp2),
+				mTypeHandler.cType2AstType(loc, type));
+	}
+
 	private Pair<Expression, Expression> applyWraparoundsIfNecessary(final ILocation loc, final Expression left,
 			final CPrimitive leftType, final Expression right, final CPrimitive rightType) {
 		if (mTypeSizes.isUnsigned(leftType)) {
@@ -394,6 +401,25 @@ private Expression convertToIntegerType(final ILocation loc, final Expression op
 				ExpressionFactory.newBinaryExpression(loc, Operator.ARITHMINUS, wrapped, range));
 	}
 
+	@Override
+	public Expression convertInfinitePrecisionExpression(final ILocation loc, final Expression exp,
+			final CPrimitive type) {
+		if (mTypeSizes.isUnsigned(type)) {
+			// For unsigned types, we apply a wraparound
+			return applyWraparound(loc, type, exp);
+		}
+		// For unsigned types, we apply a wraparound (in the corresponding unsigned type) and shift the result
+		// accordingly.
+		final CPrimitive correspondingUnsignedType = mTypeSizes.getCorrespondingUnsignedType(type);
+		final Expression wrapped = applyWraparound(loc, correspondingUnsignedType, exp);
+		final Expression maxValue = constructLiteralForIntegerType(loc, type,
+				mTypeSizes.getMaxValueOfPrimitiveType(correspondingUnsignedType).add(BigInteger.ONE));
+		final Expression shiftedToType =
+				ExpressionFactory.newBinaryExpression(loc, Operator.ARITHMINUS, wrapped, maxValue);
+		return ExpressionFactory.constructIfThenElseExpression(loc,
+				checkInRangeInfinitePrecision(loc, wrapped, null, type), wrapped, shiftedToType);
+	}
+
 	@Override
 	public CPrimitive getCTypeOfPointerComponents() {
 		return new CPrimitive(CPrimitives.LONG);
@@ -771,6 +797,14 @@ private Expression constructBiggerMinIntExpression(final ILocation loc, final CP
 				.createIntegerLiteral(loc, mTypeSizes.getMinValueOfPrimitiveType(primType).toString()));
 	}
 
+	@Override
+	public Expression checkInRangeInfinitePrecision(final ILocation loc, final Expression expr, final ASTType inputType,
+			final CPrimitive resultType) {
+		final Expression biggerMin = constructBiggerMinIntExpression(loc, resultType, expr);
+		final Expression smallerMax = constructSmallerMaxIntExpression(loc, resultType, expr);
+		return ExpressionFactory.and(loc, List.of(biggerMin, smallerMax));
+	}
+
 	@Override
 	protected Pair<Expression, Expression> constructOverflowCheckForLeftShift(final ILocation loc,
 			final CPrimitive resultType, final Expression lhsOperand, final Expression rhsOperand,

trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/standardfunctions/StandardFunctionHandler.java

@@ -53,6 +53,7 @@
 import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation.StorageClass;
 import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory;
 import de.uni_freiburg.informatik.ultimate.boogie.StatementFactory;
+import de.uni_freiburg.informatik.ultimate.boogie.ast.ASTType;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.AssertStatement;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement;
 import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement;
@@ -408,27 +409,45 @@ private Map<String, IFunctionModelHandler> getFunctionModels() {
 		 */
 		final IFunctionModelHandler overapproximateGccOverflowCheck = (main, node, loc,
 				name) -> handleByOverapproximation(main, node, loc, name, 3, new CPrimitive(CPrimitives.BOOL));
-		fill(map, "__builtin_add_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_sadd_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_saddl_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_saddll_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_uadd_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_uaddl_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_uaddll_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_sub_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_ssub_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_ssubl_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_ssubll_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_usub_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_usubl_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_usubll_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_mul_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_smul_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_smull_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_smulll_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_umul_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_umull_overflow", overapproximateGccOverflowCheck);
-		fill(map, "__builtin_umulll_overflow", overapproximateGccOverflowCheck);
+		fill(map, "__builtin_add_overflow", die);
+		fill(map, "__builtin_sadd_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_plus, new CPrimitive(CPrimitives.INT)));
+		fill(map, "__builtin_saddl_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_plus, new CPrimitive(CPrimitives.LONG)));
+		fill(map, "__builtin_saddll_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_plus, new CPrimitive(CPrimitives.LONGLONG)));
+		fill(map, "__builtin_uadd_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_plus, new CPrimitive(CPrimitives.UINT)));
+		fill(map, "__builtin_uaddl_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_plus, new CPrimitive(CPrimitives.ULONG)));
+		fill(map, "__builtin_uaddll_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_plus, new CPrimitive(CPrimitives.ULONGLONG)));
+		fill(map, "__builtin_sub_overflow", die);
+		fill(map, "__builtin_ssub_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_minus, new CPrimitive(CPrimitives.INT)));
+		fill(map, "__builtin_ssubl_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_minus, new CPrimitive(CPrimitives.LONG)));
+		fill(map, "__builtin_ssubll_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_minus, new CPrimitive(CPrimitives.LONGLONG)));
+		fill(map, "__builtin_usub_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_minus, new CPrimitive(CPrimitives.UINT)));
+		fill(map, "__builtin_usubl_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_minus, new CPrimitive(CPrimitives.ULONG)));
+		fill(map, "__builtin_usubll_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_minus, new CPrimitive(CPrimitives.ULONGLONG)));
+		fill(map, "__builtin_mul_overflow", die);
+		fill(map, "__builtin_smul_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_multiply, new CPrimitive(CPrimitives.INT)));
+		fill(map, "__builtin_smull_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_multiply, new CPrimitive(CPrimitives.LONG)));
+		fill(map, "__builtin_smulll_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_multiply, new CPrimitive(CPrimitives.LONGLONG)));
+		fill(map, "__builtin_umul_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_multiply, new CPrimitive(CPrimitives.UINT)));
+		fill(map, "__builtin_umull_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_multiply, new CPrimitive(CPrimitives.ULONG)));
+		fill(map, "__builtin_umulll_overflow", (main, node, loc, name) -> handleBuiltinOverflow(main, node, loc, name,
+				IASTBinaryExpression.op_multiply, new CPrimitive(CPrimitives.ULONGLONG)));
 		fill(map, "__builtin_add_overflow_p", overapproximateGccOverflowCheck);
 		fill(map, "__builtin_sub_overflow_p", overapproximateGccOverflowCheck);
 		fill(map, "__builtin_mul_overflow_p", overapproximateGccOverflowCheck);
@@ -2759,6 +2778,42 @@ private List<ExpressionResult> handleFloatArguments(final IDispatcher main, fina
 		return rtr;
 	}
 
+	/**
+	 * See https://gcc.gnu.org/onlinedocs/gcc/Integer-Overflow-Builtins.html for specification
+	 */
+	private Result handleBuiltinOverflow(final IDispatcher main, final IASTFunctionCallExpression node,
+			final ILocation loc, final String name, final int operator, final CPrimitive resultType) {
+		final IASTInitializerClause[] arguments = node.getArguments();
+		checkArguments(loc, 3, name, arguments);
+		final ExpressionResultBuilder builder = new ExpressionResultBuilder();
+		final ExpressionResult left = mExprResultTransformer.convertIfNecessary(loc,
+				mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[0]), resultType);
+		final ExpressionResult right = mExprResultTransformer.convertIfNecessary(loc,
+				mExprResultTransformer.transformDispatchDecaySwitchRexBoolToInt(main, loc, arguments[1]), resultType);
+		builder.addAllExceptLrValue(left, right);
+		// Apply the operator to the first two parameters with infinite precision (i.e. ignoring any wraparound or
+		// overflows), convert the result to the given type and write it to the third argument.
+		final Pair<Expression, ASTType> infinitePrecisionResult =
+				mExpressionTranslation.constructInfinitePrecisionOperation(loc, operator, left.getLrValue().getValue(),
+						right.getLrValue().getValue(), resultType);
+		final ASTType infinitePrecisionType = infinitePrecisionResult.getSecond();
+		final AuxVarInfo auxVar = mAuxVarInfoBuilder.constructAuxVarInfo(loc, infinitePrecisionType, AUXVAR.RETURNED);
+		builder.addAuxVarWithDeclaration(auxVar);
+		builder.addStatement(StatementFactory.constructSingleAssignmentStatement(loc, auxVar.getLhs(),
+				infinitePrecisionResult.getFirst()));
+		// Write the (converted) result of the operation to the third argument
+		builder.addAllExceptLrValue(mExprResultTransformer.dispatchPointerWrite(main, loc, arguments[2],
+				mExpressionTranslation.convertInfinitePrecisionExpression(loc, auxVar.getExp(), resultType)));
+		// If the infinite precision result fits in the given type, return 0 otherwise 1.
+		final Expression inRange = mExpressionTranslation.checkInRangeInfinitePrecision(loc, auxVar.getExp(),
+				infinitePrecisionType, resultType);
+		final CPrimitive boolType = new CPrimitive(CPrimitives.BOOL);
+		final Expression zero = mExpressionTranslation.constructLiteralForIntegerType(loc, boolType, BigInteger.ZERO);
+		final Expression one = mExpressionTranslation.constructLiteralForIntegerType(loc, boolType, BigInteger.ONE);
+		final Expression resultExpr = ExpressionFactory.constructIfThenElseExpression(loc, inRange, zero, one);
+		return builder.setLrValue(new RValue(resultExpr, boolType)).build();
+	}
+
 	private Result handleFloatBuiltinBinaryComparison(final IDispatcher main, final IASTFunctionCallExpression node,
 			final ILocation loc, final String name, final int op) {
 		/*