Goose  Artifact [47cdd36bc0]

Artifact 47cdd36bc07219ecae311c484c07c5e398298ff8855f1018265734f94e18e97f:

• File bs/verify/gfctracker.h — part of check-in [0db147f117] at 2024-09-15 20:24:31 on branch cir-ssa-refactor — Add clang format settings, reformat everything (user: achavasse size: 1599)

#ifndef GOOSE_VERIFY_GFCTRACKER_H
#define GOOSE_VERIFY_GFCTRACKER_H

namespace goose::verify
{
    class Builder;

    class GFCTracker
    {
      public:
        GFCTracker( size_t size ) :
            m_gfcStorage( size )
        {
        }

        optional< Z3Val > retrieve( Builder& b, uint32_t bbIndex, const GhostFuncApplication& gfa );
        void set( Builder& b, const GhostFuncApplication& gfa, Z3Val&& val );

      private:
        uint32_t getGFIndex( const GhostFuncApplication& gfa );
        z3::expr buildFunctionApplication(
            Builder& b, uint32_t uid, const GhostFuncDeclCache::GFDecl& gfDecl, const Value& gf );
        z3::expr buildFunctionApplication( Builder& b, uint32_t uid,
            const GhostFuncDeclCache::GFDecl& gfDecl, const GhostFuncApplication& gfa );

        uint32_t getCurrentUidForBasicBlock( uint32_t bbIndex, uint32_t gfIndex ) const;
        void setCurrentUidForBasicBlock( uint32_t bbIndex, uint32_t gfIndex, uint32_t uid );

        void setForBasicBlock( Builder& b, uint32_t bbIndex, const GhostFuncApplication& gfa,
            uint32_t gfIndex, const GhostFuncDeclCache::GFDecl& gfDecl, z3::expr&& expr );

        // Each ghost func have a unique index within the current function.
        // (0: invalid index)
        unordered_map< Value, uint32_t > m_ghostFuncIndices;

        // For each ghostfunc closure, store its last index.
        using GFCState = llvm::SmallVector< uint32_t, 16 >;
        using GFCStorage = cir::TempStorage< GFCState >;

        GFCStorage m_gfcStorage;
    };
} // namespace goose::verify

#endif