1
2
3
4
5
6
7
8
9
|
1
2
3
4
5
6
7
8
9
10
11
12
|
+
+
+
|
#include "verify.h"
#include "builtins/builtins.h"
#include "helpers.inl"
using namespace goose::diagnostics;
namespace goose::verify
{
optional< Z3Val > BuildZ3ValFromConstant( const Value& val )
{
auto& c = GetZ3Context();
auto type = *ValueFromIRExpr( val.type() );
|
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
-
+
+
+
+
+
+
+
+
+
+
|
return Z3Val{ *expr, *ValueFromIRExpr( instr.type() ) };
return BuildZ3ConstantFromType( instr.type(), format( "v{}", instr.index() ) );
}
optional< Z3Val > BuildZ3Op( Builder& b, const SetVar& instr )
{
b.setVar( instr.index(), instr.value() );
const auto* zv = b.setVar( instr.index(), instr.value() );
// Assert the type's predicates.
ForEachPredicate( b, instr.value().type(), *zv, [&]( auto&& b, auto&& z3expr, auto locId )
{
// TODO: the locId that we pass here is actually that of the rhs expression of
// the assignment. Maybe we should just store the locid of the variable in the instr.
DiagnosticsContext dc( instr.value().locationId(), "When setting this variable." );
b.checkAssertion( z3expr, locId );
} );
return nullopt;
}
// Implemented in phi.cpp
optional< Z3Val > BuildZ3Op( Builder& b, const Phi& instr );
// TODO: LoadConstStr. Build a z3 str value.
|