Add checking for functions in Prelude that may return Any of exception type

[thanhnguyen-aws]

Issue #, if available: Some functions in Python prelude that returns an exception as a value of Any type, such as PAdd, PMul,... Those exceptions are not currently caught and checked in Python to Laurel translation.

Description of changes:

• Add a suffix "!AnyMaybeException" to the names of those functions to recognize them.
• Make sure that those functions propagate the exceptions of their arguments (check and return Exceptions if any of their inputs are exception).
• Add an assertion : !Any..isexception(expr) for each outermost expr that is a StaticCall of a function whose name ends with "!AnyMaybeException".

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[tautschnig]

1. The !AnyMaybeExcept suffix convention is fragile. Using string suffix matching (funcName.endsWith "!AnyMaybeExcept") as a semantic marker is error-prone — it's easy to forget the suffix when adding new functions, and the ! character in identifiers could cause issues with parsers or tools that treat it specially. A more robust approach would be a metadata annotation or a registry (similar to how withException already checks function signatures).

2. Exception checks are duplicated at every use site. For x = a + b + c, the translation generates PAdd!AnyMaybeExcept(PAdd!AnyMaybeExcept(a, b), c). The getMaybeExceptionExprs function recursively finds both calls, generating two assertions. But the inner PAdd already propagates exceptions (its body checks isexception on inputs), so the outer assertion on the full expression would catch any inner exception too. The inner assertion is redundant — it increases the number of VCs without adding verification power.

3. getMaybeExceptionExprs only traverses StaticCall and IfThenElse. Other expression forms that could contain !AnyMaybeExcept calls (e.g., nested in Assign RHS, While conditions via Any_to_bool) are handled at the statement level but not within arbitrary expression trees. This seems intentional but could miss cases.

See inline comments.