Goose  Diff

Differences From Artifact [f64bfc172f]:

• File bs/verify/loop.cpp — part of check-in [7d2def7b75] at 2020-12-27 14:40:24 on branch trunk — Renamed "ir" to "eir" (expression intermediate representation) and "llr" to "cir" (code intermediate representation) for clarity. (user: achavasse size: 5958)

To Artifact [31ef0d646d]:

• File bs/verify/loop.cpp — part of check-in [26c691ecb9] at 2021-01-02 18:24:23 on branch trunk — Yet one more reference/address refactor: each calculation step (getting temp addr, getting var addr, selecting a member) is now a separate cir instruction. We need this level of generalization to be able to obtain addresses from anywhere, including variables and function parameters. (user: achavasse size: 5958)

68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

            m_remapper.nextLoopIteration();
            uint32_t firstInductionIterationHeaderIndex = m_remapper.remapBBId( header );
            m_builder.setCurrentBB( firstInductionIterationHeaderIndex );

            if( ms_TraceMode )
                cout << "  == Havocing modified addresses for loop " << header.index() << endl;

            m_cfg->forEachAddressModifiedInLoop( header.index(), [&]( auto&& type, auto&& addr )
            {
                HavocAddress( m_builder, firstInductionIterationHeaderIndex, type, addr );
            } );

            if( ms_TraceMode )
                cout << "  == Unrolling first induction case for loop " << header.index() << endl;

|

68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

            m_remapper.nextLoopIteration();
            uint32_t firstInductionIterationHeaderIndex = m_remapper.remapBBId( header );
            m_builder.setCurrentBB( firstInductionIterationHeaderIndex );

            if( ms_TraceMode )
                cout << "  == Havocing modified addresses for loop " << header.index() << endl;

            m_cfg->forEachAddressModifiedByLoop( header.index(), [&]( auto&& type, auto&& addr )
            {
                HavocAddress( m_builder, firstInductionIterationHeaderIndex, type, addr );
            } );

            if( ms_TraceMode )
                cout << "  == Unrolling first induction case for loop " << header.index() << endl;