53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
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 addresses modified during the current loop and emit
// the first unrolling for the induction case.
|
|
|
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
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, LocationId locationId )
{
m_builder.assume( expr );
return true;
} );
// Havoc all the addresses modified during the current loop and emit
// the first unrolling for the induction case.
|
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
// For the final loop instance, if we aren't at the last value of k before giving up,
// we want to resolve the assertions without emitting diagnostics:
// if they fail it means we need to increase k and try again.
// Otherwise, we want to use the regular assertion handler that will emit error
// messages for all failed assertions.
if( k == maxK )
{
m_builder.setAssertionHandler( [&]( auto&& expr, auto&& exprToCheck, uint32_t locationId )
{
return checkAssertion( expr, exprToCheck, locationId );
} );
}
else
{
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;
|
|
|
|
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
// For the final loop instance, if we aren't at the last value of k before giving up,
// we want to resolve the assertions without emitting diagnostics:
// if they fail it means we need to increase k and try again.
// Otherwise, we want to use the regular assertion handler that will emit error
// messages for all failed assertions.
if( k == maxK )
{
m_builder.setAssertionHandler( [&]( auto&& expr, auto&& exprToCheck, LocationId locationId )
{
return checkAssertion( expr, exprToCheck, locationId );
} );
}
else
{
m_builder.setAssertionHandler( [&]( const z3::expr& expr, const z3::expr& exprToCheck, LocationId 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;
|