Goose  Diff

Differences From Artifact [c19b774202]:

  • File bs/verify/loop.cpp — part of check-in [b4385d9930] at 2019-11-04 19:53:00 on branch trunk — Verifier: more work on loop verification. (user: achavasse size: 212)

To Artifact [c318dca5f2]:

  • File bs/verify/loop.cpp — part of check-in [f7c8245cb2] at 2019-11-16 16:27:32 on branch trunk —
    • while: remove code attempting to detect infinite loops, this will be best left to the verifier.
    • verifier: loop unrolling now works.
    (user: achavasse size: 871)

1
2
3
4
5
6
7



















8
9
10
#include "verify.h"
#include "builtins/builtins.h"

namespace goose::verify
{
    bool Func::checkLoop( const llr::BasicBlock& bb, queue< const BasicBlock* >& parentWorkQueue )
    {



















        return true;
    }
}







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>



1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
#include "verify.h"
#include "builtins/builtins.h"

namespace goose::verify
{
    bool Func::checkLoop( const llr::BasicBlock& bb, queue< const BasicBlock* >& parentWorkQueue )
    {
        if( ms_TraceMode )
            cout << "  == Checking loop " << bb.index() << endl;

        // Just try to unroll the loop a few times for now so we can check that
        // everything gets linker together properly
        m_remapper.beginLoopUnrolling( bb.index() );

        buildZ3Expressions( bb, &parentWorkQueue );

        m_remapper.nextLoopIteration();
        buildZ3Expressions( bb, &parentWorkQueue );

        m_remapper.nextLoopIteration();
        buildZ3Expressions( bb, &parentWorkQueue );

        m_remapper.endLoopUnrolling();

        if( ms_TraceMode )
            cout << "  == Finished checking loop " << bb.index() << endl;
        return true;
    }
}