Best way to prevent arithmetic overflow/underflows during rewriting?

[remi-delmas-3000]

Hi !

In this example I have a simple constant folding rule:

(datatype Math
  (Num i64)
  (Add Math Math)
)
(rewrite (Add (Num x) (Num y)) (Num (+ x y)))
(let expr (Add (Num 9223372036854775807) (Num 9223372036854775807)))
(run 4)
(extract expr 2)

I can trigger overflows on i64 addition

(
   (Add (Num 9223372036854775807) (Num 9223372036854775807))
   (Num -2)
)

It seems like egglog does not try to detect overflows/underflows on either i64 or rationals (which are pairs of i64), or occurences of nans/+inf on f64.

I'm trying to use egglog to simplify mathematical expressions over mathematical Ints and Rationals, so to ensure soundness I'd like to either (from worst to best):

.1 detect overflows during rewriting and trigger panics
.2 guard against applying constant folding rules if they would trigger overflows/underflows
.3 replace the i64, rationals and f64 with arbitrary precision equivalents (think GMP, MPFR, etc. )

I know that .3 is not possible without modifying the egglog source code, but would either 1 or 2 be possible as of today ?

How do people usually ensure soundness with that type of constant propagation rules ?

Thanks !

[oflatt]

Great question!
2 is certainly possible today by adding conditions to the rule.
1 and 3 require changing the primitive implementation, as you said. I think that you don't actually have to change egglog though, there are public rust APIs for adding new primitives (not well documented unfortunately)

[remi-delmas-3000]

Thank you for your answer !

2 is certainly possible today by adding conditions to the rule.

Can that be done from the egglog DSL or do we need to do that through the Rust API ? The overflow conditions would require disjunctions and references to i64::MAX or i64::MIN. It seems like the DSL only supports conjunctions as guards.

there are public rust APIs for adding new primitives (not well documented unfortunately)

Do you have a pointer to the API in question ?

[oflatt]

Here's the API I was thinking of:
https://docs.rs/egglog/latest/egglog/struct.EGraph.html#method.add_primitive
Let us know if there are problems with it or things that we forgot to make public!

[oflatt]

I was imagining doing 2 from the egglog DSL, defining a max and min int yourself using globals
There is a boolean or in egglog, defined here: https://github.com/egraphs-good/egglog/blob/main/src/sort/bool.rs
We could really use some documentation of the primitive operators!

[oflatt]

There's also a bool-> here:

egglog/src/sort/i64.rs

Line 58 in ecc3be5

add_primitives!(typeinfo, "bool-<" = |a: i64, b: i64| -> bool { a < b });

It produces a boolean instead of an egglog filter

[remi-delmas-3000]

Thank you !

[saulshanabrook]

If there was a way to add over/underflow protection to the builtins here as well I could see that being useful generally!