Move complete handling of functions to `MathLibraryModel`, support additional functions #750

schuessf · 2025-09-29T14:52:02Z

PR #714 refactored the way standard functions in C are modeled in Boogie. As a result, separate classes are now used to handle functions from specific C libraries. In particular, the class MathLibraryModel is responsible for modeling functions from math.h. However, in case of MathLibraryModel the actual translation is delegated to BitvectorTranslation::constructOtherUnaryFloatOperation and BitvectorTranslation::constructOtherBinaryFloatOperation (the other implementations of those methods in IntegerTranslation simply throw an exception, since these float operations are not supported), while FloatFunction serves as some kind of connection (with some hacky string operations to determine the C type). Consequently, whenever support for new math library functions is added, three classes had to be changed (MathLibraryModel, BitvectorTranslation, FloatFunction), which made the process cumbersome.

Therefore, this PR removed all the handling of standard functions from BitvectorTranslation, as well as the (rather hacky) class FloatFunction and moved the translation of functions from math.h entirely to MathLibraryModel (similar as done in other library models). To facilitate this, new methods were added to ExpressionTranslation to serve as a proper API. In BitvectorTranslation these methods implement calls to SMT-defined floating-point theory functions, while in IntegerTranslation, they throw exceptions.

Additionally, this PR added support for more functions from math.h (with the help of overapproximations):

signbit, remainder, copysign: They were removed in 042d866 (see this comment), and since then only an exception was thrown. This was due to an unsoundness, since we were not able to handle negative NaNs in SMT, but they can occur in C (with the help of copysign). While some efforts were made to handle these cases precisely (see Represent ambivalent floats as bitvectors #440), they were left incomplete, so this PR uses overapproximations instead. Specifically, when NaN values appear as arguments to copysign or signbit, the result is safely overapproximated, which remains precise enough for most of the cases.
Several numeric functions (e.g., sin, exp, ...) were added, with an error handling (i.e., ±0, ±∞ and NaN as arguments) according to the C standard. For all other return values, a very coarse overapproximation is used, capturing simple properties - for example sin(x) is always between -1 and 1, and exp(x) is always at least x+1. Despite this coarse overapproximation, the translation should still be precise enough to verify some (very simple) tasks of the neural-networks benchmarks.

("The CNF conversion does not support quantifiers")

(precise except for NaN)

…and fmod explicitly

danieldietsch · 2025-09-30T07:54:15Z

@schuessf @bahnwaerter does this lead to conflicts with the refactored memory model?

schuessf · 2025-09-30T08:06:56Z

@schuessf @bahnwaerter does this lead to conflicts with the refactored memory model?

I don't think so, this PR basically just changes MathLibraryModel and removes two methods from BitvectorTranslation, whereas the memory model refactoring mostly changes MemoryHandler.

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

maul-esel

👍 Thanks for making this effort to further improve our library handling, and even extending it!

I don't know much about floating-point arithmetic, so I couldn't review those aspects in detail. I have left some comments/questions mostly on the architecture.

maul-esel · 2025-09-30T09:47:01Z

...eiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java

 	}

