Permission Management

[The-Ray-Man]

Tracking: Permission Management System (Fold/Unfold)

This issue tracks the implementation of the permission management strategy as defined in the folding-unfolding.md design document. The core goal is to integrate Uniqueness Analysis results into the translation process to automate predicate folding and unfolding.

Phase 1: Data Extraction & Association

• Uniqueness Analysis Integration:
  • Execute uniqueness analysis for every method to extract flow facts.
  • Location: Hook into registerForVerification within ProgramConverter.
• FIR-to-CFG Mapping:
  • Implement a DFS traversal on CFGNodes to build a mapping from FirElement to its corresponding CFGNodes.
  • Requirement: Store only the first and last nodes for each element.
  • Note: Pay close attention to edge cases where FIR elements may not map 1:1 to CFG structures.

Phase 2: Core Infrastructure Updates

• State Persistence in MethodConverter:
  • Store the firToNodes map and flowFacts within MethodConverter to make them accessible during the FirElement -> ExpEmbedding translation.
• ExpEmbedding Interface Changes:
  • Add properties to represent the Uniqueness state both before and after expression execution.
  • Add a property to track used paths, implemented via a recursive lookup.

Phase 3: Translation & Logic Implementation

• Update StmtConversionVisitor:
  • Modify the visitor to inject the Uniqueness state into generated ExpEmbeddings where applicable.
• Permission Management Logic:
  • Create a PermissionManagement object/service.
  • Responsibility 1: Identify necessary fold/unfold operations for a given ExpEmbedding.
  • Responsibility 2: Extract necessary invariants.
• Unique Predicate Logic:
  • Update the in the design repository mentioned ExpEmbeddings to insert folds and unfolds of unique predicates where necessary.
    • Declare
    • Assign
    • FieldModification
    • MethodCall
    • Return. Partially Implemented - missing support from uniqueness checker.
    • If
    • While
    • Elvis missing support from uniqueness checker.
• Shared Predicate Logic:
  • Update the FieldAccess embedding to handle the decision logic for unfolding shared predicates.

Currently not Supported:

• member functions. It is yet unclear how to handle the uniqueness type of the receiver.
• fold/unfold of fields that were inherited.