1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
+
-
+
|
#include "verify.h"
#include "builtins/builtins.h"
#include "helpers.inl"
using namespace goose::diagnostics;
namespace goose::verify
{
template< bool CheckResult, typename I >
bool BuildZ3Op( Builder& b, const Call& instr )
bool BuildZ3CallCheck( Builder& b, const I& instr )
{
Value ft;
auto fVal = b.pop< Value >();
if( fVal )
ft = *EIRToValue( fVal->type() );
else
|
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
+
+
+
-
-
+
+
+
|
return false;
auto fvi = fvd->verifInfos;
if( !fvi )
return false;
optional< Z3Val > retExpr;
if constexpr( CheckResult )
{
if( fvd->returnType != GetValueType< void >() )
retExpr = BuildZ3ConstantFromType( b, fvd->returnType, format( "r{}", b.newUniqueId() ) );
if( fvd->returnType != GetValueType< void >() )
retExpr = BuildZ3ConstantFromType( b, fvd->returnType, format( "r{}", b.newUniqueId() ) );
}
// Create a temporary builder to construct the z3 expressions out of the
// function's pre-conditions and postconditions, configured
// to perform the necessary replacements for arguments and for the
// return value placeholder.
Builder cb = b;
|
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
115
116
117
118
119
120
121
|
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
+
+
-
-
-
+
+
+
+
+
+
-
-
-
-
-
+
+
+
+
+
-
-
-
-
-
-
-
+
+
+
+
+
+
+
-
-
+
+
+
+
-
+
+
+
+
+
+
+
+
+
+
+
|
DiagnosticsContext dc( fVal->locationId(), "At this call." );
b.checkAssertion( z3expr, locId );
} );
return true;
} );
if constexpr( CheckResult )
{
// Setup the return value placeholder
if( retExpr )
cb.setPlaceholder( "@result"_sid, retExpr->expr );
// Setup the return value placeholder
if( retExpr )
cb.setPlaceholder( "@result"_sid, retExpr->expr );
}
// Check preconditions.
const auto& preConds = fvi->preConds();
preConds->forEach( [&]( auto&& val )
{
if( auto zv = TryBuildZ3ExprFromValue( cb, val ) )
{
DiagnosticsContext dc( fVal->locationId(), "At this call." );
b.checkAssertion( zv->expr, val.locationId() );
}
} );
if constexpr( CheckResult )
{
// Add the return type's predicates as assumptions.
ForEachPredicate( cb, fvd->returnType, retExpr->expr, [&]( auto&& z3expr, auto locId )
{
b.assume( z3expr );
} );
// Add the return type's predicates as assumptions.
ForEachPredicate( cb, fvd->returnType, retExpr->expr, [&]( auto&& z3expr, auto locId )
{
b.assume( z3expr );
} );
// Add postconditions as assumptions.
const auto& postConds = fvi->postConds();
postConds->forEach( [&]( auto&& val )
{
if( auto zv = TryBuildZ3ExprFromValue( cb, val ) )
b.assume( zv->expr );
} );
// Add postconditions as assumptions.
const auto& postConds = fvi->postConds();
postConds->forEach( [&]( auto&& val )
{
if( auto zv = TryBuildZ3ExprFromValue( cb, val ) )
b.assume( zv->expr );
} );
if( retExpr )
b.push( move( *retExpr ) );
if( retExpr )
b.push( move( *retExpr ) );
}
return true;
}
}
|