+	private ExpressionResult handleSqrt(final IDispatcher main, final IASTFunctionCallExpression node,
+			final ILocation loc, final String name, final CPrimitive type) {


minor refactoring suggestion: why not let these kinds of methods take a CPrimitives and have one new CPrimitive(...) call in the method, rather than one in every usage? This will improve readability of getFunctionModels.

...ltimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java

...k/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java

…tion

maul-esel

Just a couple more small comments.

...cdt/translation/implementation/base/expressiontranslation/BitvectorFloatingPointHandler.java

...ultimate/cdt/translation/implementation/base/expressiontranslation/BitvectorTranslation.java

...ltimate/cdt/translation/implementation/base/expressiontranslation/ExpressionTranslation.java

...cdt/translation/implementation/base/expressiontranslation/BitvectorFloatingPointHandler.java

maul-esel · 2025-10-02T11:09:53Z

...k/ultimate/cdt/translation/implementation/base/expressiontranslation/IntegerTranslation.java

-	}
-
 	@Override
 	public Expression getCurrentRoundingMode() {


Another candidate that could potentially be moved to IFloatingPointHandler

...t/translation/implementation/base/expressiontranslation/UnsupportedFloatingPointHandler.java

bahnwaerter · 2025-10-07T22:04:45Z

@schuessf @bahnwaerter does this lead to conflicts with the refactored memory model?

I don't think so, this PR basically just changes MathLibraryModel and removes two methods from BitvectorTranslation, whereas the memory model refactoring mostly changes MemoryHandler.

You're right. The changes only affect the memory model, which particularly affects the memory structure and addressing. There may be a small merge conflict, but this should be very easy to resolve. I would suggest that we merge the memory model first (as soon as the last unsoundness issues have been resolved) and then merge this pull request.

trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-2.c

...t/translation/implementation/base/expressiontranslation/UnsupportedFloatingPointHandler.java

Co-authored-by: Dominik Klumpp <[email protected]>

schuessf · 2025-10-15T12:45:01Z

...eiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java

+		// signbit(x) := isNegative(x) ? 1 : 0;
+		new OverapproxVariable("sign of NaN", loc).annotate(nondet);
+		final Expression zero = mExpressionTranslation.constructLiteralForIntegerType(loc, intType, BigInteger.ZERO);
+		builder.addStatement(StatementFactory.constructIfStatement(loc, mFloatHandler.isNan(loc, argument, type),


@danieldietsch @Heizmann As you have worked with floats in the past, does this handling of signbit (incl. the overapproximation) seem reasonable?

schuessf · 2025-10-15T12:45:11Z

...eiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java

+								type)));
+		// TODO: Overapproximate if second is NaN
+		new OverapproxVariable("sign of NaN", loc).annotate(nondet);
+		builder.addStatement(StatementFactory.constructIfStatement(loc, mFloatHandler.isNan(loc, first, type),


@danieldietsch @Heizmann As you have worked with floats in the past, does this handling of copysign (incl. the overapproximation) seem reasonable?

schuessf · 2025-10-15T12:50:32Z

...eiburg/informatik/ultimate/cdt/translation/implementation/base/library/MathLibraryModel.java

+		final List<ExpressionResult> arguments = handleFloatArguments(main, node, loc, name, 2, type);
+		final Expression first = arguments.get(0).getLrValue().getValue();
+		final Expression second = arguments.get(1).getLrValue().getValue();
+		return new ExpressionResultBuilder().addAllExceptLrValue(arguments)


@danieldietsch In 042d866 you removed also the support for remainder, claiming in this comment that our handling was also unsound. In this PR, however, I added support again using the SMT function fp.rem. The documentations for fp.rem and remainder seemed to match and I could not find any unsoundness. Do you remember the issue with remainder?

schuessf added 30 commits August 6, 2025 16:36

Minor: Use switch

39223e3

Add support for __builtin_isinf_sign

ccd24bb

Return ExpressionResult instead of RValue

c25732f

Add helper function

1a66829

Add AuxVarInfoBuilder as a parameter

e0e4141

Overapproximate some arithmetic float functions

63bdab8

Add tests

73a4810

Towards a proper API for float functions

9522cf5

Move handling of some functions to MathLibraryModel

8034038

Support linux functions again

3283cf0

Move more function to MathLibraryModel

330e0e8

Move handling of float functions to MathLibraryModel

6c011c8

Remove FloatFunction (not needed anymore)

23ff49d

Remove unused method, rename method

48d1ae7

Bugfix: Function names

a32c07c

Bugfix: Wrong function

543f4ab

Bugfix: Wrong type

1c8eb22

Move tests that are not supported by MathSAT

727c84a

("The CNF conversion does not support quantifiers")

Make tests slightly easier (to succeed in regression tests)

46a0d13

Move number classification macros to MathLibraryModel

4d851bd

Add comments, minor changes

66aae93

Fix typo

bf7a0d4

Move TODOs to overapproximated functions

0b25900

Overapproximate fmod, restructure TODOs

d229a66

Pass RoundingMode as expression

a036861

Support rounding functions using the current rounding mode

5ca4edb

Add more precise overapproximations for signbit and copysign

90bdd6f

(precise except for NaN)

Remove generic overapproximation handling, overapproximate remainder …

1875505

…and fmod explicitly

Move tests from todo to regression again

f464a71

Support remainder properly

82e5778

schuessf added 3 commits August 22, 2025 10:51

Use assertions from ESMBC tests that should pass

5b01a3b

Bugfix: Use abs in fmod

e8b7474

Use remainderf instead of remainder (seems easier for SMT solvers)

07e8290

schuessf requested review from Heizmann, danieldietsch and maul-esel September 29, 2025 14:52

schuessf added feature C translation float Things that originate from the treatment of IEEE 754 floats labels Sep 29, 2025

schuessf added 2 commits September 30, 2025 10:23

Merge branch 'dev' into float-functions

5064033

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

Fix comment

65b5143

maul-esel reviewed Sep 30, 2025

View reviewed changes

schuessf added 3 commits October 1, 2025 18:04

Introduce IFloatingPointHandler, more refactoring in BitvectorTransla…

c334a14

…tion

Bugfix: boolean return typess

6f88a4b

Add headers

3953fe2

maul-esel reviewed Oct 2, 2025

View reviewed changes

schuessf added 5 commits October 2, 2025 13:41

Move interface to own file

d973c03

Store IFloatingPointHandler instance in field

ee444e8

Bugfix: Order of arguments

2cd309e

Merge branch 'dev' into float-functions

f78ba90

Add some documentation

a718cdf

maul-esel approved these changes Oct 9, 2025

View reviewed changes

trunk/examples/programs/FloatingPoint/regression/c/all/ctrans-float-copysign-2.c Outdated Show resolved Hide resolved

...t/translation/implementation/base/expressiontranslation/UnsupportedFloatingPointHandler.java Outdated Show resolved Hide resolved

schuessf and others added 4 commits October 10, 2025 09:36

Update documentation

b45b622

Co-authored-by: Dominik Klumpp <[email protected]>

Add comments for outcommented assertions

6a390c5

Add timeouts to .testignore

9acfa12

Add another timeout to .testignore

47b3e22

schuessf commented Oct 15, 2025

View reviewed changes

Move complete handling of functions to MathLibraryModel, support additional functions #750

Are you sure you want to change the base?

Move complete handling of functions to MathLibraryModel, support additional functions #750

Uh oh!

Conversation

schuessf commented Sep 29, 2025

Uh oh!

danieldietsch commented Sep 30, 2025

Uh oh!

schuessf commented Sep 30, 2025

Uh oh!

maul-esel left a comment

Choose a reason for hiding this comment

Uh oh!

maul-esel Sep 30, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

maul-esel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

maul-esel Oct 2, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

bahnwaerter commented Oct 7, 2025

Uh oh!

Uh oh!

Uh oh!

schuessf Oct 15, 2025

Choose a reason for hiding this comment

Uh oh!

schuessf Oct 15, 2025

Choose a reason for hiding this comment

Uh oh!

schuessf Oct 15, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Move complete handling of functions to `MathLibraryModel`, support additional functions #750

Move complete handling of functions to `MathLibraryModel`, support additional functions #750