Skip to content

Conversation

@csanadtelbisz
Copy link
Contributor

@csanadtelbisz csanadtelbisz commented Jun 24, 2025

Making the statements, expressions and types serializable. For this, the relevant classes were converted into Kotlin.

Important changes:

  • The above classes are Kotlin data classes now that are serializable. Serialization is not automatic (it can only be automatic with sealed classes but we have expressions defined in different modules so this is not an option). A KSP task is introduced that automatically generates a serialization module containing serializers for the classes in the core module. These serialization modules (e.g., hu.bme.mit.theta.core.type.generated.expr.exprSerializerModule) can be used for serialization. Note that the serialization module has to be extended whenever a new expression/type is declared in a different (gradle project) module. See the core serialization module definition in SerializerModule.kt that can be included in extended module definitions.
  • Hash codes and equals function implementations are removed from the above classes: they are replaced by the auto-generated ones for Kotlin data classes. The equals (and/or hashcode implementations) are preserved when it does not trivially compares the attributes (e.g., signedness is not considered in some classes). Declarations such as VarDecl or ParamDecl were only considered equal when we had the same references: since this is not representable in a serialized form of the instances, a new id attribute is added to Decl for the sole purpose of serialization. Do not use this id in other contexts.

csanadtelbisz and others added 30 commits June 17, 2025 10:19
…tion-ai

# Conflicts:
#	subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
#	subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvType.java
#	subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java
#	subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibExprTransformer.java
#	subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibTermTransformer.java
#	subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java
#	subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt
@csanadtelbisz csanadtelbisz marked this pull request as ready for review July 1, 2025 13:57
@csanadtelbisz csanadtelbisz requested a review from Copilot July 1, 2025 13:58

This comment was marked as off-topic.

@csanadtelbisz csanadtelbisz force-pushed the stmt-expr-serialization-ai branch from ff7cb8c to 3adb961 Compare July 18, 2025 13:43
@leventeBajczi leventeBajczi requested a review from kris7t September 1, 2025 16:11
@kris7t
Copy link
Contributor

kris7t commented Sep 2, 2025

Does the migration of the Stmt and Expr classes from Java to Kotlin lead to API breakage in other branches, especially long-running ones? While this is not a blocker (although @leventeBajczi could probably provide more insight on the Theta API stability policy), it should be something we watch out for (and preferably document) to help us in future merges/rebases.

@csanadtelbisz
Copy link
Contributor Author

Does the migration of the Stmt and Expr classes from Java to Kotlin lead to API breakage in other branches, especially long-running ones?

The only breaking changes that I am aware of (but they are not really changes in the API, rather consequences of Java-Kotlin conversion):

  • All methods of a Kotlin object cannot be imported together with a *. So the used methods have to be manually listed. For example, see subprojects/cfa/cfa-analysis/src/main/kotlin/hu/bme/mit/theta/cfa/analysis/CfaToMonolithicExpr.kt#L35-L36 where the imports are expanded instead of simply importing import hu.bme.mit.theta.core.type.fptype.FpExprs.*
  • Tuple2s are replaced by Kotlin Pair, but it can also be used from java
  • Also, see the PR description for changes related to hash codes, but it should not cause any changes in how they behave

@csanadtelbisz csanadtelbisz added this to the svcomp26 milestone Oct 20, 2025
@csanadtelbisz csanadtelbisz self-assigned this Oct 20, 2025
@leventeBajczi
Copy link
Contributor

@csanadtelbisz, can you take a look at the conflicts?

@csanadtelbisz
Copy link
Contributor Author

I think this is not a crucial change for sv-comp, and it brings many fundamental changes (mostly refactoring that affects the core of Theta). So I vote for postponing this PR after sv-comp to avoid a hurried merge.

@csanadtelbisz csanadtelbisz removed this from the svcomp26 milestone Oct 29, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants