1
2
3
4
5
6
7
8
9
10
|
#include "verify.h"
#include "builtins/builtins.h"
|
<
|
1
2
3
4
5
6
7
8
9
|
#include "verify.h"
#include "builtins/builtins.h"
using namespace goose::diagnostics;
namespace goose::verify
{
bool Func::checkLoop( const llr::BasicBlock& header, queue< const BasicBlock* >& parentWorkQueue )
{
if( ms_TraceMode )
|
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
// If a counter example was found while emitting the base case,
// we know the verification failed and we can stop here.
completed = true;
break;
}
}
// Push the solver state before unrolling the induction case,
// so that we can rollback all of this for the next attempt, if any.
m_solver.push();
unordered_set< uint32_t > convertedBBIndices = m_convertedBBIndices;
// Likewise for the remapper: we don't want to keep the edge infos from the induction case unrolling,
// plus we need to keep the state to do the next unrolling of the base case correctly.
RemapperLocalStateGuard rsg( m_remapper );
// Set a different assertion handler for the induction case: we want to just emit them as assumptions.
BuilderStateGuard bsg( m_builder, [&]( const z3::expr& expr, const z3::expr& exprToCheck, uint32_t locationId )
{
m_builder.assume( expr );
return true;
} );
// Havoc all the variables modified during the current loop and emit
// the first unrolling for the induction case.
|
|
|
<
<
|
|
|
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
// If a counter example was found while emitting the base case,
// we know the verification failed and we can stop here.
completed = true;
break;
}
}
// Push the solver state, builder state and remapper before unrolling the induction case,
// so that we can rollback all of this for the next attempt, if any.
m_solver.push();
unordered_set< uint32_t > convertedBBIndices = m_convertedBBIndices;
auto savedBuilder = m_builder;
auto savedRemapper = m_remapper;
// Set a different assertion handler for the induction case: we want to just emit them as assumptions.
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, uint32_t locationId )
{
m_builder.assume( expr );
return true;
} );
// Havoc all the variables modified during the current loop and emit
// the first unrolling for the induction case.
|
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
m_remapper.nextLoopIteration();
buildZ3Expressions( header, &parentWorkQueue );
++i;
}
// For the final loop instance, we want to resolve the assertions, but without emitting diagnostics:
// if they fail it means we need to increase k and try again.
BuilderStateGuard bsg2( m_builder, [&]( const z3::expr& expr, const z3::expr& exprToCheck, uint32_t locationId )
{
if( ms_TraceMode )
return true;
z3::expr_vector exprVec( GetZ3Context() );
exprVec.push_back( exprToCheck );
bool result = m_solver.check( exprVec ) == z3::check_result::unsat;
if( ( !result && ms_DumpSolverOnFailure ) || ( result && ms_DumpSolverOnSuccess ) )
cout << "Solver dump:\n" << m_solver << "check_unsat_ind: " << exprToCheck << endl << endl;
return result;
} );
m_remapper.nextLoopIteration();
if( buildZ3Expressions( header, &parentWorkQueue ) )
{
completed = true;
break;
}
m_convertedBBIndices = move( convertedBBIndices );
m_solver.pop();
}
if( !completed )
{
// If completed is false, the verification couldn't be completed with the maxK value used.
// The whole business is undecidable so obviously there will be cases where we can't tell
// whether the program is good.
|
|
|
>
>
>
|
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
m_remapper.nextLoopIteration();
buildZ3Expressions( header, &parentWorkQueue );
++i;
}
// For the final loop instance, we want to resolve the assertions, but without emitting diagnostics:
// if they fail it means we need to increase k and try again.
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, uint32_t locationId )
{
if( ms_TraceMode )
return true;
z3::expr_vector exprVec( GetZ3Context() );
exprVec.push_back( exprToCheck );
bool result = m_solver.check( exprVec ) == z3::check_result::unsat;
if( ( !result && ms_DumpSolverOnFailure ) || ( result && ms_DumpSolverOnSuccess ) )
cout << "Solver dump:\n" << m_solver << "check_unsat_ind: " << exprToCheck << endl << endl;
return result;
} );
m_remapper.nextLoopIteration();
if( buildZ3Expressions( header, &parentWorkQueue ) && !m_builder.hasCheckFailed() )
{
completed = true;
break;
}
m_convertedBBIndices = move( convertedBBIndices );
m_solver.pop();
m_remapper = move( savedRemapper );
m_builder = move( savedBuilder );
}
if( !completed )
{
// If completed is false, the verification couldn't be completed with the maxK value used.
// The whole business is undecidable so obviously there will be cases where we can't tell
// whether the program is good.
|