Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support of complex type constraints #41

Merged
merged 15 commits into from
Jul 26, 2023
Merged

Support of complex type constraints #41

merged 15 commits into from
Jul 26, 2023

Conversation

sergeypospelov
Copy link
Member

@sergeypospelov sergeypospelov commented Jul 18, 2023

The PR adds complex type constraints:

  • UIsSubtypeExpr
  • UIsSupertypeExpr

Details

UTypeSolver

Extracted verify function to a separated class UTypeSolver to simplify configuring.

Previously, the constraint (%1 == 42 || %2 <: A) caused RE, because USolverBase and UTypeSolver didn't support propositional variables for type constraints. The PR fixes it in the following way:

  • While translating type constraints, keep their mkConsts declarations.
  • When decoding a model, iterate over its declarations and get those one, which refer to type constraints. Include their interpretation.
  • When performing a type constraints check, in UTypeSolver include the information about interpreted UIsSubtypeExpr and UIsSupertypeExpr.
  • If the current region becomes empty, then add the conflict lemma with the reference disequalities and related propositional variables.

UIsSupertypeExpr

Add a special type constraint for expressing the type of the ref is supertype of the subtype.

class UIsSupertypeExpr<Type> internal constructor(
    ctx: UContext,
    val ref: UHeapRef,
    val subtype: Type,
) : USymbol<UBoolSort>(ctx) { ... }

Now it's unused, but it's necessary for type connections and virtual invokes, which will be added in the future.

Minor

  • Changed type of refs in equality constraints from UHeapRef to USymbolicHeapRef
  • Introduced UTransformer
  • Added explicit error reasons in expressions and components
  • Made some renames in UTypeSystem and related entities
  • Added some simple optimizations in UTypeRegion

PR TODO:

  • Tests
  • Fix TODOs
  • Comments
  • Description

@sergeypospelov sergeypospelov force-pushed the sergey/instanceof branch 2 times, most recently from d777277 to da6b53d Compare July 20, 2023 12:09
@sergeypospelov sergeypospelov changed the title WIP: Support of complex type constraints Support of complex type constraints Jul 24, 2023
@sergeypospelov
Copy link
Member Author

sergeypospelov commented Jul 26, 2023

@Damtev, could you review again? Unresolve conversations if something is unclear.

Copy link
Member

@Damtev Damtev left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@sergeypospelov sergeypospelov merged commit df42a40 into main Jul 26, 2023
1 check passed
@sergeypospelov sergeypospelov deleted the sergey/instanceof branch August 21, 2023 07:14
@sergeypospelov sergeypospelov mentioned this pull request Aug 21, 2023
57 tasks
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