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
30
31
32
33
34
35
36
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
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
30
31
32
33
34
35
36
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
-
+
-
+
-
+
+
+
+
-
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
-
+
-
+
-
+
-
+
-
+
|
#include "verify.h"
#include "builtins/builtins.h"
using namespace goose::diagnostics;
namespace goose::verify
{
bool Func::checkLoop( const llr::BasicBlock& bb, queue< const BasicBlock* >& parentWorkQueue )
bool Func::checkLoop( const llr::BasicBlock& header, queue< const BasicBlock* >& parentWorkQueue )
{
if( ms_TraceMode )
cout << " == Checking loop " << bb.index() << endl;
cout << " == Checking loop " << header.index() << endl;
m_remapper.beginLoopUnrolling( bb.index() );
m_remapper.beginLoopUnrolling( header.index() );
bool completed = false;
uint32_t k = 0;
// Max K is hardcoded for now. Maybe we'll allow it to be changed per function.
// Or maybe we won't limit K but rather the number of expressions added to the solver
// (so that we have a limit that works consistently regardless of loop nesting depth)
uint32_t maxK = 16;
while( !completed && k < maxK )
{
++k;
{
DiagnosticsContext dc( header.locationId(), "In this loop." );
// Unroll the base case just once for each increasing K: we save the state of the z3 solver
// before generating the induction case, so we can incrementally add unrolling of the base
// case one at a time to save some work.
m_remapper.nextLoopIteration();
if( !buildZ3Expressions( bb, &parentWorkQueue ) )
{
// If a counter example was found while emitting the base case,
// we know the verification failed and we can stop here.
completed = true;
break;
// Unroll the base case just once for each increasing K: we save the state of the z3 solver
// before generating the induction case, so we can incrementally add unrolling of the base
// case one at a time to save some work.
m_remapper.nextLoopIteration();
if( !buildZ3Expressions( header, &parentWorkQueue ) )
{
// 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 asumptions.
// 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.
m_remapper.nextLoopIteration();
uint32_t firstInductionIterationHeaderIndex = m_remapper.remapBBId( bb );
uint32_t firstInductionIterationHeaderIndex = m_remapper.remapBBId( header );
m_cfg->forEachVariableModifiedInLoop( bb.index(), [&]( auto&& type, uint32_t varId )
m_cfg->forEachVariableModifiedInLoop( header.index(), [&]( auto&& type, uint32_t varId )
{
m_builder.havocVar( firstInductionIterationHeaderIndex, type, varId );
} );
buildZ3Expressions( bb, &parentWorkQueue );
buildZ3Expressions( header, &parentWorkQueue );
// Emit the rest of the induction case.
uint32_t i = 1;
while( i < k )
{
m_remapper.nextLoopIteration();
buildZ3Expressions( bb, &parentWorkQueue );
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 )
{
|
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
115
116
117
118
119
120
121
122
123
124
125
126
127
|
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
-
+
-
+
-
-
-
-
+
-
+
|
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( bb, &parentWorkQueue ) )
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.
//
// Perhaps instead of this we should display the assertion that failes at max K as an indication
// Perhaps instead of this we should display the assertion that failed at max K as an indication
// of what might be wrong.
//
// TODO: we also need a location for that... Maybe let the loop parser set a proper location id in the loop header?
// (like at the loop key word + the condition?)
DiagnosticsManager::GetInstance().emitErrorMessage( 0,
cout << " == Finished checking loop " << bb.index() << endl;
cout << " == Finished checking loop " << header.index() << endl;
return completed && !m_builder.hasCheckFailed();
}
}
|